From 4d542bc7eafadb16b845cf05d1eb4988eb55ed0f Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Tue, 20 Oct 2015 13:32:18 +0200 Subject: Updated PR by removing whitespaces. Bug 17450. --- lib/Maps.v | 226 ++++++++++++++++++++++++++++++------------------------------- 1 file changed, 113 insertions(+), 113 deletions(-) (limited to 'lib/Maps.v') diff --git a/lib/Maps.v b/lib/Maps.v index 63ac0c09..39fec9fd 100644 --- a/lib/Maps.v +++ b/lib/Maps.v @@ -126,7 +126,7 @@ Module Type TREE. forall (A: Type) (m: t A) (i: elt) (v: A), In (i, v) (elements m) -> get i m = Some v. Hypothesis elements_keys_norepet: - forall (A: Type) (m: t A), + forall (A: Type) (m: t A), list_norepet (List.map (@fst elt A) (elements m)). Hypothesis elements_extensional: forall (A: Type) (m n: t A), @@ -396,7 +396,7 @@ Module PTree <: TREE. generalize (H xH); simpl; congruence. destruct (andb_prop _ _ H). rewrite IHm1 in H0. rewrite IHm2 in H1. destruct x; simpl; auto. - apply andb_true_intro; split. + apply andb_true_intro; split. apply IHm1. intros; apply (H (xO x)). apply IHm2. intros; apply (H (xI x)). Qed. @@ -414,18 +414,18 @@ Module PTree <: TREE. induction m1; intros. - simpl. rewrite bempty_correct. split; intros. rewrite gleaf. rewrite H. auto. - generalize (H x). rewrite gleaf. destruct (get x m2); tauto. + generalize (H x). rewrite gleaf. destruct (get x m2); tauto. - destruct m2. + unfold beq. rewrite bempty_correct. split; intros. rewrite H. rewrite gleaf. auto. generalize (H x). rewrite gleaf. destruct (get x (Node m1_1 o m1_2)); tauto. + simpl. split; intros. * destruct (andb_prop _ _ H). destruct (andb_prop _ _ H0). - rewrite IHm1_1 in H3. rewrite IHm1_2 in H1. + rewrite IHm1_1 in H3. rewrite IHm1_2 in H1. destruct x; simpl. apply H1. apply H3. destruct o; destruct o0; auto || congruence. * apply andb_true_intro. split. apply andb_true_intro. split. - generalize (H xH); simpl. destruct o; destruct o0; tauto. + generalize (H xH); simpl. destruct o; destruct o0; tauto. apply IHm1_1. intros; apply (H (xO x)). apply IHm1_2. intros; apply (H (xI x)). Qed. @@ -450,7 +450,7 @@ Module PTree <: TREE. intros j. simpl. rewrite IH. reflexivity. intros j. simpl. rewrite IH. reflexivity. Qed. - + Lemma prev_involutive i : prev (prev i) = i. Proof (prev_append_prev i xH). @@ -513,7 +513,7 @@ Module PTree <: TREE. forall (A: Type) (l r: t A) (x: option A) (i: positive), get i (Node' l x r) = get i (Node l x r). Proof. - intros. unfold Node'. + intros. unfold Node'. destruct l; destruct x; destruct r; auto. destruct i; simpl; auto; rewrite gleaf; auto. Qed. @@ -531,9 +531,9 @@ Module PTree <: TREE. get i (filter1 pred m) = match get i m with None => None | Some x => if pred x then Some x else None end. Proof. - intros until m. revert m i. induction m; simpl; intros. + intros until m. revert m i. induction m; simpl; intros. rewrite gleaf; auto. - rewrite gnode'. destruct i; simpl; auto. destruct o; auto. + rewrite gnode'. destruct i; simpl; auto. destruct o; auto. Qed. Section COMBINE. @@ -589,7 +589,7 @@ Module PTree <: TREE. induction m1; intros; simpl. rewrite gleaf. apply xgcombine_r. destruct m2; simpl. - rewrite gleaf. rewrite <- xgcombine_l. auto. + rewrite gleaf. rewrite <- xgcombine_l. auto. repeat rewrite gnode'. destruct i; simpl; auto. Qed. @@ -622,10 +622,10 @@ Module PTree <: TREE. auto. rewrite IHm1_1. rewrite IHm1_2. - auto. + auto. Qed. - Fixpoint xelements (A : Type) (m : t A) (i : positive) + Fixpoint xelements (A : Type) (m : t A) (i : positive) (k: list (positive * A)) {struct m} : list (positive * A) := match m with @@ -651,7 +651,7 @@ Module PTree <: TREE. Remark xelements_leaf: forall A i, xelements (@Leaf A) i nil = nil. Proof. - intros; reflexivity. + intros; reflexivity. Qed. Remark xelements_node: @@ -685,8 +685,8 @@ Module PTree <: TREE. apply xelements_incl. right. auto. auto. inv H. apply xelements_incl. left. reflexivity. - apply xelements_incl. auto. - auto. + apply xelements_incl. auto. + auto. inv H. Qed. @@ -694,7 +694,7 @@ Module PTree <: TREE. forall (A: Type) (m: t A) (i: positive) (v: A), get i m = Some v -> In (i, v) (elements m). Proof. - intros A m i v H. + intros A m i v H. generalize (xelements_correct m i xH nil H). rewrite prev_append_prev. exact id. Qed. @@ -703,11 +703,11 @@ Module PTree <: TREE. In (k, v) (xelements m i nil) -> exists j, k = prev (prev_append j i) /\ get j m = Some v. Proof. - induction m; intros. + induction m; intros. - rewrite xelements_leaf in H. contradiction. - rewrite xelements_node in H. rewrite ! in_app_iff in H. destruct H as [P | [P | P]]. + exploit IHm1; eauto. intros (j & Q & R). exists (xO j); auto. - + destruct o; simpl in P; intuition auto. inv H. exists xH; auto. + + destruct o; simpl in P; intuition auto. inv H. exists xH; auto. + exploit IHm2; eauto. intros (j & Q & R). exists (xI j); auto. Qed. @@ -715,8 +715,8 @@ Module PTree <: TREE. forall (A: Type) (m: t A) (i: positive) (v: A), In (i, v) (elements m) -> get i m = Some v. Proof. - unfold elements. intros A m i v H. exploit in_xelements; eauto. intros (j & P & Q). - rewrite prev_append_prev in P. change i with (prev_append 1 i) in P. + unfold elements. intros A m i v H. exploit in_xelements; eauto. intros (j & P & Q). + rewrite prev_append_prev in P. change i with (prev_append 1 i) in P. exploit prev_append_inj; eauto. intros; congruence. Qed. @@ -726,7 +726,7 @@ Module PTree <: TREE. Remark xkeys_leaf: forall A i, xkeys (@Leaf A) i = nil. Proof. - intros; reflexivity. + intros; reflexivity. Qed. Remark xkeys_node: @@ -736,7 +736,7 @@ Module PTree <: TREE. ++ match o with None => nil | Some v => prev i :: nil end ++ xkeys m2 (xI i). Proof. - intros. unfold xkeys. rewrite xelements_node. rewrite ! map_app. destruct o; auto. + intros. unfold xkeys. rewrite xelements_node. rewrite ! map_app. destruct o; auto. Qed. Lemma in_xkeys: @@ -746,7 +746,7 @@ Module PTree <: TREE. Proof. unfold xkeys; intros. apply (list_in_map_inv) in H. destruct H as ((j, v) & -> & H). - exploit in_xelements; eauto. intros (k & P & Q). exists k; auto. + exploit in_xelements; eauto. intros (k & P & Q). exists k; auto. Qed. Lemma xelements_keys_norepet: @@ -756,26 +756,26 @@ Module PTree <: TREE. induction m; intros. - rewrite xkeys_leaf; constructor. - assert (NOTIN1: ~ In (prev i) (xkeys m1 (xO i))). - { red; intros. exploit in_xkeys; eauto. intros (j & EQ). + { red; intros. exploit in_xkeys; eauto. intros (j & EQ). rewrite prev_append_prev in EQ. simpl in EQ. apply prev_append_inj in EQ. discriminate. } assert (NOTIN2: ~ In (prev i) (xkeys m2 (xI i))). - { red; intros. exploit in_xkeys; eauto. intros (j & EQ). + { red; intros. exploit in_xkeys; eauto. intros (j & EQ). rewrite prev_append_prev in EQ. simpl in EQ. apply prev_append_inj in EQ. discriminate. } assert (DISJ: forall x, In x (xkeys m1 (xO i)) -> In x (xkeys m2 (xI i)) -> False). - { intros. exploit in_xkeys. eexact H. intros (j1 & EQ1). - exploit in_xkeys. eexact H0. intros (j2 & EQ2). + { intros. exploit in_xkeys. eexact H. intros (j1 & EQ1). + exploit in_xkeys. eexact H0. intros (j2 & EQ2). rewrite prev_append_prev in *. simpl in *. rewrite EQ2 in EQ1. apply prev_append_inj in EQ1. discriminate. } - rewrite xkeys_node. apply list_norepet_append. auto. + rewrite xkeys_node. apply list_norepet_append. auto. destruct o; simpl; auto. constructor; auto. - red; intros. red; intros; subst y. destruct o; simpl in H0. - destruct H0. subst x. tauto. eauto. eauto. + red; intros. red; intros; subst y. destruct o; simpl in H0. + destruct H0. subst x. tauto. eauto. eauto. Qed. Theorem elements_keys_norepet: - forall (A: Type) (m: t A), + forall (A: Type) (m: t A), list_norepet (List.map (@fst elt A) (elements m)). Proof. - intros. apply (xelements_keys_norepet m xH). + intros. apply (xelements_keys_norepet m xH). Qed. Remark xelements_empty: @@ -783,7 +783,7 @@ Module PTree <: TREE. Proof. induction m; intros. auto. - rewrite xelements_node. rewrite IHm1, IHm2. destruct o; auto. + rewrite xelements_node. rewrite IHm1, IHm2. destruct o; auto. generalize (H xH); simpl; congruence. intros. apply (H (xI i0)). intros. apply (H (xO i0)). @@ -806,29 +806,29 @@ Module PTree <: TREE. (xelements m j nil) (xelements n j nil)). { induction m; intros. - - rewrite xelements_leaf. rewrite xelements_empty. constructor. - intros. destruct (get i n) eqn:E; auto. exploit H0; eauto. + - rewrite xelements_leaf. rewrite xelements_empty. constructor. + intros. destruct (get i n) eqn:E; auto. exploit H0; eauto. intros [x [P Q]]. rewrite gleaf in P; congruence. - - destruct n as [ | n1 o' n2 ]. + - destruct n as [ | n1 o' n2 ]. + rewrite xelements_leaf, xelements_empty. constructor. - intros. destruct (get i (Node m1 o m2)) eqn:E; auto. exploit H; eauto. + intros. destruct (get i (Node m1 o m2)) eqn:E; auto. exploit H; eauto. intros [x [P Q]]. rewrite gleaf in P; congruence. + rewrite ! xelements_node. apply list_forall2_app. - apply IHm1. - intros. apply (H (xO i) x); auto. + apply IHm1. + intros. apply (H (xO i) x); auto. intros. apply (H0 (xO i) y); auto. - apply list_forall2_app. + apply list_forall2_app. destruct o, o'. - destruct (H xH a) as [x [P Q]]. auto. simpl in P. inv P. + destruct (H xH a) as [x [P Q]]. auto. simpl in P. inv P. constructor. auto. constructor. destruct (H xH a) as [x [P Q]]. auto. simpl in P. inv P. destruct (H0 xH b) as [x [P Q]]. auto. simpl in P. inv P. constructor. - apply IHm2. - intros. apply (H (xI i) x); auto. + apply IHm2. + intros. apply (H (xI i) x); auto. intros. apply (H0 (xI i) y); auto. } - intros. apply H with (j := xH); auto. + intros. apply H with (j := xH); auto. Qed. Theorem elements_extensional: @@ -836,8 +836,8 @@ Module PTree <: TREE. (forall i, get i m = get i n) -> elements m = elements n. Proof. - intros. - exploit (elements_canonical_order (fun (x y: A) => x = y) m n). + intros. + exploit (elements_canonical_order (fun (x y: A) => x = y) m n). intros. rewrite H in H0. exists x; auto. intros. rewrite <- H in H0. exists y; auto. induction 1. auto. destruct a1 as [a2 a3]; destruct b1 as [b2 b3]; simpl in *. @@ -862,8 +862,8 @@ Module PTree <: TREE. { destruct i; simpl remove. destruct m1; auto. destruct o; auto. destruct (remove i m2); auto. - destruct o; auto. destruct m2; auto. destruct (remove i m1); auto. - destruct m1; auto. destruct m2; auto. + destruct o; auto. destruct m2; auto. destruct (remove i m1); auto. + destruct m1; auto. destruct m2; auto. } rewrite REMOVE. destruct i; simpl in H. + destruct (IHm2 i (xI j) H) as (l1 & l2 & EQ & EQ'). @@ -883,7 +883,7 @@ Module PTree <: TREE. rewrite xelements_node, EQ', ! app_ass. auto. + subst o. exists (xelements m1 (xO j) nil); exists (xelements m2 (xI j) nil); split. rewrite xelements_node. rewrite prev_append_prev. auto. - rewrite xelements_node; auto. + rewrite xelements_node; auto. Qed. Theorem elements_remove: @@ -891,8 +891,8 @@ Module PTree <: TREE. get i m = Some v -> exists l1 l2, elements m = l1 ++ (i,v) :: l2 /\ elements (remove i m) = l1 ++ l2. Proof. - intros. exploit xelements_remove. eauto. instantiate (1 := xH). - rewrite prev_append_prev. auto. + intros. exploit xelements_remove. eauto. instantiate (1 := xH). + rewrite prev_append_prev. auto. Qed. Fixpoint xfold (A B: Type) (f: B -> positive -> A -> B) @@ -920,7 +920,7 @@ Module PTree <: TREE. simpl. auto. destruct o; simpl. rewrite <- IHm1. simpl. rewrite <- IHm2. auto. - rewrite <- IHm1. rewrite <- IHm2. auto. + rewrite <- IHm1. rewrite <- IHm2. auto. Qed. Theorem fold_spec: @@ -928,7 +928,7 @@ Module PTree <: TREE. fold f m v = List.fold_left (fun a p => f a (fst p) (snd p)) (elements m) v. Proof. - intros. unfold fold, elements. rewrite <- xfold_xelements. auto. + intros. unfold fold, elements. rewrite <- xfold_xelements. auto. Qed. Fixpoint fold1 (A B: Type) (f: B -> A -> B) (m: t A) (v: B) {struct m} : B := @@ -952,7 +952,7 @@ Module PTree <: TREE. simpl. auto. destruct o; simpl. rewrite <- IHm1. simpl. rewrite <- IHm2. auto. - rewrite <- IHm1. rewrite <- IHm2. auto. + rewrite <- IHm1. rewrite <- IHm2. auto. Qed. Theorem fold1_spec: @@ -960,7 +960,7 @@ Module PTree <: TREE. fold1 f m v = List.fold_left (fun a p => f a (snd p)) (elements m) v. Proof. - intros. apply fold1_xelements with (l := @nil (positive * A)). + intros. apply fold1_xelements with (l := @nil (positive * A)). Qed. End PTree. @@ -1064,7 +1064,7 @@ Module IMap(X: INDEXED_TYPE). Lemma gi: forall (A: Type) (x: A) (i: X.t), get i (init x) = x. Proof. - intros. unfold get, init. apply PMap.gi. + intros. unfold get, init. apply PMap.gi. Qed. Lemma gss: @@ -1077,19 +1077,19 @@ Module IMap(X: INDEXED_TYPE). forall (A: Type) (i j: X.t) (x: A) (m: t A), i <> j -> get i (set j x m) = get i m. Proof. - intros. unfold get, set. apply PMap.gso. - red. intro. apply H. apply X.index_inj; auto. + intros. unfold get, set. apply PMap.gso. + red. intro. apply H. apply X.index_inj; auto. Qed. Lemma gsspec: forall (A: Type) (i j: X.t) (x: A) (m: t A), get i (set j x m) = if X.eq i j then x else get i m. Proof. - intros. unfold get, set. + intros. unfold get, set. rewrite PMap.gsspec. case (X.eq i j); intro. subst j. rewrite peq_true. reflexivity. - rewrite peq_false. reflexivity. + rewrite peq_false. reflexivity. red; intro. elim n. apply X.index_inj; auto. Qed. @@ -1097,7 +1097,7 @@ Module IMap(X: INDEXED_TYPE). forall (A B: Type) (f: A -> B) (i: X.t) (m: t A), get i (map f m) = f(get i m). Proof. - intros. unfold map, get. apply PMap.gmap. + intros. unfold map, get. apply PMap.gmap. Qed. Lemma set2: @@ -1225,7 +1225,7 @@ Hypothesis P_compat: (forall x, T.get x m = T.get x m') -> P m a -> P m' a. -Hypothesis H_base: +Hypothesis H_base: P (T.empty _) init. Hypothesis H_rec: @@ -1253,23 +1253,23 @@ Remark H_rec': P' l a -> P' (l ++ (k, v) :: nil) (f a k v). Proof. - unfold P'; intros. - set (m0 := T.remove k m). + unfold P'; intros. + set (m0 := T.remove k m). apply P_compat with (T.set k v m0). intros. unfold m0. rewrite T.gsspec. destruct (T.elt_eq x k). symmetry. apply T.elements_complete. rewrite <- (H2 (x, v)). apply in_or_app. simpl. intuition congruence. apply T.gro. auto. - apply H_rec. unfold m0. apply T.grs. apply T.elements_complete. auto. - apply H1. red. intros [k' v']. - split; intros. - apply T.elements_correct. unfold m0. rewrite T.gro. apply T.elements_complete. - rewrite <- (H2 (k', v')). apply in_or_app. auto. + apply H_rec. unfold m0. apply T.grs. apply T.elements_complete. auto. + apply H1. red. intros [k' v']. + split; intros. + apply T.elements_correct. unfold m0. rewrite T.gro. apply T.elements_complete. + rewrite <- (H2 (k', v')). apply in_or_app. auto. red; intro; subst k'. elim H. change k with (fst (k, v')). apply in_map. auto. assert (T.get k' m0 = Some v'). apply T.elements_complete. auto. unfold m0 in H4. rewrite T.grspec in H4. destruct (T.elt_eq k' k). congruence. assert (In (k', v') (T.elements m)). apply T.elements_correct; auto. - rewrite <- (H2 (k', v')) in H5. destruct (in_app_or _ _ _ H5). auto. + rewrite <- (H2 (k', v')) in H5. destruct (in_app_or _ _ _ H5). auto. simpl in H6. intuition congruence. Qed. @@ -1282,10 +1282,10 @@ Lemma fold_rec_aux: Proof. induction l1; intros; simpl. rewrite <- List.app_nil_end. auto. - destruct a as [k v]; simpl in *. inv H1. + destruct a as [k v]; simpl in *. inv H1. change ((k, v) :: l1) with (((k, v) :: nil) ++ l1). rewrite <- List.app_ass. apply IHl1. rewrite app_ass. auto. - red; intros. rewrite map_app in H3. destruct (in_app_or _ _ _ H3). apply H0; auto with coqlib. + red; intros. rewrite map_app in H3. destruct (in_app_or _ _ _ H3). apply H0; auto with coqlib. simpl in H4. intuition congruence. auto. unfold f'. simpl. apply H_rec'; auto. eapply list_disjoint_notin; eauto with coqlib. @@ -1300,8 +1300,8 @@ Proof. apply fold_rec_aux. simpl. red; intros; tauto. simpl. red; intros. elim H0. - apply T.elements_keys_norepet. - apply H_base'. + apply T.elements_keys_norepet. + apply H_base'. simpl in H. red in H. apply H. red; intros. tauto. Qed. @@ -1319,18 +1319,18 @@ Theorem cardinal_remove: forall x m y, T.get x m = Some y -> (cardinal (T.remove x m) < cardinal m)%nat. Proof. unfold cardinal; intros. - exploit T.elements_remove; eauto. intros (l1 & l2 & P & Q). + exploit T.elements_remove; eauto. intros (l1 & l2 & P & Q). rewrite P, Q. rewrite ! app_length. simpl. omega. Qed. Theorem cardinal_set: forall x m y, T.get x m = None -> (cardinal m < cardinal (T.set x y m))%nat. Proof. - intros. set (m' := T.set x y m). - replace (cardinal m) with (cardinal (T.remove x m')). - apply cardinal_remove with y. unfold m'; apply T.gss. - unfold cardinal. f_equal. apply T.elements_extensional. - intros. unfold m'. rewrite T.grspec, T.gsspec. + intros. set (m' := T.set x y m). + replace (cardinal m) with (cardinal (T.remove x m')). + apply cardinal_remove with y. unfold m'; apply T.gss. + unfold cardinal. f_equal. apply T.elements_extensional. + intros. unfold m'. rewrite T.grspec, T.gsspec. destruct (T.elt_eq i x); auto. congruence. Qed. @@ -1352,16 +1352,16 @@ Proof. intros m0 f. unfold for_all. apply fold_rec; intros. - (* Extensionality *) - rewrite H0. split; intros. rewrite <- H in H2; auto. rewrite H in H2; auto. + rewrite H0. split; intros. rewrite <- H in H2; auto. rewrite H in H2; auto. - (* Base case *) split; intros. rewrite T.gempty in H0; congruence. auto. - (* Inductive case *) split; intros. - destruct (andb_prop _ _ H2). rewrite T.gsspec in H3. destruct (T.elt_eq x k). + destruct (andb_prop _ _ H2). rewrite T.gsspec in H3. destruct (T.elt_eq x k). inv H3. auto. apply H1; auto. - apply andb_true_intro. split. - rewrite H1. intros. apply H2. rewrite T.gso; auto. congruence. + apply andb_true_intro. split. + rewrite H1. intros. apply H2. rewrite T.gso; auto. congruence. apply H2. apply T.gss. Qed. @@ -1375,7 +1375,7 @@ Proof. intros m0 f. unfold exists_. apply fold_rec; intros. - (* Extensionality *) - rewrite H0. split; intros (x0 & a0 & P & Q); exists x0; exists a0; split; auto; congruence. + rewrite H0. split; intros (x0 & a0 & P & Q); exists x0; exists a0; split; auto; congruence. - (* Base case *) split; intros. congruence. destruct H as (x & a & P & Q). rewrite T.gempty in P; congruence. - (* Inductive case *) @@ -1383,7 +1383,7 @@ Proof. destruct (orb_true_elim _ _ H2). rewrite H1 in e. destruct e as (x1 & a1 & P & Q). exists x1; exists a1; split; auto. rewrite T.gso; auto. congruence. - exists k; exists v; split; auto. apply T.gss. + exists k; exists v; split; auto. apply T.gss. destruct H2 as (x1 & a1 & P & Q). apply orb_true_intro. rewrite T.gsspec in P. destruct (T.elt_eq x1 k). inv P. right; auto. @@ -1394,11 +1394,11 @@ Remark exists_for_all: forall m f, exists_ m f = negb (for_all m (fun x a => negb (f x a))). Proof. - intros. unfold exists_, for_all. rewrite ! T.fold_spec. - change false with (negb true). generalize (T.elements m) true. + intros. unfold exists_, for_all. rewrite ! T.fold_spec. + change false with (negb true). generalize (T.elements m) true. induction l; simpl; intros. auto. - rewrite <- IHl. f_equal. + rewrite <- IHl. f_equal. destruct b; destruct (f (fst a) (snd a)); reflexivity. Qed. @@ -1406,11 +1406,11 @@ Remark for_all_exists: forall m f, for_all m f = negb (exists_ m (fun x a => negb (f x a))). Proof. - intros. unfold exists_, for_all. rewrite ! T.fold_spec. - change true with (negb false). generalize (T.elements m) false. + intros. unfold exists_, for_all. rewrite ! T.fold_spec. + change true with (negb false). generalize (T.elements m) false. induction l; simpl; intros. auto. - rewrite <- IHl. f_equal. + rewrite <- IHl. f_equal. destruct b; destruct (f (fst a) (snd a)); reflexivity. Qed. @@ -1418,20 +1418,20 @@ Lemma for_all_false: forall m f, for_all m f = false <-> (exists x a, T.get x m = Some a /\ f x a = false). Proof. - intros. rewrite for_all_exists. - rewrite negb_false_iff. rewrite exists_correct. - split; intros (x & a & P & Q); exists x; exists a; split; auto. + intros. rewrite for_all_exists. + rewrite negb_false_iff. rewrite exists_correct. + split; intros (x & a & P & Q); exists x; exists a; split; auto. rewrite negb_true_iff in Q. auto. - rewrite Q; auto. + rewrite Q; auto. Qed. Lemma exists_false: forall m f, exists_ m f = false <-> (forall x a, T.get x m = Some a -> f x a = false). Proof. - intros. rewrite exists_for_all. + intros. rewrite exists_for_all. rewrite negb_false_iff. rewrite for_all_correct. - split; intros. apply H in H0. rewrite negb_true_iff in H0. auto. rewrite H; auto. + split; intros. apply H in H0. rewrite negb_true_iff in H0. auto. rewrite H; auto. Qed. End FORALL_EXISTS. @@ -1457,20 +1457,20 @@ Proof. set (p1 := fun x a1 => match T.get x m2 with None => false | Some a2 => beqA a1 a2 end). set (p2 := fun x a2 => match T.get x m1 with None => false | Some a1 => beqA a1 a2 end). destruct (for_all m1 p1) eqn:F1; [destruct (for_all m2 p2) eqn:F2 | idtac]. - + cut (T.beq beqA m1 m2 = true). congruence. - rewrite for_all_correct in *. rewrite T.beq_correct; intros. - destruct (T.get x m1) as [a1|] eqn:X1. + + cut (T.beq beqA m1 m2 = true). congruence. + rewrite for_all_correct in *. rewrite T.beq_correct; intros. + destruct (T.get x m1) as [a1|] eqn:X1. generalize (F1 _ _ X1). unfold p1. destruct (T.get x m2); congruence. destruct (T.get x m2) as [a2|] eqn:X2; auto. - generalize (F2 _ _ X2). unfold p2. rewrite X1. congruence. + generalize (F2 _ _ X2). unfold p2. rewrite X1. congruence. + rewrite for_all_false in F2. destruct F2 as (x & a & P & Q). - exists x. rewrite P. unfold p2 in Q. destruct (T.get x m1); auto. + exists x. rewrite P. unfold p2 in Q. destruct (T.get x m1); auto. + rewrite for_all_false in F1. destruct F1 as (x & a & P & Q). exists x. rewrite P. unfold p1 in Q. destruct (T.get x m2); auto. - (* existence -> beq = false *) destruct H as [x P]. - destruct (T.beq beqA m1 m2) eqn:E; auto. - rewrite T.beq_correct in E. + destruct (T.beq beqA m1 m2) eqn:E; auto. + rewrite T.beq_correct in E. generalize (E x). destruct (T.get x m1); destruct (T.get x m2); tauto || congruence. Qed. @@ -1493,7 +1493,7 @@ Definition Equal (m1 m2: T.t A) : Prop := Lemma Equal_refl: forall m, Equal m m. Proof. - intros; red; intros. destruct (T.get x m); auto. reflexivity. + intros; red; intros. destruct (T.get x m); auto. reflexivity. Qed. Lemma Equal_sym: forall m1 m2, Equal m1 m2 -> Equal m2 m1. @@ -1505,7 +1505,7 @@ Lemma Equal_trans: forall m1 m2 m3, Equal m1 m2 -> Equal m2 m3 -> Equal m1 m3. Proof. intros; red; intros. generalize (H x) (H0 x). destruct (T.get x m1); destruct (T.get x m2); try tauto; - destruct (T.get x m3); try tauto. + destruct (T.get x m3); try tauto. intros. transitivity a0; auto. Qed. @@ -1525,15 +1525,15 @@ Program Definition Equal_dec (m1 m2: T.t A) : { m1 === m2 } + { m1 =/= m2 } := Next Obligation. rename Heq_anonymous into B. symmetry in B. rewrite T.beq_correct in B. - red; intros. generalize (B x). - destruct (T.get x m1); destruct (T.get x m2); auto. - intros. eapply proj_sumbool_true; eauto. + red; intros. generalize (B x). + destruct (T.get x m1); destruct (T.get x m2); auto. + intros. eapply proj_sumbool_true; eauto. Qed. Next Obligation. assert (T.beq (fun a1 a2 => proj_sumbool (a1 == a2)) m1 m2 = true). - apply T.beq_correct; intros. - generalize (H x). - destruct (T.get x m1); destruct (T.get x m2); try tauto. + apply T.beq_correct; intros. + generalize (H x). + destruct (T.get x m1); destruct (T.get x m2); try tauto. intros. apply proj_sumbool_is_true; auto. unfold equiv, complement in H0. congruence. Qed. -- cgit