Natded: nettoyage de preuves (unionmap)

bf5fa1c8 · Pierre Letouzey · 5e0e5897 · bf5fa1c8 · bf5fa1c8 · bf5fa1c8
Commit bf5fa1c8 authored May 07, 2019 by Pierre Letouzey
--- a/Alpha.v
+++ b/Alpha.v
@@ -255,8 +255,7 @@ Proof.
 induction t as [v|f a IH] using term_ind'; cbn.
 - case eqbspec; auto. namedec.
 - intros NI. f_equal. apply map_id_iff.
-   intros t Ht. apply IH; auto. rewrite unionmap_in in NI.
-   contradict NI. now exists t.
+   intros t Ht. apply IH; auto. eapply unionmap_notin; eauto.
 Qed.

 Lemma partialsubst_notin x t f :
@@ -265,7 +264,7 @@ Lemma partialsubst_notin x t f :
 Proof.
 induction f; cbn; intros NI; f_equal; auto with set.
 - apply map_id_iff. intros a Ha. apply term_subst_notin.
-   rewrite unionmap_in in NI. contradict NI. now exists a.
+   eapply unionmap_notin; eauto.
 - case eqbspec; cbn; auto.
   intros NE. case Names.mem; f_equal; auto with set.
 Qed.
@@ -283,15 +282,10 @@ Lemma term_vars_subst x u t :
 Proof.
 induction t using term_ind'; cbn.
 - case eqbspec; cbn; auto with set.
- - intros v. rewrite unionmap_in.
-   intros (a & IN & IN'). rewrite in_map_iff in IN'.
-   destruct IN' as (b & <- & IN').
-   apply H in IN; trivial.
+ - intros v. rewrite unionmap_map_in.
+   intros (a & IN & IN'). apply H in IN; trivial.
   revert IN.
-   nameiff. rewrite unionmap_in in *.
-   intros [(U,V)|W].
-   + left. split; auto. now exists b.
-   + now right.
+   nameiff. intros [(U,V)|W]; auto. left; split; eauto with set.
 Qed.

 Lemma term_vars_subst_in x u t :
@@ -313,8 +307,7 @@ Proof.
     * intros _.
       assert (E'' : map (Term.substs [(x, u)]) l = l).
       { apply map_id_iff. intros a Ha.
-         apply term_subst_notin. contradict E'.
-         rewrite unionmap_in. now exists a. }
+         apply term_subst_notin. eapply unionmap_notin; eauto. }
       change Names.elt with variable in *.
       rewrite E''.
       fold (Term.subst x u t). rewrite (IH t E).
@@ -332,10 +325,9 @@ Lemma term_vars_subst_in' x u t :
 Proof.
 induction t using term_ind'; cbn.
 - case eqbspec; cbn; auto with set.
- - intros IN v Hv. rewrite unionmap_in in *.
-   destruct IN as (a & Ha & IN).
-   exists (Term.subst x u a); split; auto using in_map.
-   now apply (H a IN Ha).
+ - intros IN v Hv. rewrite unionmap_map_in.
+   rewrite unionmap_in in IN. destruct IN as (a & Ha & IN).
+   exists a; split; auto. apply H; auto.
 Qed.

 Lemma allvars_partialsubst x t f :

--- a/Alpha2.v
+++ b/Alpha2.v
@@ -292,7 +292,7 @@ Proof.
 - f_equal; clear f.
   rewrite !map_map.
   apply map_ext_in. intros t Ht. apply IH; auto.
-   rewrite unionmap_in in NI. contradict NI. now exists t.
+   eapply unionmap_notin; eauto.
 Qed.

 Lemma nam2mix_partialsubst' stk stk' x z f :
@@ -764,11 +764,8 @@ Proof.
   rewrite eqb_sym.
   case eqbspec; simpl.
   + intros -> [IN|[= ->]]. intuition.
-     unfold Subst.outvars. rewrite unionmap_in.
-     intros ((a,t) & IN & IN').
-     rewrite in_map_iff in IN'.
-     destruct IN' as ((a',b) & [= -> <-] & IN').
-     rewrite unassoc_in in IN'.
+     unfold Subst.outvars. rewrite unionmap_map_in.
+     intros ((a,b) & IN & IN'). rewrite unassoc_in in IN'.
     simpl in IN. rewrite Names.singleton_spec in IN.
     destruct (H' a b); intuition.
   + intros NE [IN|SO];

--- a/Meta.v
+++ b/Meta.v
@@ -55,8 +55,7 @@ Lemma level_bsubst n u (f:formula) :
 Proof.
 revert n.
 induction f; cbn; intros n Hf Hu; auto with arith.
- - rewrite map_map. apply list_max_map_le.
-   rewrite list_max_map_le in Hf; auto using level_bsubst_term.
+ - apply (level_bsubst_term n u (Fun "" l)); auto.
 - rewrite max_le in *; intuition.
 - specialize (IHf (S n)). omega.
 Qed.
@@ -67,11 +66,7 @@ Lemma bsubst_term_fvars n (u t:term) :
 Names.Subset (fvars (bsubst n u t)) (Names.union (fvars u) (fvars t)).
 Proof.
 induction t as [ | | f l IH] using term_ind'; cbn; auto with *.
- intros v. rewrite Names.union_spec, !unionmap_in.
- intros (a & Hv & Ha). rewrite in_map_iff in Ha.
- destruct Ha as (a' & <- & Ha'). apply IH in Hv; auto.
- rewrite Names.union_spec in Hv; destruct Hv as [Hv|Hv]; auto.
- right. now exists a'.
+ apply subset_unionmap_map; auto.
 Qed.

 Lemma bsubst_fvars n u (f:formula) :
@@ -79,11 +74,7 @@ Lemma bsubst_fvars n u (f:formula) :
 Proof.
 revert n.
 induction f; cbn; intros; auto with *.
- - intros v. rewrite Names.union_spec, !unionmap_in.
-   intros (a & Hv & Ha). rewrite in_map_iff in Ha.
-   destruct Ha as (a' & <- & Ha'). apply bsubst_term_fvars in Hv; auto.
-   rewrite Names.union_spec in Hv; destruct Hv as [Hv|Hv]; auto.
-   right. now exists a'.
+ - apply (bsubst_term_fvars n u (Fun "" l)).
 - rewrite IHf1, IHf2. namedec.
 Qed.

@@ -249,9 +240,8 @@ Proof.
 induction t as [ | |f l IH] using term_ind'; cbn.
 - unfold Names.singleton. cbn. namedec.
 - namedec.
- - intros v. rewrite unionmap_in. intros (a & Ha & Ha').
-   rewrite in_map_iff in Ha'. destruct Ha' as (t & <- & Ht).
-   generalize (IH t Ht v Ha). apply flatmap_subset; auto.
+ - intros v. rewrite unionmap_map_in. intros (a & Hv & Ha).
+   generalize (IH a Ha v Hv). apply flatmap_subset; auto.
   intro. eauto with set.
 Qed.

@@ -1208,14 +1198,7 @@ Proof.
 induction t as [ | | f l IH] using term_ind'; cbn; auto with *.
 destruct funsymbs; cbn; auto with *.
 case eqbspec; cbn; auto with *.
- intros _. clear f a.
- intros v. rewrite Names.add_spec, !unionmap_in.
- intros (t & Hv & Ht).
- rewrite in_map_iff in Ht.
- destruct Ht as (a & <- & Ha).
- apply IH in Hv; auto.
- rewrite Names.add_spec in Hv. destruct Hv as [Hv|Hv]; auto.
- right. now exists a.
+ intros _. apply subset_unionmap_map'; auto.
 Qed.

 Lemma restrict_form_fvars sign x f :
@@ -1225,14 +1208,8 @@ Proof.
 induction f; cbn; auto with *.
 destruct predsymbs; cbn; auto with *.
 case eqbspec; cbn; auto with *.
- intros _. clear p a.
- intros v. rewrite Names.add_spec, !unionmap_in.
- intros (t & Hv & Ht).
- rewrite in_map_iff in Ht.
- destruct Ht as (a & <- & Ha).
- apply restrict_term_fvars in Hv; auto.
- rewrite Names.add_spec in Hv. destruct Hv as [Hv|Hv]; auto.
- right. now exists a.
+ intros _. apply subset_unionmap_map'.
+ intros t _. apply restrict_term_fvars.
 Qed.

 Lemma restrict_ctx_fvars sign x c :
@@ -1240,14 +1217,8 @@ Lemma restrict_ctx_fvars sign x c :
              (Names.add x (fvars c)).
 Proof.
 unfold restrict_ctx.
- intros v. unfold fvars, fvars_list.
- rewrite Names.add_spec, !unionmap_in.
- intros (f & Hv & Hf).
- rewrite in_map_iff in Hf.
- destruct Hf as (a & <- & Ha).
- apply restrict_form_fvars in Hv; auto.
- rewrite Names.add_spec in Hv. destruct Hv as [Hv|Hv]; auto.
- right. now exists a.
+ apply subset_unionmap_map'.
+ intros f _. apply restrict_form_fvars.
 Qed.

 Lemma restrict_seq_fvars sign x s :
@@ -1272,13 +1243,7 @@ Proof.
 induction d as [r s ds IH] using derivation_ind'; cbn.
 rewrite restrict_rule_fvars, restrict_seq_fvars.
 rewrite Forall_forall in IH.
- intros v. nameiff.
- rewrite !unionmap_in. intuition.
- destruct H0 as (a & Hv & Ha).
- rewrite in_map_iff in Ha. destruct Ha as (a' & <- & Ha').
- apply IH in Hv; auto. rewrite Names.add_spec in Hv.
- destruct Hv; auto.
- right; right; right; left. now exists a'.
+ apply subset_unionmap_map' in IH. rewrite IH. namedec.
 Qed.


@@ -1491,11 +1456,7 @@ Proof.
 induction t as [ | | f l IH] using term_ind';
   cbn - [Nat.ltb]; auto with *.
 - case Nat.ltb_spec; cbn; auto with *.
- - intros v. rewrite Names.add_spec, !unionmap_in.
-   intros (a & Hv & Ha).
-   rewrite in_map_iff in Ha. destruct Ha as (a' & <- & Ha').
-   apply IH in Hv; auto. apply Names.add_spec in Hv.
-   destruct Hv; auto. right; now exists a'.
+ - apply subset_unionmap_map'; auto.
 Qed.

 Lemma forcelevel_fvars n x f :
@@ -1503,11 +1464,8 @@ Lemma forcelevel_fvars n x f :
 Proof.
 revert n.
 induction f; cbn; intros; auto with *.
- - intros v. rewrite Names.add_spec, !unionmap_in.
-   intros (a & Hv & Ha).
-   rewrite in_map_iff in Ha. destruct Ha as (a' & <- & Ha').
-   apply forcelevel_term_fvars in Hv; auto. apply Names.add_spec in Hv.
-   destruct Hv; auto. right; now exists a'.
+ - apply subset_unionmap_map'.
+   intros t _. apply forcelevel_term_fvars.
 - rewrite IHf1, IHf2. namedec.
 Qed.

@@ -1515,11 +1473,8 @@ Lemma forcelevel_ctx_fvars x (c:context) :
 Names.Subset (fvars (forcelevel_ctx x c)) (Names.add x (fvars c)).
 Proof.
 unfold forcelevel_ctx. unfold fvars, fvars_list.
- intros v. rewrite Names.add_spec, !unionmap_in.
- intros (a & Hv & Ha).
- rewrite in_map_iff in Ha. destruct Ha as (a' & <- & Ha').
- apply forcelevel_fvars in Hv; auto. apply Names.add_spec in Hv.
- destruct Hv; auto. right; now exists a'.
+ apply subset_unionmap_map'.
+ intros f _. apply forcelevel_fvars.
 Qed.

 Lemma forcelevel_term_level n x t :

--- a/Models.v
+++ b/Models.v
@@ -78,8 +78,7 @@ Proof.
   + unfold BClosed in *. cbn in BC.
     rewrite list_max_map_0 in BC; auto.
   + unfold FClosed in *. cbn in FC.
-     intros v. specialize (FC v). contradict FC.
-     rewrite unionmap_in. now exists t.
+     intros v. eapply unionmap_notin; eauto.
 - intros (E,F).
   rewrite Forall_forall in F.
   repeat split; cbn.
@@ -105,8 +104,7 @@ Proof.
   + unfold BClosed in *. cbn in BC.
     rewrite list_max_map_0 in BC; auto.
   + unfold FClosed in *. cbn in FC.
-     intros v. specialize (FC v). contradict FC.
-     rewrite unionmap_in. now exists t.
+     intros v. eapply unionmap_notin; eauto.
 - intros (E,F).
   rewrite Forall_forall in F.
   repeat split; cbn.

--- a/NameProofs.v
+++ b/NameProofs.v
@@ -77,6 +77,43 @@ Qed.

 Hint Resolve unionmap_in' : set.

+Lemma unionmap_notin {A} (f: A -> t) (l: list A) v a :
+ ~In v (unionmap f l) -> List.In a l -> ~In v (f a).
+Proof.
+ intros NI IN. contradict NI. eapply unionmap_in'; eauto.
+Qed.
+
+Lemma unionmap_map_in {A B} (f: B -> t) (g : A -> B) (l: list A) v :
+ In v (unionmap f (List.map g l)) <-> exists a, In v (f (g a)) /\ List.In a l.
+Proof.
+ rewrite unionmap_in.
+ split.
+ - intros (b & Hv & Hb). apply in_map_iff in Hb.
+   destruct Hb as (a & <- & Ha). now exists a.
+ - intros (a & Hv & Ha). exists (g a). split; auto.
+   apply in_map_iff. now exists a.
+Qed.
+
+Lemma subset_unionmap_map {A} (f: A -> t) (g : A -> A) (l: list A) s :
+ (forall x, List.In x l -> Subset (f (g x)) (union s (f x))) ->
+ Subset (unionmap f (List.map g l)) (union s (unionmap f l)).
+Proof.
+ intros H v.
+ rewrite union_spec, unionmap_map_in, unionmap_in.
+ intros (a & Hv & Ha). apply H in Hv; auto.
+ rewrite union_spec in Hv. destruct Hv as [Hv|Hv]; auto.
+ right. now exists a.
+Qed.
+
+Lemma subset_unionmap_map' {A} (f: A -> t) (g : A -> A) (l: list A) c :
+ (forall x, List.In x l -> Subset (f (g x)) (add c (f x))) ->
+ Subset (unionmap f (List.map g l)) (add c (unionmap f l)).
+Proof.
+ intros H. rewrite NamesP.add_union_singleton.
+ apply subset_unionmap_map. intros x Hx.
+ rewrite <- NamesP.add_union_singleton; auto.
+Qed.
+
 Lemma map_in_aux (f : name -> name) l y acc :
 In y
  (List.fold_left (fun vs a => add (f a) vs) l acc) <->

--- a/PreModels.v
+++ b/PreModels.v
@@ -137,12 +137,12 @@ Proof.
 intros E.
 unfold interp_ctx.
 split; intros H f Hf.
- rewrite <- (interp_form_ext genv); auto with set.
- intros v Hv. apply E. unfold fvars, fvars_list.
- rewrite unionmap_in. exists f. now split.
- rewrite (interp_form_ext genv); auto with set.
- intros v Hv. apply E. unfold fvars, fvars_list.
- rewrite unionmap_in. exists f. now split.
+ - rewrite <- (interp_form_ext genv); auto with set.
+   intros v Hv. apply E. unfold fvars, fvars_list.
+   eauto with set.
+ - rewrite (interp_form_ext genv); auto with set.
+   intros v Hv. apply E. unfold fvars, fvars_list.
+   eauto with set.
 Qed.

 Lemma interp_term_more_lenv genv lenv lenv' t :

--- a/Theories.v
+++ b/Theories.v
@@ -949,10 +949,7 @@ Proof.
       rewrite Hm.
       apply delcst_HenkinAll_signext.
     * rewrite form_funs_wf. apply WfAxiom. simpl. now right.
-       intros IN.
-       assert (Names.In c (Names.unionmap form_funs (HenkinAxList th nc n))).
-       { rewrite unionmap_in. now exists A. }
-       namedec.
+       eapply unionmap_notin; eauto; namedec.
   + clearbody f. clear Ew. rewrite form_funs_ok. cbn.
     destruct WF as (CK,?). cbn in CK. now rewrite CK.
     cbn. namedec.