4.2. Module: alba.core.logic

4.2.1. Axioms and Builtin Definitions

Predicate (A: Any): Any := A -> Prop

Relation (A B: Any): Any := A -> B -> Prop

Endorelation (A: Any): Any := Relation A A

class False: Prop :=     -- no constructor

class True: Prop  := trueValid: True

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

(/=) {A: Any} (a b: A): Prop :=
    Not (a = b)

class (/\) (A B: Prop): Prop :=
    (,): A -> B -> (/\)

(<->) (A B: Prop): Prop
    -- 'A <-> B': 'A' and 'B' are logically equivalent
:=
    (A -> B) /\ (B -> A)

class (\/) (A B: Prop): Prop :=
    left  : A -> (\/)
    right : B -> (\/)

class Exist {A: Any} (P: Predicate A): Prop :=
    exist {x}: P x -> Exist

class (=) {A: Any}: Endorelation A :=
    identical {x} : x = x

class Accessible {A: Any} (R: Endorelation A): Predicate A :=
    access {x}: (∀ y, R y x -> Accessible y) -> Accessible x

4.2.2. Equality

(=).flip {A: Any}: all {a b: A}: a = b -> b = a
    -- Equality is symmetric.
:= case
    \ identical := identical

    -- long form
    \ {x} {x} (identical {x}) := identical {x}


(=).(+) {A: Any}: all {a b c: A}: a = b -> b = c -> a = c
    -- Equality is transitive.
:= case
    \ identical identical := identical

    -- long form
    \ {x} {x} {x} (identical {x}) (identical {x}) :=
        identical {x}


(=).inject
    {A: Any}
    {F: A -> Any}
    (f: all x: F x)
    : all {a b}: a = b -> f a = f b
    -- Equal arguments to a function imply equal results.
:= case
    \ identical = identical

    -- long form
    \ {x} {x} (identical {x}) :=
        identical {f x}


(=).substitute
    {A: Any}
    : all {a b} {F: A -> Any}: a = b -> F a -> F b
    -- Equal expressions satisfy the same predicate
:= case
    \ identical e :=
        e

    -- long form
    \ {x x F} (identical {x}) e :=
        e