Haskell Road to Logic, Math, Programming 演習3.5

eq.v

From mathcomp Require Import all_ssreflect.
Set Implicit Arguments.

Lemma eq (p q r : Prop): (p <-> q) -> ((p -> r) <-> (q -> r)).
Proof.
  move => [pq qp].
  split.
  move => pr q0.
  apply pr.
  apply qp.
  assumption.

  move => qr p0.
  apply qr.
  apply pq.
  assumption.
Qed.

Lemma eq2 (p q r : Prop): (p <-> q) -> ((r -> p) <-> (r -> q)).
Proof.
  move => [pq qp].
  split.
  move => pr q0.
  apply pq.
  apply pr.
  assumption.

  move => qr p0.
  apply qp.
  apply qr.
  assumption.
Qed.

equiv.hs

{-# LANGUAGE TypeOperators #-}
type (<=>) a b = (a->b, b->a)

eq :: (p <=> q) -> ((p -> r) <=> (q -> r))
eq (pq, qp) = (\pr ->         -- (=>)
                  \q ->
                    pr (qp q), -- :: r
               \qr ->         -- (<=)
                  \p ->
                    qr (pq p) -- :: r
              )


eq2 :: (p <=> q) -> ((r -> p) <=> (r -> q))
eq2 pqqp =
  (((fst pqqp) . ),  ((snd pqqp) . ))


{-eq2 :: (p <=> q) -> ((r -> p) <=> (r -> q))
eq2 (pq, qp) =
  (\rp -> pq . rp,
   \rq -> qp . rq) -}