-- This file:
--   http://anggtwu.net/LEAN/distributivity1.lean.html
--   http://anggtwu.net/LEAN/distributivity1.lean
--          (find-angg "LEAN/distributivity1.lean")
-- Author: Eduardo Ochs <eduardoochs@gmail.com>
--
-- (defun e () (interactive) (find-angg "LEAN/distributivity1.lean"))
-- (defun d () (interactive) (find-LATEX "2017distributivity.tex"))
--
-- (find-angg ".emacs.papers" "tpinlean4" "37" "-- distributivity")



variable (P Q R : Prop)
variable {P Q R : Prop}
variable {p : P}
variable {q : Q}


example (p : P) (q : Q) : P ∧ Q := And.intro p q
example (p : P) (q : Q) : P ∧ Q := And.intro p q

example (_ : Int)       := 42
example (_ : Int) : Int := 42


example    (p : P) (q : Q) : P ∧ Q := And.intro p q
#check fun (p : P) (q : Q)         => And.intro p q

example (P Q : Prop) : P ∧ Q → Q ∧ P := fun (paq : P ∧ Q) => ⟨paq.2, paq.1⟩
example (P Q : Prop) : P ∧ Q → Q ∧ P := fun (paq : P ∧ Q) => And.intro (paq.2) (paq.1)

example (P Q : Prop) : P ∧ Q ↔ Q ∧ P :=
  Iff.intro
    (fun (paq : P ∧ Q) => And.intro (paq.2) (paq.1))
    (fun (qap : Q ∧ P) => And.intro (qap.2) (qap.1))


example (P Q R : Prop) : P ∧ (Q ∨ R) ↔ (P ∧ Q) ∨ (P ∧ R) :=
  Iff.intro (fun (_) => _) _



theorem ta (p : P) (q : Q) : P ∧ Q := And.intro p q
example    (p : P) (q : Q) : P ∧ Q := And.intro p q
#check fun (p : P) (q : Q)         => And.intro p q
#check fun (p : P) (q : Q)         =>
  let paq := And.intro p q
  paq







-- distributivity
example (p q r : Prop) : p ∧ (q ∨ r) ↔ (p ∧ q) ∨ (p ∧ r) :=
  Iff.intro
    (fun h : p ∧ (q ∨ r) =>
      have hp : p := h.left
      Or.elim (h.right)
        (fun hq : q =>
          show (p ∧ q) ∨ (p ∧ r) from Or.inl ⟨hp, hq⟩)
        (fun hr : r =>
          show (p ∧ q) ∨ (p ∧ r) from Or.inr ⟨hp, hr⟩))
    (fun h : (p ∧ q) ∨ (p ∧ r) =>
      Or.elim h
        (fun hpq : p ∧ q =>
          have hp : p := hpq.left
          have hq : q := hpq.right
          show p ∧ (q ∨ r) from ⟨hp, Or.inl hq⟩)
        (fun hpr : p ∧ r =>
          have hp : p := hpr.left
          have hr : r := hpr.right
          show p ∧ (q ∨ r) from ⟨hp, Or.inr hr⟩))







example (paq : P ∧ Q) : Q ∧ P :=
  have p : P := paq.left
  have q : Q := paq.right
  show Q ∧ P from And.intro q p


#check fun  x        => x + 1
#check fun (x : Int) => x + 1
#check fun {α : Type} (x : α) => x


#check fun  x y                => x + y
#check fun (x : Int)  y        => x + y
#check fun (x : Int) (y : Int) => x + y
#check fun (x y : Int)         => x + y





#check fun a : P => a
#check fun p : P => Or.intro_left Q p

#check fun (par : P ∧ R) => par.left
#check fun (par : P ∧ R) => Or.intro_left Q par.left


example (par : P ∧ R) : P ∨ Q :=
  have p : P := par.left
  have poq : P ∨ Q := Or.intro_left Q p
  show P ∨ Q from poq










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