Commit 1dad75e6 authored by Raphael Cauderlier's avatar Raphael Cauderlier

Replace type by Type.

The main motivation is to ease integration into higher-order logic
which would orhterwise require fol.term to be a definable
symbol (which poses injectivity problems).

This change requires -coc, and the latest (v2.5.1) versions of Dedukti
and Meta Dedukti (because -coc was not present before in Meta
Dedukti). fol.term is now defined as the identity over types so it is
not mandatory to remove it from the developments but fol.type needs to
be replaced by Type since Dedukti does not allow kind-level
definitions.

A new bug has been discovered (#21276). It has been triggered by the
eqcert.match_f_equal_goal function and has required to remove the
eqcert.f_equal certificate transformer.
parent 8ede9890
......@@ -63,8 +63,8 @@ echo > .config_vars &&
# Mandatory
find_and_check_binary "dkdep" ".native" "DKDEP" "-version" "" &&
find_and_check_binary "dkcheck" ".native" "DKCHECK" "-version" "Dedukti v2.5" &&
find_and_check_binary "dkmeta" ".native" "DKMETA" "-version" "Dedukti v2.5" &&
find_and_check_binary "dkcheck" ".native" "DKCHECK" "-version" "Dedukti v2.5.1" &&
find_and_check_binary "dkmeta" ".native" "DKMETA" "-version" "Meta Dedukti v2.5.1" &&
find_and_check_binary "skcheck" ".native" "SKCHECK" "-version" "Sukerujo v2.5" &&
find_and_check_binary "skmeta" ".native" "SKMETA" "-version" "Sukerujo v2.5" &&
......
......@@ -9,7 +9,7 @@ endif
# Dedukti files
DKS = $(wildcard *.dk)
DKOS = $(DKS:.dk=.dko)
DKCHECK_OPTIONS =
DKCHECK_OPTIONS = -coc
all: $(DKOS)
......
#NAME eq.
def type := fol.type.
def types := fol.types.
def term := fol.term.
def terms := fol.terms.
......@@ -27,10 +26,10 @@ def O := nat.O.
def S := nat.S.
(; 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.
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))) -->
......@@ -38,14 +37,14 @@ def eq (A : type) : term A -> term A -> prop := pred_apply (Eq A).
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 =>
c : (term A -> prop) =>
H : proof (c x) =>
H.
thm eq_symm (A : type) :
thm eq_symm (A : Type) :
proof (all A (x : term A =>
all A (y : term A =>
imp (eq A y x) (eq A x y))))
......@@ -55,7 +54,7 @@ thm eq_symm (A : type) :
H : proof (eq A y x) =>
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 =>
all A (y : term A =>
all A (z : term A =>
......@@ -70,7 +69,7 @@ thm eq_trans (A : type) :
H2 : proof (eq A y z) =>
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 =>
all A (y : term A =>
imp (eq A x y) (imp (p x) (p y)))))
......@@ -80,7 +79,7 @@ thm eq_p_equal (A : type) (p : term A -> prop) :
H : proof (eq A x y) =>
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 =>
all A (y : term A =>
imp (eq A x y) (eq B (f x) (f y)))))
......@@ -111,14 +110,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))
:= 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)
[A,L,B,f,f'] fun_eq (fol.cons_type A L) B f f' -->
all A (x : 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))))).
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)
[A,L,B,f,f'] eq_fun_eq (fol.cons_type A L) B f -->
x : term A =>
......
#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 ;)
(; Type system ;)
type : Type.
term : type -> Type.
def term (A : Type) := A.
(; Arities of function and predicate symbols are list of types ;)
types : Type.
nil_type : types.
cons_type : type -> types -> types.
cons_type : Type -> types -> types.
(; To ease the definition of new symbols, we provide an nary
constructor read_types of list of types:
......@@ -22,11 +27,11 @@ def nat := nat.Nat.
(; The type of the read_types function is defined inductively ;)
def read_types_T : nat -> Type.
[] 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:
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
[L,A,B] snoc_type (cons_type A L) B --> cons_type A (snoc_type L B).
......@@ -37,7 +42,7 @@ def read_types_acc : n : nat -> types -> read_types_T n.
[acc] read_types_acc nat.O acc --> acc
[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] ;)
def read_types (n : nat) : read_types_T n
......@@ -49,12 +54,12 @@ def read_types (n : nat) : read_types_T n
and fun_codomain should be extended ;)
function : Type.
def fun_arity : function -> types.
def fun_codomain : function -> type.
def fun_codomain : function -> Type.
(; Function application is unnary ;)
terms : types -> Type.
nil_term : terms nil_type.
cons_term : A : type -> term A ->
cons_term : A : Type -> term A ->
tail_types : types ->
terms tail_types ->
terms (cons_type A tail_types).
......@@ -66,12 +71,12 @@ def apply_fun : f : function ->
applications, we derive an nary application fun_apply ;)
(; 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
[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] ;)
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.
[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)).
......@@ -85,8 +90,8 @@ false : prop.
and : prop -> prop -> prop.
or : prop -> prop -> prop.
imp : prop -> prop -> prop.
all : A : type -> (term A -> prop) -> prop.
ex : A : type -> (term A -> prop) -> prop.
all : A : Type -> (term A -> prop) -> prop.
ex : A : Type -> (term A -> prop) -> prop.
(; Derived connectives ;)
def not (p : prop) := imp p false.
......@@ -186,17 +191,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 :=
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)
:=
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)
:=
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 =>
......@@ -205,7 +210,7 @@ thm ex_intro (A : type) (p : term A -> prop) :
Hc : (x : term A -> proof (p x) -> proof c) =>
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) ->
(a : term A -> proof (p a) -> proof c) ->
proof c
......
......@@ -5,7 +5,7 @@ https://en.wikipedia.org/wiki/Presburger_arithmetic ;)
(; There is just one sort representing natural numbers ;)
Nat : fol.type.
Nat : Type.
(; There is just one predicate symbol for equality ;)
EQ : fol.predicate.
......
......@@ -3,7 +3,7 @@ include ../.config_vars
# Dedukti files
DKS = $(wildcard *.dk)
DKOS = $(DKS:.dk=.dko)
DKCHECK_OPTIONS = -I ../fol -nl
DKCHECK_OPTIONS = -I ../fol -nl -coc
all: $(DKOS)
......
......@@ -8,7 +8,6 @@
;)
def type := fol.type.
def term := fol.term.
def prop := fol.prop.
def proof := fol.proof.
......@@ -17,7 +16,7 @@ def imp := fol.imp.
context : Type.
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.
certificate : Type.
......@@ -80,7 +79,7 @@ clear : prop -> certificate -> certificate.
[A,G,B,c] run A G (clear B c) --> run A (ctx_remove B G) c.
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
[f,A,a,G]
try_all_variables f (cons_ctx_var A a G)
......@@ -93,7 +92,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
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).
......@@ -158,7 +157,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.
(; 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.
def fix_prop : ((prop -> certificate) -> prop -> certificate) -> prop -> certificate.
......@@ -204,8 +203,8 @@ def match_prop : prop ->
(prop -> prop -> certificate) -> (; and ;)
(prop -> prop -> certificate) -> (; or ;)
(prop -> prop -> certificate) -> (; imp ;)
(A : type -> (term A -> prop) -> certificate) -> (; all ;)
(A : type -> (term A -> prop) -> certificate) -> (; ex ;)
(A : Type -> (term A -> prop) -> certificate) -> (; all ;)
(A : Type -> (term A -> prop) -> certificate) -> (; ex ;)
(p : fol.predicate ->
fol.terms (fol.pred_arity p) ->
certificate) ->
......@@ -259,7 +258,7 @@ def match_imp (A : prop) (c1 : prop -> prop -> certificate) (c2 : certificate) :
(__ => __ => 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
c2
(__ => __ => c2)
......@@ -269,7 +268,7 @@ def match_all (A : prop) (c1 : A : type -> (term A -> prop) -> certificate) (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
c2
(__ => __ => c2)
......@@ -354,12 +353,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)).
(; 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).
(; destruct_all A B a c1 c2 proves G if c1 prove (all A B) and c2
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)
(c2 : certificate) : certificate
:=
......@@ -367,7 +366,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 ;)
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,c] run G B (ifeq_type _ _ _ c) --> run G B c.
......@@ -378,7 +377,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) ;)
witness_of_bad_type : 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 =>
match_ex G
......@@ -394,7 +393,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
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
:=
with_goal (G =>
......
......@@ -9,14 +9,13 @@
(; Certificates for manipulating equalities ;)
def type := fol.type.
def term := fol.term.
def prop := fol.prop.
def proof := fol.proof.
def certificate := cert.certificate.
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.and _ _) _ c --> c
......@@ -34,12 +33,12 @@ def match_equality : prop -> (A : type -> term A -> term A -> certificate) -> ce
--> c A a b
[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 ;)
def reflexivity : certificate :=
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.raise (not_convertible A a b))
)
......@@ -48,7 +47,7 @@ def reflexivity : certificate :=
(; symmetry c proves a = b if c proves b = a ;)
def symmetry (c : certificate) : certificate :=
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)
(eq.eq A a b)
(eq.eq_symm A a b)
......@@ -58,9 +57,9 @@ def symmetry (c : certificate) : certificate :=
trans_bad_type : tac.exc.
(; 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 =>
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.refine2 (eq.eq A' a (f b))
(eq.eq A' (f b) c)
......@@ -71,124 +70,8 @@ def transitivity (A : type) (b : term A) (c1 : certificate) (c2 : certificate) :
(cert.raise trans_bad_type))
(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} ;)
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.refine2 (eq.eq A a b)
......
......@@ -12,13 +12,12 @@ def proof := fol.proof.
def not := fol.not.
def or := fol.or.
def all := fol.all.
def type := fol.type.
def term := fol.term.
def certificate := cert.certificate.
(; Specialisation lemma: apply a function f through ;)
def specialize (A : type)
def specialize (A : Type)
(B : term A -> prop)
(f : term A -> term A)
(H : proof (all A B)) : proof (all A (x => B (f x)))
......@@ -81,7 +80,7 @@ cons_clause : lit -> clause -> clause.
qclause : Type.
base_qclause : clause -> qclause.
qqclause : A : type -> (term A -> qclause) -> qclause.
qqclause : A : Type -> (term A -> qclause) -> qclause.
def clause_append : clause -> clause -> clause.
[C] clause_append nil_clause C --> C
......
......@@ -15,7 +15,6 @@
- no deep manipulation of variables and meta variables
;)
def type := fol.type.
def term := fol.term.
def prop := fol.prop.
def proof := fol.proof.
......@@ -40,7 +39,7 @@ def try : A : prop -> tactic A -> (exc -> tactic A) -> tactic A.
[A,t] try A (ret _ t) _ --> ret A t
[t,f] try _ (raise _ t) f --> f t.
def fix_term : A : type ->
def fix_term : A : Type ->
B : (term A -> prop) ->
((x : term A -> tactic (B x)) -> x : term A -> tactic (B x)) ->
x : term A -> tactic (B x).
......@@ -52,7 +51,7 @@ def fix_proof : A : prop ->
proof A -> tactic B.
[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) ->
(x : term A -> tactic (B x)) ->
tactic (all A B).
......
......@@ -7,7 +7,6 @@
(setq-local dedukti-compile-options '("-nc" "-e" "-nl" "-I" "../fol"))
;)
def type := fol.type.
def term := fol.term.
def prop := fol.prop.
def types := fol.types.
......@@ -33,14 +32,14 @@ def read_types := fol.read_types.
substitution : Type.
empty_subst : substitution.
cons_subst : A : type ->
cons_subst : A : Type ->
term A ->
term A ->
substitution ->
substitution.
def subst_prop : substitution -> prop -> prop.
def subst_term : substitution -> B : type -> term B -> term B.
def subst_term : substitution -> B : Type -> term B -> term B.
def subst_terms : substitution -> Bs : types -> terms Bs -> terms Bs.
[] subst_prop _ fol.false --> false
......@@ -82,13 +81,13 @@ unify_success : substitution -> unify_result.
unify_failure : unify_result.
(; This is technically the same type as substitution
list (Σ A : type. term A * term A)
list (Σ A : Type. term A * term A)
We keep them separate because they serve different purposes.
;)
unify_problem : Type.
unify_nil : unify_problem.
unify_cons : A : type -> term A -> term A -> unify_problem -> unify_problem.
unify_cons : A : Type -> term A -> term A -> unify_problem -> unify_problem.
def unify_cons_terms : As : types -> terms As -> terms As -> unify_problem -> unify_problem.
[pb] unify_cons_terms fol.nil_type fol.nil_term fol.nil_term pb --> pb
......@@ -110,8 +109,8 @@ def bor : bool -> bool -> bool.
[] bor bfalse btrue --> btrue
[] bor bfalse bfalse --> bfalse.
def occur : A : type -> term A -> B : type -> term B -> bool.
def occur_terms : A : type -> term A -> Bs : types -> terms Bs -> bool.
def occur : A : Type -> term A -> B : Type -> term B -> bool.
def occur_terms : A : Type -> term A -> Bs : types -> terms Bs -> bool.
[x] occur _ x _ x --> btrue
[A,x,f,l] occur A x _ (fol.apply_fun f l) --> occur_terms A x (fun_arity f) l
[] occur _ _ _ _ --> bfalse.
......@@ -121,8 +120,8 @@ def occur_terms : A : type -> term A -> Bs : types -> terms Bs -> bool.
bor (occur A x B b) (occur_terms A x Bs bs).
def unify : unify_problem -> unify_result.
def unify_occur : unify_problem -> A : type -> term A -> term A -> bool -> unify_result -> unify_result.
def subst_in_unify_problem : A : type -> term A -> term A -> unify_problem -> unify_problem.
def unify_occur : unify_problem -> A : Type -> term A -> term A -> bool -> unify_result -> unify_result.
def subst_in_unify_problem : A : Type -> term A -> term A -> unify_problem -> unify_problem.
[] unify unify_nil --> unify_success empty_subst
[f,l,l',pb] unify (unify_cons _ (fol.apply_fun f l) (fol.apply_fun f l') pb) -->
unify (unify_cons_terms (fun_arity f) l l' pb)
......@@ -143,7 +142,7 @@ def subst_in_unify_problem : A : type -> term A -> term A -> unify_problem -> un
(subst_in_unify_problem A x a pb).
A : type.
A : Type.
f : function.
[] fol.fun_arity f --> read_types (nat.S (nat.S nat.O)) A A.
[] fol.fun_codomain f --> A.
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment