summaryrefslogtreecommitdiff
path: root/theories/FSets/FMapAVL.v
diff options
context:
space:
mode:
Diffstat (limited to 'theories/FSets/FMapAVL.v')
-rw-r--r--theories/FSets/FMapAVL.v62
1 files changed, 31 insertions, 31 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.
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-28 19:32:13 +0000