From 308bf5149499299e75e165af3df4db9506e7e286 Mon Sep 17 00:00:00 2001
From: qwjyh <urataw421@gmail.com>
Date: Sat, 20 Apr 2024 13:24:32 +0900
Subject: [PATCH] init (3.2 negation)

---
 prop_as_types.lean | 98 ++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 98 insertions(+)
 create mode 100644 prop_as_types.lean

diff --git a/prop_as_types.lean b/prop_as_types.lean
new file mode 100644
index 0000000..4db0e83
--- /dev/null
+++ b/prop_as_types.lean
@@ -0,0 +1,98 @@
+--
+-- 3. Propositions and Proofs
+--
+
+-- Propositions as Types
+
+-- https://stackoverflow.com/questions/69182724/lean-4-unknown-identifier-proof
+-- The code below actually does not work
+-- #check And
+-- #check Or
+-- #check Not
+-- #check Implies
+--
+-- variable (p q r : Prop)
+-- #check And p q
+-- #check Or p q
+-- #print Or
+-- #check Implies (And p q) (And q p)
+-- #check p → q
+
+-- Working with Propositions as Types
+variable {p : Prop}
+variable {q : Prop}
+
+-- theorem t1 : p → q → p := fun hp : p => fun hq : q => hp
+theorem t1 : p → q → p :=
+  fun hp : p =>
+  fun hq : q =>
+  show p from hp
+
+#print t1
+
+variable (p q r s : Prop)
+
+#check t1 p q
+#check t1 r s
+
+-- Propositional Logic
+
+-- conj
+variable (p q : Prop)
+
+example (hp : p) (hq : q) : p ∧ q := And.intro hp hq
+
+#check fun (hp : p) (hq : q) => And.intro hp hq
+
+variable (p q : Prop)
+
+example (h : p ∧ q) : p := And.left h
+example (h : p ∧ q) : q := And.right h
+
+example (h : p ∧ q) : q ∧ p :=
+  And.intro (And.right h) (And.left h)
+
+variable (hp : p) (hq : q)
+#check (⟨hp, hq⟩ : p ∧ q)
+
+example (h : p ∧ q) : q ∧ p :=
+  ⟨h.right, h.left⟩
+
+example (h : p ∧ q) : q ∧ p ∧ q :=
+  ⟨h.right, ⟨h.left, h.right⟩⟩
+
+example (h : p ∧ q) : q ∧ p ∧ q :=
+  ⟨h.right, h.left, h.right⟩
+
+-- disjunction
+variable (p q : Prop)
+example (hp : p) : p ∨ q := Or.intro_left q hp
+example (hq : q) : p ∨ q := Or.intro_right p hq
+
+example (h : p ∨ q) : q ∨ p :=
+  Or.elim h
+    (fun hp : p =>
+      show q ∨ p from Or.intro_right _ hp)
+    (fun hq : q =>
+      show q ∨ p from Or.intro_left _ hq)
+
+example (h : p ∨ q) : q ∨ p :=
+  Or.elim h (fun hq => Or.inr hq) (fun hp => Or.inl hp)
+
+example (h : p ∨ q) : q ∨ p :=
+  h.elim (fun hq => Or.inr hq) (fun hp => Or.inl hp)
+
+-- Negation and Falsity
+variable (p q : Prop)
+
+example (hpq : p → q) (hnq : ¬q) : ¬p :=
+  fun hp : p =>
+  show False from hnq (hpq hp)
+
+example (hp : p) (hnp : ¬p) : q := False.elim (hnp hp)
+
+example (hp : p) (hnp : ¬p) : q := absurd hp hnp
+
+example (hnp : ¬p) (hq : q) (hqp : q → p) : r :=
+  absurd (hqp hq) hnp
+