Commit 3f795b3c authored by Raphael Cauderlier's avatar Raphael Cauderlier

Revert "Replace type by Type."

This reverts commit 1dad75e6.

Conflicts:
	configure

In Dedukti v2.6, we can now declare term as injective so the user can
handle higher-order logic by adding injective rewrite rules on term.
parent f01f1cef
...@@ -9,7 +9,7 @@ endif ...@@ -9,7 +9,7 @@ endif
# Dedukti files # Dedukti files
DKS = $(wildcard *.dk) DKS = $(wildcard *.dk)
DKOS = $(DKS:.dk=.dko) DKOS = $(DKS:.dk=.dko)
DKCHECK_OPTIONS = -coc DKCHECK_OPTIONS =
all: $(DKOS) all: $(DKOS)
......
#NAME eq. #NAME eq.
def type := fol.type.
def types := fol.types. def types := fol.types.
def term := fol.term. def term := fol.term.
def terms := fol.terms. def terms := fol.terms.
...@@ -26,10 +27,10 @@ def O := nat.O. ...@@ -26,10 +27,10 @@ def O := nat.O.
def S := nat.S. def S := nat.S.
(; Equality is a family of binary predicate symbols. ;) (; Equality is a family of binary predicate symbols. ;)
Eq : Type -> predicate. Eq : type -> predicate.
[A] fol.pred_arity (Eq A) --> read_types (S (S O)) A A. [A] fol.pred_arity (Eq A) --> read_types (S (S O)) A A.
def eq (A : Type) : term A -> term A -> prop := pred_apply (Eq A). def eq (A : type) : term A -> term A -> prop := pred_apply (Eq A).
[A,x,y] fol.proof (fol.apply_pred (Eq A) (fol.cons_term _ x _ (fol.cons_term _ y _ fol.nil_term))) --> [A,x,y] fol.proof (fol.apply_pred (Eq A) (fol.cons_term _ x _ (fol.cons_term _ y _ fol.nil_term))) -->
...@@ -37,14 +38,14 @@ def eq (A : Type) : term A -> term A -> prop := pred_apply (Eq A). ...@@ -37,14 +38,14 @@ def eq (A : Type) : term A -> term A -> prop := pred_apply (Eq A).
proof (c x) -> proof (c y). proof (c x) -> proof (c y).
thm eq_refl (A : Type) : proof (all A (x : term A => eq A x x)) thm eq_refl (A : type) : proof (all A (x : term A => eq A x x))
:= :=
x : term A => x : term A =>
c : (term A -> prop) => c : (term A -> prop) =>
H : proof (c x) => H : proof (c x) =>
H. H.
thm eq_symm (A : Type) : thm eq_symm (A : type) :
proof (all A (x : term A => proof (all A (x : term A =>
all A (y : term A => all A (y : term A =>
imp (eq A y x) (eq A x y)))) imp (eq A y x) (eq A x y))))
...@@ -54,7 +55,7 @@ thm eq_symm (A : Type) : ...@@ -54,7 +55,7 @@ thm eq_symm (A : Type) :
H : proof (eq A y x) => H : proof (eq A y x) =>
H (x : term A => eq A x y) (eq_refl A y). H (x : term A => eq A x y) (eq_refl A y).
thm eq_trans (A : Type) : thm eq_trans (A : type) :
proof (all A (x : term A => proof (all A (x : term A =>
all A (y : term A => all A (y : term A =>
all A (z : term A => all A (z : term A =>
...@@ -69,7 +70,7 @@ thm eq_trans (A : Type) : ...@@ -69,7 +70,7 @@ thm eq_trans (A : Type) :
H2 : proof (eq A y z) => H2 : proof (eq A y z) =>
H2 (y : term A => eq A x y) H. H2 (y : term A => eq A x y) H.
thm eq_p_equal (A : Type) (p : term A -> prop) : thm eq_p_equal (A : type) (p : term A -> prop) :
proof (all A (x : term A => proof (all A (x : term A =>
all A (y : term A => all A (y : term A =>
imp (eq A x y) (imp (p x) (p y))))) imp (eq A x y) (imp (p x) (p y)))))
...@@ -79,7 +80,7 @@ thm eq_p_equal (A : Type) (p : term A -> prop) : ...@@ -79,7 +80,7 @@ thm eq_p_equal (A : Type) (p : term A -> prop) :
H : proof (eq A x y) => H : proof (eq A x y) =>
H p. H p.
thm eq_f_equal (A : Type) (B : Type) (f : term A -> term B) : thm eq_f_equal (A : type) (B : type) (f : term A -> term B) :
proof (all A (x : term A => proof (all A (x : term A =>
all A (y : term A => all A (y : term A =>
imp (eq A x y) (eq B (f x) (f y))))) imp (eq A x y) (eq B (f x) (f y)))))
...@@ -110,14 +111,14 @@ def eq_pred_imp : L : types -> p : (terms L -> prop) -> proof (pred_imp L p p). ...@@ -110,14 +111,14 @@ def eq_pred_imp : L : types -> p : (terms L -> prop) -> proof (pred_imp L p p).
thm eq_pred_equal (p : predicate) : proof (pred_imp (pred_arity p) (apply_pred p) (apply_pred p)) thm eq_pred_equal (p : predicate) : proof (pred_imp (pred_arity p) (apply_pred p) (apply_pred p))
:= eq_pred_imp (pred_arity p) (apply_pred p). := eq_pred_imp (pred_arity p) (apply_pred p).
def fun_eq : L : types -> B : Type -> (terms L -> term B) -> (terms L -> term B) -> prop. def fun_eq : L : types -> B : type -> (terms L -> term B) -> (terms L -> term B) -> prop.
[B,b,b'] fun_eq fol.nil_type B b b' --> eq B (b nil_term) (b' nil_term) [B,b,b'] fun_eq fol.nil_type B b b' --> eq B (b nil_term) (b' nil_term)
[A,L,B,f,f'] fun_eq (fol.cons_type A L) B f f' --> [A,L,B,f,f'] fun_eq (fol.cons_type A L) B f f' -->
all A (x : term A => all A (x : term A =>
all A (y : term A => all A (y : term A =>
imp (eq A x y) (fun_eq L B (l : terms L => f (cons_term A x L l)) (l : terms L => f' (cons_term A y L l))))). imp (eq A x y) (fun_eq L B (l : terms L => f (cons_term A x L l)) (l : terms L => f' (cons_term A y L l))))).
def eq_fun_eq : L : types -> B : Type -> f : (terms L -> term B) -> proof (fun_eq L B f f). def eq_fun_eq : L : types -> B : type -> f : (terms L -> term B) -> proof (fun_eq L B f f).
[B,b] eq_fun_eq fol.nil_type B b --> eq_refl B (b nil_term) [B,b] eq_fun_eq fol.nil_type B b --> eq_refl B (b nil_term)
[A,L,B,f,f'] eq_fun_eq (fol.cons_type A L) B f --> [A,L,B,f,f'] eq_fun_eq (fol.cons_type A L) B f -->
x : term A => x : term A =>
......
#NAME fol. #NAME fol.
(; Customization of Emacs mode for Dedukti.
(setq-local dedukti-check-options '("-nc" "-coc"))
(setq-local dedukti-compile-options '("-nc" "-e" "-coc"))
;)
(; Polymorphic first-order logic ;) (; Polymorphic first-order logic ;)
(; Type system ;) (; Type system ;)
def term (A : Type) := A. type : Type.
inj term : type -> Type.
(; Arities of function and predicate symbols are list of types ;) (; Arities of function and predicate symbols are list of types ;)
types : Type. types : Type.
nil_type : types. nil_type : types.
cons_type : Type -> types -> types. cons_type : type -> types -> types.
(; To ease the definition of new symbols, we provide an nary (; To ease the definition of new symbols, we provide an nary
constructor read_types of list of types: constructor read_types of list of types:
...@@ -27,11 +22,11 @@ def nat := nat.Nat. ...@@ -27,11 +22,11 @@ def nat := nat.Nat.
(; The type of the read_types function is defined inductively ;) (; The type of the read_types function is defined inductively ;)
def read_types_T : nat -> Type. def read_types_T : nat -> Type.
[] read_types_T nat.O --> types. [] read_types_T nat.O --> types.
[n] read_types_T (nat.S n) --> Type -> read_types_T n. [n] read_types_T (nat.S n) --> type -> read_types_T n.
(; Adding an element to the tail of a list of types: (; Adding an element to the tail of a list of types:
snoc_type [A1 .. An] B = [A1 .. An B] ;) snoc_type [A1 .. An] B = [A1 .. An B] ;)
def snoc_type : types -> Type -> types. def snoc_type : types -> type -> types.
[A] snoc_type nil_type A --> cons_type A nil_type [A] snoc_type nil_type A --> cons_type A nil_type
[L,A,B] snoc_type (cons_type A L) B --> cons_type A (snoc_type L B). [L,A,B] snoc_type (cons_type A L) B --> cons_type A (snoc_type L B).
...@@ -42,7 +37,7 @@ def read_types_acc : n : nat -> types -> read_types_T n. ...@@ -42,7 +37,7 @@ def read_types_acc : n : nat -> types -> read_types_T n.
[acc] read_types_acc nat.O acc --> acc [acc] read_types_acc nat.O acc --> acc
[n,acc] [n,acc]
read_types_acc (nat.S n) acc read_types_acc (nat.S n) acc
--> t : Type => read_types_acc n (snoc_type acc t). --> t : type => read_types_acc n (snoc_type acc t).
(; read_types n A1 .. An = [A1 .. An] ;) (; read_types n A1 .. An = [A1 .. An] ;)
def read_types (n : nat) : read_types_T n def read_types (n : nat) : read_types_T n
...@@ -54,12 +49,12 @@ def read_types (n : nat) : read_types_T n ...@@ -54,12 +49,12 @@ def read_types (n : nat) : read_types_T n
and fun_codomain should be extended ;) and fun_codomain should be extended ;)
function : Type. function : Type.
def fun_arity : function -> types. def fun_arity : function -> types.
def fun_codomain : function -> Type. def fun_codomain : function -> type.
(; Function application is unnary ;) (; Function application is unnary ;)
terms : types -> Type. terms : types -> Type.
nil_term : terms nil_type. nil_term : terms nil_type.
cons_term : A : Type -> term A -> cons_term : A : type -> term A ->
tail_types : types -> tail_types : types ->
terms tail_types -> terms tail_types ->
terms (cons_type A tail_types). terms (cons_type A tail_types).
...@@ -71,12 +66,12 @@ def apply_fun : f : function -> ...@@ -71,12 +66,12 @@ def apply_fun : f : function ->
applications, we derive an nary application fun_apply ;) applications, we derive an nary application fun_apply ;)
(; read_f_T [A1 .. An] C --> A1 -> .. -> An -> C ;) (; read_f_T [A1 .. An] C --> A1 -> .. -> An -> C ;)
def read_f_T : types -> Type -> Type. def read_f_T : types -> type -> Type.
[C] read_f_T nil_type C --> term C [C] read_f_T nil_type C --> term C
[A,As,C] read_f_T (cons_type A As) C --> term A -> read_f_T As C. [A,As,C] read_f_T (cons_type A As) C --> term A -> read_f_T As C.
(; read_f [A1 .. An] C f a1 .. an --> f [a1 .. an] ;) (; read_f [A1 .. An] C f a1 .. an --> f [a1 .. an] ;)
def read_f : As : types -> C : Type -> (terms As -> term C) -> read_f_T As C. def read_f : As : types -> C : type -> (terms As -> term C) -> read_f_T As C.
[C,f] read_f nil_type C f --> f nil_term. [C,f] read_f nil_type C f --> f nil_term.
[A,As,C,f] read_f (cons_type A As) C f --> a : term A => read_f As C (as : terms As => f (cons_term A a As as)). [A,As,C,f] read_f (cons_type A As) C f --> a : term A => read_f As C (as : terms As => f (cons_term A a As as)).
...@@ -90,8 +85,8 @@ false : prop. ...@@ -90,8 +85,8 @@ false : prop.
and : prop -> prop -> prop. and : prop -> prop -> prop.
or : prop -> prop -> prop. or : prop -> prop -> prop.
imp : prop -> prop -> prop. imp : prop -> prop -> prop.
all : A : Type -> (term A -> prop) -> prop. all : A : type -> (term A -> prop) -> prop.
ex : A : Type -> (term A -> prop) -> prop. ex : A : type -> (term A -> prop) -> prop.
(; Derived connectives ;) (; Derived connectives ;)
def not (p : prop) := imp p false. def not (p : prop) := imp p false.
...@@ -191,17 +186,17 @@ thm imp_intro (a : prop) (b : prop) : (proof a -> proof b) -> proof (imp a b) := ...@@ -191,17 +186,17 @@ thm imp_intro (a : prop) (b : prop) : (proof a -> proof b) -> proof (imp a b) :=
thm imp_elim (a : prop) (b : prop) : proof (imp a b) -> proof a -> proof b := thm imp_elim (a : prop) (b : prop) : proof (imp a b) -> proof a -> proof b :=
Hab : proof (imp a b) => Hab. Hab : proof (imp a b) => Hab.
thm all_intro (A : Type) (p : term A -> prop) : thm all_intro (A : type) (p : term A -> prop) :
(a : term A -> proof (p a)) -> proof (all A p) (a : term A -> proof (p a)) -> proof (all A p)
:= :=
HAp : (a : term A -> proof (p a)) => HAp. HAp : (a : term A -> proof (p a)) => HAp.
thm all_elim (A : Type) (p : term A -> prop) : thm all_elim (A : type) (p : term A -> prop) :
proof (all A p) -> a : term A -> proof (p a) proof (all A p) -> a : term A -> proof (p a)
:= :=
HAp : proof (all A p) => HAp. HAp : proof (all A p) => HAp.
thm ex_intro (A : Type) (p : term A -> prop) : thm ex_intro (A : type) (p : term A -> prop) :
a : term A -> proof (p a) -> proof (ex A p) a : term A -> proof (p a) -> proof (ex A p)
:= :=
a : term A => a : term A =>
...@@ -210,7 +205,7 @@ thm ex_intro (A : Type) (p : term A -> prop) : ...@@ -210,7 +205,7 @@ thm ex_intro (A : Type) (p : term A -> prop) :
Hc : (x : term A -> proof (p x) -> proof c) => Hc : (x : term A -> proof (p x) -> proof c) =>
Hc a Hpa. Hc a Hpa.
thm ex_elim (A : Type) (p : term A -> prop) (c : prop) : thm ex_elim (A : type) (p : term A -> prop) (c : prop) :
proof (ex A p) -> proof (ex A p) ->
(a : term A -> proof (p a) -> proof c) -> (a : term A -> proof (p a) -> proof c) ->
proof c proof c
......
...@@ -5,7 +5,7 @@ https://en.wikipedia.org/wiki/Presburger_arithmetic ;) ...@@ -5,7 +5,7 @@ https://en.wikipedia.org/wiki/Presburger_arithmetic ;)
(; There is just one sort representing natural numbers ;) (; There is just one sort representing natural numbers ;)
Nat : Type. Nat : fol.type.
(; There is just one predicate symbol for equality ;) (; There is just one predicate symbol for equality ;)
EQ : fol.predicate. EQ : fol.predicate.
......
...@@ -3,7 +3,7 @@ include ../.config_vars ...@@ -3,7 +3,7 @@ include ../.config_vars
# Dedukti files # Dedukti files
DKS = $(wildcard *.dk) DKS = $(wildcard *.dk)
DKOS = $(DKS:.dk=.dko) DKOS = $(DKS:.dk=.dko)
DKCHECK_OPTIONS = -I ../fol -nl -coc DKCHECK_OPTIONS = -I ../fol -nl
all: $(DKOS) all: $(DKOS)
......
...@@ -8,6 +8,7 @@ ...@@ -8,6 +8,7 @@
;) ;)
def type := fol.type.
def term := fol.term. def term := fol.term.
def prop := fol.prop. def prop := fol.prop.
def proof := fol.proof. def proof := fol.proof.
...@@ -16,7 +17,7 @@ def imp := fol.imp. ...@@ -16,7 +17,7 @@ def imp := fol.imp.
context : Type. context : Type.
nil_ctx : context. nil_ctx : context.
cons_ctx_var : A : Type -> term A -> context -> context. cons_ctx_var : A : type -> term A -> context -> context.
cons_ctx_proof : A : prop -> proof A -> context -> context. cons_ctx_proof : A : prop -> proof A -> context -> context.
certificate : Type. certificate : Type.
...@@ -79,7 +80,7 @@ clear : prop -> certificate -> certificate. ...@@ -79,7 +80,7 @@ clear : prop -> certificate -> certificate.
[A,G,B,c] run A G (clear B c) --> run A (ctx_remove B G) c. [A,G,B,c] run A G (clear B c) --> run A (ctx_remove B G) c.
no_successful_variable : tac.exc. no_successful_variable : tac.exc.
def try_all_variables : (A : Type -> term A -> certificate) -> context -> certificate. def try_all_variables : (A : type -> term A -> certificate) -> context -> certificate.
[] try_all_variables _ nil_ctx --> raise no_successful_variable [] try_all_variables _ nil_ctx --> raise no_successful_variable
[f,A,a,G] [f,A,a,G]
try_all_variables f (cons_ctx_var A a G) try_all_variables f (cons_ctx_var A a G)
...@@ -92,7 +93,7 @@ def try_all_variables : (A : Type -> term A -> certificate) -> context -> certif ...@@ -92,7 +93,7 @@ def try_all_variables : (A : Type -> term A -> certificate) -> context -> certif
(; with_variable (A => a => c) proves G |- B if c proves G |- B for (; with_variable (A => a => c) proves G |- B if c proves G |- B for
any variable (a : A) in G;) any variable (a : A) in G;)
def with_variable (f : A : Type -> term A -> certificate) : certificate def with_variable (f : A : type -> term A -> certificate) : certificate
:= :=
with_context (G => try_all_variables f G). with_context (G => try_all_variables f G).
...@@ -157,7 +158,7 @@ def read_props : m : nat.Nat -> n : nat.Nat -> k : nat.Nat -> As : props m -> re ...@@ -157,7 +158,7 @@ def read_props : m : nat.Nat -> n : nat.Nat -> k : nat.Nat -> As : props m -> re
def refinen (n : nat.Nat) := read_props nat.O n n nil_prop. def refinen (n : nat.Nat) := read_props nat.O n n nil_prop.
(; fix_term A f a proves G |- B if f (fix_term A f) a proves G |- B ;) (; fix_term A f a proves G |- B if f (fix_term A f) a proves G |- B ;)
def fix_term : A : Type -> ((term A -> certificate) -> term A -> certificate) -> term A -> certificate. def fix_term : A : type -> ((term A -> certificate) -> term A -> certificate) -> term A -> certificate.
[A,F,a] fix_term A F a --> F (fix_term A F) a. [A,F,a] fix_term A F a --> F (fix_term A F) a.
def fix_prop : ((prop -> certificate) -> prop -> certificate) -> prop -> certificate. def fix_prop : ((prop -> certificate) -> prop -> certificate) -> prop -> certificate.
...@@ -203,8 +204,8 @@ def match_prop : prop -> ...@@ -203,8 +204,8 @@ def match_prop : prop ->
(prop -> prop -> certificate) -> (; and ;) (prop -> prop -> certificate) -> (; and ;)
(prop -> prop -> certificate) -> (; or ;) (prop -> prop -> certificate) -> (; or ;)
(prop -> prop -> certificate) -> (; imp ;) (prop -> prop -> certificate) -> (; imp ;)
(A : Type -> (term A -> prop) -> certificate) -> (; all ;) (A : type -> (term A -> prop) -> certificate) -> (; all ;)
(A : Type -> (term A -> prop) -> certificate) -> (; ex ;) (A : type -> (term A -> prop) -> certificate) -> (; ex ;)
(p : fol.predicate -> (p : fol.predicate ->
fol.terms (fol.pred_arity p) -> fol.terms (fol.pred_arity p) ->
certificate) -> certificate) ->
...@@ -258,7 +259,7 @@ def match_imp (A : prop) (c1 : prop -> prop -> certificate) (c2 : certificate) : ...@@ -258,7 +259,7 @@ def match_imp (A : prop) (c1 : prop -> prop -> certificate) (c2 : certificate) :
(__ => __ => c2) (__ => __ => c2)
(__ => __ => c2). (__ => __ => c2).
def match_all (A : prop) (c1 : A : Type -> (term A -> prop) -> certificate) (c2 : certificate) : certificate := def match_all (A : prop) (c1 : A : type -> (term A -> prop) -> certificate) (c2 : certificate) : certificate :=
match_prop A match_prop A
c2 c2
(__ => __ => c2) (__ => __ => c2)
...@@ -268,7 +269,7 @@ def match_all (A : prop) (c1 : A : Type -> (term A -> prop) -> certificate) (c2 ...@@ -268,7 +269,7 @@ def match_all (A : prop) (c1 : A : Type -> (term A -> prop) -> certificate) (c2
(__ => __ => c2) (__ => __ => c2)
(__ => __ => c2). (__ => __ => c2).
def match_ex (A : prop) (c1 : A : Type -> (term A -> prop) -> certificate) (c2 : certificate) : certificate := def match_ex (A : prop) (c1 : A : type -> (term A -> prop) -> certificate) (c2 : certificate) : certificate :=
match_prop A match_prop A
c2 c2
(__ => __ => c2) (__ => __ => c2)
...@@ -353,12 +354,12 @@ def destruct_imp (A : prop) (B : prop) (c1 : certificate) (c2 : certificate) (c3 ...@@ -353,12 +354,12 @@ def destruct_imp (A : prop) (B : prop) (c1 : certificate) (c2 : certificate) (c3
with_goal (G => refinen (nat.S (nat.S (nat.S nat.O))) (imp A B) A (imp B G) G (ab => a => bg => bg (ab a)) c1 c2 (intro c3)). with_goal (G => refinen (nat.S (nat.S (nat.S nat.O))) (imp A B) A (imp B G) G (ab => a => bg => bg (ab a)) c1 c2 (intro c3)).
(; apply A B a c proves (B a) if c proves all A B ;) (; apply A B a c proves (B a) if c proves all A B ;)
def apply (A : Type) (B : term A -> prop) (a : term A) : certificate -> certificate := def apply (A : type) (B : term A -> prop) (a : term A) : certificate -> certificate :=
refine (all A B) (B a) (ab => ab a). refine (all A B) (B a) (ab => ab a).
(; destruct_all A B a c1 c2 proves G if c1 prove (all A B) and c2 (; destruct_all A B a c1 c2 proves G if c1 prove (all A B) and c2
proves imp (B a) G ;) proves imp (B a) G ;)
def destruct_all (A : Type) (B : term A -> prop) def destruct_all (A : type) (B : term A -> prop)
(a : term A) (c1 : certificate) (a : term A) (c1 : certificate)
(c2 : certificate) : certificate (c2 : certificate) : certificate
:= :=
...@@ -366,7 +367,7 @@ def destruct_all (A : Type) (B : term A -> prop) ...@@ -366,7 +367,7 @@ def destruct_all (A : Type) (B : term A -> prop)
(; To delay the comparison of types, we define ifeq_type only when it is run ;) (; To delay the comparison of types, we define ifeq_type only when it is run ;)
ifeq_type : A : Type -> B : Type -> ((term A -> term B) -> certificate) -> certificate -> certificate. ifeq_type : A : type -> B : type -> ((term A -> term B) -> certificate) -> certificate -> certificate.
[G,B,A,f] run G B (ifeq_type A A f _) --> run G B (f (x => x)) [G,B,A,f] run G B (ifeq_type A A f _) --> run G B (f (x => x))
[G,B,c] run G B (ifeq_type _ _ _ c) --> run G B c. [G,B,c] run G B (ifeq_type _ _ _ c) --> run G B c.
...@@ -377,7 +378,7 @@ ifeq_prop : A : prop -> B : prop -> ((proof A -> proof B) -> certificate) -> cer ...@@ -377,7 +378,7 @@ ifeq_prop : A : prop -> B : prop -> ((proof A -> proof B) -> certificate) -> cer
(; exists A a c proves ex A B if c proves (B a) ;) (; exists A a c proves ex A B if c proves (B a) ;)
witness_of_bad_type : tac.exc. witness_of_bad_type : tac.exc.
not_an_existential : tac.exc. not_an_existential : tac.exc.
def exists (A : Type) (a : term A) (c : certificate) : certificate def exists (A : type) (a : term A) (c : certificate) : certificate
:= :=
with_goal (G => with_goal (G =>
match_ex G match_ex G
...@@ -393,7 +394,7 @@ def exists (A : Type) (a : term A) (c : certificate) : certificate ...@@ -393,7 +394,7 @@ def exists (A : Type) (a : term A) (c : certificate) : certificate
(; destruct_ex A B c1 c2 proves G |- C if c1 proves G |- ex A B and c2 (; destruct_ex A B c1 c2 proves G |- C if c1 proves G |- ex A B and c2
proves G,(a:A),B a |- C ;) proves G,(a:A),B a |- C ;)
def destruct_ex (A : Type) (B : term A -> prop) (c1 : certificate) (c2 def destruct_ex (A : type) (B : term A -> prop) (c1 : certificate) (c2
: certificate) : certificate : certificate) : certificate
:= :=
with_goal (G => with_goal (G =>
......
...@@ -9,13 +9,14 @@ ...@@ -9,13 +9,14 @@
(; Certificates for manipulating equalities ;) (; Certificates for manipulating equalities ;)
def type := fol.type.
def term := fol.term. def term := fol.term.
def prop := fol.prop. def prop := fol.prop.
def proof := fol.proof. def proof := fol.proof.
def certificate := cert.certificate. def certificate := cert.certificate.
not_an_equality : tac.exc. not_an_equality : tac.exc.
def match_equality : prop -> (A : Type -> term A -> term A -> certificate) -> certificate -> certificate. def match_equality : prop -> (A : type -> term A -> term A -> certificate) -> certificate -> certificate.
[c] match_equality fol.false _ c --> c [c] match_equality fol.false _ c --> c
[c] match_equality (fol.and _ _) _ c --> c [c] match_equality (fol.and _ _) _ c --> c
...@@ -33,12 +34,12 @@ def match_equality : prop -> (A : Type -> term A -> term A -> certificate) -> ce ...@@ -33,12 +34,12 @@ def match_equality : prop -> (A : Type -> term A -> term A -> certificate) -> ce
--> c A a b --> c A a b
[c] match_equality (fol.apply_pred _ _) _ c --> c. [c] match_equality (fol.apply_pred _ _) _ c --> c.
not_convertible : A : Type -> term A -> term A -> tac.exc. not_convertible : A : type -> term A -> term A -> tac.exc.
(; reflexivity proves goals of the form a = a ;) (; reflexivity proves goals of the form a = a ;)
def reflexivity : certificate := def reflexivity : certificate :=
cert.with_goal (G => cert.with_goal (G =>
match_equality G (A : Type => a : term A => b : term A => match_equality G (A : type => a : term A => b : term A =>
cert.try (cert.exact (eq.eq A a a) (eq.eq_refl A a)) cert.try (cert.exact (eq.eq A a a) (eq.eq_refl A a))
(__ => cert.raise (not_convertible A a b)) (__ => cert.raise (not_convertible A a b))
) )
...@@ -47,7 +48,7 @@ def reflexivity : certificate := ...@@ -47,7 +48,7 @@ def reflexivity : certificate :=
(; symmetry c proves a = b if c proves b = a ;) (; symmetry c proves a = b if c proves b = a ;)
def symmetry (c : certificate) : certificate := def symmetry (c : certificate) : certificate :=
cert.with_goal (G => cert.with_goal (G =>
match_equality G (A : Type => a : term A => b : term A => match_equality G (A : type => a : term A => b : term A =>
cert.refine (eq.eq A b a) cert.refine (eq.eq A b a)
(eq.eq A a b) (eq.eq A a b)
(eq.eq_symm A a b) (eq.eq_symm A a b)
...@@ -57,9 +58,9 @@ def symmetry (c : certificate) : certificate := ...@@ -57,9 +58,9 @@ def symmetry (c : certificate) : certificate :=
trans_bad_type : tac.exc. trans_bad_type : tac.exc.
(; transitivity A b c1 c2 proves a = c if c1 proves a = b and c2 proves b = c ;) (; transitivity A b c1 c2 proves a = c if c1 proves a = b and c2 proves b = c ;)
def transitivity (A : Type) (b : term A) (c1 : certificate) (c2 : certificate) : certificate := def transitivity (A : type) (b : term A) (c1 : certificate) (c2 : certificate) : certificate :=
cert.with_goal (G => cert.with_goal (G =>
match_equality G (A' : Type => a : term A' => c : term A' => match_equality G (A' : type => a : term A' => c : term A' =>
cert.ifeq_type A A' (f => cert.ifeq_type A A' (f =>
cert.refine2 (eq.eq A' a (f b)) cert.refine2 (eq.eq A' a (f b))
(eq.eq A' (f b) c) (eq.eq A' (f b) c)
...@@ -70,8 +71,124 @@ def transitivity (A : Type) (b : term A) (c1 : certificate) (c2 : certificate) : ...@@ -70,8 +71,124 @@ def transitivity (A : Type) (b : term A) (c1 : certificate) (c2 : certificate) :
(cert.raise trans_bad_type)) (cert.raise trans_bad_type))
(cert.raise not_an_equality)). (cert.raise not_an_equality)).
(; f_equal f c .. cn proves f(a1, .., an) = f(b1, .., bn) if each ci proves ai = bi ;)
def match_f_equal_goal : prop ->
(f : fol.function ->
fol.terms (fol.fun_arity f) ->
fol.terms (fol.fun_arity f) ->
certificate) ->
certificate.
[A,f,as,bs,c] match_f_equal_goal (fol.apply_pred
(eq.Eq A)
(fol.cons_term _ (fol.apply_fun f as)
_ (fol.cons_term _ (fol.apply_fun f bs)
_ fol.nil_term)))
c
--> c f as bs.
certificates : fol.types -> Type.
nil_cert : certificates fol.nil_type.
cons_cert : A : type -> As : fol.types -> certificate -> certificates As -> certificates (fol.cons_type A As).
def ifeq_certs : L : fol.types ->
L' : fol.types ->
certificates L ->
certificates L'.
[L,c] ifeq_certs L L c --> c.
(; f_equal_fun L B f [a1 .. an] [b1 .. bn] [c1 .. cn] proves
f [a1 .. an] = f [b1 .. bn] if each ci proves ai = bi ;)
def f_equal_fun : L : fol.types ->
B : type ->
(fol.terms L -> term B) ->
fol.terms L ->
fol.terms L ->
certificates L -> certificate.
[] f_equal_fun _ _ _ fol.nil_term fol.nil_term nil_cert --> reflexivity
[B,f,A,a,As,as,b,bs,c,cs]
f_equal_fun
(fol.cons_type _ _)
B
f
(fol.cons_term A a As as)
(fol.cons_term _ b _ bs)
(cons_cert _ _ c cs)
-->
cert.refine2
(eq.eq A a b)
(eq.eq B
(f (fol.cons_term A a As as))
(f (fol.cons_term A a As bs)))
(eq.eq B
(f (fol.cons_term A a As as))
(f (fol.cons_term A b As bs)))
(Hab : proof (eq.eq A a b) =>
Hf : proof (eq.eq B
(f (fol.cons_term A a As as))
(f (fol.cons_term A a As bs))) =>
Hab (b => eq.eq B
(f (fol.cons_term A a As as))
(f (fol.cons_term A b As bs)))
Hf)
c
(f_equal_fun As B (l => f (fol.cons_term A a As l)) as bs cs).
def f_equal_fun_on_goal (L : fol.types) (cs : certificates L) : certificate
:=
cert.with_goal (G => match_f_equal_goal G
(f => as => bs =>
f_equal_fun
(fol.fun_arity f)
(fol.fun_codomain f)
(fol.apply_fun f)
as bs (ifeq_certs L (fol.fun_arity f) cs)
)).
def f_equal_T : fol.types -> Type.
[] f_equal_T fol.nil_type --> certificate
[As] f_equal_T (fol.cons_type _ As) --> certificate -> f_equal_T As.
def append_type : fol.types -> fol.types -> fol.types.
[As] append_type As fol.nil_type --> As
[As,B,Bs]
append_type As (fol.cons_type B Bs) -->
append_type (fol.snoc_type As B) Bs.
def snoc_cert : L : fol.types ->
A : type ->
certificates L ->
certificate ->
certificates (fol.snoc_type L A).
[A,c] snoc_cert _ A nil_cert c --> cons_cert A fol.nil_type c nil_cert
[A,B,Bs,c,cs,ca]
snoc_cert (fol.cons_type _ _) A (cons_cert B Bs c cs) ca
-->
cons_cert B (fol.snoc_type Bs A) c (snoc_cert Bs A cs ca).
def f_equal_fun_n : L' : fol.types ->
L : fol.types ->
certificates L ->
f_equal_T L'.
[L,B,f,as,bs,cs]
f_equal_fun_n fol.nil_type L cs
-->
f_equal_fun_on_goal L cs
[A,As,L,B,f,as,bs,cs]
f_equal_fun_n (fol.cons_type A As) L cs
-->
c : certificate =>
f_equal_fun_n As (fol.snoc_type L A) (snoc_cert L A cs c).
def f_equal (f : fol.function) :=
f_equal_fun_n
(fol.fun_arity f)
fol.nil_type
nil_cert.
(; rewrite A a b c1 c2 proves G if c1 proves a = b and c2 proves G{b/a} ;) (; rewrite A a b c1 c2 proves G if c1 proves a = b and c2 proves G{b/a} ;)
def rewrite (A : Type) (a : term A) (b : term A) (c1 : certificate) (c2 : certificate) : certificate def rewrite (A : type) (a : term A) (b : term A) (c1 : certificate) (c2 : certificate) : certificate
:= :=
cert.with_goal (G => cert.with_goal (G =>
cert.refine2 (eq.eq A a b) cert.refine2 (eq.eq A a b)
......
...@@ -12,12 +12,13 @@ def proof := fol.proof. ...@@ -12,12 +12,13 @@ def proof := fol.proof.
def not := fol.not. def not := fol.not.
def or := fol.or. def or := fol.or.
def all := fol.all. def all := fol.all.
def type := fol.type.
def term := fol.term. def term := fol.term.
def certificate := cert.certificate. def certificate := cert.certificate.
(; Specialisation lemma: apply a function f through ;) (; Specialisation lemma: apply a function f through ;)
def specialize (A : Type) def specialize (A : type)
(B : term A -> prop) (B : term A -> prop)
(f : term A -> term A) (f : term A -> term A)
(H : proof (all A B)) : proof (all A (x => B (f x))) (H : proof (all A B)) : proof (all A (x => B (f x)))
...@@ -80,7 +81,7 @@ cons_clause : lit -> clause -> clause. ...@@ -80,7 +81,7 @@ cons_clause : lit -> clause -> clause.
qclause : Type. qclause : Type.
base_qclause : clause -> qclause. base_qclause : clause -> qclause.
qqclause : A : Type -> (term A -> qclause) -> qclause. qqclause : A : type -> (term A -> qclause) -> qclause.
def clause_append : clause -> clause -> clause. def clause_append : clause -> clause -> clause.
[C] clause_append nil_clause C --> C [C] clause_append nil_clause C --> C
......
...@@ -15,6 +15,7 @@ ...@@ -15,6 +15,7 @@
- no deep manipulation of variables and meta variables - no deep manipulation of variables and meta variables
;) ;)
def type := fol.type.
def term := fol.term. def term := fol.term.
def prop := fol.prop. def prop := fol.prop.
def proof := fol.proof. def proof := fol.proof.
...@@ -39,7 +40,7 @@ def try : A : prop -> tactic A -> (exc -> tactic A) -> tactic A. ...@@ -39,7 +40,7 @@ def try : A : prop -> tactic A -> (exc -> tactic A) -> tactic A.
[A,t] try A (ret _ t) _ --> ret A t [A,t] try A (ret _ t) _ --> ret A t
[t,f] try _ (raise _ t) f --> f t. [t,f] try _ (raise _ t) f --> f t.
def fix_term : A : Type -> def fix_term : A : type ->
B : (term A -> prop) -> B : (term A -> prop) ->
((x : term A -> tactic (B x)) -> x : term A -> tactic (B x)) -> ((x : term A -> tactic (B x)) -> x : term A -> tactic (B x)) ->
x : term A -> tactic (B x). x : term A -> tactic (B x).
...@@ -51,7 +52,7 @@ def fix_proof : A : prop -> ...@@ -51,7 +52,7 @@ def fix_proof : A : prop ->
proof A -> tactic B. proof A -> tactic B.
[A,B,f,t] fix_proof A B f t --> f (fix_proof A B f) t. [A,B,f,t] fix_proof A B f t --> f (fix_proof A B f) t.
def intro_term : A : Type -> def intro_term : A : type ->
B : (term A -> prop) -> B : (term A -> prop) ->
(x : term A -> tactic (B x)) -> (x : term A -> tactic (B x)) ->
tactic (all A B). tactic (all A B).
......
...@@ -7,6 +7,7 @@ ...@@ -7,6 +7,7 @@
(setq-local dedukti-compile-options '("-nc" "-e" "-nl" "-I" "../fol")) (setq-local dedukti-compile-options '("-nc" "-e" "-nl" "-I" "../fol"))
;) ;)
def type := fol.type.
def term := fol.term. def term := fol.term.
def prop := fol.prop. def prop := fol.prop.
def types := fol.types. def types := fol.types.
...@@ -32,14 +33,14 @@ def read_types := fol.read_types. ...@@ -32,14 +33,14 @@ def read_types := fol.read_types.
substitution : Type. substitution : Type.
empty_subst : substitution. empty_subst : substitution.
cons_subst : A : Type -> cons_subst : A : type ->
term A ->