PeirceLEM.hs

-- 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)

PeirceLEM.v

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.