before LateDays

basics/main.lean

@@ -31,6 +31,16 @@ theorem test_next_weekday : next_weekday (next_weekday .Saturday) = .Tuesday :=
 #print and
 #print or
 
+def andb (b₁ : Bool) (b₂ : Bool) : Bool :=
+  match b₁ with
+  | true => b₂
+  | false => false
+
+def orb (b₁ : Bool) (b₂ : Bool) : Bool :=
+  match b₁ with
+  | true => true
+  | false => b₂
+
 example : or true false = true := by rfl
 example : or false false = false := by rfl
 example : or false true = true := by rfl
@@ -350,3 +360,30 @@ end Exercise
 -- skipping
 
 --- More Exercises
+namespace Exercise
+
+theorem identity_fn_applied_twice : ∀ (f : Bool → Bool), (∀ (x : Bool), f x = x) → ∀ (b : Bool), f (f b) = b := by
+  intro f
+  intro h₁
+  intro b
+  rw [h₁]
+  rw [h₁]
+
+theorem negation_fn_applied_twice : ∀ (f : Bool → Bool), (∀ (x : Bool), f x = not x) → ∀ (b : Bool), f (f b) = b := by
+  intros f h b
+  rw [h]
+  rw [h]
+  rw [@Bool.not_eq_eq_eq_not]
+
+theorem andb_eq_orb :
+  ∀ (b c : Bool),
+  (andb b c = orb b c) →
+  b = c
+:= by
+  intros b c
+  intro h
+  cases b
+  case true => exact id (Eq.symm h)
+  case false => exact h
+
+end Exercise