Commit fdf21d42 authored by Pierre Letouzey's avatar Pierre Letouzey
Browse files

Equiv2, suite

parent 4b365452
......@@ -333,6 +333,8 @@ Proof.
auto.
Qed.
(* TODO: reciproque au précédent ? *)
(* Unused for the moment *)
Lemma nam2mix0_partialsubst x u f :
IsSimple x u f ->
......@@ -342,19 +344,19 @@ Proof.
apply nam2mix_partialsubst; auto.
Qed.
Lemma term_subst_bsubst stk (x z:variable) t :
Lemma term_subst_bsubst stk (x:variable) u t :
~In x stk ->
~In z stk ->
~Vars.In z (Term.vars t) ->
nam2mix_term stk (Term.subst x (Var z) t) =
Mix.bsubst (length stk) (Mix.FVar z) (nam2mix_term (stk++[x]) t).
(forall v, In v stk -> ~Vars.In v (Term.vars u)) ->
nam2mix_term stk (Term.subst x u t) =
Mix.bsubst (length stk) (nam2mix_term [] u)
(nam2mix_term (stk++[x]) t).
Proof.
induction t as [v|f l IH] using term_ind'; intros X Z1 Z2; cbn in *.
induction t as [v|f l IH] using term_ind'; intros X U; cbn in *.
- case eqbspec.
+ intros ->. cbn.
rewrite <-list_index_notin in Z1. rewrite Z1.
+ intros ->.
rewrite list_index_app_r; auto. cbn. rewrite eqb_refl. cbn.
rewrite Nat.add_0_r. now rewrite eqb_refl.
rewrite Nat.add_0_r. rewrite eqb_refl.
now apply nam2mix_term_nostack.
+ intros NE. cbn.
rewrite list_index_app_l' by (simpl; intuition).
destruct (list_index v stk) eqn:E; cbn; auto.
......@@ -363,23 +365,22 @@ Proof.
- f_equal; clear f.
rewrite !map_map.
apply map_ext_in. intros t Ht. apply IH; auto.
contradict Z2. rewrite vars_unionmap_in. now exists t.
Qed.
Lemma partialsubst_bsubst stk x z f :
Lemma partialsubst_bsubst stk x u f :
~In x stk ->
~In z stk ->
~Vars.In z (allvars f) ->
nam2mix stk (partialsubst x (Var z) f) =
Mix.bsubst (length stk) (Mix.FVar z) (nam2mix (stk++[x]) f).
(forall v, In v stk -> ~Vars.In v (Term.vars u)) ->
IsSimple x u f ->
nam2mix stk (partialsubst x u f) =
Mix.bsubst (length stk) (nam2mix_term [] u)
(nam2mix (stk++[x]) f).
Proof.
revert stk.
induction f; cbn; intros stk X Z1 Z2; f_equal; auto.
- injection (term_subst_bsubst stk x z (Fun "" l)); auto.
- apply IHf1; auto. varsdec0.
- apply IHf2; auto. varsdec0.
- fold (v =? z)%string. change (v =? z)%string with (v =? z).
case eqbspec; cbn.
induction f; cbn; intros stk X U IS; f_equal; auto.
- injection (term_subst_bsubst stk x u (Fun "" l)); auto.
- destruct IS as (IS1,IS2); auto.
- destruct IS as (IS1,IS2); auto.
- case eqbspec; cbn.
+ intros <-.
change (x::stk++[x]) with ((x::stk)++[x]).
rewrite nam2mix_shadowstack by (simpl; auto).
......@@ -387,16 +388,28 @@ Proof.
apply form_level_bsubst_id.
now rewrite nam2mix_level.
+ intros NE.
destruct IS as [->|(NI,IS)]; [easy|].
rewrite vars_mem_false by varsdec0.
apply IHf; simpl; intuition.
apply IHf; simpl; auto.
intuition.
intros y [<-|Hy]; auto.
Qed.
Lemma partialsubst_bsubst0 x u f :
IsSimple x u f ->
nam2mix [] (partialsubst x u f) =
Mix.bsubst 0 (nam2mix_term [] u) (nam2mix [x] f).
Proof.
apply partialsubst_bsubst; auto.
Qed.
Lemma partialsubst_bsubst0 x z f :
Lemma partialsubst_bsubst0_var x z f :
~Vars.In z (allvars f) ->
nam2mix [] (partialsubst x (Var z) f) =
Mix.bsubst 0 (Mix.FVar z) (nam2mix [x] f).
Proof.
apply partialsubst_bsubst; auto.
intros.
apply (partialsubst_bsubst0 x (Var z)); auto.
Qed.
Lemma nam2mix_rename_iff z v v' f f' :
......@@ -407,7 +420,7 @@ Lemma nam2mix_rename_iff z v v' f f' :
nam2mix [v] f = nam2mix [v'] f'.
Proof.
intros Hz.
rewrite 2 partialsubst_bsubst0 by varsdec.
rewrite 2 partialsubst_bsubst0_var by varsdec.
split.
- intros H. apply bsubst_fresh_inj in H; auto.
rewrite !nam2mix_fvars. cbn. rewrite !freevars_allvars. varsdec.
......@@ -485,6 +498,27 @@ Proof.
apply Subst_subst.
Qed.
Lemma nam2mix_Subst_bsubst0 x u f f' :
Subst x u f f' ->
nam2mix [] f' =
Mix.bsubst 0 (nam2mix_term [] u) (nam2mix [x] f).
Proof.
intros (f0 & EQ & SI).
apply AlphaEq_nam2mix_gen with (stk:=[x]) in EQ.
rewrite EQ.
apply SimpleSubst_carac in SI. destruct SI as (<- & IS).
now apply partialsubst_bsubst0.
Qed.
Lemma nam2mix_alt_subst_bsubst0 x u f :
nam2mix [] (Alt.subst x u f) =
Mix.bsubst 0 (nam2mix_term [] u) (nam2mix [x] f).
Proof.
apply nam2mix_Subst_bsubst0.
apply Subst_subst.
Qed.
Lemma term_substs_ext h h' t :
(forall v, list_assoc_dft v h (Var v) =
list_assoc_dft v h' (Var v)) ->
......
(** Conversion from Named derivations to Locally Nameless derivations *)
Require Import RelationClasses Arith Omega Defs Proofs Equiv Alpha Alpha2.
Require Import RelationClasses Arith Omega Defs Proofs Equiv Alpha Alpha2 Meta.
Require Nam Mix.
Import ListNotations.
Import Nam Nam.Form.
......@@ -129,91 +129,22 @@ Proof.
Qed.
(*
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).
Lemma nam2mix_alt_subst_nop x f :
nam2mix [] (Alt.subst x (Var x) f) = nam2mix [] 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.
rewrite nam2mix_alt_subst. simpl.
unfold Mix.fsubst.
apply form_vmap_id.
intros y Hy. unfold Mix.varsubst.
case eqbspec; intros; subst; auto.
Qed.
Lemma nam2mix_subst v t f :
nam2mix [] (Nam.formula_subst v t f) =
Mix.bsubst 0 (nam2mix_term [] t) (nam2mix [v] f).
Lemma alt_subst_nop x f :
AlphaEq (Alt.subst x (Var x) f) f.
Proof.
Admitted. (* preuve ??? *)
*)
apply nam2mix_canonical.
apply nam2mix_alt_subst_nop.
Qed.
Lemma nam2mix_deriv_valid_step logic (d:Nam.derivation) :
Mix.valid_deriv_step logic (nam2mix_deriv d) =
......@@ -254,41 +185,37 @@ Proof.
rewrite <- nam2mix_ctx_eqb.
case eqbspec; auto. intro Ec. simpl.
rewrite <- nam2mix_eqb. cbn.
apply eq_true_iff_eq. simpl.
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); split.
+ change (Mix.FVar x) with (nam2mix_term [] (Nam.Var x)) in U.
simpl in U.
rewrite <- nam2mix_rename_iff with (z:=x).
rewrite <- partialsubst_bsubst0 in U.
rewrite <- U.
+ change (Mix.FVar x) with (nam2mix_term [] (Var x)) in U.
rewrite <- nam2mix_alt_subst_bsubst0 in U.
(* rewrite <- nam2mix_rename_iff with (z:=x).
rewrite <- U. *)
(* subst x par x donc idem. Mais quid des allvars au lieu de freevars :( ? *)
admit.
admit.
admit.
+ (* faut montrer que c equiv c0 -> memes variables libres *)
rewrite <- nam2mix_ctx_fvars. rewrite <- Ec. varsdec.
+ rewrite U.
change (Mix.FVar x) with (nam2mix_term [] (Nam.Var x)).
simpl.
rewrite <- partialsubst_bsubst0.
(* subst x par x donc idem. Mais quid des allvars au lieu de freevars :( ? *)
admit.
admit.
rewrite <- nam2mix_alt_subst_bsubst0.
symmetry. apply nam2mix_alt_subst_nop.
+ rewrite Ec, U, nam2mix_ctx_fvars.
rewrite nam2mix_fvars. simpl. varsdec.
- repeat (break; cbn; auto).
rewrite !nam2mix_ctx_eqb. case eqb; simpl; auto.
rewrite <- nam2mix_eqb.
admit.
rewrite nam2mix_subst_alt.
now rewrite nam2mix_alt_subst_bsubst0.
- repeat (break; cbn; auto).
rewrite !nam2mix_ctx_eqb. case eqb; simpl; auto.
rewrite <- nam2mix_eqb.
admit.
rewrite nam2mix_subst_alt.
now rewrite nam2mix_alt_subst_bsubst0.
- repeat (break; cbn - [αeq]; auto);
rewrite ?andb_false_r; auto.
rewrite <- nam2mix_seq_eqb, <- nam2mix_eqb. cbn.
......@@ -310,7 +237,8 @@ Proof.
rewrite V. auto.
* rewrite W.
change (Mix.FVar x) with (nam2mix_term [] (Nam.Var x)).
admit.
rewrite <- nam2mix_alt_subst_bsubst0.
symmetry. apply nam2mix_alt_subst_nop.
* destruct s. cbn in *. injection U as U U'. admit.
- repeat (break; cbn; auto).
case eqb; simpl; auto.
......
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