diff options
Diffstat (limited to 'theories/FSets')
| -rw-r--r-- | theories/FSets/FMapAVL.v | 62 | ||||
| -rw-r--r-- | theories/FSets/FMapFacts.v | 72 | ||||
| -rw-r--r-- | theories/FSets/FMapFullAVL.v | 12 | ||||
| -rw-r--r-- | theories/FSets/FMapList.v | 41 | ||||
| -rw-r--r-- | theories/FSets/FMapPositive.v | 119 | ||||
| -rw-r--r-- | theories/FSets/FMapWeakList.v | 27 | ||||
| -rw-r--r-- | theories/FSets/FSetBridge.v | 20 | ||||
| -rw-r--r-- | theories/FSets/FSetCompat.v | 2 | ||||
| -rw-r--r-- | theories/FSets/FSetDecide.v | 6 | ||||
| -rw-r--r-- | theories/FSets/FSetEqProperties.v | 2 | ||||
| -rw-r--r-- | theories/FSets/FSetInterface.v | 2 | ||||
| -rw-r--r-- | theories/FSets/FSetPositive.v | 95 | ||||
| -rw-r--r-- | theories/FSets/FSetProperties.v | 3 |
13 files changed, 233 insertions, 230 deletions
diff --git a/theories/FSets/FMapAVL.v b/theories/FSets/FMapAVL.v index c68216e6..c9e5b8dd 100644 --- a/theories/FSets/FMapAVL.v +++ b/theories/FSets/FMapAVL.v @@ -270,7 +270,7 @@ Fixpoint elements_aux (acc : list (key*elt)) m : list (key*elt) := | Node l x d r _ => elements_aux ((x,d) :: elements_aux acc r) l end. -(** then [elements] is an instanciation with an empty [acc] *) +(** then [elements] is an instantiation with an empty [acc] *) Definition elements := elements_aux nil. @@ -342,7 +342,7 @@ Notation "t #r" := (t_right t) (at level 9, format "t '#r'"). Fixpoint map (elt elt' : Type)(f : elt -> elt')(m : t elt) : t elt' := match m with - | Leaf => Leaf _ + | Leaf _ => Leaf _ | Node l x d r h => Node (map f l) x (f d) (map f r) h end. @@ -350,7 +350,7 @@ Fixpoint map (elt elt' : Type)(f : elt -> elt')(m : t elt) : t elt' := Fixpoint mapi (elt elt' : Type)(f : key -> elt -> elt')(m : t elt) : t elt' := match m with - | Leaf => Leaf _ + | Leaf _ => Leaf _ | Node l x d r h => Node (mapi f l) x (f x d) (mapi f r) h end. @@ -359,7 +359,7 @@ Fixpoint mapi (elt elt' : Type)(f : key -> elt -> elt')(m : t elt) : t elt' := Fixpoint map_option (elt elt' : Type)(f : key -> elt -> option elt')(m : t elt) : t elt' := match m with - | Leaf => Leaf _ + | Leaf _ => Leaf _ | Node l x d r h => match f x d with | Some d' => join (map_option f l) x d' (map_option f r) @@ -370,7 +370,7 @@ Fixpoint map_option (elt elt' : Type)(f : key -> elt -> option elt')(m : t elt) (** * Optimized map2 Suggestion by B. Gregoire: a [map2] function with specialized - arguments allowing to bypass some tree traversal. Instead of one + arguments that allows bypassing some tree traversal. Instead of one [f0] of type [key -> option elt -> option elt' -> option elt''], we ask here for: - [f] which is a specialisation of [f0] when first option isn't [None] @@ -389,8 +389,8 @@ Variable mapr : t elt' -> t elt''. Fixpoint map2_opt m1 m2 := match m1, m2 with - | Leaf, _ => mapr m2 - | _, Leaf => mapl m1 + | Leaf _, _ => mapr m2 + | _, Leaf _ => mapl m1 | Node l1 x1 d1 r1 h1, _ => let (l2',o2,r2') := split x1 m2 in match f x1 d1 o2 with @@ -534,7 +534,7 @@ Ltac order := match goal with | _ => MX.order end. -Ltac intuition_in := repeat progress (intuition; inv In; inv MapsTo). +Ltac intuition_in := repeat (intuition; inv In; inv MapsTo). (* Function/Functional Scheme can't deal with internal fix. Let's do its job by hand: *) @@ -1247,11 +1247,11 @@ Proof. intros m1 m2; functional induction (concat m1 m2); intros; auto; try factornode _x _x0 _x1 _x2 _x3 as m1. apply join_bst; auto. - change (bst (m2',xd)#1); rewrite <-e1; eauto. + change (bst (m2',xd)#1). rewrite <-e1; eauto. intros y Hy. apply H1; auto. rewrite remove_min_in, e1; simpl; auto. - change (gt_tree (m2',xd)#2#1 (m2',xd)#1); rewrite <-e1; eauto. + change (gt_tree (m2',xd)#2#1 (m2',xd)#1). rewrite <-e1; eauto. Qed. Hint Resolve concat_bst. @@ -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. @@ -1367,7 +1367,7 @@ Proof. induction s; simpl; intros; auto. rewrite IHs1, IHs2. unfold elements; simpl. - rewrite 2 IHs1, IHs2, <- !app_nil_end, !app_ass; auto. + rewrite 2 IHs1, IHs2, !app_nil_r, !app_ass; auto. Qed. Lemma elements_node : @@ -1376,7 +1376,7 @@ Lemma elements_node : elements (Node t1 x e t2 z) ++ l. Proof. unfold elements; simpl; intros. - rewrite !elements_app, <- !app_nil_end, !app_ass; auto. + rewrite !elements_app, !app_nil_r, !app_ass; auto. Qed. (** * Fold *) @@ -1424,7 +1424,7 @@ Qed. i.e. the list of elements actually compared *) Fixpoint flatten_e (e : enumeration elt) : list (key*elt) := match e with - | End => nil + | End _ => nil | More x e t r => (x,e) :: elements t ++ flatten_e r end. @@ -1433,14 +1433,14 @@ Lemma flatten_e_elements : elements l ++ flatten_e (More x d r e) = elements (Node l x d r z) ++ flatten_e e. Proof. - intros; simpl; apply elements_node. + intros; apply elements_node. Qed. Lemma cons_1 : forall (s:t elt) e, flatten_e (cons s e) = elements s ++ flatten_e e. Proof. - induction s; simpl; auto; intros. - rewrite IHs1; apply flatten_e_elements; auto. + induction s; auto; intros. + simpl flatten_e; rewrite IHs1; apply flatten_e_elements; auto. Qed. (** Proof of correction for the comparison *) @@ -1478,7 +1478,7 @@ Lemma equal_cont_IfEq : forall m1 cont e2 l, (forall e, IfEq (cont e) l (flatten_e e)) -> IfEq (equal_cont cmp m1 cont e2) (elements m1 ++ l) (flatten_e e2). Proof. - induction m1 as [|l1 Hl1 x1 d1 r1 Hr1 h1]; simpl; intros; auto. + induction m1 as [|l1 Hl1 x1 d1 r1 Hr1 h1]; intros; auto. rewrite <- elements_node; simpl. apply Hl1; auto. clear e2; intros [|x2 d2 r2 e2]. @@ -1491,9 +1491,9 @@ Lemma equal_IfEq : forall (m1 m2:t elt), IfEq (equal cmp m1 m2) (elements m1) (elements m2). Proof. intros; unfold equal. - rewrite (app_nil_end (elements m1)). + rewrite <- (app_nil_r (elements m1)). replace (elements m2) with (flatten_e (cons m2 (End _))) - by (rewrite cons_1; simpl; rewrite <-app_nil_end; auto). + by (rewrite cons_1; simpl; rewrite app_nil_r; auto). apply equal_cont_IfEq. intros. apply equal_end_IfEq; auto. @@ -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. @@ -1930,7 +1930,7 @@ Module IntMake (I:Int)(X: OrderedType) <: S with Module E := X. Lemma Equivb_Equivb : forall cmp m m', Equivb cmp m m' <-> Raw.Proofs.Equivb cmp m m'. Proof. - intros; unfold Equivb, Equiv, Raw.Proofs.Equivb, In; intuition. + intros; unfold Equivb, Equiv, Raw.Proofs.Equivb, In. intuition. generalize (H0 k); do 2 rewrite In_alt; intuition. generalize (H0 k); do 2 rewrite In_alt; intuition. generalize (H0 k); do 2 rewrite <- In_alt; intuition. @@ -2016,7 +2016,7 @@ Module IntMake_ord (I:Int)(X: OrderedType)(D : OrderedType) <: Definition compare_more x1 d1 (cont:R.enumeration D.t -> comparison) e2 := match e2 with - | R.End => Gt + | R.End _ => Gt | R.More x2 d2 r2 e2 => match X.compare x1 x2 with | EQ _ => match D.compare d1 d2 with @@ -2033,7 +2033,7 @@ Module IntMake_ord (I:Int)(X: OrderedType)(D : OrderedType) <: Fixpoint compare_cont s1 (cont:R.enumeration D.t -> comparison) e2 := match s1 with - | R.Leaf => cont e2 + | R.Leaf _ => cont e2 | R.Node l1 x1 d1 r1 _ => compare_cont l1 (compare_more x1 d1 (compare_cont r1 cont)) e2 end. @@ -2041,7 +2041,7 @@ Module IntMake_ord (I:Int)(X: OrderedType)(D : OrderedType) <: (** Initial continuation *) Definition compare_end (e2:R.enumeration D.t) := - match e2 with R.End => Eq | _ => Lt end. + match e2 with R.End _ => Eq | _ => Lt end. (** The complete comparison *) @@ -2084,7 +2084,7 @@ Module IntMake_ord (I:Int)(X: OrderedType)(D : OrderedType) <: (forall e, Cmp (cont e) l (P.flatten_e e)) -> Cmp (compare_cont s1 cont e2) (R.elements s1 ++ l) (P.flatten_e e2). Proof. - induction s1 as [|l1 Hl1 x1 d1 r1 Hr1 h1]; simpl; intros; auto. + induction s1 as [|l1 Hl1 x1 d1 r1 Hr1 h1]; intros; auto. rewrite <- P.elements_node; simpl. apply Hl1; auto. clear e2. intros [|x2 d2 r2 e2]. simpl; auto. @@ -2096,9 +2096,9 @@ Module IntMake_ord (I:Int)(X: OrderedType)(D : OrderedType) <: Cmp (compare_pure s1 s2) (R.elements s1) (R.elements s2). Proof. intros; unfold compare_pure. - rewrite (app_nil_end (R.elements s1)). + rewrite <- (app_nil_r (R.elements s1)). replace (R.elements s2) with (P.flatten_e (R.cons s2 (R.End _))) by - (rewrite P.cons_1; simpl; rewrite <- app_nil_end; auto). + (rewrite P.cons_1; simpl; rewrite app_nil_r; auto). auto using compare_cont_Cmp, compare_end_Cmp. Qed. diff --git a/theories/FSets/FMapFacts.v b/theories/FSets/FMapFacts.v index 0c1448c9..8c6f4b64 100644 --- a/theories/FSets/FMapFacts.v +++ b/theories/FSets/FMapFacts.v @@ -437,12 +437,6 @@ intros; do 2 rewrite mem_find_b; rewrite remove_o; unfold eqb. destruct (eq_dec x y); auto. Qed. -Definition option_map (A B:Type)(f:A->B)(o:option A) : option B := - match o with - | Some a => Some (f a) - | None => None - end. - Lemma map_o : forall m x (f:elt->elt'), find x (map f m) = option_map f (find x m). Proof. @@ -519,7 +513,7 @@ Proof. intros. rewrite eq_option_alt. intro e. rewrite <- find_mapsto_iff, elements_mapsto_iff. unfold eqb. -rewrite <- findA_NoDupA; intuition; try apply elements_3w; eauto. +rewrite <- findA_NoDupA; dintuition; try apply elements_3w; eauto. Qed. Lemma elements_b : forall m x, @@ -678,9 +672,9 @@ Qed. Add Parametric Morphism elt : (@Empty elt) with signature Equal ==> iff as Empty_m. Proof. -unfold Empty; intros m m' Hm; intuition. -rewrite <-Hm in H0; eauto. -rewrite Hm in H0; eauto. +unfold Empty; intros m m' Hm. split; intros; intro. +rewrite <-Hm in H0; eapply H, H0. +rewrite Hm in H0; eapply H, H0. Qed. Add Parametric Morphism elt : (@is_empty elt) @@ -708,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') @@ -835,8 +829,8 @@ Module WProperties_fun (E:DecidableType)(M:WSfun E). Definition uncurry {U V W : Type} (f : U -> V -> W) : U*V -> W := fun p => f (fst p) (snd p). - Definition of_list (l : list (key*elt)) := - List.fold_right (uncurry (@add _)) (empty _) l. + Definition of_list := + List.fold_right (uncurry (@add _)) (empty elt). Definition to_list := elements. @@ -867,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 -> @@ -934,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. @@ -1124,6 +1118,27 @@ Module WProperties_fun (E:DecidableType)(M:WSfun E). auto with *. Qed. + Lemma fold_Equal2 : forall m1 m2 i j, Equal m1 m2 -> eqA i j -> + eqA (fold f m1 i) (fold f m2 j). + Proof. + intros. + rewrite 2 fold_spec_right. + assert (NoDupA eqk (rev (elements m1))) by (auto with * ). + assert (NoDupA eqk (rev (elements m2))) by (auto with * ). + apply fold_right_equivlistA_restr2 with (R:=complement eqk)(eqA:=eqke) + ; auto with *. + - intros (k1,e1) (k2,e2) (Hk,He) a1 a2 Ha; simpl in *; apply Comp; auto. + - unfold complement, eq_key, eq_key_elt; repeat red. intuition eauto. + - intros (k,e) (k',e') z z' h h'; unfold eq_key, uncurry;simpl; auto. + rewrite h'. + auto. + - rewrite <- NoDupA_altdef; auto. + - intros (k,e). + rewrite 2 InA_rev, <- 2 elements_mapsto_iff, 2 find_mapsto_iff, H; + auto with *. + Qed. + + Lemma fold_Add : forall m1 m2 k e i, ~In k m1 -> Add k e m1 m2 -> eqA (fold f m2 i) (f k e (fold f m1 i)). Proof. @@ -1871,14 +1886,9 @@ Module OrdProperties (M:S). find_mapsto_iff, (H0 t0), <- find_mapsto_iff, add_mapsto_iff by (auto with *). unfold O.eqke, O.ltk; simpl. - destruct (E.compare t0 x); intuition. - right; split; auto; ME.order. - ME.order. - elim H. - exists e0; apply MapsTo_1 with t0; auto. - right; right; split; auto; ME.order. - ME.order. - right; split; auto; ME.order. + destruct (E.compare t0 x); intuition; try fold (~E.eq x t0); auto. + - elim H; exists e0; apply MapsTo_1 with t0; auto. + - fold (~E.lt t0 x); auto. Qed. Lemma elements_Add_Above : forall m m' x e, @@ -1901,7 +1911,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. @@ -1930,7 +1940,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. @@ -1986,7 +1996,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/FMapFullAVL.v b/theories/FSets/FMapFullAVL.v index e1c60351..a7be3232 100644 --- a/theories/FSets/FMapFullAVL.v +++ b/theories/FSets/FMapFullAVL.v @@ -660,7 +660,7 @@ Module IntMake_ord (I:Int)(X: OrderedType)(D : OrderedType) <: Fixpoint cardinal_e (e:Raw.enumeration D.t) := match e with - | Raw.End => 0%nat + | Raw.End _ => 0%nat | Raw.More _ _ r e => S (Raw.cardinal r + cardinal_e e) end. @@ -674,12 +674,14 @@ Module IntMake_ord (I:Int)(X: OrderedType)(D : OrderedType) <: Definition cardinal_e_2 ee := (cardinal_e (fst ee) + cardinal_e (snd ee))%nat. + Local Unset Keyed Unification. + Function compare_aux (ee:Raw.enumeration D.t * Raw.enumeration D.t) { measure cardinal_e_2 ee } : comparison := match ee with - | (Raw.End, Raw.End) => Eq - | (Raw.End, Raw.More _ _ _ _) => Lt - | (Raw.More _ _ _ _, Raw.End) => Gt + | (Raw.End _, Raw.End _) => Eq + | (Raw.End _, Raw.More _ _ _ _) => Lt + | (Raw.More _ _ _ _, Raw.End _) => Gt | (Raw.More x1 d1 r1 e1, Raw.More x2 d2 r2 e2) => match X.compare x1 x2 with | EQ _ => match D.compare d1 d2 with @@ -726,7 +728,7 @@ Module IntMake_ord (I:Int)(X: OrderedType)(D : OrderedType) <: intros. assert (H1:=cons_1 m1 (Raw.End _)). assert (H2:=cons_1 m2 (Raw.End _)). - simpl in *; rewrite <- app_nil_end in *; rewrite <-H1,<-H2. + simpl in *; rewrite app_nil_r in *; rewrite <-H1,<-H2. apply (@compare_aux_Cmp (Raw.cons m1 (Raw.End _), Raw.cons m2 (Raw.End _))). Qed. 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. diff --git a/theories/FSets/FMapPositive.v b/theories/FSets/FMapPositive.v index c59f7c22..3eac15b0 100644 --- a/theories/FSets/FMapPositive.v +++ b/theories/FSets/FMapPositive.v @@ -8,13 +8,11 @@ (** * FMapPositive : an implementation of FMapInterface for [positive] keys. *) -Require Import Bool ZArith OrderedType OrderedTypeEx FMapInterface. +Require Import Bool OrderedType ZArith OrderedType OrderedTypeEx FMapInterface. Set Implicit Arguments. Local Open Scope positive_scope. - Local Unset Elimination Schemes. -Local Unset Case Analysis Schemes. (** This file is an adaptation to the [FMap] framework of a work by Xavier Leroy and Sandrine Blazy (used for building certified compilers). @@ -71,7 +69,7 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits. Module E:=PositiveOrderedTypeBits. Module ME:=KeyOrderedType E. - Definition key := positive. + Definition key := positive : Type. Inductive tree (A : Type) := | Leaf : tree A @@ -84,7 +82,7 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits. Section A. Variable A:Type. - Arguments Leaf [A]. + Arguments Leaf {A}. Definition empty : t A := Leaf. @@ -95,7 +93,7 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits. | _ => false end. - Fixpoint find (i : positive) (m : t A) : option A := + Fixpoint find (i : key) (m : t A) : option A := match m with | Leaf => None | Node l o r => @@ -106,7 +104,7 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits. end end. - Fixpoint mem (i : positive) (m : t A) : bool := + Fixpoint mem (i : key) (m : t A) : bool := match m with | Leaf => false | Node l o r => @@ -117,7 +115,7 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits. end end. - Fixpoint add (i : positive) (v : A) (m : t A) : t A := + Fixpoint add (i : key) (v : A) (m : t A) : t A := match m with | Leaf => match i with @@ -133,7 +131,7 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits. end end. - Fixpoint remove (i : positive) (m : t A) : t A := + Fixpoint remove (i : key) (m : t A) : t A := match i with | xH => match m with @@ -165,7 +163,7 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits. (** [elements] *) - Fixpoint xelements (m : t A) (i : positive) : list (positive * A) := + Fixpoint xelements (m : t A) (i : key) : list (key * A) := match m with | Leaf => nil | Node l None r => @@ -192,33 +190,33 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits. Section CompcertSpec. Theorem gempty: - forall (i: positive), find i empty = None. + forall (i: key), find i empty = None. Proof. destruct i; simpl; auto. Qed. Theorem gss: - forall (i: positive) (x: A) (m: t A), find i (add i x m) = Some x. + forall (i: key) (x: A) (m: t A), find i (add i x m) = Some x. Proof. induction i; destruct m; simpl; auto. Qed. - Lemma gleaf : forall (i : positive), find i (Leaf : t A) = None. + Lemma gleaf : forall (i : key), find i (Leaf : t A) = None. Proof. exact gempty. Qed. Theorem gso: - forall (i j: positive) (x: A) (m: t A), + forall (i j: key) (x: A) (m: t A), i <> j -> find i (add j x m) = find i m. Proof. induction i; intros; destruct j; destruct m; simpl; try rewrite <- (gleaf i); auto; try apply IHi; congruence. Qed. - Lemma rleaf : forall (i : positive), remove i (Leaf : t A) = Leaf. + Lemma rleaf : forall (i : key), remove i Leaf = Leaf. Proof. destruct i; simpl; auto. Qed. Theorem grs: - forall (i: positive) (m: t A), find i (remove i m) = None. + forall (i: key) (m: t A), find i (remove i m) = None. Proof. induction i; destruct m. simpl; auto. @@ -238,7 +236,7 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits. Qed. Theorem gro: - forall (i j: positive) (m: t A), + forall (i j: key) (m: t A), i <> j -> find i (remove j m) = find i m. Proof. induction i; intros; destruct j; destruct m; @@ -267,11 +265,11 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits. Qed. Lemma xelements_correct: - forall (m: t A) (i j : positive) (v: A), + forall (m: t A) (i j : key) (v: A), find i m = Some v -> List.In (append j i, v) (xelements m j). Proof. induction m; intros. - rewrite (gleaf i) in H; congruence. + rewrite (gleaf i) in H; discriminate. destruct o; destruct i; simpl; simpl in H. rewrite append_assoc_1; apply in_or_app; right; apply in_cons; apply IHm2; auto. @@ -284,14 +282,14 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits. Qed. Theorem elements_correct: - forall (m: t A) (i: positive) (v: A), + forall (m: t A) (i: key) (v: A), find i m = Some v -> List.In (i, v) (elements m). Proof. intros m i v H. exact (xelements_correct m i xH H). Qed. - Fixpoint xfind (i j : positive) (m : t A) : option A := + Fixpoint xfind (i j : key) (m : t A) : option A := match i, j with | _, xH => find i m | xO ii, xO jj => xfind ii jj m @@ -300,7 +298,7 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits. end. Lemma xfind_left : - forall (j i : positive) (m1 m2 : t A) (o : option A) (v : A), + forall (j i : key) (m1 m2 : t A) (o : option A) (v : A), xfind i (append j (xO xH)) m1 = Some v -> xfind i j (Node m1 o m2) = Some v. Proof. induction j; intros; destruct i; simpl; simpl in H; auto; try congruence. @@ -308,7 +306,7 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits. Qed. Lemma xelements_ii : - forall (m: t A) (i j : positive) (v: A), + forall (m: t A) (i j : key) (v: A), List.In (xI i, v) (xelements m (xI j)) -> List.In (i, v) (xelements m j). Proof. induction m. @@ -324,7 +322,7 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits. Qed. Lemma xelements_io : - forall (m: t A) (i j : positive) (v: A), + forall (m: t A) (i j : key) (v: A), ~List.In (xI i, v) (xelements m (xO j)). Proof. induction m. @@ -339,7 +337,7 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits. Qed. Lemma xelements_oo : - forall (m: t A) (i j : positive) (v: A), + forall (m: t A) (i j : key) (v: A), List.In (xO i, v) (xelements m (xO j)) -> List.In (i, v) (xelements m j). Proof. induction m. @@ -355,7 +353,7 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits. Qed. Lemma xelements_oi : - forall (m: t A) (i j : positive) (v: A), + forall (m: t A) (i j : key) (v: A), ~List.In (xO i, v) (xelements m (xI j)). Proof. induction m. @@ -370,7 +368,7 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits. Qed. Lemma xelements_ih : - forall (m1 m2: t A) (o: option A) (i : positive) (v: A), + forall (m1 m2: t A) (o: option A) (i : key) (v: A), List.In (xI i, v) (xelements (Node m1 o m2) xH) -> List.In (i, v) (xelements m2 xH). Proof. destruct o; simpl; intros; destruct (in_app_or _ _ _ H). @@ -383,7 +381,7 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits. Qed. Lemma xelements_oh : - forall (m1 m2: t A) (o: option A) (i : positive) (v: A), + forall (m1 m2: t A) (o: option A) (i : key) (v: A), List.In (xO i, v) (xelements (Node m1 o m2) xH) -> List.In (i, v) (xelements m1 xH). Proof. destruct o; simpl; intros; destruct (in_app_or _ _ _ H). @@ -396,7 +394,7 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits. Qed. Lemma xelements_hi : - forall (m: t A) (i : positive) (v: A), + forall (m: t A) (i : key) (v: A), ~List.In (xH, v) (xelements m (xI i)). Proof. induction m; intros. @@ -411,7 +409,7 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits. Qed. Lemma xelements_ho : - forall (m: t A) (i : positive) (v: A), + forall (m: t A) (i : key) (v: A), ~List.In (xH, v) (xelements m (xO i)). Proof. induction m; intros. @@ -426,13 +424,13 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits. Qed. Lemma find_xfind_h : - forall (m: t A) (i: positive), find i m = xfind i xH m. + forall (m: t A) (i: key), find i m = xfind i xH m. Proof. destruct i; simpl; auto. Qed. Lemma xelements_complete: - forall (i j : positive) (m: t A) (v: A), + forall (i j : key) (m: t A) (v: A), List.In (i, v) (xelements m j) -> xfind i j m = Some v. Proof. induction i; simpl; intros; destruct j; simpl. @@ -460,7 +458,7 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits. Qed. Theorem elements_complete: - forall (m: t A) (i: positive) (v: A), + forall (m: t A) (i: key) (v: A), List.In (i, v) (elements m) -> find i m = Some v. Proof. intros m i v H. @@ -481,22 +479,22 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits. End CompcertSpec. - Definition MapsTo (i:positive)(v:A)(m:t A) := find i m = Some v. + Definition MapsTo (i:key)(v:A)(m:t A) := find i m = Some v. - Definition In (i:positive)(m:t A) := exists e:A, MapsTo i e m. + Definition In (i:key)(m:t A) := exists e:A, MapsTo i e m. - Definition Empty m := forall (a : positive)(e:A) , ~ MapsTo a e m. + Definition Empty m := forall (a : key)(e:A) , ~ MapsTo a e m. - Definition eq_key (p p':positive*A) := E.eq (fst p) (fst p'). + Definition eq_key (p p':key*A) := E.eq (fst p) (fst p'). - Definition eq_key_elt (p p':positive*A) := + Definition eq_key_elt (p p':key*A) := E.eq (fst p) (fst p') /\ (snd p) = (snd p'). - Definition lt_key (p p':positive*A) := E.lt (fst p) (fst p'). + Definition lt_key (p p':key*A) := E.lt (fst p) (fst p'). - Global Program Instance eqk_equiv : Equivalence eq_key. - Global Program Instance eqke_equiv : Equivalence eq_key_elt. - Global Program Instance ltk_strorder : StrictOrder lt_key. + Global Instance eqk_equiv : Equivalence eq_key := _. + Global Instance eqke_equiv : Equivalence eq_key_elt := _. + Global Instance ltk_strorder : StrictOrder lt_key := _. Lemma mem_find : forall m x, mem x m = match find x m with None => false | _ => true end. @@ -717,8 +715,8 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits. Lemma elements_3w : NoDupA eq_key (elements m). Proof. - change eq_key with (@ME.eqk A). - apply ME.Sort_NoDupA; apply elements_3; auto. + apply ME.Sort_NoDupA. + apply elements_3. Qed. End FMapSpec. @@ -729,9 +727,9 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits. Section Mapi. - Variable f : positive -> A -> B. + Variable f : key -> A -> B. - Fixpoint xmapi (m : t A) (i : positive) : t B := + Fixpoint xmapi (m : t A) (i : key) : t B := match m with | Leaf => @Leaf B | Node l o r => Node (xmapi l (append i (xO xH))) @@ -748,7 +746,7 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits. End A. Lemma xgmapi: - forall (A B: Type) (f: positive -> A -> B) (i j : positive) (m: t A), + forall (A B: Type) (f: key -> A -> B) (i j : key) (m: t A), find i (xmapi f m j) = option_map (f (append j i)) (find i m). Proof. induction i; intros; destruct m; simpl; auto. @@ -758,7 +756,7 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits. Qed. Theorem gmapi: - forall (A B: Type) (f: positive -> A -> B) (i: positive) (m: t A), + forall (A B: Type) (f: key -> A -> B) (i: key) (m: t A), find i (mapi f m) = option_map (f i) (find i m). Proof. intros. @@ -814,7 +812,7 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits. Variable A B C : Type. Variable f : option A -> option B -> option C. - Arguments Leaf [A]. + Arguments Leaf {A}. Fixpoint xmap2_l (m : t A) : t C := match m with @@ -822,7 +820,7 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits. | Node l o r => Node (xmap2_l l) (f o None) (xmap2_l r) end. - Lemma xgmap2_l : forall (i : positive) (m : t A), + Lemma xgmap2_l : forall (i : key) (m : t A), f None None = None -> find i (xmap2_l m) = f (find i m) None. Proof. induction i; intros; destruct m; simpl; auto. @@ -834,7 +832,7 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits. | Node l o r => Node (xmap2_r l) (f None o) (xmap2_r r) end. - Lemma xgmap2_r : forall (i : positive) (m : t B), + Lemma xgmap2_r : forall (i : key) (m : t B), f None None = None -> find i (xmap2_r m) = f None (find i m). Proof. induction i; intros; destruct m; simpl; auto. @@ -850,7 +848,7 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits. end end. - Lemma gmap2: forall (i: positive)(m1:t A)(m2: t B), + Lemma gmap2: forall (i: key)(m1:t A)(m2: t B), f None None = None -> find i (_map2 m1 m2) = f (find i m1) (find i m2). Proof. @@ -898,11 +896,11 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits. Section Fold. Variables A B : Type. - Variable f : positive -> A -> B -> B. + Variable f : key -> A -> B -> B. - Fixpoint xfoldi (m : t A) (v : B) (i : positive) := + Fixpoint xfoldi (m : t A) (v : B) (i : key) := match m with - | Leaf => v + | Leaf _ => v | Node l (Some x) r => xfoldi r (f i x (xfoldi l v (append i 2))) (append i 3) | Node l None r => @@ -940,8 +938,8 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits. Fixpoint equal (A:Type)(cmp : A -> A -> bool)(m1 m2 : t A) : bool := match m1, m2 with - | Leaf, _ => is_empty m2 - | _, Leaf => is_empty m1 + | Leaf _, _ => is_empty m2 + | _, Leaf _ => is_empty m1 | Node l1 o1 r1, Node l2 o2 r2 => (match o1, o2 with | None, None => true @@ -1072,16 +1070,16 @@ Module PositiveMapAdditionalFacts. (* Derivable from the Map interface *) Theorem gsspec: - forall (A:Type)(i j: positive) (x: A) (m: t A), + forall (A:Type)(i j: key) (x: A) (m: t A), 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 *) Theorem gsident: - forall (A:Type)(i: positive) (m: t A) (v: A), + forall (A:Type)(i: key) (m: t A) (v: A), find i m = Some v -> add i v m = m. Proof. induction i; intros; destruct m; simpl; simpl in H; try congruence. @@ -1120,4 +1118,3 @@ Module PositiveMapAdditionalFacts. Qed. End PositiveMapAdditionalFacts. - 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. diff --git a/theories/FSets/FSetBridge.v b/theories/FSets/FSetBridge.v index 1ac544e1..97f140b3 100644 --- a/theories/FSets/FSetBridge.v +++ b/theories/FSets/FSetBridge.v @@ -284,7 +284,7 @@ Module DepOfNodep (Import M: S) <: Sdep with Module E := M.E. Lemma choose_equal : forall s s', Equal s s' -> match choose s, choose s' with - | inleft (exist x _), inleft (exist x' _) => E.eq x x' + | inleft (exist _ x _), inleft (exist _ x' _) => E.eq x x' | inright _, inright _ => True | _, _ => False end. @@ -423,7 +423,7 @@ Module NodepOfDep (M: Sdep) <: S with Module E := M.E. Definition choose (s : t) : option elt := match choose s with - | inleft (exist x _) => Some x + | inleft (exist _ x _) => Some x | inright _ => None end. @@ -472,7 +472,7 @@ Module NodepOfDep (M: Sdep) <: S with Module E := M.E. Definition min_elt (s : t) : option elt := match min_elt s with - | inleft (exist x _) => Some x + | inleft (exist _ x _) => Some x | inright _ => None end. @@ -500,7 +500,7 @@ Module NodepOfDep (M: Sdep) <: S with Module E := M.E. Definition max_elt (s : t) : option elt := match max_elt s with - | inleft (exist x _) => Some x + | inleft (exist _ x _) => Some x | inright _ => None end. @@ -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 := diff --git a/theories/FSets/FSetCompat.v b/theories/FSets/FSetCompat.v index 6b3d86d3..b1769da3 100644 --- a/theories/FSets/FSetCompat.v +++ b/theories/FSets/FSetCompat.v @@ -283,6 +283,8 @@ Module Update_WSets Lemma is_empty_spec : is_empty s = true <-> Empty s. Proof. intros; symmetry; apply MF.is_empty_iff. Qed. + + Declare Equivalent Keys In M.In. Lemma add_spec : In y (add x s) <-> E.eq y x \/ In y s. Proof. intros. rewrite MF.add_iff. intuition. Qed. diff --git a/theories/FSets/FSetDecide.v b/theories/FSets/FSetDecide.v index f64df9fe..ad067eb3 100644 --- a/theories/FSets/FSetDecide.v +++ b/theories/FSets/FSetDecide.v @@ -15,7 +15,7 @@ (** This file implements a decision procedure for a certain class of propositions involving finite sets. *) -Require Import Decidable DecidableTypeEx FSetFacts. +Require Import Decidable Setoid DecidableTypeEx FSetFacts. (** First, a version for Weak Sets in functorial presentation *) @@ -115,8 +115,8 @@ the above form: not affect the namespace if you import the enclosing module [Decide]. *) Module FSetLogicalFacts. - Require Export Decidable. - Require Export Setoid. + Export Decidable. + Export Setoid. (** ** Lemmas and Tactics About Decidable Propositions *) diff --git a/theories/FSets/FSetEqProperties.v b/theories/FSets/FSetEqProperties.v index ac495c04..f2f4cc2c 100644 --- a/theories/FSets/FSetEqProperties.v +++ b/theories/FSets/FSetEqProperties.v @@ -822,7 +822,7 @@ Proof. intros. rewrite for_all_exists in H; auto. rewrite negb_true_iff in H. -elim (for_all_mem_4 (fun x =>negb (f x)) Comp' s);intros;auto. +destruct (for_all_mem_4 (fun x =>negb (f x)) Comp' s) as (x,p); auto. elim p;intros. exists x;split;auto. rewrite <-negb_false_iff; auto. diff --git a/theories/FSets/FSetInterface.v b/theories/FSets/FSetInterface.v index a0361119..c791f49a 100644 --- a/theories/FSets/FSetInterface.v +++ b/theories/FSets/FSetInterface.v @@ -497,7 +497,7 @@ Module Type Sdep. in the dependent version of [choose], so we leave it separate. *) Parameter choose_equal : forall s s', Equal s s' -> match choose s, choose s' with - | inleft (exist x _), inleft (exist x' _) => E.eq x x' + | inleft (exist _ x _), inleft (exist _ x' _) => E.eq x x' | inright _, inright _ => True | _, _ => False end. diff --git a/theories/FSets/FSetPositive.v b/theories/FSets/FSetPositive.v index e5d55ac5..7398c6d6 100644 --- a/theories/FSets/FSetPositive.v +++ b/theories/FSets/FSetPositive.v @@ -19,20 +19,15 @@ Require Import Bool BinPos OrderedType OrderedTypeEx FSetInterface. Set Implicit Arguments. - Local Open Scope lazy_bool_scope. Local Open Scope positive_scope. - Local Unset Elimination Schemes. -Local Unset Case Analysis Schemes. -Local Unset Boolean Equality Schemes. - Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits. Module E:=PositiveOrderedTypeBits. - Definition elt := positive. + Definition elt := positive : Type. Inductive tree := | Leaf : tree @@ -40,9 +35,9 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits. Scheme tree_ind := Induction for tree Sort Prop. - Definition t := tree. + Definition t := tree : Type. - Definition empty := Leaf. + Definition empty : t := Leaf. Fixpoint is_empty (m : t) : bool := match m with @@ -50,7 +45,7 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits. | Node l b r => negb b &&& is_empty l &&& is_empty r end. - Fixpoint mem (i : positive) (m : t) : bool := + Fixpoint mem (i : elt) (m : t) {struct m} : bool := match m with | Leaf => false | Node l o r => @@ -61,7 +56,7 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits. end end. - Fixpoint add (i : positive) (m : t) : t := + Fixpoint add (i : elt) (m : t) : t := match m with | Leaf => match i with @@ -81,13 +76,13 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits. (** helper function to avoid creating empty trees that are not leaves *) - Definition node l (b: bool) r := + Definition node (l : t) (b: bool) (r : t) : t := if b then Node l b r else match l,r with | Leaf,Leaf => Leaf | _,_ => Node l false r end. - Fixpoint remove (i : positive) (m : t) : t := + Fixpoint remove (i : elt) (m : t) {struct m} : t := match m with | Leaf => Leaf | Node l o r => @@ -98,7 +93,7 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits. end end. - Fixpoint union (m m': t) := + Fixpoint union (m m': t) : t := match m with | Leaf => m' | Node l o r => @@ -108,7 +103,7 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits. end end. - Fixpoint inter (m m': t) := + Fixpoint inter (m m': t) : t := match m with | Leaf => Leaf | Node l o r => @@ -118,7 +113,7 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits. end end. - Fixpoint diff (m m': t) := + Fixpoint diff (m m': t) : t := match m with | Leaf => Leaf | Node l o r => @@ -150,7 +145,7 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits. (** reverses [y] and concatenate it with [x] *) - Fixpoint rev_append y x := + Fixpoint rev_append (y x : elt) : elt := match y with | 1 => x | y~1 => rev_append y x~1 @@ -161,8 +156,8 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits. Section Fold. - Variables B : Type. - Variable f : positive -> B -> B. + Variable B : Type. + Variable f : elt -> B -> B. (** the additional argument, [i], records the current path, in reverse order (this should be more efficient: we reverse this argument @@ -170,7 +165,7 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits. we also use this convention in all functions below *) - Fixpoint xfold (m : t) (v : B) (i : positive) := + Fixpoint xfold (m : t) (v : B) (i : elt) := match m with | Leaf => v | Node l true r => @@ -184,9 +179,9 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits. Section Quantifiers. - Variable f : positive -> bool. + Variable f : elt -> bool. - Fixpoint xforall (m : t) (i : positive) := + Fixpoint xforall (m : t) (i : elt) := match m with | Leaf => true | Node l o r => @@ -194,21 +189,21 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits. end. Definition for_all m := xforall m 1. - Fixpoint xexists (m : t) (i : positive) := + Fixpoint xexists (m : t) (i : elt) := match m with | Leaf => false | Node l o r => (o &&& f (rev i)) ||| xexists r i~1 ||| xexists l i~0 end. Definition exists_ m := xexists m 1. - Fixpoint xfilter (m : t) (i : positive) := + Fixpoint xfilter (m : t) (i : elt) : t := match m with | Leaf => Leaf | Node l o r => node (xfilter l i~0) (o &&& f (rev i)) (xfilter r i~1) end. Definition filter m := xfilter m 1. - Fixpoint xpartition (m : t) (i : positive) := + Fixpoint xpartition (m : t) (i : elt) : t * t := match m with | Leaf => (Leaf,Leaf) | Node l o r => @@ -226,7 +221,7 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits. (** uses [a] to accumulate values rather than doing a lot of concatenations *) - Fixpoint xelements (m : t) (i : positive) (a: list positive) := + Fixpoint xelements (m : t) (i : elt) (a: list elt) := match m with | Leaf => a | Node l false r => xelements l i~0 (xelements r i~1 a) @@ -250,7 +245,7 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits. (** would it be more efficient to use a path like in the above functions ? *) - Fixpoint choose (m: t) := + Fixpoint choose (m: t) : option elt := match m with | Leaf => None | Node l o r => if o then Some 1 else @@ -260,7 +255,7 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits. end end. - Fixpoint min_elt (m: t) := + Fixpoint min_elt (m: t) : option elt := match m with | Leaf => None | Node l o r => @@ -270,7 +265,7 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits. end end. - Fixpoint max_elt (m: t) := + Fixpoint max_elt (m: t) : option elt := match m with | Leaf => None | Node l o r => @@ -311,6 +306,9 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits. Notation "s [<=] t" := (Subset s t) (at level 70, no associativity). Definition eq := Equal. + + Declare Equivalent Keys Equal eq. + Definition lt m m' := compare_fun m m' = Lt. (** Specification of [In] *) @@ -355,10 +353,7 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits. case o; trivial. destruct l; trivial. destruct r; trivial. - symmetry. destruct x. - apply mem_Leaf. - apply mem_Leaf. - reflexivity. + now destruct x. Qed. Local Opaque node. @@ -367,8 +362,7 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits. Lemma is_empty_spec: forall s, Empty s <-> is_empty s = true. Proof. unfold Empty, In. - induction s as [|l IHl o r IHr]; simpl. - setoid_rewrite mem_Leaf. firstorder. + induction s as [|l IHl o r IHr]; simpl. now split. rewrite <- 2andb_lazy_alt, 2andb_true_iff, <- IHl, <- IHr. clear IHl IHr. destruct o; simpl; split. intro H. elim (H 1). reflexivity. @@ -759,7 +753,7 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits. Proof. intros. rewrite diff_spec. split; assumption. Qed. (** Specification of [fold] *) - + Lemma fold_1: forall s (A : Type) (i : A) (f : elt -> A -> A), fold f s i = fold_left (fun a e => f e a) (elements s) i. Proof. @@ -807,15 +801,15 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits. rewrite <- andb_lazy_alt. apply andb_true_iff. Qed. - Lemma filter_1 : forall s x f, compat_bool E.eq f -> + Lemma filter_1 : forall s x f, @compat_bool elt E.eq f -> In x (filter f s) -> In x s. Proof. unfold filter. intros s x f _. rewrite xfilter_spec. tauto. Qed. - Lemma filter_2 : forall s x f, compat_bool E.eq f -> + Lemma filter_2 : forall s x f, @compat_bool elt E.eq f -> In x (filter f s) -> f x = true. Proof. unfold filter. intros s x f _. rewrite xfilter_spec. tauto. Qed. - Lemma filter_3 : forall s x f, compat_bool E.eq f -> In x s -> + Lemma filter_3 : forall s x f, @compat_bool elt E.eq f -> In x s -> f x = true -> In x (filter f s). Proof. unfold filter. intros s x f _. rewrite xfilter_spec. tauto. Qed. @@ -826,8 +820,7 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits. xforall f s i = true <-> For_all (fun x => f (i@x) = true) s. Proof. unfold For_all, In. intro f. - induction s as [|l IHl o r IHr]; intros i; simpl. - setoid_rewrite mem_Leaf. intuition discriminate. + induction s as [|l IHl o r IHr]; intros i; simpl. now split. rewrite <- 2andb_lazy_alt, <- orb_lazy_alt, 2 andb_true_iff. rewrite IHl, IHr. clear IHl IHr. split. @@ -841,11 +834,11 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits. apply H. assumption. Qed. - Lemma for_all_1 : forall s f, compat_bool E.eq f -> + Lemma for_all_1 : forall s f, @compat_bool elt E.eq f -> For_all (fun x => f x = true) s -> for_all f s = true. Proof. intros s f _. unfold for_all. rewrite xforall_spec. trivial. Qed. - Lemma for_all_2 : forall s f, compat_bool E.eq f -> + Lemma for_all_2 : forall s f, @compat_bool elt E.eq f -> for_all f s = true -> For_all (fun x => f x = true) s. Proof. intros s f _. unfold for_all. rewrite xforall_spec. trivial. Qed. @@ -857,7 +850,7 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits. Proof. unfold Exists, In. intro f. induction s as [|l IHl o r IHr]; intros i; simpl. - setoid_rewrite mem_Leaf. firstorder. + split; [ discriminate | now intros [ _ [? _]]]. rewrite <- 2orb_lazy_alt, 2orb_true_iff, <- andb_lazy_alt, andb_true_iff. rewrite IHl, IHr. clear IHl IHr. split. @@ -868,11 +861,11 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits. intros [[x|x|] H]; eauto. Qed. - Lemma exists_1 : forall s f, compat_bool E.eq f -> + Lemma exists_1 : forall s f, @compat_bool elt E.eq f -> Exists (fun x => f x = true) s -> exists_ f s = true. Proof. intros s f _. unfold exists_. rewrite xexists_spec. trivial. Qed. - Lemma exists_2 : forall s f, compat_bool E.eq f -> + Lemma exists_2 : forall s f, @compat_bool elt E.eq f -> exists_ f s = true -> Exists (fun x => f x = true) s. Proof. intros s f _. unfold exists_. rewrite xexists_spec. trivial. Qed. @@ -888,11 +881,11 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits. destruct o; simpl; rewrite IHl, IHr; reflexivity. Qed. - Lemma partition_1 : forall s f, compat_bool E.eq f -> + Lemma partition_1 : forall s f, @compat_bool elt E.eq f -> Equal (fst (partition f s)) (filter f s). Proof. intros. rewrite partition_filter. apply eq_refl. Qed. - Lemma partition_2 : forall s f, compat_bool E.eq f -> + Lemma partition_2 : forall s f, @compat_bool elt E.eq f -> Equal (snd (partition f s)) (filter (fun x => negb (f x)) s). Proof. intros. rewrite partition_filter. apply eq_refl. Qed. @@ -909,7 +902,7 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits. induction s as [|l IHl o r IHr]; simpl. intros. split; intro H. left. assumption. - destruct H as [H|[x [Hx Hx']]]. assumption. elim (empty_1 Hx'). + destruct H as [H|[x [Hx Hx']]]. assumption. discriminate. intros j acc y. case o. rewrite IHl. rewrite InA_cons. rewrite IHr. clear IHl IHr. split. @@ -1000,7 +993,7 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits. constructor. intros x H. apply E.lt_not_eq in H. apply H. reflexivity. intro. apply E.lt_trans. - intros ? ? <- ? ? <-. reflexivity. + solve_proper. apply elements_3. Qed. @@ -1111,7 +1104,7 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits. destruct (min_elt r). injection H. intros <-. clear H. destruct y as [z|z|]. - apply (IHr p z); trivial. + apply (IHr e z); trivial. elim (Hp _ H'). discriminate. discriminate. @@ -1165,7 +1158,7 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits. injection H. intros <-. clear H. destruct y as [z|z|]. elim (Hp _ H'). - apply (IHl p z); trivial. + apply (IHl e z); trivial. discriminate. discriminate. Qed. diff --git a/theories/FSets/FSetProperties.v b/theories/FSets/FSetProperties.v index d53ce0c8..25b042ca 100644 --- a/theories/FSets/FSetProperties.v +++ b/theories/FSets/FSetProperties.v @@ -995,8 +995,7 @@ Module OrdProperties (M:S). leb_1, gtb_1, (H0 a) by auto with *. intuition. destruct (E.compare a x); intuition. - right; right; split; auto with *. - ME.order. + fold (~E.lt a x); auto with *. Qed. Definition Above x s := forall y, In y s -> E.lt y x. |