Lean4 学習5 - ushumpei’s blog

Inductive Types の Exercises の exponentiation の実装。

色々感じが掴めてきて rw、simp を使わないでかけるようになってきた

Eq.refl に何か渡すことで 何か = 何かの評価 の等式が得られる
Eq.refl は自動的に解決されるので calc の Eq.refl の行は本来不要 (不安だから自分は書いている)
関数定義で変な場合わけを書くと Eq.refl で機能しなくなる
- Eq.refl は帰納型の定義に基づいてなんかしているのだろうか？
- まずは自分が定義した性質を rfl で証明できることを確かめると良さそう、今回でいう pow_succ、pow_zero
式を部分的に変更したい場合は congrArg を使えばよくて、第一引数に無名関数、第二引数に Eq を渡す
:= fun n => match n with は省略可能な時があるっぽい
a < b は b > a と同じっぽい (定義を見にいくと reducible が付いていたからそれのおかげ？)
数学的帰納法は明示しなくても使えるっぽい？ (pow_le_pow_of_le_left の証明)
- 数学的帰納法というより証明を再帰的に行える？なんか対応してそう

  open Nat
  def my_pow (n : Nat): Nat → Nat 
  | 0 => 1
  -- | 1 => n -- ここに変な定義を入れてしまうと `Eq.refl` が機能しなくなる
  | succ m => (my_pow n m) * n

  def instPow : Pow Nat Nat := { pow := my_pow }
  attribute [local instance] instPow

  theorem pow_succ (n m : Nat) : n^(succ m) = n^m * n := Eq.refl (n^(succ m))
  theorem pow_zero (n : Nat) : n^0 = 1 := Eq.refl (n^0)
  theorem pow_le_pow_of_le_left {n m : Nat} (h : n ≤ m) : ∀ (i : Nat), n^i ≤ m^i := fun i => match i with
    | 0 =>
      calc n^0
      _ = 1   := Eq.refl (n^0)
      _ ≤ 1   := Nat.le_refl 1
      _ = m^0 := Eq.symm (Eq.refl (m^0))
    | i + 1 =>
      calc n^(i+1)
      _ = n^i * n := Eq.refl (n^(i+1))
      _ ≤ m^i * m := Nat.mul_le_mul (pow_le_pow_of_le_left h i) h
  theorem pow_le_pow_of_le_right {n : Nat} (hx : n > 0) {i : Nat} : ∀ {j}, i ≤ j → n^i ≤ n^j
    | 0, h =>
      have _ : i = 0 := (Nat.le_zero_eq i).mp h
      calc n^i
      _ = n^0 := congrArg (n^·) ‹i = 0› 
      _ ≤ n^0 := Nat.le_refl (n^0) 
    | j + 1, h =>
      match Nat.le_or_eq_of_le_succ h with
      | Or.inr h =>
        calc n^i
        _ = n^(j+1) := congrArg (n^·) h
        _ ≤ n^(j+1) := Nat.le_refl (n^(j+1))
      | Or.inl h => 
        -- n > 0 は 0 < n と同じ、というルールがある
        have _ : 1 ≤ n := Nat.succ_le_of_lt hx
        calc n^i
        _ = (n^i) * 1 := Eq.symm (Nat.mul_one (n^i))
        _ ≤ (n^j) * n := Nat.mul_le_mul (pow_le_pow_of_le_right hx h) ‹1 ≤ n› 
        _ = n^(j+1)   := Eq.symm (Eq.refl (n^(j+1)))
  theorem pos_pow_of_pos {n : Nat} (m : Nat) (h : 0 < n) : 0 < n^m :=
    match m with
    | 0 =>
      calc 0
      _ < 1 := Nat.zero_lt_one
      _ = n^0 := Eq.refl (n^0)
    | m+1 =>
        calc 0
        _ < (n^m)     := pos_pow_of_pos m h
        _ = (n^m) * 1 := Eq.symm (Nat.mul_one (n^m))
        _ ≤ (n^m) * n := Nat.mul_le_mul_left (n^m) (Nat.succ_le_of_lt h)
        _ = n^(m+1)   := Eq.symm (Eq.refl (n^(m+1)))

感想

慣れてきたのでそろそろ以下のことがしてみたい
- Mathlib を使って微分幾何とかやってみる
- 世の中にありそうなプログラムの検証を行う
定理証明支援系で証明した関数を他のプログラム言語に抽出する、という利用方法があるらしい: https://onct.oita-ct.ac.jp/seigyo/nishimura_hp/pdf/2017watanabe.pdf
- Lean4 だとどうか、とか自分の書ける各言語と相性のいい定理証明支援系はなんだ？とか調べたい
rfl とか rw とか simp とかはなくても書けることがわかったので、使ってもいいような気もしてきた
シンタックスシュガーがありすぎて使うべきかどうか迷う
コードのシンタックスハイライト見つからなかったので haskell のやつ使っている