From 44708b89bfed037b39c27a016adc9cde25f00339 Mon Sep 17 00:00:00 2001
From: qwjyh <urataw421@gmail.com>
Date: Wed, 4 Jun 2025 23:15:03 +0900
Subject: [PATCH] before LateDays

---
 basics/main.lean | 37 +++++++++++++++++++++++++++++++++++++
 1 file changed, 37 insertions(+)

diff --git a/basics/main.lean b/basics/main.lean
index b0db83a..900dd14 100755
--- a/basics/main.lean
+++ b/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