vault backup: 2025-02-11 13:31:22

300s School/ME 2150 - High Assurance Cyber-Physical Systems/Lean.md

@@ -1 +1,43 @@
-Given by Jeremy Avigad, From CMU's Philosopy department
+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