basics_minimal.dk

#REQUIRE cc.
#REQUIRE dk_bool.
#REQUIRE dk_logic.
#REQUIRE dk_tuple.

(; Ceci est une version minimale écrite à la main du fichier
habituellement généré basics.dk. Ce fichier permet de tester Zenon
indépendamment de FoCaLiZe. ;)

def Is_true := dk_logic.ebP.

def bool__t := dk_bool.bool.
def true := dk_bool.true.
def false := dk_bool.false.

def _amper__amper_ : cc.eT bool__t -> cc.eT bool__t -> cc.eT bool__t
               := dk_bool.and.

def _bar__bar_ : cc.eT bool__t -> cc.eT bool__t -> cc.eT bool__t
           := dk_bool.or.

def _tilda__tilda_ : cc.eT bool__t -> cc.eT bool__t := dk_bool.not.

def _bar__lt__gt__bar_ : cc.eT bool__t -> cc.eT bool__t -> cc.eT bool__t
                   := dk_bool.xor.

def prod := dk_tuple.prod.

def pair (a : cc.uT)
         (b : cc.uT)
         (x : cc.eT a)
         (y : cc.eT b)
         : cc.eT (dk_tuple.prod a b) :=
  (dk_tuple.pair a b x y).

def fst (a : cc.uT)
        (b : cc.uT)
        (x : cc.eT (dk_tuple.prod a b)) :
        cc.eT a :=
      dk_tuple.fst a b x.

def snd (a : cc.uT)
        (b : cc.uT)
        (x : cc.eT (dk_tuple.prod a b)) :
        cc.eT b :=
      dk_tuple.snd a b x.

_equal_ : a : cc.uT -> cc.eT a -> cc.eT a -> cc.eT bool__t.

def syntactic_equal := _equal_.

__beq_refl  : a : cc.uT ->
              x : cc.eT a ->
              dk_logic.eP (dk_logic.ebP (_equal_ a x x)).

__beq_symm  : a : cc.uT ->
              x : cc.eT a ->
              y : cc.eT a ->
              dk_logic.eP (dk_logic.ebP (_equal_ a x y)) ->
              dk_logic.eP (dk_logic.ebP (_equal_ a y x)).

__beq_trans  : a : cc.uT ->
               x : cc.eT a ->
               y : cc.eT a ->
               z : cc.eT a ->
               dk_logic.eP (dk_logic.ebP (_equal_ a x y)) ->
               dk_logic.eP (dk_logic.ebP (_equal_ a y z)) ->
               dk_logic.eP (dk_logic.ebP (_equal_ a x z)).