🦆
Lean 入門 (5)
Lean 入門 (4) の続きです。Theorem Proving in Lean 4 を写経しつつ読みます。
- Lean 入門(3): １〜５章
- Lean 入門(4): ４章
- Lean 入門(5): ６〜７章
- Lean 入門(6)): ８章
- Lean 入門(7): ９〜１２章
6. Interacting with Lean
Notation 関係の話です。必要になったら戻ることにしてスキップします。
7. Inductive Types
自分で型を定義する話と、帰納法、そして帰納法を使った証明に関する話。この節の演習問題をじっくり解くのが重要だと思います。
-
deriving Reprを定義に追加すると、#evalで文字列表現を表示してくれる。 - もし何かの証明をしていて、繰り返し使いそうな補題の候補が出てきたら、その部分だけ切り出して予め
theoremとして証明し、@[simp] theoremと@[simp]タグを付けておく。すると以後の証明でsimpタクティックで自動証明に使ってくれる。（後の Exercise で多用してる。）- ただし
xxx_commみたいな交換法則系はsimpが勝手に書き換えて予想外の副作用をもたらす場合があるので要注意。xxx_assocみたいなのは定義しておくと標準形に直してくれる気がする。 - 一般的には、等式系の定理は
(複雑な式) = (簡単な式、あるいは計算が進んだ式)の形で定義しておくとsimpで使いやすいかも。
- ただし
- 帰納的に証明された関数に関する証明は、
unfold {関数名},simp,rw [ih](ihは帰納法の仮定) を繰り返してると（簡単な問題なら）割と解けがち。-
inductionの仮定は強い（＝汎用性が高い）方が使い勝手が良い。だからinductionタクティックする前に、その帰納法の対象以外の変数はrevertタクティックでforallの状態に戻してからinductionする。そうすると帰納法の仮定が強くなる。 -
append (xs ys: List α)みたいなのが出てくる証明の場合、どちらの変数で帰納法を回すのかはケースバイケースとしか言いようがないが、appendの定義としてxsに関する帰納法で定義されてるので、revert ys; induction xs withで試す方が相性が良い（と思う）。
-
7.10. Exercises
1.
自然数に関する加減乗冪を定義し色々証明しろという問題。自前で my_add という加法を定義して、そこから関数や定理を増やしていきます。とりあえず加法の交換則と結合則だけ証明することを目標に。途中の補題として 0 が加法の単位元であることも示しておきます。
open Nat
def my_add (m n:Nat): Nat :=
match n with
| 0 => m
| succ n => succ (my_add m n)
#eval my_add 2 3
@[simp] theorem my_zero_add (n : Nat) : my_add 0 n = n := by
induction n with
| zero => rfl
| succ n ih => unfold my_add; rw [ih]
@[simp] theorem my_add_zero (n : Nat) : my_add n 0 = n := by
rfl
@[simp] theorem my_succ_add (n m : Nat) : my_add (succ n) m = succ (my_add n m) := by
induction m with
| zero => rfl
| succ m ihm => unfold my_add; apply succ_inj.mpr; rw [ihm]
@[simp] theorem my_add_succ (n m : Nat) : my_add n (succ m) = succ (my_add n m) := by
induction m with
| zero => rfl
| succ m ihm => unfold my_add; apply succ_inj.mpr; rw [ihm]
theorem my_add_comm (m n : Nat) : my_add n m = my_add m n := by
induction m with
| zero => rw [my_zero_add, my_add_zero]
| succ m' ihm => simp; exact ihm
@[simp] theorem my_add_assoc (l m n: Nat) : my_add (my_add l m) n = my_add l (my_add m n) := by
revert m l
induction n with
| zero => simp
| succ n' ih =>
unfold my_add; intros l m; simp; rw [ih l m]
def my_mul (n m:Nat): Nat :=
match m with
| 0 => 0
| succ m' => my_add n (my_mul n m')
#eval my_mul 3 5
def my_pred (n:Nat): Nat :=
match n with
| 0 => 0
| 1 => 0
| succ n' => n'
#eval my_pred 5
def my_sub (n m:Nat): Nat :=
match n,m with
| 0, _ => 0
| _, 0 => n
| succ n', succ m' => my_sub n' m'
#eval my_sub 3 4
#eval my_sub 5 3
def my_exp (n m:Nat): Nat :=
match m with
| 0 => 1
| succ m' => my_mul n (my_exp n m')
#eval my_exp 2 3
2.
便利な List に関する補題無しに自力で証明したかったので、自前で Lst 型を定義しています。
inductive Lst where
| nl : Lst
| cns (h : Nat) (t : Lst) : Lst
deriving Repr
variable (h:Nat)(as bs cs xs ys zs: Lst)
def my_append (as bs : Lst) : Lst :=
match as with
| Lst.nl => bs
| Lst.cns a as => Lst.cns a (my_append as bs)
@[simp] theorem my_append_nil (as: Lst) : my_append as Lst.nl = as := by
induction as with
| nl => rfl
| cns h t ih => unfold my_append; rw [ih]
@[simp] theorem my_nil_append (as: Lst) : my_append Lst.nl as = as := by
unfold my_append; rfl
@[simp] theorem my_append_head_nil : my_append (Lst.cns h Lst.nl) ys = Lst.cns h ys := by
revert h
induction ys with
| nl => unfold my_append; simp
| cns x xs ih => unfold my_append; simp
@[simp] def my_cons_append : my_append (Lst.cns h xs) ys = Lst.cns h (my_append xs ys) := by
revert h ys
induction xs with
| nl => intros ys h; simp
| cns hd tl ih => intros h ys; unfold my_append; rw [ih]
@[simp] theorem my_append_assoc0:
my_append as (my_append bs cs) = my_append (my_append as bs) cs := by
revert bs cs
induction as with
| nl => simp
| cns hd tl ih => intros bs cs; unfold my_append; rw [ih bs cs ]; simp
def my_length (xs: Lst): Nat :=
match xs with
| Lst.nl => 0
| Lst.cns hd tl => succ (my_length tl)
@[simp] theorem my_length_nl_zero : my_length Lst.nl = 0 := by
unfold my_length; rfl
@[simp] theorem my_length_cns (h:Nat)(t:Lst) : my_length (Lst.cns h t) = succ (my_length t) := by
revert h
induction t with
| nl => intro h; unfold my_length; simp
| cns hd tl ih => intro h; unfold my_length; rw [ih hd]
@[simp] theorem length_add0: my_length (my_append xs ys) = my_length xs + my_length ys := by
revert ys
induction xs with
| nl =>
intro xs; unfold my_length; simp
| cns h t ih =>
intro xs; simp; rw [ih]; rw [Nat.add_assoc]; simp +arith
def my_reverse (xs: Lst) : Lst :=
match xs with
| Lst.nl => Lst.nl
| Lst.cns h t => my_append (my_reverse t) (Lst.cns h Lst.nl)
@[simp] theorem reverse_nl0: my_reverse Lst.nl = Lst.nl := by
unfold my_reverse; rfl
#eval my_reverse (Lst.cns 1 (Lst.cns 2 (Lst.cns 3 Lst.nl)))
@[simp] theorem reverse_length_eq0: my_length (my_reverse xs) = my_length xs := by
induction xs with
| nl => unfold my_reverse; rfl
| cns h t ih => unfold my_reverse; simp; rw [ih]
@[simp] theorem reverse_cns0: my_reverse (Lst.cns h xs) = my_append (my_reverse xs) (Lst.cns h Lst.nl) := by
revert h
induction xs with
| nl => simp; unfold my_reverse; simp
| cns h' t ih => unfold my_reverse; rw [← ih]; simp
@[simp] theorem cns_reverse0: my_reverse (my_append xs (Lst.cns h Lst.nl)) = Lst.cns h (my_reverse xs) := by
revert h
induction xs with
| nl => simp
| cns hd tl ih => intro h; unfold my_reverse; simp; rw [ih]; simp
@[simp] theorem reverse_append0: my_reverse (my_append xs ys) = my_append (my_reverse ys) (my_reverse xs) := by
revert ys
induction xs with
| nl => simp
| cns hd tl ih => intro ys; simp; rw [ih];
theorem reverse_reverse0: my_reverse (my_reverse xs) = xs := by
induction xs with
| nl => unfold my_reverse; simp
| cns h t ih => simp; exact ih
3.
多項式環を定義します。eval は単純に定数項の演算だけ処理します。ここからもうちょっと式の簡約とかやろうと思ったのですが、停止性（評価が止まること、例えば必ず項の数が減るとか）を示さないとダメっぽくて、とりあえず今の時点では諦め。
inductive Term where
| const : Nat → Term -- constant
| var : Nat → Term -- variable with index=n
| plus : Term → Term → Term -- sum
| times : Term → Term → Term -- product
deriving Repr
def eval (t: Term): Term :=
match t with
| Term.const n => Term.const n
| Term.var n => Term.var n
| Term.plus s' t' =>
let es := eval s'
let et := eval t'
match es, et with
| Term.const n, Term.const m => Term.const (n+m)
| _, _ => Term.plus es et
| Term.times s' t' =>
let es := eval s'
let et := eval t'
match es, et with
| Term.const n, Term.const m => Term.const (n+m)
| _, _ => Term.times es et
#eval eval (Term.const 3) -- Term.const 3
#eval eval (Term.plus (Term.const 2) (Term.const 3)) -- Term.const 5
#eval eval (Term.plus (Term.const 2) (Term.var 3)) -- Term.plus (Term.const 2) (Term.var 3)
#eval eval (Term.plus (Term.const 1) (Term.plus (Term.const 2) (Term.const 3))) -- Term.const 6
4.
ブール代数を実装しろ、ということと理解しました。
inductive LExp where
| L_true : LExp -- constant
| L_false : LExp
| L_and : LExp -> LExp -> LExp
| L_or : LExp -> LExp -> LExp
| L_not : LExp -> LExp
deriving Repr
def L_eval (t: LExp): LExp :=
match t with
| LExp.L_and s' t' =>
let es := L_eval s'
let et := L_eval t'
match es, et with
| LExp.L_true, LExp.L_true => LExp.L_true
| LExp.L_false, _ => LExp.L_false
| _, LExp.L_false => LExp.L_false
| _, _ => LExp.L_and es et
| LExp.L_or s' t' =>
let es := L_eval s'
let et := L_eval t'
match es, et with
| LExp.L_false, LExp.L_false => LExp.L_false
| LExp.L_true, _ => LExp.L_true
| _, LExp.L_true => LExp.L_true
| _, _ => LExp.L_or es et
| LExp.L_not s' =>
let es := L_eval s'
match es with
| LExp.L_true => LExp.L_false
| LExp.L_false => LExp.L_true
| _ => LExp.L_not es
| _ => t
#eval L_eval (LExp.L_and (LExp.L_not LExp.L_false) (LExp.L_or (LExp.L_false) (LExp.L_true)))
これだけだと簡単すぎるので、追加で色々やってみます。まず、L_eval の結果が L_true か L_false になることを示します。
@[simp] theorem L_eval_terminate : ∀ t: LExp, L_eval t = LExp.L_true ∨ L_eval t = LExp.L_false := by
intro t
induction t with
| L_true => left; rfl
| L_false => right; rfl
| L_not t' ih =>
cases ih with
| inl ih => right; unfold L_eval; rw [ih]
| inr ih => left; unfold L_eval; rw [ih]
| L_and s' t' ihs iht =>
cases ihs with
| inl ihs =>
cases iht with
| inl iht => left; unfold L_eval; rw [ihs, iht]
| inr iht => right; unfold L_eval; rw [ihs, iht]
| inr ihs =>
cases iht with
| inl iht => right; unfold L_eval; rw [ihs, iht]
| inr iht => right; unfold L_eval; rw [ihs, iht]
| L_or s' t' ihs iht =>
cases ihs with
| inl ihs =>
cases iht with
| inl iht => left; unfold L_eval; rw [ihs, iht]
| inr iht => left; unfold L_eval; rw [ihs, iht]
| inr ihs =>
cases iht with
| inl iht => left; unfold L_eval; rw [ihs, iht]
| inr iht => right; unfold L_eval; rw [ihs, iht]
ついで、LExp を Bool 型の式に変換する関数を作ります。不要かもしれないのですが、評価を 1-step 進める書き換え規則を定義しておきます。
def LExp_to_Bool (t: LExp) : Bool :=
match t with
| LExp.L_true => true
| LExp.L_false => false
| LExp.L_and s' t' => Bool.and (LExp_to_Bool s') (LExp_to_Bool t')
| LExp.L_or s' t' => Bool.or (LExp_to_Bool s') (LExp_to_Bool t')
| LExp.L_not s' => Bool.not (LExp_to_Bool s')
@[simp] theorem LExp_to_Bool_not: ∀ t:LExp, LExp_to_Bool (LExp.L_not t) = Bool.not (LExp_to_Bool t) := by
intro t; rfl
@[simp] theorem LExp_to_Bool_and: ∀ s t:LExp, LExp_to_Bool (LExp.L_and s t) = Bool.and (LExp_to_Bool s) (LExp_to_Bool t) := by
intro s t; rfl
@[simp] theorem LExp_to_Bool_or: ∀ s t:LExp, LExp_to_Bool (LExp.L_or s t) = Bool.or (LExp_to_Bool s) (LExp_to_Bool t) := by
intro s t; rfl
最後に、L_eval の評価が Bool の評価を一致してることを証明します。といっても、L_eval_terminate で場合分けして、同じような処理してるだけですが。
@[simp] theorem LExp_eq_Bool : ∀ t: LExp, LExp_to_Bool (L_eval t) = LExp_to_Bool t := by
intro t
induction t with
| L_true => unfold L_eval; rfl
| L_false => unfold L_eval; rfl
| L_not t' ih =>
have h: L_eval t' = LExp.L_true ∨ L_eval t' = LExp.L_false := by simp
cases h with
| inl h' =>
unfold L_eval; rw [h']; rw [h'] at ih;
simp; rw [← ih]; rfl
| inr h' =>
unfold L_eval; rw [h']; rw [h'] at ih;
simp; rw [← ih]; rfl
| L_and s' t' ihs iht =>
have hs: L_eval s' = LExp.L_true ∨ L_eval s' = LExp.L_false := by simp
have ht: L_eval t' = LExp.L_true ∨ L_eval t' = LExp.L_false := by simp
cases hs with
| inl hs' =>
cases ht with
| inl ht' =>
unfold L_eval; rw [hs', ht'];
rw [hs'] at ihs; rw [ht'] at iht; simp;
rw [← ihs, ← iht]; rfl
| inr ht' =>
unfold L_eval; rw [hs', ht'];
rw [hs'] at ihs; rw [ht'] at iht; simp;
rw [← ihs, ← iht]; rfl
| inr hs' =>
cases ht with
| inl ht' =>
unfold L_eval; rw [hs', ht'];
rw [hs'] at ihs; rw [ht'] at iht; simp;
rw [← ihs, ← iht]; rfl
| inr ht' =>
unfold L_eval; rw [hs', ht'];
rw [hs'] at ihs; rw [ht'] at iht; simp;
rw [← ihs, ← iht]; rfl
| L_or s' t' ihs iht =>
have hs: L_eval s' = LExp.L_true ∨ L_eval s' = LExp.L_false :=
L_eval_terminate s'
have ht: L_eval t' = LExp.L_true ∨ L_eval t' = LExp.L_false :=
L_eval_terminate t'
cases hs with
| inl hs' =>
cases ht with
| inl ht' =>
unfold L_eval; rw [hs', ht'];
rw [hs'] at ihs; rw [ht'] at iht; simp;
rw [← ihs, ← iht]; rfl
| inr ht' =>
unfold L_eval; rw [hs', ht'];
rw [hs'] at ihs; rw [ht'] at iht; simp;
rw [← ihs, ← iht]; rfl
| inr hs' =>
cases ht with
| inl ht' =>
unfold L_eval; rw [hs', ht'];
rw [hs'] at ihs; rw [ht'] at iht; simp;
rw [← ihs, ← iht]; rfl
| inr ht' =>
unfold L_eval; rw [hs', ht'];
rw [hs'] at ihs; rw [ht'] at iht; simp;
rw [← ihs, ← iht]; rfl
Discussion