Skip to content

GitLab

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

Equiv: cleanup

parent 8e98bda2
Hide whitespace changes
Inline Side-by-side
Equiv.v
View file @ fb32a921
......@@ -14,6 +14,8 @@ Local Open Scope eqb_scope.
Implicit Types x y z v : variable.
Implicit Types stack stk : list variable.
Local Coercion Var : variable >-> term.
(** From named to locally nameless *)
Fixpoint nam2mix_term stack t :=
......@@ -183,105 +185,55 @@ Proof.
case eqbspec; [intros ->;intuition|auto].
Qed.
(** [nam2mix] and [partialsubst] *)
(** [nam2mix_term] is injective *)
Lemma nam2mix_term_subst stk x u t:
~In x stk ->
nam2mix_term stk (Term.subst x u t) =
Mix.fsubst x (nam2mix_term stk u) (nam2mix_term stk t).
Lemma nam2mix_term_inj t t' :
nam2mix_term [] t = nam2mix_term [] t' <-> t = t'.
Proof.
induction t as [v|f l IH] using term_ind'; intros NI; cbn.
- case eqbspec.
+ intros ->.
rewrite <-list_index_notin in NI. rewrite NI.
cbn. unfold Mix.varsubst. now rewrite eqb_refl.
+ intros NE.
cbn.
destruct (list_index v stk); cbn; auto.
unfold Mix.varsubst. case eqbspec; congruence.
- f_equal; clear f.
rewrite !map_map.
apply map_ext_in. intros t Ht. apply IH; auto.
split; [ | intros <-; auto ].
revert t t'.
fix IH 1. destruct t, t'; cbn; try easy.
- now intros [= <-].
- intros [= <- EQ]. f_equal.
revert l l0 EQ.
fix IH' 1. destruct l, l0; cbn; try easy.
intros [= EQ EQ']. f_equal; auto.
Qed.
Lemma nam2mix_partialsubst stk x u f :
~In x stk ->
(forall v, In v stk -> ~Names.In v (Term.vars u)) ->
IsSimple x u f ->
nam2mix stk (partialsubst x u f) =
Mix.fsubst x (nam2mix_term [] u) (nam2mix stk f).
Proof.
revert stk.
induction f; cbn; intros stk Hx Hu IS; f_equal; auto.
- rewrite <- (nam2mix_term_nostack stk); auto.
injection (nam2mix_term_subst stk x u (Fun "" l)); easy.
- intuition.
- intuition.
- case eqbspec; cbn.
+ intros ->.
unfold Mix.fsubst.
rewrite form_vmap_id; auto.
intros x. rewrite nam2mix_fvars. simpl.
unfold Mix.varsubst.
intros IN.
case eqbspec; auto. intros <-. namedec.
+ intros NE.
destruct IS as [-> | (NI,IS)]; [easy|].
apply IHf; simpl; intuition; subst; eauto.
Qed.
(** [nam2mix_term] and substitutions *)
Lemma nam2mix_term_subst' stk stk' x z t :
Lemma nam2mix_term_rename stk stk' x z t :
~In x stk ->
~In z stk ->
~Names.In z (Term.vars t) ->
nam2mix_term (stk++z::stk') (Term.subst x (Var z) t) =
nam2mix_term (stk++z::stk') (Term.subst x z t) =
nam2mix_term (stk++x::stk') t.
Proof.
induction t as [v|f l IH] using term_ind'; intros Hx Hz NI; cbn in *.
- case eqbspec; cbn.
+ intros ->.
rewrite 2 list_index_app_r by intuition.
simpl; rewrite 2 eqb_refl. simpl; auto.
+ intros NE. destruct (In_dec string_dec v stk).
- case eqbspec; [intros ->|intros NE]; cbn.
+ rewrite 2 list_index_app_r by intuition.
simpl. rewrite 2 eqb_refl. auto.
+ destruct (In_dec string_dec v stk).
* rewrite 2 list_index_app_l; auto.
* rewrite 2 list_index_app_r by auto. simpl.
do 2 case eqbspec; auto. namedec. intuition.
do 2 case eqbspec; intuition.
- f_equal; clear f.
rewrite !map_map.
apply map_ext_in. intros t Ht. apply IH; auto.
eapply unionmap_notin; eauto.
rewrite !map_map. apply map_ext_in. eauto using unionmap_notin.
Qed.
Lemma nam2mix0_partialsubst x u f :
IsSimple x u f ->
nam2mix [] (partialsubst x u f) =
Mix.fsubst x (nam2mix_term [] u) (nam2mix [] f).
Proof.
apply nam2mix_partialsubst; auto.
Qed.
Lemma nam2mix_rename stk stk' x z f :
Lemma nam2mix_term_subst stk x u t:
~In x stk ->
~In z stk ->
~Names.In z (allvars f) ->
nam2mix (stk++z::stk') (rename x z f) =
nam2mix (stk++x::stk') f.
nam2mix_term stk (Term.subst x u t) =
Mix.fsubst x (nam2mix_term stk u) (nam2mix_term stk t).
Proof.
revert stk.
induction f; cbn; intros stk Hx Hz IS; f_equal; auto.
- injection (nam2mix_term_subst' stk stk' x z (Fun "" l)); easy.
- intuition.
- intuition.
- case eqbspec; cbn.
+ intros <-.
symmetry.
apply (nam2mix_shadowstack' (x::stk)). simpl; auto.
right. rewrite freevars_allvars. namedec.
+ intros NE.
apply (IHf (v::stk)).
simpl. intuition.
simpl. intuition.
namedec.
induction t as [v|f l IH] using term_ind'; intros NI; cbn.
- case eqbspec; [intros ->|intros NE]; cbn.
+ rewrite <-list_index_notin in NI. rewrite NI.
cbn. unfold Mix.varsubst. now rewrite eqb_refl.
+ destruct (list_index v stk); cbn; auto.
unfold Mix.varsubst. case eqbspec; intuition.
- f_equal; clear f.
rewrite !map_map. apply map_ext_in; auto.
Qed.
Lemma term_subst_bsubst stk x u t :
......@@ -292,148 +244,55 @@ Lemma term_subst_bsubst stk x u t :
(nam2mix_term (stk++[x]) t).
Proof.
induction t as [v|f l IH] using term_ind'; intros X U; cbn in *.
- case eqbspec.
+ intros ->.
rewrite list_index_app_r; auto. cbn. rewrite eqb_refl. cbn.
- case eqbspec; [intros ->|intros NE]; cbn.
+ rewrite list_index_app_r; auto. cbn. rewrite eqb_refl. cbn.
rewrite Nat.add_0_r. rewrite eqb_refl.
now apply nam2mix_term_nostack.
+ intros NE. cbn.
rewrite list_index_app_l' by (simpl; intuition).
+ rewrite list_index_app_l' by (simpl; intuition).
destruct (list_index v stk) eqn:E; cbn; auto.
apply list_index_lt_length in E.
case eqbspec; intros; subst; auto; omega.
- f_equal; clear f.
rewrite !map_map.
apply map_ext_in. intros t Ht. apply IH; auto.
rewrite !map_map. apply map_ext_in. auto.
Qed.
Lemma partialsubst_bsubst stk x u f :
~In x stk ->
(forall v, In v stk -> ~Names.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 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).
symmetry.
apply form_level_bsubst_id.
now rewrite nam2mix_level.
+ intros NE.
destruct IS as [->|(NI,IS)]; [easy|].
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.
(** [nam2mix] and renaming *)
Lemma rename_bsubst0 x z f :
Lemma nam2mix_rename stk stk' x z f :
~In x stk ->
~In z stk ->
~Names.In z (allvars f) ->
nam2mix [] (rename x z f) =
Mix.bsubst 0 (Mix.FVar z) (nam2mix [x] f).
Proof.
intros.
rewrite rename_partialsubst by auto.
apply (partialsubst_bsubst0 x (Var z)); auto.
Qed.
Lemma nam2mix_rename_iff z v v' f f' :
~ Names.In z (Names.union (allvars f) (allvars f')) ->
nam2mix [] (rename v z f) = nam2mix [] (rename v' z f')
<->
nam2mix [v] f = nam2mix [v'] f'.
nam2mix (stk++z::stk') (rename x z f) =
nam2mix (stk++x::stk') f.
Proof.
intros Hz.
rewrite 2 rename_bsubst0 by namedec.
split.
- intros H. apply bsubst_fresh_inj in H; auto.
rewrite !nam2mix_fvars. cbn. rewrite !freevars_allvars. namedec.
- now intros ->.
revert stk.
induction f; cbn; intros stk Hx Hz IS; f_equal; auto.
- injection (nam2mix_term_rename stk stk' x z (Fun "" l)); easy.
- intuition.
- intuition.
- case eqbspec; [intros <-|intros NE]; cbn.
+ symmetry.
apply (nam2mix_shadowstack' (x::stk)).
* simpl; auto.
* right. rewrite freevars_allvars. namedec.
+ apply (IHf (v::stk)); simpl; intuition.
Qed.
Lemma nam2mix_term_inj t t' :
nam2mix_term [] t = nam2mix_term [] t' <-> t = t'.
Proof.
split; [ | intros <-; auto ].
revert t t'.
fix IH 1. destruct t, t'; cbn; try easy.
- now intros [= <-].
- intros [= <- EQ]. f_equal.
revert l l0 EQ.
fix IH' 1. destruct l, l0; cbn; try easy.
intros [= EQ EQ']. f_equal; auto.
Qed.
(** [nam2mix] identifies equivalent formulas.
This is one side of the more general [nam2mix_canonical_gen] below. *)
Lemma nam2mix_canonical f f' :
nam2mix [] f = nam2mix [] f' <-> AlphaEq f f'.
Proof.
split.
- set (h := S (Nat.max (height f) (height f'))).
assert (LT : height f < h) by (unfold h; auto with *).
assert (LT' : height f' < h) by (unfold h; auto with *).
clearbody h. revert f f' LT LT'.
induction h as [|h IH]; [inversion 1|].
destruct f, f'; simpl; intros LT LT'; simpl_height; try easy.
+ intros [= <- E].
destruct (nam2mix_term_inj (Fun "" l) (Fun "" l0)) as (H,_).
simpl in H. injection H as <-; auto. now f_equal.
+ intros [= E]; auto.
+ intros [= <- E1 E2]; auto.
+ intros [= <- E].
destruct (exist_fresh (Names.union (allvars f) (allvars f'))) as (z,Hz).
apply AEqQu with z; auto.
apply IH; try rewrite rename_height; auto.
apply nam2mix_rename_iff; auto.
- induction 1; cbn; f_equal; auto.
apply (nam2mix_rename_iff z); auto.
Qed.
(** We've just seen that [nam2mix []] maps alpha-equivalent formulas
to equal formulas. This is actually also true for
[nam2mix stk] with any [stk]. Here comes a first part
of this statement, the full version is below in
[nam2mix_canonical_gen].
*)
Lemma AlphaEq_nam2mix_gen stk f f' :
Lemma nam2mix_canonical_gen1 stk f f' :
AlphaEq f f' -> nam2mix stk f = nam2mix stk f'.
Proof.
intros H. revert stk.
induction H; cbn; intros stk; f_equal; auto.
generalize (IHAlphaEq (z::stk)).
rewrite (nam2mix_rename [] stk v z) by (auto; namedec).
rewrite (nam2mix_rename [] stk v' z) by (auto; namedec).
rewrite <- (nam2mix_rename [] stk v z) by (auto; namedec).
rewrite <- (nam2mix_rename [] stk v' z) by (auto; namedec).
auto.
Qed.
(** SUBST *)
Lemma nam2mix_Subst_fsubst stk x u f f' :
~In x stk ->
(forall v, In v stk -> ~Names.In v (Term.vars u)) ->
Subst x u f f' ->
nam2mix stk f' = Mix.fsubst x (nam2mix_term [] u) (nam2mix stk f).
Proof.
intros NI CL (f0 & EQ & SI).
apply AlphaEq_nam2mix_gen with (stk:=stk) in EQ. rewrite EQ.
apply SimpleSubst_carac in SI. destruct SI as (<- & IS).
apply nam2mix_partialsubst; auto.
Qed.
(** [nam2mix] and substitutions *)
Lemma nam2mix_subst_fsubst stk x u f :
~In x stk ->
......@@ -441,9 +300,26 @@ Lemma nam2mix_subst_fsubst stk x u f :
nam2mix stk (subst x u f) =
Mix.fsubst x (nam2mix_term [] u) (nam2mix stk f).
Proof.
intros.
apply nam2mix_Subst_fsubst; auto.
apply Subst_subst.
intros X U.
destruct (subst_carac x u f) as (f' & EQ & SI & ->).
apply (nam2mix_canonical_gen1 stk) in EQ. rewrite EQ. clear f EQ.
revert stk X U SI.
induction f'; cbn; intros stk X U IS; f_equal; auto.
- rewrite <- (nam2mix_term_nostack stk); auto.
injection (nam2mix_term_subst stk x u (Fun "" l)); easy.
- intuition.
- intuition.
- case eqbspec; cbn.
+ intros ->.
unfold Mix.fsubst.
rewrite form_vmap_id; auto.
intros x. rewrite nam2mix_fvars. simpl.
unfold Mix.varsubst.
intros IN.
case eqbspec; auto. intros <-. namedec.
+ intros NE.
destruct IS as [-> | (NI,IS)]; [easy|].
apply IHf'; simpl; intuition; subst; eauto.
Qed.
Lemma nam2mix0_subst_fsubst x u f :
......@@ -453,19 +329,15 @@ Proof.
apply nam2mix_subst_fsubst; auto.
Qed.
Lemma nam2mix_Subst_bsubst stk x u f f' :
~In x stk ->
(forall v, In v stk -> ~Names.In v (Term.vars u)) ->
Subst x u f f' ->
nam2mix stk f' =
Mix.bsubst (length stk) (nam2mix_term [] u)
(nam2mix (stk++[x]) f).
Lemma nam2mix_subst_nop x stk f :
~In x stk ->
nam2mix stk (subst x x f) = nam2mix stk f.
Proof.
intros NI CL (f0 & EQ & SI).
apply AlphaEq_nam2mix_gen with (stk:=stk++[x]) in EQ.
rewrite EQ.
apply SimpleSubst_carac in SI. destruct SI as (<- & IS).
now apply partialsubst_bsubst.
intros NI.
rewrite nam2mix_subst_fsubst; auto.
- cbn. unfold Mix.fsubst. rewrite form_vmap_id; auto.
intros v Hv. unfold Mix.varsubst. case eqbspec; auto. now intros ->.
- intros v Hv. cbn. nameiff. now intros ->.
Qed.
Lemma nam2mix_subst_bsubst stk x u f :
......@@ -475,9 +347,26 @@ Lemma nam2mix_subst_bsubst stk x u f :
Mix.bsubst (length stk) (nam2mix_term [] u)
(nam2mix (stk++[x]) f).
Proof.
intros.
apply nam2mix_Subst_bsubst; auto.
apply Subst_subst.
intros NI H.
destruct (subst_carac x u f) as (f' & EQ & SI & ->).
apply (nam2mix_canonical_gen1 (stk++[x])) in EQ. rewrite EQ. clear f EQ.
revert stk NI H SI.
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).
symmetry.
apply form_level_bsubst_id.
now rewrite nam2mix_level.
+ intros NE.
destruct IS as [->|(NI,IS)]; [easy|].
apply IHf'; simpl; auto.
intuition.
intros y [<-|Hy]; auto.
Qed.
Lemma nam2mix_subst_bsubst0 x u f :
......@@ -487,11 +376,9 @@ Proof.
apply nam2mix_subst_bsubst; auto.
Qed.
Lemma nam2mix_rename_iff2 z v v' f f' :
Lemma nam2mix_rename_iff z v v' f f' :
~ Names.In z (Names.union (freevars f) (freevars f')) ->
nam2mix [] (subst v (Var z) f) =
nam2mix [] (subst v' (Var z) f')
<->
nam2mix [] (subst v z f) = nam2mix [] (subst v' z f') <->
nam2mix [v] f = nam2mix [v'] f'.
Proof.
intros Hz.
......@@ -502,81 +389,88 @@ Proof.
- now intros ->.
Qed.
Lemma nam2mix_subst_nop x f :
nam2mix [] (subst x (Var x) f) = nam2mix [] f.
Proof.
rewrite nam2mix0_subst_fsubst. simpl.
unfold Mix.fsubst.
apply form_vmap_id.
intros y Hy. unfold Mix.varsubst.
case eqbspec; intros; subst; auto.
Qed.
Lemma subst_nop x f :
AlphaEq (subst x (Var x) f) f.
Lemma nam2mix_bsubst0_var x f :
Mix.bsubst 0 (Mix.FVar x) (nam2mix [x] f) = nam2mix [] f.
Proof.
apply nam2mix_canonical.
apply nam2mix_subst_nop.
rewrite <- (nam2mix_subst_nop x [] f) by auto.
symmetry. apply nam2mix_subst_bsubst0.
Qed.
Lemma nam2mix_rename_iff3 v x f f' :
Lemma nam2mix_rename_iff2 v x f f' :
~ Names.In x (Names.remove v (freevars f)) ->
nam2mix [] (subst v (Var x) f) = nam2mix [] f'
<->
nam2mix [] (subst v x f) = nam2mix [] f' <->
nam2mix [v] f = nam2mix [x] f'.
Proof.
intros Hx.
rewrite nam2mix_subst_bsubst0. cbn.
rewrite <- (nam2mix_bsubst0_var x f').
split.
- rewrite <- (nam2mix_subst_nop x f').
rewrite nam2mix_subst_bsubst0. cbn.
apply bsubst_fresh_inj.
- apply bsubst_fresh_inj.
rewrite !nam2mix_fvars. cbn. namedec.
- intros ->.
rewrite <- (nam2mix_subst_bsubst0 x (Var x)).
apply nam2mix_subst_nop.
- now intros ->.
Qed.
Lemma nam2mix_nostack stk f f' :
nam2mix stk f = nam2mix stk f' <->
nam2mix [] f = nam2mix [] f'.
(** [nam2mix []] identifies equivalent formulas and only them.
This result also holds with arbitrary stacks, see
[nam2mix_canonical] below. *)
Lemma nam2mix_canonical f f' :
nam2mix [] f = nam2mix [] f' <-> AlphaEq f f'.
Proof.
split.
- rewrite <- (rev_involutive stk).
set (s := rev stk). clearbody s.
revert f f'.
induction s as [|x s IH].
+ trivial.
+ intros f f'. simpl.
destruct (List.In_dec string_dec x (rev s)) as [IN|NI].
* rewrite 2 nam2mix_shadowstack; auto.
* intros Eq.
apply IH.
assert (E := subst_nop x f).
apply AlphaEq_nam2mix_gen with (stk:=rev s) in E.
rewrite <- E.
assert (E' := subst_nop x f').
apply AlphaEq_nam2mix_gen with (stk:=rev s) in E'.
rewrite <- E'.
clear E E'.
rewrite !nam2mix_subst_bsubst, Eq; simpl; auto.
intros v Hv. nameiff. now intros ->.
intros v Hv. nameiff. now intros ->.
- rewrite nam2mix_canonical. apply AlphaEq_nam2mix_gen.
Qed.
(** TODO Again !! *)
split; [ | apply nam2mix_canonical_gen1 ].
set (h := S (Nat.max (height f) (height f'))).
assert (LT : height f < h) by (unfold h; auto with *).
assert (LT' : height f' < h) by (unfold h; auto with *).
clearbody h. revert f f' LT LT'.
induction h as [|h IH]; [inversion 1|].
destruct f, f'; simpl; intros LT LT'; simpl_height; try easy.
- intros [= <- E].
destruct (nam2mix_term_inj (Fun "" l) (Fun "" l0)) as (H,_).
simpl in H. injection H as <-; auto. now f_equal.
- intros [= E]; auto.
- intros [= <- E1 E2]; auto.
- intros [= <- E].
destruct (exist_fresh (Names.union (allvars f) (allvars f'))) as (z,Hz).
apply AEqQu with z; auto.
apply IH; try rewrite rename_height; auto.
rewrite !rename_subst by auto with set.
apply nam2mix_rename_iff; auto.
rewrite !freevars_allvars. namedec.
Qed.
Lemma nam2mix_canonical_gen stk f f' :
nam2mix stk f = nam2mix stk f' <-> AlphaEq f f'.
Proof.
rewrite nam2mix_nostack. apply nam2mix_canonical.
split; [ | apply nam2mix_canonical_gen1 ].
rewrite <- (rev_involutive stk).
set (s := rev stk). clearbody s.
revert f f'.
induction s as [|x s IH].
- intros; simpl in *. now apply nam2mix_canonical.
- intros f f'. simpl.
destruct (List.In_dec string_dec x (rev s)) as [IN|NI].
+ rewrite 2 nam2mix_shadowstack; auto.
+ intros Eq.
apply IH.
rewrite <- (nam2mix_subst_nop x (rev s) f NI).
rewrite <- (nam2mix_subst_nop x (rev s) f' NI).
rewrite !nam2mix_subst_bsubst, Eq; simpl; auto.
* intros v Hv. nameiff. now intros ->.
* intros v Hv. nameiff. now intros ->.
Qed.
Lemma nam2mix_eqb (f f' : Nam.formula) :
(nam2mix [] f =? nam2mix [] f') = (f =? f').
Proof.
case eqbspec; rewrite nam2mix_canonical.
- intros. symmetry. now apply AlphaEq_equiv.
- intros H. rewrite <- AlphaEq_equiv in H.
symmetry. exact (not_true_is_false _ H).
Qed.
(** Swapping substitutions.
This technical lemma is described in Alexandre's course notes.
See also [Alpha.partialsubst_partialsubst]. In fact, we won't
reuse it afterwards. *)
use it afterwards. *)
Lemma subst_subst x x' u u' f :
x<>x' -> ~Names.In x (Term.vars u') ->
......@@ -598,7 +492,7 @@ Lemma subst_QuGen x z t q v f :
x<>v ->
~Names.In z (Names.add x (Names.union (freevars f) (Term.vars t))) ->
AlphaEq (subst x t (Quant q v f))
(Quant q z (subst x t (subst v (Var z) f))).
(Quant q z (subst x t (subst v z f))).
Proof.
intros NE NI.
apply nam2mix_canonical. cbn - [subst].
......@@ -606,16 +500,7 @@ Proof.
f_equal.
rewrite nam2mix_subst_fsubst by (simpl; namedec).
f_equal.
apply nam2mix_rename_iff3; auto. namedec.
Qed.
Lemma nam2mix_eqb (f f' : Nam.formula) :
(nam2mix [] f =? nam2mix [] f') = (f =? f').
Proof.
case eqbspec; rewrite nam2mix_canonical.
- intros. symmetry. now apply AlphaEq_equiv.
- intros H. rewrite <- AlphaEq_equiv in H.
symmetry. exact (not_true_is_false _ H).
apply nam2mix_rename_iff2; auto. namedec.
Qed.
(** Proofs about [mix2nam] *)
......
Equiv2.v
View file @ fb32a921
......@@ -152,15 +152,11 @@ Proof.
rewrite !Names.mem_spec.
rewrite !eqb_eq.
split; intros ((U,V),W); split; try split; auto.
+ change (Mix.FVar x) with (nam2mix_term [] (Var x)) in V.
rewrite <- nam2mix_subst_bsubst0 in V.