Lean4で使えるTactics及びCommand
参考文献
低レベル
test/を見ると理解が進む．
by_contra
intro hでも出来る場合があるが，これはかなり強力にFalseにする
congr
合同性に基づいてゴールをバラす．
例を見たほうがわかりやすい．
code:std4_congr
example
(c : Prop → Prop → Prop → Prop) (x x' y z z' : Prop)
(h₀ : x ↔ x') (h₁ : z ↔ z') : c x y z ↔ c x' y z' := by
apply Iff.of_eq
congr
· guard_target =ₐ x = x'
apply_ext_lemma
assumption
· guard_target =ₐ z = z'
ext
assumption
apply Iff.of_eq後示すべき目標はc x y z = c x' y z'だが，
congrによってx = x'とz = z'を示せば十分であるようにゴールが変わる．
これらは自明なので
その他は例を参照のこと．
guard_hyp
仮定及び仮定の型が一致しているかをチェック
基本は↓
型の場合はguard_hyp h : t
値の場合はguard_hyp h := v
どのぐらいの一致に基づいてによって色々種類がある
guard_target
ゴールが一致しているかチェック．
guard_expr
#guard_expr
Expressionが一致しているかチェックするコマンド
simpa
simp + assumption?
by_contra'
change
existsi
code:mathlib4_existi
example : ∃ x : Nat, x = x := by
existsi 42
rfl
example : ∃ x : Nat, ∃ y : Nat, x = y := by
existsi 42, 42
rfl
知ってると知らないではかなりExists系の証明の落差が激しいと思う
そうか？
同じようなTacticsにuseがある
こちらは書き換えた上でrflも可能な限り試して無みる
$ example : ∃ x : Nat, x = x := by use 42
#explode
code:mathlib4_expliode
info: true_iff : ∀ (p : Prop), (True ↔ p) = p
0 │ │ p ├ Prop
1 │ │ x✝ │ ┌ True ↔ p
2 │ │ trivial │ │ True
3 │1,2 │ Iff.mp │ │ p
4 │1,3 │ ∀I │ (True ↔ p) → p
5 │ │ h │ ┌ p
6 │ │ x✝ │ │ ┌ True
7 │6,5 │ ∀I │ │ True → p
8 │ │ x✝ │ │ ┌ p
9 │8,2 │ ∀I │ │ p → True
10│7,9 │ Iff.intro │ │ True ↔ p
11│5,10│ ∀I │ p → (True ↔ p)
12│4,11│ Iff.intro │ (True ↔ p) ↔ p
13│12 │ propext │ (True ↔ p) = p
14│0,13│ ∀I │ ∀ (p : Prop), (True ↔ p) = p
congr!