Commit 44fc0b7b authored by Pierre Letouzey's avatar Pierre Letouzey
Browse files

renommage: gen_signature -> signature

parent be062cbe
......@@ -18,19 +18,26 @@ Definition arity := nat.
Bind Scope string_scope with function_symbol.
Bind Scope string_scope with predicate_symbol.
Record gen_signature :=
{ gen_fun_symbs : function_symbol -> option arity;
gen_pred_symbs : predicate_symbol -> option arity }.
Record signature :=
make_infinite_sign
{ funsymbs : function_symbol -> option arity;
predsymbs : predicate_symbol -> option arity }.
(** A finite version *)
Module Finite.
Record signature :=
{ fun_symbs : list (function_symbol * arity);
pred_symbs : list (predicate_symbol * arity) }.
make_finite_sign
{ funsymbs : list (function_symbol * arity);
predsymbs : list (predicate_symbol * arity) }.
Definition to_infinite sign :=
make_infinite_sign
(fun s => list_assoc s sign.(funsymbs))
(fun s => list_assoc s sign.(predsymbs)).
Definition generalize_signature sign :=
{| gen_fun_symbs := fun s => list_assoc s sign.(fun_symbs);
gen_pred_symbs := fun s => list_assoc s sign.(pred_symbs) |}.
End Finite.
(** In pratice, the symbols could be special characters as "+", or
......@@ -38,12 +45,12 @@ Definition generalize_signature sign :=
the parenthesis characters or the comma. *)
Definition peano_sign :=
{| fun_symbs := [("O",0);("S",1);("+",2);("*",2)];
pred_symbs := [("=",2)] |}.
{| Finite.funsymbs := [("O",0);("S",1);("+",2);("*",2)];
Finite.predsymbs := [("=",2)] |}.
Definition zf_sign :=
{| fun_symbs := [];
pred_symbs := [("=",2);("∈",2)] |}.
{| Finite.funsymbs := [];
Finite.predsymbs := [("=",2);("∈",2)] |}.
(** Variables *)
......
......@@ -15,7 +15,7 @@ Lemma check_bsubst_term sign n (u t:term) :
Proof.
induction t as [ | | f l IH] using term_ind'; cbn; auto.
- case eqbspec; auto.
- destruct gen_fun_symbs; auto.
- destruct funsymbs; auto.
rewrite !lazy_andb_iff, map_length.
intros Hu (Hl,Hl'); split; auto.
rewrite forallb_forall in *. intros t Ht.
......@@ -28,7 +28,7 @@ Lemma check_bsubst sign n u (f:formula) :
Proof.
revert n.
induction f; cbn; intros n Hu Hf; auto.
- destruct gen_pred_symbs; auto.
- destruct predsymbs; auto.
rewrite !lazy_andb_iff in *. rewrite map_length.
destruct Hf as (Hl,Hl'); split; auto.
rewrite forallb_forall in *. intros t Ht.
......@@ -1118,7 +1118,7 @@ Qed.
Fixpoint restrict_term sign x t :=
match t with
| Fun f l =>
match sign.(gen_fun_symbs) f with
match sign.(funsymbs) f with
| None => FVar x
| Some ar =>
if length l =? ar then Fun f (map (restrict_term sign x) l)
......@@ -1132,7 +1132,7 @@ Fixpoint restrict sign x f :=
| True => True
| False => False
| Pred p l =>
match sign.(gen_pred_symbs) p with
match sign.(predsymbs) p with
| None => False
| Some ar =>
if length l =? ar then Pred p (map (restrict_term sign x) l)
......@@ -1174,7 +1174,7 @@ Lemma restrict_term_level sign x t :
Proof.
revert t.
fix IH 1. destruct t as [ | | f l]; cbn; auto with *.
destruct gen_fun_symbs; cbn; auto with *.
destruct funsymbs; cbn; auto with *.
case eqbspec; cbn; auto with *.
intros _. clear f a.
revert l.
......@@ -1191,7 +1191,7 @@ Lemma restrict_level sign x f :
level (restrict sign x f) <= level f.
Proof.
induction f; cbn; auto using Nat.max_le_compat with *.
destruct gen_pred_symbs; cbn; auto with *.
destruct predsymbs; cbn; auto with *.
case eqbspec; cbn; auto with *.
intros _. clear p a.
induction l as [|t l IH]; cbn;
......@@ -1209,7 +1209,7 @@ Lemma restrict_term_fvars sign x t :
(Vars.add x (fvars t)).
Proof.
induction t as [ | | f l IH] using term_ind'; cbn; auto with *.
destruct gen_fun_symbs; cbn; auto with *.
destruct funsymbs; cbn; auto with *.
case eqbspec; cbn; auto with *.
intros _. clear f a.
intros v. rewrite Vars.add_spec, !vars_unionmap_in.
......@@ -1226,7 +1226,7 @@ Lemma restrict_form_fvars sign x f :
(Vars.add x (fvars f)).
Proof.
induction f; cbn; auto with *.
destruct gen_pred_symbs; cbn; auto with *.
destruct predsymbs; cbn; auto with *.
case eqbspec; cbn; auto with *.
intros _. clear p a.
intros v. rewrite Vars.add_spec, !vars_unionmap_in.
......@@ -1291,7 +1291,7 @@ Lemma restrict_term_bsubst sign x n (t u:term) :
Proof.
induction t as [ | |f l IH] using term_ind'; cbn; auto.
- case eqbspec; auto.
- destruct gen_fun_symbs; cbn; auto with *.
- destruct funsymbs; cbn; auto with *.
rewrite map_length.
case eqbspec; cbn; auto.
intros _.
......@@ -1304,7 +1304,7 @@ Lemma restrict_bsubst sign x n t f :
Proof.
revert n.
induction f; cbn; intros; f_equal; auto.
destruct gen_pred_symbs; cbn; auto with *.
destruct predsymbs; cbn; auto with *.
rewrite map_length.
case eqbspec; cbn; auto.
intros _.
......@@ -1355,7 +1355,7 @@ Lemma check_restrict_term_id sign x (t:term) :
check sign t = true -> restrict_term sign x t = t.
Proof.
induction t as [ | | f l IH] using term_ind'; cbn; auto.
destruct gen_fun_symbs; try easy.
destruct funsymbs; try easy.
rewrite lazy_andb_iff. intros (->,H). f_equal.
rewrite forallb_forall in H.
apply map_id_iff; auto.
......@@ -1365,7 +1365,7 @@ Lemma check_restrict_id sign x (f:formula) :
check sign f = true -> restrict sign x f = f.
Proof.
induction f; cbn; intros; f_equal; auto.
- destruct gen_pred_symbs; try easy.
- destruct predsymbs; try easy.
rewrite lazy_andb_iff in H. destruct H as (->,H). f_equal.
rewrite forallb_forall in H.
apply map_id_iff; auto using check_restrict_term_id.
......@@ -1386,7 +1386,7 @@ Lemma restrict_term_check sign x (t:term) :
check sign (restrict_term sign x t) = true.
Proof.
induction t as [ | | f l IH] using term_ind'; cbn; auto.
destruct gen_fun_symbs eqn:E; try easy.
destruct funsymbs eqn:E; try easy.
case eqbspec; cbn; auto.
intros <-.
rewrite E.
......@@ -1399,7 +1399,7 @@ Lemma restrict_form_check sign x (f:formula) :
check sign (restrict sign x f) = true.
Proof.
induction f; cbn; auto.
- destruct gen_pred_symbs eqn:E; try easy.
- destruct predsymbs eqn:E; try easy.
case eqbspec; cbn; auto.
intros <-.
rewrite E.
......@@ -1740,7 +1740,7 @@ Proof.
induction t as [ | | f l IH] using term_ind';
cbn - [Nat.ltb]; auto.
- case Nat.ltb_spec; auto.
- destruct gen_fun_symbs as [ar|] eqn:E; auto.
- destruct funsymbs as [ar|] eqn:E; auto.
rewrite map_length.
case eqbspec; cbn; auto.
intros _. f_equal.
......@@ -1754,7 +1754,7 @@ Lemma restrict_forcelevel sign x n y f :
Proof.
revert n.
induction f; cbn; intros; f_equal; auto.
destruct gen_pred_symbs as [ar|] eqn:E; auto.
destruct predsymbs as [ar|] eqn:E; auto.
rewrite map_length.
case eqbspec; cbn; auto.
intros _. f_equal.
......
......@@ -85,7 +85,7 @@ Compute print_term peano_term_example.
with instances for terms, formulas, context, sequent, ... *)
(** Check for known function/predicate symbols + correct arity *)
Class Check (A : Type) := check : gen_signature -> A -> bool.
Class Check (A : Type) := check : signature -> A -> bool.
Arguments check {_} {_} _ !_.
(** Replace a bound variable with a term *)
......@@ -123,7 +123,7 @@ Definition fsubst {A}`{VMap A} (v:variable)(u:term) :=
(** Some structural extensions of these generic functions *)
Instance check_list {A}`{Check A} : Check (list A) :=
fun (sign : gen_signature) => List.forallb (check sign).
fun (sign : signature) => List.forallb (check sign).
Instance bsubst_list {A}`{BSubst A} : BSubst (list A) :=
fun n t => List.map (bsubst n t).
......@@ -138,7 +138,7 @@ Instance vmap_list {A}`{VMap A} : VMap (list A) :=
fun h => List.map (vmap h).
Instance check_pair {A B}`{Check A}`{Check B} : Check (A*B) :=
fun (sign : gen_signature) '(a,b) => check sign a &&& check sign b.
fun (sign : signature) '(a,b) => check sign a &&& check sign b.
Instance bsubst_pair {A B}`{BSubst A}`{BSubst B} : BSubst (A*B) :=
fun n t '(a,b) => (bsubst n t a, bsubst n t b).
......@@ -158,19 +158,19 @@ Instance vmap_pair {A B}`{VMap A}`{VMap B} : VMap (A*B) :=
with the correct arity. *)
Instance check_term : Check term :=
fun (sign : gen_signature) =>
fun (sign : signature) =>
fix check_term t :=
match t with
| FVar _ | BVar _ => true
| Fun f args =>
match sign.(gen_fun_symbs) f with
match sign.(funsymbs) f with
| None => false
| Some ar =>
(List.length args =? ar) &&& (List.forallb check_term args)
end
end.
Compute check (generalize_signature peano_sign) peano_term_example.
Compute check (Finite.to_infinite peano_sign) peano_term_example.
Instance term_fvars : FVars term :=
fix term_fvars t :=
......@@ -291,7 +291,7 @@ Definition test_form := (∃ (True <-> Pred "p" [#0;#0]))%form.
(** Utilities about formula *)
Instance check_formula : Check formula :=
fun (sign : gen_signature) =>
fun (sign : signature) =>
fix check_formula f :=
match f with
| True | False => true
......@@ -299,7 +299,7 @@ Instance check_formula : Check formula :=
| Op _ f f' => check_formula f &&& check_formula f'
| Quant _ f => check_formula f
| Pred p args =>
match sign.(gen_pred_symbs) p with
match sign.(predsymbs) p with
| None => false
| Some ar =>
(List.length args =? ar) &&& (List.forallb (check sign) args)
......
......@@ -104,18 +104,18 @@ Compute Term.print peano_term_example.
iff it only refer to known function symbols and use them
with the correct arity. *)
Fixpoint check (sign : gen_signature) t :=
Fixpoint check (sign : signature) t :=
match t with
| Var _ => true
| Fun f args =>
match sign.(gen_fun_symbs) f with
match sign.(funsymbs) f with
| None => false
| Some ar =>
(List.length args =? ar) &&& (List.forallb (check sign) args)
end
end.
Compute Term.check (generalize_signature peano_sign) peano_term_example.
Compute Term.check (Finite.to_infinite peano_sign) peano_term_example.
(** The set of variables occurring in a term *)
......@@ -239,14 +239,14 @@ Compute Form.print (Iff True False).
(** Utilities about formula *)
Fixpoint check (sign : gen_signature) f :=
Fixpoint check (sign : signature) f :=
match f with
| True | False => true
| Not f => check sign f
| Op _ f f' => check sign f &&& check sign f'
| Quant _ v f => check sign f
| Pred p args =>
match sign.(gen_pred_symbs) p with
match sign.(predsymbs) p with
| None => false
| Some ar =>
(List.length args =? ar) &&& (List.forallb (Term.check sign) args)
......
......@@ -12,7 +12,7 @@ Local Open Scope eqb_scope.
- with bounded variables that are indeed bounded
- without free variables *)
Definition Wf (sign:gen_signature) (A:formula) :=
Definition Wf (sign:signature) (A:formula) :=
check sign A = true /\ BClosed A /\ FClosed A.
Hint Unfold Wf.
......@@ -46,7 +46,7 @@ Proof.
Qed.
Lemma bsubst_cst_wf sign c A :
sign.(gen_fun_symbs) c = Some 0 ->
sign.(funsymbs) c = Some 0 ->
Wf sign (A) -> Wf sign (bsubst 0 (Cst c) A).
Proof.
intros E (CK & BC & FC).
......@@ -56,11 +56,11 @@ Proof.
- rewrite bsubst_fvars. cbn - [Vars.union]. varsdec.
Qed.
Definition ValidDerivOn logic (sign:gen_signature) d :=
Definition ValidDerivOn logic (sign:signature) d :=
check sign d = true /\ BClosed d /\ Valid logic d.
Record theory :=
{ sign :> gen_signature;
{ sign :> signature;
IsAxiom : formula -> Prop;
WfAxiom : forall A, IsAxiom A -> Wf sign A }.
......@@ -155,8 +155,8 @@ Definition optfun_finer {A B} (f f' : A -> option B) :=
forall a, opt_finer (f a) (f' a).
Definition SignExtend sign sign' :=
optfun_finer (sign.(gen_fun_symbs)) (sign'.(gen_fun_symbs)) /\
optfun_finer (sign.(gen_pred_symbs)) (sign'.(gen_pred_symbs)).
optfun_finer (sign.(funsymbs)) (sign'.(funsymbs)) /\
optfun_finer (sign.(predsymbs)) (sign'.(predsymbs)).
Lemma signext_refl sign : SignExtend sign sign.
Proof.
......@@ -179,7 +179,7 @@ Proof.
intros (SE,_).
induction t using term_ind'; cbn; auto.
destruct (SE f) as [->|<-]; try easy.
destruct gen_fun_symbs; auto.
destruct funsymbs; auto.
destruct (length args =? a); auto.
rewrite !forallb_forall; auto.
Qed.
......@@ -190,7 +190,7 @@ Proof.
intros SE.
induction f; cbn; auto.
destruct (proj2 SE p) as [->|<-]; try easy.
destruct gen_pred_symbs; auto.
destruct predsymbs; auto.
destruct (length l =? a); auto.
rewrite !forallb_forall; eauto using signext_check_term.
rewrite !lazy_andb_iff; intuition.
......@@ -264,7 +264,7 @@ Proof.
Qed.
Definition IsEqualityTheory th :=
th.(gen_pred_symbs) "=" = Some 2 /\
th.(predsymbs) "=" = Some 2 /\
IsTheorem th (Pred "=" [#0; #0])%form /\
forall A z,
check th A = true ->
......@@ -343,8 +343,8 @@ Qed.
(** Tweaking the function symbols of a signature *)
Definition modify_funsymbs sign modif :=
{| gen_fun_symbs := modif (sign.(gen_fun_symbs));
gen_pred_symbs := sign.(gen_pred_symbs) |}.
{| funsymbs := modif (sign.(funsymbs));
predsymbs := sign.(predsymbs) |}.
(** Henkin extension : from an existential theorem [A],
adding a new constant [c] as witness and the new axiom [A(c)].
......@@ -358,7 +358,7 @@ Definition Henkin_axiom Ax (A:formula) c :=
fun f => Ax f \/ f = bsubst 0 (Cst c) A.
Lemma Henkin_signext sign c :
sign.(gen_fun_symbs) c = None ->
sign.(funsymbs) c = None ->
SignExtend sign (Henkin_sign sign c).
Proof.
intros Hc.
......@@ -367,7 +367,7 @@ Proof.
Qed.
Lemma Henkin_ax_wf th A c :
th.(gen_fun_symbs) c = None ->
th.(funsymbs) c = None ->
IsTheorem th (A) ->
forall B, Henkin_axiom th.(IsAxiom) A c B ->
Wf (Henkin_sign th c) B.
......@@ -380,7 +380,7 @@ Proof.
Qed.
Definition Henkin_ext th A c
(E:th.(gen_fun_symbs) c = None)
(E:th.(funsymbs) c = None)
(Thm:IsTheorem th (A)) :=
{| sign := Henkin_sign th c;
IsAxiom := Henkin_axiom th.(IsAxiom) A c;
......@@ -388,7 +388,7 @@ Definition Henkin_ext th A c
|}.
Lemma Henkin_consext th A c
(E:th.(gen_fun_symbs) c = None)
(E:th.(funsymbs) c = None)
(Thm:IsTheorem th (A)) :
ConservativeExt th (Henkin_ext th A c E Thm).
Proof.
......@@ -496,7 +496,7 @@ Proof.
Qed.
Lemma Henkin_ax_wf' th A c :
th.(gen_fun_symbs) c = Some 0 ->
th.(funsymbs) c = Some 0 ->
IsTheorem th (A) ->
forall B, Henkin_axiom th.(IsAxiom) A c B -> Wf th B.
Proof.
......@@ -506,7 +506,7 @@ Proof.
Qed.
Definition Henkin_halfext th A c
(E : th.(gen_fun_symbs) c = Some 0)
(E : th.(funsymbs) c = Some 0)
(Thm : IsTheorem th (A))
:=
{| sign := th;
......@@ -521,7 +521,7 @@ Definition Henkin_halfext th A c
of [th]. *)
Lemma Henkin_halfext_consext th A c
(E : th.(gen_fun_symbs) c = Some 0)
(E : th.(funsymbs) c = Some 0)
(Thm : IsTheorem th (A))
(AW : AxiomsWithout th c)
(CK : check (delcst th c) A = true) :
......@@ -536,7 +536,7 @@ Proof.
split; cbn; auto using signext_refl.
intros B HB. apply ax_thm. cbn. now left.
- intros T.
assert (E' : gen_fun_symbs (delcst_th th c AW) c = None).
assert (E' : funsymbs (delcst_th th c AW) c = None).
{ cbn. now rewrite eqb_refl. }
assert (Thm' : IsTheorem (delcst_th th c AW) (A)).
{ apply delcst_consext; split; auto. cbn.
......@@ -555,7 +555,7 @@ Qed.
(** At least we preserve consistency *)
Lemma Henkin_halfext_consistent th A c
(E : th.(gen_fun_symbs) c = Some 0)
(E : th.(funsymbs) c = Some 0)
(Thm : IsTheorem th (A))
(AW : AxiomsWithout th c)
(CK : check (delcst th c) A = true) :
......@@ -576,7 +576,7 @@ Qed.
Definition WitnessSaturated th :=
forall A, IsTheorem th ( A) ->
exists c,
th.(gen_fun_symbs) c = Some 0 /\
th.(funsymbs) c = Some 0 /\
IsTheorem th (bsubst 0 (Cst c) A).
(** Actually, we won't bother considering only existential
......@@ -593,7 +593,7 @@ Definition WitnessSaturated th :=
Definition WitnessSuperSaturated th :=
forall A, Wf th ( A) ->
exists c,
th.(gen_fun_symbs) c = Some 0 /\
th.(funsymbs) c = Some 0 /\
IsTheorem th (( A) -> bsubst 0 (Cst c) A).
(** Super-saturated implies saturated *)
......@@ -624,10 +624,10 @@ Qed.
Moreover, we should be able to recognize these names
(for building the new signature). *)
Record NewCsts (sign : gen_signature) :=
Record NewCsts (sign : signature) :=
{ csts :> nat -> string;
csts_inj : forall n m, csts n = csts m -> n = m;
csts_ok : forall n, sign.(gen_fun_symbs) (csts n) = None;
csts_ok : forall n, sign.(funsymbs) (csts n) = None;
test : string -> bool;
test_ok : forall s, test s = true <-> exists n, csts n = s }.
......@@ -715,7 +715,7 @@ Proof.
fix IH 1. destruct t as [ | | f l]; cbn; auto.
intros NI.
case eqbspec; [varsdec|].
intros _. destruct gen_fun_symbs; auto.
intros _. destruct funsymbs; auto.
case eqb; auto.
revert l NI.
fix IH' 1. destruct l as [ |t l]; cbn; auto.
......@@ -728,7 +728,7 @@ Lemma form_funs_ok sign f c :
check (delcst sign c) f = check sign f.
Proof.
induction f; cbn; auto.
- intros NI. destruct gen_pred_symbs; auto.
- intros NI. destruct predsymbs; auto.
case eqb; auto.
revert l NI.
induction l as [|t l]; cbn; auto.
......@@ -925,7 +925,7 @@ Proof.
destruct (fresh_cst_in_cands used nc) as (m,Hm).
assert (NI := fresh_cst_ok used nc (csts_inj _ nc)).
set (c := fresh_cst used nc) in *.
assert (E : (HenkinSeq th nc n).(gen_fun_symbs) c = Some 0).
assert (E : (HenkinSeq th nc n).(funsymbs) c = Some 0).
{ simpl. replace (test th nc c) with true; auto.
symmetry. rewrite Hm, test_ok. now exists m. }
assert (Thm : IsTheorem (HenkinSeq th nc n)
......
......@@ -21,12 +21,12 @@ Definition get_arity {A B} (o : option { n:nat & arity_fun A n B}) :=
Definition modfuns M := string -> option { n:nat & arity_fun M n M }.
Definition modpreds M := string -> option { n:nat & arity_fun M n Prop }.
Record PreModel (M:Type)(sign:gen_signature) :=
Record PreModel (M:Type)(sign:signature) :=
{ someone : M; (* M is non-empty *)
funs : modfuns M;
preds : modpreds M;
funsOk : forall s, sign.(gen_fun_symbs) s = get_arity (funs s);
predsOk : forall s, sign.(gen_pred_symbs) s = get_arity (preds s)
funsOk : forall s, sign.(funsymbs) s = get_arity (funs s);
predsOk : forall s, sign.(predsymbs) s = get_arity (preds s)
}.
(** A premodel is also called a Σ-structure. For a complete model
......@@ -37,7 +37,7 @@ Record PreModel (M:Type)(sign:gen_signature) :=
anywhere in this file (yet?) !! *)
Section PREMODEL.
Variable sign : gen_signature.
Variable sign : signature.
Variable M:Type.
Variable Mo : PreModel M sign.
......
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