Commit 851f7d80 authored by Guillaume GENESTIER's avatar Guillaume GENESTIER

JFLA files

parent 4a14869a
#NAME FOL.
o : Type.
def eps : o -> Type.
i : Type.
top : o.
[ ] eps top --> z:o -> (eps z) -> (eps z).
bot : o.
[ ] eps bot --> z:o -> (eps z).
imp : o -> o -> o.
[a, b] eps (imp a b) --> eps a -> eps b.
def not : o -> o := x:o => imp x bot.
or : o -> o -> o.
[x, y] eps (or x y)
--> z:o -> (eps x -> eps z) -> (eps y -> eps z) -> eps z.
fa_i : (i -> o) -> o.
[y] eps (fa_i y) --> x:i -> eps (y x).
ex_i : (i -> o) -> o.
[y] eps (ex_i y) --> z:o -> (x:i -> eps (y x) -> (eps z)) -> eps z.
const : i.
\ No newline at end of file
#NAME ML.
(; Deep embedding of types ;)
type : Type.
o : type.
i : type.
arrow : type -> type -> type.
(; Shallowing types ;)
def term : type -> Type.
[a : type, b : type] term (arrow a b) --> term a -> term b.
(; type nat = O | S of nat ;)
nat : type.
O : term nat.
S : term nat -> term nat.
def destrO : r : type -> term nat -> term r -> term r -> term r.
def destrS : r : type -> term nat -> (term nat -> term r) -> term r -> term r.
[R,f,d] destrO R O f d --> f.
[R,f,d] destrO R (S _) f d --> d.
[R,f,d] destrS R O f d --> d.
[R,f,d,n] destrS R (S n) f d --> (f n).
def block : A : type -> B : type -> term (arrow (arrow A B) (arrow A B)).
[R, f] block nat R f O --> f O.
[R, f, n] block nat R f (S n) --> f (S n).
(; let prec n = match n with O -> O | S p -> p ;)
def prec : term (arrow nat nat) :=
n => destrO nat n O (destrS nat n (p => p) n).
#SNF prec (S (S O)).
(; let plus n m = match n with O -> m | S p -> S (plus p m) ;)
def plus : term (arrow nat (arrow nat nat)).
[] plus --> n => m => destrO nat n m (destrS nat n (p => S (block nat (arrow nat nat) plus p m)) m).
#SNF plus (S (S (S O))) (S (S (S O))).
#put the path of your dkcheck binary
DKCHECK = dkcheck
#put the path of your dkdep binary
DKDEP = dkdep
DKOPTIONS = -nl -errors-in-snf
DKS=$(wildcard *.dk)
# DKOS need not have the same name that the corresponding Dedukti
# files (modulogic.dk becomes zen.dko) but for each file f.dk, dkdep
# f.dk outputs the name of the produced dko file before the ':'
# character.
DKOS=$(shell cut -d ':' -f 1 .depend)
all: $(DKOS)
%.dko:
$(DKCHECK) -e $(DKOPTIONS) $<
clean:
rm -f *.dko .depend
depend: .depend
.depend:
$(DKDEP) *.dk > ./.depend
-include .depend
#NAME tocheck.
def p : zen.term (zen.iota) -> zen.prop.
def zenon_X0__28Prop_29 : zen.term (zen.iota).
def zenon_G :
zen.proof (zen.not
(zen.exists (zen.iota)
(v_Vm : (zen.term (zen.iota))
=> zen.imp
(p (v_Vm)) (zen.forall (zen.iota)
(v_Vn : (zen.term (zen.iota))
=> p (v_Vn))))))
-> zen.seq.
[] zenon_G -->
v_Vo : (zen.proof (zen.not
(zen.exists (zen.iota)
(v_Vm : (zen.term (zen.iota))
=> zen.imp
(p (v_Vm)) (zen.forall (zen.iota)
(v_Vn : (zen.term (zen.iota))
=> p (v_Vn)))))))
=> zen.Rnotex
(zen.iota)
(v_Vm : (zen.term (zen.iota))
=> zen.imp
(p (v_Vm)) (zen.forall (zen.iota)
(v_Vn : (zen.term (zen.iota))
=> p (v_Vn))))
(zenon_X0__28Prop_29)
(v_Vp : (zen.proof (zen.not
(zen.imp
(p (zenon_X0__28Prop_29)) (zen.forall (zen.iota)
(v_Vn : (zen.term (zen.iota))
=> p (v_Vn))))))
=> zen.Rnotimply
(p (zenon_X0__28Prop_29))
(zen.forall (zen.iota)
(v_Vn : (zen.term (zen.iota))
=> p (v_Vn)))
(v_Vq : (zen.proof (p (zenon_X0__28Prop_29)))
=> v_Vr : (zen.proof (zen.not
(zen.forall (zen.iota)
(v_Vn : (zen.term (zen.iota))
=> p (v_Vn)))))
=> zen.Rnotall
(zen.iota)
(v_Vn : (zen.term (zen.iota))
=> p (v_Vn))
(v_Vs : (zen.term (zen.iota))
=> v_Vt : (zen.proof (zen.not
(p (v_Vs))))
=> zen.Rnotex
(zen.iota)
(v_Vm : (zen.term (zen.iota))
=> zen.imp
(p (v_Vm)) (zen.forall (zen.iota)
(v_Vn : (zen.term (zen.iota))
=> p (v_Vn))))
(v_Vs)
(v_Vu : (zen.proof (zen.not
(zen.imp
(p (v_Vs)) (zen.forall (zen.iota)
(v_Vn : (zen.term (zen.iota))
=> p (v_Vn))))))
=> zen.Rnotimply
(p (v_Vs))
(zen.forall (zen.iota)
(v_Vn : (zen.term (zen.iota))
=> p (v_Vn)))
(v_Vv : (zen.proof (p (v_Vs)))
=> v_Vr : (zen.proof (zen.not
(zen.forall (zen.iota)
(v_Vn : (zen.term (zen.iota))
=> p (v_Vn)))))
=> zen.Raxiom
(p (v_Vs))
(v_Vv)
(v_Vt)
)
(v_Vu)
)
(v_Vo)
)
(v_Vr)
)
(v_Vp)
)
(v_Vo)
.
(; This file was generated by Holide. ;)
#NAME bool_2Ddef.
def type_0 : hol.type :=
hol.bool.
def type_1 : hol.type :=
hol.arr type_0 type_0.
def type_2 : hol.type :=
hol.arr type_1 type_0.
def term_0 : hol.term (hol.arr type_1 type_2) :=
hol.eq type_1.
def term_1 : p_1 : hol.term type_0 -> hol.term type_0 :=
p_1 : hol.term type_0 => p_1.
def term_2 : hol.term type_1 :=
p_1 : hol.term type_0 => term_1 p_1.
def term_3 : hol.term type_0 :=
term_0 term_2 term_2.
(; Constant Data.Bool.T ;)
Data_2EBool_2ET : hol.term type_0.
(; defineConst ;)
thm_0 : hol.proof (hol.eq type_0 Data_2EBool_2ET term_3).
def type_3 : hol.type :=
hol.arr type_0 type_1.
def term_4 : hol.term type_3 :=
hol.eq type_0.
def term_5 : hol.term type_0 :=
Data_2EBool_2ET.
def type_4 : hol.type :=
hol.arr type_3 type_0.
def term_6 : f_1 : hol.term type_3 -> hol.term type_3 :=
f_1 : hol.term type_3 => f_1.
def term_7 : q_1 : hol.term type_0 -> hol.term type_0 :=
q_1 : hol.term type_0 => q_1.
def term_8 : hol.term type_3 :=
p_1 : hol.term type_0 => q_2 : hol.term type_0 => hol.eq type_4 (f_3 : hol.term type_3 => term_6 f_3 (term_1 p_1) (term_7 q_2)) (f_3 : hol.term type_3 => term_6 f_3 term_5 term_5).
(; Constant Data.Bool./\ ;)
Data_2EBool_2E_2F_5C : hol.term type_3.
(; defineConst ;)
thm_1 : hol.proof (hol.eq type_3 Data_2EBool_2E_2F_5C term_8).
def term_9 : hol.term (hol.arr type_3 type_4) :=
hol.eq type_3.
def term_10 : hol.term type_3 :=
Data_2EBool_2E_2F_5C.
def term_11 : hol.term type_3 :=
p_1 : hol.term type_0 => q_2 : hol.term type_0 => term_4 (term_10 (term_1 p_1) (term_7 q_2)) (term_1 p_1).
(; Constant Data.Bool.==> ;)
Data_2EBool_2E_3D_3D_3E : hol.term type_3.
(; defineConst ;)
thm_2 : hol.proof (term_9 Data_2EBool_2E_3D_3D_3E term_11).
def term_12 : hol.term type_3 :=
Data_2EBool_2E_3D_3D_3E.
def type_5 : hol.type -> hol.type :=
A : hol.type => A.
def type_6 : hol.type -> hol.type :=
A : hol.type => hol.arr (type_5 A) type_0.
def type_7 : hol.type -> hol.type :=
A : hol.type => hol.arr (type_6 A) type_0.
def term_13 : A : hol.type -> p_1 : hol.term (type_6 A) -> hol.term (type_6 A) :=
A : hol.type => p_1 : hol.term (type_6 A) => p_1.
def term_14 : A : hol.type -> hol.term (type_7 A) :=
A : hol.type => p_1 : hol.term (type_6 A) => hol.eq (type_6 A) (term_13 A p_1) (x_2 : hol.term (type_5 A) => term_5).
(; Constant Data.Bool.! ;)
Data_2EBool_2E_21 : A : hol.type -> hol.term (type_7 A).
(; defineConst ;)
thm_3 : A : hol.type -> hol.proof (hol.eq (type_7 A) (Data_2EBool_2E_21 (type_5 A)) (term_14 A)).
def term_15 : A : hol.type -> hol.term (hol.arr (type_7 A) (hol.arr (type_7 A) type_0)) :=
A : hol.type => hol.eq (type_7 A).
def term_16 : A : hol.type -> hol.term (type_7 A) :=
A : hol.type => Data_2EBool_2E_21 (type_5 A).
def term_17 : hol.term type_2 :=
Data_2EBool_2E_21 type_0.
def term_18 : A : hol.type -> x_1 : hol.term (type_5 A) -> hol.term (type_5 A) :=
A : hol.type => x_1 : hol.term (type_5 A) => x_1.
def term_19 : A : hol.type -> x_1 : hol.term (type_5 A) -> p_2 : hol.term (type_6 A) -> hol.term type_0 :=
A : hol.type => x_1 : hol.term (type_5 A) => p_2 : hol.term (type_6 A) => term_13 A p_2 (term_18 A x_1).
def term_20 : A : hol.type -> hol.term (type_7 A) :=
A : hol.type => p_1 : hol.term (type_6 A) => term_17 (q_2 : hol.term type_0 => term_12 (term_16 A (x_3 : hol.term (type_5 A) => term_12 (term_19 A x_3 p_1) (term_7 q_2))) (term_7 q_2)).
(; Constant Data.Bool.? ;)
Data_2EBool_2E_3F : A : hol.type -> hol.term (type_7 A).
(; defineConst ;)
thm_4 : A : hol.type -> hol.proof (term_15 A (Data_2EBool_2E_3F (type_5 A)) (term_20 A)).
def term_21 : A : hol.type -> hol.term (type_7 A) :=
A : hol.type => Data_2EBool_2E_3F (type_5 A).
def term_22 : p_1 : hol.term type_0 -> hol.term type_1 :=
p_1 : hol.term type_0 => term_12 (term_1 p_1).
def term_23 : r_1 : hol.term type_0 -> hol.term type_0 :=
r_1 : hol.term type_0 => r_1.
def term_24 : hol.term type_3 :=
p_1 : hol.term type_0 => q_2 : hol.term type_0 => term_17 (r_3 : hol.term type_0 => term_12 (term_22 p_1 (term_23 r_3)) (term_12 (term_12 (term_7 q_2) (term_23 r_3)) (term_23 r_3))).
(; Constant Data.Bool.\/ ;)
Data_2EBool_2E_5C_2F : hol.term type_3.
(; defineConst ;)
thm_5 : hol.proof (term_9 Data_2EBool_2E_5C_2F term_24).
def term_25 : hol.term type_0 :=
term_17 term_2.
(; Constant Data.Bool.F ;)
Data_2EBool_2EF : hol.term type_0.
(; defineConst ;)
thm_6 : hol.proof (term_4 Data_2EBool_2EF term_25).
def term_26 : hol.term type_0 :=
Data_2EBool_2EF.
def term_27 : hol.term type_1 :=
p_1 : hol.term type_0 => term_22 p_1 term_26.
(; Constant Data.Bool.~ ;)
Data_2EBool_2E_7E : hol.term type_1.
(; defineConst ;)
thm_7 : hol.proof (term_0 Data_2EBool_2E_7E term_27).
def term_28 : A : hol.type -> y_1 : hol.term (type_5 A) -> hol.term (type_5 A) :=
A : hol.type => y_1 : hol.term (type_5 A) => y_1.
def term_29 : A : hol.type -> x_1 : hol.term (type_5 A) -> hol.term (type_6 A) :=
A : hol.type => x_1 : hol.term (type_5 A) => hol.eq (type_5 A) (term_18 A x_1).
def term_30 : A : hol.type -> hol.term (type_7 A) :=
A : hol.type => p_1 : hol.term (type_6 A) => term_10 (term_21 A (term_13 A p_1)) (term_16 A (x_2 : hol.term (type_5 A) => term_16 A (y_3 : hol.term (type_5 A) => term_12 (term_10 (term_19 A x_2 p_1) (term_13 A p_1 (term_28 A y_3))) (term_29 A x_2 (term_28 A y_3))))).
(; Constant Data.Bool.?! ;)
Data_2EBool_2E_3F_21 : A : hol.type -> hol.term (type_7 A).
(; defineConst ;)
thm_8 : A : hol.type -> hol.proof (term_15 A (Data_2EBool_2E_3F_21 (type_5 A)) (term_30 A)).
def term_31 : t_1 : hol.term type_0 -> hol.term type_1 :=
t_1 : hol.term type_0 => term_4 t_1.
def term_32 : A : hol.type -> hol.term (hol.arr type_0 (hol.arr (type_5 A) (hol.arr (type_5 A) (type_5 A)))) :=
A : hol.type => t_1 : hol.term type_0 => t1_2 : hol.term (type_5 A) => t2_3 : hol.term (type_5 A) => hol.select (type_5 A) (x_4 : hol.term (type_5 A) => term_10 (term_12 (term_31 t_1 term_5) (term_29 A x_4 t1_2)) (term_12 (term_31 t_1 term_26) (term_29 A x_4 t2_3))).
(; Constant Data.Bool.cond ;)
Data_2EBool_2Econd : A : hol.type -> hol.term (hol.arr type_0 (hol.arr (type_5 A) (hol.arr (type_5 A) (type_5 A)))).
(; defineConst ;)
thm_9 : A : hol.type -> hol.proof (hol.eq (hol.arr type_0 (hol.arr (type_5 A) (hol.arr (type_5 A) (type_5 A)))) (Data_2EBool_2Econd (type_5 A)) (term_32 A)).
def type_8 : hol.type -> hol.type :=
A : hol.type => hol.arr type_0 (hol.arr (type_5 A) (hol.arr (type_5 A) (type_5 A))).
#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).
#NAME cc2.
U_Type : Type.
U_Kind : Type.
def e_Type : U_Type -> Type.
def e_Kind : U_Kind -> Type.
u_Type : U_Kind.
pi_TT : a : U_Type -> (e_Type a -> U_Type) -> U_Type.
pi_TK : a : U_Type -> (e_Type a -> U_Kind) -> U_Kind.
pi_KT : a : U_Kind -> (e_Kind a -> U_Type) -> U_Type.
pi_KK : a : U_Kind -> (e_Kind a -> U_Kind) -> U_Kind.
[] e_Kind u_Type --> U_Type.
[a, b] e_Type (pi_TT a b) --> x: e_Type a -> e_Type (b x).
[a, b] e_Type (pi_KT a b) --> x: e_Kind a -> e_Type (b x).
[a, b] e_Kind (pi_TK a b) --> x: e_Type a -> e_Kind (b x).
[a, b] e_Kind (pi_KK a b) --> x: e_Kind a -> e_Kind (b x).
def id_Type : U_Type -> U_Type :=
x : U_Type => x.
#CHECK id_Type (pi_KT u_Type (a => a)), U_Type.
(; inductive types ;)
list : U_Type -> U_Type.
nil : A : U_Type -> e_Type (list A).
cons : A : U_Type -> e_Type A -> e_Type (list A) -> e_Type (list A).
def elim_list : A : U_Type -> P : (e_Type (list A) -> U_Type) ->
e_Type (P (nil A)) ->
(x : e_Type A -> l2 : e_Type (list A) -> e_Type (P l2) -> e_Type (P (cons A x l2))) ->
l : e_Type (list A) -> e_Type (P l).
[A, P, case_nil, case_cons]
elim_list A P case_nil case_cons (nil {A}) -->
case_nil.
[A, P, case_nil, case_cons, x, l]
elim_list A P case_nil case_cons (cons {A} x l) -->
case_cons x l (elim_list A P case_nil case_cons l).
def append : A : U_Type -> e_Type (list A) -> e_Type (list A) -> e_Type (list A) :=
A => l1 => l2 =>
elim_list A (__ => list A) l2 (x => l1' => l1'l2 => cons A x l1'l2) l1.
(; universes ;)
level : Type.
0 : level.
S : level -> level.
U : level -> Type.
def eps : i : level -> U i -> Type.
u : i : level -> U (S i).
[i] eps _ (u i) --> U i.
def pi : i : level -> a : U i -> b : (eps i a -> U i) -> U i.
[i, a, b] eps _ (pi i a b) --> x : eps i a -> eps i (b x).
lift : i : level -> U i -> U (S i).
[i, a] eps _ (lift i a) --> eps i a.
[i, a, b] pi _ (lift i a) (x => lift {i} (b x)) -->
lift i (pi i a (x => b x)).
#NAME classical_predicate.
(; Deep embedding ;)
alpha : Type. (; Type of atoms ;)
o : Type. (; Type of propositions ;)
s : Type.
bot : o.
top : o.
not : o -> o.
imp : o -> o -> o.
and : o -> o -> o.
or : o -> o -> o.
all_s : (s -> o) -> o.
ex_s : (s -> o) -> o.
atom : alpha -> o.
f : s -> s.
a : s.
P : s -> alpha.
A : alpha.
(; Shallowing translation ;)
def eps : o -> Type.
[] eps bot --> z : o -> eps z.
[] eps top --> z : o -> eps z -> eps z.
[p] eps (not p) --> eps p -> eps bot.
[a, b] eps (imp a b) --> eps a -> eps b.
[a, b] eps (and a b) --> z : o -> (eps a -> eps b -> eps z) -> eps z.
[a, b] eps (or a b) --> z : o -> (eps a -> eps z) -> (eps b -> eps z) -> eps z.
[f] eps (all_s f) --> x : s -> eps (f x).
[f] eps (ex_s f) --> z : o -> (x : s -> eps (f x) -> eps z) -> eps z.
(; classical logic ;)
def atom_c : alpha -> o := a => not (not (atom a)).
def bot_c : o := not (not bot).
def top_c : o := not (not top).
def not_c : o -> o := a => not (not (not a)).
def imp_c : o -> o -> o := a => b => not (not (imp a b)).
def and_c : o -> o -> o := a => b => not (not (and a b)).
def or_c : o -> o -> o := a => b => not (not (or a b)).
def all_s_c : (s -> o) -> o := f => not (not (all_s f)).
def ex_s_c : (s -> o) -> o := f => not (not (ex_s f)).
(; proofs ;)
def nnpp : eps (imp_c (not_c (not_c (atom_c A))) (atom_c A)) :=
h1 => h1 (h2 => h3 => h2 (h4 => h4 (h5 => h5 (h6 => h6 h3)))).
def chapeau : eps (ex_s_c (x => imp_c (atom_c (P x))
(all_s_c (y => atom_c (P y))))) :=
h => h
(z => h0 => h0 a
(h1 => h1 (p => h3 => h3 (x => h4 =>
h (z0 => h5 =>
h5 x (h6 => h6 (h7 =>
po =>
h7 h4))))))).
\ No newline at end of file
#NAME constructive_predicate.
(; Deep embedding ;)
o : Type. (; Type of propositions ;)
s1 : Type.
s2 : Type.
bot : o.
top : o.
not : o -> o.
imp : o -> o -> o.
and : o -> o -> o.
or : o -> o -> o.
all_s1 : (s1 -> o) -> o.
all_s2 : (s2 -> o) -> o.
ex_s1 : (s1 -> o) -> o.
ex_s2 : (s2 -> o) -> o.
f : s1 -> s1.
a : s1.
b : s2.
P : s1 -> o.
Q : s1 -> s2 -> o.
A : o.
B : o.
(; Shallowing translation ;)
def eps : o -> Type.
[] eps bot --> z : o -> eps z.
[] eps top --> z : o -> eps z -> eps z.
[p] eps (not p) --> eps p -> eps bot.
[a, b] eps (imp a b) --> eps a -> eps b.
[a, b] eps (and a b) --> z : o -> (eps a -> eps b -> eps z) -> eps z.
[a, b] eps (or a b) --> z : o -> (eps a -> eps z) -> (eps b -> eps z) -> eps z.
[f] eps (all_s1 f) --> x : s1 -> eps (f x).
[f] eps (all_s2 f) --> x : s2 -> eps (f x).
[f] eps (ex_s1 f) --> z : o -> (x : s1 -> eps (f x) -> eps z) -> eps z.
[f] eps (ex_s2 f) --> z : o -> (x : s2 -> eps (f x) -> eps z) -> eps z.
(; Proof ;)
def thm1 : eps (imp (and A B) (or A B)) :=
p => z => pa => pb => p z (ta => tb => pa ta).
def thm2 : eps (imp (all_s1 (x => imp (P x) (P (f x)))) (imp (P a) (P (f (f a))))) :=
pall => ppa => pall (f a) (pall a ppa).
#NAME dk_bool.
(; Bool ;)
(; Declaration ;)
bool : cc.uT.
def Bool : Type := cc.eT bool.
(; Constructors ;)
true : Bool.
false : Bool.
(; Pattern-matching ;)
def match :
P : (Bool -> cc.uT) ->
cc.eT (P true) ->
cc.eT (P false) ->
b : Bool ->
cc.eT (P b).
[P : Bool -> cc.uT,
Ht : cc.eT (P true),
Hf : cc.eT (P false) ]
match P Ht Hf true --> Ht
[P : Bool -> cc.uT,
Ht : cc.eT (P true),
Hf : cc.eT (P false) ]
match P Ht Hf false --> Hf.
(; Operations ;)
(; polymorphic if .. then .. else .. ;)
def ite :
A : cc.uT ->
Bool ->
cc.eT A ->
cc.eT A ->
cc.eT A.
[ A : cc.uT,
x : cc.eT A,
y : cc.eT A,
b : Bool ]
ite A b x y
-->
match (b : Bool => A) x y b.
def match__true :
Bool ->
A : cc.uT ->
cc.eT A ->
cc.eT A ->
cc.eT A.
[ A : cc.uT, b : Bool, t : cc.eT A, e : cc.eT A]
match__true b A t e --> ite A b t e.
def match__false :
Bool ->
A : cc.uT ->
cc.eT A ->
cc.eT A ->
cc.eT A.
[ A : cc.uT, b : Bool, t : cc.eT A, e : cc.eT A]
match__false b A t e --> ite A b e t.
(; boolean if .. then .. else .. ;)
def iteb : Bool -> Bool -> Bool -> Bool
:= ite bool.
(; negation ;)
def not : Bool -> Bool.
[] not true --> false
[] not false --> true
[ b : Bool ] not (not b) --> b.
(; binary operators ;)
def and : Bool -> Bool -> Bool.
[ b : Bool ] and b true --> b
[ b : Bool ] and true b --> b
[ b : Bool ] and b false --> false
[ b : Bool ] and false b --> false.
def or : Bool -> Bool -> Bool.
[ b : Bool ] or b true --> true
[ b : Bool ] or true b --> true
[ b : Bool ] or b false --> b
[ b : Bool ] or false b --> b.
def xor : Bool -> Bool -> Bool.
[ b : Bool ] xor b true --> not b
[ b : Bool ] xor true b --> not b
[ b : Bool ] xor b false --> b
[ b : Bool ] xor false b --> b.
def imp : Bool -> Bool -> Bool.
[ b : Bool ] imp b true --> true
[ b : Bool ] imp true b --> b
[ b : Bool ] imp b false --> not b
[ b : Bool ] imp false b --> true.
def eqv : Bool -> Bool -> Bool.
[ b : Bool ] eqv b true --> b
[ b : Bool ] eqv true b --> b
[ b : Bool ] eqv b false --> not b
[ b : Bool ] eqv false b --> not b.
(; Associativity ;)
[ b1 : Bool, b2 : Bool, b3 : Bool ]
and b1 (and b2 b3) --> and (and b1 b2) b3.
[ b1 : Bool, b2 : Bool, b3 : Bool ]
or b1 (or b2 b3) --> or (or b1 b2) b3.
[ b1 : Bool, b2 : Bool, b3 : Bool ]
xor b1 (xor b2 b3) --> xor (xor b1 b2) b3.
(; Distributivity ;)
[ b1 : Bool, b2 : Bool, b3 : Bool ]
and b1 (or b2 b3) --> or (and b1 b2) (and b1 b3).
[ b1 : Bool, b2 : Bool, b3 : Bool ]
and (or b1 b2) b3 --> or (and b1 b3) (and b2 b3).
[ b1 : Bool, b2 : Bool ]
not (and b1 b2) --> or (not b1) (not b2).
[ b1 : Bool, b2 : Bool ]
not (or b1 b2) --> and (not b1) (not b2).
[ b1 : Bool, b2 : Bool ]
not (xor b1 b2) --> eqv (not b1) (not b2).
[ b1 : Bool, b2 : Bool ]
not (eqv b1 b2) --> xor (not b1) (not b2).
(; Indempotence ;)
[ b : Bool ]
and b b --> b.
[ b : Bool ]
or b b --> b.
[ b : Bool ]
xor b b --> false.
[ b : Bool ]
imp b b --> true.
[ b : Bool ]
eqv b b --> true.
#NAME dk_logic.
(; Impredicative prop ;)
prop : cc.uT.
def Prop : Type := cc.eT 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).