Coqチュートリアル2章に出てくる命題をHaskellで書いてみた

CoqTut2.hs

{-# LANGUAGE TypeOperators, Rank2Types #-}
module CoqTut2 where

-- prop0 : forall (A : Prop), A -> A
prop0 :: forall a. a -> a
prop0 = id

-- prop1 : forall (P Q : Prop), (forall P : Prop, (P -> Q) -> Q) -> ((P -> Q) -> P) -> P
prop1 :: forall p q. (forall p. (p -> q) -> q) -> ((p -> q) -> p) -> p
prop1 h h0 = h0 $ const $ h h

-- prop1' : forall (P Q : Prop), (forall P : Prop, (P -> Q) -> Q) -> ((P -> Q) -> P) -> P
prop1' :: forall p q. (forall p. (p -> q) -> q) -> ((p -> q) -> p) -> p
prop1' h h0 = h0 $ const $ h $ \h2 -> h2

-- prop2 : forall (P Q R : Prop), (P -> Q) -> (Q -> R) -> P -> R
prop2 :: forall p q r. (p -> q) -> (q -> r) -> p -> r
prop2 h h0 h1 = h0 (h h1)

data Void
type Not p = p -> Void

-- prop3 : forall P : Prop, P -> ~~P.
prop3 :: forall p. p -> Not (Not p)
prop3 h h0 = h0 h

type (:\/) = Either

-- prop4 : forall (P Q : Prop),  P \/ Q -> Q \/ P
prop4 :: forall p q. p :\/ q -> q :\/ p
prop4 h = case h of
  Left h0  -> Right h0
  Right h0 -> Left h0

type (:/\) = (,)

-- prop5 : forall (P Q : Prop), P /\ Q -> Q /\ P
prop5 :: forall p q. p :/\ q -> q :/\ p
prop5 h = case h of
  (h0, h1) -> (h1, h0)