diff options
Diffstat (limited to 'theories/FSets/FMapList.v')
| -rw-r--r-- | theories/FSets/FMapList.v | 41 |
1 files changed, 20 insertions, 21 deletions
diff --git a/theories/FSets/FMapList.v b/theories/FSets/FMapList.v index f15ab222..13cb559b 100644 --- a/theories/FSets/FMapList.v +++ b/theories/FSets/FMapList.v @@ -403,7 +403,7 @@ Proof. apply H1 with k; destruct (X.eq_dec x k); auto. - destruct (X.compare x x'); try contradiction; clear y. + destruct (X.compare x x') as [Hlt|Heq|Hlt]; try contradiction; clear y. destruct (H0 x). assert (In x ((x',e')::l')). apply H; auto. @@ -527,7 +527,7 @@ Fixpoint mapi (f: key -> elt -> elt') (m:t elt) : t elt' := | nil => nil | (k,e)::m' => (k,f k e) :: mapi f m' end. - + End Elt. Section Elt2. (* A new section is necessary for previous definitions to work @@ -543,14 +543,13 @@ Proof. intros m x e f. (* functional induction map elt elt' f m. *) (* Marche pas ??? *) induction m. - inversion 1. + inversion 1. destruct a as (x',e'). simpl. - inversion_clear 1. + inversion_clear 1. constructor 1. unfold eqke in *; simpl in *; intuition congruence. - constructor 2. unfold MapsTo in *; auto. Qed. @@ -799,7 +798,7 @@ Proof. intros. simpl. destruct a as (k,e); destruct a0 as (k',e'). - destruct (X.compare k k'). + destruct (X.compare k k') as [Hlt|Heq|Hlt]. inversion_clear Hm. constructor; auto. assert (lelistA (ltk (elt:=elt')) (k, e') ((k',e')::m')) by auto. @@ -868,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. @@ -923,7 +922,7 @@ Proof. destruct o; destruct o'; simpl in *; try discriminate; auto. destruct a as (k,(oo,oo')); simpl in *. inversion_clear H2. - destruct (X.compare x k); simpl in *. + destruct (X.compare x k) as [Hlt|Heq|Hlt]; simpl in *. (* x < k *) destruct (f' (oo,oo')); simpl. elim_comp. @@ -959,7 +958,7 @@ Proof. destruct a as (k,(oo,oo')). simpl. inversion_clear H2. - destruct (X.compare x k). + destruct (X.compare x k) as [Hlt|Heq|Hlt]. (* x < k *) unfold f'; simpl. destruct (f oo oo'); simpl. @@ -1208,7 +1207,7 @@ Proof. destruct a as (x,e). destruct p as (x',e'). unfold equal; simpl. - destruct (X.compare x x'); simpl; intuition. + destruct (X.compare x x') as [Hlt|Heq|Hlt]; simpl; intuition. unfold cmp at 1. MD.elim_comp; clear H; simpl. inversion_clear Hl. @@ -1245,21 +1244,21 @@ 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|Heq|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; try destruct a as (x,e); try destruct p as (x',e'); auto. - destruct (X.compare x x'); MapS.Raw.MX.elim_comp; intuition. + destruct (X.compare x x') as [Hlt|Heq|Hlt]; MapS.Raw.MX.elim_comp; intuition. inversion_clear Hm; inversion_clear Hm'. apply (IHm H0 (Build_slist H4)); auto. Qed. @@ -1272,8 +1271,8 @@ Proof. try destruct a as (x,e); try destruct p as (x',e'); try destruct p0 as (x'',e''); try contradiction; auto. - destruct (X.compare x x'); - destruct (X.compare x' x''); + destruct (X.compare x x') as [Hlt|Heq|Hlt]; + destruct (X.compare x' x'') as [Hlt'|Heq'|Hlt']; MapS.Raw.MX.elim_comp; intuition. apply D.eq_trans with e'; auto. inversion_clear Hm1; inversion_clear Hm2; inversion_clear Hm3. @@ -1288,8 +1287,8 @@ Proof. try destruct a as (x,e); try destruct p as (x',e'); try destruct p0 as (x'',e''); try contradiction; auto. - destruct (X.compare x x'); - destruct (X.compare x' x''); + destruct (X.compare x x') as [Hlt|Heq|Hlt]; + destruct (X.compare x' x'') as [Hlt'|Heq'|Hlt']; MapS.Raw.MX.elim_comp; intuition. left; apply D.lt_trans with e'; auto. left; apply lt_eq with e'; auto. @@ -1307,7 +1306,7 @@ Proof. intros (m2, Hm2); destruct m2; unfold eq, lt; simpl; try destruct a as (x,e); try destruct p as (x',e'); try contradiction; auto. - destruct (X.compare x x'); auto. + destruct (X.compare x x') as [Hlt|Heq|Hlt]; auto. intuition. exact (D.lt_not_eq H0 H1). inversion_clear Hm1; inversion_clear Hm2. |