Commit 8b720c66 authored by Raphael Cauderlier's avatar Raphael Cauderlier

type -> sort

parent 0d0c865f
#NAME NUM343_1.
def type := fol.type.
def sort := fol.sort.
def term := fol.term.
def prop := fol.prop.
def proof := fol.proof.
......@@ -15,19 +15,19 @@ def predicate := fol.predicate.
def function := fol.function.
def pred_apply := fol.pred_apply.
def fun_apply := fol.fun_apply.
def read_types := fol.read_types.
def nil_type := fol.nil_type.
def read_sorts := fol.read_sorts.
def nil_sort := fol.nil_sort.
def 0 := nat.O.
def 1 := nat.S 0.
def 2 := nat.S 1.
(; Signature ;)
A : type.
A : sort.
LEQ : predicate.
[] fol.pred_arity LEQ --> read_types 2 A A.
[] fol.pred_arity LEQ --> read_sorts 2 A A.
N : function.
[] fol.fun_arity N --> nil_type.
[] fol.fun_arity N --> nil_sort.
[] fol.fun_codomain N --> A.
def leq : term A -> term A -> prop := pred_apply LEQ.
......
......@@ -7,18 +7,18 @@
(setq-local dedukti-compile-options '("-nc" "-e" "-nl" "-I" "../fol" "-I" "../meta"))
;)
BAR : fol.type.
BAR : fol.sort.
(; We have to assume that the bar is not empty, that is we have a term
of type BAR. Let's call it Joe. ;)
of sort BAR. Let's call it Joe. ;)
JOE : fol.function.
[] fol.fun_arity JOE --> fol.nil_type.
[] fol.fun_arity JOE --> fol.nil_sort.
[] fol.fun_codomain JOE --> BAR.
def Joe : fol.term BAR := fol.fun_apply JOE.
(; The "drink" predicate. ;)
DRINK : fol.predicate.
[] fol.pred_arity DRINK --> fol.read_types (nat.S nat.O) BAR.
[] fol.pred_arity DRINK --> fol.read_sorts (nat.S nat.O) BAR.
def drink (x : fol.term BAR) : fol.prop := fol.pred_apply DRINK x.
def drinker_statement : fol.prop :=
......@@ -50,7 +50,7 @@ def drinker_paradox : fol.proof drinker_statement :=
(cert.with_assumption (E => e =>
cert.destruct_ex BAR ndrink (cert.exact E e)
(; ¬∀, ∃¬, John, ¬drink John ⊢ ∃x. drink x → ∀ ;)
(cert.with_variable (B : fol.type => John : fol.term B =>
(cert.with_variable (B : fol.sort => John : fol.term B =>
cert.exists B John
(; ¬∀, ∃¬, John, ¬drink John ⊢ drink John → ∀ ;)
(cert.intro cert.absurd)))))))).
#NAME resolution_examples.
def type := fol.type.
def sort := fol.sort.
def term := fol.term.
def prop := fol.prop.
def proof := fol.proof.
......@@ -15,21 +15,21 @@ def predicate := fol.predicate.
def function := fol.function.
def pred_apply := fol.pred_apply.
def fun_apply := fol.fun_apply.
def read_types := fol.read_types.
def nil_type := fol.nil_type.
def read_sorts := fol.read_sorts.
def nil_sort := fol.nil_sort.
def 0 := nat.O.
def 1 := nat.S 0.
(; Signature ;)
A : type.
A : sort.
P : predicate.
[] fol.pred_arity P --> read_types 1 A.
[] fol.pred_arity P --> read_sorts 1 A.
O : function.
[] fol.fun_arity O --> nil_type.
[] fol.fun_arity O --> nil_sort.
[] fol.fun_codomain O --> A.
S : function.
[] fol.fun_arity S --> read_types 1 A.
[] fol.fun_arity S --> read_sorts 1 A.
[] fol.fun_codomain S --> A.
def p : term A -> prop := pred_apply P.
......
......@@ -13,4 +13,4 @@ cons_clause : litteral -> clause -> clause.
qclause : Type.
qc_base : clause -> qclause.
qc_all : A : fol.type -> (fol.term A -> qclause) -> qclause.
qc_all : A : fol.sort -> (fol.term A -> qclause) -> qclause.
#NAME eq.
def type := fol.type.
def types := fol.types.
def sort := fol.sort.
def sorts := fol.sorts.
def term := fol.term.
def terms := fol.terms.
def nil_term := fol.nil_term.
def cons_term := fol.cons_term.
def read_types := fol.read_types.
def read_sorts := fol.read_sorts.
def prop := fol.prop.
def imp := fol.imp.
......@@ -27,21 +27,21 @@ def O := nat.O.
def S := nat.S.
(; Equality is a family of binary predicate symbols. ;)
Eq : type -> predicate.
[A] fol.pred_arity (Eq A) --> read_types (S (S O)) A A.
Eq : sort -> predicate.
[A] fol.pred_arity (Eq A) --> read_sorts (S (S O)) A A.
def eq (A : type) : term A -> term A -> prop := pred_apply (Eq A).
def eq (A : sort) : 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))) -->
p : (term A -> prop) -> proof (p x) -> proof (p y).
def eq_refl (A : type) : proof (all A (x => eq A x x)) :=
def eq_refl (A : sort) : proof (all A (x => eq A x x)) :=
fol.all_intro A (x => eq A x x) (x => p => H => H).
def eq_congr (A : type) (x : term A) (y : term A) (H : proof (eq A x y)) : c : (term A -> prop) -> proof (c x) -> proof (c y) := H.
def eq_congr (A : sort) (x : term A) (y : term A) (H : proof (eq A x y)) : c : (term A -> prop) -> proof (c x) -> proof (c y) := H.
def eq_symm (A : type) :
def eq_symm (A : sort) :
proof (all A (x : term A =>
all A (y : term A =>
imp (eq A y x) (eq A x y)))) :=
......@@ -50,7 +50,7 @@ def eq_symm (A : type) :
(y => fol.imp_intro (eq A y x) (eq A x y)
(Hyx => eq_congr A y x Hyx (z => eq A z y) (fol.all_elim A (x => eq A x x) (eq_refl A) y)))).
def eq_trans (A : type) :
def eq_trans (A : sort) :
proof (all A (x : term A =>
all A (y : term A =>
all A (z : term A =>
......@@ -64,7 +64,7 @@ def eq_trans (A : type) :
(Hxy => fol.imp_intro (eq A y z) (eq A x z)
(Hyz => eq_congr A y z Hyz (t => eq A x t) Hxy))))).
def eq_p_equal (A : type) (p : term A -> prop) :
def eq_p_equal (A : sort) (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))))) :=
......@@ -74,21 +74,21 @@ def eq_p_equal (A : type) (p : term A -> prop) :
(Hxy => fol.imp_intro (p x) (p y)
(Hpx => eq_congr A x y Hxy p Hpx)))).
eq_f_equal : A : type -> B : type -> f : (term A -> term B) ->
eq_f_equal : A : sort -> B : sort -> 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))))).
def pred_imp : L : types -> (terms L -> prop) -> (terms L -> prop) -> prop.
[p,q] pred_imp fol.nil_type p q --> imp (p nil_term) (q nil_term)
[A,L,p,q] pred_imp (fol.cons_type A L) p q -->
def pred_imp : L : sorts -> (terms L -> prop) -> (terms L -> prop) -> prop.
[p,q] pred_imp fol.nil_sort p q --> imp (p nil_term) (q nil_term)
[A,L,p,q] pred_imp (fol.cons_sort A L) p q -->
all A (x : term A =>
all A (y : term A =>
imp (eq A x y) (pred_imp L (l : terms L => p (cons_term A x L l)) (l : terms L => q (cons_term A y L l))))).
def eq_pred_imp : L : types -> p : (terms L -> prop) -> proof (pred_imp L p p).
[p] eq_pred_imp fol.nil_type p --> fol.imp_intro (p nil_term) (p nil_term) (Hp => Hp)
[A,L,p] eq_pred_imp (fol.cons_type A L) p -->
def eq_pred_imp : L : sorts -> p : (terms L -> prop) -> proof (pred_imp L p p).
[p] eq_pred_imp fol.nil_sort p --> fol.imp_intro (p nil_term) (p nil_term) (Hp => Hp)
[A,L,p] eq_pred_imp (fol.cons_sort A L) p -->
fol.all_intro A (x => all A (y => imp (eq A x y) (pred_imp L (l => p (cons_term A x L l)) (l => p (cons_term A y L l)))))
(x =>
fol.all_intro A (y => imp (eq A x y) (pred_imp L (l => p (cons_term A x L l)) (l => p (cons_term A y L l))))
......@@ -100,16 +100,16 @@ 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.
[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' -->
def fun_eq : L : sorts -> B : sort -> (terms L -> term B) -> (terms L -> term B) -> prop.
[B,b,b'] fun_eq fol.nil_sort B b b' --> eq B (b nil_term) (b' nil_term)
[A,L,B,f,f'] fun_eq (fol.cons_sort 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).
[B,b] eq_fun_eq fol.nil_type B b --> fol.all_elim B (x => eq B x x) (eq_refl B) (b nil_term)
[A,L,B,f,f'] eq_fun_eq (fol.cons_type A L) B f -->
def eq_fun_eq : L : sorts -> B : sort -> f : (terms L -> term B) -> proof (fun_eq L B f f).
[B,b] eq_fun_eq fol.nil_sort B b --> fol.all_elim B (x => eq B x x) (eq_refl B) (b nil_term)
[A,L,B,f,f'] eq_fun_eq (fol.cons_sort A L) B f -->
fol.all_intro A (x => all A (y => 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)))))
(x =>
fol.all_intro A (y => 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))))
......
......@@ -3,61 +3,61 @@
(; Polymorphic first-order logic ;)
(; Type system ;)
type : Type.
term : type -> Type.
sort : Type.
term : sort -> Type.
(; Arities of function and predicate symbols are list of types ;)
types : Type.
nil_type : types.
cons_type : type -> types -> types.
(; Arities of function and predicate symbols are list of sorts ;)
sorts : Type.
nil_sort : sorts.
cons_sort : sort -> sorts -> sorts.
(; To ease the definition of new symbols, we provide an nary
constructor read_types of list of types:
read_types n A1 A2 ... An =
cons_type A1 (cons_type A2 (... cons_type An nil_type))
constructor read_sorts of list of sorts:
read_sorts n A1 A2 ... An =
cons_sort A1 (cons_sort A2 (... cons_sort An nil_sort))
;)
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.
(; The type of the read_sorts function is defined inductively ;)
def read_sorts_T : nat -> Type.
[] read_sorts_T nat.O --> sorts.
[n] read_sorts_T (nat.S n) --> sort -> read_sorts_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.
[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).
(; Adding an element to the tail of a list of sorts:
snoc_sort [A1 .. An] B = [A1 .. An B] ;)
def snoc_sort : sorts -> sort -> sorts.
[A] snoc_sort nil_sort A --> cons_sort A nil_sort
[L,A,B] snoc_sort (cons_sort A L) B --> cons_sort A (snoc_sort L B).
(; Auxiliary function:
read_tyes_acc m [A1 .. An] B1 .. Bm = [A1 .. An B1 .. Bm]
;)
def read_types_acc : n : nat -> types -> read_types_T n.
[acc] read_types_acc nat.O acc --> acc
def read_sorts_acc : n : nat -> sorts -> read_sorts_T n.
[acc] read_sorts_acc nat.O acc --> acc
[n,acc]
read_types_acc (nat.S n) acc
--> t : type => read_types_acc n (snoc_type acc t).
read_sorts_acc (nat.S n) acc
--> t : sort => read_sorts_acc n (snoc_sort acc t).
(; read_types n A1 .. An = [A1 .. An] ;)
def read_types (n : nat) : read_types_T n
:= read_types_acc n nil_type.
(; read_sorts n A1 .. An = [A1 .. An] ;)
def read_sorts (n : nat) : read_sorts_T n
:= read_sorts_acc n nil_sort.
(; Terms are trees built from function symbols ;)
(; function is the type of function symbols, ;)
(; function is the sort of function symbols, ;)
(; each time a function symbol is declared, the functions fun_arity
and fun_codomain should be extended ;)
function : Type.
def fun_arity : function -> types.
def fun_codomain : function -> type.
def fun_arity : function -> sorts.
def fun_codomain : function -> sort.
(; Function application is unnary ;)
terms : types -> Type.
nil_term : terms nil_type.
cons_term : A : type -> term A ->
tail_types : types ->
terms : sorts -> Type.
nil_term : terms nil_sort.
cons_term : A : sort -> term A ->
tail_types : sorts ->
terms tail_types ->
terms (cons_type A tail_types).
terms (cons_sort A tail_types).
apply_fun : f : function ->
terms (fun_arity f) ->
term (fun_codomain f).
......@@ -66,24 +66,24 @@ 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.
[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.
def read_f_T : sorts -> sort -> Type.
[C] read_f_T nil_sort C --> term C
[A,As,C] read_f_T (cons_sort 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.
[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)).
def read_f : As : sorts -> C : sort -> (terms As -> term C) -> read_f_T As C.
[C,f] read_f nil_sort C f --> f nil_term.
[A,As,C,f] read_f (cons_sort A As) C f --> a : term A => read_f As C (as : terms As => f (cons_term A a As as)).
def fun_apply (f : function) := read_f (fun_arity f) (fun_codomain f) (apply_fun f).
def fun_arrs := read_f_T.
def fun_uncurry : As : types -> A : type -> fun_arrs As A -> terms As -> term A.
[A,f] fun_uncurry nil_type A f nil_term --> f
[A,As,B,f,a,as] fun_uncurry (cons_type A As) B f (cons_term _ a _ as) --> fun_uncurry As B (f a) as.
def fun_uncurry : As : sorts -> A : sort -> fun_arrs As A -> terms As -> term A.
[A,f] fun_uncurry nil_sort A f nil_term --> f
[A,As,B,f,a,as] fun_uncurry (cons_sort A As) B f (cons_term _ a _ as) --> fun_uncurry As B (f a) as.
def make_fun : As : types -> A : type -> (fun_arrs As A) -> function.
def make_fun : As : sorts -> A : sort -> (fun_arrs As A) -> function.
[As] fun_arity (make_fun As _ _) --> As.
[A] fun_codomain (make_fun _ A _) --> A.
(; [As, A, f, as] apply_fun (make_fun As A f) as --> fun_uncurry As A f as. ;)
......@@ -104,8 +104,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 : sort -> (term A -> prop) -> prop.
ex : A : sort -> (term A -> prop) -> prop.
(; Derived connectives ;)
def not (p : prop) := imp p false.
......@@ -160,38 +160,38 @@ def nimp : n : nat -> nand_type (nat.S n) := nimp_aux nil_prop.
all A₁ (a₁ : term A₁ => all A₂ (a₂ : term A₂ => … all Aₙ (aₙ : term Aₙ => P a₁ a₂ … aₙ)…)) ;)
(; nall_aux [A₁; …; Aₙ] : (term A₁ -> … -> term Aₙ -> prop) -> prop ;)
def nall_aux_type : types -> Type.
[] nall_aux_type nil_type --> prop.
[A,As] nall_aux_type (cons_type A As) --> term A -> nall_aux_type As.
def nall_aux_type : sorts -> Type.
[] nall_aux_type nil_sort --> prop.
[A,As] nall_aux_type (cons_sort A As) --> term A -> nall_aux_type As.
def nall_aux : As : types -> nall_aux_type As -> prop.
[P] nall_aux nil_type --> P => P.
[A,As,P] nall_aux (cons_type A As) --> P => all A (a => nall_aux As (P a)).
def nall_aux : As : sorts -> nall_aux_type As -> prop.
[P] nall_aux nil_sort --> P => P.
[A,As,P] nall_aux (cons_sort A As) --> P => all A (a => nall_aux As (P a)).
def nex_aux : As : types -> nall_aux_type As -> prop.
[P] nex_aux nil_type --> P => P.
[A,As,P] nex_aux (cons_type A As) --> P => ex A (a => nex_aux As (P a)).
def nex_aux : As : sorts -> nall_aux_type As -> prop.
[P] nex_aux nil_sort --> P => P.
[A,As,P] nex_aux (cons_sort A As) --> P => ex A (a => nex_aux As (P a)).
(; nall_aux2 [B₁; …; Bₘ] n A₁ … Aₙ = nall_aux [B₁; …; Bₘ; A₁; …; Aₙ] ;)
(; nall_aux2_type Bs n A₁ … Aₙ = nall_aux_type (Bs^As) -> prop ;)
def nall_aux2_type : types -> nat -> Type.
def nall_aux2_type : sorts -> nat -> Type.
[Bs] nall_aux2_type Bs nat.O --> nall_aux_type Bs -> prop
[Bs,n] nall_aux2_type Bs (nat.S n) --> A : type -> nall_aux2_type (snoc_type Bs A) n.
[Bs,n] nall_aux2_type Bs (nat.S n) --> A : sort -> nall_aux2_type (snoc_sort Bs A) n.
def nall_aux2 : Bs : types -> n : nat -> nall_aux2_type Bs n.
def nall_aux2 : Bs : sorts -> n : nat -> nall_aux2_type Bs n.
[Bs] nall_aux2 Bs nat.O --> nall_aux Bs
[Bs,n] nall_aux2 Bs (nat.S n) --> A => nall_aux2 (snoc_type Bs A) n.
[Bs,n] nall_aux2 Bs (nat.S n) --> A => nall_aux2 (snoc_sort Bs A) n.
def nex_aux2 : Bs : types -> n : nat -> nall_aux2_type Bs n.
def nex_aux2 : Bs : sorts -> n : nat -> nall_aux2_type Bs n.
[Bs] nex_aux2 Bs nat.O --> nex_aux Bs
[Bs,n] nex_aux2 Bs (nat.S n) --> A => nex_aux2 (snoc_type Bs A) n.
[Bs,n] nex_aux2 Bs (nat.S n) --> A => nex_aux2 (snoc_sort Bs A) n.
def nall (n : nat) : nall_aux2_type nil_type n := nall_aux2 nil_type n.
def nex (n : nat) : nall_aux2_type nil_type n := nex_aux2 nil_type n.
def nall (n : nat) : nall_aux2_type nil_sort n := nall_aux2 nil_sort n.
def nex (n : nat) : nall_aux2_type nil_sort n := nex_aux2 nil_sort n.
(; Predicate application is also nary ;)
predicate : Type.
def pred_arity : predicate -> types.
def pred_arity : predicate -> sorts.
apply_pred : p : predicate ->
terms (pred_arity p) ->
prop.
......@@ -200,25 +200,25 @@ apply_pred : p : predicate ->
applications, we derive an nary application pred_apply ;)
(; read_p_T [A1 .. An] --> A1 -> .. -> prop ;)
def read_p_T : types -> Type.
[] read_p_T nil_type --> prop
[A,As] read_p_T (cons_type A As) --> term A -> read_p_T As.
def read_p_T : sorts -> Type.
[] read_p_T nil_sort --> prop
[A,As] read_p_T (cons_sort A As) --> term A -> read_p_T As.
(; read_p [A1 .. An] p a1 .. an --> p [a1 .. an] ;)
def read_p : As : types -> (terms As -> prop) -> read_p_T As.
[p] read_p nil_type p --> p nil_term.
[A,As,p] read_p (cons_type A As) p -->
def read_p : As : sorts -> (terms As -> prop) -> read_p_T As.
[p] read_p nil_sort p --> p nil_term.
[A,As,p] read_p (cons_sort A As) p -->
a : term A => read_p As (as : terms As => p (cons_term A a As as)).
def pred_apply (p : predicate) := read_p (pred_arity p) (apply_pred p).
def pred_arrs := read_p_T.
def pred_uncurry : As : types -> pred_arrs As -> terms As -> prop.
[p] pred_uncurry nil_type p nil_term --> p
[A,As,p,a,as] pred_uncurry (cons_type A As) p (cons_term _ a _ as) --> pred_uncurry As (p a) as.
def pred_uncurry : As : sorts -> pred_arrs As -> terms As -> prop.
[p] pred_uncurry nil_sort p nil_term --> p
[A,As,p,a,as] pred_uncurry (cons_sort A As) p (cons_term _ a _ as) --> pred_uncurry As (p a) as.
def make_pred : As : types -> (pred_arrs As) -> predicate.
def make_pred : As : sorts -> (pred_arrs As) -> predicate.
[As] pred_arity (make_pred As _) --> As.
(; [As, p, as] apply_pred (make_pred As p) as --> pred_uncurry As p as. ;)
......@@ -261,15 +261,15 @@ def or_elim (a : prop) (b : prop) (c : prop) (H : proof (or a b)) (fa : proof a
def imp_intro (a : prop) (b : prop) (f : proof a -> proof b) : proof (imp a b) := f.
def imp_elim (a : prop) (b : prop) (H : proof (imp a b)) : proof a -> proof b := H.
def all_intro (A : type) (p : term A -> prop)
def all_intro (A : sort) (p : term A -> prop)
(f : a : term A -> proof (p a)) : proof (all A p) := f.
def all_elim (A : type) (p : term A -> prop)
def all_elim (A : sort) (p : term A -> prop)
(H : proof (all A p)) : a : term A -> proof (p a) := H.
def ex_intro (A : type) (p : term A -> prop) (a : term A)
def ex_intro (A : sort) (p : term A -> prop) (a : term A)
(Ha : proof (p a)) : proof (ex A p) :=
c : prop => f : (a : term A -> proof (p a) -> proof c) => f a Ha.
def ex_elim (A : type) (p : term A -> prop) (c : prop)
def ex_elim (A : sort) (p : term A -> prop) (c : prop)
(H : proof (ex A p)) (f : a : term A -> proof (p a) -> proof c) : proof c :=
H c f.
......
#NAME inhabited_types.
def default_value : A : fol.type -> fol.term A.
......@@ -5,7 +5,7 @@ https://en.wikipedia.org/wiki/Presburger_arithmetic ;)
(; There is just one sort representing natural numbers ;)
Nat : fol.type.
Nat : fol.sort.
(; There is just one predicate symbol for equality ;)
EQ : fol.predicate.
......@@ -21,10 +21,10 @@ ONE : fol.function.
ADD : fol.function.
(; Arities ;)
[] fol.pred_arity EQ --> fol.read_types (nat.S (nat.S nat.O)) Nat Nat.
[] fol.fun_arity ZERO --> fol.nil_type.
[] fol.fun_arity ONE --> fol.nil_type.
[] fol.fun_arity ADD --> fol.read_types (nat.S (nat.S nat.O)) Nat Nat.
[] fol.pred_arity EQ --> fol.read_sorts (nat.S (nat.S nat.O)) Nat Nat.
[] fol.fun_arity ZERO --> fol.nil_sort.
[] fol.fun_arity ONE --> fol.nil_sort.
[] fol.fun_arity ADD --> fol.read_sorts (nat.S (nat.S nat.O)) Nat Nat.
[] fol.fun_codomain ZERO --> Nat.
[] fol.fun_codomain ONE --> Nat.
[] fol.fun_codomain ADD --> Nat.
......
......@@ -45,8 +45,8 @@ about [[* Resolution][resolution]].
We have chosen to use a multi-sorted version of first-order logic. In
this setting, the arity of a predicate or function symbol is not
simply a natural number but a list of types (also known as /sorts/)
and each function symbol has a codomain type.
simply a natural number but a list of sorts (also known as /types/)
and each function symbol has a codomain sort.
We use a multi-sorted logic for two reasons. First, some automatic
provers such as Zenon Arith and Zipperposition work in this
......@@ -58,26 +58,26 @@ be soundly done if we have a way to distinguish booleans from numbers.
** Syntax
The syntax of multi-sorted first-order logic is composed of four
syntactic categories: types, terms, formulae, and proofs.
syntactic categories: sorts, terms, formulae, and proofs.
*** Types
*** Sorts
First-order types (also known as /sorts/) are the elements of the
Dedukti type =fol.type=. The file [[./fol/fol.dk][fol/fol.dk]] does not provide any
function to build types; instead the definer of a theory is expected
to declare the various types she needs.
First-order sorts are the elements of the Dedukti type =fol.sort=.
The file [[./fol/fol.dk][fol/fol.dk]] does not provide any function to build sorts;
instead the definer of a theory is expected to declare the various
sorts she needs.
However, once some types have been declared, the file [[./fol/fol.dk][fol/fol.dk]]
provides functions for building lists of types. The Dedukti type of
lists of types is =fol.types= and its constructors are
- =fol.nil_type : fol.types= and
- =fol.cons_type : fol.type -> fol.types -> fol.types=
However, once some sorts have been declared, the file [[./fol/fol.dk][fol/fol.dk]]
provides functions for building lists of sorts. The Dedukti type of
lists of sorts is =fol.sorts= and its constructors are
- =fol.nil_sort : fol.sorts= and
- =fol.cons_sort : fol.sort -> fol.sorts -> fol.sorts=
For convenience, the file [[./fol/fol.dk][fol/fol.dk]] also defines an n-ary function
for building lists of types:
- =fol.read_types n A1 … An= is defined as =fol.cons_type A1 (… (fol.cons_type An fol.nil_type)…)=
for building lists of sorts:
- =fol.read_sorts n A1 … An= is defined as =fol.cons_sort A1 (… (fol.cons_sort An fol.nil_sort)…)=
The first parameter =n= of =fol.read_types= is a natural number of
The first parameter =n= of =fol.read_sorts= is a natural number of
type =nat.Nat=. It can be built from
- =nat.O : nat.Nat= representing 0 and
- =nat.S : nat.Nat -> nat.Nat= representing the successor operation
......@@ -89,33 +89,33 @@ following sense:
- Dedukti typing judgment is used to represent first-order typing
- Dedukti variables are used to represent first-order variables
If =A= is a first-order type, the Dedukti type of first-order terms of
type =A= is =fol.term A=; in other words, the Dedukti symbol
=fol.term= has type =fol.type -> Type=.
If =A= is a sort, the Dedukti type of first-order terms of
sort =A= is =fol.term A=; in other words, the Dedukti symbol
=fol.term= has type =fol.sort -> Type=.
A function symbol is a Dedukti term of type =fol.function=.
A codomain and an arity are respectively associated to each function
symbol by the functions
- =fol.fun_arity : fol.function -> fol.types= and
- =fol.fun_codomain : fol.function -> fol.type=
- =fol.fun_arity : fol.function -> fol.sorts= and
- =fol.fun_codomain : fol.function -> fol.sort=
If =As= is a list of types, then =fol.terms As= is the Dedukti type of
lists of terms whose types match =As=. This type has two constructors:
- =fol.nil_term : fol.terms fol.nil_type= representing the empty list
If =As= is a list of sorts, then =fol.terms As= is the Dedukti type of
lists of terms whose sorts match =As=. This type has two constructors:
- =fol.nil_term : fol.terms fol.nil_sort= representing the empty list
of terms
- =fol.cons_term : A : fol.type -> fol.term A -> tail_types : fol.types -> fol.terms tail_types -> fol.terms (fol.cons_type A tail_types)=
- =fol.cons_term : A : fol.sort -> fol.term A -> tail_sorts : fol.sorts -> fol.terms tail_sorts -> fol.terms (fol.cons_sort A tail_sorts)=
The only constructor of =fol.term A= is application of a function
symbol =f= whose codomain is =A= to a list of terms whose types match
symbol =f= whose codomain is =A= to a list of terms whose sorts match
the arity of =f=.
- =fol.apply_fun : f : fol.function -> fol.terms (fol.fun_arity f) -> fol.term (fol.fun_codomain f)=
For convenience, the file [[./fol/fol.dk][fol/fol.dk]] also defines an n-ary function
for applying a function symbol to terms:
- if =f= is a function symbol of arity =fol.read_types n A1 … An= and
of codomain =B=, and if =a1=, …, =an= are =n= terms of type =A1=, …,
=An= respectively, then =fol.fun_apply f a1 … an= has type =B=.
- if =f= is a function symbol of arity =fol.read_sorts n A1 … An= and
of codomain =B=, and if =a1=, …, =an= are =n= terms of sort =A1=, …,
=An= respectively, then =fol.fun_apply f a1 … an= has sort =B=.
*** Formulae
......@@ -132,7 +132,7 @@ the predicate symbol. Predicate symbols and their arities are defined
similarly to function symbols. A predicate symbol is a Dedukti term of
type =fol.predicate=. An artity is associated to each predicate
symbol by the function
- =fol.pred_arity : fol.predicate -> fol.types=
- =fol.pred_arity : fol.predicate -> fol.sorts=
Applying a predicate symbol on a list of terms respecting its arity
produces a formula:
......@@ -140,8 +140,8 @@ produces a formula:
For convenience, the file [[./fol/fol.dk][fol/fol.dk]] also defines an n-ary function
for applying a predicate symbol to terms:
- if =p= is a predicate symbol of arity =fol.read_types n A1 … An= and
if =a1=, …, =an= are =n= terms of type =A1=, …, =An= respectively,
- if =p= is a predicate symbol of arity =fol.read_sorts n A1 … An= and
if =a1=, …, =an= are =n= terms of sort =A1=, …, =An= respectively,
then =fol.pred_apply p a1 … an= has type =fol.prop=.
**** Logical connectives
......@@ -164,24 +164,24 @@ connectives respectively defined by:
**** Quantifiers
We consider universal and existential quantifiers. Each quantifier
binds a single variable of a given type. As we promised in [[* Terms][the section
binds a single variable of a given sort. As we promised in [[* Terms][the section
about terms]], variable binding is shallow in the sense that variables
are represented by Dedukti variables.
The universal and existential quantifiers are respectively =fol.all=
and =fol.ex=. They have the same Dedukti type: =A : fol.type -> (fol.term A -> fol.prop) -> fol.prop=.
and =fol.ex=. They have the same Dedukti type: =A : fol.sort -> (fol.term A -> fol.prop) -> fol.prop=.
**** n-ary connectives and quantifiers
For convenience, n-ary versions =fol.nand=, =fol.nor=, =fol.nimp=,
=fol.nall=, and =fol.nex= of respectively =fol.or=, =fol.and=,
=fol.imp=, =fol.all=, and =fol.ex= are also defined with the following
types:
sorts:
- =fol.nand : n : nat.Nat -> A₁ : prop -> … -> Aₙ : prop -> prop=
- =fol.nor : n : nat.Nat -> A₁ : prop -> … -> Aₙ : prop -> prop=
- =fol.nimp : n : nat.Nat -> A₁ : prop -> … -> Aₙ : prop -> prop -> prop=
- =fol.nall : n : nat.Nat -> A₁ : type -> … -> Aₙ : type -> (term A₁ -> … -> term Aₙ -> prop) -> prop=
- =fol.nex : n : nat.Nat -> A₁ : type -> … -> Aₙ : type -> (term A₁ -> … -> term Aₙ -> prop) -> prop=
- =fol.nall : n : nat.Nat -> A₁ : sort -> … -> Aₙ : sort -> (term A₁ -> … -> term Aₙ -> prop) -> prop=
- =fol.nex : n : nat.Nat -> A₁ : sort -> … -> Aₙ : sort -> (term A₁ -> … -> term Aₙ -> prop) -> prop=
They are defined by nesting the corresponding connectives and quantifiers as follows:
- =fol.nand 0 = fol.true=
......@@ -211,16 +211,16 @@ corresponding certificates constructors presented in [[* Reasoning][the reasonin
- =fol.or_elim : A : fol.prop -> B : fol.prop -> C : fol.prop -> fol.proof (fol.or A B) -> (fol.proof A -> fool.proof C) -> (fol.proof B -> fool.proof C) -> fol.proof C=
- =fol.imp_intro : A : fol.prop -> B : fol.prop -> (fol.proof A -> fol.proof B) -> fol.proof (fol.imp A B)=
- =fol.imp_elim : A : fol.prop -> B : fol.prop -> fol.proof (fol.imp A B) -> fol.proof A -> fol.proof B=
- =fol.all_intro : A : fol.type -> B : (fol.term A -> fol.prop) -> (a : fol.term A -> fol.proof (B a)) -> fol.proof (fol.all A B)=
- =fol.all_elim : A : fol.type -> B : (fol.term A -> fol.prop) -> fol.proof (fol.all A B) -> a : fol.term A -> fol.proof (B a)=
- =fol.ex_intro : A : fol.type -> B : (fol.term A -> fol.prop) -> a : fol.term A -> fol.proof (B a) -> fol.proof (fol.ex A B)=
- =fol.ex_elim : A : fol.type -> B : (fol.term A -> fol.prop) -> C : fol.prop -> fol.proof (fol.ex A B) -> (a : fol.term A -> fol.proof (B a) -> fol.proof C) -> fol.proof C=
- =fol.all_intro : A : fol.sort -> B : (fol.term A -> fol.prop) -> (a : fol.term A -> fol.proof (B a)) -> fol.proof (fol.all A B)=
- =fol.all_elim : A : fol.sort -> B : (fol.term A -> fol.prop) -> fol.proof (fol.all A B) -> a : fol.term A -> fol.proof (B a)=
- =fol.ex_intro : A : fol.sort -> B : (fol.term A -> fol.prop) -> a : fol.term A -> fol.proof (B a) -> fol.proof (fol.ex A B)=
- =fol.ex_elim : A : fol.sort -> B : (fol.term A -> fol.prop) -> C : fol.prop -> fol.proof (fol.ex A B) -> (a : fol.term A -> fol.proof (B a) -> fol.proof C) -> fol.proof C=
** Defining a first-order theory
To define a new first-order theory, we start by declaring the sorts,
predicate symbols, and function symbols as new constants of type
=fol.type=, =fol.predicate=, and =fol.function= respectively. We then
=fol.sort=, =fol.predicate=, and =fol.function= respectively. We then
define the arity of each function and predicate symbol and the
codomain sort of each function symbol by extending the definitions of
=fol.pred_arity=, =fol.fun_arity=, and =fol.fun_codomain= respectively.
......@@ -242,11 +242,11 @@ definable so Deduction Modulo first-order theories can be defined.
We treat equality as a first-order theory defined in the file
[[./fol/eq.dk][fol/eq.dk]]. Equality is a family of predicate symbols parameterized by
a sort:
- =eq.Eq : fol.type -> fol.predicate=
- =eq.Eq : fol.sort -> fol.predicate=
The predicate symbol =eq.Eq A= expects two terms of type =A= so the arity of the symbol =eq.Eq A= is =fol.read_types (nat.S (nat.S nat.O)) A A=.
The predicate symbol =eq.Eq A= expects two terms of sort =A= so the arity of the symbol =eq.Eq A= is =fol.read_sorts (nat.S (nat.S nat.O)) A A=.
The shortcut notation =eq.eq A a b= where =A= has type =fol.type= and
The shortcut notation =eq.eq A a b= where =A= has type =fol.sort= and
both =a= and =b= have type =fol.term A= denotes the formula
=fol.pred_apply (eq.Eq A) a b=.
......@@ -254,14 +254,14 @@ Equality is defined impredicatively as all the logical connectives and
quantifiers. The file [[./fol/eq.dl][fol/eq.dk]] also contains proofs of the following
facts:
- Equality is reflexive:
=eq.eq_refl : A : fol.type -> fol.proof (fol.all A (x => eq.eq A x x))=
=eq.eq_refl : A : fol.sort -> fol.proof (fol.all A (x => eq.eq A x x))=
- Equality is symmetric:
=eq.eq_symm : A : fol.type -> fol.proof (fol.all A (x => fol.all A (y => fol.imp (eq.eq A y x) (eq.eq A x y))))=
=eq.eq_symm : A : fol.sort -> fol.proof (fol.all A (x => fol.all A (y => fol.imp (eq.eq A y x) (eq.eq A x y))))=
- Equality is transitive:
=eq.eq_trans : A : fol.type -> fol.proof (fol.all A (x => fol.all A (y => fol.all A (z => fol.imp (eq.eq A x y) (fol.imp (eq.eq A y z) (eq.eq A x z))))))=
=eq.eq_trans : A : fol.sort -> fol.proof (fol.all A (x => fol.all A (y => fol.all A (z => fol.imp (eq.eq A x y) (fol.imp (eq.eq A y z) (eq.eq A x z))))))=
- Equality is a congruence with respect to all function symbols:
=eq.eq_fun_equal : f : fol.function -> fol.proof (fol.all A1 (x1 => fol.all A1 (y1 => fol.imp (eq.eq A1 x1 y1) (… fol.all An (xn => fol.all An (yn => fol.imp (eq.eq An xn yn) (eq.eq B (fol.apply_fun f x1 … xn) (fol.apply_fun f y1 … yn)))) …))))=
where =f= has arity =fol.read_types n A1 … An= and codomain =B=.
where =f= has arity =fol.read_sorts n A1 … An= and codomain =B=.
- Equality is a congruence with respect to all predicate symbols:
=eq.eq_pred_equal : p : fol.predicate -> fol.proof (fol.all A1 (x1 => fol.all A1 (y1 => fol.imp (eq.eq A1 x1 y1) (… fol.all An (xn => fol.all An (yn => fol.imp (eq.eq An xn yn) (fol.imp (fol.apply_pred p x1 … xn) (fol.apply_pred p y1 … yn)))) …))))=
where =p= has arity =fol.read_yypes n A1 … An=
......@@ -345,7 +345,7 @@ The tactic language uses a shallow representation of variables and
contexts. In order to introduce a new variable or assumption in
context, we use non-linear higher-order rewriting to define the symbols =tac.intro_term= and =tac.intro_proof=:
#+BEGIN_SRC dedukti
def intro_term : A : fol.type ->
def intro_term : A : fol.sort ->
B : (fol.term A -> fol.prop) ->
(x : fol.term A -> tac.tactic (B x)) ->
tac.tactic (fol.all A B).
......@@ -394,7 +394,7 @@ a tactic attempting to prove the goal formula.
- =cert.context : Type=
- =cert.nil_ctx : cert.context=
- =cert.cons_ctx_var : A : fol.type -> fol.term A -> cert.context -> cert.context=
- =cert.cons_ctx_var : A : fol.sort -> fol.term A -> cert.context -> cert.context=
- =cert.cons_ctx_proof : A : fol.prop -> fol.proof A -> cert.context -> cert.context=
- =cert.certificate : Type=
- =cert.run : A : fol.prop -> cert.context -> cert.certificate -> tac.tactic A=
......@@ -434,7 +434,7 @@ certificate succeeds if the goal is either an implication =fol.imp A
B= such that =c= successfully proves =B= in a context extended by the
assumption =A= or a universal statement =fol.all A B= such that =c=
successfully proves =B a= in a context extended by the variable =a= of
type =A=. On any other goal, the tactic =cert.intro c= raises the
sort =A=. On any other goal, the tactic =cert.intro c= raises the
exception =cert.not_a_product=.
Moreover, the file [[./meta/cert.dk][meta/cert.dk]] defines certificate primitives for
......@@ -464,7 +464,7 @@ assumptions or all variables in parallel. This behaviour is provided
by the =cert.with_assumption= and =cert.with_variable= certificate
combinators:
- =cert.with_assumption : (A : fol.prop -> fol.proof A -> cert.certificate) -> cert.certificate=
- =cert.with_variable : (A : fol.type -> fol.term A -> cert.certificate) -> cert.certificate=
- =cert.with_variable : (A : fol.sort -> fol.term A -> cert.certificate) -> cert.certificate=
The =cert.with_assumption f= certificates is successful if =f A a= is
successful for any assumption =a : fol.proof A=. Otherwise, it raises
......@@ -491,8 +491,8 @@ can be used for this purpose:
(fol.prop -> fol.prop -> cert.certificate) ->
(fol.prop -> fol.prop -> cert.certificate) ->
(fol.prop -> fol.prop -> cert.certificate) ->
(A : fol.type -> (fol.term A -> fol.prop) -> cert.certificate) ->
(A : fol.type -> (fol.term A -> fol.prop) -> cert.certificate) ->
(A : fol.sort -> (fol.term A -> fol.prop) -> cert.certificate) ->
(A : fol.sort -> (fol.term A -> fol.prop) -> cert.certificate) ->
(p : fol.predicate ->
fol.terms (fol.pred_arity p) ->
cert.certificate) ->
......@@ -517,18 +517,18 @@ on each of the cases:
- =cert.match_and : fol.prop -> (fol.prop -> fol.prop -> cert.certificate) -> cert.certificate -> cert.certificate=
- =cert.match_or : fol.prop -> (fol.prop -> fol.prop -> cert.certificate) -> cert.certificate -> cert.certificate=
- =cert.match_imp : fol.prop -> (fol.prop -> fol.prop -> cert.certificate) -> cert.certificate -> cert.certificate=
- =cert.match_all : fol.prop -> (A : fol.type -> (fol.term A -> fol.prop) -> cert.certificate) -> cert.certificate -> cert.certificate=
- =cert.match_ex : fol.prop -> (A : fol.type -> (fol.term A -> fol.prop) -> cert.certificate) -> cert.certificate -> cert.certificate=
- =cert.match_all : fol.prop -> (A : fol.sort -> (fol.term A -> fol.prop) -> cert.certificate) -> cert.certificate -> cert.certificate=
- =cert.match_ex : fol.prop -> (A : fol.sort -> (fol.term A -> fol.prop) -> cert.certificate) -> cert.certificate -> cert.certificate=
- =cert.match_pred : fol.prop -> (p : fol.predicate -> fol.terms (fol.pred_arity p) -> cert.certificate) -> cert.certificate -> cert.certificate=
** Type and formulae comparison
** Sort and formulae comparison
We have seen how to inspect the structure of a formula but this is of
little use until we are able to test whether or not two formulae or
types are identical and obtain coercion functions when they are.
sorts are identical and obtain coercion functions when they are.
This behaviour is provided by the following combinators:
- =cert.ifeq_type : A : fol.type -> B : fol.type -> ((fol.term A -> fol.term B) -> cert.certificate) -> cert.certificate -> cert.certificate=
- =cert.ifeq_sort : A : fol.sort -> B : fol.sort -> ((fol.term A -> fol.term B) -> cert.certificate) -> cert.certificate -> cert.certificate=
- =cert.ifeq_prop : A : fol.prop -> B : fol.prop -> ((fol.proof A -> fol.proof B) -> cert.certificate) -> cert.certificate -> cert.certificate=
** Reasoning
......@@ -546,7 +546,7 @@ The following combinators are used to apply a lemma:
- =cert.refine2 : A : fol.prop -> B : fol.prop -> C : fol.prop -> (fol.proof A -> fol.proof B -> fol.proof C) -> cert.certificate -> cert.certificate -> cert.certificate=
- =cert.refinen : n : nat.Nat -> A1 : fol.prop -> … -> An : fol.prop -> B : fol.prop -> (fol.proof A1 -> … -> fol.proof An -> fol.proof B) -> c1 : cert.certificate -> … -> cn : cert.certificate -> cert.certificate=
- =cert.assert : fol.prop -> cert.certificate -> cert.certificate -> cert.certificate=
- =cert.apply : A : fol.type -> (fol.term A -> fol.prop) -> fol.term A -> cert.certificate -> cert.certificate=
- =cert.apply : A : fol.sort -> (fol.term A -> fol.prop) -> fol.term A -> cert.certificate -> cert.certificate=
The certificate =cert.refine A B f c= proves =B= by applying the lemma
=f= which has an assumption =A= proved by the certificate =c=.
......@@ -573,7 +573,7 @@ each proves the current goal if it has a particular shape:
- =cert.split : cert.certificate -> cert.certificate -> cert.certificate=
- =cert.left : cert.certificate -> cert.certificate=
- =cert.right : cert.certificate -> cert.certificate=
- =cert.exists : A : fol.type -> fol.term A -> cert.certificate -> cert.certificate=
- =cert.exists : A : fol.sort -> fol.term A -> cert.certificate -> cert.certificate=
The certificate =cert.trivial= proves the goal =fol.true=. The
certificate =cert.split c1 c2= proves =fol.and A B= if =c1= proves =A=
......@@ -590,8 +590,8 @@ The following certificates are used to reason from assumptions:
- =cert.destruct_and : fol.prop -> fol.prop -> cert.certificate -> cert.certificate -> cert.certificate=
- =cert.destruct_or : fol.prop -> fol.prop -> cert.certificate