From 6da452fe22ecdc0e93900d05c67d0dd328d6d0c6 Mon Sep 17 00:00:00 2001 From: Dane Sabo Date: Tue, 11 Feb 2025 13:31:22 -0500 Subject: [PATCH] vault backup: 2025-02-11 13:31:22 --- .../Lean.md | 44 ++++++++++++++++++- 1 file changed, 43 insertions(+), 1 deletion(-) diff --git a/300s School/ME 2150 - High Assurance Cyber-Physical Systems/Lean.md b/300s School/ME 2150 - High Assurance Cyber-Physical Systems/Lean.md index 342ac549e..0c973b57e 100644 --- a/300s School/ME 2150 - High Assurance Cyber-Physical Systems/Lean.md +++ b/300s School/ME 2150 - High Assurance Cyber-Physical Systems/Lean.md @@ -1 +1,43 @@ -Given by Jeremy Avigad, From CMU's Philosopy department \ No newline at end of file +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 \ No newline at end of file