Logic

module Logic

import Data.Bifunctor

%default total

%access export

Iff

The following iff-related functions are ported from Coq.Init.Logic.

iff a b, written a <-> b, expresses the equivalence of a and b.

infixl 9 <->

public export
(<->) : Type -> Type -> Type
(<->) a b = (a -> b, b -> a)

A ↔ A

iff_refl : a <-> a
iff_refl = (id, id)

(A ↔ B)→(B ↔ C)→(A ↔ C)

iff_trans : (a <-> b) -> (b <-> c) -> (a <-> c)
iff_trans (ab, ba) (bc, cb) = (bc . ab, ba . cb)

(A ↔ B)→(B ↔ A)

iff_sym : (a <-> b) -> (b <-> a)
iff_sym = swap

Since (A ∧ B)→B and (A ∧ C)→C, (B ↔ C)→((A ∧ B)↔(A ∧ C)).

and_iff_compat_l : (b <-> c) -> ((a, b) <-> (a, c))
and_iff_compat_l = bimap second second

Since (B ∧ A)→B and (C ∧ A)→C, (B ↔ C)→((B ∧ A)↔(C ∧ A)).

and_iff_compat_r : (b <-> c) -> ((b, a) <-> (c, a))
and_iff_compat_r = bimap first first

Since B → (A ∨ B) and C → (A ∨ C), (B ↔ C)→((A ∨ B)↔(A ∨ C)).

or_iff_compat_l : (b <-> c) -> (Either a b <-> Either a c)
or_iff_compat_l = bimap second second

Since B → (B ∨ A) and C → (C ∨ A), (B ↔ C)→((B ∨ A)↔(C ∨ A)).

or_iff_compat_r : (b <-> c) -> (Either b a <-> Either c a)
or_iff_compat_r = bimap first first

¬A ↔ (A ↔ ⊥)

neg_void : Not a <-> (a <-> Void)
neg_void = (flip MkPair void, fst)

Given B → A and C → A, ((A ∧ B)↔(A ∧ C)) ↔ (B ↔ C).

and_cancel_l : (b -> a) -> (c -> a) -> (((a, b) <-> (a, c)) <-> (b <-> c))
and_cancel_l ba ca = (bimap f g, and_iff_compat_l)
  where
    f pf b = snd $ pf (ba b, b)
    g pg c = snd $ pg (ca c, c)

Given B → A and C → A, ((B ∧ A)↔(C ∧ A)) ↔ (B ↔ C).

and_cancel_r : (b -> a) -> (c -> a) -> (((b, a) <-> (c, a)) <-> (b <-> c))
and_cancel_r ba ca = (bimap f g, and_iff_compat_r)
  where
    f pf b = fst $ pf (b, ba b)
    g pg c = fst $ pg (c, ca c)

(A ∧ B)↔(B ∧ A)

and_comm : (a, b) <-> (b, a)
and_comm = (swap, swap)

((A ∧ B)∧C)↔(A ∧ B ∧ C)

and_assoc : ((a, b), c) <-> (a, b, c)
and_assoc = (\((a, b), c) => (a, b, c), \(a, b, c) => ((a, b), c))

(B → ¬A)→(C → ¬A)→(((A ∨ B)↔(A ∨ C)) ↔ (B ↔ C))

or_cancel_l : (b -> Not a)
           -> (c -> Not a)
           -> ((Either a b <-> Either a c) <-> (b <-> c))
or_cancel_l bNotA cNotA = (bimap f g, or_iff_compat_l)
  where
    f ef b = go (bNotA b) (ef (Right b))
    g eg c = go (cNotA c) (eg (Right c))
    go : Not a -> Either a b -> b
    go lf = either (void . lf) id

(B → ¬A)→(C → ¬A)→(((B ∨ A)↔(C ∨ A)) ↔ (B ↔ C))

or_cancel_r : (b -> Not a)
           -> (c -> Not a)
           -> ((Either b a <-> Either c a) <-> (b <-> c))
or_cancel_r bNotA cNotA = (bimap f g, or_iff_compat_r)
  where
    f ef b = go (bNotA b) (ef (Left b))
    g eg c = go (cNotA c) (eg (Left c))
    go : Not p -> Either q p -> q
    go rf = either id (void . rf)

(A ∨ B)↔(B ∨ A)

or_comm : Either a b <-> Either b a
or_comm = (mirror, mirror)

((A ∨ B)∨C)→(A ∨ (B ∨ C))

or_assoc_lemma1 : Either (Either a b) c -> Either a (Either b c)
or_assoc_lemma1 = either (second Left) (pure . pure)

(A ∨ (B ∨ C)) → ((A ∨ B)∨C)

or_assoc_lemma2 : Either a (Either b c) -> Either (Either a b) c
or_assoc_lemma2 = either (Left . Left) (first Right)

((A ∨ B)∨C)↔(A ∨ (B ∨ C))

or_assoc : Either (Either a b) c <-> Either a (Either b c)
or_assoc = (or_assoc_lemma1, or_assoc_lemma2)

(A ↔ B)→((A → B)∧(B → A))

iff_and : (a <-> b) -> (a -> b, b -> a)
iff_and = id

(A ↔ B)↔((A → B)∧(B → A))

iff_to_and : (a <-> b) <-> (a -> b, b -> a)
iff_to_and = (id, id)