Built with Alectryon, running Coq+SerAPI v8.10.0+0.7.0. Coq sources are in this panel; goals and messages will appear in the other. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑ Ctrl+↓ to navigate, Ctrl+🖱️ to focus.
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
(* <O___,, * (see CREDITS file for the list of authors) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
MSetGenTree : sets via generic trees
- empty is_empty
- mem
- compare equal subset
- fold cardinal elements
- for_all exists - min_elt max_elt choose
Require Import FunInd Orders OrdersFacts MSetInterface PeanoNat. Local Open Scope list_scope. Local Open Scope lazy_bool_scope. (* For nicer extraction, we create induction principles only when needed *) Local Unset Elimination Schemes. Module Type InfoTyp. Parameter t : Set. End InfoTyp.
Module Type Ops (X:OrderedType)(Info:InfoTyp). Definition elt := X.t. Hint Transparent elt : core. Inductive tree : Type := | Leaf : tree | Node : Info.t -> tree -> X.t -> tree -> tree.
Definition empty := Leaf. Definition is_empty t := match t with | Leaf => true | _ => false end.
The mem function is deciding membership. It exploits the
binary search tree invariant to achieve logarithmic complexity.
Fixpoint mem x t :=
match t with
| Leaf => false
| Node _ l k r =>
match X.compare x k with
| Lt => mem x l
| Eq => true
| Gt => mem x r
end
end.
Fixpoint min_elt (t : tree) : option elt := match t with | Leaf => None | Node _ Leaf x r => Some x | Node _ l x r => min_elt l end. Fixpoint max_elt (t : tree) : option elt := match t with | Leaf => None | Node _ l x Leaf => Some x | Node _ l x r => max_elt r end. Definition choose := min_elt.
Fixpoint fold {A: Type} (f: elt -> A -> A) (t: tree) (base: A) : A := match t with | Leaf => base | Node _ l x r => fold f r (f x (fold f l base)) end. Fixpoint elements_aux acc s := match s with | Leaf => acc | Node _ l x r => elements_aux (x :: elements_aux acc r) l end. Definition elements := elements_aux nil. Fixpoint rev_elements_aux acc s := match s with | Leaf => acc | Node _ l x r => rev_elements_aux (x :: rev_elements_aux acc l) r end. Definition rev_elements := rev_elements_aux nil. Fixpoint cardinal (s : tree) : nat := match s with | Leaf => 0 | Node _ l _ r => S (cardinal l + cardinal r) end. Fixpoint maxdepth s := match s with | Leaf => 0 | Node _ l _ r => S (max (maxdepth l) (maxdepth r)) end. Fixpoint mindepth s := match s with | Leaf => 0 | Node _ l _ r => S (min (mindepth l) (mindepth r)) end.
We do not use the standard boolean operators of Coq,
but lazy ones.
Fixpoint for_all (f:elt->bool) s := match s with | Leaf => true | Node _ l x r => f x &&& for_all f l &&& for_all f r end. Fixpoint exists_ (f:elt->bool) s := match s with | Leaf => false | Node _ l x r => f x ||| exists_ f l ||| exists_ f r end.
The algorithm here has been suggested by Xavier Leroy,
and transformed into c.p.s. by Benjamin Grégoire.
The original ocaml code (with non-structural recursive calls)
has also been formalized (thanks to Function+measure), see
ocaml_compare in MSetFullAVL. The following code with
continuations computes dramatically faster in Coq, and
should be almost as efficient after extraction.
Enumeration of the elements of a tree. This corresponds
to the "samefringe" notion in the literature.
Inductive enumeration :=
| End : enumeration
| More : elt -> tree -> enumeration -> enumeration.
cons t e adds the elements of tree t on the head of
enumeration e.
Fixpoint cons s e : enumeration :=
match s with
| Leaf => e
| Node _ l x r => cons l (More x r e)
end.
One step of comparison of elements
Definition compare_more x1 (cont:enumeration->comparison) e2 :=
match e2 with
| End => Gt
| More x2 r2 e2 =>
match X.compare x1 x2 with
| Eq => cont (cons r2 e2)
| Lt => Lt
| Gt => Gt
end
end.
Comparison of left tree, middle element, then right tree
Fixpoint compare_cont s1 (cont:enumeration->comparison) e2 :=
match s1 with
| Leaf => cont e2
| Node _ l1 x1 r1 =>
compare_cont l1 (compare_more x1 (compare_cont r1 cont)) e2
end.
Initial continuation
Definition compare_end e2 :=
match e2 with End => Eq | _ => Lt end.
The complete comparison
Definition compare s1 s2 := compare_cont s1 compare_end (cons s2 End). Definition equal s1 s2 := match compare s1 s2 with Eq => true | _ => false end.
In ocaml, recursive calls are made on "half-trees" such as
(Node _ l1 x1 Leaf) and (Node _ Leaf x1 r1). Instead of these
non-structural calls, we propose here two specialized functions
for these situations. This version should be almost as efficient
as the one of ocaml (closures as arguments may slow things a bit),
it is simply less compact. The exact ocaml version has also been
formalized (thanks to Function+measure), see ocaml_subset in
MSetFullAVL.
Fixpoint subsetl (subset_l1 : tree -> bool) x1 s2 : bool := match s2 with | Leaf => false | Node _ l2 x2 r2 => match X.compare x1 x2 with | Eq => subset_l1 l2 | Lt => subsetl subset_l1 x1 l2 | Gt => mem x1 r2 &&& subset_l1 s2 end end. Fixpoint subsetr (subset_r1 : tree -> bool) x1 s2 : bool := match s2 with | Leaf => false | Node _ l2 x2 r2 => match X.compare x1 x2 with | Eq => subset_r1 r2 | Lt => mem x1 l2 &&& subset_r1 s2 | Gt => subsetr subset_r1 x1 r2 end end. Fixpoint subset s1 s2 : bool := match s1, s2 with | Leaf, _ => true | Node _ _ _ _, Leaf => false | Node _ l1 x1 r1, Node _ l2 x2 r2 => match X.compare x1 x2 with | Eq => subset l1 l2 &&& subset r1 r2 | Lt => subsetl (subset l1) x1 l2 &&& subset r1 s2 | Gt => subsetr (subset r1) x1 r2 &&& subset l1 s2 end end. End Ops.
Module Type Props (X:OrderedType)(Info:InfoTyp)(Import M:Ops X Info).
Inductive InT (x : elt) : tree -> Prop := | IsRoot : forall c l r y, X.eq x y -> InT x (Node c l y r) | InLeft : forall c l r y, InT x l -> InT x (Node c l y r) | InRight : forall c l r y, InT x r -> InT x (Node c l y r). Definition In := InT.
Definition Equal s s' := forall a : elt, InT a s <-> InT a s'. Definition Subset s s' := forall a : elt, InT a s -> InT a s'. Definition Empty s := forall a : elt, ~ InT a s. Definition For_all (P : elt -> Prop) s := forall x, InT x s -> P x. Definition Exists (P : elt -> Prop) s := exists x, InT x s /\ P x.
lt_tree x s: all elements in s are smaller than x
(resp. greater for gt_tree)
Definition lt_tree x s := forall y, InT y s -> X.lt y x. Definition gt_tree x s := forall y, InT y s -> X.lt x y.
bst t : t is a binary search tree
Inductive bst : tree -> Prop :=
| BSLeaf : bst Leaf
| BSNode : forall c x l r, bst l -> bst r ->
lt_tree x l -> gt_tree x r -> bst (Node c l x r).
bst is the (decidable) invariant our trees will have to satisfy.
Definition IsOk := bst. Class Ok (s:tree) : Prop := ok : bst s. Instance bst_Ok s (Hs : bst s) : Ok s := { ok := Hs }. Fixpoint ltb_tree x s := match s with | Leaf => true | Node _ l y r => match X.compare x y with | Gt => ltb_tree x l && ltb_tree x r | _ => false end end. Fixpoint gtb_tree x s := match s with | Leaf => true | Node _ l y r => match X.compare x y with | Lt => gtb_tree x l && gtb_tree x r | _ => false end end. Fixpoint isok s := match s with | Leaf => true | Node _ l x r => isok l && isok r && ltb_tree x l && gtb_tree x r end.
Module Import MX := OrderedTypeFacts X.
Scheme tree_ind := Induction for tree Sort Prop. Scheme bst_ind := Induction for bst Sort Prop. Local Hint Resolve MX.eq_refl MX.eq_trans MX.lt_trans ok : core. Local Hint Immediate MX.eq_sym : core. Local Hint Unfold In lt_tree gt_tree : core. Local Hint Constructors InT bst : core. Local Hint Unfold Ok : core.
Automatic treatment of Ok hypothesis
Ltac clear_inversion H := inversion H; clear H; subst. Ltac inv_ok := match goal with | H:Ok (Node _ _ _ _) |- _ => clear_inversion H; inv_ok | H:Ok Leaf |- _ => clear H; inv_ok | H:bst ?x |- _ => change (Ok x) in H; inv_ok | _ => idtac end.
A tactic to repeat inversion_clear on all hyps of the
form (f (Node _ _ _ _))
Ltac is_tree_constr c := match c with | Leaf => idtac | Node _ _ _ _ => idtac | _ => fail end. Ltac invtree f := match goal with | H:f ?s |- _ => is_tree_constr s; clear_inversion H; invtree f | H:f _ ?s |- _ => is_tree_constr s; clear_inversion H; invtree f | H:f _ _ ?s |- _ => is_tree_constr s; clear_inversion H; invtree f | _ => idtac end. Ltac inv := inv_ok; invtree InT. Ltac intuition_in := repeat (intuition; inv).
Helper tactic concerning order of elements.
Ltac order := match goal with
| U: lt_tree _ ?s, V: InT _ ?s |- _ => generalize (U _ V); clear U; order
| U: gt_tree _ ?s, V: InT _ ?s |- _ => generalize (U _ V); clear U; order
| _ => MX.order
end.
isok is indeed a decision procedure for Ok
forall (x : X.t) (s : tree), lt_tree x s <-> ltb_tree x s = trueforall (x : X.t) (s : tree), lt_tree x s <-> ltb_tree x s = truex:X.tlt_tree x Leaf <-> true = truex:X.tc:Info.tl:treey:X.tr:treeIHl:lt_tree x l <-> ltb_tree x l = trueIHr:lt_tree x r <-> ltb_tree x r = truelt_tree x (Node c l y r) <-> match X.compare x y with | Gt => ltb_tree x l && ltb_tree x r | _ => false end = truex:X.tc:Info.tl:treey:X.tr:treeIHl:lt_tree x l <-> ltb_tree x l = trueIHr:lt_tree x r <-> ltb_tree x r = truelt_tree x (Node c l y r) <-> match X.compare x y with | Gt => ltb_tree x l && ltb_tree x r | _ => false end = truex:X.tc:Info.tl:treey:X.tr:treeIHl:lt_tree x l <-> ltb_tree x l = trueIHr:lt_tree x r <-> ltb_tree x r = trueH:X.eq x ylt_tree x (Node c l y r) <-> false = truex:X.tc:Info.tl:treey:X.tr:treeIHl:lt_tree x l <-> ltb_tree x l = trueIHr:lt_tree x r <-> ltb_tree x r = trueH:X.lt x ylt_tree x (Node c l y r) <-> false = truex:X.tc:Info.tl:treey:X.tr:treeIHl:lt_tree x l <-> ltb_tree x l = trueIHr:lt_tree x r <-> ltb_tree x r = trueH:X.lt y xlt_tree x (Node c l y r) <-> ltb_tree x l && ltb_tree x r = truex:X.tc:Info.tl:treey:X.tr:treeIHl:lt_tree x l <-> ltb_tree x l = trueIHr:lt_tree x r <-> ltb_tree x r = trueH:X.eq x yH0:lt_tree x (Node c l y r)false = truex:X.tc:Info.tl:treey:X.tr:treeIHl:lt_tree x l <-> ltb_tree x l = trueIHr:lt_tree x r <-> ltb_tree x r = trueH:X.lt x ylt_tree x (Node c l y r) <-> false = truex:X.tc:Info.tl:treey:X.tr:treeIHl:lt_tree x l <-> ltb_tree x l = trueIHr:lt_tree x r <-> ltb_tree x r = trueH:X.lt y xlt_tree x (Node c l y r) <-> ltb_tree x l && ltb_tree x r = truex:X.tc:Info.tl:treey:X.tr:treeIHl:lt_tree x l <-> ltb_tree x l = trueIHr:lt_tree x r <-> ltb_tree x r = trueH:X.eq x yH0:lt_tree x (Node c l y r)H1:X.lt y xfalse = truex:X.tc:Info.tl:treey:X.tr:treeIHl:lt_tree x l <-> ltb_tree x l = trueIHr:lt_tree x r <-> ltb_tree x r = trueH:X.lt x ylt_tree x (Node c l y r) <-> false = truex:X.tc:Info.tl:treey:X.tr:treeIHl:lt_tree x l <-> ltb_tree x l = trueIHr:lt_tree x r <-> ltb_tree x r = trueH:X.lt y xlt_tree x (Node c l y r) <-> ltb_tree x l && ltb_tree x r = truex:X.tc:Info.tl:treey:X.tr:treeIHl:lt_tree x l <-> ltb_tree x l = trueIHr:lt_tree x r <-> ltb_tree x r = trueH:X.lt x ylt_tree x (Node c l y r) <-> false = truex:X.tc:Info.tl:treey:X.tr:treeIHl:lt_tree x l <-> ltb_tree x l = trueIHr:lt_tree x r <-> ltb_tree x r = trueH:X.lt y xlt_tree x (Node c l y r) <-> ltb_tree x l && ltb_tree x r = truex:X.tc:Info.tl:treey:X.tr:treeIHl:lt_tree x l <-> ltb_tree x l = trueIHr:lt_tree x r <-> ltb_tree x r = trueH:X.lt x yH0:lt_tree x (Node c l y r)false = truex:X.tc:Info.tl:treey:X.tr:treeIHl:lt_tree x l <-> ltb_tree x l = trueIHr:lt_tree x r <-> ltb_tree x r = trueH:X.lt y xlt_tree x (Node c l y r) <-> ltb_tree x l && ltb_tree x r = truex:X.tc:Info.tl:treey:X.tr:treeIHl:lt_tree x l <-> ltb_tree x l = trueIHr:lt_tree x r <-> ltb_tree x r = trueH:X.lt x yH0:lt_tree x (Node c l y r)H1:X.lt y xfalse = truex:X.tc:Info.tl:treey:X.tr:treeIHl:lt_tree x l <-> ltb_tree x l = trueIHr:lt_tree x r <-> ltb_tree x r = trueH:X.lt y xlt_tree x (Node c l y r) <-> ltb_tree x l && ltb_tree x r = truex:X.tc:Info.tl:treey:X.tr:treeIHl:lt_tree x l <-> ltb_tree x l = trueIHr:lt_tree x r <-> ltb_tree x r = trueH:X.lt y xlt_tree x (Node c l y r) <-> ltb_tree x l && ltb_tree x r = trueunfold lt_tree; intuition_in; order. Qed.x:X.tc:Info.tl:treey:X.tr:treeIHl:lt_tree x l <-> ltb_tree x l = trueIHr:lt_tree x r <-> ltb_tree x r = trueH:X.lt y xlt_tree x (Node c l y r) <-> lt_tree x l /\ lt_tree x rforall (x : X.t) (s : tree), gt_tree x s <-> gtb_tree x s = trueforall (x : X.t) (s : tree), gt_tree x s <-> gtb_tree x s = truex:X.tgt_tree x Leaf <-> true = truex:X.tc:Info.tl:treey:X.tr:treeIHl:gt_tree x l <-> gtb_tree x l = trueIHr:gt_tree x r <-> gtb_tree x r = truegt_tree x (Node c l y r) <-> match X.compare x y with | Lt => gtb_tree x l && gtb_tree x r | _ => false end = truex:X.tc:Info.tl:treey:X.tr:treeIHl:gt_tree x l <-> gtb_tree x l = trueIHr:gt_tree x r <-> gtb_tree x r = truegt_tree x (Node c l y r) <-> match X.compare x y with | Lt => gtb_tree x l && gtb_tree x r | _ => false end = truex:X.tc:Info.tl:treey:X.tr:treeIHl:gt_tree x l <-> gtb_tree x l = trueIHr:gt_tree x r <-> gtb_tree x r = trueH:X.eq x ygt_tree x (Node c l y r) <-> false = truex:X.tc:Info.tl:treey:X.tr:treeIHl:gt_tree x l <-> gtb_tree x l = trueIHr:gt_tree x r <-> gtb_tree x r = trueH:X.lt x ygt_tree x (Node c l y r) <-> gtb_tree x l && gtb_tree x r = truex:X.tc:Info.tl:treey:X.tr:treeIHl:gt_tree x l <-> gtb_tree x l = trueIHr:gt_tree x r <-> gtb_tree x r = trueH:X.lt y xgt_tree x (Node c l y r) <-> false = truex:X.tc:Info.tl:treey:X.tr:treeIHl:gt_tree x l <-> gtb_tree x l = trueIHr:gt_tree x r <-> gtb_tree x r = trueH:X.eq x yH0:gt_tree x (Node c l y r)false = truex:X.tc:Info.tl:treey:X.tr:treeIHl:gt_tree x l <-> gtb_tree x l = trueIHr:gt_tree x r <-> gtb_tree x r = trueH:X.lt x ygt_tree x (Node c l y r) <-> gtb_tree x l && gtb_tree x r = truex:X.tc:Info.tl:treey:X.tr:treeIHl:gt_tree x l <-> gtb_tree x l = trueIHr:gt_tree x r <-> gtb_tree x r = trueH:X.lt y xgt_tree x (Node c l y r) <-> false = truex:X.tc:Info.tl:treey:X.tr:treeIHl:gt_tree x l <-> gtb_tree x l = trueIHr:gt_tree x r <-> gtb_tree x r = trueH:X.eq x yH0:gt_tree x (Node c l y r)H1:X.lt x yfalse = truex:X.tc:Info.tl:treey:X.tr:treeIHl:gt_tree x l <-> gtb_tree x l = trueIHr:gt_tree x r <-> gtb_tree x r = trueH:X.lt x ygt_tree x (Node c l y r) <-> gtb_tree x l && gtb_tree x r = truex:X.tc:Info.tl:treey:X.tr:treeIHl:gt_tree x l <-> gtb_tree x l = trueIHr:gt_tree x r <-> gtb_tree x r = trueH:X.lt y xgt_tree x (Node c l y r) <-> false = truex:X.tc:Info.tl:treey:X.tr:treeIHl:gt_tree x l <-> gtb_tree x l = trueIHr:gt_tree x r <-> gtb_tree x r = trueH:X.lt x ygt_tree x (Node c l y r) <-> gtb_tree x l && gtb_tree x r = truex:X.tc:Info.tl:treey:X.tr:treeIHl:gt_tree x l <-> gtb_tree x l = trueIHr:gt_tree x r <-> gtb_tree x r = trueH:X.lt y xgt_tree x (Node c l y r) <-> false = truex:X.tc:Info.tl:treey:X.tr:treeIHl:gt_tree x l <-> gtb_tree x l = trueIHr:gt_tree x r <-> gtb_tree x r = trueH:X.lt x ygt_tree x (Node c l y r) <-> gt_tree x l /\ gt_tree x rx:X.tc:Info.tl:treey:X.tr:treeIHl:gt_tree x l <-> gtb_tree x l = trueIHr:gt_tree x r <-> gtb_tree x r = trueH:X.lt y xgt_tree x (Node c l y r) <-> false = truex:X.tc:Info.tl:treey:X.tr:treeIHl:gt_tree x l <-> gtb_tree x l = trueIHr:gt_tree x r <-> gtb_tree x r = trueH:X.lt y xgt_tree x (Node c l y r) <-> false = truex:X.tc:Info.tl:treey:X.tr:treeIHl:gt_tree x l <-> gtb_tree x l = trueIHr:gt_tree x r <-> gtb_tree x r = trueH:X.lt y xH0:gt_tree x (Node c l y r)false = trueorder. Qed.x:X.tc:Info.tl:treey:X.tr:treeIHl:gt_tree x l <-> gtb_tree x l = trueIHr:gt_tree x r <-> gtb_tree x r = trueH:X.lt y xH0:gt_tree x (Node c l y r)H1:X.lt x yfalse = trueforall s : tree, Ok s <-> isok s = trueforall s : tree, Ok s <-> isok s = trueOk Leaf <-> true = truec:Info.tl:treey:X.tr:treeIHl:Ok l <-> isok l = trueIHr:Ok r <-> isok r = trueOk (Node c l y r) <-> isok l && isok r && ltb_tree y l && gtb_tree y r = truec:Info.tl:treey:X.tr:treeIHl:Ok l <-> isok l = trueIHr:Ok r <-> isok r = trueOk (Node c l y r) <-> isok l && isok r && ltb_tree y l && gtb_tree y r = trueintuition_in. Qed.c:Info.tl:treey:X.tr:treeIHl:Ok l <-> isok l = trueIHr:Ok r <-> isok r = trueOk (Node c l y r) <-> ((Ok l /\ Ok r) /\ lt_tree y l) /\ gt_tree y rs:treeisok s = true -> Ok sintros; apply <- isok_iff; auto. Qed.s:treeisok s = true -> Ok s
forall (s : tree) (x y : X.t), X.eq x y -> InT x s -> InT y sinduction s; simpl; intuition_in; eauto. Qed. Local Hint Immediate In_1 : core.forall (s : tree) (x y : X.t), X.eq x y -> InT x s -> InT y sProper (X.eq ==> eq ==> iff) InTProper (X.eq ==> eq ==> iff) InTProper (X.eq ==> eq ==> impl) InTapply In_1 with x; auto. Qed.x, y:X.tH:X.eq x yy0:treeH1:InT x y0InT y y0forall (c : Info.t) (l : tree) (x : X.t) (r : tree) (y : elt), InT y (Node c l x r) <-> InT y l \/ X.eq y x \/ InT y rintuition_in. Qed.forall (c : Info.t) (l : tree) (x : X.t) (r : tree) (y : elt), InT y (Node c l x r) <-> InT y l \/ X.eq y x \/ InT y rforall x : elt, InT x Leaf <-> Falseintuition_in. Qed.forall x : elt, InT x Leaf <-> False
Results about lt_tree and gt_tree
forall x : elt, lt_tree x Leafred; inversion 1. Qed.forall x : elt, lt_tree x Leafforall x : elt, gt_tree x Leafred; inversion 1. Qed.forall x : elt, gt_tree x Leafforall (x y : elt) (l r : tree) (i : Info.t), lt_tree x l -> lt_tree x r -> X.lt y x -> lt_tree x (Node i l y r)unfold lt_tree; intuition_in; order. Qed.forall (x y : elt) (l r : tree) (i : Info.t), lt_tree x l -> lt_tree x r -> X.lt y x -> lt_tree x (Node i l y r)forall (x y : elt) (l r : tree) (i : Info.t), gt_tree x l -> gt_tree x r -> X.lt x y -> gt_tree x (Node i l y r)unfold gt_tree; intuition_in; order. Qed. Local Hint Resolve lt_leaf gt_leaf lt_tree_node gt_tree_node : core.forall (x y : elt) (l r : tree) (i : Info.t), gt_tree x l -> gt_tree x r -> X.lt x y -> gt_tree x (Node i l y r)forall (x : elt) (t : tree), lt_tree x t -> ~ InT x tintros; intro; order. Qed.forall (x : elt) (t : tree), lt_tree x t -> ~ InT x tforall x y : X.t, X.lt x y -> forall t : tree, lt_tree x t -> lt_tree y teauto. Qed.forall x y : X.t, X.lt x y -> forall t : tree, lt_tree x t -> lt_tree y tforall (x : elt) (t : tree), gt_tree x t -> ~ InT x tintros; intro; order. Qed.forall (x : elt) (t : tree), gt_tree x t -> ~ InT x tforall x y : X.t, X.lt y x -> forall t : tree, gt_tree x t -> gt_tree y teauto. Qed.forall x y : X.t, X.lt y x -> forall t : tree, gt_tree x t -> gt_tree y tProper (X.eq ==> eq ==> iff) lt_treeProper (X.eq ==> eq ==> iff) lt_treeProper (X.eq ==> eq ==> impl) lt_treex, x':X.tHx:X.eq x x's, s':treeHs:s = s'H:lt_tree x sy:eltHy:InT y s'X.lt y x'setoid_rewrite <- Hx; auto. Qed.x, x':X.tHx:X.eq x x's':treeH:lt_tree x s'y:eltHy:InT y s'X.lt y x'Proper (X.eq ==> eq ==> iff) gt_treeProper (X.eq ==> eq ==> iff) gt_treeProper (X.eq ==> eq ==> impl) gt_treex, x':X.tHx:X.eq x x's, s':treeHs:s = s'H:gt_tree x sy:eltHy:InT y s'X.lt x' ysetoid_rewrite <- Hx; auto. Qed. Local Hint Resolve lt_tree_not_in lt_tree_trans gt_tree_not_in gt_tree_trans : core. Ltac induct s x := induction s as [|i l IHl x' r IHr]; simpl; intros; [|elim_compare x x'; intros; inv]. Ltac auto_tc := auto with typeclass_instances. Ltac ok := inv; change bst with Ok in *; match goal with | |- Ok (Node _ _ _ _) => constructor; auto_tc; ok | |- lt_tree _ (Node _ _ _ _) => apply lt_tree_node; ok | |- gt_tree _ (Node _ _ _ _) => apply gt_tree_node; ok | _ => eauto with typeclass_instances end.x, x':X.tHx:X.eq x x's':treeH:gt_tree x s'y:eltHy:InT y s'X.lt x' y
Empty emptyEmpty emptyinversion H. Qed.x:eltH:InT x emptyFalseOk emptyauto. Qed.Ok empty
forall s : tree, is_empty s = true <-> Empty sforall s : tree, is_empty s = true <-> Empty strue = true <-> Empty Leafc:Info.tr:treex:X.tl:treefalse = true <-> Empty (Node c r x l)true = true <-> Empty Leaftrue = true -> Empty Leafinv.x:eltH:InT x LeafFalsec:Info.tr:treex:X.tl:treefalse = true <-> Empty (Node c r x l)c:Info.tr:treex:X.tl:treefalse = true -> Empty (Node c r x l)c:Info.tr:treex:X.tl:treeEmpty (Node c r x l) -> false = trueintro H; elim (H x); auto. Qed.c:Info.tr:treex:X.tl:treeEmpty (Node c r x l) -> false = true
forall (s : tree) (x : X.t), Ok s -> mem x s = true <-> InT x sforall (s : tree) (x : X.t), Ok s -> mem x s = true <-> InT x ss:treex:X.tH:Ok smem x s = true -> InT x ss:treex:X.tH:Ok sInT x s -> mem x s = trueinduct s x; now auto.s:treex:X.tH:Ok smem x s = true -> InT x sinduct s x; intuition_in; order. Qed.s:treex:X.tH:Ok sInT x s -> mem x s = true
Functional Scheme min_elt_ind := Induction for min_elt Sort Prop. Functional Scheme max_elt_ind := Induction for max_elt Sort Prop.s:treex:eltmin_elt s = Some x -> InT x sfunctional induction (min_elt s); auto; inversion 1; auto. Qed.s:treex:eltmin_elt s = Some x -> InT x ss:treex, y:eltH:Ok smin_elt s = Some x -> InT y s -> ~ X.lt y xs:treex, y:eltH:Ok smin_elt s = Some x -> InT y s -> ~ X.lt y xs:treex:eltH:Ok sforall y : elt, min_elt s = Some x -> InT y s -> ~ X.lt y xx:eltH:Ok Leafforall y : elt, None = Some x -> InT y Leaf -> ~ X.lt y xx:elt_x:Info.tx0:X.tr:treeH:Ok (Node _x Leaf x0 r)forall y : elt, Some x0 = Some x -> InT y (Node _x Leaf x0 r) -> ~ X.lt y xx:elt_x:Info.tx0:X.tr:tree_x1:Info.tl1:treex1:X.tr1:treeH:Ok (Node _x (Node _x1 l1 x1 r1) x0 r)IHo:Ok (Node _x1 l1 x1 r1) -> forall y : elt, min_elt (Node _x1 l1 x1 r1) = Some x -> InT y (Node _x1 l1 x1 r1) -> ~ X.lt y xforall y : elt, min_elt (Node _x1 l1 x1 r1) = Some x -> InT y (Node _x (Node _x1 l1 x1 r1) x0 r) -> ~ X.lt y xdiscriminate.x:eltH:Ok Leafforall y : elt, None = Some x -> InT y Leaf -> ~ X.lt y xx:elt_x:Info.tx0:X.tr:treeH:Ok (Node _x Leaf x0 r)forall y : elt, Some x0 = Some x -> InT y (Node _x Leaf x0 r) -> ~ X.lt y xx:elt_x:Info.tx0:X.tr:treeH:Ok (Node _x Leaf x0 r)y:eltV:Some x0 = Some xW:InT y (Node _x Leaf x0 r)~ X.lt y xinv; order.x:elt_x:Info.tr:treeH:Ok (Node _x Leaf x r)y:eltW:InT y (Node _x Leaf x r)~ X.lt y xx:elt_x:Info.tx0:X.tr:tree_x1:Info.tl1:treex1:X.tr1:treeH:Ok (Node _x (Node _x1 l1 x1 r1) x0 r)IHo:Ok (Node _x1 l1 x1 r1) -> forall y : elt, min_elt (Node _x1 l1 x1 r1) = Some x -> InT y (Node _x1 l1 x1 r1) -> ~ X.lt y xforall y : elt, min_elt (Node _x1 l1 x1 r1) = Some x -> InT y (Node _x (Node _x1 l1 x1 r1) x0 r) -> ~ X.lt y xx:elt_x:Info.tx0:X.tr:tree_x1:Info.tl1:treex1:X.tr1:treeIHo:Ok (Node _x1 l1 x1 r1) -> forall y0 : elt, min_elt (Node _x1 l1 x1 r1) = Some x -> InT y0 (Node _x1 l1 x1 r1) -> ~ X.lt y0 xy:eltH0:min_elt (Node _x1 l1 x1 r1) = Some xH7:Ok rH8:lt_tree x0 (Node _x1 l1 x1 r1)H9:gt_tree x0 rH5:Ok l1H10:Ok r1H11:lt_tree x1 l1H12:gt_tree x1 r1H2:X.eq y x0~ X.lt y xx:elt_x:Info.tx0:X.tr:tree_x1:Info.tl1:treex1:X.tr1:treeIHo:Ok (Node _x1 l1 x1 r1) -> forall y0 : elt, min_elt (Node _x1 l1 x1 r1) = Some x -> InT y0 (Node _x1 l1 x1 r1) -> ~ X.lt y0 xy:eltH0:min_elt (Node _x1 l1 x1 r1) = Some xH7:Ok rH8:lt_tree x0 (Node _x1 l1 x1 r1)H9:gt_tree x0 rH5:Ok l1H10:Ok r1H11:lt_tree x1 l1H12:gt_tree x1 r1H2:InT y r~ X.lt y xx:elt_x:Info.tx0:X.tr:tree_x1:Info.tl1:treex1:X.tr1:treeIHo:Ok (Node _x1 l1 x1 r1) -> forall y0 : elt, min_elt (Node _x1 l1 x1 r1) = Some x -> InT y0 (Node _x1 l1 x1 r1) -> ~ X.lt y0 xy:eltH0:min_elt (Node _x1 l1 x1 r1) = Some xH7:Ok rH8:lt_tree x0 (Node _x1 l1 x1 r1)H9:gt_tree x0 rH5:Ok l1H10:Ok r1H11:lt_tree x1 l1H12:gt_tree x1 r1H2:X.eq y x0~ X.lt y xorder.x:elt_x:Info.tx0:X.tr:tree_x1:Info.tl1:treex1:X.tr1:treeIHo:Ok (Node _x1 l1 x1 r1) -> forall y0 : elt, min_elt (Node _x1 l1 x1 r1) = Some x -> InT y0 (Node _x1 l1 x1 r1) -> ~ X.lt y0 xy:eltH0:min_elt (Node _x1 l1 x1 r1) = Some xH7:Ok rH8:lt_tree x0 (Node _x1 l1 x1 r1)H9:gt_tree x0 rH5:Ok l1H10:Ok r1H11:lt_tree x1 l1H12:gt_tree x1 r1H2:X.eq y x0H:X.lt x x0~ X.lt y xx:elt_x:Info.tx0:X.tr:tree_x1:Info.tl1:treex1:X.tr1:treeIHo:Ok (Node _x1 l1 x1 r1) -> forall y0 : elt, min_elt (Node _x1 l1 x1 r1) = Some x -> InT y0 (Node _x1 l1 x1 r1) -> ~ X.lt y0 xy:eltH0:min_elt (Node _x1 l1 x1 r1) = Some xH7:Ok rH8:lt_tree x0 (Node _x1 l1 x1 r1)H9:gt_tree x0 rH5:Ok l1H10:Ok r1H11:lt_tree x1 l1H12:gt_tree x1 r1H2:InT y r~ X.lt y xx:elt_x:Info.tx0:X.tr:tree_x1:Info.tl1:treex1:X.tr1:treeIHo:Ok (Node _x1 l1 x1 r1) -> forall y0 : elt, min_elt (Node _x1 l1 x1 r1) = Some x -> InT y0 (Node _x1 l1 x1 r1) -> ~ X.lt y0 xy:eltH0:min_elt (Node _x1 l1 x1 r1) = Some xH7:Ok rH8:lt_tree x0 (Node _x1 l1 x1 r1)H9:gt_tree x0 rH5:Ok l1H10:Ok r1H11:lt_tree x1 l1H12:gt_tree x1 r1H2:InT y rH:X.lt x1 x0~ X.lt y xorder. Qed.x:elt_x:Info.tx0:X.tr:tree_x1:Info.tl1:treex1:X.tr1:treeIHo:Ok (Node _x1 l1 x1 r1) -> forall y0 : elt, min_elt (Node _x1 l1 x1 r1) = Some x -> InT y0 (Node _x1 l1 x1 r1) -> ~ X.lt y0 xy:eltH0:min_elt (Node _x1 l1 x1 r1) = Some xH7:Ok rH8:lt_tree x0 (Node _x1 l1 x1 r1)H9:gt_tree x0 rH5:Ok l1H10:Ok r1H11:lt_tree x1 l1H12:gt_tree x1 r1H2:InT y rH:X.lt x1 x0H1:~ X.lt x1 x~ X.lt y xs:treemin_elt s = None -> Empty ss:treemin_elt s = None -> Empty sNone = None -> Empty Leaf_x:Info.tx:X.t_x0:treeSome x = None -> Empty (Node _x Leaf x _x0)_x:Info.tx:X.t_x0:tree_x1:Info.t_x2:tree_x3:X.t_x4:treeIHo:min_elt (Node _x1 _x2 _x3 _x4) = None -> Empty (Node _x1 _x2 _x3 _x4)min_elt (Node _x1 _x2 _x3 _x4) = None -> Empty (Node _x (Node _x1 _x2 _x3 _x4) x _x0)_x:Info.tx:X.t_x0:treeSome x = None -> Empty (Node _x Leaf x _x0)_x:Info.tx:X.t_x0:tree_x1:Info.t_x2:tree_x3:X.t_x4:treeIHo:min_elt (Node _x1 _x2 _x3 _x4) = None -> Empty (Node _x1 _x2 _x3 _x4)min_elt (Node _x1 _x2 _x3 _x4) = None -> Empty (Node _x (Node _x1 _x2 _x3 _x4) x _x0)_x:Info.tx:X.t_x0:tree_x1:Info.t_x2:tree_x3:X.t_x4:treeIHo:min_elt (Node _x1 _x2 _x3 _x4) = None -> Empty (Node _x1 _x2 _x3 _x4)min_elt (Node _x1 _x2 _x3 _x4) = None -> Empty (Node _x (Node _x1 _x2 _x3 _x4) x _x0)destruct (IHo H0 _x3); auto. Qed._x:Info.tx:X.t_x0:tree_x1:Info.t_x2:tree_x3:X.t_x4:treeIHo:min_elt (Node _x1 _x2 _x3 _x4) = None -> Empty (Node _x1 _x2 _x3 _x4)H0:min_elt (Node _x1 _x2 _x3 _x4) = NoneEmpty (Node _x (Node _x1 _x2 _x3 _x4) x _x0)s:treex:eltmax_elt s = Some x -> InT x sfunctional induction (max_elt s); auto; inversion 1; auto. Qed.s:treex:eltmax_elt s = Some x -> InT x ss:treex, y:eltH:Ok smax_elt s = Some x -> InT y s -> ~ X.lt x ys:treex, y:eltH:Ok smax_elt s = Some x -> InT y s -> ~ X.lt x ys:treex:eltH:Ok sforall y : elt, max_elt s = Some x -> InT y s -> ~ X.lt x yx:eltH:Ok Leafforall y : elt, None = Some x -> InT y Leaf -> ~ X.lt x yx:elt_x:Info.tr:treex0:X.tH:Ok (Node _x r x0 Leaf)forall y : elt, Some x0 = Some x -> InT y (Node _x r x0 Leaf) -> ~ X.lt x yx:elt_x:Info.tr:treex0:X.t_x1:Info.tl1:treex1:X.tr1:treeH:Ok (Node _x r x0 (Node _x1 l1 x1 r1))IHo:Ok (Node _x1 l1 x1 r1) -> forall y : elt, max_elt (Node _x1 l1 x1 r1) = Some x -> InT y (Node _x1 l1 x1 r1) -> ~ X.lt x yforall y : elt, max_elt (Node _x1 l1 x1 r1) = Some x -> InT y (Node _x r x0 (Node _x1 l1 x1 r1)) -> ~ X.lt x ydiscriminate.x:eltH:Ok Leafforall y : elt, None = Some x -> InT y Leaf -> ~ X.lt x yx:elt_x:Info.tr:treex0:X.tH:Ok (Node _x r x0 Leaf)forall y : elt, Some x0 = Some x -> InT y (Node _x r x0 Leaf) -> ~ X.lt x yx:elt_x:Info.tr:treex0:X.tH:Ok (Node _x r x0 Leaf)y:eltV:Some x0 = Some xW:InT y (Node _x r x0 Leaf)~ X.lt x yinv; order.x:elt_x:Info.tr:treeH:Ok (Node _x r x Leaf)y:eltW:InT y (Node _x r x Leaf)~ X.lt x yx:elt_x:Info.tr:treex0:X.t_x1:Info.tl1:treex1:X.tr1:treeH:Ok (Node _x r x0 (Node _x1 l1 x1 r1))IHo:Ok (Node _x1 l1 x1 r1) -> forall y : elt, max_elt (Node _x1 l1 x1 r1) = Some x -> InT y (Node _x1 l1 x1 r1) -> ~ X.lt x yforall y : elt, max_elt (Node _x1 l1 x1 r1) = Some x -> InT y (Node _x r x0 (Node _x1 l1 x1 r1)) -> ~ X.lt x yx:elt_x:Info.tr:treex0:X.t_x1:Info.tl1:treex1:X.tr1:treeIHo:Ok (Node _x1 l1 x1 r1) -> forall y0 : elt, max_elt (Node _x1 l1 x1 r1) = Some x -> InT y0 (Node _x1 l1 x1 r1) -> ~ X.lt x y0y:eltH0:max_elt (Node _x1 l1 x1 r1) = Some xH6:Ok rH8:lt_tree x0 rH9:gt_tree x0 (Node _x1 l1 x1 r1)H5:Ok l1H10:Ok r1H11:lt_tree x1 l1H12:gt_tree x1 r1H2:X.eq y x0~ X.lt x yx:elt_x:Info.tr:treex0:X.t_x1:Info.tl1:treex1:X.tr1:treeIHo:Ok (Node _x1 l1 x1 r1) -> forall y0 : elt, max_elt (Node _x1 l1 x1 r1) = Some x -> InT y0 (Node _x1 l1 x1 r1) -> ~ X.lt x y0y:eltH0:max_elt (Node _x1 l1 x1 r1) = Some xH6:Ok rH8:lt_tree x0 rH9:gt_tree x0 (Node _x1 l1 x1 r1)H5:Ok l1H10:Ok r1H11:lt_tree x1 l1H12:gt_tree x1 r1H2:InT y r~ X.lt x yx:elt_x:Info.tr:treex0:X.t_x1:Info.tl1:treex1:X.tr1:treeIHo:Ok (Node _x1 l1 x1 r1) -> forall y0 : elt, max_elt (Node _x1 l1 x1 r1) = Some x -> InT y0 (Node _x1 l1 x1 r1) -> ~ X.lt x y0y:eltH0:max_elt (Node _x1 l1 x1 r1) = Some xH6:Ok rH8:lt_tree x0 rH9:gt_tree x0 (Node _x1 l1 x1 r1)H5:Ok l1H10:Ok r1H11:lt_tree x1 l1H12:gt_tree x1 r1H2:X.eq y x0~ X.lt x yorder.x:elt_x:Info.tr:treex0:X.t_x1:Info.tl1:treex1:X.tr1:treeIHo:Ok (Node _x1 l1 x1 r1) -> forall y0 : elt, max_elt (Node _x1 l1 x1 r1) = Some x -> InT y0 (Node _x1 l1 x1 r1) -> ~ X.lt x y0y:eltH0:max_elt (Node _x1 l1 x1 r1) = Some xH6:Ok rH8:lt_tree x0 rH9:gt_tree x0 (Node _x1 l1 x1 r1)H5:Ok l1H10:Ok r1H11:lt_tree x1 l1H12:gt_tree x1 r1H2:X.eq y x0H:X.lt x0 x~ X.lt x yx:elt_x:Info.tr:treex0:X.t_x1:Info.tl1:treex1:X.tr1:treeIHo:Ok (Node _x1 l1 x1 r1) -> forall y0 : elt, max_elt (Node _x1 l1 x1 r1) = Some x -> InT y0 (Node _x1 l1 x1 r1) -> ~ X.lt x y0y:eltH0:max_elt (Node _x1 l1 x1 r1) = Some xH6:Ok rH8:lt_tree x0 rH9:gt_tree x0 (Node _x1 l1 x1 r1)H5:Ok l1H10:Ok r1H11:lt_tree x1 l1H12:gt_tree x1 r1H2:InT y r~ X.lt x yx:elt_x:Info.tr:treex0:X.t_x1:Info.tl1:treex1:X.tr1:treeIHo:Ok (Node _x1 l1 x1 r1) -> forall y0 : elt, max_elt (Node _x1 l1 x1 r1) = Some x -> InT y0 (Node _x1 l1 x1 r1) -> ~ X.lt x y0y:eltH0:max_elt (Node _x1 l1 x1 r1) = Some xH6:Ok rH8:lt_tree x0 rH9:gt_tree x0 (Node _x1 l1 x1 r1)H5:Ok l1H10:Ok r1H11:lt_tree x1 l1H12:gt_tree x1 r1H2:InT y rH:X.lt x0 x1~ X.lt x yorder. Qed.x:elt_x:Info.tr:treex0:X.t_x1:Info.tl1:treex1:X.tr1:treeIHo:Ok (Node _x1 l1 x1 r1) -> forall y0 : elt, max_elt (Node _x1 l1 x1 r1) = Some x -> InT y0 (Node _x1 l1 x1 r1) -> ~ X.lt x y0y:eltH0:max_elt (Node _x1 l1 x1 r1) = Some xH6:Ok rH8:lt_tree x0 rH9:gt_tree x0 (Node _x1 l1 x1 r1)H5:Ok l1H10:Ok r1H11:lt_tree x1 l1H12:gt_tree x1 r1H2:InT y rH:X.lt x0 x1H1:~ X.lt x x1~ X.lt x ys:treemax_elt s = None -> Empty ss:treemax_elt s = None -> Empty sNone = None -> Empty Leaf_x:Info.t_x0:treex:X.tSome x = None -> Empty (Node _x _x0 x Leaf)_x:Info.t_x0:treex:X.t_x1:Info.t_x2:tree_x3:X.t_x4:treeIHo:max_elt (Node _x1 _x2 _x3 _x4) = None -> Empty (Node _x1 _x2 _x3 _x4)max_elt (Node _x1 _x2 _x3 _x4) = None -> Empty (Node _x _x0 x (Node _x1 _x2 _x3 _x4))_x:Info.t_x0:treex:X.tSome x = None -> Empty (Node _x _x0 x Leaf)_x:Info.t_x0:treex:X.t_x1:Info.t_x2:tree_x3:X.t_x4:treeIHo:max_elt (Node _x1 _x2 _x3 _x4) = None -> Empty (Node _x1 _x2 _x3 _x4)max_elt (Node _x1 _x2 _x3 _x4) = None -> Empty (Node _x _x0 x (Node _x1 _x2 _x3 _x4))_x:Info.t_x0:treex:X.t_x1:Info.t_x2:tree_x3:X.t_x4:treeIHo:max_elt (Node _x1 _x2 _x3 _x4) = None -> Empty (Node _x1 _x2 _x3 _x4)max_elt (Node _x1 _x2 _x3 _x4) = None -> Empty (Node _x _x0 x (Node _x1 _x2 _x3 _x4))destruct (IHo H0 _x3); auto. Qed._x:Info.t_x0:treex:X.t_x1:Info.t_x2:tree_x3:X.t_x4:treeIHo:max_elt (Node _x1 _x2 _x3 _x4) = None -> Empty (Node _x1 _x2 _x3 _x4)H0:max_elt (Node _x1 _x2 _x3 _x4) = NoneEmpty (Node _x _x0 x (Node _x1 _x2 _x3 _x4))forall (s : tree) (x : elt), choose s = Some x -> InT x sexact min_elt_spec1. Qed.forall (s : tree) (x : elt), choose s = Some x -> InT x sforall s : tree, choose s = None -> Empty sexact min_elt_spec3. Qed.forall s : tree, choose s = None -> Empty sforall (s s' : tree) (x x' : elt), Ok s -> Ok s' -> choose s = Some x -> choose s' = Some x' -> Equal s s' -> X.eq x x'forall (s s' : tree) (x x' : elt), Ok s -> Ok s' -> choose s = Some x -> choose s' = Some x' -> Equal s s' -> X.eq x x's, s':treex, x':eltHb:Ok sHb':Ok s'Hx:min_elt s = Some xHx':min_elt s' = Some x'H:forall a : elt, InT a s <-> InT a s'X.eq x x's, s':treex, x':eltHb:Ok sHb':Ok s'Hx:min_elt s = Some xHx':min_elt s' = Some x'H:forall a : elt, InT a s <-> InT a s'~ X.lt x x's, s':treex, x':eltHb:Ok sHb':Ok s'Hx:min_elt s = Some xHx':min_elt s' = Some x'H:forall a : elt, InT a s <-> InT a s'H0:~ X.lt x x'X.eq x x's, s':treex, x':eltHb:Ok sHb':Ok s'Hx:min_elt s = Some xHx':min_elt s' = Some x'H:forall a : elt, InT a s <-> InT a s'InT x s's, s':treex, x':eltHb:Ok sHb':Ok s'Hx:min_elt s = Some xHx':min_elt s' = Some x'H:forall a : elt, InT a s <-> InT a s'H0:~ X.lt x x'X.eq x x's, s':treex, x':eltHb:Ok sHb':Ok s'Hx:min_elt s = Some xHx':min_elt s' = Some x'H:forall a : elt, InT a s <-> InT a s'H0:~ X.lt x x'X.eq x x's, s':treex, x':eltHb:Ok sHb':Ok s'Hx:min_elt s = Some xHx':min_elt s' = Some x'H:forall a : elt, InT a s <-> InT a s'H0:~ X.lt x x'~ X.lt x' xs, s':treex, x':eltHb:Ok sHb':Ok s'Hx:min_elt s = Some xHx':min_elt s' = Some x'H:forall a : elt, InT a s <-> InT a s'H0:~ X.lt x x'H1:~ X.lt x' xX.eq x x's, s':treex, x':eltHb:Ok sHb':Ok s'Hx:min_elt s = Some xHx':min_elt s' = Some x'H:forall a : elt, InT a s <-> InT a s'H0:~ X.lt x x'InT x' ss, s':treex, x':eltHb:Ok sHb':Ok s'Hx:min_elt s = Some xHx':min_elt s' = Some x'H:forall a : elt, InT a s <-> InT a s'H0:~ X.lt x x'H1:~ X.lt x' xX.eq x x'elim_compare x x'; intuition. Qed.s, s':treex, x':eltHb:Ok sHb':Ok s'Hx:min_elt s = Some xHx':min_elt s' = Some x'H:forall a : elt, InT a s <-> InT a s'H0:~ X.lt x x'H1:~ X.lt x' xX.eq x x'
forall (s : tree) (acc : list X.t) (x : X.t), InA X.eq x (elements_aux acc s) <-> InT x s \/ InA X.eq x accforall (s : tree) (acc : list X.t) (x : X.t), InA X.eq x (elements_aux acc s) <-> InT x s \/ InA X.eq x accforall (acc : list X.t) (x : X.t), InA X.eq x acc <-> InT x Leaf \/ InA X.eq x accc:Info.tl:treex:X.tr:treeHl:forall (acc : list X.t) (x0 : X.t), InA X.eq x0 (elements_aux acc l) <-> InT x0 l \/ InA X.eq x0 accHr:forall (acc : list X.t) (x0 : X.t), InA X.eq x0 (elements_aux acc r) <-> InT x0 r \/ InA X.eq x0 accforall (acc : list X.t) (x0 : X.t), InA X.eq x0 (elements_aux (x :: elements_aux acc r) l) <-> InT x0 (Node c l x r) \/ InA X.eq x0 accacc:list X.tx:X.tH0:InT x LeafInA X.eq x accc:Info.tl:treex:X.tr:treeHl:forall (acc : list X.t) (x0 : X.t), InA X.eq x0 (elements_aux acc l) <-> InT x0 l \/ InA X.eq x0 accHr:forall (acc : list X.t) (x0 : X.t), InA X.eq x0 (elements_aux acc r) <-> InT x0 r \/ InA X.eq x0 accforall (acc : list X.t) (x0 : X.t), InA X.eq x0 (elements_aux (x :: elements_aux acc r) l) <-> InT x0 (Node c l x r) \/ InA X.eq x0 accc:Info.tl:treex:X.tr:treeHl:forall (acc : list X.t) (x0 : X.t), InA X.eq x0 (elements_aux acc l) <-> InT x0 l \/ InA X.eq x0 accHr:forall (acc : list X.t) (x0 : X.t), InA X.eq x0 (elements_aux acc r) <-> InT x0 r \/ InA X.eq x0 accforall (acc : list X.t) (x0 : X.t), InA X.eq x0 (elements_aux (x :: elements_aux acc r) l) <-> InT x0 (Node c l x r) \/ InA X.eq x0 accc:Info.tl:treex:X.tr:treeHl:forall (acc0 : list X.t) (x1 : X.t), InA X.eq x1 (elements_aux acc0 l) <-> InT x1 l \/ InA X.eq x1 acc0Hr:forall (acc0 : list X.t) (x1 : X.t), InA X.eq x1 (elements_aux acc0 r) <-> InT x1 r \/ InA X.eq x1 acc0acc:list X.tx0:X.tInA X.eq x0 (elements_aux (x :: elements_aux acc r) l) <-> InT x0 (Node c l x r) \/ InA X.eq x0 accc:Info.tl:treex:X.tr:treeHl:forall (acc0 : list X.t) (x1 : X.t), InA X.eq x1 (elements_aux acc0 l) <-> InT x1 l \/ InA X.eq x1 acc0Hr:forall (acc0 : list X.t) (x1 : X.t), InA X.eq x1 (elements_aux acc0 r) <-> InT x1 r \/ InA X.eq x1 acc0acc:list X.tx0:X.tInT x0 l \/ InA X.eq x0 (x :: elements_aux acc r) <-> InT x0 (Node c l x r) \/ InA X.eq x0 accintuition; inversion_clear H3; intuition. Qed.c:Info.tl:treex:X.tr:treeacc:list X.tx0:X.tH:InA X.eq x0 (elements_aux acc r) -> InT x0 r \/ InA X.eq x0 accH0:InT x0 r \/ InA X.eq x0 acc -> InA X.eq x0 (elements_aux acc r)InT x0 l \/ InA X.eq x0 (x :: elements_aux acc r) <-> InT x0 (Node c l x r) \/ InA X.eq x0 accforall (s : tree) (x : X.t), InA X.eq x (elements s) <-> InT x sforall (s : tree) (x : X.t), InA X.eq x (elements s) <-> InT x sinversion_clear H0. Qed.s:treex:X.tH:InT x s -> InA X.eq x (elements_aux nil s)H1:InA X.eq x (elements s)H0:InA X.eq x nilH3:InA X.eq x (elements_aux nil s)InT x sforall (s : tree) (acc : list X.t), Ok s -> Sorted X.lt acc -> (forall x y : elt, InA X.eq x acc -> InT y s -> X.lt y x) -> Sorted X.lt (elements_aux acc s)forall (s : tree) (acc : list X.t), Ok s -> Sorted X.lt acc -> (forall x y : elt, InA X.eq x acc -> InT y s -> X.lt y x) -> Sorted X.lt (elements_aux acc s)c:Info.tl:treey:X.tr:treeHl:forall acc0 : list X.t, Ok l -> Sorted X.lt acc0 -> (forall x y0 : elt, InA X.eq x acc0 -> InT y0 l -> X.lt y0 x) -> Sorted X.lt (elements_aux acc0 l)Hr:forall acc0 : list X.t, Ok r -> Sorted X.lt acc0 -> (forall x y0 : elt, InA X.eq x acc0 -> InT y0 r -> X.lt y0 x) -> Sorted X.lt (elements_aux acc0 r)acc:list X.tH:Ok (Node c l y r)H0:Sorted X.lt accH1:forall x y0 : elt, InA X.eq x acc -> InT y0 (Node c l y r) -> X.lt y0 xSorted X.lt (elements_aux (y :: elements_aux acc r) l)c:Info.tl:treey:X.tr:treeHl:forall acc0 : list X.t, Ok l -> Sorted X.lt acc0 -> (forall x y0 : elt, InA X.eq x acc0 -> InT y0 l -> X.lt y0 x) -> Sorted X.lt (elements_aux acc0 l)Hr:forall acc0 : list X.t, Ok r -> Sorted X.lt acc0 -> (forall x y0 : elt, InA X.eq x acc0 -> InT y0 r -> X.lt y0 x) -> Sorted X.lt (elements_aux acc0 r)acc:list X.tH0:Sorted X.lt accH1:forall x y0 : elt, InA X.eq x acc -> InT y0 (Node c l y r) -> X.lt y0 xH6:Ok lH7:Ok rH8:lt_tree y lH9:gt_tree y rSorted X.lt (elements_aux (y :: elements_aux acc r) l)c:Info.tl:treey:X.tr:treeHl:forall acc0 : list X.t, Ok l -> Sorted X.lt acc0 -> (forall x y0 : elt, InA X.eq x acc0 -> InT y0 l -> X.lt y0 x) -> Sorted X.lt (elements_aux acc0 l)Hr:forall acc0 : list X.t, Ok r -> Sorted X.lt acc0 -> (forall x y0 : elt, InA X.eq x acc0 -> InT y0 r -> X.lt y0 x) -> Sorted X.lt (elements_aux acc0 r)acc:list X.tH0:Sorted X.lt accH1:forall x y0 : elt, InA X.eq x acc -> InT y0 (Node c l y r) -> X.lt y0 xH6:Ok lH7:Ok rH8:lt_tree y lH9:gt_tree y rSorted X.lt (y :: elements_aux acc r)c:Info.tl:treey:X.tr:treeHl:forall acc0 : list X.t, Ok l -> Sorted X.lt acc0 -> (forall x y0 : elt, InA X.eq x acc0 -> InT y0 l -> X.lt y0 x) -> Sorted X.lt (elements_aux acc0 l)Hr:forall acc0 : list X.t, Ok r -> Sorted X.lt acc0 -> (forall x y0 : elt, InA X.eq x acc0 -> InT y0 r -> X.lt y0 x) -> Sorted X.lt (elements_aux acc0 r)acc:list X.tH0:Sorted X.lt accH1:forall x y0 : elt, InA X.eq x acc -> InT y0 (Node c l y r) -> X.lt y0 xH6:Ok lH7:Ok rH8:lt_tree y lH9:gt_tree y rforall x y0 : elt, InA X.eq x (y :: elements_aux acc r) -> InT y0 l -> X.lt y0 xc:Info.tl:treey:X.tr:treeHl:forall acc0 : list X.t, Ok l -> Sorted X.lt acc0 -> (forall x y0 : elt, InA X.eq x acc0 -> InT y0 l -> X.lt y0 x) -> Sorted X.lt (elements_aux acc0 l)Hr:forall acc0 : list X.t, Ok r -> Sorted X.lt acc0 -> (forall x y0 : elt, InA X.eq x acc0 -> InT y0 r -> X.lt y0 x) -> Sorted X.lt (elements_aux acc0 r)acc:list X.tH0:Sorted X.lt accH1:forall x y0 : elt, InA X.eq x acc -> InT y0 (Node c l y r) -> X.lt y0 xH6:Ok lH7:Ok rH8:lt_tree y lH9:gt_tree y rSorted X.lt (elements_aux acc r)c:Info.tl:treey:X.tr:treeHl:forall acc0 : list X.t, Ok l -> Sorted X.lt acc0 -> (forall x y0 : elt, InA X.eq x acc0 -> InT y0 l -> X.lt y0 x) -> Sorted X.lt (elements_aux acc0 l)Hr:forall acc0 : list X.t, Ok r -> Sorted X.lt acc0 -> (forall x y0 : elt, InA X.eq x acc0 -> InT y0 r -> X.lt y0 x) -> Sorted X.lt (elements_aux acc0 r)acc:list X.tH0:Sorted X.lt accH1:forall x y0 : elt, InA X.eq x acc -> InT y0 (Node c l y r) -> X.lt y0 xH6:Ok lH7:Ok rH8:lt_tree y lH9:gt_tree y rHdRel X.lt y (elements_aux acc r)c:Info.tl:treey:X.tr:treeHl:forall acc0 : list X.t, Ok l -> Sorted X.lt acc0 -> (forall x y0 : elt, InA X.eq x acc0 -> InT y0 l -> X.lt y0 x) -> Sorted X.lt (elements_aux acc0 l)Hr:forall acc0 : list X.t, Ok r -> Sorted X.lt acc0 -> (forall x y0 : elt, InA X.eq x acc0 -> InT y0 r -> X.lt y0 x) -> Sorted X.lt (elements_aux acc0 r)acc:list X.tH0:Sorted X.lt accH1:forall x y0 : elt, InA X.eq x acc -> InT y0 (Node c l y r) -> X.lt y0 xH6:Ok lH7:Ok rH8:lt_tree y lH9:gt_tree y rforall x y0 : elt, InA X.eq x (y :: elements_aux acc r) -> InT y0 l -> X.lt y0 xc:Info.tl:treey:X.tr:treeHl:forall acc0 : list X.t, Ok l -> Sorted X.lt acc0 -> (forall x y0 : elt, InA X.eq x acc0 -> InT y0 l -> X.lt y0 x) -> Sorted X.lt (elements_aux acc0 l)Hr:forall acc0 : list X.t, Ok r -> Sorted X.lt acc0 -> (forall x y0 : elt, InA X.eq x acc0 -> InT y0 r -> X.lt y0 x) -> Sorted X.lt (elements_aux acc0 r)acc:list X.tH0:Sorted X.lt accH1:forall x y0 : elt, InA X.eq x acc -> InT y0 (Node c l y r) -> X.lt y0 xH6:Ok lH7:Ok rH8:lt_tree y lH9:gt_tree y rHdRel X.lt y (elements_aux acc r)c:Info.tl:treey:X.tr:treeHl:forall acc0 : list X.t, Ok l -> Sorted X.lt acc0 -> (forall x y0 : elt, InA X.eq x acc0 -> InT y0 l -> X.lt y0 x) -> Sorted X.lt (elements_aux acc0 l)Hr:forall acc0 : list X.t, Ok r -> Sorted X.lt acc0 -> (forall x y0 : elt, InA X.eq x acc0 -> InT y0 r -> X.lt y0 x) -> Sorted X.lt (elements_aux acc0 r)acc:list X.tH0:Sorted X.lt accH1:forall x y0 : elt, InA X.eq x acc -> InT y0 (Node c l y r) -> X.lt y0 xH6:Ok lH7:Ok rH8:lt_tree y lH9:gt_tree y rforall x y0 : elt, InA X.eq x (y :: elements_aux acc r) -> InT y0 l -> X.lt y0 xc:Info.tl:treey:X.tr:treeHl:forall acc0 : list X.t, Ok l -> Sorted X.lt acc0 -> (forall x y0 : elt, InA X.eq x acc0 -> InT y0 l -> X.lt y0 x) -> Sorted X.lt (elements_aux acc0 l)Hr:forall acc0 : list X.t, Ok r -> Sorted X.lt acc0 -> (forall x y0 : elt, InA X.eq x acc0 -> InT y0 r -> X.lt y0 x) -> Sorted X.lt (elements_aux acc0 r)acc:list X.tH0:Sorted X.lt accH1:forall x y0 : elt, InA X.eq x acc -> InT y0 (Node c l y r) -> X.lt y0 xH6:Ok lH7:Ok rH8:lt_tree y lH9:gt_tree y rforall y0 : X.t, InA OrderTac.TO.eq y0 (elements_aux acc r) -> X.lt y y0c:Info.tl:treey:X.tr:treeHl:forall acc0 : list X.t, Ok l -> Sorted X.lt acc0 -> (forall x y0 : elt, InA X.eq x acc0 -> InT y0 l -> X.lt y0 x) -> Sorted X.lt (elements_aux acc0 l)Hr:forall acc0 : list X.t, Ok r -> Sorted X.lt acc0 -> (forall x y0 : elt, InA X.eq x acc0 -> InT y0 r -> X.lt y0 x) -> Sorted X.lt (elements_aux acc0 r)acc:list X.tH0:Sorted X.lt accH1:forall x y0 : elt, InA X.eq x acc -> InT y0 (Node c l y r) -> X.lt y0 xH6:Ok lH7:Ok rH8:lt_tree y lH9:gt_tree y rforall x y0 : elt, InA X.eq x (y :: elements_aux acc r) -> InT y0 l -> X.lt y0 xc:Info.tl:treey:X.tr:treeHl:forall acc0 : list X.t, Ok l -> Sorted X.lt acc0 -> (forall x y1 : elt, InA X.eq x acc0 -> InT y1 l -> X.lt y1 x) -> Sorted X.lt (elements_aux acc0 l)Hr:forall acc0 : list X.t, Ok r -> Sorted X.lt acc0 -> (forall x y1 : elt, InA X.eq x acc0 -> InT y1 r -> X.lt y1 x) -> Sorted X.lt (elements_aux acc0 r)acc:list X.tH0:Sorted X.lt accH1:forall x y1 : elt, InA X.eq x acc -> InT y1 (Node c l y r) -> X.lt y1 xH6:Ok lH7:Ok rH8:lt_tree y lH9:gt_tree y ry0:X.tH:InA OrderTac.TO.eq y0 (elements_aux acc r)X.lt y y0c:Info.tl:treey:X.tr:treeHl:forall acc0 : list X.t, Ok l -> Sorted X.lt acc0 -> (forall x y0 : elt, InA X.eq x acc0 -> InT y0 l -> X.lt y0 x) -> Sorted X.lt (elements_aux acc0 l)Hr:forall acc0 : list X.t, Ok r -> Sorted X.lt acc0 -> (forall x y0 : elt, InA X.eq x acc0 -> InT y0 r -> X.lt y0 x) -> Sorted X.lt (elements_aux acc0 r)acc:list X.tH0:Sorted X.lt accH1:forall x y0 : elt, InA X.eq x acc -> InT y0 (Node c l y r) -> X.lt y0 xH6:Ok lH7:Ok rH8:lt_tree y lH9:gt_tree y rforall x y0 : elt, InA X.eq x (y :: elements_aux acc r) -> InT y0 l -> X.lt y0 xc:Info.tl:treey:X.tr:treeHl:forall acc0 : list X.t, Ok l -> Sorted X.lt acc0 -> (forall x y0 : elt, InA X.eq x acc0 -> InT y0 l -> X.lt y0 x) -> Sorted X.lt (elements_aux acc0 l)Hr:forall acc0 : list X.t, Ok r -> Sorted X.lt acc0 -> (forall x y0 : elt, InA X.eq x acc0 -> InT y0 r -> X.lt y0 x) -> Sorted X.lt (elements_aux acc0 r)acc:list X.tH0:Sorted X.lt accH1:forall x y0 : elt, InA X.eq x acc -> InT y0 (Node c l y r) -> X.lt y0 xH6:Ok lH7:Ok rH8:lt_tree y lH9:gt_tree y rforall x y0 : elt, InA X.eq x (y :: elements_aux acc r) -> InT y0 l -> X.lt y0 xc:Info.tl:treey:X.tr:treeHl:forall acc0 : list X.t, Ok l -> Sorted X.lt acc0 -> (forall x0 y1 : elt, InA X.eq x0 acc0 -> InT y1 l -> X.lt y1 x0) -> Sorted X.lt (elements_aux acc0 l)Hr:forall acc0 : list X.t, Ok r -> Sorted X.lt acc0 -> (forall x0 y1 : elt, InA X.eq x0 acc0 -> InT y1 r -> X.lt y1 x0) -> Sorted X.lt (elements_aux acc0 r)acc:list X.tH0:Sorted X.lt accH1:forall x0 y1 : elt, InA X.eq x0 acc -> InT y1 (Node c l y r) -> X.lt y1 x0H6:Ok lH7:Ok rH8:lt_tree y lH9:gt_tree y rx, y0:eltH:InA X.eq x (y :: elements_aux acc r)H2:InT y0 lX.lt y0 xc:Info.tl:treey:X.tr:treeHl:forall acc0 : list X.t, Ok l -> Sorted X.lt acc0 -> (forall x0 y1 : elt, InA X.eq x0 acc0 -> InT y1 l -> X.lt y1 x0) -> Sorted X.lt (elements_aux acc0 l)Hr:forall acc0 : list X.t, Ok r -> Sorted X.lt acc0 -> (forall x0 y1 : elt, InA X.eq x0 acc0 -> InT y1 r -> X.lt y1 x0) -> Sorted X.lt (elements_aux acc0 r)acc:list X.tH0:Sorted X.lt accH1:forall x0 y1 : elt, InA X.eq x0 acc -> InT y1 (Node c l y r) -> X.lt y1 x0H6:Ok lH7:Ok rH8:lt_tree y lH9:gt_tree y rx, y0:eltH2:InT y0 lH3:X.eq x yX.lt y0 xc:Info.tl:treey:X.tr:treeHl:forall acc0 : list X.t, Ok l -> Sorted X.lt acc0 -> (forall x0 y1 : elt, InA X.eq x0 acc0 -> InT y1 l -> X.lt y1 x0) -> Sorted X.lt (elements_aux acc0 l)Hr:forall acc0 : list X.t, Ok r -> Sorted X.lt acc0 -> (forall x0 y1 : elt, InA X.eq x0 acc0 -> InT y1 r -> X.lt y1 x0) -> Sorted X.lt (elements_aux acc0 r)acc:list X.tH0:Sorted X.lt accH1:forall x0 y1 : elt, InA X.eq x0 acc -> InT y1 (Node c l y r) -> X.lt y1 x0H6:Ok lH7:Ok rH8:lt_tree y lH9:gt_tree y rx, y0:eltH2:InT y0 lH3:InA X.eq x (elements_aux acc r)X.lt y0 xdestruct (elements_spec1' r acc x); intuition eauto. Qed.c:Info.tl:treey:X.tr:treeHl:forall acc0 : list X.t, Ok l -> Sorted X.lt acc0 -> (forall x0 y1 : elt, InA X.eq x0 acc0 -> InT y1 l -> X.lt y1 x0) -> Sorted X.lt (elements_aux acc0 l)Hr:forall acc0 : list X.t, Ok r -> Sorted X.lt acc0 -> (forall x0 y1 : elt, InA X.eq x0 acc0 -> InT y1 r -> X.lt y1 x0) -> Sorted X.lt (elements_aux acc0 r)acc:list X.tH0:Sorted X.lt accH1:forall x0 y1 : elt, InA X.eq x0 acc -> InT y1 (Node c l y r) -> X.lt y1 x0H6:Ok lH7:Ok rH8:lt_tree y lH9:gt_tree y rx, y0:eltH2:InT y0 lH3:InA X.eq x (elements_aux acc r)X.lt y0 xforall s : tree, Ok s -> Sorted X.lt (elements s)forall s : tree, Ok s -> Sorted X.lt (elements s)intros; inversion H0. Qed. Local Hint Resolve elements_spec2 : core.s:treeH:Ok sforall x y : elt, InA X.eq x nil -> InT y s -> X.lt y xforall s : tree, Ok s -> NoDupA X.eq (elements s)forall s : tree, Ok s -> NoDupA X.eq (elements s)eapply SortA_NoDupA; eauto with *. Qed.s:treeH:Ok sNoDupA X.eq (elements s)forall (s : tree) (acc : list X.t), length acc + cardinal s = length (elements_aux acc s)forall (s : tree) (acc : list X.t), length acc + cardinal s = length (elements_aux acc s)s:treet:Info.tt0:treeH:forall acc0 : list X.t, length acc0 + cardinal t0 = length (elements_aux acc0 t0)t1:X.tt2:treeH0:forall acc0 : list X.t, length acc0 + cardinal t2 = length (elements_aux acc0 t2)acc:list X.tlength acc + S (cardinal t0 + cardinal t2) = length (elements_aux (t1 :: elements_aux acc t2) t0)s:treet:Info.tt0:treeH:forall acc0 : list X.t, length acc0 + cardinal t0 = length (elements_aux acc0 t0)t1:X.tt2:treeH0:forall acc0 : list X.t, length acc0 + cardinal t2 = length (elements_aux acc0 t2)acc:list X.tlength acc + S (cardinal t0 + cardinal t2) = length (t1 :: elements_aux acc t2) + cardinal t0s:treet:Info.tt0:treeH:forall acc0 : list X.t, length acc0 + cardinal t0 = length (elements_aux acc0 t0)t1:X.tt2:treeH0:forall acc0 : list X.t, length acc0 + cardinal t2 = length (elements_aux acc0 t2)acc:list X.tlength acc + S (cardinal t0 + cardinal t2) = S (length (elements_aux acc t2) + cardinal t0)s:treet:Info.tt0:treeH:forall acc0 : list X.t, length acc0 + cardinal t0 = length (elements_aux acc0 t0)t1:X.tt2:treeH0:forall acc0 : list X.t, length acc0 + cardinal t2 = length (elements_aux acc0 t2)acc:list X.tlength acc + S (cardinal t0 + cardinal t2) = S (length acc + cardinal t2 + cardinal t0)now rewrite <- Nat.add_succ_r, Nat.add_assoc. Qed.s:treet:Info.tt0:treeH:forall acc0 : list X.t, length acc0 + cardinal t0 = length (elements_aux acc0 t0)t1:X.tt2:treeH0:forall acc0 : list X.t, length acc0 + cardinal t2 = length (elements_aux acc0 t2)acc:list X.tlength acc + S (cardinal t2 + cardinal t0) = S (length acc + cardinal t2 + cardinal t0)forall s : tree, cardinal s = length (elements s)exact (fun s => elements_aux_cardinal s nil). Qed. Definition cardinal_spec (s:tree)(Hs:Ok s) := elements_cardinal s.forall s : tree, cardinal s = length (elements s)forall (s : tree) (acc : list X.t), elements_aux acc s = elements s ++ accforall (s : tree) (acc : list X.t), elements_aux acc s = elements s ++ acct:Info.ts1:treet0:X.ts2:treeIHs1:forall acc0 : list X.t, elements_aux acc0 s1 = elements s1 ++ acc0IHs2:forall acc0 : list X.t, elements_aux acc0 s2 = elements s2 ++ acc0acc:list X.telements_aux (t0 :: elements_aux acc s2) s1 = elements (Node t s1 t0 s2) ++ acct:Info.ts1:treet0:X.ts2:treeIHs1:forall acc0 : list X.t, elements_aux acc0 s1 = elements s1 ++ acc0IHs2:forall acc0 : list X.t, elements_aux acc0 s2 = elements s2 ++ acc0acc:list X.telements s1 ++ t0 :: elements s2 ++ acc = elements (Node t s1 t0 s2) ++ accrewrite 2 IHs1, IHs2, !app_nil_r, !app_ass; auto. Qed.t:Info.ts1:treet0:X.ts2:treeIHs1:forall acc0 : list X.t, elements_aux acc0 s1 = elements s1 ++ acc0IHs2:forall acc0 : list X.t, elements_aux acc0 s2 = elements s2 ++ acc0acc:list X.telements_aux nil s1 ++ t0 :: elements_aux nil s2 ++ acc = elements_aux (t0 :: elements_aux nil s2) s1 ++ accc:Info.tl:treex:X.tr:treeelements (Node c l x r) = elements l ++ x :: elements rc:Info.tl:treex:X.tr:treeelements (Node c l x r) = elements l ++ x :: elements rnow rewrite !elements_app, !app_nil_r. Qed.c:Info.tl:treex:X.tr:treeelements_aux (x :: elements_aux nil r) l = elements_aux nil l ++ x :: elements_aux nil rforall (s : tree) (acc : list X.t), rev_elements_aux acc s = rev_elements s ++ accforall (s : tree) (acc : list X.t), rev_elements_aux acc s = rev_elements s ++ acct:Info.ts1:treet0:X.ts2:treeIHs1:forall acc0 : list X.t, rev_elements_aux acc0 s1 = rev_elements s1 ++ acc0IHs2:forall acc0 : list X.t, rev_elements_aux acc0 s2 = rev_elements s2 ++ acc0acc:list X.trev_elements_aux (t0 :: rev_elements_aux acc s1) s2 = rev_elements (Node t s1 t0 s2) ++ acct:Info.ts1:treet0:X.ts2:treeIHs1:forall acc0 : list X.t, rev_elements_aux acc0 s1 = rev_elements s1 ++ acc0IHs2:forall acc0 : list X.t, rev_elements_aux acc0 s2 = rev_elements s2 ++ acc0acc:list X.trev_elements s2 ++ t0 :: rev_elements s1 ++ acc = rev_elements (Node t s1 t0 s2) ++ accrewrite IHs1, 2 IHs2, !app_nil_r, !app_ass; auto. Qed.t:Info.ts1:treet0:X.ts2:treeIHs1:forall acc0 : list X.t, rev_elements_aux acc0 s1 = rev_elements s1 ++ acc0IHs2:forall acc0 : list X.t, rev_elements_aux acc0 s2 = rev_elements s2 ++ acc0acc:list X.trev_elements_aux nil s2 ++ t0 :: rev_elements_aux nil s1 ++ acc = rev_elements_aux (t0 :: rev_elements_aux nil s1) s2 ++ accc:Info.tl:treex:X.tr:treerev_elements (Node c l x r) = rev_elements r ++ x :: rev_elements lc:Info.tl:treex:X.tr:treerev_elements (Node c l x r) = rev_elements r ++ x :: rev_elements lnow rewrite !rev_elements_app, !app_nil_r. Qed.c:Info.tl:treex:X.tr:treerev_elements_aux (x :: rev_elements_aux nil l) r = rev_elements_aux nil r ++ x :: rev_elements_aux nil ls:treerev_elements s = rev (elements s)s:treerev_elements s = rev (elements s)c:Info.tl:treex:X.tr:treeIHl:rev_elements l = rev (elements l)IHr:rev_elements r = rev (elements r)rev_elements (Node c l x r) = rev (elements (Node c l x r))c:Info.tl:treex:X.tr:treeIHl:rev_elements l = rev (elements l)IHr:rev_elements r = rev (elements r)rev (elements r) ++ x :: rev (elements l) = rev (x :: elements r) ++ rev (elements l)now rewrite !app_ass. Qed.c:Info.tl:treex:X.tr:treeIHl:rev_elements l = rev (elements l)IHr:rev_elements r = rev (elements r)rev (elements r) ++ x :: rev (elements l) = (rev (elements r) ++ x :: nil) ++ rev (elements l)
The converse of elements_spec2, used in MSetRBT
(* TODO: TO MIGRATE ELSEWHERE... *)l1, l2:list X.tSorted X.lt (l1 ++ l2) -> Sorted X.lt l1 /\ Sorted X.lt l2 /\ (forall x1 x2 : X.t, InA X.eq x1 l1 -> InA X.eq x2 l2 -> X.lt x1 x2)l1, l2:list X.tSorted X.lt (l1 ++ l2) -> Sorted X.lt l1 /\ Sorted X.lt l2 /\ (forall x1 x2 : X.t, InA X.eq x1 l1 -> InA X.eq x2 l2 -> X.lt x1 x2)l2:list X.tSorted X.lt (nil ++ l2) -> Sorted X.lt nil /\ Sorted X.lt l2 /\ (forall x1 x2 : X.t, InA X.eq x1 nil -> InA X.eq x2 l2 -> X.lt x1 x2)a1:X.tl1, l2:list X.tIHl1:Sorted X.lt (l1 ++ l2) -> Sorted X.lt l1 /\ Sorted X.lt l2 /\ (forall x1 x2 : X.t, InA X.eq x1 l1 -> InA X.eq x2 l2 -> X.lt x1 x2)Sorted X.lt ((a1 :: l1) ++ l2) -> Sorted X.lt (a1 :: l1) /\ Sorted X.lt l2 /\ (forall x1 x2 : X.t, InA X.eq x1 (a1 :: l1) -> InA X.eq x2 l2 -> X.lt x1 x2)l2:list X.tSorted X.lt (nil ++ l2) -> Sorted X.lt nil /\ Sorted X.lt l2 /\ (forall x1 x2 : X.t, InA X.eq x1 nil -> InA X.eq x2 l2 -> X.lt x1 x2)l2:list X.tH:Sorted X.lt l2forall x1 x2 : X.t, InA X.eq x1 nil -> InA X.eq x2 l2 -> X.lt x1 x2now rewrite InA_nil in *.l2:list X.tH:Sorted X.lt l2x1, x2:X.tH0:InA X.eq x1 nilH1:InA X.eq x2 l2X.lt x1 x2a1:X.tl1, l2:list X.tIHl1:Sorted X.lt (l1 ++ l2) -> Sorted X.lt l1 /\ Sorted X.lt l2 /\ (forall x1 x2 : X.t, InA X.eq x1 l1 -> InA X.eq x2 l2 -> X.lt x1 x2)Sorted X.lt ((a1 :: l1) ++ l2) -> Sorted X.lt (a1 :: l1) /\ Sorted X.lt l2 /\ (forall x1 x2 : X.t, InA X.eq x1 (a1 :: l1) -> InA X.eq x2 l2 -> X.lt x1 x2)a1:X.tl1, l2:list X.tIHl1:Sorted X.lt (l1 ++ l2) -> Sorted X.lt l1 /\ Sorted X.lt l2 /\ (forall x1 x2 : X.t, InA X.eq x1 l1 -> InA X.eq x2 l2 -> X.lt x1 x2)Sorted X.lt (a1 :: l1 ++ l2) -> Sorted X.lt (a1 :: l1) /\ Sorted X.lt l2 /\ (forall x1 x2 : X.t, InA X.eq x1 (a1 :: l1) -> InA X.eq x2 l2 -> X.lt x1 x2)a1:X.tl1, l2:list X.tIHl1:Sorted X.lt (l1 ++ l2) -> Sorted X.lt l1 /\ Sorted X.lt l2 /\ (forall x1 x2 : X.t, InA X.eq x1 l1 -> InA X.eq x2 l2 -> X.lt x1 x2)Hs:Sorted X.lt (l1 ++ l2)Hhd:HdRel X.lt a1 (l1 ++ l2)Sorted X.lt (a1 :: l1) /\ Sorted X.lt l2 /\ (forall x1 x2 : X.t, InA X.eq x1 (a1 :: l1) -> InA X.eq x2 l2 -> X.lt x1 x2)a1:X.tl1, l2:list X.tIHl1:Sorted X.lt (l1 ++ l2) -> Sorted X.lt l1 /\ Sorted X.lt l2 /\ (forall x1 x2 : X.t, InA X.eq x1 l1 -> InA X.eq x2 l2 -> X.lt x1 x2)Hs:Sorted X.lt (l1 ++ l2)Hhd:HdRel X.lt a1 (l1 ++ l2)H1:Sorted X.lt l1H2:Sorted X.lt l2H3:forall x1 x2 : X.t, InA X.eq x1 l1 -> InA X.eq x2 l2 -> X.lt x1 x2Sorted X.lt (a1 :: l1) /\ Sorted X.lt l2 /\ (forall x1 x2 : X.t, InA X.eq x1 (a1 :: l1) -> InA X.eq x2 l2 -> X.lt x1 x2)a1:X.tl1, l2:list X.tIHl1:Sorted X.lt (l1 ++ l2) -> Sorted X.lt l1 /\ Sorted X.lt l2 /\ (forall x1 x2 : X.t, InA X.eq x1 l1 -> InA X.eq x2 l2 -> X.lt x1 x2)Hs:Sorted X.lt (l1 ++ l2)Hhd:HdRel X.lt a1 (l1 ++ l2)H1:Sorted X.lt l1H2:Sorted X.lt l2H3:forall x1 x2 : X.t, InA X.eq x1 l1 -> InA X.eq x2 l2 -> X.lt x1 x2Sorted X.lt (a1 :: l1)a1:X.tl1, l2:list X.tIHl1:Sorted X.lt (l1 ++ l2) -> Sorted X.lt l1 /\ Sorted X.lt l2 /\ (forall x1 x2 : X.t, InA X.eq x1 l1 -> InA X.eq x2 l2 -> X.lt x1 x2)Hs:Sorted X.lt (l1 ++ l2)Hhd:HdRel X.lt a1 (l1 ++ l2)H1:Sorted X.lt l1H2:Sorted X.lt l2H3:forall x1 x2 : X.t, InA X.eq x1 l1 -> InA X.eq x2 l2 -> X.lt x1 x2Sorted X.lt l2a1:X.tl1, l2:list X.tIHl1:Sorted X.lt (l1 ++ l2) -> Sorted X.lt l1 /\ Sorted X.lt l2 /\ (forall x1 x2 : X.t, InA X.eq x1 l1 -> InA X.eq x2 l2 -> X.lt x1 x2)Hs:Sorted X.lt (l1 ++ l2)Hhd:HdRel X.lt a1 (l1 ++ l2)H1:Sorted X.lt l1H2:Sorted X.lt l2H3:forall x1 x2 : X.t, InA X.eq x1 l1 -> InA X.eq x2 l2 -> X.lt x1 x2forall x1 x2 : X.t, InA X.eq x1 (a1 :: l1) -> InA X.eq x2 l2 -> X.lt x1 x2a1:X.tl1, l2:list X.tIHl1:Sorted X.lt (l1 ++ l2) -> Sorted X.lt l1 /\ Sorted X.lt l2 /\ (forall x1 x2 : X.t, InA X.eq x1 l1 -> InA X.eq x2 l2 -> X.lt x1 x2)Hs:Sorted X.lt (l1 ++ l2)Hhd:HdRel X.lt a1 (l1 ++ l2)H1:Sorted X.lt l1H2:Sorted X.lt l2H3:forall x1 x2 : X.t, InA X.eq x1 l1 -> InA X.eq x2 l2 -> X.lt x1 x2Sorted X.lt (a1 :: l1)destruct l1; simpl in *; auto; inversion_clear Hhd; auto.a1:X.tl1, l2:list X.tIHl1:Sorted X.lt (l1 ++ l2) -> Sorted X.lt l1 /\ Sorted X.lt l2 /\ (forall x1 x2 : X.t, InA X.eq x1 l1 -> InA X.eq x2 l2 -> X.lt x1 x2)Hs:Sorted X.lt (l1 ++ l2)Hhd:HdRel X.lt a1 (l1 ++ l2)H1:Sorted X.lt l1H2:Sorted X.lt l2H3:forall x1 x2 : X.t, InA X.eq x1 l1 -> InA X.eq x2 l2 -> X.lt x1 x2HdRel X.lt a1 l1trivial.a1:X.tl1, l2:list X.tIHl1:Sorted X.lt (l1 ++ l2) -> Sorted X.lt l1 /\ Sorted X.lt l2 /\ (forall x1 x2 : X.t, InA X.eq x1 l1 -> InA X.eq x2 l2 -> X.lt x1 x2)Hs:Sorted X.lt (l1 ++ l2)Hhd:HdRel X.lt a1 (l1 ++ l2)H1:Sorted X.lt l1H2:Sorted X.lt l2H3:forall x1 x2 : X.t, InA X.eq x1 l1 -> InA X.eq x2 l2 -> X.lt x1 x2Sorted X.lt l2a1:X.tl1, l2:list X.tIHl1:Sorted X.lt (l1 ++ l2) -> Sorted X.lt l1 /\ Sorted X.lt l2 /\ (forall x1 x2 : X.t, InA X.eq x1 l1 -> InA X.eq x2 l2 -> X.lt x1 x2)Hs:Sorted X.lt (l1 ++ l2)Hhd:HdRel X.lt a1 (l1 ++ l2)H1:Sorted X.lt l1H2:Sorted X.lt l2H3:forall x1 x2 : X.t, InA X.eq x1 l1 -> InA X.eq x2 l2 -> X.lt x1 x2forall x1 x2 : X.t, InA X.eq x1 (a1 :: l1) -> InA X.eq x2 l2 -> X.lt x1 x2a1:X.tl1, l2:list X.tIHl1:Sorted X.lt (l1 ++ l2) -> Sorted X.lt l1 /\ Sorted X.lt l2 /\ (forall x0 x3 : X.t, InA X.eq x0 l1 -> InA X.eq x3 l2 -> X.lt x0 x3)Hs:Sorted X.lt (l1 ++ l2)Hhd:HdRel X.lt a1 (l1 ++ l2)H1:Sorted X.lt l1H2:Sorted X.lt l2H3:forall x0 x3 : X.t, InA X.eq x0 l1 -> InA X.eq x3 l2 -> X.lt x0 x3x1, x2:X.tHx1:InA X.eq x1 (a1 :: l1)Hx2:InA X.eq x2 l2X.lt x1 x2a1:X.tl1, l2:list X.tIHl1:Sorted X.lt (l1 ++ l2) -> Sorted X.lt l1 /\ Sorted X.lt l2 /\ (forall x0 x3 : X.t, InA X.eq x0 l1 -> InA X.eq x3 l2 -> X.lt x0 x3)Hs:Sorted X.lt (l1 ++ l2)Hhd:HdRel X.lt a1 (l1 ++ l2)H1:Sorted X.lt l1H2:Sorted X.lt l2H3:forall x0 x3 : X.t, InA X.eq x0 l1 -> InA X.eq x3 l2 -> X.lt x0 x3x1, x2:X.tHx1:X.eq x1 a1 \/ InA X.eq x1 l1Hx2:InA X.eq x2 l2X.lt x1 x2a1:X.tl1, l2:list X.tIHl1:Sorted X.lt (l1 ++ l2) -> Sorted X.lt l1 /\ Sorted X.lt l2 /\ (forall x0 x3 : X.t, InA X.eq x0 l1 -> InA X.eq x3 l2 -> X.lt x0 x3)Hs:Sorted X.lt (l1 ++ l2)Hhd:HdRel X.lt a1 (l1 ++ l2)H1:Sorted X.lt l1H2:Sorted X.lt l2H3:forall x0 x3 : X.t, InA X.eq x0 l1 -> InA X.eq x3 l2 -> X.lt x0 x3x1, x2:X.tH:X.eq x1 a1Hx2:InA X.eq x2 l2X.lt x1 x2a1:X.tl1, l2:list X.tIHl1:Sorted X.lt (l1 ++ l2) -> Sorted X.lt l1 /\ Sorted X.lt l2 /\ (forall x0 x3 : X.t, InA X.eq x0 l1 -> InA X.eq x3 l2 -> X.lt x0 x3)Hs:Sorted X.lt (l1 ++ l2)Hhd:HdRel X.lt a1 (l1 ++ l2)H1:Sorted X.lt l1H2:Sorted X.lt l2H3:forall x0 x3 : X.t, InA X.eq x0 l1 -> InA X.eq x3 l2 -> X.lt x0 x3x1, x2:X.tH:InA X.eq x1 l1Hx2:InA X.eq x2 l2X.lt x1 x2a1:X.tl1, l2:list X.tIHl1:Sorted X.lt (l1 ++ l2) -> Sorted X.lt l1 /\ Sorted X.lt l2 /\ (forall x0 x3 : X.t, InA X.eq x0 l1 -> InA X.eq x3 l2 -> X.lt x0 x3)Hs:Sorted X.lt (l1 ++ l2)Hhd:HdRel X.lt a1 (l1 ++ l2)H1:Sorted X.lt l1H2:Sorted X.lt l2H3:forall x0 x3 : X.t, InA X.eq x0 l1 -> InA X.eq x3 l2 -> X.lt x0 x3x1, x2:X.tH:X.eq x1 a1Hx2:InA X.eq x2 l2X.lt x1 x2a1:X.tl1, l2:list X.tIHl1:Sorted X.lt (l1 ++ l2) -> Sorted X.lt l1 /\ Sorted X.lt l2 /\ (forall x0 x3 : X.t, InA X.eq x0 l1 -> InA X.eq x3 l2 -> X.lt x0 x3)Hs:Sorted X.lt (l1 ++ l2)Hhd:HdRel X.lt a1 (l1 ++ l2)H1:Sorted X.lt l1H2:Sorted X.lt l2H3:forall x0 x3 : X.t, InA X.eq x0 l1 -> InA X.eq x3 l2 -> X.lt x0 x3x1, x2:X.tH:X.eq x1 a1Hx2:InA X.eq x2 l2X.lt a1 x2rewrite InA_app_iff; auto_tc.a1:X.tl1, l2:list X.tIHl1:Sorted X.lt (l1 ++ l2) -> Sorted X.lt l1 /\ Sorted X.lt l2 /\ (forall x0 x3 : X.t, InA X.eq x0 l1 -> InA X.eq x3 l2 -> X.lt x0 x3)Hs:Sorted X.lt (l1 ++ l2)Hhd:HdRel X.lt a1 (l1 ++ l2)H1:Sorted X.lt l1H2:Sorted X.lt l2H3:forall x0 x3 : X.t, InA X.eq x0 l1 -> InA X.eq x3 l2 -> X.lt x0 x3x1, x2:X.tH:X.eq x1 a1Hx2:InA X.eq x2 l2InA X.eq x2 (l1 ++ l2)auto. Qed.a1:X.tl1, l2:list X.tIHl1:Sorted X.lt (l1 ++ l2) -> Sorted X.lt l1 /\ Sorted X.lt l2 /\ (forall x0 x3 : X.t, InA X.eq x0 l1 -> InA X.eq x3 l2 -> X.lt x0 x3)Hs:Sorted X.lt (l1 ++ l2)Hhd:HdRel X.lt a1 (l1 ++ l2)H1:Sorted X.lt l1H2:Sorted X.lt l2H3:forall x0 x3 : X.t, InA X.eq x0 l1 -> InA X.eq x3 l2 -> X.lt x0 x3x1, x2:X.tH:InA X.eq x1 l1Hx2:InA X.eq x2 l2X.lt x1 x2s:treeSorted X.lt (elements s) -> Ok ss:treeSorted X.lt (elements s) -> Ok sSorted X.lt (elements Leaf) -> Ok Leafc:Info.tl:treex:X.tr:treeIHl:Sorted X.lt (elements l) -> Ok lIHr:Sorted X.lt (elements r) -> Ok rSorted X.lt (elements (Node c l x r)) -> Ok (Node c l x r)auto.Sorted X.lt (elements Leaf) -> Ok Leafc:Info.tl:treex:X.tr:treeIHl:Sorted X.lt (elements l) -> Ok lIHr:Sorted X.lt (elements r) -> Ok rSorted X.lt (elements (Node c l x r)) -> Ok (Node c l x r)c:Info.tl:treex:X.tr:treeIHl:Sorted X.lt (elements l) -> Ok lIHr:Sorted X.lt (elements r) -> Ok rSorted X.lt (elements l ++ x :: elements r) -> Ok (Node c l x r)c:Info.tl:treex:X.tr:treeIHl:Sorted X.lt (elements l) -> Ok lIHr:Sorted X.lt (elements r) -> Ok rH:Sorted X.lt (elements l ++ x :: elements r)Ok (Node c l x r)c:Info.tl:treex:X.tr:treeIHl:Sorted X.lt (elements l) -> Ok lIHr:Sorted X.lt (elements r) -> Ok rH:Sorted X.lt (elements l ++ x :: elements r)H1:Sorted X.lt (elements l)H2:Sorted X.lt (x :: elements r)H3:forall x1 x2 : X.t, InA X.eq x1 (elements l) -> InA X.eq x2 (x :: elements r) -> X.lt x1 x2Ok (Node c l x r)c:Info.tl:treex:X.tr:treeIHl:Sorted X.lt (elements l) -> Ok lIHr:Sorted X.lt (elements r) -> Ok rH:Sorted X.lt (elements l ++ x :: elements r)H1:Sorted X.lt (elements l)H3:forall x1 x2 : X.t, InA X.eq x1 (elements l) -> InA X.eq x2 (x :: elements r) -> X.lt x1 x2H0:Sorted X.lt (elements r)H4:HdRel X.lt x (elements r)Ok (Node c l x r)c:Info.tl:treex:X.tr:treeIHl:Sorted X.lt (elements l) -> Ok lIHr:Sorted X.lt (elements r) -> Ok rH:Sorted X.lt (elements l ++ x :: elements r)H1:Sorted X.lt (elements l)H3:forall x1 x2 : X.t, InA X.eq x1 (elements l) -> InA X.eq x2 (x :: elements r) -> X.lt x1 x2H0:Sorted X.lt (elements r)H4:HdRel X.lt x (elements r)lt_tree x lc:Info.tl:treex:X.tr:treeIHl:Sorted X.lt (elements l) -> Ok lIHr:Sorted X.lt (elements r) -> Ok rH:Sorted X.lt (elements l ++ x :: elements r)H1:Sorted X.lt (elements l)H3:forall x1 x2 : X.t, InA X.eq x1 (elements l) -> InA X.eq x2 (x :: elements r) -> X.lt x1 x2H0:Sorted X.lt (elements r)H4:HdRel X.lt x (elements r)gt_tree x rc:Info.tl:treex:X.tr:treeIHl:Sorted X.lt (elements l) -> Ok lIHr:Sorted X.lt (elements r) -> Ok rH:Sorted X.lt (elements l ++ x :: elements r)H1:Sorted X.lt (elements l)H3:forall x1 x2 : X.t, InA X.eq x1 (elements l) -> InA X.eq x2 (x :: elements r) -> X.lt x1 x2H0:Sorted X.lt (elements r)H4:HdRel X.lt x (elements r)lt_tree x lc:Info.tl:treex:X.tr:treeIHl:Sorted X.lt (elements l) -> Ok lIHr:Sorted X.lt (elements r) -> Ok rH:Sorted X.lt (elements l ++ x :: elements r)H1:Sorted X.lt (elements l)H3:forall x1 x2 : X.t, InA X.eq x1 (elements l) -> InA X.eq x2 (x :: elements r) -> X.lt x1 x2H0:Sorted X.lt (elements r)H4:HdRel X.lt x (elements r)y:eltHy:InT y lX.lt y xc:Info.tl:treex:X.tr:treeIHl:Sorted X.lt (elements l) -> Ok lIHr:Sorted X.lt (elements r) -> Ok rH:Sorted X.lt (elements l ++ x :: elements r)H1:Sorted X.lt (elements l)H3:forall x1 x2 : X.t, InA X.eq x1 (elements l) -> InA X.eq x2 (x :: elements r) -> X.lt x1 x2H0:Sorted X.lt (elements r)H4:HdRel X.lt x (elements r)y:eltHy:InT y lInA X.eq y (elements l)c:Info.tl:treex:X.tr:treeIHl:Sorted X.lt (elements l) -> Ok lIHr:Sorted X.lt (elements r) -> Ok rH:Sorted X.lt (elements l ++ x :: elements r)H1:Sorted X.lt (elements l)H3:forall x1 x2 : X.t, InA X.eq x1 (elements l) -> InA X.eq x2 (x :: elements r) -> X.lt x1 x2H0:Sorted X.lt (elements r)H4:HdRel X.lt x (elements r)y:eltHy:InT y lInA X.eq x (x :: elements r)now rewrite elements_spec1.c:Info.tl:treex:X.tr:treeIHl:Sorted X.lt (elements l) -> Ok lIHr:Sorted X.lt (elements r) -> Ok rH:Sorted X.lt (elements l ++ x :: elements r)H1:Sorted X.lt (elements l)H3:forall x1 x2 : X.t, InA X.eq x1 (elements l) -> InA X.eq x2 (x :: elements r) -> X.lt x1 x2H0:Sorted X.lt (elements r)H4:HdRel X.lt x (elements r)y:eltHy:InT y lInA X.eq y (elements l)c:Info.tl:treex:X.tr:treeIHl:Sorted X.lt (elements l) -> Ok lIHr:Sorted X.lt (elements r) -> Ok rH:Sorted X.lt (elements l ++ x :: elements r)H1:Sorted X.lt (elements l)H3:forall x1 x2 : X.t, InA X.eq x1 (elements l) -> InA X.eq x2 (x :: elements r) -> X.lt x1 x2H0:Sorted X.lt (elements r)H4:HdRel X.lt x (elements r)y:eltHy:InT y lInA X.eq x (x :: elements r)now left.c:Info.tl:treex:X.tr:treeIHl:Sorted X.lt (elements l) -> Ok lIHr:Sorted X.lt (elements r) -> Ok rH:Sorted X.lt (elements l ++ x :: elements r)H1:Sorted X.lt (elements l)H3:forall x1 x2 : X.t, InA X.eq x1 (elements l) -> InA X.eq x2 (x :: elements r) -> X.lt x1 x2H0:Sorted X.lt (elements r)H4:HdRel X.lt x (elements r)y:eltHy:InT y lX.eq x x \/ InA X.eq x (elements r)c:Info.tl:treex:X.tr:treeIHl:Sorted X.lt (elements l) -> Ok lIHr:Sorted X.lt (elements r) -> Ok rH:Sorted X.lt (elements l ++ x :: elements r)H1:Sorted X.lt (elements l)H3:forall x1 x2 : X.t, InA X.eq x1 (elements l) -> InA X.eq x2 (x :: elements r) -> X.lt x1 x2H0:Sorted X.lt (elements r)H4:HdRel X.lt x (elements r)gt_tree x rc:Info.tl:treex:X.tr:treeIHl:Sorted X.lt (elements l) -> Ok lIHr:Sorted X.lt (elements r) -> Ok rH:Sorted X.lt (elements l ++ x :: elements r)H1:Sorted X.lt (elements l)H3:forall x1 x2 : X.t, InA X.eq x1 (elements l) -> InA X.eq x2 (x :: elements r) -> X.lt x1 x2H0:Sorted X.lt (elements r)H4:HdRel X.lt x (elements r)y:eltHy:InT y rX.lt x ynow rewrite elements_spec1. Qed.c:Info.tl:treex:X.tr:treeIHl:Sorted X.lt (elements l) -> Ok lIHr:Sorted X.lt (elements r) -> Ok rH:Sorted X.lt (elements l ++ x :: elements r)H1:Sorted X.lt (elements l)H3:forall x1 x2 : X.t, InA X.eq x1 (elements l) -> InA X.eq x2 (x :: elements r) -> X.lt x1 x2H0:Sorted X.lt (elements r)H4:HdRel X.lt x (elements r)y:eltHy:InT y rInA X.eq y (elements r)
s:treef:X.t -> boolProper (X.eq ==> eq) f -> for_all f s = true <-> For_all (fun x : elt => f x = true) ss:treef:X.t -> boolProper (X.eq ==> eq) f -> for_all f s = true <-> For_all (fun x : elt => f x = true) ss:treef:X.t -> boolHf:Proper (X.eq ==> eq) ffor_all f s = true <-> (forall x : elt, InT x s -> f x = true)f:X.t -> boolHf:Proper (X.eq ==> eq) ftrue = true <-> (forall x : elt, InT x Leaf -> f x = true)i:Info.tl:treex:X.tr:treef:X.t -> boolHf:Proper (X.eq ==> eq) fIHl:for_all f l = true <-> (forall x0 : elt, InT x0 l -> f x0 = true)IHr:for_all f r = true <-> (forall x0 : elt, InT x0 r -> f x0 = true)f x &&& for_all f l &&& for_all f r = true <-> (forall x0 : elt, InT x0 (Node i l x r) -> f x0 = true)split; intros; inv; auto.f:X.t -> boolHf:Proper (X.eq ==> eq) ftrue = true <-> (forall x : elt, InT x Leaf -> f x = true)i:Info.tl:treex:X.tr:treef:X.t -> boolHf:Proper (X.eq ==> eq) fIHl:for_all f l = true <-> (forall x0 : elt, InT x0 l -> f x0 = true)IHr:for_all f r = true <-> (forall x0 : elt, InT x0 r -> f x0 = true)f x &&& for_all f l &&& for_all f r = true <-> (forall x0 : elt, InT x0 (Node i l x r) -> f x0 = true)i:Info.tl:treex:X.tr:treef:X.t -> boolHf:Proper (X.eq ==> eq) fIHl:for_all f l = true <-> (forall x0 : elt, InT x0 l -> f x0 = true)IHr:for_all f r = true <-> (forall x0 : elt, InT x0 r -> f x0 = true)(f x = true /\ (forall x0 : elt, InT x0 l -> f x0 = true)) /\ (forall x0 : elt, InT x0 r -> f x0 = true) <-> (forall x0 : elt, InT x0 (Node i l x r) -> f x0 = true)i:Info.tl:treex:X.tr:treef:X.t -> boolHf:Proper (X.eq ==> eq) f(f x = true /\ (forall x0 : elt, InT x0 l -> f x0 = true)) /\ (forall x0 : elt, InT x0 r -> f x0 = true) <-> (forall x0 : elt, InT x0 (Node i l x r) -> f x0 = true)eauto. Qed.i:Info.tl:treex:X.tr:treef:X.t -> boolHf:Proper (X.eq ==> eq) fH1:forall x1 : elt, InT x1 r -> f x1 = trueH:f x = trueH2:forall x1 : elt, InT x1 l -> f x1 = truex0:eltH4:X.eq x0 xf x0 = trues:treef:X.t -> boolProper (X.eq ==> eq) f -> exists_ f s = true <-> Exists (fun x : elt => f x = true) ss:treef:X.t -> boolProper (X.eq ==> eq) f -> exists_ f s = true <-> Exists (fun x : elt => f x = true) ss:treef:X.t -> boolHf:Proper (X.eq ==> eq) fexists_ f s = true <-> (exists x : elt, InT x s /\ f x = true)f:X.t -> boolHf:Proper (X.eq ==> eq) ffalse = true <-> (exists x : elt, InT x Leaf /\ f x = true)i:Info.tl:treex:X.tr:treef:X.t -> boolHf:Proper (X.eq ==> eq) fIHl:exists_ f l = true <-> (exists x0 : elt, InT x0 l /\ f x0 = true)IHr:exists_ f r = true <-> (exists x0 : elt, InT x0 r /\ f x0 = true)f x ||| exists_ f l ||| exists_ f r = true <-> (exists x0 : elt, InT x0 (Node i l x r) /\ f x0 = true)f:X.t -> boolHf:Proper (X.eq ==> eq) ffalse = true <-> (exists x : elt, InT x Leaf /\ f x = true)f:X.t -> boolHf:Proper (X.eq ==> eq) ffalse = true -> exists x : elt, InT x Leaf /\ f x = truef:X.t -> boolHf:Proper (X.eq ==> eq) f(exists x : elt, InT x Leaf /\ f x = true) -> false = truediscriminate.f:X.t -> boolHf:Proper (X.eq ==> eq) ffalse = true -> exists x : elt, InT x Leaf /\ f x = trueintros (y,(H,_)); inv.f:X.t -> boolHf:Proper (X.eq ==> eq) f(exists x : elt, InT x Leaf /\ f x = true) -> false = truei:Info.tl:treex:X.tr:treef:X.t -> boolHf:Proper (X.eq ==> eq) fIHl:exists_ f l = true <-> (exists x0 : elt, InT x0 l /\ f x0 = true)IHr:exists_ f r = true <-> (exists x0 : elt, InT x0 r /\ f x0 = true)f x ||| exists_ f l ||| exists_ f r = true <-> (exists x0 : elt, InT x0 (Node i l x r) /\ f x0 = true)i:Info.tl:treex:X.tr:treef:X.t -> boolHf:Proper (X.eq ==> eq) fIHl:exists_ f l = true <-> (exists x0 : elt, InT x0 l /\ f x0 = true)IHr:exists_ f r = true <-> (exists x0 : elt, InT x0 r /\ f x0 = true)(f x = true \/ (exists x0 : elt, InT x0 l /\ f x0 = true)) \/ (exists x0 : elt, InT x0 r /\ f x0 = true) <-> (exists x0 : elt, InT x0 (Node i l x r) /\ f x0 = true)i:Info.tl:treex:X.tr:treef:X.t -> boolHf:Proper (X.eq ==> eq) f(f x = true \/ (exists x0 : elt, InT x0 l /\ f x0 = true)) \/ (exists x0 : elt, InT x0 r /\ f x0 = true) <-> (exists x0 : elt, InT x0 (Node i l x r) /\ f x0 = true)i:Info.tl:treex:X.tr:treef:X.t -> boolHf:Proper (X.eq ==> eq) fH:f x = trueexists x0 : elt, InT x0 (Node i l x r) /\ f x0 = truei:Info.tl:treex:X.tr:treef:X.t -> boolHf:Proper (X.eq ==> eq) fy:eltH:InT y lH':f y = trueexists x0 : elt, InT x0 (Node i l x r) /\ f x0 = truei:Info.tl:treex:X.tr:treef:X.t -> boolHf:Proper (X.eq ==> eq) fy:eltH:InT y rH':f y = trueexists x0 : elt, InT x0 (Node i l x r) /\ f x0 = truei:Info.tl:treex:X.tr:treef:X.t -> boolHf:Proper (X.eq ==> eq) fy:eltH:InT y (Node i l x r)H':f y = true(f x = true \/ (exists x0 : elt, InT x0 l /\ f x0 = true)) \/ (exists x0 : elt, InT x0 r /\ f x0 = true)exists x; auto.i:Info.tl:treex:X.tr:treef:X.t -> boolHf:Proper (X.eq ==> eq) fH:f x = trueexists x0 : elt, InT x0 (Node i l x r) /\ f x0 = trueexists y; auto.i:Info.tl:treex:X.tr:treef:X.t -> boolHf:Proper (X.eq ==> eq) fy:eltH:InT y lH':f y = trueexists x0 : elt, InT x0 (Node i l x r) /\ f x0 = trueexists y; auto.i:Info.tl:treex:X.tr:treef:X.t -> boolHf:Proper (X.eq ==> eq) fy:eltH:InT y rH':f y = trueexists x0 : elt, InT x0 (Node i l x r) /\ f x0 = trueinv; [left;left|left;right|right]; try (exists y); eauto. Qed.i:Info.tl:treex:X.tr:treef:X.t -> boolHf:Proper (X.eq ==> eq) fy:eltH:InT y (Node i l x r)H':f y = true(f x = true \/ (exists x0 : elt, InT x0 l /\ f x0 = true)) \/ (exists x0 : elt, InT x0 r /\ f x0 = true)
A:Typef:elt -> A -> As:treei:Aacc:list eltfold_left (flip f) (elements_aux acc s) i = fold_left (flip f) acc (fold f s i)A:Typef:elt -> A -> As:treei:Aacc:list eltfold_left (flip f) (elements_aux acc s) i = fold_left (flip f) acc (fold f s i)A:Typef:elt -> A -> As:treeforall (i : A) (acc : list elt), fold_left (flip f) (elements_aux acc s) i = fold_left (flip f) acc (fold f s i)A:Typef:elt -> A -> Ac:Info.tl:treex:X.tr:treeIHl:forall (i0 : A) (acc0 : list elt), fold_left (flip f) (elements_aux acc0 l) i0 = fold_left (flip f) acc0 (fold f l i0)IHr:forall (i0 : A) (acc0 : list elt), fold_left (flip f) (elements_aux acc0 r) i0 = fold_left (flip f) acc0 (fold f r i0)i:Aacc:list eltfold_left (flip f) (elements_aux (x :: elements_aux acc r) l) i = fold_left (flip f) acc (fold f r (f x (fold f l i)))A:Typef:elt -> A -> Ac:Info.tl:treex:X.tr:treeIHl:forall (i0 : A) (acc0 : list elt), fold_left (flip f) (elements_aux acc0 l) i0 = fold_left (flip f) acc0 (fold f l i0)IHr:forall (i0 : A) (acc0 : list elt), fold_left (flip f) (elements_aux acc0 r) i0 = fold_left (flip f) acc0 (fold f r i0)i:Aacc:list eltfold_left (flip f) (x :: elements_aux acc r) (fold f l i) = fold_left (flip f) acc (fold f r (f x (fold f l i)))A:Typef:elt -> A -> Ac:Info.tl:treex:X.tr:treeIHl:forall (i0 : A) (acc0 : list elt), fold_left (flip f) (elements_aux acc0 l) i0 = fold_left (flip f) acc0 (fold f l i0)IHr:forall (i0 : A) (acc0 : list elt), fold_left (flip f) (elements_aux acc0 r) i0 = fold_left (flip f) acc0 (fold f r i0)i:Aacc:list eltfold_left (flip f) (elements_aux acc r) (flip f (fold f l i) x) = fold_left (flip f) acc (fold f r (f x (fold f l i)))apply IHr. Qed.A:Typef:elt -> A -> Ac:Info.tl:treex:X.tr:treeIHl:forall (i0 : A) (acc0 : list elt), fold_left (flip f) (elements_aux acc0 l) i0 = fold_left (flip f) acc0 (fold f l i0)IHr:forall (i0 : A) (acc0 : list elt), fold_left (flip f) (elements_aux acc0 r) i0 = fold_left (flip f) acc0 (fold f r i0)i:Aacc:list eltfold_left (flip f) (elements_aux acc r) (f x (fold f l i)) = fold_left (flip f) acc (fold f r (f x (fold f l i)))s:treeA:Typei:Af:elt -> A -> Afold f s i = fold_left (flip f) (elements s) is:treeA:Typei:Af:elt -> A -> Afold f s i = fold_left (flip f) (elements s) is:treeA:Typef:elt -> A -> Aforall i : A, fold f s i = fold_left (flip f) (elements s) is:treeA:Typef:elt -> A -> Aforall i : A, fold f s i = fold_left (flip f) (elements_aux nil s) ic:Info.tl:treex:X.tr:treeA:Typef:elt -> A -> AIHl:forall i0 : A, fold f l i0 = fold_left (flip f) (elements_aux nil l) i0IHr:forall i0 : A, fold f r i0 = fold_left (flip f) (elements_aux nil r) i0i:Afold f r (f x (fold f l i)) = fold_left (flip f) (elements_aux (x :: elements_aux nil r) l) ic:Info.tl:treex:X.tr:treeA:Typef:elt -> A -> AIHl:forall i0 : A, fold f l i0 = fold_left (flip f) (elements_aux nil l) i0IHr:forall i0 : A, fold f r i0 = fold_left (flip f) (elements_aux nil r) i0i:Afold f r (f x (fold f l i)) = fold_left (flip f) (x :: elements_aux nil r) (fold f l i)simpl; auto. Qed.c:Info.tl:treex:X.tr:treeA:Typef:elt -> A -> AIHl:forall i0 : A, fold f l i0 = fold_left (flip f) (elements_aux nil l) i0IHr:forall i0 : A, fold f r i0 = fold_left (flip f) (elements_aux nil r) i0i:Afold_left (flip f) (elements_aux nil r) (f x (fold f l i)) = fold_left (flip f) (x :: elements_aux nil r) (fold f l i)
forall (subset_l1 : tree -> bool) (l1 : tree) (x1 : X.t) (c1 : Info.t) (s2 : tree), Ok (Node c1 l1 x1 Leaf) -> Ok s2 -> (forall s : tree, Ok s -> subset_l1 s = true <-> Subset l1 s) -> subsetl subset_l1 x1 s2 = true <-> Subset (Node c1 l1 x1 Leaf) s2forall (subset_l1 : tree -> bool) (l1 : tree) (x1 : X.t) (c1 : Info.t) (s2 : tree), Ok (Node c1 l1 x1 Leaf) -> Ok s2 -> (forall s : tree, Ok s -> subset_l1 s = true <-> Subset l1 s) -> subsetl subset_l1 x1 s2 = true <-> Subset (Node c1 l1 x1 Leaf) s2subset_l1:tree -> booll1:treex1:X.tc1:Info.tH:Ok (Node c1 l1 x1 Leaf)H0:Ok LeafH1:forall s : tree, Ok s -> subset_l1 s = true <-> Subset l1 sfalse = true <-> Subset (Node c1 l1 x1 Leaf) Leafsubset_l1:tree -> booll1:treex1:X.tc1, c2:Info.tl2:treex2:X.tr2:treeIHl2:Ok (Node c1 l1 x1 Leaf) -> Ok l2 -> (forall s : tree, Ok s -> subset_l1 s = true <-> Subset l1 s) -> subsetl subset_l1 x1 l2 = true <-> Subset (Node c1 l1 x1 Leaf) l2IHr2:Ok (Node c1 l1 x1 Leaf) -> Ok r2 -> (forall s : tree, Ok s -> subset_l1 s = true <-> Subset l1 s) -> subsetl subset_l1 x1 r2 = true <-> Subset (Node c1 l1 x1 Leaf) r2H:Ok (Node c1 l1 x1 Leaf)H0:Ok (Node c2 l2 x2 r2)H1:forall s : tree, Ok s -> subset_l1 s = true <-> Subset l1 smatch X.compare x1 x2 with | Eq => subset_l1 l2 | Lt => subsetl subset_l1 x1 l2 | Gt => mem x1 r2 &&& subset_l1 (Node c2 l2 x2 r2) end = true <-> Subset (Node c1 l1 x1 Leaf) (Node c2 l2 x2 r2)subset_l1:tree -> booll1:treex1:X.tc1:Info.tH:Ok (Node c1 l1 x1 Leaf)H0:Ok LeafH1:forall s : tree, Ok s -> subset_l1 s = true <-> Subset l1 sH2:forall a : elt, InT a (Node c1 l1 x1 Leaf) -> InT a Leaffalse = truesubset_l1:tree -> booll1:treex1:X.tc1, c2:Info.tl2:treex2:X.tr2:treeIHl2:Ok (Node c1 l1 x1 Leaf) -> Ok l2 -> (forall s : tree, Ok s -> subset_l1 s = true <-> Subset l1 s) -> subsetl subset_l1 x1 l2 = true <-> Subset (Node c1 l1 x1 Leaf) l2IHr2:Ok (Node c1 l1 x1 Leaf) -> Ok r2 -> (forall s : tree, Ok s -> subset_l1 s = true <-> Subset l1 s) -> subsetl subset_l1 x1 r2 = true <-> Subset (Node c1 l1 x1 Leaf) r2H:Ok (Node c1 l1 x1 Leaf)H0:Ok (Node c2 l2 x2 r2)H1:forall s : tree, Ok s -> subset_l1 s = true <-> Subset l1 smatch X.compare x1 x2 with | Eq => subset_l1 l2 | Lt => subsetl subset_l1 x1 l2 | Gt => mem x1 r2 &&& subset_l1 (Node c2 l2 x2 r2) end = true <-> Subset (Node c1 l1 x1 Leaf) (Node c2 l2 x2 r2)subset_l1:tree -> booll1:treex1:X.tc1, c2:Info.tl2:treex2:X.tr2:treeIHl2:Ok (Node c1 l1 x1 Leaf) -> Ok l2 -> (forall s : tree, Ok s -> subset_l1 s = true <-> Subset l1 s) -> subsetl subset_l1 x1 l2 = true <-> Subset (Node c1 l1 x1 Leaf) l2IHr2:Ok (Node c1 l1 x1 Leaf) -> Ok r2 -> (forall s : tree, Ok s -> subset_l1 s = true <-> Subset l1 s) -> subsetl subset_l1 x1 r2 = true <-> Subset (Node c1 l1 x1 Leaf) r2H:Ok (Node c1 l1 x1 Leaf)H0:Ok (Node c2 l2 x2 r2)H1:forall s : tree, Ok s -> subset_l1 s = true <-> Subset l1 smatch X.compare x1 x2 with | Eq => subset_l1 l2 | Lt => subsetl subset_l1 x1 l2 | Gt => mem x1 r2 &&& subset_l1 (Node c2 l2 x2 r2) end = true <-> Subset (Node c1 l1 x1 Leaf) (Node c2 l2 x2 r2)subset_l1:tree -> booll1:treex1:X.tc1, c2:Info.tl2:treex2:X.tr2:treeIHl2:Ok l2 -> (forall s : tree, Ok s -> subset_l1 s = true <-> Subset l1 s) -> subsetl subset_l1 x1 l2 = true <-> Subset (Node c1 l1 x1 Leaf) l2IHr2:Ok (Node c1 l1 x1 Leaf) -> Ok r2 -> (forall s : tree, Ok s -> subset_l1 s = true <-> Subset l1 s) -> subsetl subset_l1 x1 r2 = true <-> Subset (Node c1 l1 x1 Leaf) r2H:Ok (Node c1 l1 x1 Leaf)H0:Ok (Node c2 l2 x2 r2)H1:forall s : tree, Ok s -> subset_l1 s = true <-> Subset l1 smatch X.compare x1 x2 with | Eq => subset_l1 l2 | Lt => subsetl subset_l1 x1 l2 | Gt => mem x1 r2 &&& subset_l1 (Node c2 l2 x2 r2) end = true <-> Subset (Node c1 l1 x1 Leaf) (Node c2 l2 x2 r2)subset_l1:tree -> booll1:treex1:X.tc1, c2:Info.tl2:treex2:X.tr2:treeIHl2:Ok l2 -> (forall s : tree, Ok s -> subset_l1 s = true <-> Subset l1 s) -> subsetl subset_l1 x1 l2 = true <-> Subset (Node c1 l1 x1 Leaf) l2IHr2:Ok r2 -> (forall s : tree, Ok s -> subset_l1 s = true <-> Subset l1 s) -> subsetl subset_l1 x1 r2 = true <-> Subset (Node c1 l1 x1 Leaf) r2H:Ok (Node c1 l1 x1 Leaf)H0:Ok (Node c2 l2 x2 r2)H1:forall s : tree, Ok s -> subset_l1 s = true <-> Subset l1 smatch X.compare x1 x2 with | Eq => subset_l1 l2 | Lt => subsetl subset_l1 x1 l2 | Gt => mem x1 r2 &&& subset_l1 (Node c2 l2 x2 r2) end = true <-> Subset (Node c1 l1 x1 Leaf) (Node c2 l2 x2 r2)subset_l1:tree -> booll1:treex1:X.tc1, c2:Info.tl2:treex2:X.tr2:treeIHl2:Ok l2 -> (forall s : tree, Ok s -> subset_l1 s = true <-> Subset l1 s) -> subsetl subset_l1 x1 l2 = true <-> Subset (Node c1 l1 x1 Leaf) l2IHr2:Ok r2 -> (forall s : tree, Ok s -> subset_l1 s = true <-> Subset l1 s) -> subsetl subset_l1 x1 r2 = true <-> Subset (Node c1 l1 x1 Leaf) r2H1:forall s : tree, Ok s -> subset_l1 s = true <-> Subset l1 sH6:Ok l2H7:Ok r2H8:lt_tree x2 l2H9:gt_tree x2 r2H5:Ok l1H11:lt_tree x1 l1H12:gt_tree x1 Leafmatch X.compare x1 x2 with | Eq => subset_l1 l2 | Lt => subsetl subset_l1 x1 l2 | Gt => mem x1 r2 &&& subset_l1 (Node c2 l2 x2 r2) end = true <-> Subset (Node c1 l1 x1 Leaf) (Node c2 l2 x2 r2)subset_l1:tree -> booll1:treex1:X.tc1, c2:Info.tl2:treex2:X.tr2:treeIHl2:Ok l2 -> (forall s : tree, Ok s -> subset_l1 s = true <-> Subset l1 s) -> subsetl subset_l1 x1 l2 = true <-> Subset (Node c1 l1 x1 Leaf) l2IHr2:Ok r2 -> (forall s : tree, Ok s -> subset_l1 s = true <-> Subset l1 s) -> subsetl subset_l1 x1 r2 = true <-> Subset (Node c1 l1 x1 Leaf) r2H1:forall s : tree, Ok s -> subset_l1 s = true <-> Subset l1 sH6:Ok l2H7:Ok r2H8:lt_tree x2 l2H9:gt_tree x2 r2H5:Ok l1H11:lt_tree x1 l1H12:gt_tree x1 LeafH:X.eq x1 x2subset_l1 l2 = true <-> Subset (Node c1 l1 x1 Leaf) (Node c2 l2 x2 r2)subset_l1:tree -> booll1:treex1:X.tc1, c2:Info.tl2:treex2:X.tr2:treeIHl2:Ok l2 -> (forall s : tree, Ok s -> subset_l1 s = true <-> Subset l1 s) -> subsetl subset_l1 x1 l2 = true <-> Subset (Node c1 l1 x1 Leaf) l2IHr2:Ok r2 -> (forall s : tree, Ok s -> subset_l1 s = true <-> Subset l1 s) -> subsetl subset_l1 x1 r2 = true <-> Subset (Node c1 l1 x1 Leaf) r2H1:forall s : tree, Ok s -> subset_l1 s = true <-> Subset l1 sH6:Ok l2H7:Ok r2H8:lt_tree x2 l2H9:gt_tree x2 r2H5:Ok l1H11:lt_tree x1 l1H12:gt_tree x1 LeafH:X.lt x1 x2subsetl subset_l1 x1 l2 = true <-> Subset (Node c1 l1 x1 Leaf) (Node c2 l2 x2 r2)subset_l1:tree -> booll1:treex1:X.tc1, c2:Info.tl2:treex2:X.tr2:treeIHl2:Ok l2 -> (forall s : tree, Ok s -> subset_l1 s = true <-> Subset l1 s) -> subsetl subset_l1 x1 l2 = true <-> Subset (Node c1 l1 x1 Leaf) l2IHr2:Ok r2 -> (forall s : tree, Ok s -> subset_l1 s = true <-> Subset l1 s) -> subsetl subset_l1 x1 r2 = true <-> Subset (Node c1 l1 x1 Leaf) r2H1:forall s : tree, Ok s -> subset_l1 s = true <-> Subset l1 sH6:Ok l2H7:Ok r2H8:lt_tree x2 l2H9:gt_tree x2 r2H5:Ok l1H11:lt_tree x1 l1H12:gt_tree x1 LeafH:X.lt x2 x1mem x1 r2 &&& subset_l1 (Node c2 l2 x2 r2) = true <-> Subset (Node c1 l1 x1 Leaf) (Node c2 l2 x2 r2)subset_l1:tree -> booll1:treex1:X.tc1, c2:Info.tl2:treex2:X.tr2:treeH6:Ok l2H7:Ok r2H8:lt_tree x2 l2H9:gt_tree x2 r2H5:Ok l1H11:lt_tree x1 l1H12:gt_tree x1 LeafH:X.eq x1 x2Subset l1 l2 <-> Subset (Node c1 l1 x1 Leaf) (Node c2 l2 x2 r2)subset_l1:tree -> booll1:treex1:X.tc1, c2:Info.tl2:treex2:X.tr2:treeIHl2:Ok l2 -> (forall s : tree, Ok s -> subset_l1 s = true <-> Subset l1 s) -> subsetl subset_l1 x1 l2 = true <-> Subset (Node c1 l1 x1 Leaf) l2IHr2:Ok r2 -> (forall s : tree, Ok s -> subset_l1 s = true <-> Subset l1 s) -> subsetl subset_l1 x1 r2 = true <-> Subset (Node c1 l1 x1 Leaf) r2H1:forall s : tree, Ok s -> subset_l1 s = true <-> Subset l1 sH6:Ok l2H7:Ok r2H8:lt_tree x2 l2H9:gt_tree x2 r2H5:Ok l1H11:lt_tree x1 l1H12:gt_tree x1 LeafH:X.lt x1 x2subsetl subset_l1 x1 l2 = true <-> Subset (Node c1 l1 x1 Leaf) (Node c2 l2 x2 r2)subset_l1:tree -> booll1:treex1:X.tc1, c2:Info.tl2:treex2:X.tr2:treeIHl2:Ok l2 -> (forall s : tree, Ok s -> subset_l1 s = true <-> Subset l1 s) -> subsetl subset_l1 x1 l2 = true <-> Subset (Node c1 l1 x1 Leaf) l2IHr2:Ok r2 -> (forall s : tree, Ok s -> subset_l1 s = true <-> Subset l1 s) -> subsetl subset_l1 x1 r2 = true <-> Subset (Node c1 l1 x1 Leaf) r2H1:forall s : tree, Ok s -> subset_l1 s = true <-> Subset l1 sH6:Ok l2H7:Ok r2H8:lt_tree x2 l2H9:gt_tree x2 r2H5:Ok l1H11:lt_tree x1 l1H12:gt_tree x1 LeafH:X.lt x2 x1mem x1 r2 &&& subset_l1 (Node c2 l2 x2 r2) = true <-> Subset (Node c1 l1 x1 Leaf) (Node c2 l2 x2 r2)subset_l1:tree -> booll1:treex1:X.tc1, c2:Info.tl2:treex2:X.tr2:treeH6:Ok l2H7:Ok r2H8:lt_tree x2 l2H9:gt_tree x2 r2H5:Ok l1H11:lt_tree x1 l1H12:gt_tree x1 LeafH:X.eq x1 x2(forall a : elt, InT a l1 -> InT a l2) <-> (forall a : elt, InT a (Node c1 l1 x1 Leaf) -> InT a (Node c2 l2 x2 r2))subset_l1:tree -> booll1:treex1:X.tc1, c2:Info.tl2:treex2:X.tr2:treeIHl2:Ok l2 -> (forall s : tree, Ok s -> subset_l1 s = true <-> Subset l1 s) -> subsetl subset_l1 x1 l2 = true <-> Subset (Node c1 l1 x1 Leaf) l2IHr2:Ok r2 -> (forall s : tree, Ok s -> subset_l1 s = true <-> Subset l1 s) -> subsetl subset_l1 x1 r2 = true <-> Subset (Node c1 l1 x1 Leaf) r2H1:forall s : tree, Ok s -> subset_l1 s = true <-> Subset l1 sH6:Ok l2H7:Ok r2H8:lt_tree x2 l2H9:gt_tree x2 r2H5:Ok l1H11:lt_tree x1 l1H12:gt_tree x1 LeafH:X.lt x1 x2subsetl subset_l1 x1 l2 = true <-> Subset (Node c1 l1 x1 Leaf) (Node c2 l2 x2 r2)subset_l1:tree -> booll1:treex1:X.tc1, c2:Info.tl2:treex2:X.tr2:treeIHl2:Ok l2 -> (forall s : tree, Ok s -> subset_l1 s = true <-> Subset l1 s) -> subsetl subset_l1 x1 l2 = true <-> Subset (Node c1 l1 x1 Leaf) l2IHr2:Ok r2 -> (forall s : tree, Ok s -> subset_l1 s = true <-> Subset l1 s) -> subsetl subset_l1 x1 r2 = true <-> Subset (Node c1 l1 x1 Leaf) r2H1:forall s : tree, Ok s -> subset_l1 s = true <-> Subset l1 sH6:Ok l2H7:Ok r2H8:lt_tree x2 l2H9:gt_tree x2 r2H5:Ok l1H11:lt_tree x1 l1H12:gt_tree x1 LeafH:X.lt x2 x1mem x1 r2 &&& subset_l1 (Node c2 l2 x2 r2) = true <-> Subset (Node c1 l1 x1 Leaf) (Node c2 l2 x2 r2)l1:treex1:X.tc1, c2:Info.tl2:treex2:X.tr2:treeH6:Ok l2H7:Ok r2H8:lt_tree x2 l2H9:gt_tree x2 r2H5:Ok l1H11:lt_tree x1 l1H12:gt_tree x1 LeafH:X.eq x1 x2H0:boolH1:forall a0 : elt, InT a0 l1 -> InT a0 l2a:eltH4:X.eq a x1InT a (Node c2 l2 x2 r2)l1:treex1:X.tc1, c2:Info.tl2:treex2:X.tr2:treeH6:Ok l2H7:Ok r2H8:lt_tree x2 l2H9:gt_tree x2 r2H5:Ok l1H11:lt_tree x1 l1H12:gt_tree x1 LeafH:X.eq x1 x2H0:boolH1:forall a0 : elt, InT a0 (Node c1 l1 x1 Leaf) -> InT a0 (Node c2 l2 x2 r2)a:eltH2:InT a l1InT a l2subset_l1:tree -> booll1:treex1:X.tc1, c2:Info.tl2:treex2:X.tr2:treeIHl2:Ok l2 -> (forall s : tree, Ok s -> subset_l1 s = true <-> Subset l1 s) -> subsetl subset_l1 x1 l2 = true <-> Subset (Node c1 l1 x1 Leaf) l2IHr2:Ok r2 -> (forall s : tree, Ok s -> subset_l1 s = true <-> Subset l1 s) -> subsetl subset_l1 x1 r2 = true <-> Subset (Node c1 l1 x1 Leaf) r2H1:forall s : tree, Ok s -> subset_l1 s = true <-> Subset l1 sH6:Ok l2H7:Ok r2H8:lt_tree x2 l2H9:gt_tree x2 r2H5:Ok l1H11:lt_tree x1 l1H12:gt_tree x1 LeafH:X.lt x1 x2subsetl subset_l1 x1 l2 = true <-> Subset (Node c1 l1 x1 Leaf) (Node c2 l2 x2 r2)subset_l1:tree -> booll1:treex1:X.tc1, c2:Info.tl2:treex2:X.tr2:treeIHl2:Ok l2 -> (forall s : tree, Ok s -> subset_l1 s = true <-> Subset l1 s) -> subsetl subset_l1 x1 l2 = true <-> Subset (Node c1 l1 x1 Leaf) l2IHr2:Ok r2 -> (forall s : tree, Ok s -> subset_l1 s = true <-> Subset l1 s) -> subsetl subset_l1 x1 r2 = true <-> Subset (Node c1 l1 x1 Leaf) r2H1:forall s : tree, Ok s -> subset_l1 s = true <-> Subset l1 sH6:Ok l2H7:Ok r2H8:lt_tree x2 l2H9:gt_tree x2 r2H5:Ok l1H11:lt_tree x1 l1H12:gt_tree x1 LeafH:X.lt x2 x1mem x1 r2 &&& subset_l1 (Node c2 l2 x2 r2) = true <-> Subset (Node c1 l1 x1 Leaf) (Node c2 l2 x2 r2)l1:treex1:X.tc1, c2:Info.tl2:treex2:X.tr2:treeH6:Ok l2H7:Ok r2H8:lt_tree x2 l2H9:gt_tree x2 r2H5:Ok l1H11:lt_tree x1 l1H12:gt_tree x1 LeafH:X.eq x1 x2H0:boolH1:forall a0 : elt, InT a0 (Node c1 l1 x1 Leaf) -> InT a0 (Node c2 l2 x2 r2)a:eltH2:InT a l1InT a l2subset_l1:tree -> booll1:treex1:X.tc1, c2:Info.tl2:treex2:X.tr2:treeIHl2:Ok l2 -> (forall s : tree, Ok s -> subset_l1 s = true <-> Subset l1 s) -> subsetl subset_l1 x1 l2 = true <-> Subset (Node c1 l1 x1 Leaf) l2IHr2:Ok r2 -> (forall s : tree, Ok s -> subset_l1 s = true <-> Subset l1 s) -> subsetl subset_l1 x1 r2 = true <-> Subset (Node c1 l1 x1 Leaf) r2H1:forall s : tree, Ok s -> subset_l1 s = true <-> Subset l1 sH6:Ok l2H7:Ok r2H8:lt_tree x2 l2H9:gt_tree x2 r2H5:Ok l1H11:lt_tree x1 l1H12:gt_tree x1 LeafH:X.lt x1 x2subsetl subset_l1 x1 l2 = true <-> Subset (Node c1 l1 x1 Leaf) (Node c2 l2 x2 r2)subset_l1:tree -> booll1:treex1:X.tc1, c2:Info.tl2:treex2:X.tr2:treeIHl2:Ok l2 -> (forall s : tree, Ok s -> subset_l1 s = true <-> Subset l1 s) -> subsetl subset_l1 x1 l2 = true <-> Subset (Node c1 l1 x1 Leaf) l2IHr2:Ok r2 -> (forall s : tree, Ok s -> subset_l1 s = true <-> Subset l1 s) -> subsetl subset_l1 x1 r2 = true <-> Subset (Node c1 l1 x1 Leaf) r2H1:forall s : tree, Ok s -> subset_l1 s = true <-> Subset l1 sH6:Ok l2H7:Ok r2H8:lt_tree x2 l2H9:gt_tree x2 r2H5:Ok l1H11:lt_tree x1 l1H12:gt_tree x1 LeafH:X.lt x2 x1mem x1 r2 &&& subset_l1 (Node c2 l2 x2 r2) = true <-> Subset (Node c1 l1 x1 Leaf) (Node c2 l2 x2 r2)subset_l1:tree -> booll1:treex1:X.tc1, c2:Info.tl2:treex2:X.tr2:treeIHl2:Ok l2 -> (forall s : tree, Ok s -> subset_l1 s = true <-> Subset l1 s) -> subsetl subset_l1 x1 l2 = true <-> Subset (Node c1 l1 x1 Leaf) l2IHr2:Ok r2 -> (forall s : tree, Ok s -> subset_l1 s = true <-> Subset l1 s) -> subsetl subset_l1 x1 r2 = true <-> Subset (Node c1 l1 x1 Leaf) r2H1:forall s : tree, Ok s -> subset_l1 s = true <-> Subset l1 sH6:Ok l2H7:Ok r2H8:lt_tree x2 l2H9:gt_tree x2 r2H5:Ok l1H11:lt_tree x1 l1H12:gt_tree x1 LeafH:X.lt x1 x2subsetl subset_l1 x1 l2 = true <-> Subset (Node c1 l1 x1 Leaf) (Node c2 l2 x2 r2)subset_l1:tree -> booll1:treex1:X.tc1, c2:Info.tl2:treex2:X.tr2:treeIHl2:Ok l2 -> (forall s : tree, Ok s -> subset_l1 s = true <-> Subset l1 s) -> subsetl subset_l1 x1 l2 = true <-> Subset (Node c1 l1 x1 Leaf) l2IHr2:Ok r2 -> (forall s : tree, Ok s -> subset_l1 s = true <-> Subset l1 s) -> subsetl subset_l1 x1 r2 = true <-> Subset (Node c1 l1 x1 Leaf) r2H1:forall s : tree, Ok s -> subset_l1 s = true <-> Subset l1 sH6:Ok l2H7:Ok r2H8:lt_tree x2 l2H9:gt_tree x2 r2H5:Ok l1H11:lt_tree x1 l1H12:gt_tree x1 LeafH:X.lt x2 x1mem x1 r2 &&& subset_l1 (Node c2 l2 x2 r2) = true <-> Subset (Node c1 l1 x1 Leaf) (Node c2 l2 x2 r2)subset_l1:tree -> booll1:treex1:X.tc1, c2:Info.tl2:treex2:X.tr2:treeH6:Ok l2H7:Ok r2H8:lt_tree x2 l2H9:gt_tree x2 r2H5:Ok l1H11:lt_tree x1 l1H12:gt_tree x1 LeafH:X.lt x1 x2Subset (Node c1 l1 x1 Leaf) l2 <-> Subset (Node c1 l1 x1 Leaf) (Node c2 l2 x2 r2)subset_l1:tree -> booll1:treex1:X.tc1, c2:Info.tl2:treex2:X.tr2:treeIHl2:Ok l2 -> (forall s : tree, Ok s -> subset_l1 s = true <-> Subset l1 s) -> subsetl subset_l1 x1 l2 = true <-> Subset (Node c1 l1 x1 Leaf) l2IHr2:Ok r2 -> (forall s : tree, Ok s -> subset_l1 s = true <-> Subset l1 s) -> subsetl subset_l1 x1 r2 = true <-> Subset (Node c1 l1 x1 Leaf) r2H1:forall s : tree, Ok s -> subset_l1 s = true <-> Subset l1 sH6:Ok l2H7:Ok r2H8:lt_tree x2 l2H9:gt_tree x2 r2H5:Ok l1H11:lt_tree x1 l1H12:gt_tree x1 LeafH:X.lt x2 x1mem x1 r2 &&& subset_l1 (Node c2 l2 x2 r2) = true <-> Subset (Node c1 l1 x1 Leaf) (Node c2 l2 x2 r2)subset_l1:tree -> booll1:treex1:X.tc1, c2:Info.tl2:treex2:X.tr2:treeH6:Ok l2H7:Ok r2H8:lt_tree x2 l2H9:gt_tree x2 r2H5:Ok l1H11:lt_tree x1 l1H12:gt_tree x1 LeafH:X.lt x1 x2(forall a : elt, InT a (Node c1 l1 x1 Leaf) -> InT a l2) <-> (forall a : elt, InT a (Node c1 l1 x1 Leaf) -> InT a (Node c2 l2 x2 r2))subset_l1:tree -> booll1:treex1:X.tc1, c2:Info.tl2:treex2:X.tr2:treeIHl2:Ok l2 -> (forall s : tree, Ok s -> subset_l1 s = true <-> Subset l1 s) -> subsetl subset_l1 x1 l2 = true <-> Subset (Node c1 l1 x1 Leaf) l2IHr2:Ok r2 -> (forall s : tree, Ok s -> subset_l1 s = true <-> Subset l1 s) -> subsetl subset_l1 x1 r2 = true <-> Subset (Node c1 l1 x1 Leaf) r2H1:forall s : tree, Ok s -> subset_l1 s = true <-> Subset l1 sH6:Ok l2H7:Ok r2H8:lt_tree x2 l2H9:gt_tree x2 r2H5:Ok l1H11:lt_tree x1 l1H12:gt_tree x1 LeafH:X.lt x2 x1mem x1 r2 &&& subset_l1 (Node c2 l2 x2 r2) = true <-> Subset (Node c1 l1 x1 Leaf) (Node c2 l2 x2 r2)l1:treex1:X.tc1, c2:Info.tl2:treex2:X.tr2:treeH6:Ok l2H7:Ok r2H8:lt_tree x2 l2H9:gt_tree x2 r2H5:Ok l1H11:lt_tree x1 l1H12:gt_tree x1 LeafH:X.lt x1 x2H0:boolH1:forall a0 : elt, InT a0 (Node c1 l1 x1 Leaf) -> InT a0 (Node c2 l2 x2 r2)a:eltH4:X.eq a x1InT a l2l1:treex1:X.tc1, c2:Info.tl2:treex2:X.tr2:treeH6:Ok l2H7:Ok r2H8:lt_tree x2 l2H9:gt_tree x2 r2H5:Ok l1H11:lt_tree x1 l1H12:gt_tree x1 LeafH:X.lt x1 x2H0:boolH1:forall a0 : elt, InT a0 (Node c1 l1 x1 Leaf) -> InT a0 (Node c2 l2 x2 r2)a:eltH4:InT a l1InT a l2subset_l1:tree -> booll1:treex1:X.tc1, c2:Info.tl2:treex2:X.tr2:treeIHl2:Ok l2 -> (forall s : tree, Ok s -> subset_l1 s = true <-> Subset l1 s) -> subsetl subset_l1 x1 l2 = true <-> Subset (Node c1 l1 x1 Leaf) l2IHr2:Ok r2 -> (forall s : tree, Ok s -> subset_l1 s = true <-> Subset l1 s) -> subsetl subset_l1 x1 r2 = true <-> Subset (Node c1 l1 x1 Leaf) r2H1:forall s : tree, Ok s -> subset_l1 s = true <-> Subset l1 sH6:Ok l2H7:Ok r2H8:lt_tree x2 l2H9:gt_tree x2 r2H5:Ok l1H11:lt_tree x1 l1H12:gt_tree x1 LeafH:X.lt x2 x1mem x1 r2 &&& subset_l1 (Node c2 l2 x2 r2) = true <-> Subset (Node c1 l1 x1 Leaf) (Node c2 l2 x2 r2)l1:treex1:X.tc1, c2:Info.tl2:treex2:X.tr2:treeH6:Ok l2H7:Ok r2H8:lt_tree x2 l2H9:gt_tree x2 r2H5:Ok l1H11:lt_tree x1 l1H12:gt_tree x1 LeafH:X.lt x1 x2H0:boolH1:forall a0 : elt, InT a0 (Node c1 l1 x1 Leaf) -> InT a0 (Node c2 l2 x2 r2)a:eltH4:InT a l1InT a l2subset_l1:tree -> booll1:treex1:X.tc1, c2:Info.tl2:treex2:X.tr2:treeIHl2:Ok l2 -> (forall s : tree, Ok s -> subset_l1 s = true <-> Subset l1 s) -> subsetl subset_l1 x1 l2 = true <-> Subset (Node c1 l1 x1 Leaf) l2IHr2:Ok r2 -> (forall s : tree, Ok s -> subset_l1 s = true <-> Subset l1 s) -> subsetl subset_l1 x1 r2 = true <-> Subset (Node c1 l1 x1 Leaf) r2H1:forall s : tree, Ok s -> subset_l1 s = true <-> Subset l1 sH6:Ok l2H7:Ok r2H8:lt_tree x2 l2H9:gt_tree x2 r2H5:Ok l1H11:lt_tree x1 l1H12:gt_tree x1 LeafH:X.lt x2 x1mem x1 r2 &&& subset_l1 (Node c2 l2 x2 r2) = true <-> Subset (Node c1 l1 x1 Leaf) (Node c2 l2 x2 r2)subset_l1:tree -> booll1:treex1:X.tc1, c2:Info.tl2:treex2:X.tr2:treeIHl2:Ok l2 -> (forall s : tree, Ok s -> subset_l1 s = true <-> Subset l1 s) -> subsetl subset_l1 x1 l2 = true <-> Subset (Node c1 l1 x1 Leaf) l2IHr2:Ok r2 -> (forall s : tree, Ok s -> subset_l1 s = true <-> Subset l1 s) -> subsetl subset_l1 x1 r2 = true <-> Subset (Node c1 l1 x1 Leaf) r2H1:forall s : tree, Ok s -> subset_l1 s = true <-> Subset l1 sH6:Ok l2H7:Ok r2H8:lt_tree x2 l2H9:gt_tree x2 r2H5:Ok l1H11:lt_tree x1 l1H12:gt_tree x1 LeafH:X.lt x2 x1mem x1 r2 &&& subset_l1 (Node c2 l2 x2 r2) = true <-> Subset (Node c1 l1 x1 Leaf) (Node c2 l2 x2 r2)subset_l1:tree -> booll1:treex1:X.tc1, c2:Info.tl2:treex2:X.tr2:treeH6:Ok l2H7:Ok r2H8:lt_tree x2 l2H9:gt_tree x2 r2H5:Ok l1H11:lt_tree x1 l1H12:gt_tree x1 LeafH:X.lt x2 x1mem x1 r2 = true /\ Subset l1 (Node c2 l2 x2 r2) <-> Subset (Node c1 l1 x1 Leaf) (Node c2 l2 x2 r2)subset_l1:tree -> booll1:treex1:X.tc1, c2:Info.tl2:treex2:X.tr2:treeH6:Ok l2H7:Ok r2H8:lt_tree x2 l2H9:gt_tree x2 r2H5:Ok l1H11:lt_tree x1 l1H12:gt_tree x1 LeafH:X.lt x2 x1mem x1 r2 = true /\ (forall a : elt, InT a l1 -> InT a (Node c2 l2 x2 r2)) <-> (forall a : elt, InT a (Node c1 l1 x1 Leaf) -> InT a (Node c2 l2 x2 r2))l1:treex1:X.tc1, c2:Info.tl2:treex2:X.tr2:treeH6:Ok l2H7:Ok r2H8:lt_tree x2 l2H9:gt_tree x2 r2H5:Ok l1H11:lt_tree x1 l1H12:gt_tree x1 LeafH:X.lt x2 x1H0:boolH2:mem x1 r2 = trueH3:forall a0 : elt, InT a0 l1 -> InT a0 (Node c2 l2 x2 r2)a:eltH10:X.eq a x1InT a (Node c2 l2 x2 r2)l1:treex1:X.tc1, c2:Info.tl2:treex2:X.tr2:treeH6:Ok l2H7:Ok r2H8:lt_tree x2 l2H9:gt_tree x2 r2H5:Ok l1H11:lt_tree x1 l1H12:gt_tree x1 LeafH:X.lt x2 x1H0:boolH1:forall a : elt, InT a (Node c1 l1 x1 Leaf) -> InT a (Node c2 l2 x2 r2)mem x1 r2 = truel1:treex1:X.tc1, c2:Info.tl2:treex2:X.tr2:treeH6:Ok l2H7:Ok r2H8:lt_tree x2 l2H9:gt_tree x2 r2H5:Ok l1H11:lt_tree x1 l1H12:gt_tree x1 LeafH:X.lt x2 x1H0:boolH2:mem x1 r2 = trueH3:forall a0 : elt, InT a0 l1 -> InT a0 (Node c2 l2 x2 r2)a:eltH10:X.eq a x1InT a r2l1:treex1:X.tc1, c2:Info.tl2:treex2:X.tr2:treeH6:Ok l2H7:Ok r2H8:lt_tree x2 l2H9:gt_tree x2 r2H5:Ok l1H11:lt_tree x1 l1H12:gt_tree x1 LeafH:X.lt x2 x1H0:boolH1:forall a : elt, InT a (Node c1 l1 x1 Leaf) -> InT a (Node c2 l2 x2 r2)mem x1 r2 = truel1:treex1:X.tc1, c2:Info.tl2:treex2:X.tr2:treeH6:Ok l2H7:Ok r2H8:lt_tree x2 l2H9:gt_tree x2 r2H5:Ok l1H11:lt_tree x1 l1H12:gt_tree x1 LeafH:X.lt x2 x1H0:boolH2:mem x1 r2 = trueH3:forall a0 : elt, InT a0 l1 -> InT a0 (Node c2 l2 x2 r2)a:eltH10:X.eq a x1InT x1 r2l1:treex1:X.tc1, c2:Info.tl2:treex2:X.tr2:treeH6:Ok l2H7:Ok r2H8:lt_tree x2 l2H9:gt_tree x2 r2H5:Ok l1H11:lt_tree x1 l1H12:gt_tree x1 LeafH:X.lt x2 x1H0:boolH1:forall a : elt, InT a (Node c1 l1 x1 Leaf) -> InT a (Node c2 l2 x2 r2)mem x1 r2 = truel1:treex1:X.tc1, c2:Info.tl2:treex2:X.tr2:treeH6:Ok l2H7:Ok r2H8:lt_tree x2 l2H9:gt_tree x2 r2H5:Ok l1H11:lt_tree x1 l1H12:gt_tree x1 LeafH:X.lt x2 x1H0:boolH1:forall a : elt, InT a (Node c1 l1 x1 Leaf) -> InT a (Node c2 l2 x2 r2)mem x1 r2 = trueassert (InT x1 (Node c2 l2 x2 r2)) by auto; intuition_in; order. Qed.l1:treex1:X.tc1, c2:Info.tl2:treex2:X.tr2:treeH6:Ok l2H7:Ok r2H8:lt_tree x2 l2H9:gt_tree x2 r2H5:Ok l1H11:lt_tree x1 l1H12:gt_tree x1 LeafH:X.lt x2 x1H0:boolH1:forall a : elt, InT a (Node c1 l1 x1 Leaf) -> InT a (Node c2 l2 x2 r2)InT x1 r2forall (subset_r1 : tree -> bool) (r1 : tree) (x1 : X.t) (c1 : Info.t) (s2 : tree), bst (Node c1 Leaf x1 r1) -> bst s2 -> (forall s : tree, bst s -> subset_r1 s = true <-> Subset r1 s) -> subsetr subset_r1 x1 s2 = true <-> Subset (Node c1 Leaf x1 r1) s2forall (subset_r1 : tree -> bool) (r1 : tree) (x1 : X.t) (c1 : Info.t) (s2 : tree), bst (Node c1 Leaf x1 r1) -> bst s2 -> (forall s : tree, bst s -> subset_r1 s = true <-> Subset r1 s) -> subsetr subset_r1 x1 s2 = true <-> Subset (Node c1 Leaf x1 r1) s2subset_r1:tree -> boolr1:treex1:X.tc1:Info.tH:bst (Node c1 Leaf x1 r1)H0:bst LeafH1:forall s : tree, bst s -> subset_r1 s = true <-> Subset r1 sfalse = true <-> Subset (Node c1 Leaf x1 r1) Leafsubset_r1:tree -> boolr1:treex1:X.tc1, c2:Info.tl2:treex2:X.tr2:treeIHl2:bst (Node c1 Leaf x1 r1) -> bst l2 -> (forall s : tree, bst s -> subset_r1 s = true <-> Subset r1 s) -> subsetr subset_r1 x1 l2 = true <-> Subset (Node c1 Leaf x1 r1) l2IHr2:bst (Node c1 Leaf x1 r1) -> bst r2 -> (forall s : tree, bst s -> subset_r1 s = true <-> Subset r1 s) -> subsetr subset_r1 x1 r2 = true <-> Subset (Node c1 Leaf x1 r1) r2H:bst (Node c1 Leaf x1 r1)H0:bst (Node c2 l2 x2 r2)H1:forall s : tree, bst s -> subset_r1 s = true <-> Subset r1 smatch X.compare x1 x2 with | Eq => subset_r1 r2 | Lt => mem x1 l2 &&& subset_r1 (Node c2 l2 x2 r2) | Gt => subsetr subset_r1 x1 r2 end = true <-> Subset (Node c1 Leaf x1 r1) (Node c2 l2 x2 r2)subset_r1:tree -> boolr1:treex1:X.tc1:Info.tH:bst (Node c1 Leaf x1 r1)H0:bst LeafH1:forall s : tree, bst s -> subset_r1 s = true <-> Subset r1 sH2:forall a : elt, InT a (Node c1 Leaf x1 r1) -> InT a Leaffalse = truesubset_r1:tree -> boolr1:treex1:X.tc1, c2:Info.tl2:treex2:X.tr2:treeIHl2:bst (Node c1 Leaf x1 r1) -> bst l2 -> (forall s : tree, bst s -> subset_r1 s = true <-> Subset r1 s) -> subsetr subset_r1 x1 l2 = true <-> Subset (Node c1 Leaf x1 r1) l2IHr2:bst (Node c1 Leaf x1 r1) -> bst r2 -> (forall s : tree, bst s -> subset_r1 s = true <-> Subset r1 s) -> subsetr subset_r1 x1 r2 = true <-> Subset (Node c1 Leaf x1 r1) r2H:bst (Node c1 Leaf x1 r1)H0:bst (Node c2 l2 x2 r2)H1:forall s : tree, bst s -> subset_r1 s = true <-> Subset r1 smatch X.compare x1 x2 with | Eq => subset_r1 r2 | Lt => mem x1 l2 &&& subset_r1 (Node c2 l2 x2 r2) | Gt => subsetr subset_r1 x1 r2 end = true <-> Subset (Node c1 Leaf x1 r1) (Node c2 l2 x2 r2)subset_r1:tree -> boolr1:treex1:X.tc1, c2:Info.tl2:treex2:X.tr2:treeIHl2:bst (Node c1 Leaf x1 r1) -> bst l2 -> (forall s : tree, bst s -> subset_r1 s = true <-> Subset r1 s) -> subsetr subset_r1 x1 l2 = true <-> Subset (Node c1 Leaf x1 r1) l2IHr2:bst (Node c1 Leaf x1 r1) -> bst r2 -> (forall s : tree, bst s -> subset_r1 s = true <-> Subset r1 s) -> subsetr subset_r1 x1 r2 = true <-> Subset (Node c1 Leaf x1 r1) r2H:bst (Node c1 Leaf x1 r1)H0:bst (Node c2 l2 x2 r2)H1:forall s : tree, bst s -> subset_r1 s = true <-> Subset r1 smatch X.compare x1 x2 with | Eq => subset_r1 r2 | Lt => mem x1 l2 &&& subset_r1 (Node c2 l2 x2 r2) | Gt => subsetr subset_r1 x1 r2 end = true <-> Subset (Node c1 Leaf x1 r1) (Node c2 l2 x2 r2)subset_r1:tree -> boolr1:treex1:X.tc1, c2:Info.tl2:treex2:X.tr2:treeIHl2:bst l2 -> (forall s : tree, bst s -> subset_r1 s = true <-> Subset r1 s) -> subsetr subset_r1 x1 l2 = true <-> Subset (Node c1 Leaf x1 r1) l2IHr2:bst (Node c1 Leaf x1 r1) -> bst r2 -> (forall s : tree, bst s -> subset_r1 s = true <-> Subset r1 s) -> subsetr subset_r1 x1 r2 = true <-> Subset (Node c1 Leaf x1 r1) r2H:bst (Node c1 Leaf x1 r1)H0:bst (Node c2 l2 x2 r2)H1:forall s : tree, bst s -> subset_r1 s = true <-> Subset r1 smatch X.compare x1 x2 with | Eq => subset_r1 r2 | Lt => mem x1 l2 &&& subset_r1 (Node c2 l2 x2 r2) | Gt => subsetr subset_r1 x1 r2 end = true <-> Subset (Node c1 Leaf x1 r1) (Node c2 l2 x2 r2)subset_r1:tree -> boolr1:treex1:X.tc1, c2:Info.tl2:treex2:X.tr2:treeIHl2:bst l2 -> (forall s : tree, bst s -> subset_r1 s = true <-> Subset r1 s) -> subsetr subset_r1 x1 l2 = true <-> Subset (Node c1 Leaf x1 r1) l2IHr2:bst r2 -> (forall s : tree, bst s -> subset_r1 s = true <-> Subset r1 s) -> subsetr subset_r1 x1 r2 = true <-> Subset (Node c1 Leaf x1 r1) r2H:bst (Node c1 Leaf x1 r1)H0:bst (Node c2 l2 x2 r2)H1:forall s : tree, bst s -> subset_r1 s = true <-> Subset r1 smatch X.compare x1 x2 with | Eq => subset_r1 r2 | Lt => mem x1 l2 &&& subset_r1 (Node c2 l2 x2 r2) | Gt => subsetr subset_r1 x1 r2 end = true <-> Subset (Node c1 Leaf x1 r1) (Node c2 l2 x2 r2)subset_r1:tree -> boolr1:treex1:X.tc1, c2:Info.tl2:treex2:X.tr2:treeIHl2:bst l2 -> (forall s : tree, bst s -> subset_r1 s = true <-> Subset r1 s) -> subsetr subset_r1 x1 l2 = true <-> Subset (Node c1 Leaf x1 r1) l2IHr2:bst r2 -> (forall s : tree, bst s -> subset_r1 s = true <-> Subset r1 s) -> subsetr subset_r1 x1 r2 = true <-> Subset (Node c1 Leaf x1 r1) r2H1:forall s : tree, bst s -> subset_r1 s = true <-> Subset r1 sH6:Ok l2H7:Ok r2H8:lt_tree x2 l2H9:gt_tree x2 r2H10:Ok r1H11:lt_tree x1 LeafH12:gt_tree x1 r1match X.compare x1 x2 with | Eq => subset_r1 r2 | Lt => mem x1 l2 &&& subset_r1 (Node c2 l2 x2 r2) | Gt => subsetr subset_r1 x1 r2 end = true <-> Subset (Node c1 Leaf x1 r1) (Node c2 l2 x2 r2)subset_r1:tree -> boolr1:treex1:X.tc1, c2:Info.tl2:treex2:X.tr2:treeIHl2:bst l2 -> (forall s : tree, bst s -> subset_r1 s = true <-> Subset r1 s) -> subsetr subset_r1 x1 l2 = true <-> Subset (Node c1 Leaf x1 r1) l2IHr2:bst r2 -> (forall s : tree, bst s -> subset_r1 s = true <-> Subset r1 s) -> subsetr subset_r1 x1 r2 = true <-> Subset (Node c1 Leaf x1 r1) r2H1:forall s : tree, bst s -> subset_r1 s = true <-> Subset r1 sH6:Ok l2H7:Ok r2H8:lt_tree x2 l2H9:gt_tree x2 r2H10:Ok r1H11:lt_tree x1 LeafH12:gt_tree x1 r1H:X.eq x1 x2subset_r1 r2 = true <-> Subset (Node c1 Leaf x1 r1) (Node c2 l2 x2 r2)subset_r1:tree -> boolr1:treex1:X.tc1, c2:Info.tl2:treex2:X.tr2:treeIHl2:bst l2 -> (forall s : tree, bst s -> subset_r1 s = true <-> Subset r1 s) -> subsetr subset_r1 x1 l2 = true <-> Subset (Node c1 Leaf x1 r1) l2IHr2:bst r2 -> (forall s : tree, bst s -> subset_r1 s = true <-> Subset r1 s) -> subsetr subset_r1 x1 r2 = true <-> Subset (Node c1 Leaf x1 r1) r2H1:forall s : tree, bst s -> subset_r1 s = true <-> Subset r1 sH6:Ok l2H7:Ok r2H8:lt_tree x2 l2H9:gt_tree x2 r2H10:Ok r1H11:lt_tree x1 LeafH12:gt_tree x1 r1H:X.lt x1 x2mem x1 l2 &&& subset_r1 (Node c2 l2 x2 r2) = true <-> Subset (Node c1 Leaf x1 r1) (Node c2 l2 x2 r2)subset_r1:tree -> boolr1:treex1:X.tc1, c2:Info.tl2:treex2:X.tr2:treeIHl2:bst l2 -> (forall s : tree, bst s -> subset_r1 s = true <-> Subset r1 s) -> subsetr subset_r1 x1 l2 = true <-> Subset (Node c1 Leaf x1 r1) l2IHr2:bst r2 -> (forall s : tree, bst s -> subset_r1 s = true <-> Subset r1 s) -> subsetr subset_r1 x1 r2 = true <-> Subset (Node c1 Leaf x1 r1) r2H1:forall s : tree, bst s -> subset_r1 s = true <-> Subset r1 sH6:Ok l2H7:Ok r2H8:lt_tree x2 l2H9:gt_tree x2 r2H10:Ok r1H11:lt_tree x1 LeafH12:gt_tree x1 r1H:X.lt x2 x1subsetr subset_r1 x1 r2 = true <-> Subset (Node c1 Leaf x1 r1) (Node c2 l2 x2 r2)subset_r1:tree -> boolr1:treex1:X.tc1, c2:Info.tl2:treex2:X.tr2:treeH6:Ok l2H7:Ok r2H8:lt_tree x2 l2H9:gt_tree x2 r2H10:Ok r1H11:lt_tree x1 LeafH12:gt_tree x1 r1H:X.eq x1 x2Subset r1 r2 <-> Subset (Node c1 Leaf x1 r1) (Node c2 l2 x2 r2)subset_r1:tree -> boolr1:treex1:X.tc1, c2:Info.tl2:treex2:X.tr2:treeIHl2:bst l2 -> (forall s : tree, bst s -> subset_r1 s = true <-> Subset r1 s) -> subsetr subset_r1 x1 l2 = true <-> Subset (Node c1 Leaf x1 r1) l2IHr2:bst r2 -> (forall s : tree, bst s -> subset_r1 s = true <-> Subset r1 s) -> subsetr subset_r1 x1 r2 = true <-> Subset (Node c1 Leaf x1 r1) r2H1:forall s : tree, bst s -> subset_r1 s = true <-> Subset r1 sH6:Ok l2H7:Ok r2H8:lt_tree x2 l2H9:gt_tree x2 r2H10:Ok r1H11:lt_tree x1 LeafH12:gt_tree x1 r1H:X.lt x1 x2mem x1 l2 &&& subset_r1 (Node c2 l2 x2 r2) = true <-> Subset (Node c1 Leaf x1 r1) (Node c2 l2 x2 r2)subset_r1:tree -> boolr1:treex1:X.tc1, c2:Info.tl2:treex2:X.tr2:treeIHl2:bst l2 -> (forall s : tree, bst s -> subset_r1 s = true <-> Subset r1 s) -> subsetr subset_r1 x1 l2 = true <-> Subset (Node c1 Leaf x1 r1) l2IHr2:bst r2 -> (forall s : tree, bst s -> subset_r1 s = true <-> Subset r1 s) -> subsetr subset_r1 x1 r2 = true <-> Subset (Node c1 Leaf x1 r1) r2H1:forall s : tree, bst s -> subset_r1 s = true <-> Subset r1 sH6:Ok l2H7:Ok r2H8:lt_tree x2 l2H9:gt_tree x2 r2H10:Ok r1H11:lt_tree x1 LeafH12:gt_tree x1 r1H:X.lt x2 x1subsetr subset_r1 x1 r2 = true <-> Subset (Node c1 Leaf x1 r1) (Node c2 l2 x2 r2)subset_r1:tree -> boolr1:treex1:X.tc1, c2:Info.tl2:treex2:X.tr2:treeH6:Ok l2H7:Ok r2H8:lt_tree x2 l2H9:gt_tree x2 r2H10:Ok r1H11:lt_tree x1 LeafH12:gt_tree x1 r1H:X.eq x1 x2(forall a : elt, InT a r1 -> InT a r2) <-> (forall a : elt, InT a (Node c1 Leaf x1 r1) -> InT a (Node c2 l2 x2 r2))subset_r1:tree -> boolr1:treex1:X.tc1, c2:Info.tl2:treex2:X.tr2:treeIHl2:bst l2 -> (forall s : tree, bst s -> subset_r1 s = true <-> Subset r1 s) -> subsetr subset_r1 x1 l2 = true <-> Subset (Node c1 Leaf x1 r1) l2IHr2:bst r2 -> (forall s : tree, bst s -> subset_r1 s = true <-> Subset r1 s) -> subsetr subset_r1 x1 r2 = true <-> Subset (Node c1 Leaf x1 r1) r2H1:forall s : tree, bst s -> subset_r1 s = true <-> Subset r1 sH6:Ok l2H7:Ok r2H8:lt_tree x2 l2H9:gt_tree x2 r2H10:Ok r1H11:lt_tree x1 LeafH12:gt_tree x1 r1H:X.lt x1 x2mem x1 l2 &&& subset_r1 (Node c2 l2 x2 r2) = true <-> Subset (Node c1 Leaf x1 r1) (Node c2 l2 x2 r2)subset_r1:tree -> boolr1:treex1:X.tc1, c2:Info.tl2:treex2:X.tr2:treeIHl2:bst l2 -> (forall s : tree, bst s -> subset_r1 s = true <-> Subset r1 s) -> subsetr subset_r1 x1 l2 = true <-> Subset (Node c1 Leaf x1 r1) l2IHr2:bst r2 -> (forall s : tree, bst s -> subset_r1 s = true <-> Subset r1 s) -> subsetr subset_r1 x1 r2 = true <-> Subset (Node c1 Leaf x1 r1) r2H1:forall s : tree, bst s -> subset_r1 s = true <-> Subset r1 sH6:Ok l2H7:Ok r2H8:lt_tree x2 l2H9:gt_tree x2 r2H10:Ok r1H11:lt_tree x1 LeafH12:gt_tree x1 r1H:X.lt x2 x1subsetr subset_r1 x1 r2 = true <-> Subset (Node c1 Leaf x1 r1) (Node c2 l2 x2 r2)r1:treex1:X.tc1, c2:Info.tl2:treex2:X.tr2:treeH6:Ok l2H7:Ok r2H8:lt_tree x2 l2H9:gt_tree x2 r2H10:Ok r1H11:lt_tree x1 LeafH12:gt_tree x1 r1H:X.eq x1 x2H0:boolH1:forall a0 : elt, InT a0 r1 -> InT a0 r2a:eltH4:X.eq a x1InT a (Node c2 l2 x2 r2)r1:treex1:X.tc1, c2:Info.tl2:treex2:X.tr2:treeH6:Ok l2H7:Ok r2H8:lt_tree x2 l2H9:gt_tree x2 r2H10:Ok r1H11:lt_tree x1 LeafH12:gt_tree x1 r1H:X.eq x1 x2H0:boolH1:forall a0 : elt, InT a0 (Node c1 Leaf x1 r1) -> InT a0 (Node c2 l2 x2 r2)a:eltH2:InT a r1InT a r2subset_r1:tree -> boolr1:treex1:X.tc1, c2:Info.tl2:treex2:X.tr2:treeIHl2:bst l2 -> (forall s : tree, bst s -> subset_r1 s = true <-> Subset r1 s) -> subsetr subset_r1 x1 l2 = true <-> Subset (Node c1 Leaf x1 r1) l2IHr2:bst r2 -> (forall s : tree, bst s -> subset_r1 s = true <-> Subset r1 s) -> subsetr subset_r1 x1 r2 = true <-> Subset (Node c1 Leaf x1 r1) r2H1:forall s : tree, bst s -> subset_r1 s = true <-> Subset r1 sH6:Ok l2H7:Ok r2H8:lt_tree x2 l2H9:gt_tree x2 r2H10:Ok r1H11:lt_tree x1 LeafH12:gt_tree x1 r1H:X.lt x1 x2mem x1 l2 &&& subset_r1 (Node c2 l2 x2 r2) = true <-> Subset (Node c1 Leaf x1 r1) (Node c2 l2 x2 r2)subset_r1:tree -> boolr1:treex1:X.tc1, c2:Info.tl2:treex2:X.tr2:treeIHl2:bst l2 -> (forall s : tree, bst s -> subset_r1 s = true <-> Subset r1 s) -> subsetr subset_r1 x1 l2 = true <-> Subset (Node c1 Leaf x1 r1) l2IHr2:bst r2 -> (forall s : tree, bst s -> subset_r1 s = true <-> Subset r1 s) -> subsetr subset_r1 x1 r2 = true <-> Subset (Node c1 Leaf x1 r1) r2H1:forall s : tree, bst s -> subset_r1 s = true <-> Subset r1 sH6:Ok l2H7:Ok r2H8:lt_tree x2 l2H9:gt_tree x2 r2H10:Ok r1H11:lt_tree x1 LeafH12:gt_tree x1 r1H:X.lt x2 x1subsetr subset_r1 x1 r2 = true <-> Subset (Node c1 Leaf x1 r1) (Node c2 l2 x2 r2)r1:treex1:X.tc1, c2:Info.tl2:treex2:X.tr2:treeH6:Ok l2H7:Ok r2H8:lt_tree x2 l2H9:gt_tree x2 r2H10:Ok r1H11:lt_tree x1 LeafH12:gt_tree x1 r1H:X.eq x1 x2H0:boolH1:forall a0 : elt, InT a0 (Node c1 Leaf x1 r1) -> InT a0 (Node c2 l2 x2 r2)a:eltH2:InT a r1InT a r2subset_r1:tree -> boolr1:treex1:X.tc1, c2:Info.tl2:treex2:X.tr2:treeIHl2:bst l2 -> (forall s : tree, bst s -> subset_r1 s = true <-> Subset r1 s) -> subsetr subset_r1 x1 l2 = true <-> Subset (Node c1 Leaf x1 r1) l2IHr2:bst r2 -> (forall s : tree, bst s -> subset_r1 s = true <-> Subset r1 s) -> subsetr subset_r1 x1 r2 = true <-> Subset (Node c1 Leaf x1 r1) r2H1:forall s : tree, bst s -> subset_r1 s = true <-> Subset r1 sH6:Ok l2H7:Ok r2H8:lt_tree x2 l2H9:gt_tree x2 r2H10:Ok r1H11:lt_tree x1 LeafH12:gt_tree x1 r1H:X.lt x1 x2mem x1 l2 &&& subset_r1 (Node c2 l2 x2 r2) = true <-> Subset (Node c1 Leaf x1 r1) (Node c2 l2 x2 r2)subset_r1:tree -> boolr1:treex1:X.tc1, c2:Info.tl2:treex2:X.tr2:treeIHl2:bst l2 -> (forall s : tree, bst s -> subset_r1 s = true <-> Subset r1 s) -> subsetr subset_r1 x1 l2 = true <-> Subset (Node c1 Leaf x1 r1) l2IHr2:bst r2 -> (forall s : tree, bst s -> subset_r1 s = true <-> Subset r1 s) -> subsetr subset_r1 x1 r2 = true <-> Subset (Node c1 Leaf x1 r1) r2H1:forall s : tree, bst s -> subset_r1 s = true <-> Subset r1 sH6:Ok l2H7:Ok r2H8:lt_tree x2 l2H9:gt_tree x2 r2H10:Ok r1H11:lt_tree x1 LeafH12:gt_tree x1 r1H:X.lt x2 x1subsetr subset_r1 x1 r2 = true <-> Subset (Node c1 Leaf x1 r1) (Node c2 l2 x2 r2)subset_r1:tree -> boolr1:treex1:X.tc1, c2:Info.tl2:treex2:X.tr2:treeIHl2:bst l2 -> (forall s : tree, bst s -> subset_r1 s = true <-> Subset r1 s) -> subsetr subset_r1 x1 l2 = true <-> Subset (Node c1 Leaf x1 r1) l2IHr2:bst r2 -> (forall s : tree, bst s -> subset_r1 s = true <-> Subset r1 s) -> subsetr subset_r1 x1 r2 = true <-> Subset (Node c1 Leaf x1 r1) r2H1:forall s : tree, bst s -> subset_r1 s = true <-> Subset r1 sH6:Ok l2H7:Ok r2H8:lt_tree x2 l2H9:gt_tree x2 r2H10:Ok r1H11:lt_tree x1 LeafH12:gt_tree x1 r1H:X.lt x1 x2mem x1 l2 &&& subset_r1 (Node c2 l2 x2 r2) = true <-> Subset (Node c1 Leaf x1 r1) (Node c2 l2 x2 r2)subset_r1:tree -> boolr1:treex1:X.tc1, c2:Info.tl2:treex2:X.tr2:treeIHl2:bst l2 -> (forall s : tree, bst s -> subset_r1 s = true <-> Subset r1 s) -> subsetr subset_r1 x1 l2 = true <-> Subset (Node c1 Leaf x1 r1) l2IHr2:bst r2 -> (forall s : tree, bst s -> subset_r1 s = true <-> Subset r1 s) -> subsetr subset_r1 x1 r2 = true <-> Subset (Node c1 Leaf x1 r1) r2H1:forall s : tree, bst s -> subset_r1 s = true <-> Subset r1 sH6:Ok l2H7:Ok r2H8:lt_tree x2 l2H9:gt_tree x2 r2H10:Ok r1H11:lt_tree x1 LeafH12:gt_tree x1 r1H:X.lt x2 x1subsetr subset_r1 x1 r2 = true <-> Subset (Node c1 Leaf x1 r1) (Node c2 l2 x2 r2)subset_r1:tree -> boolr1:treex1:X.tc1, c2:Info.tl2:treex2:X.tr2:treeH6:Ok l2H7:Ok r2H8:lt_tree x2 l2H9:gt_tree x2 r2H10:Ok r1H11:lt_tree x1 LeafH12:gt_tree x1 r1H:X.lt x1 x2mem x1 l2 = true /\ Subset r1 (Node c2 l2 x2 r2) <-> Subset (Node c1 Leaf x1 r1) (Node c2 l2 x2 r2)subset_r1:tree -> boolr1:treex1:X.tc1, c2:Info.tl2:treex2:X.tr2:treeIHl2:bst l2 -> (forall s : tree, bst s -> subset_r1 s = true <-> Subset r1 s) -> subsetr subset_r1 x1 l2 = true <-> Subset (Node c1 Leaf x1 r1) l2IHr2:bst r2 -> (forall s : tree, bst s -> subset_r1 s = true <-> Subset r1 s) -> subsetr subset_r1 x1 r2 = true <-> Subset (Node c1 Leaf x1 r1) r2H1:forall s : tree, bst s -> subset_r1 s = true <-> Subset r1 sH6:Ok l2H7:Ok r2H8:lt_tree x2 l2H9:gt_tree x2 r2H10:Ok r1H11:lt_tree x1 LeafH12:gt_tree x1 r1H:X.lt x2 x1subsetr subset_r1 x1 r2 = true <-> Subset (Node c1 Leaf x1 r1) (Node c2 l2 x2 r2)subset_r1:tree -> boolr1:treex1:X.tc1, c2:Info.tl2:treex2:X.tr2:treeH6:Ok l2H7:Ok r2H8:lt_tree x2 l2H9:gt_tree x2 r2H10:Ok r1H11:lt_tree x1 LeafH12:gt_tree x1 r1H:X.lt x1 x2mem x1 l2 = true /\ (forall a : elt, InT a r1 -> InT a (Node c2 l2 x2 r2)) <-> (forall a : elt, InT a (Node c1 Leaf x1 r1) -> InT a (Node c2 l2 x2 r2))subset_r1:tree -> boolr1:treex1:X.tc1, c2:Info.tl2:treex2:X.tr2:treeIHl2:bst l2 -> (forall s : tree, bst s -> subset_r1 s = true <-> Subset r1 s) -> subsetr subset_r1 x1 l2 = true <-> Subset (Node c1 Leaf x1 r1) l2IHr2:bst r2 -> (forall s : tree, bst s -> subset_r1 s = true <-> Subset r1 s) -> subsetr subset_r1 x1 r2 = true <-> Subset (Node c1 Leaf x1 r1) r2H1:forall s : tree, bst s -> subset_r1 s = true <-> Subset r1 sH6:Ok l2H7:Ok r2H8:lt_tree x2 l2H9:gt_tree x2 r2H10:Ok r1H11:lt_tree x1 LeafH12:gt_tree x1 r1H:X.lt x2 x1subsetr subset_r1 x1 r2 = true <-> Subset (Node c1 Leaf x1 r1) (Node c2 l2 x2 r2)r1:treex1:X.tc1, c2:Info.tl2:treex2:X.tr2:treeH6:Ok l2H7:Ok r2H8:lt_tree x2 l2H9:gt_tree x2 r2H10:Ok r1H11:lt_tree x1 LeafH12:gt_tree x1 r1H:X.lt x1 x2H0:boolH2:mem x1 l2 = trueH3:forall a0 : elt, InT a0 r1 -> InT a0 (Node c2 l2 x2 r2)a:eltH5:X.eq a x1InT a (Node c2 l2 x2 r2)r1:treex1:X.tc1, c2:Info.tl2:treex2:X.tr2:treeH6:Ok l2H7:Ok r2H8:lt_tree x2 l2H9:gt_tree x2 r2H10:Ok r1H11:lt_tree x1 LeafH12:gt_tree x1 r1H:X.lt x1 x2H0:boolH1:forall a : elt, InT a (Node c1 Leaf x1 r1) -> InT a (Node c2 l2 x2 r2)mem x1 l2 = truesubset_r1:tree -> boolr1:treex1:X.tc1, c2:Info.tl2:treex2:X.tr2:treeIHl2:bst l2 -> (forall s : tree, bst s -> subset_r1 s = true <-> Subset r1 s) -> subsetr subset_r1 x1 l2 = true <-> Subset (Node c1 Leaf x1 r1) l2IHr2:bst r2 -> (forall s : tree, bst s -> subset_r1 s = true <-> Subset r1 s) -> subsetr subset_r1 x1 r2 = true <-> Subset (Node c1 Leaf x1 r1) r2H1:forall s : tree, bst s -> subset_r1 s = true <-> Subset r1 sH6:Ok l2H7:Ok r2H8:lt_tree x2 l2H9:gt_tree x2 r2H10:Ok r1H11:lt_tree x1 LeafH12:gt_tree x1 r1H:X.lt x2 x1subsetr subset_r1 x1 r2 = true <-> Subset (Node c1 Leaf x1 r1) (Node c2 l2 x2 r2)r1:treex1:X.tc1, c2:Info.tl2:treex2:X.tr2:treeH6:Ok l2H7:Ok r2H8:lt_tree x2 l2H9:gt_tree x2 r2H10:Ok r1H11:lt_tree x1 LeafH12:gt_tree x1 r1H:X.lt x1 x2H0:boolH2:mem x1 l2 = trueH3:forall a0 : elt, InT a0 r1 -> InT a0 (Node c2 l2 x2 r2)a:eltH5:X.eq a x1InT a l2r1:treex1:X.tc1, c2:Info.tl2:treex2:X.tr2:treeH6:Ok l2H7:Ok r2H8:lt_tree x2 l2H9:gt_tree x2 r2H10:Ok r1H11:lt_tree x1 LeafH12:gt_tree x1 r1H:X.lt x1 x2H0:boolH1:forall a : elt, InT a (Node c1 Leaf x1 r1) -> InT a (Node c2 l2 x2 r2)mem x1 l2 = truesubset_r1:tree -> boolr1:treex1:X.tc1, c2:Info.tl2:treex2:X.tr2:treeIHl2:bst l2 -> (forall s : tree, bst s -> subset_r1 s = true <-> Subset r1 s) -> subsetr subset_r1 x1 l2 = true <-> Subset (Node c1 Leaf x1 r1) l2IHr2:bst r2 -> (forall s : tree, bst s -> subset_r1 s = true <-> Subset r1 s) -> subsetr subset_r1 x1 r2 = true <-> Subset (Node c1 Leaf x1 r1) r2H1:forall s : tree, bst s -> subset_r1 s = true <-> Subset r1 sH6:Ok l2H7:Ok r2H8:lt_tree x2 l2H9:gt_tree x2 r2H10:Ok r1H11:lt_tree x1 LeafH12:gt_tree x1 r1H:X.lt x2 x1subsetr subset_r1 x1 r2 = true <-> Subset (Node c1 Leaf x1 r1) (Node c2 l2 x2 r2)r1:treex1:X.tc1, c2:Info.tl2:treex2:X.tr2:treeH6:Ok l2H7:Ok r2H8:lt_tree x2 l2H9:gt_tree x2 r2H10:Ok r1H11:lt_tree x1 LeafH12:gt_tree x1 r1H:X.lt x1 x2H0:boolH2:mem x1 l2 = trueH3:forall a0 : elt, InT a0 r1 -> InT a0 (Node c2 l2 x2 r2)a:eltH5:X.eq a x1InT x1 l2r1:treex1:X.tc1, c2:Info.tl2:treex2:X.tr2:treeH6:Ok l2H7:Ok r2H8:lt_tree x2 l2H9:gt_tree x2 r2H10:Ok r1H11:lt_tree x1 LeafH12:gt_tree x1 r1H:X.lt x1 x2H0:boolH1:forall a : elt, InT a (Node c1 Leaf x1 r1) -> InT a (Node c2 l2 x2 r2)mem x1 l2 = truesubset_r1:tree -> boolr1:treex1:X.tc1, c2:Info.tl2:treex2:X.tr2:treeIHl2:bst l2 -> (forall s : tree, bst s -> subset_r1 s = true <-> Subset r1 s) -> subsetr subset_r1 x1 l2 = true <-> Subset (Node c1 Leaf x1 r1) l2IHr2:bst r2 -> (forall s : tree, bst s -> subset_r1 s = true <-> Subset r1 s) -> subsetr subset_r1 x1 r2 = true <-> Subset (Node c1 Leaf x1 r1) r2H1:forall s : tree, bst s -> subset_r1 s = true <-> Subset r1 sH6:Ok l2H7:Ok r2H8:lt_tree x2 l2H9:gt_tree x2 r2H10:Ok r1H11:lt_tree x1 LeafH12:gt_tree x1 r1H:X.lt x2 x1subsetr subset_r1 x1 r2 = true <-> Subset (Node c1 Leaf x1 r1) (Node c2 l2 x2 r2)r1:treex1:X.tc1, c2:Info.tl2:treex2:X.tr2:treeH6:Ok l2H7:Ok r2H8:lt_tree x2 l2H9:gt_tree x2 r2H10:Ok r1H11:lt_tree x1 LeafH12:gt_tree x1 r1H:X.lt x1 x2H0:boolH1:forall a : elt, InT a (Node c1 Leaf x1 r1) -> InT a (Node c2 l2 x2 r2)mem x1 l2 = truesubset_r1:tree -> boolr1:treex1:X.tc1, c2:Info.tl2:treex2:X.tr2:treeIHl2:bst l2 -> (forall s : tree, bst s -> subset_r1 s = true <-> Subset r1 s) -> subsetr subset_r1 x1 l2 = true <-> Subset (Node c1 Leaf x1 r1) l2IHr2:bst r2 -> (forall s : tree, bst s -> subset_r1 s = true <-> Subset r1 s) -> subsetr subset_r1 x1 r2 = true <-> Subset (Node c1 Leaf x1 r1) r2H1:forall s : tree, bst s -> subset_r1 s = true <-> Subset r1 sH6:Ok l2H7:Ok r2H8:lt_tree x2 l2H9:gt_tree x2 r2H10:Ok r1H11:lt_tree x1 LeafH12:gt_tree x1 r1H:X.lt x2 x1subsetr subset_r1 x1 r2 = true <-> Subset (Node c1 Leaf x1 r1) (Node c2 l2 x2 r2)r1:treex1:X.tc1, c2:Info.tl2:treex2:X.tr2:treeH6:Ok l2H7:Ok r2H8:lt_tree x2 l2H9:gt_tree x2 r2H10:Ok r1H11:lt_tree x1 LeafH12:gt_tree x1 r1H:X.lt x1 x2H0:boolH1:forall a : elt, InT a (Node c1 Leaf x1 r1) -> InT a (Node c2 l2 x2 r2)InT x1 l2subset_r1:tree -> boolr1:treex1:X.tc1, c2:Info.tl2:treex2:X.tr2:treeIHl2:bst l2 -> (forall s : tree, bst s -> subset_r1 s = true <-> Subset r1 s) -> subsetr subset_r1 x1 l2 = true <-> Subset (Node c1 Leaf x1 r1) l2IHr2:bst r2 -> (forall s : tree, bst s -> subset_r1 s = true <-> Subset r1 s) -> subsetr subset_r1 x1 r2 = true <-> Subset (Node c1 Leaf x1 r1) r2H1:forall s : tree, bst s -> subset_r1 s = true <-> Subset r1 sH6:Ok l2H7:Ok r2H8:lt_tree x2 l2H9:gt_tree x2 r2H10:Ok r1H11:lt_tree x1 LeafH12:gt_tree x1 r1H:X.lt x2 x1subsetr subset_r1 x1 r2 = true <-> Subset (Node c1 Leaf x1 r1) (Node c2 l2 x2 r2)subset_r1:tree -> boolr1:treex1:X.tc1, c2:Info.tl2:treex2:X.tr2:treeIHl2:bst l2 -> (forall s : tree, bst s -> subset_r1 s = true <-> Subset r1 s) -> subsetr subset_r1 x1 l2 = true <-> Subset (Node c1 Leaf x1 r1) l2IHr2:bst r2 -> (forall s : tree, bst s -> subset_r1 s = true <-> Subset r1 s) -> subsetr subset_r1 x1 r2 = true <-> Subset (Node c1 Leaf x1 r1) r2H1:forall s : tree, bst s -> subset_r1 s = true <-> Subset r1 sH6:Ok l2H7:Ok r2H8:lt_tree x2 l2H9:gt_tree x2 r2H10:Ok r1H11:lt_tree x1 LeafH12:gt_tree x1 r1H:X.lt x2 x1subsetr subset_r1 x1 r2 = true <-> Subset (Node c1 Leaf x1 r1) (Node c2 l2 x2 r2)subset_r1:tree -> boolr1:treex1:X.tc1, c2:Info.tl2:treex2:X.tr2:treeH6:Ok l2H7:Ok r2H8:lt_tree x2 l2H9:gt_tree x2 r2H10:Ok r1H11:lt_tree x1 LeafH12:gt_tree x1 r1H:X.lt x2 x1Subset (Node c1 Leaf x1 r1) r2 <-> Subset (Node c1 Leaf x1 r1) (Node c2 l2 x2 r2)subset_r1:tree -> boolr1:treex1:X.tc1, c2:Info.tl2:treex2:X.tr2:treeH6:Ok l2H7:Ok r2H8:lt_tree x2 l2H9:gt_tree x2 r2H10:Ok r1H11:lt_tree x1 LeafH12:gt_tree x1 r1H:X.lt x2 x1(forall a : elt, InT a (Node c1 Leaf x1 r1) -> InT a r2) <-> (forall a : elt, InT a (Node c1 Leaf x1 r1) -> InT a (Node c2 l2 x2 r2))r1:treex1:X.tc1, c2:Info.tl2:treex2:X.tr2:treeH6:Ok l2H7:Ok r2H8:lt_tree x2 l2H9:gt_tree x2 r2H10:Ok r1H11:lt_tree x1 LeafH12:gt_tree x1 r1H:X.lt x2 x1H0:boolH1:forall a0 : elt, InT a0 (Node c1 Leaf x1 r1) -> InT a0 (Node c2 l2 x2 r2)a:eltH4:X.eq a x1InT a r2r1:treex1:X.tc1, c2:Info.tl2:treex2:X.tr2:treeH6:Ok l2H7:Ok r2H8:lt_tree x2 l2H9:gt_tree x2 r2H10:Ok r1H11:lt_tree x1 LeafH12:gt_tree x1 r1H:X.lt x2 x1H0:boolH1:forall a0 : elt, InT a0 (Node c1 Leaf x1 r1) -> InT a0 (Node c2 l2 x2 r2)a:eltH4:InT a r1InT a r2assert (InT a (Node c2 l2 x2 r2)) by auto; intuition_in; order. Qed.r1:treex1:X.tc1, c2:Info.tl2:treex2:X.tr2:treeH6:Ok l2H7:Ok r2H8:lt_tree x2 l2H9:gt_tree x2 r2H10:Ok r1H11:lt_tree x1 LeafH12:gt_tree x1 r1H:X.lt x2 x1H0:boolH1:forall a0 : elt, InT a0 (Node c1 Leaf x1 r1) -> InT a0 (Node c2 l2 x2 r2)a:eltH4:InT a r1InT a r2forall s1 s2 : tree, Ok s1 -> Ok s2 -> subset s1 s2 = true <-> Subset s1 s2forall s1 s2 : tree, Ok s1 -> Ok s2 -> subset s1 s2 = true <-> Subset s1 s2s2:treeH:Ok LeafH0:Ok s2true = true <-> Subset Leaf s2c1:Info.tl1:treex1:X.tr1:treeIHl1:forall s0 : tree, Ok l1 -> Ok s0 -> subset l1 s0 = true <-> Subset l1 s0IHr1:forall s0 : tree, Ok r1 -> Ok s0 -> subset r1 s0 = true <-> Subset r1 s0s2:treeH:Ok (Node c1 l1 x1 r1)H0:Ok s2match s2 with | Leaf => false | Node _ l2 x2 r2 => match X.compare x1 x2 with | Eq => subset l1 l2 &&& subset r1 r2 | Lt => subsetl (subset l1) x1 l2 &&& subset r1 s2 | Gt => subsetr (subset r1) x1 r2 &&& subset l1 s2 end end = true <-> Subset (Node c1 l1 x1 r1) s2c1:Info.tl1:treex1:X.tr1:treeIHl1:forall s0 : tree, Ok l1 -> Ok s0 -> subset l1 s0 = true <-> Subset l1 s0IHr1:forall s0 : tree, Ok r1 -> Ok s0 -> subset r1 s0 = true <-> Subset r1 s0s2:treeH:Ok (Node c1 l1 x1 r1)H0:Ok s2match s2 with | Leaf => false | Node _ l2 x2 r2 => match X.compare x1 x2 with | Eq => subset l1 l2 &&& subset r1 r2 | Lt => subsetl (subset l1) x1 l2 &&& subset r1 s2 | Gt => subsetr (subset r1) x1 r2 &&& subset l1 s2 end end = true <-> Subset (Node c1 l1 x1 r1) s2c1:Info.tl1:treex1:X.tr1:treeIHl1:forall s2 : tree, Ok l1 -> Ok s2 -> subset l1 s2 = true <-> Subset l1 s2IHr1:forall s2 : tree, Ok r1 -> Ok s2 -> subset r1 s2 = true <-> Subset r1 s2H:Ok (Node c1 l1 x1 r1)H0:Ok Leaffalse = true <-> Subset (Node c1 l1 x1 r1) Leafc1:Info.tl1:treex1:X.tr1:treeIHl1:forall s2 : tree, Ok l1 -> Ok s2 -> subset l1 s2 = true <-> Subset l1 s2IHr1:forall s2 : tree, Ok r1 -> Ok s2 -> subset r1 s2 = true <-> Subset r1 s2c2:Info.tl2:treex2:X.tr2:treeH:Ok (Node c1 l1 x1 r1)H0:Ok (Node c2 l2 x2 r2)match X.compare x1 x2 with | Eq => subset l1 l2 &&& subset r1 r2 | Lt => subsetl (subset l1) x1 l2 &&& subset r1 (Node c2 l2 x2 r2) | Gt => subsetr (subset r1) x1 r2 &&& subset l1 (Node c2 l2 x2 r2) end = true <-> Subset (Node c1 l1 x1 r1) (Node c2 l2 x2 r2)c1:Info.tl1:treex1:X.tr1:treeIHl1:forall s2 : tree, Ok l1 -> Ok s2 -> subset l1 s2 = true <-> Subset l1 s2IHr1:forall s2 : tree, Ok r1 -> Ok s2 -> subset r1 s2 = true <-> Subset r1 s2H1:forall a : elt, InT a (Node c1 l1 x1 r1) -> InT a LeafH6:Ok l1H7:Ok r1H8:lt_tree x1 l1H9:gt_tree x1 r1false = truec1:Info.tl1:treex1:X.tr1:treeIHl1:forall s2 : tree, Ok l1 -> Ok s2 -> subset l1 s2 = true <-> Subset l1 s2IHr1:forall s2 : tree, Ok r1 -> Ok s2 -> subset r1 s2 = true <-> Subset r1 s2c2:Info.tl2:treex2:X.tr2:treeH:Ok (Node c1 l1 x1 r1)H0:Ok (Node c2 l2 x2 r2)match X.compare x1 x2 with | Eq => subset l1 l2 &&& subset r1 r2 | Lt => subsetl (subset l1) x1 l2 &&& subset r1 (Node c2 l2 x2 r2) | Gt => subsetr (subset r1) x1 r2 &&& subset l1 (Node c2 l2 x2 r2) end = true <-> Subset (Node c1 l1 x1 r1) (Node c2 l2 x2 r2)c1:Info.tl1:treex1:X.tr1:treeIHl1:forall s2 : tree, Ok l1 -> Ok s2 -> subset l1 s2 = true <-> Subset l1 s2IHr1:forall s2 : tree, Ok r1 -> Ok s2 -> subset r1 s2 = true <-> Subset r1 s2c2:Info.tl2:treex2:X.tr2:treeH:Ok (Node c1 l1 x1 r1)H0:Ok (Node c2 l2 x2 r2)match X.compare x1 x2 with | Eq => subset l1 l2 &&& subset r1 r2 | Lt => subsetl (subset l1) x1 l2 &&& subset r1 (Node c2 l2 x2 r2) | Gt => subsetr (subset r1) x1 r2 &&& subset l1 (Node c2 l2 x2 r2) end = true <-> Subset (Node c1 l1 x1 r1) (Node c2 l2 x2 r2)c1:Info.tl1:treex1:X.tr1:treeIHl1:forall s2 : tree, Ok l1 -> Ok s2 -> subset l1 s2 = true <-> Subset l1 s2IHr1:forall s2 : tree, Ok r1 -> Ok s2 -> subset r1 s2 = true <-> Subset r1 s2c2:Info.tl2:treex2:X.tr2:treeH5:Ok l2H6:Ok r2H7:lt_tree x2 l2H8:gt_tree x2 r2H4:Ok l1H9:Ok r1H10:lt_tree x1 l1H11:gt_tree x1 r1match X.compare x1 x2 with | Eq => subset l1 l2 &&& subset r1 r2 | Lt => subsetl (subset l1) x1 l2 &&& subset r1 (Node c2 l2 x2 r2) | Gt => subsetr (subset r1) x1 r2 &&& subset l1 (Node c2 l2 x2 r2) end = true <-> Subset (Node c1 l1 x1 r1) (Node c2 l2 x2 r2)c1:Info.tl1:treex1:X.tr1:treeIHl1:forall s2 : tree, Ok l1 -> Ok s2 -> subset l1 s2 = true <-> Subset l1 s2IHr1:forall s2 : tree, Ok r1 -> Ok s2 -> subset r1 s2 = true <-> Subset r1 s2c2:Info.tl2:treex2:X.tr2:treeH5:Ok l2H6:Ok r2H7:lt_tree x2 l2H8:gt_tree x2 r2H4:Ok l1H9:Ok r1H10:lt_tree x1 l1H11:gt_tree x1 r1H:X.eq x1 x2subset l1 l2 &&& subset r1 r2 = true <-> Subset (Node c1 l1 x1 r1) (Node c2 l2 x2 r2)c1:Info.tl1:treex1:X.tr1:treeIHl1:forall s2 : tree, Ok l1 -> Ok s2 -> subset l1 s2 = true <-> Subset l1 s2IHr1:forall s2 : tree, Ok r1 -> Ok s2 -> subset r1 s2 = true <-> Subset r1 s2c2:Info.tl2:treex2:X.tr2:treeH5:Ok l2H6:Ok r2H7:lt_tree x2 l2H8:gt_tree x2 r2H4:Ok l1H9:Ok r1H10:lt_tree x1 l1H11:gt_tree x1 r1H:X.lt x1 x2subsetl (subset l1) x1 l2 &&& subset r1 (Node c2 l2 x2 r2) = true <-> Subset (Node c1 l1 x1 r1) (Node c2 l2 x2 r2)c1:Info.tl1:treex1:X.tr1:treeIHl1:forall s2 : tree, Ok l1 -> Ok s2 -> subset l1 s2 = true <-> Subset l1 s2IHr1:forall s2 : tree, Ok r1 -> Ok s2 -> subset r1 s2 = true <-> Subset r1 s2c2:Info.tl2:treex2:X.tr2:treeH5:Ok l2H6:Ok r2H7:lt_tree x2 l2H8:gt_tree x2 r2H4:Ok l1H9:Ok r1H10:lt_tree x1 l1H11:gt_tree x1 r1H:X.lt x2 x1subsetr (subset r1) x1 r2 &&& subset l1 (Node c2 l2 x2 r2) = true <-> Subset (Node c1 l1 x1 r1) (Node c2 l2 x2 r2)c1:Info.tl1:treex1:X.tr1:treeIHl1:forall s2 : tree, Ok l1 -> Ok s2 -> subset l1 s2 = true <-> Subset l1 s2IHr1:forall s2 : tree, Ok r1 -> Ok s2 -> subset r1 s2 = true <-> Subset r1 s2c2:Info.tl2:treex2:X.tr2:treeH5:Ok l2H6:Ok r2H7:lt_tree x2 l2H8:gt_tree x2 r2H4:Ok l1H9:Ok r1H10:lt_tree x1 l1H11:gt_tree x1 r1H:X.eq x1 x2Subset l1 l2 /\ Subset r1 r2 <-> Subset (Node c1 l1 x1 r1) (Node c2 l2 x2 r2)c1:Info.tl1:treex1:X.tr1:treeIHl1:forall s2 : tree, Ok l1 -> Ok s2 -> subset l1 s2 = true <-> Subset l1 s2IHr1:forall s2 : tree, Ok r1 -> Ok s2 -> subset r1 s2 = true <-> Subset r1 s2c2:Info.tl2:treex2:X.tr2:treeH5:Ok l2H6:Ok r2H7:lt_tree x2 l2H8:gt_tree x2 r2H4:Ok l1H9:Ok r1H10:lt_tree x1 l1H11:gt_tree x1 r1H:X.lt x1 x2subsetl (subset l1) x1 l2 &&& subset r1 (Node c2 l2 x2 r2) = true <-> Subset (Node c1 l1 x1 r1) (Node c2 l2 x2 r2)c1:Info.tl1:treex1:X.tr1:treeIHl1:forall s2 : tree, Ok l1 -> Ok s2 -> subset l1 s2 = true <-> Subset l1 s2IHr1:forall s2 : tree, Ok r1 -> Ok s2 -> subset r1 s2 = true <-> Subset r1 s2c2:Info.tl2:treex2:X.tr2:treeH5:Ok l2H6:Ok r2H7:lt_tree x2 l2H8:gt_tree x2 r2H4:Ok l1H9:Ok r1H10:lt_tree x1 l1H11:gt_tree x1 r1H:X.lt x2 x1subsetr (subset r1) x1 r2 &&& subset l1 (Node c2 l2 x2 r2) = true <-> Subset (Node c1 l1 x1 r1) (Node c2 l2 x2 r2)c1:Info.tl1:treex1:X.tr1:treec2:Info.tl2:treex2:X.tr2:treeH5:Ok l2H6:Ok r2H7:lt_tree x2 l2H8:gt_tree x2 r2H4:Ok l1H9:Ok r1H10:lt_tree x1 l1H11:gt_tree x1 r1H:X.eq x1 x2Subset l1 l2 /\ Subset r1 r2 <-> Subset (Node c1 l1 x1 r1) (Node c2 l2 x2 r2)c1:Info.tl1:treex1:X.tr1:treeIHl1:forall s2 : tree, Ok l1 -> Ok s2 -> subset l1 s2 = true <-> Subset l1 s2IHr1:forall s2 : tree, Ok r1 -> Ok s2 -> subset r1 s2 = true <-> Subset r1 s2c2:Info.tl2:treex2:X.tr2:treeH5:Ok l2H6:Ok r2H7:lt_tree x2 l2H8:gt_tree x2 r2H4:Ok l1H9:Ok r1H10:lt_tree x1 l1H11:gt_tree x1 r1H:X.lt x1 x2subsetl (subset l1) x1 l2 &&& subset r1 (Node c2 l2 x2 r2) = true <-> Subset (Node c1 l1 x1 r1) (Node c2 l2 x2 r2)c1:Info.tl1:treex1:X.tr1:treeIHl1:forall s2 : tree, Ok l1 -> Ok s2 -> subset l1 s2 = true <-> Subset l1 s2IHr1:forall s2 : tree, Ok r1 -> Ok s2 -> subset r1 s2 = true <-> Subset r1 s2c2:Info.tl2:treex2:X.tr2:treeH5:Ok l2H6:Ok r2H7:lt_tree x2 l2H8:gt_tree x2 r2H4:Ok l1H9:Ok r1H10:lt_tree x1 l1H11:gt_tree x1 r1H:X.lt x2 x1subsetr (subset r1) x1 r2 &&& subset l1 (Node c2 l2 x2 r2) = true <-> Subset (Node c1 l1 x1 r1) (Node c2 l2 x2 r2)c1:Info.tl1:treex1:X.tr1:treec2:Info.tl2:treex2:X.tr2:treeH5:Ok l2H6:Ok r2H7:lt_tree x2 l2H8:gt_tree x2 r2H4:Ok l1H9:Ok r1H10:lt_tree x1 l1H11:gt_tree x1 r1H:X.eq x1 x2H1:forall a0 : elt, InT a0 l1 -> InT a0 l2H2:forall a0 : elt, InT a0 r1 -> InT a0 r2a:eltH12:X.eq a x1InT a (Node c2 l2 x2 r2)c1:Info.tl1:treex1:X.tr1:treec2:Info.tl2:treex2:X.tr2:treeH5:Ok l2H6:Ok r2H7:lt_tree x2 l2H8:gt_tree x2 r2H4:Ok l1H9:Ok r1H10:lt_tree x1 l1H11:gt_tree x1 r1H:X.eq x1 x2H0:forall a0 : elt, InT a0 (Node c1 l1 x1 r1) -> InT a0 (Node c2 l2 x2 r2)a:eltH1:InT a l1InT a l2c1:Info.tl1:treex1:X.tr1:treec2:Info.tl2:treex2:X.tr2:treeH5:Ok l2H6:Ok r2H7:lt_tree x2 l2H8:gt_tree x2 r2H4:Ok l1H9:Ok r1H10:lt_tree x1 l1H11:gt_tree x1 r1H:X.eq x1 x2H0:forall a0 : elt, InT a0 (Node c1 l1 x1 r1) -> InT a0 (Node c2 l2 x2 r2)a:eltH1:InT a r1InT a r2c1:Info.tl1:treex1:X.tr1:treeIHl1:forall s2 : tree, Ok l1 -> Ok s2 -> subset l1 s2 = true <-> Subset l1 s2IHr1:forall s2 : tree, Ok r1 -> Ok s2 -> subset r1 s2 = true <-> Subset r1 s2c2:Info.tl2:treex2:X.tr2:treeH5:Ok l2H6:Ok r2H7:lt_tree x2 l2H8:gt_tree x2 r2H4:Ok l1H9:Ok r1H10:lt_tree x1 l1H11:gt_tree x1 r1H:X.lt x1 x2subsetl (subset l1) x1 l2 &&& subset r1 (Node c2 l2 x2 r2) = true <-> Subset (Node c1 l1 x1 r1) (Node c2 l2 x2 r2)c1:Info.tl1:treex1:X.tr1:treeIHl1:forall s2 : tree, Ok l1 -> Ok s2 -> subset l1 s2 = true <-> Subset l1 s2IHr1:forall s2 : tree, Ok r1 -> Ok s2 -> subset r1 s2 = true <-> Subset r1 s2c2:Info.tl2:treex2:X.tr2:treeH5:Ok l2H6:Ok r2H7:lt_tree x2 l2H8:gt_tree x2 r2H4:Ok l1H9:Ok r1H10:lt_tree x1 l1H11:gt_tree x1 r1H:X.lt x2 x1subsetr (subset r1) x1 r2 &&& subset l1 (Node c2 l2 x2 r2) = true <-> Subset (Node c1 l1 x1 r1) (Node c2 l2 x2 r2)c1:Info.tl1:treex1:X.tr1:treec2:Info.tl2:treex2:X.tr2:treeH5:Ok l2H6:Ok r2H7:lt_tree x2 l2H8:gt_tree x2 r2H4:Ok l1H9:Ok r1H10:lt_tree x1 l1H11:gt_tree x1 r1H:X.eq x1 x2H0:forall a0 : elt, InT a0 (Node c1 l1 x1 r1) -> InT a0 (Node c2 l2 x2 r2)a:eltH1:InT a l1InT a l2c1:Info.tl1:treex1:X.tr1:treec2:Info.tl2:treex2:X.tr2:treeH5:Ok l2H6:Ok r2H7:lt_tree x2 l2H8:gt_tree x2 r2H4:Ok l1H9:Ok r1H10:lt_tree x1 l1H11:gt_tree x1 r1H:X.eq x1 x2H0:forall a0 : elt, InT a0 (Node c1 l1 x1 r1) -> InT a0 (Node c2 l2 x2 r2)a:eltH1:InT a r1InT a r2c1:Info.tl1:treex1:X.tr1:treeIHl1:forall s2 : tree, Ok l1 -> Ok s2 -> subset l1 s2 = true <-> Subset l1 s2IHr1:forall s2 : tree, Ok r1 -> Ok s2 -> subset r1 s2 = true <-> Subset r1 s2c2:Info.tl2:treex2:X.tr2:treeH5:Ok l2H6:Ok r2H7:lt_tree x2 l2H8:gt_tree x2 r2H4:Ok l1H9:Ok r1H10:lt_tree x1 l1H11:gt_tree x1 r1H:X.lt x1 x2subsetl (subset l1) x1 l2 &&& subset r1 (Node c2 l2 x2 r2) = true <-> Subset (Node c1 l1 x1 r1) (Node c2 l2 x2 r2)c1:Info.tl1:treex1:X.tr1:treeIHl1:forall s2 : tree, Ok l1 -> Ok s2 -> subset l1 s2 = true <-> Subset l1 s2IHr1:forall s2 : tree, Ok r1 -> Ok s2 -> subset r1 s2 = true <-> Subset r1 s2c2:Info.tl2:treex2:X.tr2:treeH5:Ok l2H6:Ok r2H7:lt_tree x2 l2H8:gt_tree x2 r2H4:Ok l1H9:Ok r1H10:lt_tree x1 l1H11:gt_tree x1 r1H:X.lt x2 x1subsetr (subset r1) x1 r2 &&& subset l1 (Node c2 l2 x2 r2) = true <-> Subset (Node c1 l1 x1 r1) (Node c2 l2 x2 r2)c1:Info.tl1:treex1:X.tr1:treec2:Info.tl2:treex2:X.tr2:treeH5:Ok l2H6:Ok r2H7:lt_tree x2 l2H8:gt_tree x2 r2H4:Ok l1H9:Ok r1H10:lt_tree x1 l1H11:gt_tree x1 r1H:X.eq x1 x2H0:forall a0 : elt, InT a0 (Node c1 l1 x1 r1) -> InT a0 (Node c2 l2 x2 r2)a:eltH1:InT a r1InT a r2c1:Info.tl1:treex1:X.tr1:treeIHl1:forall s2 : tree, Ok l1 -> Ok s2 -> subset l1 s2 = true <-> Subset l1 s2IHr1:forall s2 : tree, Ok r1 -> Ok s2 -> subset r1 s2 = true <-> Subset r1 s2c2:Info.tl2:treex2:X.tr2:treeH5:Ok l2H6:Ok r2H7:lt_tree x2 l2H8:gt_tree x2 r2H4:Ok l1H9:Ok r1H10:lt_tree x1 l1H11:gt_tree x1 r1H:X.lt x1 x2subsetl (subset l1) x1 l2 &&& subset r1 (Node c2 l2 x2 r2) = true <-> Subset (Node c1 l1 x1 r1) (Node c2 l2 x2 r2)c1:Info.tl1:treex1:X.tr1:treeIHl1:forall s2 : tree, Ok l1 -> Ok s2 -> subset l1 s2 = true <-> Subset l1 s2IHr1:forall s2 : tree, Ok r1 -> Ok s2 -> subset r1 s2 = true <-> Subset r1 s2c2:Info.tl2:treex2:X.tr2:treeH5:Ok l2H6:Ok r2H7:lt_tree x2 l2H8:gt_tree x2 r2H4:Ok l1H9:Ok r1H10:lt_tree x1 l1H11:gt_tree x1 r1H:X.lt x2 x1subsetr (subset r1) x1 r2 &&& subset l1 (Node c2 l2 x2 r2) = true <-> Subset (Node c1 l1 x1 r1) (Node c2 l2 x2 r2)c1:Info.tl1:treex1:X.tr1:treeIHl1:forall s2 : tree, Ok l1 -> Ok s2 -> subset l1 s2 = true <-> Subset l1 s2IHr1:forall s2 : tree, Ok r1 -> Ok s2 -> subset r1 s2 = true <-> Subset r1 s2c2:Info.tl2:treex2:X.tr2:treeH5:Ok l2H6:Ok r2H7:lt_tree x2 l2H8:gt_tree x2 r2H4:Ok l1H9:Ok r1H10:lt_tree x1 l1H11:gt_tree x1 r1H:X.lt x1 x2subsetl (subset l1) x1 l2 &&& subset r1 (Node c2 l2 x2 r2) = true <-> Subset (Node c1 l1 x1 r1) (Node c2 l2 x2 r2)c1:Info.tl1:treex1:X.tr1:treeIHl1:forall s2 : tree, Ok l1 -> Ok s2 -> subset l1 s2 = true <-> Subset l1 s2IHr1:forall s2 : tree, Ok r1 -> Ok s2 -> subset r1 s2 = true <-> Subset r1 s2c2:Info.tl2:treex2:X.tr2:treeH5:Ok l2H6:Ok r2H7:lt_tree x2 l2H8:gt_tree x2 r2H4:Ok l1H9:Ok r1H10:lt_tree x1 l1H11:gt_tree x1 r1H:X.lt x2 x1subsetr (subset r1) x1 r2 &&& subset l1 (Node c2 l2 x2 r2) = true <-> Subset (Node c1 l1 x1 r1) (Node c2 l2 x2 r2)c1:Info.tl1:treex1:X.tr1:treeIHl1:forall s2 : tree, Ok l1 -> Ok s2 -> subset l1 s2 = true <-> Subset l1 s2IHr1:forall s2 : tree, Ok r1 -> Ok s2 -> subset r1 s2 = true <-> Subset r1 s2c2:Info.tl2:treex2:X.tr2:treeH5:Ok l2H6:Ok r2H7:lt_tree x2 l2H8:gt_tree x2 r2H4:Ok l1H9:Ok r1H10:lt_tree x1 l1H11:gt_tree x1 r1H:X.lt x1 x2subsetl (subset l1) x1 l2 = true /\ Subset r1 (Node c2 l2 x2 r2) <-> Subset (Node c1 l1 x1 r1) (Node c2 l2 x2 r2)c1:Info.tl1:treex1:X.tr1:treeIHl1:forall s2 : tree, Ok l1 -> Ok s2 -> subset l1 s2 = true <-> Subset l1 s2IHr1:forall s2 : tree, Ok r1 -> Ok s2 -> subset r1 s2 = true <-> Subset r1 s2c2:Info.tl2:treex2:X.tr2:treeH5:Ok l2H6:Ok r2H7:lt_tree x2 l2H8:gt_tree x2 r2H4:Ok l1H9:Ok r1H10:lt_tree x1 l1H11:gt_tree x1 r1H:X.lt x2 x1subsetr (subset r1) x1 r2 &&& subset l1 (Node c2 l2 x2 r2) = true <-> Subset (Node c1 l1 x1 r1) (Node c2 l2 x2 r2)c1:Info.tl1:treex1:X.tr1:treeIHl1:forall s2 : tree, Ok l1 -> Ok s2 -> subset l1 s2 = true <-> Subset l1 s2IHr1:forall s2 : tree, Ok r1 -> Ok s2 -> subset r1 s2 = true <-> Subset r1 s2c2:Info.tl2:treex2:X.tr2:treeH5:Ok l2H6:Ok r2H7:lt_tree x2 l2H8:gt_tree x2 r2H4:Ok l1H9:Ok r1H10:lt_tree x1 l1H11:gt_tree x1 r1H:X.lt x1 x2Subset (Node c1 l1 x1 Leaf) l2 /\ Subset r1 (Node c2 l2 x2 r2) <-> Subset (Node c1 l1 x1 r1) (Node c2 l2 x2 r2)c1:Info.tl1:treex1:X.tr1:treeIHl1:forall s2 : tree, Ok l1 -> Ok s2 -> subset l1 s2 = true <-> Subset l1 s2IHr1:forall s2 : tree, Ok r1 -> Ok s2 -> subset r1 s2 = true <-> Subset r1 s2c2:Info.tl2:treex2:X.tr2:treeH5:Ok l2H6:Ok r2H7:lt_tree x2 l2H8:gt_tree x2 r2H4:Ok l1H9:Ok r1H10:lt_tree x1 l1H11:gt_tree x1 r1H:X.lt x2 x1subsetr (subset r1) x1 r2 &&& subset l1 (Node c2 l2 x2 r2) = true <-> Subset (Node c1 l1 x1 r1) (Node c2 l2 x2 r2)c1:Info.tl1:treex1:X.tr1:treec2:Info.tl2:treex2:X.tr2:treeH5:Ok l2H6:Ok r2H7:lt_tree x2 l2H8:gt_tree x2 r2H4:Ok l1H9:Ok r1H10:lt_tree x1 l1H11:gt_tree x1 r1H:X.lt x1 x2Subset (Node c1 l1 x1 Leaf) l2 /\ Subset r1 (Node c2 l2 x2 r2) <-> Subset (Node c1 l1 x1 r1) (Node c2 l2 x2 r2)c1:Info.tl1:treex1:X.tr1:treeIHl1:forall s2 : tree, Ok l1 -> Ok s2 -> subset l1 s2 = true <-> Subset l1 s2IHr1:forall s2 : tree, Ok r1 -> Ok s2 -> subset r1 s2 = true <-> Subset r1 s2c2:Info.tl2:treex2:X.tr2:treeH5:Ok l2H6:Ok r2H7:lt_tree x2 l2H8:gt_tree x2 r2H4:Ok l1H9:Ok r1H10:lt_tree x1 l1H11:gt_tree x1 r1H:X.lt x2 x1subsetr (subset r1) x1 r2 &&& subset l1 (Node c2 l2 x2 r2) = true <-> Subset (Node c1 l1 x1 r1) (Node c2 l2 x2 r2)c1:Info.tl1:treex1:X.tr1:treec2:Info.tl2:treex2:X.tr2:treeH5:Ok l2H6:Ok r2H7:lt_tree x2 l2H8:gt_tree x2 r2H4:Ok l1H9:Ok r1H10:lt_tree x1 l1H11:gt_tree x1 r1H:X.lt x1 x2H0:forall a0 : elt, InT a0 (Node c1 l1 x1 r1) -> InT a0 (Node c2 l2 x2 r2)a:eltH3:X.eq a x1InT a l2c1:Info.tl1:treex1:X.tr1:treec2:Info.tl2:treex2:X.tr2:treeH5:Ok l2H6:Ok r2H7:lt_tree x2 l2H8:gt_tree x2 r2H4:Ok l1H9:Ok r1H10:lt_tree x1 l1H11:gt_tree x1 r1H:X.lt x1 x2H0:forall a0 : elt, InT a0 (Node c1 l1 x1 r1) -> InT a0 (Node c2 l2 x2 r2)a:eltH3:InT a l1InT a l2c1:Info.tl1:treex1:X.tr1:treeIHl1:forall s2 : tree, Ok l1 -> Ok s2 -> subset l1 s2 = true <-> Subset l1 s2IHr1:forall s2 : tree, Ok r1 -> Ok s2 -> subset r1 s2 = true <-> Subset r1 s2c2:Info.tl2:treex2:X.tr2:treeH5:Ok l2H6:Ok r2H7:lt_tree x2 l2H8:gt_tree x2 r2H4:Ok l1H9:Ok r1H10:lt_tree x1 l1H11:gt_tree x1 r1H:X.lt x2 x1subsetr (subset r1) x1 r2 &&& subset l1 (Node c2 l2 x2 r2) = true <-> Subset (Node c1 l1 x1 r1) (Node c2 l2 x2 r2)c1:Info.tl1:treex1:X.tr1:treec2:Info.tl2:treex2:X.tr2:treeH5:Ok l2H6:Ok r2H7:lt_tree x2 l2H8:gt_tree x2 r2H4:Ok l1H9:Ok r1H10:lt_tree x1 l1H11:gt_tree x1 r1H:X.lt x1 x2H0:forall a0 : elt, InT a0 (Node c1 l1 x1 r1) -> InT a0 (Node c2 l2 x2 r2)a:eltH3:InT a l1InT a l2c1:Info.tl1:treex1:X.tr1:treeIHl1:forall s2 : tree, Ok l1 -> Ok s2 -> subset l1 s2 = true <-> Subset l1 s2IHr1:forall s2 : tree, Ok r1 -> Ok s2 -> subset r1 s2 = true <-> Subset r1 s2c2:Info.tl2:treex2:X.tr2:treeH5:Ok l2H6:Ok r2H7:lt_tree x2 l2H8:gt_tree x2 r2H4:Ok l1H9:Ok r1H10:lt_tree x1 l1H11:gt_tree x1 r1H:X.lt x2 x1subsetr (subset r1) x1 r2 &&& subset l1 (Node c2 l2 x2 r2) = true <-> Subset (Node c1 l1 x1 r1) (Node c2 l2 x2 r2)c1:Info.tl1:treex1:X.tr1:treeIHl1:forall s2 : tree, Ok l1 -> Ok s2 -> subset l1 s2 = true <-> Subset l1 s2IHr1:forall s2 : tree, Ok r1 -> Ok s2 -> subset r1 s2 = true <-> Subset r1 s2c2:Info.tl2:treex2:X.tr2:treeH5:Ok l2H6:Ok r2H7:lt_tree x2 l2H8:gt_tree x2 r2H4:Ok l1H9:Ok r1H10:lt_tree x1 l1H11:gt_tree x1 r1H:X.lt x2 x1subsetr (subset r1) x1 r2 &&& subset l1 (Node c2 l2 x2 r2) = true <-> Subset (Node c1 l1 x1 r1) (Node c2 l2 x2 r2)c1:Info.tl1:treex1:X.tr1:treeIHl1:forall s2 : tree, Ok l1 -> Ok s2 -> subset l1 s2 = true <-> Subset l1 s2IHr1:forall s2 : tree, Ok r1 -> Ok s2 -> subset r1 s2 = true <-> Subset r1 s2c2:Info.tl2:treex2:X.tr2:treeH5:Ok l2H6:Ok r2H7:lt_tree x2 l2H8:gt_tree x2 r2H4:Ok l1H9:Ok r1H10:lt_tree x1 l1H11:gt_tree x1 r1H:X.lt x2 x1subsetr (subset r1) x1 r2 = true /\ Subset l1 (Node c2 l2 x2 r2) <-> Subset (Node c1 l1 x1 r1) (Node c2 l2 x2 r2)c1:Info.tl1:treex1:X.tr1:treeIHl1:forall s2 : tree, Ok l1 -> Ok s2 -> subset l1 s2 = true <-> Subset l1 s2IHr1:forall s2 : tree, Ok r1 -> Ok s2 -> subset r1 s2 = true <-> Subset r1 s2c2:Info.tl2:treex2:X.tr2:treeH5:Ok l2H6:Ok r2H7:lt_tree x2 l2H8:gt_tree x2 r2H4:Ok l1H9:Ok r1H10:lt_tree x1 l1H11:gt_tree x1 r1H:X.lt x2 x1Subset (Node c1 Leaf x1 r1) r2 /\ Subset l1 (Node c2 l2 x2 r2) <-> Subset (Node c1 l1 x1 r1) (Node c2 l2 x2 r2)c1:Info.tl1:treex1:X.tr1:treec2:Info.tl2:treex2:X.tr2:treeH5:Ok l2H6:Ok r2H7:lt_tree x2 l2H8:gt_tree x2 r2H4:Ok l1H9:Ok r1H10:lt_tree x1 l1H11:gt_tree x1 r1H:X.lt x2 x1Subset (Node c1 Leaf x1 r1) r2 /\ Subset l1 (Node c2 l2 x2 r2) <-> Subset (Node c1 l1 x1 r1) (Node c2 l2 x2 r2)c1:Info.tl1:treex1:X.tr1:treec2:Info.tl2:treex2:X.tr2:treeH5:Ok l2H6:Ok r2H7:lt_tree x2 l2H8:gt_tree x2 r2H4:Ok l1H9:Ok r1H10:lt_tree x1 l1H11:gt_tree x1 r1H:X.lt x2 x1H0:forall a0 : elt, InT a0 (Node c1 l1 x1 r1) -> InT a0 (Node c2 l2 x2 r2)a:eltH3:X.eq a x1InT a r2c1:Info.tl1:treex1:X.tr1:treec2:Info.tl2:treex2:X.tr2:treeH5:Ok l2H6:Ok r2H7:lt_tree x2 l2H8:gt_tree x2 r2H4:Ok l1H9:Ok r1H10:lt_tree x1 l1H11:gt_tree x1 r1H:X.lt x2 x1H0:forall a0 : elt, InT a0 (Node c1 l1 x1 r1) -> InT a0 (Node c2 l2 x2 r2)a:eltH3:InT a r1InT a r2assert (InT a (Node c2 l2 x2 r2)) by auto; intuition_in; order. Qed.c1:Info.tl1:treex1:X.tr1:treec2:Info.tl2:treex2:X.tr2:treeH5:Ok l2H6:Ok r2H7:lt_tree x2 l2H8:gt_tree x2 r2H4:Ok l1H9:Ok r1H10:lt_tree x1 l1H11:gt_tree x1 r1H:X.lt x2 x1H0:forall a0 : elt, InT a0 (Node c1 l1 x1 r1) -> InT a0 (Node c2 l2 x2 r2)a:eltH3:InT a r1InT a r2
Relations eq and lt over trees
Module L := MSetInterface.MakeListOrdering X. Definition eq := Equal.Equivalence eqfirstorder. Qed.Equivalence eqforall s s' : tree, eq s s' <-> L.eq (elements s) (elements s')forall s s' : tree, eq s s' <-> L.eq (elements s) (elements s')s, s':tree(forall a : elt, InT a s <-> InT a s') <-> (forall x : X.t, InA X.eq x (elements s) <-> InA X.eq x (elements s'))firstorder. Qed. Definition lt (s1 s2 : tree) : Prop := exists s1' s2', Ok s1' /\ Ok s2' /\ eq s1 s1' /\ eq s2 s2' /\ L.lt (elements s1') (elements s2'). Declare Equivalent Keys L.eq equivlistA.s, s':tree(forall a : elt, InT a s <-> InT a s') <-> (forall x : X.t, InT x s <-> InT x s')StrictOrder ltStrictOrder ltIrreflexive ltTransitive lts, s1, s2:treeB1:Ok s1B2:Ok s2E1:eq s s1E2:eq s s2L:L.lt (elements s1) (elements s2)FalseTransitive lts, s1, s2:treeB1:Ok s1B2:Ok s2E1:eq s s1E2:eq s s2L:L.lt (elements s1) (elements s2)eqlistA X.eq (elements s1) (elements s2)s, s1, s2:treeB1:Ok s1B2:Ok s2E1:eq s s1E2:eq s s2L:L.lt (elements s1) (elements s2)H:eqlistA X.eq (elements s1) (elements s2)FalseTransitive lts, s1, s2:treeB1:Ok s1B2:Ok s2E1:eq s s1E2:eq s s2L:L.lt (elements s1) (elements s2)equivlistA X.eq (elements s1) (elements s2)s, s1, s2:treeB1:Ok s1B2:Ok s2E1:eq s s1E2:eq s s2L:L.lt (elements s1) (elements s2)H:eqlistA X.eq (elements s1) (elements s2)FalseTransitive lts, s1, s2:treeB1:Ok s1B2:Ok s2E1:eq s s1E2:eq s s2L:L.lt (elements s1) (elements s2)eq s1 s2s, s1, s2:treeB1:Ok s1B2:Ok s2E1:eq s s1E2:eq s s2L:L.lt (elements s1) (elements s2)H:eqlistA X.eq (elements s1) (elements s2)FalseTransitive lts, s1, s2:treeB1:Ok s1B2:Ok s2E1:eq s s1E2:eq s s2L:L.lt (elements s1) (elements s2)eq s1 ss, s1, s2:treeB1:Ok s1B2:Ok s2E1:eq s s1E2:eq s s2L:L.lt (elements s1) (elements s2)H:eqlistA X.eq (elements s1) (elements s2)FalseTransitive lts, s1, s2:treeB1:Ok s1B2:Ok s2E1:eq s s1E2:eq s s2L:L.lt (elements s1) (elements s2)H:eqlistA X.eq (elements s1) (elements s2)FalseTransitive lts, s1, s2:treeB1:Ok s1B2:Ok s2E1:eq s s1E2:eq s s2L:L.lt (elements s2) (elements s2)H:eqlistA X.eq (elements s1) (elements s2)FalseTransitive ltTransitive lts1, s2, s3, s1', s2':treeB1:Ok s1'B2:Ok s2'E1:eq s1 s1'E2:eq s2 s2'L12:L.lt (elements s1') (elements s2')s2'', s3':treeB2':Ok s2''B3:Ok s3'E2':eq s2 s2''E3:eq s3 s3'L23:L.lt (elements s2'') (elements s3')lt s1 s3s1, s2, s3, s1', s2':treeB1:Ok s1'B2:Ok s2'E1:eq s1 s1'E2:eq s2 s2'L12:L.lt (elements s1') (elements s2')s2'', s3':treeB2':Ok s2''B3:Ok s3'E2':eq s2 s2''E3:eq s3 s3'L23:L.lt (elements s2'') (elements s3')L.lt (elements s1') (elements s3')s1, s2, s3, s1', s2':treeB1:Ok s1'B2:Ok s2'E1:eq s1 s1'E2:eq s2 s2'L12:L.lt (elements s1') (elements s2')s2'', s3':treeB2':Ok s2''B3:Ok s3'E2':eq s2 s2''E3:eq s3 s3'L23:L.lt (elements s2'') (elements s3')eqlistA X.eq (elements s2') (elements s2'')s1, s2, s3, s1', s2':treeB1:Ok s1'B2:Ok s2'E1:eq s1 s1'E2:eq s2 s2'L12:L.lt (elements s1') (elements s2')s2'', s3':treeB2':Ok s2''B3:Ok s3'E2':eq s2 s2''E3:eq s3 s3'L23:L.lt (elements s2'') (elements s3')H:eqlistA X.eq (elements s2') (elements s2'')L.lt (elements s1') (elements s3')s1, s2, s3, s1', s2':treeB1:Ok s1'B2:Ok s2'E1:eq s1 s1'E2:eq s2 s2'L12:L.lt (elements s1') (elements s2')s2'', s3':treeB2':Ok s2''B3:Ok s3'E2':eq s2 s2''E3:eq s3 s3'L23:L.lt (elements s2'') (elements s3')equivlistA X.eq (elements s2') (elements s2'')s1, s2, s3, s1', s2':treeB1:Ok s1'B2:Ok s2'E1:eq s1 s1'E2:eq s2 s2'L12:L.lt (elements s1') (elements s2')s2'', s3':treeB2':Ok s2''B3:Ok s3'E2':eq s2 s2''E3:eq s3 s3'L23:L.lt (elements s2'') (elements s3')H:eqlistA X.eq (elements s2') (elements s2'')L.lt (elements s1') (elements s3')s1, s2, s3, s1', s2':treeB1:Ok s1'B2:Ok s2'E1:eq s1 s1'E2:eq s2 s2'L12:L.lt (elements s1') (elements s2')s2'', s3':treeB2':Ok s2''B3:Ok s3'E2':eq s2 s2''E3:eq s3 s3'L23:L.lt (elements s2'') (elements s3')eq s2' s2''s1, s2, s3, s1', s2':treeB1:Ok s1'B2:Ok s2'E1:eq s1 s1'E2:eq s2 s2'L12:L.lt (elements s1') (elements s2')s2'', s3':treeB2':Ok s2''B3:Ok s3'E2':eq s2 s2''E3:eq s3 s3'L23:L.lt (elements s2'') (elements s3')H:eqlistA X.eq (elements s2') (elements s2'')L.lt (elements s1') (elements s3')s1, s2, s3, s1', s2':treeB1:Ok s1'B2:Ok s2'E1:eq s1 s1'E2:eq s2 s2'L12:L.lt (elements s1') (elements s2')s2'', s3':treeB2':Ok s2''B3:Ok s3'E2':eq s2 s2''E3:eq s3 s3'L23:L.lt (elements s2'') (elements s3')eq s2' s2s1, s2, s3, s1', s2':treeB1:Ok s1'B2:Ok s2'E1:eq s1 s1'E2:eq s2 s2'L12:L.lt (elements s1') (elements s2')s2'', s3':treeB2':Ok s2''B3:Ok s3'E2':eq s2 s2''E3:eq s3 s3'L23:L.lt (elements s2'') (elements s3')H:eqlistA X.eq (elements s2') (elements s2'')L.lt (elements s1') (elements s3')s1, s2, s3, s1', s2':treeB1:Ok s1'B2:Ok s2'E1:eq s1 s1'E2:eq s2 s2'L12:L.lt (elements s1') (elements s2')s2'', s3':treeB2':Ok s2''B3:Ok s3'E2':eq s2 s2''E3:eq s3 s3'L23:L.lt (elements s2'') (elements s3')H:eqlistA X.eq (elements s2') (elements s2'')L.lt (elements s1') (elements s3')rewrite H; auto. Qed.s1, s2, s3, s1', s2':treeB1:Ok s1'B2:Ok s2'E1:eq s1 s1'E2:eq s2 s2'L12:L.lt (elements s1') (elements s2')s2'', s3':treeB2':Ok s2''B3:Ok s3'E2':eq s2 s2''E3:eq s3 s3'L23:L.lt (elements s2'') (elements s3')H:eqlistA X.eq (elements s2') (elements s2'')L.lt (elements s2') (elements s3')Proper (eq ==> eq ==> iff) ltProper (eq ==> eq ==> iff) lts1, s2:treeE12:eq s1 s2s3, s4:treeE34:eq s3 s4lt s1 s3 <-> lt s2 s4s1, s2:treeE12:eq s1 s2s3, s4:treeE34:eq s3 s4lt s1 s3 -> lt s2 s4s1, s2:treeE12:eq s1 s2s3, s4:treeE34:eq s3 s4lt s2 s4 -> lt s1 s3s1, s2:treeE12:eq s1 s2s3, s4:treeE34:eq s3 s4s1', s3':treeB1:Ok s1'B3:Ok s3'E1:eq s1 s1'E3:eq s3 s3'LT:L.lt (elements s1') (elements s3')lt s2 s4s1, s2:treeE12:eq s1 s2s3, s4:treeE34:eq s3 s4lt s2 s4 -> lt s1 s3s1, s2:treeE12:eq s1 s2s3, s4:treeE34:eq s3 s4s1', s3':treeB1:Ok s1'B3:Ok s3'E1:eq s1 s1'E3:eq s3 s3'LT:L.lt (elements s1') (elements s3')eq s2 s1' /\ eq s4 s3' /\ L.lt (elements s1') (elements s3')s1, s2:treeE12:eq s1 s2s3, s4:treeE34:eq s3 s4lt s2 s4 -> lt s1 s3s1, s2:treeE12:eq s1 s2s3, s4:treeE34:eq s3 s4s1', s3':treeB1:Ok s1'B3:Ok s3'E1:eq s1 s1'E3:eq s3 s3'LT:L.lt (elements s1') (elements s3')eq s2 s1's1, s2:treeE12:eq s1 s2s3, s4:treeE34:eq s3 s4s1', s3':treeB1:Ok s1'B3:Ok s3'E1:eq s1 s1'E3:eq s3 s3'LT:L.lt (elements s1') (elements s3')eq s4 s3' /\ L.lt (elements s1') (elements s3')s1, s2:treeE12:eq s1 s2s3, s4:treeE34:eq s3 s4lt s2 s4 -> lt s1 s3s1, s2:treeE12:eq s1 s2s3, s4:treeE34:eq s3 s4s1', s3':treeB1:Ok s1'B3:Ok s3'E1:eq s1 s1'E3:eq s3 s3'LT:L.lt (elements s1') (elements s3')eq s2 s1s1, s2:treeE12:eq s1 s2s3, s4:treeE34:eq s3 s4s1', s3':treeB1:Ok s1'B3:Ok s3'E1:eq s1 s1'E3:eq s3 s3'LT:L.lt (elements s1') (elements s3')eq s4 s3' /\ L.lt (elements s1') (elements s3')s1, s2:treeE12:eq s1 s2s3, s4:treeE34:eq s3 s4lt s2 s4 -> lt s1 s3s1, s2:treeE12:eq s1 s2s3, s4:treeE34:eq s3 s4s1', s3':treeB1:Ok s1'B3:Ok s3'E1:eq s1 s1'E3:eq s3 s3'LT:L.lt (elements s1') (elements s3')eq s4 s3' /\ L.lt (elements s1') (elements s3')s1, s2:treeE12:eq s1 s2s3, s4:treeE34:eq s3 s4lt s2 s4 -> lt s1 s3s1, s2:treeE12:eq s1 s2s3, s4:treeE34:eq s3 s4s1', s3':treeB1:Ok s1'B3:Ok s3'E1:eq s1 s1'E3:eq s3 s3'LT:L.lt (elements s1') (elements s3')eq s4 s3's1, s2:treeE12:eq s1 s2s3, s4:treeE34:eq s3 s4lt s2 s4 -> lt s1 s3s1, s2:treeE12:eq s1 s2s3, s4:treeE34:eq s3 s4s1', s3':treeB1:Ok s1'B3:Ok s3'E1:eq s1 s1'E3:eq s3 s3'LT:L.lt (elements s1') (elements s3')eq s4 s3s1, s2:treeE12:eq s1 s2s3, s4:treeE34:eq s3 s4lt s2 s4 -> lt s1 s3s1, s2:treeE12:eq s1 s2s3, s4:treeE34:eq s3 s4lt s2 s4 -> lt s1 s3s1, s2:treeE12:eq s1 s2s3, s4:treeE34:eq s3 s4s1', s3':treeB1:Ok s1'B3:Ok s3'E1:eq s2 s1'E3:eq s4 s3'LT:L.lt (elements s1') (elements s3')lt s1 s3s1, s2:treeE12:eq s1 s2s3, s4:treeE34:eq s3 s4s1', s3':treeB1:Ok s1'B3:Ok s3'E1:eq s2 s1'E3:eq s4 s3'LT:L.lt (elements s1') (elements s3')eq s1 s1' /\ eq s3 s3' /\ L.lt (elements s1') (elements s3')s1, s2:treeE12:eq s1 s2s3, s4:treeE34:eq s3 s4s1', s3':treeB1:Ok s1'B3:Ok s3'E1:eq s2 s1'E3:eq s4 s3'LT:L.lt (elements s1') (elements s3')eq s1 s1's1, s2:treeE12:eq s1 s2s3, s4:treeE34:eq s3 s4s1', s3':treeB1:Ok s1'B3:Ok s3'E1:eq s2 s1'E3:eq s4 s3'LT:L.lt (elements s1') (elements s3')eq s3 s3' /\ L.lt (elements s1') (elements s3')s1, s2:treeE12:eq s1 s2s3, s4:treeE34:eq s3 s4s1', s3':treeB1:Ok s1'B3:Ok s3'E1:eq s2 s1'E3:eq s4 s3'LT:L.lt (elements s1') (elements s3')eq s3 s3' /\ L.lt (elements s1') (elements s3')transitivity s4; auto. Qed.s1, s2:treeE12:eq s1 s2s3, s4:treeE34:eq s3 s4s1', s3':treeB1:Ok s1'B3:Ok s3'E1:eq s2 s1'E3:eq s4 s3'LT:L.lt (elements s1') (elements s3')eq s3 s3'
Proof of the comparison algorithm
flatten_e e returns the list of elements of e i.e. the list
of elements actually compared
Fixpoint flatten_e (e : enumeration) : list elt := match e with | End => nil | More x t r => x :: elements t ++ flatten_e r end.forall (l : tree) (x : elt) (r : tree) (c : Info.t) (e : enumeration), elements l ++ flatten_e (More x r e) = elements (Node c l x r) ++ flatten_e eforall (l : tree) (x : elt) (r : tree) (c : Info.t) (e : enumeration), elements l ++ flatten_e (More x r e) = elements (Node c l x r) ++ flatten_e enow rewrite elements_node, app_ass. Qed.l:treex:eltr:treec:Info.te:enumerationelements l ++ flatten_e (More x r e) = elements (Node c l x r) ++ flatten_e eforall (s : tree) (e : enumeration), flatten_e (cons s e) = elements s ++ flatten_e eforall (s : tree) (e : enumeration), flatten_e (cons s e) = elements s ++ flatten_e erewrite IHs1; apply flatten_e_elements. Qed.t:Info.ts1:treet0:X.ts2:treeIHs1:forall e0 : enumeration, flatten_e (cons s1 e0) = elements s1 ++ flatten_e e0IHs2:forall e0 : enumeration, flatten_e (cons s2 e0) = elements s2 ++ flatten_e e0e:enumerationflatten_e (cons s1 (More t0 s2 e)) = elements (Node t s1 t0 s2) ++ flatten_e e
Correctness of this comparison
Definition Cmp c x y := CompSpec L.eq L.lt x y c. Local Hint Unfold Cmp flip : core.forall e2 : enumeration, Cmp (compare_end e2) nil (flatten_e e2)forall e2 : enumeration, Cmp (compare_end e2) nil (flatten_e e2)reflexivity. Qed.L.eq nil nilforall (x1 : X.t) (cont : enumeration -> comparison) (x2 : elt) (r2 : tree) (e2 : enumeration) (l : list X.t), Cmp (cont (cons r2 e2)) l (elements r2 ++ flatten_e e2) -> Cmp (compare_more x1 cont (More x2 r2 e2)) (x1 :: l) (flatten_e (More x2 r2 e2))simpl; intros; elim_compare x1 x2; simpl; red; auto. Qed.forall (x1 : X.t) (cont : enumeration -> comparison) (x2 : elt) (r2 : tree) (e2 : enumeration) (l : list X.t), Cmp (cont (cons r2 e2)) l (elements r2 ++ flatten_e e2) -> Cmp (compare_more x1 cont (More x2 r2 e2)) (x1 :: l) (flatten_e (More x2 r2 e2))forall (s1 : tree) (cont : enumeration -> comparison) (e2 : enumeration) (l : list X.t), (forall e : enumeration, Cmp (cont e) l (flatten_e e)) -> Cmp (compare_cont s1 cont e2) (elements s1 ++ l) (flatten_e e2)forall (s1 : tree) (cont : enumeration -> comparison) (e2 : enumeration) (l : list X.t), (forall e : enumeration, Cmp (cont e) l (flatten_e e)) -> Cmp (compare_cont s1 cont e2) (elements s1 ++ l) (flatten_e e2)c1:Info.tl1:treex1:X.tr1:treeHl1:forall (cont0 : enumeration -> comparison) (e0 : enumeration) (l0 : list X.t), (forall e : enumeration, Cmp (cont0 e) l0 (flatten_e e)) -> Cmp (compare_cont l1 cont0 e0) (elements l1 ++ l0) (flatten_e e0)Hr1:forall (cont0 : enumeration -> comparison) (e0 : enumeration) (l0 : list X.t), (forall e : enumeration, Cmp (cont0 e) l0 (flatten_e e)) -> Cmp (compare_cont r1 cont0 e0) (elements r1 ++ l0) (flatten_e e0)cont:enumeration -> comparisone2:enumerationl:list X.tH:forall e : enumeration, Cmp (cont e) l (flatten_e e)Cmp (compare_cont (Node c1 l1 x1 r1) cont e2) (elements (Node c1 l1 x1 r1) ++ l) (flatten_e e2)c1:Info.tl1:treex1:X.tr1:treeHl1:forall (cont0 : enumeration -> comparison) (e0 : enumeration) (l0 : list X.t), (forall e : enumeration, Cmp (cont0 e) l0 (flatten_e e)) -> Cmp (compare_cont l1 cont0 e0) (elements l1 ++ l0) (flatten_e e0)Hr1:forall (cont0 : enumeration -> comparison) (e0 : enumeration) (l0 : list X.t), (forall e : enumeration, Cmp (cont0 e) l0 (flatten_e e)) -> Cmp (compare_cont r1 cont0 e0) (elements r1 ++ l0) (flatten_e e0)cont:enumeration -> comparisone2:enumerationl:list X.tH:forall e : enumeration, Cmp (cont e) l (flatten_e e)Cmp (compare_cont l1 (compare_more x1 (compare_cont r1 cont)) e2) (elements l1 ++ x1 :: elements r1 ++ l) (flatten_e e2)c1:Info.tl1:treex1:X.tr1:treeHl1:forall (cont0 : enumeration -> comparison) (e0 : enumeration) (l0 : list X.t), (forall e : enumeration, Cmp (cont0 e) l0 (flatten_e e)) -> Cmp (compare_cont l1 cont0 e0) (elements l1 ++ l0) (flatten_e e0)Hr1:forall (cont0 : enumeration -> comparison) (e0 : enumeration) (l0 : list X.t), (forall e : enumeration, Cmp (cont0 e) l0 (flatten_e e)) -> Cmp (compare_cont r1 cont0 e0) (elements r1 ++ l0) (flatten_e e0)cont:enumeration -> comparisone2:enumerationl:list X.tH:forall e : enumeration, Cmp (cont e) l (flatten_e e)forall e : enumeration, Cmp (compare_more x1 (compare_cont r1 cont) e) (x1 :: elements r1 ++ l) (flatten_e e)c1:Info.tl1:treex1:X.tr1:treeHl1:forall (cont0 : enumeration -> comparison) (e2 : enumeration) (l0 : list X.t), (forall e : enumeration, Cmp (cont0 e) l0 (flatten_e e)) -> Cmp (compare_cont l1 cont0 e2) (elements l1 ++ l0) (flatten_e e2)Hr1:forall (cont0 : enumeration -> comparison) (e2 : enumeration) (l0 : list X.t), (forall e : enumeration, Cmp (cont0 e) l0 (flatten_e e)) -> Cmp (compare_cont r1 cont0 e2) (elements r1 ++ l0) (flatten_e e2)cont:enumeration -> comparisonl:list X.tH:forall e : enumeration, Cmp (cont e) l (flatten_e e)forall e : enumeration, Cmp (compare_more x1 (compare_cont r1 cont) e) (x1 :: elements r1 ++ l) (flatten_e e)c1:Info.tl1:treex1:X.tr1:treeHl1:forall (cont0 : enumeration -> comparison) (e2 : enumeration) (l0 : list X.t), (forall e : enumeration, Cmp (cont0 e) l0 (flatten_e e)) -> Cmp (compare_cont l1 cont0 e2) (elements l1 ++ l0) (flatten_e e2)Hr1:forall (cont0 : enumeration -> comparison) (e2 : enumeration) (l0 : list X.t), (forall e : enumeration, Cmp (cont0 e) l0 (flatten_e e)) -> Cmp (compare_cont r1 cont0 e2) (elements r1 ++ l0) (flatten_e e2)cont:enumeration -> comparisonl:list X.tH:forall e : enumeration, Cmp (cont e) l (flatten_e e)Cmp (compare_more x1 (compare_cont r1 cont) End) (x1 :: elements r1 ++ l) (flatten_e End)c1:Info.tl1:treex1:X.tr1:treeHl1:forall (cont0 : enumeration -> comparison) (e0 : enumeration) (l0 : list X.t), (forall e : enumeration, Cmp (cont0 e) l0 (flatten_e e)) -> Cmp (compare_cont l1 cont0 e0) (elements l1 ++ l0) (flatten_e e0)Hr1:forall (cont0 : enumeration -> comparison) (e0 : enumeration) (l0 : list X.t), (forall e : enumeration, Cmp (cont0 e) l0 (flatten_e e)) -> Cmp (compare_cont r1 cont0 e0) (elements r1 ++ l0) (flatten_e e0)cont:enumeration -> comparisonl:list X.tH:forall e : enumeration, Cmp (cont e) l (flatten_e e)x2:eltr2:treee2:enumerationCmp (compare_more x1 (compare_cont r1 cont) (More x2 r2 e2)) (x1 :: elements r1 ++ l) (flatten_e (More x2 r2 e2))c1:Info.tl1:treex1:X.tr1:treeHl1:forall (cont0 : enumeration -> comparison) (e0 : enumeration) (l0 : list X.t), (forall e : enumeration, Cmp (cont0 e) l0 (flatten_e e)) -> Cmp (compare_cont l1 cont0 e0) (elements l1 ++ l0) (flatten_e e0)Hr1:forall (cont0 : enumeration -> comparison) (e0 : enumeration) (l0 : list X.t), (forall e : enumeration, Cmp (cont0 e) l0 (flatten_e e)) -> Cmp (compare_cont r1 cont0 e0) (elements r1 ++ l0) (flatten_e e0)cont:enumeration -> comparisonl:list X.tH:forall e : enumeration, Cmp (cont e) l (flatten_e e)x2:eltr2:treee2:enumerationCmp (compare_more x1 (compare_cont r1 cont) (More x2 r2 e2)) (x1 :: elements r1 ++ l) (flatten_e (More x2 r2 e2))rewrite <- cons_1; auto. Qed.c1:Info.tl1:treex1:X.tr1:treeHl1:forall (cont0 : enumeration -> comparison) (e0 : enumeration) (l0 : list X.t), (forall e : enumeration, Cmp (cont0 e) l0 (flatten_e e)) -> Cmp (compare_cont l1 cont0 e0) (elements l1 ++ l0) (flatten_e e0)Hr1:forall (cont0 : enumeration -> comparison) (e0 : enumeration) (l0 : list X.t), (forall e : enumeration, Cmp (cont0 e) l0 (flatten_e e)) -> Cmp (compare_cont r1 cont0 e0) (elements r1 ++ l0) (flatten_e e0)cont:enumeration -> comparisonl:list X.tH:forall e : enumeration, Cmp (cont e) l (flatten_e e)x2:eltr2:treee2:enumerationCmp (compare_cont r1 cont (cons r2 e2)) (elements r1 ++ l) (elements r2 ++ flatten_e e2)forall s1 s2 : tree, Cmp (compare s1 s2) (elements s1) (elements s2)forall s1 s2 : tree, Cmp (compare s1 s2) (elements s1) (elements s2)s1, s2:treeCmp (compare_cont s1 compare_end (cons s2 End)) (elements s1) (elements s2)s1, s2:treeCmp (compare_cont s1 compare_end (cons s2 End)) (elements s1 ++ nil) (elements s2)s1, s2:treeCmp (compare_cont s1 compare_end (cons s2 End)) (elements s1 ++ nil) (flatten_e (cons s2 End))s1, s2:treeforall e : enumeration, Cmp (compare_end e) nil (flatten_e e)apply compare_end_Cmp; auto. Qed.s1, s2:treee:enumerationCmp (compare_end e) nil (flatten_e e)forall s1 s2 : tree, Ok s1 -> Ok s2 -> CompSpec eq lt s1 s2 (compare s1 s2)forall s1 s2 : tree, Ok s1 -> Ok s2 -> CompSpec eq lt s1 s2 (compare s1 s2)s1, s2:treeH:Ok s1H0:Ok s2CompSpec eq lt s1 s2 (compare s1 s2)s1, s2:treeH:Ok s1H0:Ok s2H1:L.eq (elements s1) (elements s2)eq s1 s2s1, s2:treeH:Ok s1H0:Ok s2H1:L.lt (elements s1) (elements s2)lt s1 s2s1, s2:treeH:Ok s1H0:Ok s2H1:L.lt (elements s2) (elements s1)lt s2 s1s1, s2:treeH:Ok s1H0:Ok s2H1:L.lt (elements s1) (elements s2)lt s1 s2s1, s2:treeH:Ok s1H0:Ok s2H1:L.lt (elements s2) (elements s1)lt s2 s1intros; exists s2, s1; repeat split; auto. Qed.s1, s2:treeH:Ok s1H0:Ok s2H1:L.lt (elements s2) (elements s1)lt s2 s1
forall s1 s2 : tree, Ok s1 -> Ok s2 -> equal s1 s2 = true <-> eq s1 s2forall s1 s2 : tree, Ok s1 -> Ok s2 -> equal s1 s2 = true <-> eq s1 s2s1, s2:treeB1:Ok s1B2:Ok s2match compare s1 s2 with | Eq => true | _ => false end = true <-> eq s1 s2s1, s2:treeB1:Ok s1B2:Ok s2H:lt s1 s2H':eq s1 s2false = trues1, s2:treeB1:Ok s1B2:Ok s2H:lt s2 s1H':eq s1 s2false = trues1, s2:treeB1:Ok s1B2:Ok s2H:lt s2 s2H':eq s1 s2false = trues1, s2:treeB1:Ok s1B2:Ok s2H:lt s2 s1H':eq s1 s2false = trues1, s2:treeB1:Ok s1B2:Ok s2H:lt s2 s1H':eq s1 s2false = trueelim (StrictOrder_Irreflexive s2); auto. Qed.s1, s2:treeB1:Ok s1B2:Ok s2H:lt s2 s2H':eq s1 s2false = true
s:treemindepth s <= maxdepth ss:treemindepth s <= maxdepth st:Info.ts1:treet0:X.ts2:treeIHs1:mindepth s1 <= maxdepth s1IHs2:mindepth s2 <= maxdepth s2S (Init.Nat.min (mindepth s1) (mindepth s2)) <= S (Init.Nat.max (maxdepth s1) (maxdepth s2))t:Info.ts1:treet0:X.ts2:treeIHs1:mindepth s1 <= maxdepth s1IHs2:mindepth s2 <= maxdepth s2Init.Nat.min (mindepth s1) (mindepth s2) <= Init.Nat.max (maxdepth s1) (maxdepth s2)t:Info.ts1:treet0:X.ts2:treeIHs1:mindepth s1 <= maxdepth s1IHs2:mindepth s2 <= maxdepth s2Init.Nat.min (mindepth s1) (mindepth s2) <= mindepth s1t:Info.ts1:treet0:X.ts2:treeIHs1:mindepth s1 <= maxdepth s1IHs2:mindepth s2 <= maxdepth s2mindepth s1 <= Init.Nat.max (maxdepth s1) (maxdepth s2)t:Info.ts1:treet0:X.ts2:treeIHs1:mindepth s1 <= maxdepth s1IHs2:mindepth s2 <= maxdepth s2mindepth s1 <= Init.Nat.max (maxdepth s1) (maxdepth s2)t:Info.ts1:treet0:X.ts2:treeIHs1:mindepth s1 <= maxdepth s1IHs2:mindepth s2 <= maxdepth s2mindepth s1 <= maxdepth s1t:Info.ts1:treet0:X.ts2:treeIHs1:mindepth s1 <= maxdepth s1IHs2:mindepth s2 <= maxdepth s2maxdepth s1 <= Init.Nat.max (maxdepth s1) (maxdepth s2)apply Nat.le_max_l. Qed.t:Info.ts1:treet0:X.ts2:treeIHs1:mindepth s1 <= maxdepth s1IHs2:mindepth s2 <= maxdepth s2maxdepth s1 <= Init.Nat.max (maxdepth s1) (maxdepth s2)s:treecardinal s < 2 ^ maxdepth ss:treecardinal s < 2 ^ maxdepth ss:treeS (cardinal s) <= 2 ^ maxdepth sS (cardinal Leaf) <= 2 ^ maxdepth Leafc:Info.tl:treex:X.tr:treeIHl:S (cardinal l) <= 2 ^ maxdepth lIHr:S (cardinal r) <= 2 ^ maxdepth rS (cardinal (Node c l x r)) <= 2 ^ maxdepth (Node c l x r)auto.S (cardinal Leaf) <= 2 ^ maxdepth Leafc:Info.tl:treex:X.tr:treeIHl:S (cardinal l) <= 2 ^ maxdepth lIHr:S (cardinal r) <= 2 ^ maxdepth rS (cardinal (Node c l x r)) <= 2 ^ maxdepth (Node c l x r)c:Info.tl:treex:X.tr:treeIHl:S (cardinal l) <= 2 ^ maxdepth lIHr:S (cardinal r) <= 2 ^ maxdepth rS (S (cardinal l + cardinal r)) <= 2 ^ Init.Nat.max (maxdepth l) (maxdepth r) + (2 ^ Init.Nat.max (maxdepth l) (maxdepth r) + 0)c:Info.tl:treex:X.tr:treeIHl:S (cardinal l) <= 2 ^ maxdepth lIHr:S (cardinal r) <= 2 ^ maxdepth rS (cardinal l) + S (cardinal r) <= 2 ^ Init.Nat.max (maxdepth l) (maxdepth r) + 2 ^ Init.Nat.max (maxdepth l) (maxdepth r)c:Info.tl:treex:X.tr:treeIHl:S (cardinal l) <= 2 ^ maxdepth lIHr:S (cardinal r) <= 2 ^ maxdepth rmaxdepth l <= Init.Nat.max (maxdepth l) (maxdepth r)c:Info.tl:treex:X.tr:treeIHl:S (cardinal l) <= 2 ^ maxdepth lIHr:S (cardinal r) <= 2 ^ maxdepth rmaxdepth r <= Init.Nat.max (maxdepth l) (maxdepth r)apply Nat.le_max_l.c:Info.tl:treex:X.tr:treeIHl:S (cardinal l) <= 2 ^ maxdepth lIHr:S (cardinal r) <= 2 ^ maxdepth rmaxdepth l <= Init.Nat.max (maxdepth l) (maxdepth r)apply Nat.le_max_r. Qed.c:Info.tl:treex:X.tr:treeIHl:S (cardinal l) <= 2 ^ maxdepth lIHr:S (cardinal r) <= 2 ^ maxdepth rmaxdepth r <= Init.Nat.max (maxdepth l) (maxdepth r)s:tree2 ^ mindepth s <= S (cardinal s)s:tree2 ^ mindepth s <= S (cardinal s)s:tree2 ^ mindepth s <= S (cardinal s)2 ^ mindepth Leaf <= S (cardinal Leaf)c:Info.tl:treex:X.tr:treeIHl:2 ^ mindepth l <= S (cardinal l)IHr:2 ^ mindepth r <= S (cardinal r)2 ^ mindepth (Node c l x r) <= S (cardinal (Node c l x r))auto.2 ^ mindepth Leaf <= S (cardinal Leaf)c:Info.tl:treex:X.tr:treeIHl:2 ^ mindepth l <= S (cardinal l)IHr:2 ^ mindepth r <= S (cardinal r)2 ^ mindepth (Node c l x r) <= S (cardinal (Node c l x r))c:Info.tl:treex:X.tr:treeIHl:2 ^ mindepth l <= S (cardinal l)IHr:2 ^ mindepth r <= S (cardinal r)2 ^ Init.Nat.min (mindepth l) (mindepth r) + (2 ^ Init.Nat.min (mindepth l) (mindepth r) + 0) <= S (S (cardinal l + cardinal r))c:Info.tl:treex:X.tr:treeIHl:2 ^ mindepth l <= S (cardinal l)IHr:2 ^ mindepth r <= S (cardinal r)2 ^ Init.Nat.min (mindepth l) (mindepth r) + 2 ^ Init.Nat.min (mindepth l) (mindepth r) <= S (cardinal l) + S (cardinal r)c:Info.tl:treex:X.tr:treeIHl:2 ^ mindepth l <= S (cardinal l)IHr:2 ^ mindepth r <= S (cardinal r)Init.Nat.min (mindepth l) (mindepth r) <= mindepth lc:Info.tl:treex:X.tr:treeIHl:2 ^ mindepth l <= S (cardinal l)IHr:2 ^ mindepth r <= S (cardinal r)Init.Nat.min (mindepth l) (mindepth r) <= mindepth rapply Nat.le_min_l.c:Info.tl:treex:X.tr:treeIHl:2 ^ mindepth l <= S (cardinal l)IHr:2 ^ mindepth r <= S (cardinal r)Init.Nat.min (mindepth l) (mindepth r) <= mindepth lapply Nat.le_min_r. Qed.c:Info.tl:treex:X.tr:treeIHl:2 ^ mindepth l <= S (cardinal l)IHr:2 ^ mindepth r <= S (cardinal r)Init.Nat.min (mindepth l) (mindepth r) <= mindepth rs:trees <> Leaf -> Nat.log2 (cardinal s) < maxdepth ss:trees <> Leaf -> Nat.log2 (cardinal s) < maxdepth ss:treeH:s <> LeafNat.log2 (cardinal s) < maxdepth ss:treeH:s <> Leaf0 < cardinal ss:treeH:s <> Leafcardinal s < 2 ^ maxdepth sapply maxdepth_cardinal. Qed.s:treeH:s <> Leafcardinal s < 2 ^ maxdepth ss:treemindepth s <= Nat.log2 (S (cardinal s))s:treemindepth s <= Nat.log2 (S (cardinal s))s:tree0 < S (cardinal s)s:tree2 ^ mindepth s <= S (cardinal s)apply mindepth_cardinal. Qed. End Props.s:tree2 ^ mindepth s <= S (cardinal s)