LEAN写経　応用情報数理学特論　第０８回

千葉大学 萩原先生の 応用情報数理学特論　第０８回 の演習をLean4で写経してみる．

演習08-01

-- 目標１．Nat as ℕ 
-- 目標２．Int as ℤ
-- 目標３．/- -/ 
/- 
  x + y  足し算
  x - y  引き算（ ℤ ）
  x * y  掛け算
  -x     加法の逆元（ ℤ ）
  #eval  計算結果の表示
-/

#eval 1 + 1
#eval 3 * 10
#eval (-2 : Int)
#eval 1 - 2 -- 0 になる．型が自然数(Nat)のため．
#eval (1 : Int) - (2 : Int)
#eval (1 : Int) + (-2 : Int)

#eval -2 -- Lean4 では -2 は Int として扱われる（怒られない）
#eval -2 + 1 -- -1 になる．最初に評価される -2 が Int として扱われ，その後の1も Int として扱われる．

演習08-02

/- 
  目標１．
    add_zero       x + 0 = x
    zero_add       0 + x = x
    add_assoc      (x + y) + z = x + (y + z)
    add_comm       x + y = y + x
    mul_one        x * 1 = x
    one_mul        1 * x = x
    mul_assoc      (x * y) * z = x * (y * z)
    mul_comm       x * y = y * x
    left_distrib   x * (y + z) = x * y + x * z
    right_distrib  (x + y) * z = x * z + y * z
    add_left_neg   -a + a = 0
    add_right_neg  a + -a = 0
    sub_eq_add_neg a - b = a + -b
    refl           利用例として：具体的な整数の計算を実行
-/
import Mathlib.Data.Int.Basic -- Lean4 で，Intに対して上記の定理を使うには，Mathlibをimportする必要がある．

example (i j : Int) : i - j = -j + i := by
  calc i - j 
  _ = i + -j := sub_eq_add_neg i j
  _ = -j + i := add_comm i (-j)

example : (5 + 2) * (2 * 3 + 1) = 7 * 7 := rfl

-----------------------------------------
-- 以下は，Mathlibをimportしない場合
#check add_zero -- unknown identifier 'add_zero'
-- add_zero はない
#check Nat.add_zero -- Nat.add_zero (n : Nat) : n + 0 = n
#check Int.add_zero -- unknown constant 'Int.add_zero'
-- Nat.add_zero はあるようだが，Int.add_zero はない．．．
-- このように Int に関する定理は，Mathlibをimportしないと使えない．

レポート課題

-- Logic and Proof https://lean-lang.org/logic_and_proof/
-- 9.5 Exercices
import Mathlib.Data.Int.Basic

-- 3
section
  variable (U : Type)
  variable (A B C : U → Prop)

  variable (h1 : ∀ x, A x ∨ B x)
  variable (h2 : ∀ x, A x → C x)
  variable (h3 : ∀ x, B x → C x)

  example : ∀ x, C x := by
    intro x
    cases h1 x with
    | inl h => exact h2 x h
    | inr h => exact h3 x h
end
-- 6
section
  variable (U : Type)
  variable (A B : U → Prop)

  variable (h1 : ∀ x, A x → B x)
  variable (h2 : ∃ x, A x)

  example : ∃ x, B x := by
    apply Exists.elim h2 
    intro x h3
    apply Exists.intro x
    apply h1 x h3
end
-- 8
section
  variable (U : Type)
  variable (A B C : U → Prop)

  example : (¬ ∃ x, A x) → ∀ x, ¬ A x := by
    intro h1
    intro x
    intro h2
    apply h1
    apply Exists.intro x
    exact h2
    
  example : (∀ x, ¬ A x) → ¬ ∃ x, A x := by
    intro (h1 : ∀ x, ¬ A x)
    intro (h2 : ∃ x, A x)
    apply Exists.elim h2
    intro x h3
    apply h1 x
    exact h3
end
-- 9
section
  variable (U : Type)
  variable (R : U → U → Prop)

  example : (∃ x, ∀ y, R x y) → ∀ y, ∃ x, R x y := by
    intro (h1 : ∃ x, ∀ y, R x y)
    intro y -- 適当な y をとって goal を ∃ x, R x y にする
    apply Exists.elim h1
    intro x (h2 : ∀ y, R x y)
    apply Exists.intro x
    exact h2 y
end
-- 11
-- these are the axioms for a commutative ring
#check @add_assoc
#check @add_comm
#check @add_zero
#check @zero_add
#check @mul_assoc
#check @mul_comm
#check @mul_one
#check @one_mul
#check @left_distrib
#check @right_distrib
#check @add_left_neg
#check @add_right_neg
#check @sub_eq_add_neg

section
  variable (x y z : Int)

  theorem t1 : x - x = 0 := by
    calc x - x 
    _ = x + -x := sub_eq_add_neg x x
    _ = 0      := add_right_neg x

  theorem t2 (h : x + y = x + z) : y = z := by
    calc y 
    _ = 0 + y        := by rw [zero_add]
    _ = (-x + x) + y := by rw [add_left_neg]
    _ = -x + (x + y) := by rw [add_assoc]
    _ = -x + (x + z) := by rw [h]
    _ = (-x + x) + z := by rw [add_assoc]
    _ = 0 + z        := by rw [add_left_neg]
    _ = z            := by rw [zero_add]

  theorem t3 (h : x + y = z + y) : x = z := by
    calc x
    _ = x + 0        := by rw [add_zero]
    _ = x + (y + -y) := by rw [add_right_neg]
    _ = (x + y) + -y := by rw [add_assoc]
    _ = (z + y) + -y := by rw [h]
    _ = z + (y + -y) := by rw [add_assoc]
    _ = z + 0        := by rw [add_right_neg]
    _ = z            := by rw [add_zero]

  theorem t4 (h : x + y = 0) : x = -y := by
    calc x
    _ = x - 0           := by rw [sub_zero]
    _ = x - (x + y)     := by rw [h]
    _ = x + -(x + y)    := by rw [sub_eq_add_neg]
    _ = x + (-x + -y)   := by rw [neg_add]
    _ = (x + -x) + -y   := by rw [add_assoc]
    _ = 0 + -y          := by rw [add_right_neg]
    _ = -y              := by rw [zero_add]

  theorem t5 : x * 0 = 0 := by
    have h1 : x * 0 + x * 0 = x * 0 + 0 := by
      calc x * 0 + x * 0 
      _ = x * (0 + 0) := by rw [mul_add]
      _ = x * 0       := by rw [add_zero]
      _ = x * 0 + 0   := by rw [add_zero]
    apply t2 -- ?x + x * 0 = ?x + 0
    exact h1 -- ?x = x * 0 とすればよい

  theorem t6 : x * (-y) = -(x * y) := by
    have h1 : x * (-y) + x * y = 0 := by
      calc x * (-y) + x * y 
      _ = x * (-y + y) := by rw [mul_add]
      _ = x * 0        := by rw [add_left_neg]
      _ = 0            := by rw [t5]
    apply t4
    exact h1

  theorem t7 : x + x = 2 * x := by
    calc x + x 
      _ = 1 * x + 1 * x := by rw [one_mul]
      _ = (1 + 1) * x   := by rw [add_mul]
      _ = 2 * x         := rfl
end