-
-
Save agrif/2a870f3655b71615a9b7 to your computer and use it in GitHub Desktop.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| -- Exercise: prove Peirce’s law <=> law of excluded middle in Haskell | |
| {-# LANGUAGE Rank2Types #-} | |
| import Data.Void | |
| import Data.Bifunctor | |
| import Data.Functor.Identity | |
| type Not a = a -> Void | |
| type Peirce = forall a b. ((a -> b) -> a) -> a | |
| type LEM = forall a. Either (Not a) a | |
| callCC_lem :: Peirce -> LEM | |
| callCC_lem callCC = callCC $ \cc -> Left (\a -> cc (Right a)) | |
| lem_callCC :: LEM -> Peirce | |
| lem_callCC lem = either (\n -> \f -> f (absurd . n)) const lem | |
| -- Bonus exercise: prove Peirce’s law <=> double negation elimination | |
| type DNE = forall a. Not (Not a) -> a | |
| lem_dne :: LEM -> DNE | |
| lem_dne lem = either (\f -> \g -> absurd (g f)) const lem | |
| dne_lem :: DNE -> LEM | |
| dne_lem dne = dne $ \n -> n (Right . dne $ \m -> n (Left m)) | |
| callCC_dne :: Peirce -> DNE | |
| callCC_dne callCC = \dn -> callCC $ \cc -> absurd (dn cc) | |
| dne_callCC :: DNE -> Peirce | |
| dne_callCC dne f = dne $ \n -> n (f . dne $ \m -> m (absurd . n)) | |
| -- Self-inflicted exercise: prove dual Frobenius rule <=> everything else | |
| data Voider a = Voider { unVoider :: Void } | |
| type DualFrobenius = forall x p q. (x -> Either (p x) q) -> Either (x -> p x) q | |
| lem_df :: LEM -> DualFrobenius | |
| lem_df lem f = bimap (\nq -> either id (absurd . nq) . f) id lem | |
| df_lem :: DualFrobenius -> LEM | |
| df_lem df = first (\f -> unVoider . f) (df Right) | |
| callCC_df :: Peirce -> DualFrobenius | |
| callCC_df callCC f = callCC $ \cc -> Left $ \x -> either id (cc . Right) (f x) | |
| df_callCC :: DualFrobenius -> Peirce | |
| df_callCC df f = either (\g -> f (absurd . unVoider . g)) id (df Right) | |
| dne_df :: DNE -> DualFrobenius | |
| dne_df dne f = dne $ \n -> n (Left $ \x -> dne $ \m -> either (m) (n . Right) (f x)) | |
| df_dne :: DualFrobenius -> DNE | |
| df_dne df dn = either (\f -> (absurd . dn) (unVoider . f)) id (df Right) |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Section Peirce. | |
| (* the following are equivalent... *) | |
| Definition Peirce := forall A B : Prop, ((A -> B) -> A) -> A. | |
| Definition LEM := forall A : Prop, ~ A \/ A. | |
| Definition DNE := forall A : Prop, ~~A -> A. | |
| Definition DualFrobenius := forall (X : Set) (P : X -> Prop) (Q : Prop), | |
| (forall x : X, P x \/ Q) -> (forall x : X, P x) \/ Q. | |
| Lemma peirce_lem : Peirce <-> LEM. | |
| unfold Peirce, LEM. | |
| split. | |
| intros callCC A. | |
| apply callCC with (B := False). | |
| intro cc. | |
| left. | |
| intro a. | |
| apply cc. | |
| right. | |
| exact a. | |
| intros lem A B f. | |
| destruct (lem A). | |
| apply f. | |
| intro a. | |
| destruct H. | |
| exact a. | |
| exact H. | |
| Qed. | |
| Lemma peirce_dne : Peirce <-> DNE. | |
| unfold Peirce, DNE. | |
| split. | |
| intros callCC A dn. | |
| apply callCC with (B := False). | |
| intro cc. | |
| destruct dn. | |
| exact cc. | |
| intros dne A B f. | |
| apply dne. | |
| intro n. | |
| apply n. | |
| apply f. | |
| intro a. | |
| destruct n. | |
| exact a. | |
| Qed. | |
| Lemma peirce_df : Peirce <-> DualFrobenius. | |
| unfold Peirce, DualFrobenius. | |
| split. | |
| intros callCC X P Q f. | |
| apply callCC with (B := False). | |
| intro cc. | |
| left. | |
| intro x. | |
| destruct (f x). | |
| exact H. | |
| destruct cc. | |
| right. | |
| exact H. | |
| intros df A B f. | |
| destruct (df {_ : unit | A} (fun _ => False) A). | |
| intro X. | |
| destruct X. | |
| right. | |
| exact a. | |
| apply f. | |
| intro a. | |
| destruct H. | |
| split. | |
| constructor. | |
| exact a. | |
| exact H. | |
| Qed. | |
| Lemma lem_dne : LEM <-> DNE. | |
| unfold LEM, DNE. | |
| split. | |
| intros lem A dn. | |
| destruct (lem A). | |
| destruct dn. | |
| exact H. | |
| exact H. | |
| intros dne A. | |
| apply dne. | |
| intro n. | |
| apply n. | |
| right. | |
| apply dne. | |
| intro m. | |
| apply n. | |
| left. | |
| exact m. | |
| Qed. | |
| Lemma lem_df : LEM <-> DualFrobenius. | |
| unfold LEM, DualFrobenius. | |
| split. | |
| intros lem X P Q f. | |
| destruct (lem Q). | |
| left. | |
| intro x. | |
| destruct (f x). | |
| exact H0. | |
| destruct H. | |
| exact H0. | |
| right. | |
| exact H. | |
| intros df A. | |
| destruct (df {_ : unit | A} (fun _ => False) A). | |
| intro X. | |
| destruct X. | |
| right. | |
| exact a. | |
| left. | |
| intro a. | |
| apply H. | |
| split. | |
| constructor. | |
| exact a. | |
| right. | |
| exact H. | |
| Qed. | |
| Lemma dne_df : DNE <-> DualFrobenius. | |
| unfold DNE, DualFrobenius. | |
| split. | |
| intros dne X P Q f. | |
| apply dne. | |
| intro n. | |
| apply n. | |
| left. | |
| intro x. | |
| destruct (f x). | |
| exact H. | |
| destruct n. | |
| right. | |
| exact H. | |
| intros df A dn. | |
| destruct (df {_ : unit | A} (fun _ => False) A). | |
| intro X. | |
| destruct X. | |
| right. | |
| exact a. | |
| destruct dn. | |
| intro a. | |
| apply H. | |
| split. | |
| constructor. | |
| exact a. | |
| exact H. | |
| Qed. |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment