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

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

演習06-01

-- 目標１．(variable of type) → Prop
-- 目標２．Nat
variable (U : Type)
variable (u : U)
variable (A : U → Prop)

-- A は U から Prop への関数なので A u は Prop である．
#check A u

-- B は Prop から Prop への関数
variable (B : Prop → Prop)
#check B (A u)

variable (C : Nat → Prop)
#check C 0
#check C 1

演習06-02

-- 目標１．∀
variable (U : Nat → Prop) -- Nat は ℕ 

example (n : Nat) : U n → U n :=
  fun h => h
-- この書き方では n が自然数であることが仮定（コロンの左側）になっている．

example : ∀ n : Nat, U n → U n := by
  intro (n : Nat) -- intro n だけでもよい
  intro (h : U n) -- intro h だけでもよい
  exact h
-- n をコロンの右側に移動している．

example : ∀ a : Nat, U a → U a := by
  intro (b : Nat)
  intro (h : U b)
  exact h

演習06-03

-- 目標１．∀に慣れる
variable (U : Type)
variable (P Q : U → Prop)

example : ∀ x : U, P x → (P x → Q x) → Q x := by
  intro (a : U)
  intro (h : P a)
  intro (f : P a → Q a)
  exact f h

example : (∀ x : U, P x) → (∀ y : U, P y → Q y) → (∀ z : U, Q z) := by
  intro (h₁ : ∀ x : U, P x)
  intro (h₂ : ∀ y : U, P y → Q y)
  intro (z : U)
  have Pz : P z := h₁ z
  have PzQz : P z → Q z := h₂ z
  exact PzQz Pz

演習06-04

-- 目標１．∃
-- 目標２．Exists.intro
-- 目標３．Exists.elim
variable (U : Type)
variable (P : U → Prop)

#check Exists.intro -- 任意の a に P a が成り立つことを仮定して，∃ x, P x を導く
example : ∀ a : U, P a → ∃ x : U, P x := by
  intro (a : U)
  intro (h : P a)
  apply Exists.intro a h

#check Exists.elim
example : (∃ u, ¬ P u) → (∀ x, P x) → False := by
  intro (h₁ : ∃ u, ¬ P u)
  intro (h₂ : ∀ x, P x)
  apply Exists.elim h₁ -- h₁ の ∃ を消す．
  intro (a : U)
  intro (nPa : ¬ P a)
  have Pa : P a := h₂ a
  apply False.elim (nPa Pa) -- contradiction でもよい