diff options
Diffstat (limited to 'theories/FSets/FMapWeakList.v')
| -rw-r--r-- | theories/FSets/FMapWeakList.v | 27 |
1 files changed, 14 insertions, 13 deletions
diff --git a/theories/FSets/FMapWeakList.v b/theories/FSets/FMapWeakList.v index 6c1e8ca8..0f11dd7a 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] *) @@ -600,18 +601,18 @@ Definition combine_l (m:t elt)(m':t elt') : t oee' := Definition combine_r (m:t elt)(m':t elt') : t oee' := mapi (fun k e' => (find k m, Some e')) m'. -Definition fold_right_pair (A B C:Type)(f:A->B->C->C)(l:list (A*B))(i:C) := - List.fold_right (fun p => f (fst p) (snd p)) i l. +Definition fold_right_pair (A B C:Type)(f:A->B->C->C) := + List.fold_right (fun p => f (fst p) (snd p)). Definition combine (m:t elt)(m':t elt') : t oee' := let l := combine_l m m' in let r := combine_r m m' in - fold_right_pair (add (elt:=oee')) l r. + fold_right_pair (add (elt:=oee')) r l. Lemma fold_right_pair_NoDup : forall l r (Hl: NoDupA (eqk (elt:=oee')) l) (Hl: NoDupA (eqk (elt:=oee')) r), - NoDupA (eqk (elt:=oee')) (fold_right_pair (add (elt:=oee')) l r). + NoDupA (eqk (elt:=oee')) (fold_right_pair (add (elt:=oee')) r l). Proof. induction l; simpl; auto. destruct a; simpl; auto. @@ -733,7 +734,7 @@ Definition option_cons (A:Type)(k:key)(o:option A)(l:list (key*A)) := Definition map2 m m' := let m0 : t oee' := combine m m' in let m1 : t (option elt'') := map (fun p => f (fst p) (snd p)) m0 in - fold_right_pair (option_cons (A:=elt'')) m1 nil. + fold_right_pair (option_cons (A:=elt'')) nil m1. Lemma map2_NoDup : forall m (Hm:NoDupA (@eqk elt) m) m' (Hm':NoDupA (@eqk elt') m'), @@ -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. |