43 lines
1.1 KiB
Markdown
43 lines
1.1 KiB
Markdown
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
|
|
```lean
|
|
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
|
|
|
|
```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 |