cc.dk

#NAME cc.
(; Calculus of Construction embedded into Lambda-Pi Modulo ;)

uT : Type.
def eT : uT -> Type.

Pi : X : uT -> ((eT X) -> uT) -> uT.
PiT : (uT -> uT) -> uT.

[X : uT, Y : (eT X) -> uT]
    eT (Pi X Y) --> x : (eT X) -> (eT (Y x))
[Y : uT -> uT]
    eT (PiT Y) --> x : uT -> eT (Y x).

def Arrow : uT -> uT -> uT.
[ t1 : uT, t2 : uT ]
    Arrow t1 t2 --> Pi t1 (x : eT t1 => t2).

classical.dk

(; Law of excluded middle,
   defined directly as the elimination of the (p \/ ~ p) disjunction ;)

classic : p : logic.prop -> z : logic.prop ->
          (logic.proof p -> logic.proof z) ->
          (logic.proof (logic.not p) -> logic.proof z) ->
          logic.proof z.

(; Proof by contradiction using the exlcuded middle ;)

def nnpp (p : logic.prop)
  : logic.proof (logic.not (logic.not p)) -> logic.proof p :=
  H1 : logic.proof (logic.not (logic.not p)) =>
  classic p p (H2 : logic.proof p => H2)
              (H3 : logic.proof (logic.not p) => H1 H3 p).


(; de Morgan Laws for quantifiers ;)

def not_all_not_ex
  (u : logic.type) (p : logic.term u -> logic.prop) :
  logic.proof (logic.not (logic.forall u (x : logic.term u => logic.not (p x)))) ->
  logic.proof (logic.exists u p) :=
    notall : logic.proof (logic.not (logic.forall u (x : logic.term u => logic.not (p x)))) =>
      nnpp (logic.exists u p) (abs : logic.proof (logic.not (logic.exists u p)) =>
        notall (n : logic.term u => H : logic.proof (p n) =>
          abs (z : logic.prop => p0 : (x : logic.term u -> logic.proof (p x) -> logic.proof z) =>
            p0 n H
          )
        )
      ).

def not_all_ex_not
  (u : logic.type) (p : logic.term u -> logic.prop) :
  logic.proof (logic.not (logic.forall u p)) ->
  logic.proof (logic.exists u (x : logic.term u => logic.not (p x))) :=
    notall : logic.proof (logic.not (logic.forall u p)) =>
      not_all_not_ex u (x : logic.term u => logic.not (p x)) (
        (all : logic.proof (logic.forall u (x : logic.term u => logic.not (logic.not (p x)))) =>
          notall (n : logic.term u =>
            nnpp (p n) (all n)
          )
        )
      ).

def not_ex_all_not
  (u : logic.type) (p : logic.term u -> logic.prop) :
  logic.proof (logic.not (logic.exists u p)) ->
  logic.proof (logic.forall u (x : logic.term u => logic.not (p x))) :=
    notex : logic.proof (logic.not (logic.exists u p)) =>
      n : logic.term u => abs : logic.proof (p n) =>
        notex (z : logic.prop =>
          p0 : (x : logic.term u -> logic.proof (p x) -> logic.proof z) =>
            p0 n abs
          ).

def not_ex_not_all
  (u : logic.type) (p : logic.term u -> logic.prop) :
  logic.proof (logic.not (logic.exists u (x : logic.term u => logic.not (p x)))) ->
  logic.proof (logic.forall u p) :=
    H : logic.proof (logic.not (logic.exists u (x : logic.term u => logic.not (p x)))) =>
      n : logic.term u =>
        nnpp (p n) (k : logic.proof (logic.not (p n)) =>
          H (z : logic.prop =>
            p0 : (x : logic.term u -> logic.proof (logic.not (p x)) -> logic.proof z) =>
              p0 n k
          )
        ).


(; de Morgan Laws for type quantifiers ;)

def not_all_not_ex_type
  (p : logic.type -> logic.prop) :
  logic.proof (logic.not (logic.foralltype (x : logic.type => logic.not (p x)))) ->
  logic.proof (logic.existstype p) :=
    notall : logic.proof (logic.not (logic.foralltype (x : logic.type => logic.not (p x)))) =>
      nnpp (logic.existstype p) (abs : logic.proof (logic.not (logic.existstype p)) =>
        notall (n : logic.type => H : logic.proof (p n) =>
          abs (z : logic.prop => p0 : (x : logic.type -> logic.proof (p x) -> logic.proof z) =>
            p0 n H
          )
        )
      ).

def not_all_ex_not_type
  (p : logic.type -> logic.prop) :
  logic.proof (logic.not (logic.foralltype p)) ->
  logic.proof (logic.existstype (x : logic.type => logic.not (p x))) :=
    notall : logic.proof (logic.not (logic.foralltype p)) =>
      not_all_not_ex_type (x : logic.type => logic.not (p x)) (
        (all : logic.proof (logic.foralltype (x : logic.type => logic.not (logic.not (p x)))) =>
          notall (n : logic.type =>
            nnpp (p n) (all n)
          )
        )
      ).

def not_ex_all_not_type
  (p : logic.type -> logic.prop) :
  logic.proof (logic.not (logic.existstype p)) ->
  logic.proof (logic.foralltype (x : logic.type => logic.not (p x))) :=
    notex : logic.proof (logic.not (logic.existstype p)) =>
      n : logic.type => abs : logic.proof (p n) =>
        notex (z : logic.prop =>
          p0 : (x : logic.type -> logic.proof (p x) -> logic.proof z) =>
            p0 n abs
          ).

def not_ex_not_all_type
  (p : logic.type -> logic.prop) :
  logic.proof (logic.not (logic.existstype (x : logic.type => logic.not (p x)))) ->
  logic.proof (logic.foralltype p) :=
    H : logic.proof (logic.not (logic.existstype (x : logic.type => logic.not (p x)))) =>
      n : logic.type =>
        nnpp (p n) (k : logic.proof (logic.not (p n)) =>
          H (z : logic.prop =>
            p0 : (x : logic.type -> logic.proof (logic.not (p x)) -> logic.proof z) =>
              p0 n k
          )
        ).

dk_logic.dk

#NAME dk_logic.

(; Impredicative prop ;)

prop : cc.uT.
Prop : Type.
[] cc.eT prop --> Prop.
(; def ebP : cc.eT dk_bool.bool -> Prop. ;)

imp : Prop -> Prop -> Prop.
forall_type : (cc.uT -> Prop) -> Prop.
forall : A : cc.uT -> (cc.eT A -> Prop) -> Prop.

def eeP : Prop -> cc.uT.
def eP : Prop -> Type
   := f : Prop => cc.eT (eeP f).
[ f1 : Prop, f2 : Prop ]
    eeP (imp f1 f2)
      -->
    cc.Arrow (eeP f1) (eeP f2)
[ A : cc.uT, f : cc.eT A -> Prop ]
    eeP (forall A f)
      -->
    cc.Pi A (x : cc.eT A => eeP (f x)).

[ f : cc.uT -> Prop ]
    eeP (forall_type f)
      -->
    cc.PiT (x : cc.uT => eeP (f x)).

def True : Prop := forall prop (P : Prop => imp P P).
def False : Prop := forall prop (P : Prop => P).
def not (f : Prop) : Prop := imp f False.
def and (A : Prop) (B : Prop) : Prop :=
  forall prop (P : Prop => imp (imp A (imp B P)) P).
def or  (A : Prop) (B : Prop) : Prop :=
  forall prop (P : Prop => imp (imp A P) (imp (imp B P) P)).
def eqv (A : Prop) (B : Prop) : Prop :=
  and (imp A B) (imp B A).

def exists (A : cc.uT) (f : cc.eT A -> Prop) : Prop :=
  forall prop (P : Prop => imp (forall A (x : cc.eT A => imp (f x) P)) P).
def forallc (A : cc.uT) (f : cc.eT A -> Prop) : Prop :=
  not (not (forall A (x : cc.eT A => not (not (f x))))).
def existsc (A : cc.uT) (f : cc.eT A -> Prop) : Prop :=
  not (not (exists A (x : cc.eT A => not (not (f x))))).

def exists_type (f : cc.uT -> Prop) : Prop
:= forall prop (z : Prop =>
                (imp (forall_type (a : cc.uT =>
                                   imp (f a) z))
                     z)).


def TrueT : Type := eP True.
def FalseT : Type := eP False.
I : TrueT.
False_elim : A : cc.uT -> FalseT -> cc.eT A.

(;
def Istrue : dk_bool.Bool -> Type.
[ b : dk_bool.Bool ] Istrue b --> eP (ebP b).
;)

def and_intro (f1 : Prop)
              (f2 : Prop)
              (H1 : eP f1)
              (H2 : eP f2)
              : eP (and f1 f2)
    := f3 : Prop =>
       H3 : (eP f1 -> eP f2 -> eP f3) =>
       H3 H1 H2.

def and_elim1 (f1 : Prop)
              (f2 : Prop)
              (H3 : eP (and f1 f2))
              : eP f1
    := H3 f1 (H1 : eP f1 => H2 : eP f2 => H1).

def and_elim2 (f1 : Prop)
              (f2 : Prop)
              (H3 : eP (and f1 f2))
              : eP f2
    := H3 f2 (H1 : eP f1 => H2 : eP f2 => H2).

def or_intro1 (f1 : Prop)
              (f2 : Prop)
              (H1 : eP f1)
              : eP (or f1 f2)
    := f3 : Prop =>
       H13 : (eP f1 -> eP f3) =>
       H23 : (eP f2 -> eP f3) =>
       H13 H1.

def or_intro2 (f1 : Prop)
              (f2 : Prop)
              (H2 : eP f2)
              : eP (or f1 f2)
    := f3 : Prop =>
       H13 : (eP f1 -> eP f3) =>
       H23 : (eP f2 -> eP f3) =>
       H23 H2.

def or_elim (f1 : Prop)
            (f2 : Prop)
            (f3 : Prop)
            (H3 : eP (or f1 f2))
            (H13 : eP (imp f1 f3))
            (H23 : eP (imp f2 f3))
            : eP f3
    := H3 f3 H13 H23.

def eqv_intro := f1 : Prop =>
                 f2 : Prop =>
                 and_intro (imp f1 f2) (imp f2 f1).
def eqv_elim1 := f1 : Prop =>
                 f2 : Prop =>
                 and_elim1 (imp f1 f2) (imp f2 f1).
def eqv_elim2 := f1 : Prop =>
                 f2 : Prop =>
                 and_elim2 (imp f1 f2) (imp f2 f1).

(;
[] ebP dk_bool.true --> True
[] ebP dk_bool.false --> False.
;)

(; equality ;)
def equal : A : cc.uT -> x : cc.eT A -> y : cc.eT A -> Prop
      := A : cc.uT => x : cc.eT A => y : cc.eT A =>
                                     forall (cc.Arrow A prop)
                                            (H : (cc.eT A -> Prop) =>
                                             imp (H x) (H y)).

def equalc (A : cc.uT) (x : cc.eT A) (y : cc.eT A) : Prop :=
  not (not (equal A x y)).

def refl : A : cc.uT -> x : cc.eT A -> eP (equal A x x)
     := A : cc.uT => x : cc.eT A =>
                     H : (cc.eT A -> Prop) =>
                     px : eP (H x) => px.

def equal_ind :
            A : cc.uT ->
            H : (cc.eT A -> Prop) ->
            x : cc.eT A ->
            y : cc.eT A ->
            eP (equal A x y) ->
            eP (H x) ->
            eP (H y)
          :=
            A : cc.uT =>
            P : (cc.eT A -> Prop) =>
            x : cc.eT A =>
            y : cc.eT A =>
            eq: eP (equal A x y) =>
            eq P.

def equal_sym : A : cc.uT ->
            x : cc.eT A ->
            y : cc.eT A ->
            eP (equal A x y) ->
            eP (equal A y x)
          :=
            A : cc.uT =>
            x : cc.eT A =>
            y : cc.eT A =>
            eq : eP (equal A x y) =>
            equal_ind
              A
              (z : cc.eT A => equal A z x)
              x
                y
                eq
                (refl A x).

def equal_congr :
  A : cc.uT ->
  B : cc.uT ->
  f : (cc.eT A -> cc.eT B) ->
  x : cc.eT A ->
  y : cc.eT A ->
  eP (equal A x y) ->
  eP (equal B (f x) (f y))
  :=
    A : cc.uT =>
    B : cc.uT =>
    f : (cc.eT A -> cc.eT B) =>
    x : cc.eT A =>
    y : cc.eT A =>
    H : eP (equal A x y) =>
    equal_ind A (z : cc.eT A => equal B (f x) (f z)) x y H (refl B (f x)).

epsilon.dk

(; Axiomatisation for Hilbert's epsilon operator ;)

def epsilon :
  a : logic.type ->
  logic.proof (logic.inhabited a) ->
  (logic.term a -> logic.prop) -> logic.term a.

def epsilon_spec :
  a : logic.type ->
  i : logic.proof (logic.inhabited a) ->
  p :(logic.term a -> logic.prop) ->
  logic.proof (logic.exists a p) ->
  logic.proof (p (epsilon a i p)).

(; Axiomatisation for Hilbert's epsilon operator for type existencials ;)

def epsilon_type : (logic.type -> logic.prop) -> logic.type.

def epsilon_type_spec :
  p :(logic.type -> logic.prop) ->
  logic.proof (logic.existstype p) ->
  logic.proof (p (epsilon_type p)).

logic.dk

#NAME logic.

(; Polymorphic First-order logic for Archsat ;)

def prop  : Type.
def type  : Type.
def proof : prop -> Type.
def term  : type -> Type.
def arrow : type -> type -> type.


(; Constant symbols ;)

def True  : prop.
def False : prop.

def not : prop -> prop.
def and : prop -> prop -> prop.
def or  : prop -> prop -> prop.
def imp : prop -> prop -> prop.
def equiv : prop -> prop -> prop.

def forall : a : type -> (term a -> prop) -> prop.
def exists : a : type -> (term a -> prop) -> prop.

def foralltype : (type -> prop) -> prop.
def existstype : (type -> prop) -> prop.

def equal      : a : type -> term a -> term a -> prop.


(; Proofs of these rules in the encoding of the calculus of constructions ;)

[] type  --> cc.uT.
[] term  --> cc.eT.
[] arrow --> cc.Arrow.
[] prop  --> dk_logic.Prop.
[] proof --> dk_logic.eP.

[] True       --> dk_logic.True.
[] False      --> dk_logic.False.
[] not        --> dk_logic.not.
[] and        --> dk_logic.and.
[] or         --> dk_logic.or.
[] imp        --> dk_logic.imp.
[] equiv      --> dk_logic.eqv.
[] forall     --> dk_logic.forall.
[] exists     --> dk_logic.exists.
[] foralltype --> dk_logic.forall_type.
[] existstype --> dk_logic.exists_type.
[] equal      --> dk_logic.equal.


(; True ;)

def true_intro : proof True :=
  p : prop => x : proof p => x.


(; False ;)

def false_elim (p : prop)
  : proof False -> proof p :=
  H : proof False => H p.


(; Conjunction ;)

def and_intro (p : prop) (q: prop)
  : proof p -> proof q -> proof (and p q) := dk_logic.and_intro p q.

def and_ind (p : prop) (q : prop) (r : prop)
  : (proof p -> proof q -> proof r) -> proof (and p q) -> proof r :=
  f : (proof p -> proof q -> proof r) => H : proof (and p q) => H r f.

def and_elim (p : prop) (q : prop) (r : prop)
  : proof (and p q) -> (proof p -> proof q -> proof r) -> proof r :=
  H : proof (and p q) => f : (proof p -> proof q -> proof r) => H r f.


(; Disjunction ;)

def or_introl (p : prop) (q : prop)
  : proof p -> proof (or p q) :=
  H1 : proof p => z : prop =>
  H2 : (proof p -> proof z) =>
  H3 : (proof q -> proof z) => H2 H1.

def or_intror (p : prop) (q : prop)
  : proof q -> proof (or p q) :=
  H1 : proof q => z : prop =>
  H2 : (proof p -> proof z) =>
  H3 : (proof q -> proof z) => H3 H1.

def or_ind (p : prop) (q: prop) (r: prop)
  : (proof p -> proof r) -> (proof q -> proof r) -> proof (or p q) -> proof r :=
  f : (proof p -> proof r) => g : (proof q -> proof r) => H : proof (or p q) => H r f g.

def or_elim (p : prop) (q: prop) (r: prop)
  : proof (or p q) -> (proof p -> proof r) -> (proof q -> proof r) -> proof r :=
  H : proof (or p q) => f : (proof p -> proof r) => g : (proof q -> proof r) => H r f g.


(; Equality ;)

def eq_subst (a : type) (x : term a) (y: term a) (p : term a -> prop)
  : proof (equal a x y) -> proof (p x) -> proof (p y) :=
  H1 : proof (equal a x y) => H2 : proof (p x) =>
  dk_logic.equal_ind a p x y H1 H2.

def eq_refl (a: type) (x: term a) : proof (equal a x x) := dk_logic.refl a x.

def eq_sym (a : type) (x : term a) (y : term a)
  : proof (equal a x y) -> proof (equal a y x) :=
  H1 : proof (equal a x y) => dk_logic.equal_sym a x y H1.

def not_eq_sym (a : type) (x : term a) (y : term a)
  : proof (not (equal a x y)) -> proof (not (equal a y x)) :=
  H1 : proof (not (equal a x y)) => H2 : proof (equal a y x) =>
  H1 (eq_sym a y x H2).

def eq_trans (a : type) (x : term a) (y : term a) (z : term a)
  : proof (equal a x y) -> proof (equal a y z) -> proof (equal a x z) :=
  H1 : proof (equal a x y) => H2 : proof (equal a y z) =>
  eq_subst a y z (s : term a => equal a x s) H2 H1.


(; Functions and equality ;)

def f_equal
  (a : type) (b : type) (f : term a -> term b) (x : term a) (y : term a)
  : proof (equal a x y) -> proof (equal b (f x) (f y)) :=
  H : proof (equal a x y) =>
    eq_subst a x y (z : term a => equal b (f x) (f z)) H (eq_refl b (f x)).

def f_equal2
  (a : type) (b : type) (c : type) (f : term a -> term b -> term c)
  (x1 : term a) (y1 : term a) (x2 : term b) (y2 : term b)
  : proof (equal a x1 y1) -> proof (equal b x2 y2) -> proof (equal c (f x1 x2) (f y1 y2)) :=
  H1 : proof (equal a x1 y1) => H2 : proof (equal b x2 y2) =>
    eq_subst a x1 y1 (z1 : term a => equal c (f x1 x2) (f z1 y2)) H1 (
      eq_subst b x2 y2 (z2 : term b => equal c (f x1 x2) (f x1 z2)) H2 (
        eq_refl c (f x1 x2)
      )
    ).


(; Type inhabitation ;)

def inhabited : type -> prop.

def inhabits : a : type -> term a -> proof (inhabited a).