Commit 6f03c0af authored by Pierre Letouzey's avatar Pierre Letouzey
Browse files

reorganisation, modules de nommages, ...

parent cf484589
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
(** Conversion from Named derivations to Locally Nameless derivations *)
Require Import RelationClasses Arith Omega Defs Proofs Equiv Alpha Alpha2.
Require Nam Mix.
Import ListNotations.
Import Nam Nam.Form.
Local Open Scope bool_scope.
Local Open Scope lazy_bool_scope.
Local Open Scope eqb_scope.
(** Contexts *)
Definition nam2mix_ctx (c:Nam.context) : Mix.context :=
List.map (nam2mix []) c.
Definition mix2nam_ctx (c:Mix.context) : Nam.context :=
List.map (mix2nam []) c.
Lemma nam2mix_ctx_eqb (c c' : Nam.context) :
(nam2mix_ctx c =? nam2mix_ctx c') = (c =? c').
Proof.
revert c'.
induction c; destruct c'; cbn; auto.
rewrite nam2mix_eqb. case eqb; auto.
Qed.
(** Sequents *)
Definition nam2mix_seq '(Nam.Seq c f) : Mix.sequent :=
Mix.Seq (nam2mix_ctx c) (nam2mix [] f).
Definition mix2nam_seq '(Mix.Seq c f) : Nam.sequent :=
Nam.Seq (mix2nam_ctx c) (mix2nam [] f).
Lemma nam2mix_seq_eqb (s s' : Nam.sequent) :
(nam2mix_seq s =? nam2mix_seq s') = (s =? s').
Proof.
destruct s as (c,f), s' as (c',f'); cbn.
now rewrite nam2mix_ctx_eqb, nam2mix_eqb.
Qed.
(** Rule kinds *)
Definition nam2mix_rule r :=
match r with
| Nam.Ax => Mix.Ax
| Nam.Tr_i => Mix.Tr_i
| Nam.Fa_e => Mix.Fa_e
| Nam.Not_i => Mix.Not_i
| Nam.Not_e => Mix.Not_e
| Nam.And_i => Mix.And_i
| Nam.And_e1 => Mix.And_e1
| Nam.And_e2 => Mix.And_e2
| Nam.Or_i1 => Mix.Or_i1
| Nam.Or_i2 => Mix.Or_i2
| Nam.Or_e => Mix.Or_e
| Nam.Imp_i => Mix.Imp_i
| Nam.Imp_e => Mix.Imp_e
| Nam.All_i v => Mix.All_i v
| Nam.All_e t => Mix.All_e (nam2mix_term [] t)
| Nam.Ex_i t => Mix.Ex_i (nam2mix_term [] t)
| Nam.Ex_e v => Mix.Ex_e v
| Nam.Absu => Mix.Absu
end.
Definition mix2nam_rule r :=
match r with
| Mix.Ax => Nam.Ax
| Mix.Tr_i => Nam.Tr_i
| Mix.Fa_e => Nam.Fa_e
| Mix.Not_i => Nam.Not_i
| Mix.Not_e => Nam.Not_e
| Mix.And_i => Nam.And_i
| Mix.And_e1 => Nam.And_e1
| Mix.And_e2 => Nam.And_e2
| Mix.Or_i1 => Nam.Or_i1
| Mix.Or_i2 => Nam.Or_i2
| Mix.Or_e => Nam.Or_e
| Mix.Imp_i => Nam.Imp_i
| Mix.Imp_e => Nam.Imp_e
| Mix.All_i v => Nam.All_i v
| Mix.All_e t => Nam.All_e (mix2nam_term [] t)
| Mix.Ex_i t => Nam.Ex_i (mix2nam_term [] t)
| Mix.Ex_e v => Nam.Ex_e v
| Mix.Absu => Nam.Absu
end.
(** Derivations *)
Fixpoint nam2mix_deriv (d:Nam.derivation) :=
let '(Nam.Rule r s ds) := d in
Mix.Rule
(nam2mix_rule r)
(nam2mix_seq s)
(List.map nam2mix_deriv ds).
Fixpoint mix2nam_deriv (d:Mix.derivation) :=
let '(Mix.Rule r s ds) := d in
Nam.Rule
(mix2nam_rule r)
(mix2nam_seq s)
(List.map mix2nam_deriv ds).
Ltac break :=
rewrite <- ?andb_lazy_alt;
match goal with
| |- _ = match ?f ?x with _ => _ end => destruct x
| |- _ = match ?x with _ => _ end => destruct x
| |- match ?f (?g ?x) with _ => _ end = _ => destruct x
| |- match ?f ?x with _ => _ end = _ => destruct x
| |- match ?x with _ => _ end = _ => destruct x
end.
Lemma lazy_andb_false (a:bool) : a &&& false = false.
Proof.
now destruct a.
Qed.
(*
Lemma subst_equiv (sub:Nam.Subst.st) f v z q :
~Vars.In z (Vars.union (Nam.allvars f) (Nam.Subst.vars sub)) ->
Nam.AlphaEq
(Nam.formula_substs sub (Nam.Quant q v f))
(Nam.Quant q z (Nam.formula_substs ((v,Nam.Var z)::sub) f)).
Proof.
unfold Nam.AlphaEq, Nam.alpha_equiv.
intros NI.
cbn -[fresh_var Vars.union].
set (cond := negb _).
destruct cond eqn:Hcond.
- cbn -[fresh_var Vars.union].
set (z' := fresh_var _).
rewrite eqb_refl.
*)
(*
Lemma nam2mix_term_subts
forall a : Nam.term,
In a l ->
nam2mix_term (map snd subvar)
(Nam.term_substs
(map (fun '(v0, w) => (v0, Nam.Var w)) subvar ++
[(v, t)]) a) =
Mix.bsubst n (nam2mix_term [] t)
(nam2mix_term (map fst subvar ++ [v]) a)
*)
Definition subvar2sub (subvar:list (variable*variable)) :=
List.map (fun '(v,w) => (v,Nam.Var w)) subvar.
(*TODO
Lemma nam2mix_term_substs_ext
(vars:list variable)
(subvar subvar' : list (variable*variable))
(sub : Nam.Subst.st) t :
(forall v, list_assoc_dft v subvar v = list_assoc_dft v subvar' v) ->
nam2mix_term (List.map (fun v => list_assoc_dft v subvar v) vars)
(Nam.term_substs (subvar2sub subvar ++ sub) t) =
nam2mix_term (List.map (fun v => list_assoc_dft v subvar' v) vars)
(Nam.term_substs (subvar2sub subvar' ++ sub) t).
Proof.
induction t as [v|f l IH] using Nam.term_ind'; intros E.
- cbn.
Lemma nam2mix_substs_ext
(vars:list variable)
(subvar subvar' : list (variable*variable))
(sub : Nam.Subst.st) f :
(forall v, subvar v = subvar') ->
nam2mix (List.map (fun v => list_assoc_dft v subvar v) vars)
(Nam.formula_substs (subvar2sub subvar ++ sub) f) =
nam2mix (List.map (fun v => list_assoc_dft v subvar' v) vars)
(Nam.formula_substs (subvar2sub subvar' ++ sub) f).
Proof.
revert vars subvar subvar' sub.
induction f; intros var subvar subvar' sub.
- now cbn.
- now cbn.
- cbn. f_equal. rewrite !map_map. apply map_ext.
Definition InvSubVar v t f subvar :=
~In v (List.map fst subvar) /\ ~In v (List.map snd subvar) /\
(forall w, In w (List.map snd subvar) ->
~Vars.In w (Vars.union (Nam.term_vars t) (Nam.allvars f))).
Lemma nam2mix_substs n (subvar: list (variable*variable)) v t f :
InvSubVar v t f subvar ->
n = List.length subvar ->
let sub := List.map (fun '(v,w) => (v,Nam.Var w)) subvar
in
nam2mix (List.map snd subvar) (Nam.formula_substs (sub++[(v,t)]) f) =
Mix.bsubst n (nam2mix_term [] t)
(nam2mix ((List.map fst subvar) ++ [v]) f).
Proof.
revert n subvar.
induction f; cbn -[fresh_var Vars.union]; trivial.
- intros.
f_equal.
rewrite !map_map.
apply map_ext_in.
admit.
- intros. f_equal; auto.
- intros. f_equal; auto. admit. admit.
- intros.
set (cond := negb _).
destruct cond eqn:Hcond.
+ cbn. f_equal.
set (sub := filter _ _) in *.
specialize (IHf (S n) ((v0,v0)::subvar)).
cbn in IHf. rewrite <- IHf; auto.
case (eqbspec v v0).
* intros <-.
assert (sub = map (fun '(v, w) => (v, Nam.Var w)) subvar).
{ admit. }
*
admit.
+ set (sub := filter _ _) in *.
set (z := fresh_var _).
cbn -[z].
f_equal.
specialize (IHf (S n) ((v0,z)::subvar)).
cbn in IHf. rewrite <- IHf; auto.
admit.
Lemma nam2mix_subst v t f :
nam2mix [] (Nam.formula_subst v t f) =
Mix.bsubst 0 (nam2mix_term [] t) (nam2mix [v] f).
Proof.
Admitted. (* preuve ??? *)
Lemma nam2mix_deriv_valid_step logic (d:Nam.derivation) :
Mix.valid_deriv_step logic (nam2mix_deriv d) =
Nam.valid_deriv_step logic d.
Proof.
destruct d as [[ ] s ds]; cbn.
- repeat (break; cbn; auto).
unfold nam2mix_ctx.
induction c as [|A c IH]; cbn; auto.
rewrite <- nam2mix_eqb.
case eqbspec; auto.
- repeat (break; cbn; auto).
- repeat (break; cbn; auto).
rewrite <- !nam2mix_seq_eqb. now destruct d.
- repeat (break; cbn; auto).
rewrite <- !nam2mix_seq_eqb. now destruct d.
- repeat (break; cbn; auto).
now rewrite nam2mix_eqb, !nam2mix_ctx_eqb.
- repeat (break; cbn; auto).
rewrite <- !nam2mix_seq_eqb. now destruct d, d0.
- repeat (break; cbn; auto).
now rewrite <- !nam2mix_seq_eqb.
- repeat (break; cbn; auto).
now rewrite <- !nam2mix_seq_eqb.
- repeat (break; cbn; auto).
rewrite <- !nam2mix_seq_eqb. now destruct d.
- repeat (break; cbn; auto).
rewrite <- !nam2mix_seq_eqb. now destruct d.
- repeat (break; cbn; auto).
rewrite <- nam2mix_ctx_eqb, <- !nam2mix_seq_eqb.
now destruct d, d0.
- repeat (break; cbn; auto).
rewrite <- nam2mix_seq_eqb. now destruct d.
- repeat (break; cbn; auto).
rewrite <- !nam2mix_seq_eqb. now destruct d.
- repeat (break; cbn - [Nam.alpha_equiv]; auto);
rewrite ?andb_false_r; auto.
rewrite <- nam2mix_ctx_eqb.
case eqbspec; auto. intro Ec. simpl.
rewrite <- nam2mix_eqb. cbn.
apply eq_true_iff_eq. simpl.
rewrite !andb_true_iff.
rewrite !negb_true_iff, <- !not_true_iff_false.
rewrite !Vars.mem_spec.
rewrite !eqb_eq.
split; intros (U,V); split.
+ change (Mix.FVar x) with (nam2mix_term [] (Nam.Var x)) in U.
rewrite <- nam2mix_subst in U.
(* f est f0 avec des x à la place des v, donc credible *)
admit.
+ (* faut montrer que c equiv c0 -> memes variables libres *)
admit.
+ rewrite U.
change (Mix.FVar x) with (nam2mix_term [] (Nam.Var x)).
rewrite <- nam2mix_subst.
(* TODO:
alpha_equiv (Nam.formula_subst x (Nam.Var x) f) f
*)
admit.
+ (* - memes variables libres dans contextes equivs
- nam2mix [x] f0 n'a pas x comme variable libre... *)
admit.
- repeat (break; cbn; auto).
rewrite !nam2mix_ctx_eqb. case eqb; simpl; auto.
rewrite <- nam2mix_eqb.
now rewrite <- nam2mix_subst.
- repeat (break; cbn; auto).
rewrite !nam2mix_ctx_eqb. case eqb; simpl; auto.
rewrite <- nam2mix_eqb.
now rewrite <- nam2mix_subst.
- repeat (break; cbn - [Nam.alpha_equiv]; auto);
rewrite ?andb_false_r; auto.
rewrite <- nam2mix_seq_eqb, <- nam2mix_eqb. cbn.
apply eq_true_iff_eq.
rewrite !andb_true_iff.
rewrite !negb_true_iff, <- !not_true_iff_false.
rewrite !Vars.mem_spec.
rewrite !eqb_eq.
split.
+ intros (((U,V),W),X); repeat split.
* rewrite <-V in U; exact U.
* rewrite <- nam2mix_ctx_eqb. now apply eqb_eq.
* admit. (* bsubst... *)
* destruct s. cbn in *. injection U as U U'. admit.
+ intros ((U,(V,W)),Z); repeat split.
* rewrite <- nam2mix_ctx_eqb in V. apply eqb_eq in V.
rewrite U. f_equal; auto.
* rewrite <- nam2mix_ctx_eqb in V. apply eqb_eq in V.
rewrite V. auto.
* rewrite W.
change (Mix.FVar x) with (nam2mix_term [] (Nam.Var x)).
rewrite <- nam2mix_subst.
admit.
* destruct s. cbn in *. injection U as U U'. admit.
- repeat (break; cbn; auto).
case eqb; simpl; auto.
now rewrite <- nam2mix_seq_eqb.
Admitted.
*)
......@@ -8,7 +8,7 @@
# #
###############################################################################
COQMF_VFILES = AsciiOrder.v StringOrder.v StringUtils.v Utils.v Defs.v Nam.v Alpha.v AlphaAlt.v Mix.v Proofs.v Equiv.v Meta.v ToCoq.v
COQMF_VFILES = AsciiOrder.v StringOrder.v StringUtils.v Utils.v Defs.v Nam.v Mix.v Proofs.v Alpha.v Equiv.v Alpha2.v Equiv2.v Meta.v ToCoq.v
COQMF_MLIFILES =
COQMF_MLFILES =
COQMF_ML4FILES =
......
......@@ -34,6 +34,16 @@ Definition Cst (f:function_symbol) := Fun f [].
Definition peano_term_example :=
Fun "+" [Fun "S" [Cst "O"]; Var "x"].
(** Simultaneous substitution of many variables by terms.
The bindings of this substitution will be handled in parallel,
not sequentially. In particular, the variables introduced
by a binding aren't modified by other bindings.
If the substitution contains several bindings of the same
variable, the leftmost binding wins (cf. [list_assoc]). *)
Definition substitution := list (variable * term).
(** In the case of Peano, numbers are coded as iterated successors of zero *)
Fixpoint nat2term n :=
......@@ -49,18 +59,20 @@ Fixpoint term2nat t :=
| _ => None
end.
Definition print_tuple {A} (pr: A -> string) (l : list A) :=
"(" ++ String.concat "," (List.map pr l) ++ ")".
Definition is_binop s := list_mem s ["+";"*"].
Module Term.
(** Term printing
NB: + and * are printed in infix position, S(S(...O())) is printed as
the corresponding number.
*)
Definition print_tuple {A} (pr: A -> string) (l : list A) :=
"(" ++ String.concat "," (List.map pr l) ++ ")".
Definition is_binop s := list_mem s ["+";"*"].
Fixpoint print_term t :=
Fixpoint print t :=
match term2nat t with
| Some n => DecimalString.NilZero.string_of_uint (Nat.to_uint n)
| None =>
......@@ -70,14 +82,14 @@ Fixpoint print_term t :=
if is_binop f then
match args with
| [t1;t2] =>
"(" ++ print_term t1 ++ ")" ++ f ++ "(" ++ print_term t2 ++ ")"
| _ => f ++ print_tuple print_term args
"(" ++ print t1 ++ ")" ++ f ++ "(" ++ print t2 ++ ")"
| _ => f ++ print_tuple print args
end
else f ++ print_tuple print_term args
else f ++ print_tuple print args
end
end.
Compute print_term peano_term_example.
Compute Term.print peano_term_example.
(** Term parsing *)
......@@ -92,41 +104,67 @@ Compute print_term peano_term_example.
iff it only refer to known function symbols and use them
with the correct arity. *)
Fixpoint check_term (sign : gen_signature) t :=
Fixpoint check (sign : gen_signature) t :=
match t with
| Var _ => true
| Fun f args =>
match sign.(gen_fun_symbs) f with
| None => false
| Some ar =>
(List.length args =? ar) &&& (List.forallb (check_term sign) args)
(List.length args =? ar) &&& (List.forallb (check sign) args)
end
end.
Compute check_term (generalize_signature peano_sign) peano_term_example.
Compute Term.check (generalize_signature peano_sign) peano_term_example.
(** The set of variables occurring in a term *)
Fixpoint term_vars t :=
Fixpoint vars t :=
match t with
| Var v => Vars.singleton v
| Fun _ args => vars_unionmap term_vars args
| Fun _ args => vars_unionmap vars args
end.
(** Simultaneous substitution of many variables in a term. *)
Definition subst := list (variable * term).
(** Simultaneous substitution (see type [substs] above) *)
Fixpoint term_substs (sub:subst) t :=
Fixpoint substs (sub:substitution) t :=
match t with
| Var v => list_assoc_dft v sub t
| Fun f args => Fun f (List.map (term_substs sub) args)
| Fun f args => Fun f (List.map (substs sub) args)
end.
(** Substitution of a variable in a term :
in [t], [v] is replaced by [u] *)
Definition term_subst v u t := term_substs [(v,u)] t.
Definition subst v u t := substs [(v,u)] t.
(** Boolean equality over terms *)
Instance eqb : Eqb term :=
fix term_eqb t1 t2 :=
match t1, t2 with
| Var v1, Var v2 => v1 =? v2
| Fun f1 args1, Fun f2 args2 =>
(f1 =? f2) &&& (list_forallb2 term_eqb args1 args2)
| _, _ => false
end.
End Term.
Module Subst.
Definition t := substitution.
Definition invars (sub : substitution) :=
List.fold_right (fun p vs => Vars.add (fst p) vs) Vars.empty sub.
Definition outvars (sub : substitution) :=
vars_unionmap (fun '(_,t) => Term.vars t) sub.
Definition vars (sub : substitution) :=
Vars.union (invars sub) (outvars sub).
End Subst.
(** Formulas *)
......@@ -143,38 +181,6 @@ Inductive formula :=
Definition Iff a b := Op And (Op Impl a b) (Op Impl b a).
(** Formula printing *)
(** Notes:
- We use { } for putting formulas into parenthesis, instead of ( ).
*)
Definition is_infix_pred s := list_mem s ["=";"∈"].
(* TODO affichage court du <-> *)
Fixpoint print_formula f :=
match f with
| True => "True"
| False => "False"
| Pred p args =>
if is_infix_pred p then
match args with
| [t1;t2] =>
"(" ++ print_term t1 ++ ")" ++ p ++ "(" ++ print_term t2 ++ ")"
| _ => p ++ print_tuple print_term args
end
else p ++ print_tuple print_term args
| Not f => "~{" ++ print_formula f ++ "}"
| Op o f f' =>
"{" ++ print_formula f ++ "}" ++ pr_op o ++ "{" ++ print_formula f' ++ "}"
| Quant q v f => pr_quant q ++ v ++ ",{" ++ print_formula f ++ "}"
end.
Compute print_formula (Quant Ex "x" True).
Compute print_formula (Iff True False).
(* TODO: Formula parsing *)
(* Instead : Coq notations *)
......@@ -197,20 +203,53 @@ Notation "∃ x , A" := (Quant Ex x A)
Definition test_form := (∃ "x", True <-> Pred "p" [Var "x";#3])%form.
(** Formula printing *)
(** Notes:
- We use { } for putting formulas into parenthesis, instead of ( ).
*)
Definition is_infix_pred s := list_mem s ["=";""].
Module Form.
(* TODO affichage court du <-> *)
Fixpoint print f :=
match f with
| True => "True"
| False => "False"
| Pred p args =>
if is_infix_pred p then
match args with
| [t1;t2] =>
"(" ++ Term.print t1 ++ ")" ++ p ++ "(" ++ Term.print t2 ++ ")"
| _ => p ++ print_tuple Term.print args
end
else p ++ print_tuple Term.print args
| Not f => "~{" ++ print f ++ "}"
| Op o f f' =>
"{" ++ print f ++ "}" ++ pr_op o ++ "{" ++ print f' ++ "}"
| Quant q v f => pr_quant q ++ v ++ ",{" ++ print f ++ "}"
end.
Compute Form.print (Quant Ex "x" True).
Compute Form.print (Iff True False).
(** Utilities about formula *)
Fixpoint check_formula (sign : gen_signature) f :=
Fixpoint check (sign : gen_signature) f :=
match f with
| True | False => true
| Not f => check_formula sign f
| Op _ f f' => check_formula sign f &&& check_formula sign f'
| Quant _ v f => check_formula sign f
| 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
| None => false
| Some ar =>
(List.length args =? ar) &&& (List.forallb (check_term sign) args)
(List.length args =? ar) &&& (List.forallb (Term.check sign) args)
end
end.
......@@ -220,7 +259,7 @@ Fixpoint allvars f :=
| Not f => allvars f
| Op _ f f' => Vars.union (allvars f) (allvars f')
| Quant _ v f => Vars.add v (allvars f)
| Pred _ args => vars_unionmap term_vars args
| Pred _ args => vars_unionmap Term.vars args
end.
Fixpoint freevars f :=
......@@ -229,95 +268,181 @@ Fixpoint freevars f :=
| Not f => freevars f
| Op _ f f' => Vars.union (freevars f) (freevars f')
| Quant _ v f => Vars.remove v (freevars f)
| Pred _ args => vars_unionmap term_vars args
| Pred _ args => vars_unionmap Term.vars args
end.
Definition subinvars (sub : subst) :=
List.fold_right (fun p vs => Vars.add (fst p) vs) Vars.empty sub.
Definition suboutvars (sub : subst) :=
vars_unionmap (fun '(_,t) => term_vars t) sub.