Commit 57b00fc1 authored by Pierre Letouzey's avatar Pierre Letouzey
Browse files

travail (en cours) sur substitution et alpha en version nommé

parent 43a85376
This diff is collapsed.
......@@ -6,7 +6,6 @@ Require Nam Mix.
Import ListNotations.
Local Open Scope bool_scope.
Local Open Scope lazy_bool_scope.
Local Open Scope string_scope.
Local Open Scope eqb_scope.
Fixpoint nam2mix_term stack t :=
......@@ -301,7 +300,7 @@ End Nam2MixProof.
Fixpoint mix2nam_term stack t :=
match t with
| Mix.FVar v => Nam.Var v
| Mix.BVar n => Nam.Var (List.nth n stack "")
| Mix.BVar n => Nam.Var (List.nth n stack EmptyString)
| Mix.Fun f args =>
Nam.Fun f (List.map (mix2nam_term stack) args)
end.
......@@ -452,6 +451,34 @@ Proof.
- intros H. symmetry. exact (not_true_is_false _ H).
Qed.
(* TODO
(** Equivalence between form_subst and form_subst',
between alpha_equiv and alpha_equiv' *)
Lemma alpha_equiv_genalt sub1 f1 sub2 f2 h :
Nam.form_height f1 < h -> Nam.form_height f2 < h ->
Nam.alpha_equiv_gen sub1 f1 sub2 f2 =
Nam.alpha_equiv_h (Nam.form_substs sub1 f1) (Nam.form_substs sub2 f2) h.
Proof.
revert h f1 f2 sub1 sub2.
induction h.
- inversion 1.
- destruct f1; destruct f2; intros sub1 sub2 Hf1 Hf2; auto;
try (cbn; now destruct negb).
+ cbn. apply IHh; auto with arith.
+ cbn in *. case eqb; auto. rewrite <-!andb_lazy_alt.
f_equal; apply IHh; omega with *.
+ simpl Nam.alpha_equiv_gen.
set (z1 := fresh_var _).
simpl Nam.form_substs.
set (cond1 := negb _).
set (cond2 := negb _).
*)
(** Contexts *)
Definition nam2mix_ctx (c:Nam.context) : Mix.context :=
......@@ -561,6 +588,116 @@ Proof.
now destruct a.
Qed.
(*
Lemma subst_equiv (sub:Nam.subst) f v z q :
~Vars.In z (Vars.union (Nam.allvars f) (Nam.subvars 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) 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) 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) =
......@@ -665,4 +802,5 @@ Proof.
- repeat (break; cbn; auto).
case eqb; simpl; auto.
now rewrite <- nam2mix_seq_eqb.
Admitted.
\ No newline at end of file
Admitted.
*)
\ No newline at end of file
......@@ -804,8 +804,8 @@ merlin-hook::
debug:
$(foreach v,\
$(sort $(filter-out $(INITIAL_VARS) INITIAL_VARS,\
$(.VARIABLES))),\
$(info $(v) = $($(v))))
$(.VARIABLES))),\
$(info $(v) = $($(v))))
.PHONY: debug
.DEFAULT_GOAL := all
......@@ -8,13 +8,13 @@
# #
###############################################################################
COQMF_VFILES = AsciiOrder.v StringOrder.v StringUtils.v Utils.v Defs.v Nam.v Mix.v Proofs.v Equiv.v Meta.v ToCoq.v
COQMF_MLIFILES =
COQMF_MLFILES =
COQMF_ML4FILES =
COQMF_MLPACKFILES =
COQMF_MLLIBFILES =
COQMF_CMDLINE_VFILES =
COQMF_VFILES = AsciiOrder.v StringOrder.v StringUtils.v Utils.v Defs.v Nam.v Alpha.v Mix.v Proofs.v Equiv.v Meta.v ToCoq.v
COQMF_MLIFILES =
COQMF_MLFILES =
COQMF_ML4FILES =
COQMF_MLPACKFILES =
COQMF_MLLIBFILES =
COQMF_CMDLINE_VFILES =
###############################################################################
# #
......@@ -26,7 +26,7 @@ COQMF_OCAMLLIBS = -I .
COQMF_SRC_SUBDIRS = .
COQMF_COQLIBS = -I . -R . NatDed
COQMF_COQLIBS_NOML = -R . NatDed
COQMF_CMDLINE_COQLIBS =
COQMF_CMDLINE_COQLIBS =
###############################################################################
# #
......@@ -53,5 +53,5 @@ COQMF_WINDRIVE=/home/letouzey/V8
# #
###############################################################################
COQMF_OTHERFLAGS =
COQMF_OTHERFLAGS =
COQMF_INSTALLCOQDOCROOT = NatDed
......@@ -241,25 +241,25 @@ Definition suboutvars (sub : subst) :=
Definition subvars (sub : subst) :=
Vars.union (subinvars sub) (suboutvars sub).
Fixpoint formula_substs sub f :=
Fixpoint form_substs sub f :=
match f with
| True | False => f
| Pred p args => Pred p (List.map (term_substs sub) args)
| Not f => Not (formula_substs sub f)
| Op o f f' => Op o (formula_substs sub f) (formula_substs sub f')
| Not f => Not (form_substs sub f)
| Op o f f' => Op o (form_substs sub f) (form_substs sub f')
| Quant q v f' =>
let sub := List.filter (fun '(x,_) => x =? v) sub in
let out_vars := suboutvars sub in
if negb (Vars.mem v out_vars) then
Quant q v (formula_substs sub f')
Quant q v (form_substs sub f')
else
(* variable capture : we change v into a fresh variable first *)
let z := fresh_var (vars_unions [allvars f; out_vars; subinvars sub])
in
Quant q z (formula_substs ((v,Var z)::sub) f')
Quant q z (form_substs ((v,Var z)::sub) f')
end.
Definition formula_subst v t f := formula_substs [(v,t)] f.
Definition form_subst v t f := form_substs [(v,t)] f.
Instance term_eqb : Eqb term :=
fix term_eqb t1 t2 :=
......@@ -317,7 +317,7 @@ Definition allvars_ctx Γ := vars_unionmap allvars Γ.
Definition freevars_ctx Γ := vars_unionmap freevars Γ.
Definition ctx_subst v t Γ := List.map (formula_subst v t) Γ.
Definition ctx_subst v t Γ := List.map (form_subst v t) Γ.
(** Sequent *)
......@@ -339,7 +339,7 @@ Definition freevars_seq '(Γ ⊢ A) :=
Vars.union (freevars_ctx Γ) (freevars A).
Definition seq_subst v t '(Γ ⊢ A) :=
(ctx_subst v t Γ, formula_subst v t A).
(ctx_subst v t Γ, form_subst v t A).
Instance seq_eqb : Eqb sequent :=
fun '(Γ1 ⊢ A1) '(Γ2 ⊢ A2) => (Γ1 =? Γ2) &&& (A1 =? A2).
......@@ -385,9 +385,9 @@ Definition valid_deriv_step logic '(Rule r s ld) :=
| All_i x, s, [Γ ⊢ A] =>
(s =? (Γ ⊢ ∀x,A)) &&& negb (Vars.mem x (freevars_ctx Γ))
| All_e t, (Γ ⊢ B), [Γ'⊢ ∀x,A] =>
(Γ =? Γ') &&& (B =? formula_subst x t A)
(Γ =? Γ') &&& (B =? form_subst x t A)
| Ex_i t, (Γ ⊢ ∃x,A), [Γ'⊢B] =>
(Γ =? Γ') &&& (B =? formula_subst x t A)
(Γ =? Γ') &&& (B =? form_subst x t A)
| Ex_e x, s, [s1; A::Γ ⊢ B] =>
(s =? (Γ ⊢ B)) &&& (s1 =? (Γ ⊢ ∃x, A)) &&&
negb (Vars.mem x (freevars_seq s))
......
......@@ -7,6 +7,7 @@ StringUtils.v
Utils.v
Defs.v
Nam.v
Alpha.v
Mix.v
Proofs.v
Equiv.v
......
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