12/08/2020 Code/Proofs (Week 9 Wednesday)
Code/Proofs (Week 9 Wednesday)
import Data.Void
prop_id :: a -> a
prop_id = \x -> x
prop_or_false :: a -> Either a Void
prop_or_false = \x -> Left x
prop_or_true_a :: a -> Either a ()
prop_or_true_a = \x -> Left x
prop_or_true_b :: a -> Either a ()
prop_or_true_b = \x -> Right ()
www.cse.unsw.edu.au/~cs3141/20T2/Week 09/Wednesday/Code.html 1/2
xI-→ )⊤ ∧ A( → A I-∧ ⊤∧A⊢A
I-⊤⊤⊢A xA⊢A
xI-→ )⊤∨A(→A RI-∨ ⊤ ∨ A ⊢ A
xI-→ )⊤∨A(→A
I-⊤ ⊤ ⊢ A
LI-∨ ⊤ ∨ A ⊢ A xA ⊢ A
xI-→ )⊥∨A(→A
LI-∨ ⊥ ∨ A ⊢ A xA ⊢ A
xI-→ A→A xA ⊢ A
12/08/2020 Code/Proofs (Week 9 Wednesday)
This is equivalent to:
prop_double_neg_intro :: a -> (a -> Void) -> Void
prop_double_neg_intro = \x -> \f -> f x
This is equivalent to:
prop_triple_neg_elim :: (((a -> Void) -> Void) -> Void) -> a -> Void
prop_triple_neg_elim = \f -> \x -> f (\g -> g x)
prop_and_true :: a -> (a, ())
prop_and_true = \x -> (x, ())
www.cse.unsw.edu.au/~cs3141/20T2/Week 09/Wednesday/Code.html 2/2
fI-→
⊥ → A → )⊥ → )⊥ → )⊥ → A((( xI-→ ⊥→A
xI-→
fI-→
⊥ → )⊥ → A( → A ⊥ → )⊥ → A( ⊢ A
E-→
gI-→
⊥ xA g⊥→A
f ⊥ → )⊥ → )⊥ → A((
E-→
⊥ ⊢ )⊥ → A(,A xA⊢)⊥→A(,A f⊥→A⊢)⊥→A(,A
E-→
⊥
⊥ → )⊥ → A(
A¬ → A¬¬¬
A¬¬ → A