これまでの記事では、広義の順序関係 \( a \le b \) を定義し、\( n \le m \leftrightarrow \exists k,\ n + k = m \) という和の形での同値な特徴付けを示しました。今回はこの広義順序をもとに狭義順序 \( a < b \) を定義し、最終的に「任意の2つの自然数について、一方が他方以下である」という全順序性（Totality、完全律）を証明していきます。教材には引き続き「ゼロから始めるLean言語入門 手を動かして学ぶ形式数学ライブラリ開発」です。
狭義順序の定義
狭義順序は \( m < n \leftrightarrow (m + 1) \le n \) として、既に定義済みの広義順序を使って定義します。
-- m < n
def MyNat.lt (m n : MyNat) : Prop := (m + 1) <= n
-- enable to use a < b representation
instance : LT MyNat where
lt := MyNat.ltこの定義が実際に \( (m+1) \le n \) と等価であることは、定義の展開（dsimp）と反射律だけで証明できます。
example (m n : MyNat) : m < n <-> (m + 1) <= n := by
dsimp [(· < ·),MyNat.lt]
rflここで使っている (· < ·) は無名関数記法（anonymous function notation）で、fun a b => a < b の省略形です。
今回の目標—全順序性
狭義順序と広義順序の関係を補題として積み上げながら、最終的に定理 \( a \le b \lor b \le a \) を証明します。これは「任意の自然数 \( a \) と \( b \) を持ってきたとき、\( a \) は \( b \) 以下であるか、あるいは \( b \) は \( a \) 以下であるかの少なくとも一方が必ず成り立つ」ことを表す、順序の完全性（Totality）です。
補題1: 0と1は異なる
まずは当然の主張である「0と1は異なる」ことを証明し、simpに登録しておきます。もし \( 1 = 0 \) が成り立つと仮定すると、MyNatの定義である単射性が守れなくなるため、injectionタクティクで矛盾を導けます。
@[simp] theorem MyNat.one_neq_zero : 1 ≠ 0 := by
intro h
-- h : 1 = 0 ⊢ False
injection h
@[simp] theorem MyNat.zero_neq_one : 0 ≠ 1 := by
intro h
injection h補題2: 任意の自然数は0以上
次に、任意の自然数がゼロ以上であることを証明し、simpに登録します。順序を和の形に変形すれば簡単に示せます。
@[simp] theorem MyNat.zero_le (n : MyNat) : 0 <= n := by
rw [MyNat.le_iff_add] -- ⊢ ∃ k, 0 + k = n
exists n -- ⊢ 0 + n = n
simp補題3: 0以下の自然数は0のみ
0以下の自然数が0しかないことも、数学的帰納法と和の形への変換によって証明できます。
-- The only natural number less than or equal to 0 is 0.
theorem MyNat.zero_of_le_zero {n : MyNat} (h : n <= 0) : n = 0 := by
induction n with
| zero => rfl
| succ n ih =>
-- ih : n <= 0 → n = 0
-- h : n + 1 <= 0
-- ⊢ n + 1 = 0
exfalso
rw [MyNat.le_iff_add] at h
-- ih : n <= 0 → n = 0
-- h : ∃ k, n + 1 + k = 0
-- ⊢ False
obtain ⟨k, hk⟩ := h
simp_all
@[simp] theorem MyNat.le_zero {n : MyNat} : n <= 0 <-> n = 0 := by
constructor <;> intro h
· apply MyNat.zero_of_le_zero h
· simp [h]補題4: 任意の自然数はゼロまたは正
「任意の自然数がゼロまたは正である」ことも証明します。これも数学的帰納法と和の形への変換を使えば、simpで閉じられる形に持ち込めます。
theorem MyNat.eq_zero_or_pos (n : MyNat) : n = 0 ∨ 0 < n := by
induction n with
| zero =>
simp
| succ n ih => -- ih : n = 0 ∨ 0 < n ⊢ n + 1 = 0 ∨ 0 < n + 1
dsimp [(· < ·), MyNat.lt] at *
-- ih : n = 0 ∨ 0 + 1 <= n ⊢ n + 1 = 0 ∨ 0 + 1 <= n + 1
cases ih with
| inl ih => -- ih : n = 0 ⊢ n + 1 = 0 ∨ 0 + 1 <= n + 1
simp_all
| inr ih => -- ih : 0 + 1 <= n ⊢ n + 1 = 0 ∨ 0 + 1 <= n + 1
simp_all [MyNat.le_step]補題5: n <= m <-> n = m ∨ n < m
最後の補題は、狭義順序と広義順序の意味を直接結びつける \( n \le m \leftrightarrow n = m \lor n < m \) です。これも順序を和の形に直すことで証明できます。
theorem MyNat.eq_or_lt_of_le {m n : MyNat} : n <= m -> n = m ∨ n < m := by
intro h
dsimp [(· < ·), MyNat.lt]
-- h : n <= m ⊢ n = m ∨ n + 1 <= m
rw [MyNat.le_iff_add] at *
-- h : ∃ k, n + k = m ⊢ n = m ∨ ∃ k, n + 1 + k = m
obtain ⟨k, hk⟩ := h
induction k with
| zero => simp_all
| succ k _ =>
have : ∃ k, n + 1 + k = m := by
exists k
rw [← hk]
ac_rfl
simp_all
theorem MyNat.le_of_lt {a b : MyNat} (h : a < b) : a <= b := by
dsimp [(· < ·), MyNat.lt] at h
have : a <= b := calc
_ <= a + 1 := by simp
_ <= b := by assumption
-- h : a + 1 <= b
-- this : a <= b
-- ⊢ a <= b
assumption
theorem MyNat.le_of_eq_or_lt {m n : MyNat} : n = m ∨ n < m -> n <= m := by
intro h
cases h with
| inl h =>
rw [h]
| inr h =>
exact MyNat.le_of_lt h
theorem MyNat.le_iff_eq_or_lt {m n : MyNat} : n <= m <-> n = m ∨ n < m := by
constructor
· apply MyNat.eq_or_lt_of_le
· apply MyNat.le_of_eq_or_lta < b ∨ b <= a の証明
ここまでの補題を組み合わせ、帰納法を使って \( a < b \lor b \le a \) を証明します。
theorem MyNat.lt_or_ge (a b : MyNat) : a < b ∨ b <= a := by
dsimp [(· < ·), MyNat.lt]
-- ⊢ a + 1 <= b ∨ b <= a
induction a with
| zero =>
suffices 1 <= b ∨ b <= 0 from by
simp_all
have : b = 0 ∨ 0 < b := MyNat.eq_zero_or_pos b
dsimp [(· < ·), MyNat.lt] at this
-- this : b = 0 ∨ 0 + 1 <= b ⊢ 1 <= b ∨ b <= 0
cases this <;> simp_all
-- if b = 0 → b <= 0
-- if 0 + 1 <= b → 1 <= b
| succ a ih =>
-- ih : a + 1 <= b ∨ b <= a ⊢ a + 1 + 1 <= b ∨ b <= a + 1
cases ih with
| inr h =>
-- h : b <= a ⊢ a + 1 + 1 <= b ∨ b <= a + 1
right
-- h : b <= a ⊢ b <= a + 1
exact le_step h
| inl h =>
-- a + 1 <= b ⊢ a + 1 + 1 <= b ∨ b <= a + 1
simp [MyNat.le_iff_eq_or_lt] at h
-- h : a + 1 = b ∨ a + 1 < b ⊢ a + 1 + 1 <= b ∨ b <= a + 1
cases h with
| inl h =>
-- h : a + 1 = b ⊢ a + 1 + 1 <= b ∨ b <= a + 1
right
simp_all
| inr h =>
-- h : a + 1 < b ⊢ a + 1 + 1 <= b ∨ b <= a + 1
dsimp [(· < ·), MyNat.lt] at h
left
-- h : a + 1 + 1 <= b ⊢ a + 1 + 1 <= b
assumption狭義順序の別の特徴づけ
「\( a < b \)」は「\( a \le b \) かつ \( b \le a \) が成り立たない」ことと同値です。これを証明しておくと、\( \lt \) を \( \le \) と否定の組み合わせとして扱えるようになります。
-- a < b <-> a <= b ∧ ¬ b <= a
theorem MyNat.lt_of_not_le {a b : MyNat} (h : ¬ a <= b) : b < a := by
cases (MyNat.lt_or_ge b a) with
| inl h => assumption
| inr h => contradiction
theorem MyNat.not_le_of_lt {a b : MyNat} (h : a < b) : ¬ b <= a := by
intro hle
dsimp [(· < ·),MyNat.lt] at h
-- h : a + 1 <= b
-- hle : b <= a ⊢ False
rw [MyNat.le_iff_add] at *
-- h : ∃ k, a + 1 + k = b
-- hle : ∃ k, b + k = a ⊢ False
obtain ⟨k, hk⟩ := h
obtain ⟨l, hl⟩ := hle
have : a + (k + l + 1) = a := calc
_ = a + 1 + k + l := by ac_rfl
_ = b + l := by rw [hk]
_ = a := by rw [hl]
simp at this
theorem MyNat.le_iff_le_not_le (a b : MyNat) : a < b <-> a <= b ∧ ¬ b <= a := by
constructor <;> intro h
case mp => simp_all [MyNat.not_le_of_lt, MyNat.le_of_lt]
case mpr => simp_all [MyNat.lt_of_not_le]全順序性の証明
ここまでの補題が揃えば、目標だった全順序性 \( a \le b \lor b \le a \) は MyNat.lt_or_ge と MyNat.le_of_lt を組み合わせるだけで証明できます。
-- a <= b ∨ b <= a
theorem MyNat.le_total (a b : MyNat) : a <= b ∨ b <= a := by
cases (MyNat.lt_or_ge a b) <;> simp_all [MyNat.le_of_lt]これで、MyNatの広義順序と狭義順序の関係、そして全順序性まで証明できました。コードの全体は以下のリポジトリで公開しています。
0 件のコメント:
コメントを投稿