From 76adb57c72fccb4f3e416bd7f3927f4fff72178b Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sun, 1 Jun 2014 10:26:26 +0200 Subject: Making those proofs which depend on names generated for the arguments in Prop of constructors of inductive types independent of these names. Incidentally upgraded/simplified a couple of proofs, mainly in Reals. This prepares to the next commit about using names based on H for such hypotheses in Prop. --- theories/FSets/FMapAVL.v | 10 +++++----- theories/FSets/FMapFacts.v | 22 +++++++++++----------- theories/FSets/FMapList.v | 12 ++++++------ theories/FSets/FMapPositive.v | 2 +- theories/FSets/FMapWeakList.v | 17 +++++++++-------- theories/FSets/FSetBridge.v | 12 ++++++------ 6 files changed, 38 insertions(+), 37 deletions(-) (limited to 'theories/FSets') diff --git a/theories/FSets/FMapAVL.v b/theories/FSets/FMapAVL.v index bee922c6f..7f5853494 100644 --- a/theories/FSets/FMapAVL.v +++ b/theories/FSets/FMapAVL.v @@ -1270,10 +1270,10 @@ Proof. inv bst. rewrite H2, join_find; auto; clear H2. - simpl; destruct X.compare; simpl; auto. + simpl; destruct X.compare as [Hlt| |Hlt]; simpl; auto. destruct (find y m2'); auto. symmetry; rewrite not_find_iff; auto; intro. - apply (MX.lt_not_gt l); apply H1; auto; rewrite H3; auto. + apply (MX.lt_not_gt Hlt); apply H1; auto; rewrite H3; auto. intros z Hz; apply H1; auto; rewrite H3; auto. Qed. @@ -1622,8 +1622,8 @@ Lemma map_option_find : forall (m:t elt)(x:key), Proof. intros m; functional induction (map_option f m); simpl; auto; intros; inv bst; rewrite join_find || rewrite concat_find; auto; simpl; - try destruct X.compare; simpl; auto. -rewrite (f_compat d e); auto. + try destruct X.compare as [Hlt|Heq|Hlt]; simpl; auto. +rewrite (f_compat d Heq); auto. intros y H; destruct (map_option_2 H) as (? & ? & ?); eauto using MapsTo_In. intros y H; @@ -1631,7 +1631,7 @@ intros y H; rewrite <- IHt, IHt0; auto; nonify (find x0 r); auto. rewrite IHt, IHt0; auto; nonify (find x0 r); nonify (find x0 l); auto. -rewrite (f_compat d e); auto. +rewrite (f_compat d Heq); auto. rewrite <- IHt0, IHt; auto; nonify (find x0 l); auto. destruct (find x0 (map_option f r)); auto. diff --git a/theories/FSets/FMapFacts.v b/theories/FSets/FMapFacts.v index 0e3b5cef1..083965cb7 100644 --- a/theories/FSets/FMapFacts.v +++ b/theories/FSets/FMapFacts.v @@ -702,18 +702,18 @@ Add Parametric Morphism elt : (@add elt) with signature E.eq ==> eq ==> Equal ==> Equal as add_m. Proof. intros k k' Hk e m m' Hm y. -rewrite add_o, add_o; do 2 destruct eq_dec; auto. -elim n; rewrite <-Hk; auto. -elim n; rewrite Hk; auto. +rewrite add_o, add_o; do 2 destruct eq_dec as [|?Hnot]; auto. +elim Hnot; rewrite <-Hk; auto. +elim Hnot; rewrite Hk; auto. Qed. Add Parametric Morphism elt : (@remove elt) with signature E.eq ==> Equal ==> Equal as remove_m. Proof. intros k k' Hk m m' Hm y. -rewrite remove_o, remove_o; do 2 destruct eq_dec; auto. -elim n; rewrite <-Hk; auto. -elim n; rewrite Hk; auto. +rewrite remove_o, remove_o; do 2 destruct eq_dec as [|?Hnot]; auto. +elim Hnot; rewrite <-Hk; auto. +elim Hnot; rewrite Hk; auto. Qed. Add Parametric Morphism elt elt' : (@map elt elt') @@ -861,7 +861,7 @@ Module WProperties_fun (E:DecidableType)(M:WSfun E). inversion_clear Hnodup as [| ? ? Hnotin Hnodup']. specialize (IH k Hnodup'); clear Hnodup'. rewrite add_o, IH. - unfold eqb; do 2 destruct eq_dec; auto; elim n; eauto. + unfold eqb; do 2 destruct eq_dec as [|?Hnot]; auto; elim Hnot; eauto. Qed. Lemma of_list_2 : forall l, NoDupA eqk l -> @@ -928,7 +928,7 @@ Module WProperties_fun (E:DecidableType)(M:WSfun E). apply InA_eqke_eqk with k e'; auto. rewrite <- of_list_1; auto. intro k'. rewrite Hsame, add_o, of_list_1b. simpl. - unfold eqb. do 2 destruct eq_dec; auto; elim n; eauto. + unfold eqb. do 2 destruct eq_dec as [|?Hnot]; auto; elim Hnot; eauto. inversion_clear Hdup; auto. apply IHl. intros; eapply Hstep'; eauto. @@ -1890,7 +1890,7 @@ Module OrdProperties (M:S). find_mapsto_iff, (H0 t0), <- find_mapsto_iff, add_mapsto_iff by (auto with *). unfold O.eqke; simpl. intuition. - destruct (E.eq_dec x t0); auto. + destruct (E.eq_dec x t0) as [Heq|Hneq]; auto. exfalso. assert (In t0 m). exists e0; auto. @@ -1919,7 +1919,7 @@ Module OrdProperties (M:S). find_mapsto_iff, (H0 t0), <- find_mapsto_iff, add_mapsto_iff by (auto with *). unfold O.eqke; simpl. intuition. - destruct (E.eq_dec x t0); auto. + destruct (E.eq_dec x t0) as [Heq|Hneq]; auto. exfalso. assert (In t0 m). exists e0; auto. @@ -1975,7 +1975,7 @@ Module OrdProperties (M:S). inversion_clear H1; [ | inversion_clear H2; eauto ]. red in H3; simpl in H3; destruct H3. destruct p as (p1,p2). - destruct (E.eq_dec p1 x). + destruct (E.eq_dec p1 x) as [Heq|Hneq]. apply ME.lt_eq with p1; auto. inversion_clear H2. inversion_clear H5. diff --git a/theories/FSets/FMapList.v b/theories/FSets/FMapList.v index 64d5b1c9a..a6f9ae902 100644 --- a/theories/FSets/FMapList.v +++ b/theories/FSets/FMapList.v @@ -867,8 +867,8 @@ Proof. induction m'. (* m' = nil *) intros; destruct a; simpl. - destruct (X.compare x t0); simpl; auto. - inversion_clear Hm; clear H0 l Hm' IHm t0. + destruct (X.compare x t0) as [Hlt| |Hlt]; simpl; auto. + inversion_clear Hm; clear H0 Hlt Hm' IHm t0. induction m; simpl; auto. inversion_clear H. destruct a. @@ -1244,16 +1244,16 @@ Lemma eq_refl : forall m : t, eq m m. Proof. intros (m,Hm); induction m; unfold eq; simpl; auto. destruct a. - destruct (X.compare t0 t0); auto. - apply (MapS.Raw.MX.lt_antirefl l); auto. + destruct (X.compare t0 t0) as [Hlt| |Hlt]; auto. + apply (MapS.Raw.MX.lt_antirefl Hlt); auto. split. apply D.eq_refl. inversion_clear Hm. apply (IHm H). - apply (MapS.Raw.MX.lt_antirefl l); auto. + apply (MapS.Raw.MX.lt_antirefl Hlt); auto. Qed. -Lemma eq_sym : forall m1 m2 : t, eq m1 m2 -> eq m2 m1. +Lemma eq_sym : forall m1 m2 : t, eq m1 m2 -> eq m2 m1. Proof. intros (m,Hm); induction m; intros (m', Hm'); destruct m'; unfold eq; simpl; diff --git a/theories/FSets/FMapPositive.v b/theories/FSets/FMapPositive.v index 253800a45..a0ecdb756 100644 --- a/theories/FSets/FMapPositive.v +++ b/theories/FSets/FMapPositive.v @@ -1074,7 +1074,7 @@ Module PositiveMapAdditionalFacts. find i (add j x m) = if E.eq_dec i j then Some x else find i m. Proof. intros. - destruct (E.eq_dec i j); [ rewrite e; apply gss | apply gso; auto ]. + destruct (E.eq_dec i j) as [ ->|]; [ apply gss | apply gso; auto ]. Qed. (* Not derivable from the Map interface *) diff --git a/theories/FSets/FMapWeakList.v b/theories/FSets/FMapWeakList.v index e3f84723f..0f11dd7a5 100644 --- a/theories/FSets/FMapWeakList.v +++ b/theories/FSets/FMapWeakList.v @@ -146,9 +146,10 @@ Proof. induction m; simpl; auto; destruct a; intros. inversion_clear Hm. rewrite (IHm H1 x x'); auto. - destruct (X.eq_dec x t0); destruct (X.eq_dec x' t0); trivial. - elim n; apply X.eq_trans with x; auto. - elim n; apply X.eq_trans with x'; auto. + destruct (X.eq_dec x t0) as [|Hneq]; destruct (X.eq_dec x' t0) as [|?Hneq']; + trivial. + elim Hneq'; apply X.eq_trans with x; auto. + elim Hneq; apply X.eq_trans with x'; auto. Qed. (** * [add] *) @@ -787,14 +788,14 @@ Proof. destruct o; destruct o'; simpl in *; try discriminate; auto. destruct a as (k,(oo,oo')); simpl in *. inversion_clear H2. - destruct (X.eq_dec x k); simpl in *. + destruct (X.eq_dec x k) as [|Hneq]; simpl in *. (* x = k *) assert (at_least_one_then_f o o' = f oo oo'). destruct o; destruct o'; simpl in *; inversion_clear H; auto. rewrite H2. unfold f'; simpl. destruct (f oo oo'); simpl. - destruct (X.eq_dec x k); try contradict n; auto. + destruct (X.eq_dec x k) as [|Hneq]; try contradict Hneq; auto. destruct (IHm0 H1) as (_,H4); apply H4; auto. case_eq (find x m0); intros; auto. elim H0. @@ -804,7 +805,7 @@ Proof. (* k < x *) unfold f'; simpl. destruct (f oo oo'); simpl. - destruct (X.eq_dec x k); [ contradict n; auto | auto]. + destruct (X.eq_dec x k); [ contradict Hneq; auto | auto]. destruct (IHm0 H1) as (H3,_); apply H3; auto. destruct (IHm0 H1) as (H3,_); apply H3; auto. @@ -812,13 +813,13 @@ Proof. destruct a as (k,(oo,oo')). simpl. inversion_clear H2. - destruct (X.eq_dec x k). + destruct (X.eq_dec x k) as [|Hneq]. (* x = k *) discriminate. (* k < x *) unfold f'; simpl. destruct (f oo oo'); simpl. - destruct (X.eq_dec x k); [ contradict n; auto | auto]. + destruct (X.eq_dec x k); [ contradict Hneq; auto | auto]. destruct (IHm0 H1) as (_,H4); apply H4; auto. destruct (IHm0 H1) as (_,H4); apply H4; auto. Qed. diff --git a/theories/FSets/FSetBridge.v b/theories/FSets/FSetBridge.v index 6aebcf501..97f140b39 100644 --- a/theories/FSets/FSetBridge.v +++ b/theories/FSets/FSetBridge.v @@ -673,24 +673,24 @@ Module NodepOfDep (M: Sdep) <: S with Module E := M.E. forall (s : t) (x : elt) (f : elt -> bool), compat_bool E.eq f -> In x (filter f s) -> In x s. Proof. - intros s x f; unfold filter; case M.filter; intuition. - generalize (i (compat_P_aux H)); firstorder. + intros s x f; unfold filter; case M.filter as (x0,Hiff); intuition. + generalize (Hiff (compat_P_aux H)); firstorder. Qed. Lemma filter_2 : forall (s : t) (x : elt) (f : elt -> bool), compat_bool E.eq f -> In x (filter f s) -> f x = true. Proof. - intros s x f; unfold filter; case M.filter; intuition. - generalize (i (compat_P_aux H)); firstorder. + intros s x f; unfold filter; case M.filter as (x0,Hiff); intuition. + generalize (Hiff (compat_P_aux H)); firstorder. Qed. Lemma filter_3 : forall (s : t) (x : elt) (f : elt -> bool), compat_bool E.eq f -> In x s -> f x = true -> In x (filter f s). Proof. - intros s x f; unfold filter; case M.filter; intuition. - generalize (i (compat_P_aux H)); firstorder. + intros s x f; unfold filter; case M.filter as (x0,Hiff); intuition. + generalize (Hiff (compat_P_aux H)); firstorder. Qed. Definition for_all (f : elt -> bool) (s : t) : bool := -- cgit v1.2.3