From 5b7eafd0f00a16d78f99a27f5c7d5a0de77dc7e6 Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Wed, 21 Jul 2010 09:46:51 +0200 Subject: Imported Upstream snapshot 8.3~beta0+13298 --- theories/FSets/FMapFullAVL.v | 275 ++++++++++++++++++++++--------------------- 1 file changed, 138 insertions(+), 137 deletions(-) (limited to 'theories/FSets/FMapFullAVL.v') diff --git a/theories/FSets/FMapFullAVL.v b/theories/FSets/FMapFullAVL.v index 57cbbcc4..e4f8b4df 100644 --- a/theories/FSets/FMapFullAVL.v +++ b/theories/FSets/FMapFullAVL.v @@ -1,4 +1,3 @@ - (***********************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) (* Prop := | RBLeaf : avl (Leaf _) - | RBNode : forall x e l r h, + | RBNode : forall x e l r h, avl l -> avl r -> -(2) <= height l - height r <= 2 -> - h = max (height l) (height r) + 1 -> + h = max (height l) (height r) + 1 -> avl (Node l x e r h). @@ -64,28 +65,28 @@ Inductive avl : t elt -> Prop := Hint Constructors avl. -Lemma height_non_negative : forall (s : t elt), avl s -> +Lemma height_non_negative : forall (s : t elt), avl s -> height s >= 0. Proof. induction s; simpl; intros; auto with zarith. inv avl; intuition; omega_max. Qed. -Ltac avl_nn_hyp H := +Ltac avl_nn_hyp H := let nz := fresh "nz" in assert (nz := height_non_negative H). -Ltac avl_nn h := - let t := type of h in - match type of t with +Ltac avl_nn h := + let t := type of h in + match type of t with | Prop => avl_nn_hyp h | _ => match goal with H : avl h |- _ => avl_nn_hyp H end end. -(* Repeat the previous tactic. +(* Repeat the previous tactic. Drawback: need to clear the [avl _] hyps ... Thank you Ltac *) Ltac avl_nns := - match goal with + match goal with | H:avl _ |- _ => avl_nn_hyp H; clear H; avl_nns | _ => idtac end. @@ -103,49 +104,49 @@ Hint Resolve avl_node. (** Results about [height] *) -Lemma height_0 : forall l, avl l -> height l = 0 -> +Lemma height_0 : forall l, avl l -> height l = 0 -> l = Leaf _. Proof. destruct 1; intuition; simpl in *. - avl_nns; simpl in *; elimtype False; omega_max. + avl_nns; simpl in *; exfalso; omega_max. Qed. (** * Empty map *) Lemma empty_avl : avl (empty elt). -Proof. +Proof. unfold empty; auto. Qed. (** * Helper functions *) -Lemma create_avl : - forall l x e r, avl l -> avl r -> -(2) <= height l - height r <= 2 -> +Lemma create_avl : + forall l x e r, avl l -> avl r -> -(2) <= height l - height r <= 2 -> avl (create l x e r). Proof. unfold create; auto. Qed. -Lemma create_height : - forall l x e r, avl l -> avl r -> -(2) <= height l - height r <= 2 -> +Lemma create_height : + forall l x e r, avl l -> avl r -> -(2) <= height l - height r <= 2 -> height (create l x e r) = max (height l) (height r) + 1. Proof. unfold create; intros; auto. Qed. -Lemma bal_avl : forall l x e r, avl l -> avl r -> +Lemma bal_avl : forall l x e r, avl l -> avl r -> -(3) <= height l - height r <= 3 -> avl (bal l x e r). Proof. intros l x e r; functional induction (bal l x e r); intros; clearf; - inv avl; simpl in *; + inv avl; simpl in *; match goal with |- avl (assert_false _ _ _ _) => avl_nns | _ => repeat apply create_avl; simpl in *; auto end; omega_max. Qed. -Lemma bal_height_1 : forall l x e r, avl l -> avl r -> +Lemma bal_height_1 : forall l x e r, avl l -> avl r -> -(3) <= height l - height r <= 3 -> 0 <= height (bal l x e r) - max (height l) (height r) <= 1. Proof. @@ -153,25 +154,25 @@ Proof. inv avl; avl_nns; simpl in *; omega_max. Qed. -Lemma bal_height_2 : - forall l x e r, avl l -> avl r -> -(2) <= height l - height r <= 2 -> +Lemma bal_height_2 : + forall l x e r, avl l -> avl r -> -(2) <= height l - height r <= 2 -> height (bal l x e r) == max (height l) (height r) +1. Proof. intros l x e r; functional induction (bal l x e r); intros; clearf; inv avl; avl_nns; simpl in *; omega_max. Qed. -Ltac omega_bal := match goal with - | H:avl ?l, H':avl ?r |- context [ bal ?l ?x ?e ?r ] => - generalize (bal_height_1 x e H H') (bal_height_2 x e H H'); +Ltac omega_bal := match goal with + | H:avl ?l, H':avl ?r |- context [ bal ?l ?x ?e ?r ] => + generalize (bal_height_1 x e H H') (bal_height_2 x e H H'); omega_max end. (** * Insertion *) -Lemma add_avl_1 : forall m x e, avl m -> +Lemma add_avl_1 : forall m x e, avl m -> avl (add x e m) /\ 0 <= height (add x e m) - height m <= 1. -Proof. +Proof. intros m x e; functional induction (add x e m); intros; inv avl; simpl in *. intuition; try constructor; simpl; auto; try omega_max. (* LT *) @@ -196,8 +197,8 @@ Hint Resolve add_avl. (** * Extraction of minimum binding *) -Lemma remove_min_avl_1 : forall l x e r h, avl (Node l x e r h) -> - avl (remove_min l x e r)#1 /\ +Lemma remove_min_avl_1 : forall l x e r h, avl (Node l x e r h) -> + avl (remove_min l x e r)#1 /\ 0 <= height (Node l x e r h) - height (remove_min l x e r)#1 <= 1. Proof. intros l x e r; functional induction (remove_min l x e r); simpl in *; intros. @@ -210,20 +211,20 @@ Proof. omega_bal. Qed. -Lemma remove_min_avl : forall l x e r h, avl (Node l x e r h) -> - avl (remove_min l x e r)#1. +Lemma remove_min_avl : forall l x e r h, avl (Node l x e r h) -> + avl (remove_min l x e r)#1. Proof. intros; generalize (remove_min_avl_1 H); intuition. Qed. (** * Merging two trees *) -Lemma merge_avl_1 : forall m1 m2, avl m1 -> avl m2 -> - -(2) <= height m1 - height m2 <= 2 -> - avl (merge m1 m2) /\ +Lemma merge_avl_1 : forall m1 m2, avl m1 -> avl m2 -> + -(2) <= height m1 - height m2 <= 2 -> + avl (merge m1 m2) /\ 0<= height (merge m1 m2) - max (height m1) (height m2) <=1. Proof. - intros m1 m2; functional induction (merge m1 m2); intros; + intros m1 m2; functional induction (merge m1 m2); intros; try factornode _x _x0 _x1 _x2 _x3 as m1. simpl; split; auto; avl_nns; omega_max. simpl; split; auto; avl_nns; omega_max. @@ -235,16 +236,16 @@ Proof. omega_bal. Qed. -Lemma merge_avl : forall m1 m2, avl m1 -> avl m2 -> +Lemma merge_avl : forall m1 m2, avl m1 -> avl m2 -> -(2) <= height m1 - height m2 <= 2 -> avl (merge m1 m2). -Proof. +Proof. intros; generalize (merge_avl_1 H H0 H1); intuition. Qed. (** * Deletion *) -Lemma remove_avl_1 : forall m x, avl m -> +Lemma remove_avl_1 : forall m x, avl m -> avl (remove x m) /\ 0 <= height m - height (remove x m) <= 1. Proof. intros m x; functional induction (remove x m); intros. @@ -252,25 +253,25 @@ Proof. (* LT *) inv avl. destruct (IHt H0). - split. + split. apply bal_avl; auto. omega_max. omega_bal. (* EQ *) - inv avl. + inv avl. generalize (merge_avl_1 H0 H1 H2). intuition omega_max. (* GT *) inv avl. destruct (IHt H1). - split. + split. apply bal_avl; auto. omega_max. omega_bal. Qed. Lemma remove_avl : forall m x, avl m -> avl (remove x m). -Proof. +Proof. intros; generalize (remove_avl_1 x H); intuition. Qed. Hint Resolve remove_avl. @@ -278,7 +279,7 @@ Hint Resolve remove_avl. (** * Join *) -Lemma join_avl_1 : forall l x d r, avl l -> avl r -> +Lemma join_avl_1 : forall l x d r, avl l -> avl r -> avl (join l x d r) /\ 0<= height (join l x d r) - max (height l) (height r) <= 1. Proof. @@ -344,9 +345,9 @@ Hint Resolve concat_avl. (** split *) -Lemma split_avl : forall m x, avl m -> +Lemma split_avl : forall m x, avl m -> avl (split x m)#l /\ avl (split x m)#r. -Proof. +Proof. intros m x; functional induction (split x m); simpl; auto. rewrite e1 in IHt;simpl in IHt;inversion_clear 1; intuition. simpl; inversion_clear 1; auto. @@ -356,12 +357,12 @@ Qed. End Elt. Hint Constructors avl. -Section Map. +Section Map. Variable elt elt' : Type. -Variable f : elt -> elt'. +Variable f : elt -> elt'. Lemma map_height : forall m, height (map f m) = height m. -Proof. +Proof. destruct m; simpl; auto. Qed. @@ -375,10 +376,10 @@ End Map. Section Mapi. Variable elt elt' : Type. -Variable f : key -> elt -> elt'. +Variable f : key -> elt -> elt'. Lemma mapi_height : forall m, height (mapi f m) = height m. -Proof. +Proof. destruct m; simpl; auto. Qed. @@ -390,7 +391,7 @@ Qed. End Mapi. -Section Map_option. +Section Map_option. Variable elt elt' : Type. Variable f : key -> elt -> option elt'. @@ -412,12 +413,12 @@ Hypothesis mapr_avl : forall m', avl m' -> avl (mapr m'). Notation map2_opt := (map2_opt f mapl mapr). -Lemma map2_opt_avl : forall m1 m2, avl m1 -> avl m2 -> +Lemma map2_opt_avl : forall m1 m2, avl m1 -> avl m2 -> avl (map2_opt m1 m2). Proof. -intros m1 m2; functional induction (map2_opt m1 m2); auto; -factornode _x0 _x1 _x2 _x3 _x4 as r2; intros; -destruct (split_avl x1 H0); rewrite e1 in *; simpl in *; inv avl; +intros m1 m2; functional induction (map2_opt m1 m2); auto; +factornode _x0 _x1 _x2 _x3 _x4 as r2; intros; +destruct (split_avl x1 H0); rewrite e1 in *; simpl in *; inv avl; auto using join_avl, concat_avl. Qed. @@ -437,11 +438,11 @@ End AvlProofs. (** * Encapsulation - We can implement [S] with balanced binary search trees. + We can implement [S] with balanced binary search trees. When compared to [FMapAVL], we maintain here two invariants (bst and avl) instead of only bst, which is enough for fulfilling the FMap interface. -*) +*) Module IntMake (I:Int)(X: OrderedType) <: S with Module E := X. @@ -450,32 +451,32 @@ Module IntMake (I:Int)(X: OrderedType) <: S with Module E := X. Import Raw. Import Raw.Proofs. - Record bbst (elt:Type) := + Record bbst (elt:Type) := Bbst {this :> tree elt; is_bst : bst this; is_avl: avl this}. - + Definition t := bbst. Definition key := E.t. - + Section Elt. Variable elt elt' elt'': Type. Implicit Types m : t elt. - Implicit Types x y : key. - Implicit Types e : elt. + Implicit Types x y : key. + Implicit Types e : elt. Definition empty : t elt := Bbst (empty_bst elt) (empty_avl elt). Definition is_empty m : bool := is_empty m.(this). - Definition add x e m : t elt := + Definition add x e m : t elt := Bbst (add_bst x e m.(is_bst)) (add_avl x e m.(is_avl)). - Definition remove x m : t elt := + Definition remove x m : t elt := Bbst (remove_bst x m.(is_bst)) (remove_avl x m.(is_avl)). Definition mem x m : bool := mem x m.(this). Definition find x m : option elt := find x m.(this). - Definition map f m : t elt' := + Definition map f m : t elt' := Bbst (map_bst f m.(is_bst)) (map_avl f m.(is_avl)). - Definition mapi (f:key->elt->elt') m : t elt' := + Definition mapi (f:key->elt->elt') m : t elt' := Bbst (mapi_bst f m.(is_bst)) (mapi_avl f m.(is_avl)). - Definition map2 f m (m':t elt') : t elt'' := + Definition map2 f m (m':t elt') : t elt'' := Bbst (map2_bst f m.(is_bst) m'.(is_bst)) (map2_avl f m.(is_avl) m'.(is_avl)). Definition elements m : list (key*elt) := elements m.(this). Definition cardinal m := cardinal m.(this). @@ -492,14 +493,14 @@ Module IntMake (I:Int)(X: OrderedType) <: S with Module E := X. Lemma MapsTo_1 : forall m x y e, E.eq x y -> MapsTo x e m -> MapsTo y e m. Proof. intros m; exact (@MapsTo_1 _ m.(this)). Qed. - + Lemma mem_1 : forall m x, In x m -> mem x m = true. Proof. unfold In, mem; intros m x; rewrite In_alt; simpl; apply mem_1; auto. apply m.(is_bst). Qed. - - Lemma mem_2 : forall m x, mem x m = true -> In x m. + + Lemma mem_2 : forall m x, mem x m = true -> In x m. Proof. unfold In, mem; intros m x; rewrite In_alt; simpl; apply mem_2; auto. Qed. @@ -530,7 +531,7 @@ Module IntMake (I:Int)(X: OrderedType) <: S with Module E := X. Proof. intros m x y e; exact (@remove_3 elt _ x y e m.(is_bst)). Qed. - Lemma find_1 : forall m x e, MapsTo x e m -> find x m = Some e. + Lemma find_1 : forall m x e, MapsTo x e m -> find x m = Some e. Proof. intros m x e; exact (@find_1 elt _ x e m.(is_bst)). Qed. Lemma find_2 : forall m x e, find x m = Some e -> MapsTo x e m. Proof. intros m; exact (@find_2 elt m.(this)). Qed. @@ -539,36 +540,36 @@ Module IntMake (I:Int)(X: OrderedType) <: S with Module E := X. fold f m i = fold_left (fun a p => f (fst p) (snd p) a) (elements m) i. Proof. intros m; exact (@fold_1 elt m.(this) m.(is_bst)). Qed. - Lemma elements_1 : forall m x e, + Lemma elements_1 : forall m x e, MapsTo x e m -> InA eq_key_elt (x,e) (elements m). Proof. intros; unfold elements, MapsTo, eq_key_elt; rewrite elements_mapsto; auto. Qed. - Lemma elements_2 : forall m x e, + Lemma elements_2 : forall m x e, InA eq_key_elt (x,e) (elements m) -> MapsTo x e m. Proof. intros; unfold elements, MapsTo, eq_key_elt; rewrite <- elements_mapsto; auto. Qed. - Lemma elements_3 : forall m, sort lt_key (elements m). + Lemma elements_3 : forall m, sort lt_key (elements m). Proof. intros m; exact (@elements_sort elt m.(this) m.(is_bst)). Qed. - Lemma elements_3w : forall m, NoDupA eq_key (elements m). + Lemma elements_3w : forall m, NoDupA eq_key (elements m). Proof. intros m; exact (@elements_nodup elt m.(this) m.(is_bst)). Qed. Lemma cardinal_1 : forall m, cardinal m = length (elements m). Proof. intro m; exact (@elements_cardinal elt m.(this)). Qed. Definition Equal m m' := forall y, find y m = find y m'. - Definition Equiv (eq_elt:elt->elt->Prop) m m' := - (forall k, In k m <-> In k m') /\ + Definition Equiv (eq_elt:elt->elt->Prop) m m' := + (forall k, In k m <-> In k m') /\ (forall k e e', MapsTo k e m -> MapsTo k e' m' -> eq_elt e e'). Definition Equivb cmp := Equiv (Cmp cmp). - Lemma Equivb_Equivb : forall cmp m m', + Lemma Equivb_Equivb : forall cmp m m', Equivb cmp m m' <-> Raw.Proofs.Equivb cmp m m'. - Proof. + Proof. 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. @@ -576,23 +577,23 @@ Module IntMake (I:Int)(X: OrderedType) <: S with Module E := X. generalize (H0 k); do 2 rewrite <- In_alt; intuition. Qed. - Lemma equal_1 : forall m m' cmp, - Equivb cmp m m' -> equal cmp m m' = true. - Proof. - unfold equal; intros (m,b,a) (m',b',a') cmp; rewrite Equivb_Equivb; + Lemma equal_1 : forall m m' cmp, + Equivb cmp m m' -> equal cmp m m' = true. + Proof. + unfold equal; intros (m,b,a) (m',b',a') cmp; rewrite Equivb_Equivb; intros; simpl in *; rewrite equal_Equivb; auto. - Qed. + Qed. - Lemma equal_2 : forall m m' cmp, + Lemma equal_2 : forall m m' cmp, equal cmp m m' = true -> Equivb cmp m m'. - Proof. - unfold equal; intros (m,b,a) (m',b',a') cmp; rewrite Equivb_Equivb; + Proof. + unfold equal; intros (m,b,a) (m',b',a') cmp; rewrite Equivb_Equivb; intros; simpl in *; rewrite <-equal_Equivb; auto. Qed. End Elt. - Lemma map_1 : forall (elt elt':Type)(m: t elt)(x:key)(e:elt)(f:elt->elt'), + Lemma map_1 : forall (elt elt':Type)(m: t elt)(x:key)(e:elt)(f:elt->elt'), MapsTo x e m -> MapsTo x (f e) (map f m). Proof. intros elt elt' m x e f; exact (@map_1 elt elt' f m.(this) x e). Qed. @@ -600,10 +601,10 @@ Module IntMake (I:Int)(X: OrderedType) <: S with Module E := X. Proof. intros elt elt' m x f; do 2 unfold In in *; do 2 rewrite In_alt; simpl. apply map_2; auto. - Qed. + Qed. Lemma mapi_1 : forall (elt elt':Type)(m: t elt)(x:key)(e:elt) - (f:key->elt->elt'), MapsTo x e m -> + (f:key->elt->elt'), MapsTo x e m -> exists y, E.eq y x /\ MapsTo x (f y e) (mapi f m). Proof. intros elt elt' m x e f; exact (@mapi_1 elt elt' f m.(this) x e). Qed. Lemma mapi_2 : forall (elt elt':Type)(m: t elt)(x:key) @@ -613,10 +614,10 @@ Module IntMake (I:Int)(X: OrderedType) <: S with Module E := X. Qed. Lemma map2_1 : forall (elt elt' elt'':Type)(m: t elt)(m': t elt') - (x:key)(f:option elt->option elt'->option elt''), - In x m \/ In x m' -> - find x (map2 f m m') = f (find x m) (find x m'). - Proof. + (x:key)(f:option elt->option elt'->option elt''), + In x m \/ In x m' -> + find x (map2 f m m') = f (find x m) (find x m'). + Proof. unfold find, map2, In; intros elt elt' elt'' m m' x f. do 2 rewrite In_alt; intros; simpl; apply map2_1; auto. apply m.(is_bst). @@ -624,9 +625,9 @@ Module IntMake (I:Int)(X: OrderedType) <: S with Module E := X. Qed. Lemma map2_2 : forall (elt elt' elt'':Type)(m: t elt)(m': t elt') - (x:key)(f:option elt->option elt'->option elt''), + (x:key)(f:option elt->option elt'->option elt''), In x (map2 f m m') -> In x m \/ In x m'. - Proof. + Proof. unfold In, map2; intros elt elt' elt'' m m' x f. do 3 rewrite In_alt; intros; simpl in *; eapply map2_2; eauto. apply m.(is_bst). @@ -636,54 +637,54 @@ Module IntMake (I:Int)(X: OrderedType) <: S with Module E := X. End IntMake. -Module IntMake_ord (I:Int)(X: OrderedType)(D : OrderedType) <: - Sord with Module Data := D +Module IntMake_ord (I:Int)(X: OrderedType)(D : OrderedType) <: + Sord with Module Data := D with Module MapS.E := X. Module Data := D. - Module Import MapS := IntMake(I)(X). + Module Import MapS := IntMake(I)(X). Import AvlProofs. Import Raw.Proofs. Module Import MD := OrderedTypeFacts(D). Module LO := FMapList.Make_ord(X)(D). - Definition t := MapS.t D.t. + Definition t := MapS.t D.t. - Definition cmp e e' := + Definition cmp e e' := match D.compare e e' with EQ _ => true | _ => false end. - Definition elements (m:t) := + Definition elements (m:t) := LO.MapS.Build_slist (Raw.Proofs.elements_sort m.(is_bst)). - (** * As comparison function, we propose here a non-structural - version faithful to the code of Ocaml's Map library, instead of + (** * As comparison function, we propose here a non-structural + version faithful to the code of Ocaml's Map library, instead of the structural version of FMapAVL *) - Fixpoint cardinal_e (e:Raw.enumeration D.t) := - match e with + Fixpoint cardinal_e (e:Raw.enumeration D.t) := + match e with | Raw.End => 0%nat | Raw.More _ _ r e => S (Raw.cardinal r + cardinal_e e) end. - Lemma cons_cardinal_e : forall m e, + Lemma cons_cardinal_e : forall m e, cardinal_e (Raw.cons m e) = (Raw.cardinal m + cardinal_e e)%nat. Proof. induction m; simpl; intros; auto. rewrite IHm1; simpl; rewrite <- plus_n_Sm; auto with arith. Qed. - Definition cardinal_e_2 ee := + Definition cardinal_e_2 ee := (cardinal_e (fst ee) + cardinal_e (snd ee))%nat. - Function compare_aux (ee:Raw.enumeration D.t * Raw.enumeration D.t) - { measure cardinal_e_2 ee } : comparison := - match ee with + 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.More x1 d1 r1 e1, Raw.More x2 d2 r2 e2) => match X.compare x1 x2 with - | EQ _ => match D.compare d1 d2 with + | EQ _ => match D.compare d1 d2 with | EQ _ => compare_aux (Raw.cons r1 e1, Raw.cons r2 e2) | LT _ => Lt | GT _ => Gt @@ -693,10 +694,10 @@ Module IntMake_ord (I:Int)(X: OrderedType)(D : OrderedType) <: end end. Proof. - intros; unfold cardinal_e_2; simpl; + intros; unfold cardinal_e_2; simpl; abstract (do 2 rewrite cons_cardinal_e; romega with * ). Defined. - + Definition Cmp c := match c with | Eq => LO.eq_list @@ -704,7 +705,7 @@ Module IntMake_ord (I:Int)(X: OrderedType)(D : OrderedType) <: | Gt => (fun l1 l2 => LO.lt_list l2 l1) end. - Lemma cons_Cmp : forall c x1 x2 d1 d2 l1 l2, + Lemma cons_Cmp : forall c x1 x2 d1 d2 l1 l2, X.eq x1 x2 -> D.eq d1 d2 -> Cmp c l1 l2 -> Cmp c ((x1,d1)::l1) ((x2,d2)::l2). Proof. @@ -712,23 +713,23 @@ Module IntMake_ord (I:Int)(X: OrderedType)(D : OrderedType) <: Qed. Hint Resolve cons_Cmp. - Lemma compare_aux_Cmp : forall e, + Lemma compare_aux_Cmp : forall e, Cmp (compare_aux e) (flatten_e (fst e)) (flatten_e (snd e)). Proof. - intros e; functional induction (compare_aux e); simpl in *; + intros e; functional induction (compare_aux e); simpl in *; auto; intros; try clear e0; try clear e3; try MX.elim_comp; auto. rewrite 2 cons_1 in IHc; auto. Qed. - Lemma compare_Cmp : forall m1 m2, - Cmp (compare_aux (Raw.cons m1 (Raw.End _), Raw.cons m2 (Raw.End _))) + Lemma compare_Cmp : forall m1 m2, + Cmp (compare_aux (Raw.cons m1 (Raw.End _), Raw.cons m2 (Raw.End _))) (Raw.elements m1) (Raw.elements m2). Proof. - intros. + 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. - apply (@compare_aux_Cmp (Raw.cons m1 (Raw.End _), + apply (@compare_aux_Cmp (Raw.cons m1 (Raw.End _), Raw.cons m2 (Raw.End _))). Qed. @@ -737,15 +738,15 @@ Module IntMake_ord (I:Int)(X: OrderedType)(D : OrderedType) <: Definition compare (s s':t) : Compare lt eq s s'. Proof. - intros (s,b,a) (s',b',a'). + destruct s as (s,b,a), s' as (s',b',a'). generalize (compare_Cmp s s'). destruct compare_aux; intros; [apply EQ|apply LT|apply GT]; red; auto. Defined. - + (* Proofs about [eq] and [lt] *) - Definition selements (m1 : t) := + Definition selements (m1 : t) := LO.MapS.Build_slist (elements_sort m1.(is_bst)). Definition seq (m1 m2 : t) := LO.eq (selements m1) (selements m2). @@ -782,7 +783,7 @@ Module IntMake_ord (I:Int)(X: OrderedType)(D : OrderedType) <: Qed. Lemma eq_refl : forall m : t, eq m m. - Proof. + Proof. intros; rewrite eq_seq; unfold seq; intros; apply LO.eq_refl. Qed. @@ -799,13 +800,13 @@ Module IntMake_ord (I:Int)(X: OrderedType)(D : OrderedType) <: Lemma lt_trans : forall m1 m2 m3 : t, lt m1 m2 -> lt m2 m3 -> lt m1 m3. Proof. - intros m1 m2 m3; rewrite 3 lt_slt; unfold slt; + intros m1 m2 m3; rewrite 3 lt_slt; unfold slt; intros; eapply LO.lt_trans; eauto. Qed. Lemma lt_not_eq : forall m1 m2 : t, lt m1 m2 -> ~ eq m1 m2. Proof. - intros m1 m2; rewrite lt_slt, eq_seq; unfold slt, seq; + intros m1 m2; rewrite lt_slt, eq_seq; unfold slt, seq; intros; apply LO.lt_not_eq; auto. Qed. @@ -816,8 +817,8 @@ End IntMake_ord. Module Make (X: OrderedType) <: S with Module E := X :=IntMake(Z_as_Int)(X). -Module Make_ord (X: OrderedType)(D: OrderedType) - <: Sord with Module Data := D +Module Make_ord (X: OrderedType)(D: OrderedType) + <: Sord with Module Data := D with Module MapS.E := X :=IntMake_ord(Z_as_Int)(X)(D). -- cgit v1.2.3