Commit 75db8923 authored by Pierre Letouzey's avatar Pierre Letouzey
Browse files

more cleanup (Arguments for Vars.*)

parent e8a95558
......@@ -7,8 +7,6 @@ Local Open Scope bool_scope.
Local Open Scope lazy_bool_scope.
Local Open Scope eqb_scope.
Arguments Vars.union _ _ : simpl nomatch.
Local Coercion Var : variable >-> term.
(** Alternative definition of substitution,
......@@ -441,10 +439,8 @@ Proof.
varsdec.
- case eqbspec; cbn. varsdec.
intros. destruct IS as [->|(NI,IS)]; [easy|].
assert (IN' : Vars.In x (freevars f)) by varsdec.
rewrite vars_mem_false by trivial.
rewrite (IHf IS IN').
varsdec.
rewrite (IHf IS); varsdec.
Qed.
......@@ -557,6 +553,13 @@ Proof.
exists (fresh_var vars). apply fresh_var_ok.
Qed.
(** A weaker but faster version of varsdec *)
Ltac varsdec0 :=
repeat (rewrite ?Vars.add_spec, ?Vars.union_spec,
?Vars.remove_spec, ?Vars.singleton_spec in *);
intuition auto.
Ltac simpl_fresh vars H :=
unfold vars in H; cbn in H;
rewrite ?Vars.add_spec, ?Vars.union_spec in H;
......@@ -677,27 +680,24 @@ Proof.
assert (E : map (term_subst x z') l =
map (term_subst x' z') l0).
{ injection (term_subst_rename x x' z z' (Fun "" l) (Fun "" l0)).
auto. varsdec. varsdec. cbn; f_equal; auto. }
auto. varsdec0. varsdec0. cbn; f_equal; auto. }
now rewrite E.
- inversion 1; eauto.
- inversion 1; subst; constructor; eapply IH; eauto; varsdec.
- repeat match goal with |- context [(?a ?= ?b)%string] =>
fold (a =? b)%string; destruct (string_eqb_spec a b);
[exfalso; varsdec|]
end.
- inversion 1; subst; constructor; eapply IH; eauto; varsdec0.
- rewrite !vars_mem_false by varsdec0.
repeat (case eqbspec; cbn).
+ trivial.
+ intros NE <-. inversion_clear 1.
assert (~Vars.In x' (freevars f')).
{ eapply AEq_rename_aux; eauto. }
rewrite !(partialsubst_notin x') in * by trivial.
apply AEqQu with z0; auto with set.
apply AEqQu with z0; auto.
+ intros <- NE. inversion_clear 1.
assert (~Vars.In x (freevars f)).
{ apply AEq_sym in H1.
eapply AEq_rename_aux; eauto. varsdec. varsdec. }
eapply AEq_rename_aux; eauto; varsdec0. }
rewrite !(partialsubst_notin x) in * by trivial.
apply AEqQu with z0; auto with set.
apply AEqQu with z0; auto.
+ intros NE NE'. inversion_clear 1.
(* Let's pick a suitably fresh variable z1 *)
......@@ -713,14 +713,13 @@ Proof.
(* Let's use z1 instead of z0 in the main hyp *)
apply IH with (z':=z1) in H1; [ | auto | auto | varsdec].
apply IH with (z':=z1) in H1; [ | auto | auto | varsdec0].
clear H0 z0.
(* Let's use z1 in the conclusion. *)
apply AEqQu with z1; auto.
rewrite !allvars_partialsubst. cbn. varsdec.
rewrite !allvars_partialsubst; cbn; varsdec0.
revert H1.
(* We now need to swap the substitutions to
......@@ -728,12 +727,12 @@ Proof.
rewrite !(partialsubst_partialsubst x),
!(partialsubst_partialsubst x'); auto;
repeat (rewrite term_subst_notin by (cbn; varsdec));
cbn;
rewrite ?Vars.singleton_spec; auto with set.
rewrite ?term_subst_notin; cbn;
rewrite ?Vars.singleton_spec; auto;
try apply notin_IsSimple; try (varsdec0;fail).
apply IH; auto;
rewrite !allvars_partialsubst; cbn; varsdec.
rewrite !allvars_partialsubst; cbn; varsdec0.
Qed.
Lemma AEq_trans f1 f2 f3 :
......
......@@ -8,8 +8,6 @@ Local Open Scope bool_scope.
Local Open Scope lazy_bool_scope.
Local Open Scope eqb_scope.
Arguments Vars.union _ _ : simpl nomatch.
Lemma subinvars_filter v h :
Vars.Equal (subinvars (filter (fun '(x, _) => negb (x =? v)) h))
(Vars.remove v (subinvars h)).
......@@ -131,7 +129,7 @@ Proof.
Qed.
(* Unused for the moment *)
Lemma nam2mix_subst stk x u f :
Lemma nam2mix_partialsubst stk x u f :
~In x stk ->
(forall v, In v stk -> ~Vars.In v (term_vars u)) ->
IsSimple x u f ->
......@@ -198,12 +196,12 @@ Admitted.
*)
(* Unused for the moment *)
Lemma nam2mix0_subst x u f :
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_subst; auto.
apply nam2mix_partialsubst; auto.
Qed.
Lemma term_subst_bsubst stk x z t :
......@@ -242,8 +240,8 @@ 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. varsdec.
- apply IHf2; auto. varsdec.
- apply IHf1; auto. varsdec0.
- apply IHf2; auto. varsdec0.
- fold (v =? z)%string. change (v =? z)%string with (v =? z).
case eqbspec; cbn.
+ intros <-.
......@@ -253,8 +251,7 @@ Proof.
apply form_level_bsubst_id.
now rewrite nam2mix_level.
+ intros NE.
case eqbspec; cbn; [varsdec|].
intros NE'.
rewrite vars_mem_false by varsdec0.
apply IHf; simpl; intuition.
Qed.
......@@ -266,43 +263,6 @@ Proof.
apply partialsubst_bsubst; auto.
Qed.
Lemma term_bsubst_fresh_inj n z (t t':Mix.term):
~ Vars.In z (Vars.union (Mix.fvars t) (Mix.fvars t')) ->
Mix.bsubst n (Mix.FVar z) t = Mix.bsubst n (Mix.FVar z) t' ->
t = t'.
Proof.
revert t t'.
fix IH 1; destruct t, t'; cbn; intros NI; try discriminate.
- intro E. exact E.
- clear IH. case eqbspec; auto. intros -> [= ->]. varsdec.
- clear IH. case eqbspec; auto. intros -> [= ->]. varsdec.
- clear IH. do 2 case eqbspec; intros; subst; easy.
- clear IH. case eqbspec; easy.
- clear IH. case eqbspec; easy.
- intros [= <- E]; f_equal.
revert l l0 NI E.
fix IH' 1; destruct l, l0; cbn; trivial; try discriminate.
intros NI. intros [= E E']. f_equal. apply IH; auto. varsdec.
apply IH'; auto. varsdec.
Qed.
Lemma bsubst_fresh_inj n z (f f':Mix.formula):
~ Vars.In z (Vars.union (Mix.fvars f) (Mix.fvars f')) ->
Mix.bsubst n (Mix.FVar z) f = Mix.bsubst n (Mix.FVar z) f' ->
f = f'.
Proof.
revert f' n.
induction f; destruct f'; cbn; intros n NI; try easy.
- intros[= <- E]. f_equal.
injection (term_bsubst_fresh_inj n z (Mix.Fun "" l) (Mix.Fun "" l0));
cbn; auto. now f_equal.
- intros [= E]. f_equal; eauto.
- intros [= <- E1 E2]. f_equal. eapply IHf1; eauto. varsdec.
eapply IHf2; eauto. varsdec.
- intros [= <- E]. f_equal. eapply IHf; eauto.
Qed.
Lemma nam2mix_rename_iff z v v' f f' :
~ Vars.In z (Vars.union (allvars f) (allvars f')) ->
nam2mix [] (partialsubst v (Var z) f) =
......@@ -363,6 +323,26 @@ Qed.
(** SUBST *)
Lemma nam2mix_Subst x u f f' :
Subst x u f f' ->
nam2mix [] f' = Mix.fsubst x (nam2mix_term [] u) (nam2mix [] f).
Proof.
intros (f0 & EQ & SI).
apply nam2mix_AlphaEq in EQ. rewrite EQ.
apply SimpleSubst_carac in SI. destruct SI as (<- & IS).
apply nam2mix0_partialsubst; auto.
Qed.
Lemma nam2mix_subst x u f :
nam2mix [] (form_subst x u f) =
Mix.fsubst x (nam2mix_term [] u) (nam2mix [] f).
Proof.
apply nam2mix_Subst.
apply Subst_subst.
Qed.
Definition foldsubst (h:subst) :=
fold_left (fun a '(x,u) => form_subst x u a) h.
......
......@@ -58,6 +58,14 @@ Bind Scope string_scope with variable.
Module Vars := MSetRBT.Make (StringOT).
(* Prevent incomplete reductions *)
Arguments Vars.singleton !_.
Arguments Vars.add !_ !_.
Arguments Vars.remove !_ !_.
Arguments Vars.union !_ !_.
Arguments Vars.inter !_ !_.
Arguments Vars.diff !_ !_.
Definition vars_of_list := fold_right Vars.add Vars.empty.
Fixpoint vars_unions (l: list Vars.t) :=
......
......@@ -35,6 +35,44 @@ Proof.
unfold closed. intros. apply term_level_bsubst_id. auto with *.
Qed.
(** [bsubst] to a fesh variable is injective *)
Lemma term_bsubst_fresh_inj n z (t t':term):
~ Vars.In z (Vars.union (fvars t) (fvars t')) ->
bsubst n (FVar z) t = bsubst n (FVar z) t' ->
t = t'.
Proof.
revert t t'.
fix IH 1; destruct t, t'; cbn; intros NI; try discriminate.
- intro E. exact E.
- clear IH. case eqbspec; auto. intros -> [= ->]. varsdec.
- clear IH. case eqbspec; auto. intros -> [= ->]. varsdec.
- clear IH. do 2 case eqbspec; intros; subst; easy.
- clear IH. case eqbspec; easy.
- clear IH. case eqbspec; easy.
- intros [= <- E]; f_equal.
revert l l0 NI E.
fix IH' 1; destruct l, l0; cbn; trivial; try discriminate.
intros NI. intros [= E E']. f_equal. apply IH; auto. varsdec.
apply IH'; auto. varsdec.
Qed.
Lemma bsubst_fresh_inj n z (f f':formula):
~ Vars.In z (Vars.union (fvars f) (fvars f')) ->
Mix.bsubst n (Mix.FVar z) f = Mix.bsubst n (Mix.FVar z) f' ->
f = f'.
Proof.
revert f' n.
induction f; destruct f'; cbn; intros n NI; try easy.
- intros[= <- E]. f_equal.
injection (term_bsubst_fresh_inj n z (Mix.Fun "" l) (Mix.Fun "" l0));
cbn; auto. now f_equal.
- intros [= E]. f_equal; eauto.
- intros [= <- E1 E2]. f_equal. eapply IHf1; eauto. varsdec.
eapply IHf2; eauto. varsdec.
- intros [= <- E]. f_equal. eapply IHf; eauto.
Qed.
(** [vmap] basic results : extensionality, identity, composition *)
Lemma term_vmap_ext h h' (t:term) :
......@@ -122,7 +160,7 @@ Lemma term_fvars_vmap h (t:term) :
(vars_flatmap (fun v => fvars (h v)) (fvars t)).
Proof.
induction t as [ | |f l IH] using term_ind'; cbn.
- varsdec.
- unfold Vars.singleton. cbn. varsdec.
- varsdec.
- intros v. rewrite vars_unionmap_in. intros (a & Ha & Ha').
rewrite in_map_iff in Ha'. destruct Ha' as (t & <- & Ht).
......@@ -135,9 +173,9 @@ Lemma form_fvars_vmap h (f:formula) :
(fvars (vmap h f))
(vars_flatmap (fun v => fvars (h v)) (fvars f)).
Proof.
induction f; cbn; try varsdec.
induction f; simpl; try varsdec.
- apply (term_fvars_vmap h (Fun "" l)).
- rewrite vars_flatmap_union. varsdec.
- cbn. rewrite vars_flatmap_union. varsdec.
Qed.
Lemma ctx_fvars_vmap h (c:context) :
......
......@@ -725,8 +725,6 @@ Ltac break :=
| _ => idtac
end.
Arguments Vars.union !_ !_.
Ltac mytac :=
cbn in *;
break;
......@@ -756,7 +754,7 @@ Proof.
rewrite <- Vars.mem_spec. cbn. intros EQ. now rewrite EQ in *.
+ apply V_Ex_e with f; auto.
rewrite <- Vars.mem_spec. cbn. intros EQ. now rewrite EQ in *.
- induction 1; cbn; rewr; auto.
- induction 1; simpl; rewr; auto.
+ apply list_mem_in in H. now rewrite H.
+ rewrite <- Vars.mem_spec in H. destruct Vars.mem; auto.
+ rewrite <- Vars.mem_spec in H. destruct Vars.mem; auto.
......
......@@ -12,8 +12,6 @@ Ltac varsdec := VarsP.Dec.fsetdec.
Hint Extern 10 => varsdec : set.
Arguments Vars.union !_ !_.
Lemma vars_mem_false x vs : ~Vars.In x vs -> Vars.mem x vs = false.
Proof.
rewrite <- Vars.mem_spec. now case Vars.mem.
......
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