2.1. Logic

2.1.1. Function Composition

(|>) {A: Any} {F: A -> Any} (a: A) (f: all x: F x): F a
        -- 'a |> f' is equivalent to 'f a'.
        -- It is left associative
:=
    f a


(<|) {A: Any} {F: A -> Any} (f: all x: F x) (a: A): F a
        -- 'f <| a' is equivalent to 'f a'
        -- It is right associative, therefore it can be composed
        -- 'g <| f <|a' instead of 'g (f a)'
:=
    f a



(>>) {A B C: Any} (f: A -> B) (g: B -> C): A -> C
        -- '(f >> g) x' is equivalent to 'g (f x)'
:=
    \ x := g (f x)



(<<) {A B C: Any} (f: B -> C) (g: A -> B): A -> C
        -- '(f << g) x' is equivalent to 'f (g x)'
:=
    \ x := g (f x)

2.1.2. Propositions

type True: Prop :=
    (): True

type False: Prop := -- no constructor


(Not) (P: Prop): Prop := P -> False


type (/\) (A B: Prop): Prop :=
        -- (/\) is right associative i.e.
        -- A /\ B /\ C = A /\ (B /\ C)
    (,): A -> B -> _

type (\/) (A B: Prop): Prop :=
        -- (\/) is right associative i.e.
        -- A \/ B \/ C = A \/ (B \/ C)
    left:  A -> _
    right: B -> _


type Exist {A: Any} (P: A -> Prop): Prop :=
    exist {w}: P w -> _


All {A: Any} (P: A -> Prop): Prop :=
    all {x}: P x

Note that (,), left, right and exist have the types

(,):   all {A B: Prop}: A -> B -> A /\ B
left:  all {A B: Prop}: A -> A \/ B
right: all {A B: Prop}: B -> A \/ B
exist: all {A: Any} {P: A -> Prop} {w: A}: P w -> Exist P

The parameter arguments of an inductive type are all implicit and the same for all constructors of the type.

It is a simple exercise to prove commutativity of conjunction and disjunction.

flip {A B: Prop}: A /\ B -> B /\ A
:= case
    (p,q) := (q,p)

flip {A B: Prop}: A \/ B -> B \/ A
:= case
    (left p)  := right p
    (right q) := left q

From a contradiction (represented by an inhabitant of False) follows anything (ex falso quodlibet). This can be proved by a pattern match on an inhabitant of False. Since the type False has no constructors, the pattern match has no clauses.

exFalso: False -> all {A: Prop}: A
:=
    case
        -- no constructors

In classical logic the following propositions are equivalent

A                   Not Not A           -- double negation

Not (A /\ B)        Not A \/ Not B      -- de Morgan for and

Not (A \/ B)        Not A /\ Not B      -- de Morgan for or

A -> B              Not B -> Not A      -- modus tollens

We are in the domain of constructive logic. Therefore the double negation law can be proved only in forward direction, the de Morgan law for conjunction can be proved only in backward direction, the de Morgan law for disjunction can be proved in both directions.

doubleNegation {A: Prop}: A -> Not Not A
:=
    \ (pA: A) (pNotA: A -> False): False
    :=
        pNotA p


deMorganAnd {A B: Prop}: Not A \/ Not B -> Not (A /\ B)
:=
    (left pNotA)  (pA, pB) :=
        pNotA pA

    (right pNotB)  (pA, pB) :=
        pNotB pB


deMorganOrFwd {A B: Prop}: Not (A \/ B) -> Not A /\ Not B
:=
    \ pNotAOrB := (pNotAOrB << left, pNotAOrB << right)


deMorganOrBwd {A B: Prop}: Not A /\ Not B -> Not (A \/ B)
:= case
    (pNotA, pNotB) (left pA)  := pNotA pA
    (pNotA, pNotB) (right pA) := pNotB pB


modusTollens {A B: Prop}: (A -> B) -> Not B -> Not A
:=
    \ ab notb := ab >> notb

In classical logic there are the de Morgans laws for universal and existential quantification which state the equivalence of

Not (All P)                 Exist (Not << P)

Not (Exist P)               All (Not << P)

As in the case of conjunction and disjunction, for universal quantification only the backward direction can be proved.

deMorganAll {A: Any} {P: A -> Prop}: Exist (Not << P) -> Not (All P)
:= case
    (exist xNotP) xP := xNot xP


deMorganExistFwd {A: Any} {P: A -> Prop}: Not (Exist P) -> All (Not << P)
:=
    \ noXinP xP := noXinP (exist xP)


deMorganExistBwd {A: Any} {P: A -> Prop}: All (Not << P) -> Not (Exist P)
:=
    \ allXnotinP (exist xP) := allXnotinP xP

2.1.3. Equality

type (=) {A: Any}: A -> A -> Prop :=
    refl {x}: x = x

The equality relation is the smallest reflexive relation. This fact can be proved by pattern match.

recurse {A: Any} {R: A -> A -> Any} (f: all x: R x x)
: all (x y: A): x = y -> R x y
:=
    case
        (x) (_} refl := f x

The elaboration of the pattern match expression unifies x and y. Therefore f: R x x has the correct required type.

Note that R is not a propositional relation because it does not have the type A -> A -> Prop. However the function f is able to generate for each x an inhabitant of R x x. Therefore R is in the nonpropositional world the equivalent of a reflexive relation.

Note further that f is not a ghost function. Given a runtime object x it returns a runtime object of type R x x. However when fed with a ghost object it returns only a ghost object. Since recurse has to return a runtime object, the argument x cannot be implicit.

Even if the arguments x and y are not implicit, the are still derivable by unification bcause they are contained in the result type R x y.

More important than the recursor is the proof that (=) is leibniz equality which says that equal terms are indistinguishable.

cast {A: Any} {F: A -> Any}: all {a b}: a = b -> F a -> F b
:= case
    refl x := x

Equality is a congruence as well.

congruence {A B: Any} {a b: A) {f: A -> B}: a = b -> f a = f b
            --             ^ mandatory implicit (propositional type)
:=
    recurse (\ x : f x = f x := refl) a b

-- higher order unification of the metavariable R:

    R x x ~ (f x = f x)
    R a b ~ (f a = f b)

    R x y := (f x = f y)

Congruence can be proven with leibniz equality as well.

congruence {A B: Any} {a b: A} {f: A -> B} (eq: a = b) -> f a = f b
:=
    cast eq (refl {f a})

-- higher order unification of the metavarialbe F

F b ~ f a = f b

    F x := F1 x = F2 x
    F1 b ~ f a
        F1 x := f (F11 x)
        F11 b ~ a
            F11 x := a

        F2 x := f (F21 x)
        F21 b ~ b

    F2 b ~ f b

F a ~ f a = f a
f a = f (F21 a) ~ f a = f a
    F21 x := x

The most straighforward proof of leibniz equaility is by pattern match.

congruence {A B: Any}: all {a b} {f: A -> B}: a = b -> f a = f b
:= case
    refl := refl

Equality is symmetric and transitive.

flip {A: Any} {a b: A}: a = b -> b = a
:=
    recurse (\ x : x = x := refl) a b

    -- type of refl

    refl : all {A: Any} {x: A}: x = x


(,) {A: Any} {a b c: A}: a = b -> b = c -> a = c
:=
    flip >> cast

    -- instantiation of F

    F b ~ b = c
    F a ~ a = c

2.1.4. Decisions

type Decision (A: Prop) :=
    true:  A     -> _
    false: Not A -> _


Decider {A: Any} (P: A -> Prop): Any :=
        -- Type of a decider for a predicate
    all x: Decision (P x)

Decider {A B: Any} (R: A -> B -> Prop) :=
        -- Type of a decider of a relation
    all x y: Decision (R x y)

A type is decidable if it is possible to decide if two object of that type are equal. I.e. the type has a decider for equality.

abstract type Decidable (A: Any) :=
    (=): Decider ((=) {A})

If there is an endorelation between two objects of a certain type then it might be possible to compare the two objects.

type Comparison {A: Any} (R: A -> A -> Prop) (x y: A) :=
    lt:  R x y -> Not R y x -> _
    eqv: R x y -> R y x     -> _
    gt:  R y x -> Not R x y -> _


Comparer {A: Any} (R: A -> A -> Prop): Any :=
    all x y -> Comparison R x y


abstract type Comparable {A: Any} (R: A -> A -> Prop) :=
    compare: Comparer R

2.1.5. Refinement

An object of a refinement type of type A is an object of type A and a proof that the object satisfies a certain predicate P. The refinement type is like the exisitence type with the difference that the witness is not a ghost object.

type Refine {A: Any} (P: A -> Prop): Any :=
    (,) {w}: P w -> Refine