update progress

ZeroToLean/LearningLean/Basic.lean

@@ -0,0 +1 @@
+def hello := "world"

ZeroToLean/LearningLean/LeanFromYoutube.lean

@@ -0,0 +1,118 @@
+-- learned from this video https://www.youtube.com/watch?v=0QZI_m8WZ0Q --
+
+import Mathlib
+
+theorem th (h: 2=2)
+  : 2 = 2 :=
+  h
+
+
+#check th
+
+
+
+theorem th2
+  : 2 = 2 := by
+  norm_num
+
+#check Nat.add_comm
+
+theorem one_plus_two_commutative
+  : 1 + 2 = 2 + 1 := by
+  exact Nat.add_comm 1 2
+
+theorem plus_comm
+  : ∀ (a b: Nat), a + b = b + a := by
+  intro a b
+  have h := Nat.add_comm a b
+  exact h
+
+theorem alg
+  : ∀ (a b c : Nat),
+    a * (b + c) = a* (c + b) := by
+    intro a b c
+    have h : b + c = c + b := by
+      exact plus_comm b c
+    rw [h]
+
+
+theorem factorisation
+  : ∀ (a b : Nat),
+  a^2 + 2*a*b + b^2 = (a + b)^2 := by
+  intro a b
+  ring
+
+
+theorem ev20
+  : Even 20 := by
+  unfold Even
+  use 10
+
+
+theorem two_div_even
+  : ∀ n : Nat, Even n → 2 ∣ n := by
+  intro n
+  intro n_even
+  unfold Even at n_even
+  obtain ⟨r, hr⟩ := n_even
+  have n_eq_2r : n = 2 * r := by
+    rw [hr]
+    ring
+  rw[n_eq_2r]
+  simp
+
+
+
+def PrimeNum (n : Nat) : Prop :=
+  n ≥ 2 ∧ (M: Nat), m ∣ n → , = 1 ∨ m = n
+
+theorem not_prime1
+  : ¬ PrimeNum 1 := by
+  -- proof by contradiction --
+  intro pr1
+  unfold PrimeNum at pr1
+  obtain ⟨prop_left, prop_right⟩ := pr1
+  contradiction
+
+theorem not_prime9
+  : ¬ PrimeNum 9 := by
+    intro pr9
+    unfold PrimeNum at pr9
+    obtain ⟨hl, hr⟩ := pr9
+    have hr_3 := hr 3
+    have div : 3 ∣ 9 := by norm_num
+    have or_cases := hr_3 div
+    rcases or_cases with c1 ∣ c2
+    · contradiction
+    · contradiction
+  
+theorem prime_5
+  : PrimeNum 5 := by
+  unfold PrimeNum
+  have g1 : 5 ≥ 2 := by
+    norm_num
+  have g2
+    : ∀ m : Nat,
+      m ∣ 5 → m = 1 ∨ m = 5 := by
+    intro m h_m_div_5
+    match m with
+    | 0 => contradiction
+    | 1 => 
+      have h : 1 = 1 := by norm_num
+      exact Or.inl h
+    | 2 => contradiction
+    | 3 => contradiction
+    | 4 => contradiction
+    | 5 => 
+      have h : 5 = 5 := by norm_num
+      exact Or.inr h
+    | n + 6 => 
+      have h1 : 5 < n + 6 := by norm_num
+      have h2 := 
+        Nat.eq_zero_of_dvd_of_lt h_m_div_5 h1
+      contradiction
+  exact ⟨g1,g2⟩
+  
+
+#check Nat.eq_zero_of_dvd_of_lt
+

ZeroToLean/LearningLean/TheoremProvingInLean4/Chapter01_Introduction/intro.lean

@@ -0,0 +1,7 @@
+namespace Introduction
+  theorem and_commutative (p q : Prop) : p ∧ q → q ∧ p :=
+   fun hpq : p ∧ q =>
+     have hp : p := And.left hpq
+     have hq : q := And.right hpq
+     show q ∧ p from And.intro hq hp
+end Introduction

ZeroToLean/LearningLean/TheoremProvingInLean4/Chapter02_DependentTypeTheory/simplyTypeTheory.lean

@@ -0,0 +1,214 @@
+namespace simpleTypeTheory
+
+-- some are pasted from the book and some are just me testing stuff
+
+/- Define some constants. -/ 
+def m : Nat := 1 -- m is a natural number 
+def n : Nat := 0
+def b1 : Bool := true -- b1 is a Boolean 
+def b2 : Bool := false
+/- Check their types. -/ 
+#check m -- output: Nat 
+#check n 
+#check n + 0 -- Nat 
+#check m * (n + 0) -- Nat 
+#check b1 -- Bool 
+#check b1 && b2 -- "&&" is the Boolean and 
+#check b1 || b2 -- Boolean or 
+#check true -- Boolean "true" 
+/- Evaluate -/ 
+#eval 5 * 4 
+#eval m + 2 
+#eval b1 && b2 ------20 3 false
+
+
+def t : Bool := true
+def f : Bool := false
+
+#eval t ∧ f ∨ (t ∨ f)
+
+
+#check Nat → Nat
+#check Nat -> Nat
+-- type the arrow as "\to" or "\r"
+-- alternative ASCII notation
+#check Nat × Nat
+#check Prod Nat Nat
+-- type the product as "\times"
+-- alternative notation
+#check Nat → Nat → Nat
+
+#check Nat → (Nat → Nat)
+ -- same type as above
+#check Nat × Nat → Nat
+#check (Nat → Nat) → Nat -- a "functional"
+#check Nat.succ
+#check (0, 1)
+#check Nat.add
+-- Nat → Nat
+-- Nat × Nat
+-- Nat → Nat → Nat
+#check Nat.succ 2
+ -- Nat
+#check Nat.add 3
+ -- Nat → Nat
+#check Nat.add 5 2
+ -- Nat
+#check (5, 9).1
+ -- Nat
+#check (5, 9).2
+ -- Nat
+#eval Nat.succ 2
+ -- 3
+#eval Nat.add 5 2
+ -- 7
+#eval (5, 9).1
+ -- 5
+#eval (5, 9).2
+ -- 9
+
+#check Nat
+ -- Type
+#check Bool
+ -- Type
+#check Nat → Bool
+ -- Type
+#check Nat × Bool
+ -- Type
+#check Nat → Nat
+ -- ...
+#check Nat × Nat → Nat
+#check Nat → Nat → Nat
+#check Nat → (Nat → Nat)
+#check Nat → Nat → Bool
+#check (Nat → Nat) → Nat
+
+
+def α : Type := Nat
+def β : Type := Bool
+def F : Type → Type := List
+def G : Type → Type → Type := Prod
+#check α
+ -- Type
+#check F α
+ -- Type
+#check F Nat
+ -- Type
+#check G α
+ -- Type → Type
+#check G α β
+ -- Type
+#check G α Nat
+ -- Type
+
+
+def α : Type := Nat 
+#check List α -- Type 
+#check List Nat -- Type
+
+#check List
+
+end simpleTypeTheory
+
+namespace FunctionAbstractionAndEvaluation
+#check fun (x : Nat) => x + 5 -- Nat → Nat #check λ (x : Nat) => x + 5 -- λ and fun mean the same thing #check fun x => x + 5 -- Nat inferred #check λ x => x + 5 -- Nat inferred
+
+#eval (λ x : Nat => x + 5) 10 -- 15
+
+#check fun (x : Nat) => x + 5
+ -- Nat → Nat
+#check λ (x : Nat) => x + 5
+ -- λ and fun mean the same thing
+#check fun x => x + 5
+ -- Nat inferred
+#check λ x => x + 5
+ -- Nat inferred
+
+def f (n : Nat) : String := toString n
+def g (s : String) : Bool := s.length > 0
+#check fun x : Nat => x
+ -- Nat → Nat
+#check fun x : Nat => true
+ -- Nat → Bool
+#check fun x : Nat => g (f x)
+ -- Nat → Bool
+#check fun x => g (f x)
+ -- Nat → Bool
+
+ #check fun (g : String → Bool) (f : Nat → String) (x : Nat) => g (f x)
+-- (String → Bool) → (Nat → String) → Nat → Bool
+
+#check fun (α β γ : Type) (g : β → γ) (f : α → β) (x : α) => g (f x)
+
+#check (fun x : Nat => x) 1
+ -- Nat
+#check (fun x : Nat => true) 1
+ -- Bool
+#check (fun (α β γ : Type) (u : β → γ) (v : α → β) (x : α) => u (v x)) Nat String Bool g f 0
+-- Bool
+
+ -- gonna try 10p / day. stopped at 11 Definitions.
+
+
+#check let y := 2 + 2; y * y
+ -- Nat
+#eval let y := 2 + 2; y * y
+ -- 16
+def twice_double (x : Nat) : Nat :=
+  let y := x + x; y * y
+#eval twice_double 2
+ -- 16
+
+end FunctionAbstractionAndEvaluation
+
+namespace testVariableKeyword
+
+section useful
+  variable (α β γ : Type)
+  variable (g : β → γ) (f : α → β) (h : α → α)
+  variable (x : α)
+
+  def compose := g (f x)
+  def doTwice := h (h x)
+  def doThrice := h (h (h x))
+  #print doThrice
+  #print doTwice
+  #print compose
+end useful
+end testVariableKeyword
+
+
+namespace Foo
+def a : Nat := 5
+def f (x : Nat) : Nat := x + 7
+def fa : Nat := f a
+namespace Bar
+def ffa : Nat := f (f a)
+#check fa
+#check ffa
+end Bar
+#check fa
+#check Bar.ffa
+end Foo
+#check Foo.fa
+#check Foo.Bar.ffa
+section
+open Foo
+#check fa
+#check Bar.ffa
+end
+
+namespace dependant
+universe u v
+def f (α : Type u) (β : α → Type v) (a : α) (b : β a) : (a : α) × β a :=
+⟨a, b⟩
+def g (α : Type u) (β : α → Type v) (a : α) (b : β a) : Σ a : α, β a :=
+Sigma.mk a b
+def h1 (x : Nat) : Nat :=
+(f Type (fun α => α) Nat x).2
+#eval h1 5 -- 5
+def h2 (x : Nat) : Nat :=
+(g Type (fun α => α) Nat x).2
+#eval h2 5 -- 5
+end dependant
+