1.1 KiB
1.1 KiB
Given by Jeremy Avigad, From CMU's Philosopy department
We're doing veverything through a VSCode lecture.
- Lean nicely formats things like natural number symbols
- Copilot in vscode also looks pretty insane. Pretty sick preloading for what people anticipate
We're proving the factorial
def fac: N->N
| 0=>1
| n+1 => (n+1) * fac n
#check fac
#print fac
#eval fac 3 /- this will actually run the function -/
These are functional definitions
Lean is suprisingly a good programming language. Most of lean is written in lean
theorem dvd_fac: \forall n, \forall i \leq n, i | fac n:= by
intro n
induction' n with n ih
. simp: [fac] /-(now something is wrong. 1=0..? Turns out our theorem is false when i = 0!)-/
/-so change i to i+1-/
. intro i h
rw[fac]
rcases lt_or_eq_of_le (Nat.le_of_lt_succ N) with h1 | rfl
. apply dvd_mulof_dvd_right
apply ih _ h1
. dvd_mul_right
#check dvd_fac /- it works! -/
'fac' is a program, and we just proved something about it.
This is what software verification is all about.
ITP is an interactive theorem prover