• API
• FAQ
• Tools
• Archive
daily pastebin goal
51%
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.

Top