proposition: Lemma ecompare_spec m1 m2 : ecompare m1 m2 = eLcmp (bindings m1) (bindings m2).
proof: Proof. revert m2. induction m1 as [|l1 IHl1 o1 r1 IHr1]; intros m2. - simpl. generalize (bindings_nil m2). destruct bindings, is_empty; simpl; intuition easy. - generalize (bindings_nil (Node l1 o1 r1)). destruct m2 as [|l2 o2 r2]. + cbn - [is_empty bindings]. destruct (bindings (Node l1 o1 r1)), is_empty; intuition easy. + simpl. intros _. rewrite !bindings_node. rewrite IHl1, ?IHr1; clear IHl1 IHr1. rewrite list_ecompare_app. * rewrite eLcmp_fstmap by auto. destruct (eLcmp (bindings l1) (bindings l2)) as ([ ],b). { destruct o1 as [d1| ], o2 as [d2| ]; simpl. - destruct (cmp d1 d2) eqn:Eo; auto. rewrite eLcmp_fstmap; auto. - generalize (bindings_nil r2). destruct is_empty, (bindings r2); simpl; intuition; try easy. now destruct p. - generalize (bindings_nil r1). destruct is_empty, (bindings r1); simpl; intuition; try easy. now destruct p. - rewrite eLcmp_fstmap; auto. } { destruct b; auto. destruct o1; simpl; auto. generalize (bindings_nil r1). destruct bindings, is_empty; simpl; intuition easy. } { destruct b; auto. destruct o2; simpl; auto. generalize (bindings_nil r2). destruct bindings, is_empty; simpl; intuition easy. } * intros (x,d) (y,d'). rewrite !in_app_iff, !in_map_iff. intros ((k,e) & [= <- <-] & _) [P|((k',e') & [= <- <-] & _)]; simpl; auto. destruct o1; try easy. simpl in P. now destruct P as [[= <- <-]|[ ]]. * intros (x,d) (y,d'). rewrite !in_app_iff, !in_map_iff. intros ((k,e) & [= <- <-] & _) [P|((k',e') & [= <- <-] & _)]; simpl; auto. destruct o2; try easy. simpl in P. now destruct P as [[= <- <-]|[ ]]. Qed.
imports: Coq(Bool PeanoNat BinPos Orders OrdersEx OrdersLists) MMaps(Utils Comparisons Interface)