LEAN

尾递归优化

重用当前栈帧

def factorialTailRec (n : Nat) : Nat :=
  let rec aux (n : Nat) (acc : Nat) : Nat :=
    match n with
    | 0 => acc
    | n + 1 => aux n (acc * (n + 1))
  aux n 1

类

structure:类
inductive:递归定义类
class:类型类:方法

Curry-Howard 同构

命题即类型

• 而Prop是类型的类型
• 依赖变量的Prop依然是Prop
  Proof,Theorem,Lemma,Colloray本身是某个Prop的项, 证明即程序
• 一个Prop如果有项则为真

head 名称 (输入:类型): 类型 := 值
theorem name : Prop:= Proof
example=Theorem foo

• ∀ x, P(x) 对应依赖函数类型 (x : X) → P x。
• ∃ x, P(x) 对应依赖对类型 {x : X // P x}这里的//理解为and 反而更好
  量词范围默认向右延伸到表达式结束

证明策略

rfl
rw$\iff$

• repeat rw
• rw [add_zero c]
• rw [\l h]
• nth-rewrite n [h]
• rw [zero_add] at h
  symm
  exact
• doesn’t just take hypotheses, it will eat any proof which exists in the system.
  apply$\Rightarrow$
• apply h1 at h2
  intro h

contrapose
constructor
cases
left right
have

use

simp only [add_assoc, add_left_comm, add_comm]
decide
tauto
trivial

a ≠ b is notation for a = b → False

forward | backward