constructive.lean

-- you can add extra negations if you want
def extra_negations {A : Prop} (a : A) : ¬¬A :=
  show ¬¬A, from not.intro (λ (na: ¬A), na a)
  
-- You can remove extra negations beyond 2,
def triple_elim {A : Prop} (nnna : ¬¬¬A)  : ¬A :=
  show ¬A, from not.intro (λ a, nnna (extra_negations a))

-- LEM is not negated,
def nnlem {A : Prop} : ¬ ¬(A ∨ ¬A) :=
  show ¬¬(A ∨ ¬A), from not.intro (λ (nlem : ¬ (A ∨ ¬A)), 
    have na : ¬ A, from not.intro (λ a, nlem (or.inl a)),
    have a  :   A, from false.elim (nlem (or.inr na)),
    show false, from na a
  )

-- We can imagine that LEM is going to be valid through the identity
def ident {A : Prop} (a : A) : A := a
def lem_identity {A : Prop} (lem : A ∨ ¬A) : A ∨ ¬A := lem
def lem_identity2 {A : Prop} (lem : A ∨ ¬A) : A ∨ ¬A := ident lem

def bar {A B : Prop} (h : ¬ (A ∧ B)) : (A -> ¬ B) ∧ (B -> ¬ A) :=
  and.intro (λ a, (λ b, h (and.intro a b))) (λ b, (λ a, h (and.intro a b)))
  
-- So, you can imagine that you can use LEM then without taking it as an axiom.
def demorgans {A B : Prop} (lem : A ∨ ¬ A) (nab : ¬(A ∧ B)) :  ¬A ∨ ¬B :=
  or.elim lem
    (λ a  :  A, or.inr ((bar nab).left a))
    (λ na : ¬A, or.inl na)

-- Sometimes this leads to constructive proofs which are similar to classical ones
def weird_demorgans {A B : Prop} (a_or_b : A ∨ B) (nab : ¬(A ∧ B)) : ¬A ∨ ¬B :=
   or.elim a_or_b
    (λ a,
      have nb : ¬B, from ((bar nab).left) a,
     or.inr nb)
    (λ b, have na : ¬A, from ((bar nab).right b),
      or.inl na)