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

Natded: nettoyage de preuves (fresh)

parent d357b570
(** Alternative definitions of substs and alpha for named formulas *)
Require Import RelationClasses Arith Omega Defs NameProofs Nam.
Require Import Morphisms RelationClasses Arith Omega Defs NameProofs Nam.
Import ListNotations.
Import Nam.Form.
Import Nam.Form.Alt.
......@@ -912,13 +912,11 @@ Proof.
- apply Subst_Pred.
- apply Subst_Not; auto.
- apply Subst_Op; auto.
- set (vars := Names.union _ _).
assert (Hz := fresh_ok vars).
set (z := fresh _) in *. clearbody z.
- setfresh vars z Hz.
case eqbspec.
+ intros ->. apply Subst_Qu1.
+ intros NE.
destruct (Names.mem v (Term.vars t)) eqn:IN; cbn - [fresh].
destruct (Names.mem v (Term.vars t)) eqn:IN; cbn.
* clear IN.
apply Subst_Qu3 with (hsubst h v z f); auto.
{ rewrite freevars_allvars. namedec. }
......@@ -953,9 +951,7 @@ Proof.
split.
+ intros ((<-,?),?); auto.
+ now inversion_clear 1.
- set (vars := Names.union _ _).
assert (Hz := fresh_ok vars).
set (z := fresh vars) in *. clearbody z.
- setfresh vars z Hz.
rewrite <- !partialsubst_subst, !lazy_andb_iff, !eqb_eq, IH
by auto with set.
split.
......@@ -974,8 +970,6 @@ Proof.
eapply Subst_compat; eauto. apply Subst_subst.
Qed.
Require Import Morphisms RelationClasses.
Instance : Proper (eq ==> eq ==> AlphaEq ==> eq ==> iff) Subst.
Proof.
intros x x' <- t t' <- f f' Hf g g' <-.
......@@ -991,9 +985,3 @@ Proof.
intros x x' <- t t' <- f f' Hf.
apply (Subst_compat x t f f'); auto using Subst_subst.
Qed.
Lemma subst_Qu1 x t q f :
subst x t (Quant q x f) = Quant q x f.
Proof.
rewrite subst_eqn. now rewrite eqb_refl.
Qed.
......@@ -90,15 +90,11 @@ Proof.
- apply (term_substs_vars h (Fun "" l)).
- rewrite IHf1, IHf2. namedec.
- destruct (Names.mem _ _) eqn:E; simpl.
+ set (vars := Names.union _ _).
assert (Hz := fresh_ok vars).
set (z := fresh vars) in *.
+ setfresh vars z Hz.
rewrite IHf; simpl.
rewrite invars_unassoc, outvars_unassoc.
namedec.
rewrite invars_unassoc, outvars_unassoc. namedec.
+ rewrite IHf; simpl.
rewrite invars_unassoc, outvars_unassoc.
namedec.
rewrite invars_unassoc, outvars_unassoc. namedec.
Qed.
(** [nam2mix] and free variables *)
......@@ -1282,17 +1278,13 @@ Proof.
rewrite Hg. unfold g.
generalize (Inv_notin' _ _ v v IV). namedec00. }
clear MM.
set (vars := Names.union _ _).
assert (Hz := fresh_ok vars).
set (z := fresh vars) in *. clearbody z.
set (vars' := Names.union vars (Names.of_list stk)).
assert (Hz' := fresh_ok vars').
set (z' := fresh vars') in *. clearbody z'.
setfresh vars z Hz.
destruct (exist_fresh (Names.union vars (Names.of_list stk)))
as (z',Hz').
set (stk' := map (fun a => if a =? z then z' else a) stk).
unfold vars' in Hz'.
rewrite Names.union_spec in Hz'. apply Decidable.not_or in Hz'.
destruct Hz' as (Hz',Hz'2).
unfold vars in Hz,Hz'. clear vars' vars.
unfold vars in Hz,Hz'. clear vars.
rewrite outvars_app, invars_app in Hz,Hz'.
simpl in Hz, Hz'.
assert (CL' : In v stk -> chgVar h v <> v).
......
......@@ -259,9 +259,7 @@ Proof.
rewrite IHf1, IHf2 by (eapply Inv_weak; eauto; namedec).
split; [intros ((<-,<-),<-)|intros [= <- <- <-]]; easy.
- rewrite lazy_andb_iff, !eqb_eq.
set (vars := Names.union _ _).
assert (Hz := fresh_ok vars).
set (z := fresh vars) in *.
setfresh vars z Hz.
rewrite IHf by (constructor; try (eapply Inv_weak; eauto); namedec).
simpl.
split; [intros (<-,<-) | intros [=]]; easy.
......@@ -318,16 +316,11 @@ Proof.
- cbn in *. f_equal.
apply IHf; auto.
+ constructor; auto.
set (vars := Names.union (Names.of_list stack) (Mix.fvars f)).
assert (FR' := fresh_ok vars).
contradict FR'.
unfold vars at 2. nameiff. left.
now apply names_of_list_in.
setfresh vars z Hz. rewrite <- names_of_list_in. namedec.
+ simpl. omega with *.
+ simpl.
intros v [<-|IN].
* set (vars := Names.union (Names.of_list stack) (Mix.fvars f)).
generalize (fresh_ok vars). namedec.
* setfresh vars z Hz. namedec.
* apply FR in IN. namedec.
Qed.
......
......@@ -540,9 +540,7 @@ Lemma Valid_vmap_direct logic (d:derivation) :
Proof.
induction 1; intros h CL; cbn; try (econstructor; eauto; doClaim h).
- constructor. now apply in_map.
- set (vars:=Names.union _ _).
assert (Hz := fresh_ok vars).
set (z:=fresh vars) in *.
- setfresh vars z Hz.
set (h':=sub_set x (FVar z) h).
constructor.
+ cbn. namedec.
......@@ -559,9 +557,7 @@ Proof.
assert (E : getA [d1;d2] = (A)%form).
{ destruct d1. cbn in H2. now subst s. }
rewrite E.
set (vars:=Names.union _ _).
assert (Hz := fresh_ok vars).
set (z:=fresh vars) in *.
setfresh vars z Hz.
set (h':=sub_set x (FVar z) h).
apply V_Ex_e with (vmap h A).
+ cbn. namedec.
......@@ -791,16 +787,12 @@ Lemma claim_subset c c' d f :
Proof.
destruct d as (r,(c0,f0),ds). intros [= -> ->].
destruct r; cbn -[fresh vmap]; break; auto.
- set (vars := Names.add v _).
assert (Hz := fresh_ok vars).
set (z := fresh vars) in *.
cbn -[fresh]. f_equal.
- setfresh vars z Hz.
cbn. f_equal.
+ apply ctx_rename_rename. namedec.
+ apply form_rename_id. namedec.
- set (vars := Names.add v _).
assert (Hz := fresh_ok vars).
set (z := fresh vars) in *.
cbn -[fresh]. f_equal.
- setfresh vars z Hz.
cbn. f_equal.
+ apply ctx_rename_rename. namedec.
+ apply form_rename_id. namedec.
Qed.
......@@ -815,27 +807,23 @@ Proof.
try (econstructor; eauto using claim_subset; fail).
- destruct d1. cbn in H2; subst s.
econstructor; eauto using claim_subset.
- set (vars := Names.add x _).
assert (Hz := fresh_ok vars).
set (z := fresh vars) in *.
- setfresh vars z Hz.
set (h := sub_rename x z).
apply Valid_vmap_direct; auto.
cbn in H.
constructor; eauto using claim_subset.
+ unfold h. cbn - [z vmap sub_rename].
+ unfold h. cbn - [vmap sub_rename].
generalize (vmap_rename_notIn x z c'). namedec.
+ eapply IHValid; eauto.
rewrite <- (ctx_rename_id x z Γ) by namedec.
now apply ListSubset_map.
- destruct d1. cbn in H2; subst s.
set (vars := Names.add x _).
assert (Hz := fresh_ok vars).
set (z := fresh vars) in *.
setfresh vars z Hz.
set (h := sub_rename x z).
apply Valid_vmap_direct; auto.
cbn in H.
econstructor; eauto using claim_subset.
+ unfold h. cbn - [z vmap sub_rename].
+ unfold h. cbn - [vmap sub_rename].
generalize (vmap_rename_notIn x z c'). namedec.
+ eapply IHValid1; eauto.
rewrite <- (ctx_rename_id x z Γ) by namedec.
......
......@@ -394,6 +394,12 @@ Proof.
unfold strict_prefixes. simpl. namedec.
Qed.
Ltac setfresh vars z Hz :=
match goal with |- context [fresh ?v] => set (vars := v) end;
assert (Hz := fresh_ok vars);
set (z:=fresh vars) in *;
clearbody z.
Lemma exist_fresh names : exists z, ~In z names.
Proof.
exists (fresh names). apply fresh_ok.
......
......@@ -13,7 +13,7 @@ General
- Peut-on éviter tous ces "fix IH 1" ??
Eviter tous ces preuves similaires (termes, formules, etc).
- plus de exist_fresh au lieu des assert + set ?
(x) setfresh au lieu des assert + set ?
- essayer preuves de Equiv et Equiv2 directement sur hsubst
(peut-on avoir substs simultanée que en def alternative ?)
......
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