/-Propositional_logic_in_Lean 
References: https://leanprover.github.io/theorem_proving_in_lean/propositions_and_proofs.html#propositional-logic-/

variables p q r : Prop

--- shortcuts for propositional connectives ---

#check p ??? (q ??? r)        -- p \and (q \or r)
#check p ??? ?? q            -- p \imp (\neg q)
#check false ??? true       -- false \iff true 


--- syntax for making proofs (in natural deduction style) ---

/- introduction and elimination rules for some connectives -/

-- implication
-- the introduction rule corresponds to lambda abstraction
example (t : p ??? p) := ??h : p, show p, from h  -- or shortly:
example : p ??? p := assume h,h

-- the elimination rule is just function application
example (h1 : p ??? q) (h2 : p) : q := h1 h2

-- conjunction
example (h1 : p) (h2 : q) : p ??? q := and.intro h1 h2
example (h : p ??? q) : p := and.elim_left h 
example (h : p ??? q) : q := and.elim_right h

example (h : p ??? q) : p := h.left    -- a shortcut for and.intro_left h if the operation is clear from context
example (h : p ??? q) : q := h.right   -- analogous

-- disjunction
example (h : p) : p ??? q := or.intro_left q h
example (h : p) : q ??? p := or.intro_right q h

example (h : p) : p ??? q := or.inl h   -- possible if the first argument of or.intro_left is inferable from context
example (h : p) : q ??? p := or.inr h   -- analogous

-- the or.elim rule is esentially a proof by cases
example (h : p ??? q) (h1 : p ??? r) (h2 : q ??? r) : r := or.elim h h1 h2
example (h : p ??? q) (h1 : p ??? r) (h2 : q ??? r) : r := h.elim h1 h2

-- negation and falsity
-- neg is defined (as in intuitionistic logic) as (p ??? false), i.e. that any proof of p yields a contradiction
example (h : p ??? false) : ??p := not.intro h   

-- by the above definition the not.elim rule is simply function application
example (h1 : ??p) (h2 : p) : false := h1 h2

-- falsity: "anything follows from a contradiction"
example (h : false) : q := false.elim h

-- by composing the elimination rules for negation and falsity we get explosion:
example (h1 : p) (h2 : ??p) : q := (absurd h1) h2


--- hypotheses, lemmas and theorems ---

/- the term (??(x : p).t)s denotes a function that takes a proof s of a proposition p and 'inserts' it
into another proof t of some more complex proposition; intiutively this amounts to building 
bigger proofs from smaller ones -/

/-EXAMPLE 1-/
example (t : (p ??? (p ??? q)) ??? q) := 
  assume h1 : p ??? (p ??? q),        
  show q, from (and.elim_right h1) (and.elim_left h1)

/- the "assume" command corresponds to ??-abstraction, untuitively we postulate that the respective type is inhabited, i.e. that the corresponding proposition p is true (= there is a proof of p); the premise is local and we can refer back to it -/

/- or a shorter version: -/
example : (p ??? (p ??? q)) ??? q := 
  assume h1, 
  (and.elim_right h1) (and.elim_left h1)

/-EXAMPLE 2-/
example (t : ??(p ??? q) ??? (p ??? ??q)) :=
  assume h1 : ??(p ??? q),
  assume h2 : p,
  assume h3 : q,
  have nh1 : p ??? q,
    from and.intro h2 h3,   
  show false,                     
    from h1 nh1

/- and a shorter version: -/
example : ?? (p ??? q) ??? (p ??? ?? q) :=
  assume h1,
  assume h2,
  assume h3,
  h1 (and.intro h2 h3)


/- EXAMPLE 3: Transitivity of implication-/
theorem imp_trans_formal_proof : (p ??? (q ??? r)) ??? ((p ??? q) ??? (p ??? r)) :=
  assume h1 : p ??? (q ??? r),
  assume h2 : p ??? q,
  assume h3 : p,
  have h4 : q ??? r, from h1 h3,
  have h5 : q, from h2 h3,
  show r, from h4 h5 

/- and a shorter version -/
theorem imp_trans_short : (p ??? (q ??? r)) ??? ((p ??? q) ??? (p ??? r)) :=
  assume h1,
  assume h2,
  assume h3,
  (h1 h3) (h2 h3) -- Lean recognizes what we assume at which step,and also knows what is left to be shown


/- EXAMPLE 4: using or.elim -/
theorem distribution_one_direction : (p ??? (q ??? r)) ??? ((p ??? q) ??? (p ??? r)) :=
  assume h1, 
  have s1 : q ??? r, from and.elim_right h1, 
  or.elim s1          --recall that or.elim takes 3 arguments
    (assume h2 : q, 
      have t2 : p ??? q, from and.intro (and.elim_left h1) h2,
        show (p ??? q) ??? (p ??? r), from or.intro_left (p ??? r) t2) 
    (assume h3 : r,
      have t3 : p ??? r, from and.intro (and.elim_left h1) h3,
        show (p ??? q) ??? (p ??? r), from or.intro_right (p ??? q) t3)


--- classical logic ---
/- the or.intro rule does not give any hint on how to prove (p ??? ??p); this is because we are still in intuitionistic logic, where this is not a tautology -/

open classical   
#check em                   -- excluded middle (em) is now a theorem
#check by_contradiction     -- also we can use RAA

/- EXAMPLE 5: two simple examples on the use of EM and RAA -/
theorem using_em : (p ??? q) ??? (??p ??? q) := 
  assume h1,
  or.elim (em p)
    (assume h2 : p, show ??p ??? q, from or.intro_right (??p) (h1 h2))
    (assume h3 : ??p, show ??p ??? q, from or.intro_left q h3)

theorem using_raa : (??q ??? ??p) ??? (p ??? q) :=
  assume h1,
  assume h2,
  show q, from by_contradiction
    (assume h3 : ??q, show false, from (h1 h3) h2)


-- Ideas for some proofs?
-- EM implies double-negation elimination (DNE)
-- DNE implies EM
-- EM implies by_contradiction
-- in classical setting prove Peirce law (((p ??? q) ??? p) ??? p)