mirror of
https://github.com/tomasriveral/ZeroToLean.git
synced 2026-08-11 18:28:39 +02:00
329 lines
6.9 KiB
Lean4
329 lines
6.9 KiB
Lean4
-- see note of 2026-07-30 im trying to prove trivial things. Note I did ask ChatGPT for a list of things to prove.
|
||
|
||
import Mathlib
|
||
|
||
namespace basicLogic
|
||
variable {P: Prop}
|
||
variable {Q: Prop}
|
||
variable {R: Prop}
|
||
|
||
|
||
theorem p_and_q_implie_p
|
||
: P ∧ Q → P := by
|
||
intro hp
|
||
cases hp with
|
||
| intro hP =>
|
||
exact hP
|
||
|
||
theorem p_implies_p_or_q
|
||
: P → P ∨ Q := by
|
||
intro hp
|
||
exact Or.inl hp
|
||
theorem and_commutative
|
||
: P ∧ Q ↔ Q ∧ P := by
|
||
constructor
|
||
· intro hpq
|
||
cases hpq with
|
||
| intro hp hq =>
|
||
exact ⟨hq,hp⟩
|
||
· intro hqp
|
||
cases hqp with
|
||
| intro hq hp =>
|
||
exact ⟨hp,hq⟩
|
||
|
||
#check or_comm
|
||
theorem or_commutative
|
||
: P ∨ Q ↔ Q ∨ P := by
|
||
constructor
|
||
· intro p_or_q
|
||
cases p_or_q with
|
||
| inl hp =>
|
||
exact Or.inr hp
|
||
| inr hq =>
|
||
exact Or.inl hq
|
||
· intro q_or_p
|
||
cases q_or_p with
|
||
| inl hq =>
|
||
exact Or.inr hq
|
||
| inr hp =>
|
||
exact Or.inl hp
|
||
|
||
theorem p_imples_q_and_q_implies_r_Implies_p_implies_r
|
||
: (P→Q) ∧ (Q→R) → (P→R) := by
|
||
intro mainHypothesis
|
||
cases mainHypothesis with
|
||
| intro p_implies_q q_implies_r =>
|
||
intro hp
|
||
exact q_implies_r (p_implies_q hp)
|
||
|
||
#check not_not_intro
|
||
theorem double_negation
|
||
: P → ¬¬P := by
|
||
intro hp
|
||
intro hnotp
|
||
exact hnotp hp
|
||
|
||
#check and_comm
|
||
theorem and_associative
|
||
: P ∧ (Q ∧ R) ↔ (P ∧ Q) ∧ R := by
|
||
constructor
|
||
· intro h
|
||
cases h with
|
||
| intro p q_and_r =>
|
||
cases q_and_r with
|
||
| intro q r =>
|
||
exact ⟨⟨p,q⟩,r⟩
|
||
· intro h
|
||
cases h with
|
||
| intro p_and_q r =>
|
||
cases p_and_q with
|
||
| intro p q =>
|
||
exact ⟨p, ⟨q,r⟩⟩
|
||
|
||
theorem contrapositive
|
||
: (P → Q) → (¬Q → ¬P) := by
|
||
intro p_implies_q
|
||
intro not_q
|
||
intro p
|
||
exact not_q (p_implies_q p)
|
||
|
||
#check or_self
|
||
theorem p_or_p_iff_p
|
||
: P ∨ P ↔ P := by
|
||
constructor
|
||
· intro p_or_p
|
||
cases p_or_p with
|
||
| inr p =>
|
||
exact p
|
||
| inl p =>
|
||
exact p
|
||
· intro p
|
||
exact Or.inl p
|
||
theorem p_or_p_equal_p
|
||
: (P ∨ P) = P := by
|
||
exact propext p_or_p_iff_p
|
||
|
||
#check and_or_left
|
||
theorem and_or_distributivity_left
|
||
: P ∧ (Q ∨ R) ↔ P ∧ Q ∨ P ∧ R := by
|
||
constructor
|
||
· intro p_and_q_or_r
|
||
cases p_and_q_or_r with
|
||
| intro p q_or_r =>
|
||
cases q_or_r with
|
||
| inl q =>
|
||
exact Or.inl ⟨p, q⟩
|
||
| inr r =>
|
||
exact Or.inr ⟨p, r⟩
|
||
· intro p_and_q_or_p_and_r
|
||
cases p_and_q_or_p_and_r with
|
||
| inl p_and_q =>
|
||
cases p_and_q with
|
||
| intro p q =>
|
||
exact ⟨p, Or.inl q⟩
|
||
| inr p_and_r =>
|
||
cases p_and_r with
|
||
| intro p r =>
|
||
exact ⟨p, Or.inr r⟩
|
||
|
||
#check and_or_right
|
||
theorem and_or_distributivity_right
|
||
: P ∧ Q ∨ R ↔ (P ∨ R) ∧ (Q ∨ R) := by
|
||
constructor
|
||
· intro p_and_q_or_r
|
||
cases p_and_q_or_r with
|
||
| inl p_and_q =>
|
||
cases p_and_q with
|
||
| intro p q =>
|
||
exact ⟨Or.inl p, Or.inl q⟩
|
||
| inr r =>
|
||
exact ⟨Or.inr r, Or.inr r⟩
|
||
· intro p_or_r_and_q_or_r
|
||
cases p_or_r_and_q_or_r with
|
||
| intro p_or_r q_or_r =>
|
||
cases p_or_r with
|
||
| inl p =>
|
||
cases q_or_r with
|
||
| inl q =>
|
||
exact Or.inl ⟨p, q⟩
|
||
| inr r =>
|
||
exact Or.inr r
|
||
| inr r =>
|
||
exact Or.inr r
|
||
|
||
#check and_true
|
||
theorem p_and_true_iff_p
|
||
: p ∧ True ↔ p := by
|
||
constructor
|
||
· intro p_and_true
|
||
cases p_and_true with
|
||
| intro p true =>
|
||
exact p
|
||
· intro p
|
||
exact ⟨p, True.intro⟩
|
||
theorem p_and_true_equal_true
|
||
: (p ∧ True) = p := by
|
||
exact propext p_and_true_iff_p
|
||
#check true_and
|
||
theorem true_and_p_iff_p
|
||
: True ∧ p ↔ p := by
|
||
constructor
|
||
· intro true_and_p
|
||
cases true_and_p with
|
||
| intro t p =>
|
||
exact p
|
||
· intro p
|
||
exact ⟨True.intro, p⟩
|
||
theorem true_and_p_equal_p
|
||
: (True ∧ p) = p := by
|
||
exact propext true_and_p_iff_p
|
||
|
||
#check or_false
|
||
theorem p_or_false_iff_p
|
||
: P ∨ False ↔ P := by
|
||
constructor
|
||
· intro p_or_false
|
||
cases p_or_false with
|
||
| inl p =>
|
||
exact p
|
||
| inr f =>
|
||
exact False.elim f
|
||
· intro p
|
||
exact Or.inl p
|
||
theorem p_or_false_equal_p
|
||
: (P ∨ False) = P := by
|
||
exact propext p_or_false_iff_p
|
||
|
||
#check false_or
|
||
theorem false_or_p_iff_p
|
||
: False ∨ P ↔ P := by
|
||
constructor
|
||
· intro false_or_p
|
||
cases false_or_p with
|
||
| inl f =>
|
||
exact False.elim f
|
||
| inr p =>
|
||
exact p
|
||
· intro p
|
||
exact Or.inr p
|
||
theorem false_or_p_equal_p
|
||
: (False ∨ P) = P := by
|
||
exact propext false_or_p_iff_p
|
||
|
||
#check and_false
|
||
theorem and_false_iff_false
|
||
: P ∧ False ↔ False := by
|
||
constructor
|
||
· intro p_and_false
|
||
cases p_and_false with
|
||
| intro p f =>
|
||
exact f
|
||
· intro f
|
||
exact False.elim f
|
||
theorem and_false_equal_false
|
||
: (P ∧ False) = False := by
|
||
exact propext and_false_iff_false
|
||
|
||
#check false_and
|
||
theorem false_and_iff_false
|
||
: False ∧ P ↔ False := by
|
||
constructor
|
||
· intro false_and_p
|
||
cases false_and_p with
|
||
| intro f p =>
|
||
exact f
|
||
· intro f
|
||
exact False.elim f
|
||
theorem false_and_equal_false
|
||
: (False ∧ P) = False := by
|
||
exact propext false_and_iff_false
|
||
|
||
#check or_true
|
||
theorem or_true_iff_true
|
||
: P ∨ True ↔ True := by
|
||
constructor
|
||
· intro p_or_true
|
||
cases p_or_true with
|
||
| inr t =>
|
||
exact t
|
||
| inl p =>
|
||
trivial
|
||
· intro t
|
||
exact Or.inr t
|
||
theorem or_true_equal_true
|
||
: (P ∨ True) = True := by
|
||
exact propext or_true_iff_true
|
||
|
||
#check true_or
|
||
theorem true_or_iff_true
|
||
: True ∨ P ↔ True := by
|
||
constructor
|
||
· intro true_or_p
|
||
cases true_or_p with
|
||
| inl t =>
|
||
exact t
|
||
| inr p =>
|
||
trivial
|
||
· intro t
|
||
exact Or.inl t
|
||
theorem true_or_equal_true
|
||
: (True ∨ P) = True := by
|
||
exact propext true_or_iff_true
|
||
|
||
#check not_or
|
||
#check not_and_or
|
||
|
||
end basicLogic
|
||
|
||
namespace basicArithmetic
|
||
variable {n: Nat}
|
||
variable {m: Nat}
|
||
#check Nat.add_zero
|
||
theorem add_zero_nat
|
||
: n + 0 = n := by
|
||
trivial
|
||
|
||
#check Nat.zero_add
|
||
theorem zero_add_nat
|
||
: 0 + n = n := by
|
||
ring
|
||
|
||
#check Nat.add_comm
|
||
theorem add_commutative (n m : Nat)
|
||
: n + m = m + n := by
|
||
ring
|
||
|
||
#check Nat.add_one
|
||
theorem add_one_equal_succ (n: Nat)
|
||
: n + 1 = n.succ := by
|
||
trivial
|
||
|
||
#check Nat.one_add
|
||
theorem one_add_equal_succ (n: Nat)
|
||
: 1 + n = n.succ := by
|
||
calc
|
||
1 + n = n + 1 := add_commutative 1 n
|
||
_ = n.succ := add_one_equal_succ n
|
||
|
||
|
||
#check Nat.add_left_comm
|
||
theorem add_commutative_left (n m k: Nat)
|
||
: n + (m + k) = m + (n + k) := by
|
||
ring
|
||
|
||
#check Nat.add_right_comm
|
||
theorem add_commutative_right (n m k: Nat)
|
||
: n + m + k = n + k + m := by
|
||
ring
|
||
|
||
#check Nat.add_assoc
|
||
theorem add_associativity_nat (n m k: Nat)
|
||
: n + m + k = n + (m + k) := by
|
||
ring
|
||
|
||
#check Nat.mul_add
|
||
theorem mul_distribute_over_add_nat (n m k: Nat)
|
||
: n * (m + k) = n * m + n * k := by
|
||
ring
|
||
end basicArithmetic
|