/idris-logic

Propositional logic tools, inspired by the Coq standard library.

Primary LanguageIdrisMIT LicenseMIT

||| An Idris port of Coq.Init.Logic
module Logic

import Data.Bifunctor

%access export

Propositional connectives

Unit

() is the always true proposition (⊤).

%elim data Unit = MkUnit

Void

Void is the always false proposition (⊥).

%elim data Void : Type where

Negation

Not a, written ~a, is the negation of a.

syntax "~" [x] = (Not x)
Not : Type -> Type
Not a = a -> Void

Conjunction

And a b, written (a, b), is the conjunction of a and b.

Conj p q is a proof of (a, b) as soon as p is a proof of a and q a proof of b.

proj1 and proj2 are first and second projections of a conjunction.

syntax "(" [a] "," [b] ")" = (And a b)

||| The conjunction of `a` and `b`.
data And : Type -> Type -> Type where
     Conj : a -> b -> (a, b)

implementation Bifunctor And where
    bimap f g (Conj a b) = Conj (f a) (g b)

||| First projection of a conjunction.
proj1 : (a, b) -> a
proj1 (Conj a _) = a

||| Second projection of a conjunction.
proj2 : (a, b) -> b
proj2 (Conj _ b) = b

Disjunction

Either a b is the disjunction of a and b.

data Either : Type -> Type -> Type where
     Left   : a -> Either a b
     Right  : b -> Either a b

Biconditional

Proof Wiki

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

infixl 9 <->

||| The biconditional is a *binary connective* that can be voiced:
||| *p* **if and only if** *q*.
public export
(<->) : Type -> Type -> Type
(<->) a b = (a -> b, b -> a)

Biconditional is Reflexive

Proof Wiki

⊢φ ⇔ φ

||| The biconditional operator is reflexive.
iffRefl : a <-> a
iffRefl = Conj id id

Biconditional is Transitive

Proof Wiki

||| The biconditional operator is transitive.
iffTrans : (a <-> b) -> (b <-> c) -> (a <-> c)
iffTrans (Conj ab ba) (Conj bc cb) =
    Conj (bc . ab) (ba . cb)

Biconditional is Commutative

Proof Wiki

φ ⇔ ψ ⊣ ⊢ψ ⇔ φ

or

⊢(φ ⇔ ψ)⇔(ψ ⇔ φ)

||| The biconditional operator is commutative.
iffSym : (a <-> b) -> (b <-> a)
iffSym (Conj ab ba) = Conj ba ab

andIffCompatLeft

ψ ⇔ χ ⊣ ⊢(φ ∧ ψ)⇔(φ ∧ χ)

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

andIffCompatRight

ψ ⇔ χ ⊣ ⊢(ψ ∧ φ)⇔(χ ∧ φ)

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

orIffCompatLeft

ψ ⇔ χ ⊢ (φ ∨ ψ)⇔(φ ∨ χ)

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

orIffCompatRight

ψ ⇔ χ ⊢ (ψ ∨ φ)⇔(χ ∨ φ)

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

negVoid

¬φ ⊣ ⊢φ ⇔ ⊥

or

⊢¬φ ⇔ (φ ⇔ ⊥)

negVoid : (~a) <-> (a <-> Void)
negVoid = Conj (flip Conj void) proj1

andCancelLeft

andCancelLeft : (b -> a) ->
                (c -> a) ->
                (((a, b) <-> (a, c)) <-> (b <-> c))
andCancelLeft ba ca = Conj (bimap f g) andIffCompatLeft
  where
    f h b = proj2 . h $ Conj (ba b) b
    g h c = proj2 . h $ Conj (ca c) c

andCancelRight

andCancelRight : (b -> a) ->
                 (c -> a) ->
                 (((b, a) <-> (c, a)) <-> (b <-> c))
andCancelRight ba ca = Conj (bimap f g) andIffCompatRight
  where
    f h b = proj1 . h $ Conj b (ba b)
    g h c = proj1 . h $ Conj c (ca c)

Conjunction is Commutative

Proof Wiki

Formulation 1

φ ∧ ψ ⊣ ⊢ψ ∧ φ

Formulation 2

⊢(φ ∧ ψ)⇔(ψ ∧ φ)

Source

||| Conjunction is commutative.
andComm : (a, b) <-> (b, a)
andComm = Conj swap swap
  where
    swap : (p, q) -> (q, p)
    swap (Conj p q) = Conj q p

Conjunction is Associative

Proof Wiki

Formulation 1

(φ ∧ ψ)∧χ ⊣ ⊢φ ∧ (ψ ∧ χ)

Formulation 2

⊢((φ ∧ ψ)∧χ)⇔(φ ∧ (ψ ∧ χ))

Source

||| Conjunction is associative.
andAssoc : ((a, b), c) <-> (a, (b, c))
andAssoc = Conj f g
  where
    f abc@(Conj (Conj a b) c) = Conj a (first proj2 abc)
    g abc@(Conj a (Conj b c)) = Conj (second proj1 abc) c

orCancelLeft

(ψ ⟹ ¬φ)⟹(χ ⟹ ¬φ)⟹(((φ ∨ ψ)⇔(φ ∨ χ)) ⇔ (ψ ⇔ χ))

orCancelLeft : (b -> ~a) ->
               (c -> ~a) ->
               ((Either a b <-> Either a c) <-> (b <-> c))
orCancelLeft bNotA cNotA = Conj (bimap f g) orIffCompatLeft
  where
    f ef b = go (bNotA b) (ef (Right b))
    g eg c = go (cNotA c) (eg (Right c))
    go : (~a) -> Either a b -> b
    go lf = either (void . lf) id

orCancelRight

orCancelRight : (b -> ~a) ->
                (c -> ~a) ->
                ((Either b a <-> Either c a) <-> (b <-> c))
orCancelRight bNotA cNotA = Conj (bimap f g) orIffCompatRight
  where
    f ef b = go (bNotA b) (ef (Left b))
    g eg c = go (cNotA c) (eg (Left c))
    go : (~p) -> Either q p -> q
    go rf = either id (void . rf)

Disjunction is Commutative

Proof Wiki

(φ ∨ ψ)⇔(ψ ∨ φ)

||| Disjunction is commutative.
orComm : Either a b <-> Either b a
orComm = Conj mirror mirror

Disjunction is Associative

Proof Wiki

(φ ∨ ψ)∨χ ⊢ φ ∨ (ψ ∨ χ)

||| Disjunction is associative on the left.
orAssocLeft : Either (Either a b) c -> Either a (Either b c)
orAssocLeft = either (second Left) (pure . pure)

φ ∨ (ψ ∨ χ)⊢(φ ∨ ψ)∨χ

||| Disjunction is associative on the right.
orAssocRight : Either a (Either b c) -> Either (Either a b) c
orAssocRight = either (Left . Left) (first Right)

Formulation 1

(φ ∨ ψ)∨χ ⊣ ⊢φ ∨ (ψ ∨ χ)

Formulation 2

⊢((φ ∨ ψ)∨χ)⇔(φ ∨ (ψ ∨ χ))

Source

||| Disjunction is associative.
orAssoc : Either (Either a b) c <-> Either a (Either b c)
orAssoc = Conj orAssocLeft orAssocRight

iffAnd

φ ⇔ ψ ⊢ (φ ⟹ ψ)∧(ψ ⟹ φ)

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

iffAndTo

φ ⇔ ψ ⊣ ⊢(φ ⟹ ψ)∧(ψ ⟹ φ)

or

⊢(φ ⇔ ψ)⇔((φ ⟹ ψ)∧(ψ ⟹ φ))

iffToAnd : (a <-> b) <-> (a -> b, b -> a)
iffToAnd = Conj id id