daily pastebin goal
50%
SHARE
TWEET

Untitled

a guest Nov 8th, 2018 103 Never
Not a member of Pastebin yet? Sign Up, it unlocks many cool features!
  1. -- you can add extra negations if you want
  2. def extra_negations {A : Prop} (a : A) : ¬¬A :=
  3.   show ¬¬A, from not.intro (λ (na: ¬A), na a)
  4.  
  5. -- You can remove extra negations beyond 2,
  6. def triple_elim {A : Prop} (nnna : ¬¬¬A)  : ¬A :=
  7.   show ¬A, from not.intro (λ a, nnna (extra_negations a))
  8.  
  9. -- LEM is not negated,
  10. def nnlem {A : Prop} : ¬ ¬(A ∨ ¬A) :=
  11.   show ¬¬(A ∨ ¬A), from not.intro (λ (nlem : ¬ (A ∨ ¬A)),
  12.     have na : ¬ A, from not.intro (λ a, nlem (or.inl a)),
  13.     have a  :   A, from false.elim (nlem (or.inr na)),
  14.     show false, from na a
  15.   )
  16.  
  17. -- We can imagine that LEM is going to be valid through the identity
  18. def ident {A : Prop} (a : A) : A := a
  19. def lem_identity {A : Prop} (lem : A ∨ ¬A) : A ∨ ¬A := lem
  20. def lem_identity2 {A : Prop} (lem : A ∨ ¬A) : A ∨ ¬A := ident lem
  21.  
  22. def bar {A B : Prop} (h : ¬ (A ∧ B)) : (A -> ¬ B) ∧ (B -> ¬ A) :=
  23.   and.intro (λ a, (λ b, h (and.intro a b))) (λ b, (λ a, h (and.intro a b)))
  24.  
  25. -- So, you can imagine that you can use LEM then without taking it as an axiom.
  26. def demorgans {A B : Prop} (lem : A ∨ ¬ A) (nab : ¬(A ∧ B)) :  ¬A ∨ ¬B :=
  27.   or.elim lem
  28.     (λ a  :  A, or.inr ((bar nab).left a))
  29.     (λ na : ¬A, or.inl na)
  30.  
  31. -- Sometimes this leads to constructive proofs which are similar to classical ones
  32. def weird_demorgans {A B : Prop} (a_or_b : A ∨ B) (nab : ¬(A ∧ B)) : ¬A ∨ ¬B :=
  33.    or.elim a_or_b
  34.     (λ a,
  35.       have nb : ¬B, from ((bar nab).left) a,
  36.      or.inr nb)
  37.     (λ b, have na : ¬A, from ((bar nab).right b),
  38.       or.inl na)
RAW Paste Data
We use cookies for various purposes including analytics. By continuing to use Pastebin, you agree to our use of cookies as described in the Cookies Policy. OK, I Understand
 
Top