2. Propositional logic to lean

10/10/22

/-

Lecture 3: Propositional logic to lean

-/

variables P Q R : Prop

example : (P → P → Q) → (P → Q) :=
begin
  assume h p,
  apply h,
  exact p,
  exact p,
end

-- how to prove an implication?
-- assume x,
-- goal was ⊢ P → Q
-- after x : P ⊢ Q
-- assume x y,
-- goal was ⊢ P → Q → R
-- after x : p,y : Q ⊢ R
-- how to use an implication?
-- given h : P → Q
-- apply h, then need to prove p
-- given h : P → Q → R
-- then have to prove P and Q

-- CONJUNCTION (P ∧ Q) P and Q

example : P → (Q → (P ∧ Q)) :=
begin
  assume p q,
  constructor,
  exact p,
  exact q,
end

example : P ∧ Q → P :=
begin
  assume h,
  cases h with p q, --splits p and q
  exact p,
end

-- to prove P ∧ Q : use constrictor,
-- to use h : P ∧ Q : use cases h with x y,

-- P → Q → R
-- P ∧ Q -> R
-- P ↔ Q
-- \iff = if and only if

theorem curry:
(P → Q → R) ↔ (P ∧ Q → R) :=
begin
  constructor,
  assume l h,
  /- Bad Way
  cases h with p q,
  exact p,
  cases h with pq,
  exact q,
  -/
  cases h with p q,
  apply l,
  exact p,
  exact q,

  assume pqr p q,
  apply pqr,
  constructor,
  exact p,
  exact q,

end 

-- Haskell Curry
-- Int -> Int -> Int
-- (Int, Int) -> Int


-- disjunction
-- P ∨ Q, P or Q

example : P → P ∨ Q :=
begin
  assume p,
  left,
  exact p,
end

example : Q → P ∨ Q :=
begin
  assume q,
  right,
  exact q,
end

example : (P → R) → (Q → R) → (P ∨ Q) → R :=
begin
  assume pr qr pq,
  cases pq with p q,
  apply pr,
  exact p,
  apply qr, 
  exact q,
end

example : true :=
begin
  constructor,
end

example : false → P:=
begin
  assume h,
  cases h,
end

-- ex false quod libet
-- from false everything follows
-- ¬ P = P → false

example : ¬ (P ∧ ¬ P) :=
begin
  assume h,
  cases h with p np,
  apply np,
  exact p,
end