-- This file:
--   http://anggtwu.net/LEAN/propsandproofs2.lean.html
--   http://anggtwu.net/LEAN/propsandproofs2.lean
--          (find-angg "LEAN/propsandproofs2.lean")
-- Author: Eduardo Ochs <eduardoochs@gmail.com>
--
-- (defun p1 () (interactive) (find-angg "LEAN/propsandproofs1.lean"))
-- (defun p2 () (interactive) (find-angg "LEAN/propsandproofs2.lean"))

def    Implies (P Q : Prop) : Prop := P → Q
#check Implies

variable (P Q R : Prop)

theorem triv1 (p : P) : P := p
theorem triv2 («.P» : P) : P := «.P»
-- theorem triv3 («.P» : P) («P→Q» : P → Q) : Q := _
-- theorem triv4 («.P» : P) («P→Q» : P → Q) : Q := «P→Q» _
theorem triv5 («.P» : P) («P→Q» : P → Q) : Q := «P→Q» «.P»

def «♯» := 42

-- theorem triv2 (❮P❯ : P) : P := ❮P❯

-- (find-tpinlean4page 31 "h.elim instead of Or.elim h")
-- (find-tpinlean4text 31 "h.elim instead of Or.elim h")

example («P∨Q» : P ∨ Q) : Q ∨ P :=
  «P∨Q».elim (fun «P» => Or.inr «P») (fun «Q» => Or.inl «Q»)

example («P→Q» : P → Q) («¬Q» : ¬Q) : ¬P :=
  fun «P» : P =>
  show False from «¬Q» («P→Q» «P»)

-- (find-tpinlean4page 33 "theorem and_swap")
-- (find-tpinlean4text 33 "theorem and_swap")

theorem and_swap1 : P ∧ Q ↔ Q ∧ P :=
  Iff.intro
    (fun «P∧Q» : P ∧ Q =>
     show Q ∧ P from And.intro (And.right «P∧Q») (And.left «P∧Q»))
    (fun «Q∧P» : Q ∧ P =>
     show P ∧ Q from And.intro (And.right «Q∧P») (And.left «Q∧P»))

#check and_swap1
#check and_swap1 P Q                 -- p ∧ q ↔ q ∧ p

variable («P∧Q» : P ∧ Q)
example : Q ∧ P := Iff.mp (and_swap1 P Q) «P∧Q»

-- (find-tpinlean4page 33 "have hp : p := h.left")
-- (find-tpinlean4text 33 "have hp : p := h.left")

-- (find-tpinlean4page 34 "suffices hq : q from And.intro hq hp")
-- (find-tpinlean4text 34 "suffices hq : q from And.intro hq hp")

example («P∧Q» : P ∧ Q) : Q ∧ P :=
  have «P» : P := «P∧Q».left
  suffices «Q» : Q from And.intro «Q» «P»
  show Q from And.right «P∧Q»

-- (find-tpinlean4page 34 "theorem dne")
-- (find-tpinlean4text 34 "theorem dne")



open Classical

theorem dne {P : Prop} («¬¬P» : ¬¬P) : P :=
  Or.elim (em P)
    (fun «P»  :  P => «P»)
    (fun «¬P» : ¬P => absurd «¬P» «¬¬P»)

open Classical
variable (P : Prop)

example («¬¬P» : ¬¬P) : P :=
  byCases
    (fun «P»  :  P => «P»)
    (fun «¬P» : ¬P => absurd «¬P» «¬¬P»)

open Classical
variable (p : Prop)

example («¬¬P» : ¬¬P) : P :=
  byContradiction
    (fun «¬P» : ¬P =>
     show False from «¬¬P» «¬P»)

example («¬(P∧Q)» : ¬(P ∧ Q)) : ¬P ∨ ¬Q :=
  Or.elim (em P)
    (fun «P» : P =>
      Or.inr
        (show ¬Q from
          fun «Q» : Q =>
          «¬(P∧Q)» ⟨«P», «Q»⟩))
    (fun «P» : ¬P =>
      Or.inl «P»)



-- (find-tpinlean4page 40 "put into practice")
-- (find-tpinlean4text 40 "put into practice")

example (A : Type) (P Q : A → Prop) : (∀ a : A, P a ∧ Q a) → ∀ y : A, P y :=
  fun «∀a.Pa∧Qa» : ∀ a : A, P a ∧ Q a =>
  fun a' : A =>
  show P a' from («∀a.Pa∧Qa» a').left




-- Local Variables:
-- coding:  utf-8-unix
-- End: