Merge from LFSC (#26)

* Showing models as coq counter examples in tactic without constructing coq terms

* also read models when calling cvc4 with a file (deactivated because cvc4 crashes)

* Show counter examples with variables in the order they are quantified in the Coq goal

* Circumvent issue with ocamldep

* fix issue with dependencies

* fix issue with dependencies

* Translation and OCaml support for extract, zero_extend, sign_extend

* Show run times of components

* print time on stdout instead

* Tests now work with new version (master) of CVC4

* fix small printing issue

* look for date on mac os x

* proof of valid_check_bbShl: some cases to prove.

* full proof of "left shift checker".

*  full proof of "rigth shift checker".

* Support translation of terms bvlshr, bvshl but LFSC rules do not exists at the moment
Bug fix for bitvector extract (inverted arguments)

* Typo

* More modularity on the format of traces depending on the version of coq

* More straightforward definitions in Int63Native_standard

* Use the Int31 library with coq-8.5

* Use the most efficient operations of Int31

* Improved performance with coq-8.5

* Uniform treatment of sat and smt tactics

* Hopefully solved the problem with universes for the tactic

* Updated the installation instructions

* Holes for unsupported bit blasting rules

* Cherry-picking from smtcoq/smtcoq

* bug fix hole for bitblast

* Predefined arrays are not required anymore

* fix issue with coq bbT and bitof construction from ocaml

* bug fix in smtAtom for uninterpreted functions
fix verit test file

* fix issue with smtlib2 extract parsing

* It looks like we still need the PArray function instances for some examples (see vmcai_bytes.smt2)

* Solver specific reification:
Each solver has a list of supported theories which is passed to Atom.of_coq, this function creates uninterpreted functions / sorts for unsupported features.

* show counter-examples with const_farray instead of const for constant array definitions

* Vernacular commands to debug checkers.
Verit/Lfsc_Checker_Debug will always fail, reporting the first proof step of the certificate that failed be checked

* Update INSTALL.md

* show smtcoq proof when converting

* (Hopefully) repared the universes problems

* Corrected a bug with holes in proofs

* scripts for tests:
create a folder "work" under "lfsc/tests/", locate the benchmarks there.
create a folder "results" under "lfsc/tests/work/" in which you'll find the results of ./cvc4tocoq.

* make sure to give correct path for your benchs...

* Checker for array extensionality modulo symmetry of equality

* fix oversight with bitvectors larger than 63 bits

* some printing functions for smt2 ast

* handle smtlib2 files with more complicated equivalence with (= ... )

* revert: ./cvc4tocoq does not output lfsc proofs...

* bug fix one input was ignored

* Don't show verit translation of LFSC proof if environment variable DONTSHOWVERIT is set
(e.g. put export DONTSHOWVERIT="" in your .bashrc or .bashprofile)

* Also sort names of introduced variables when showing counter-example

* input files for which SMTCoq retuns false.

* input files for which SMTCoq retuns false.

* use debug checker for debug file

* More efficient debug checker

* better approximate number of failing step of certificate in debug checker

* fix mistake in ml4

* very first attempt to support goals in Prop

* bvs: comparison predicates in Prop and their <-> proofs with the ones in bool
farrays: equality predicate in Prop and its <-> proof with the one in bool.

* unit, Bool, Z, Pos: comparison and equality predicates in Prop.

* a typo fixed.

* an example of array equality in  Prop (converted into Bool by hand)...
TODO: enhance the search space of cvc4 tactic.

* first version of cvc4' tactic: "solves" the goals in Prop.
WARNING: supports only bv and array goals and might not be complete
TODO: add support for lia goals

* cvc4' support for lia
WARNING: might not be complete!

* small fix in cvc4' and some variations of examples

* small fix + support for goals in Bool and Bool = true + use of solve tactical
WARNING: does not support UF and INT63 goals in Prop

* cvc4': better arrangement

* cvc4': Prop2Bool by context search...

* cvc4': solve tactial added -> do not modify unsolved goals.

* developer documentation for the smtcoq repo

* cvc4': rudimentary support for uninterpreted function goals in Prop.

* cvc4': support for goals with Leibniz equality...
WARNING: necessary use of "Grab Existential Variables." to instantiate variable types for farrays!

* cvc4': Z.lt adapted + better support from verit...

* cvc4': support for Z.le, Z.ge, Z.gt.

* Try arrays with default value (with a constructor for constant arrays), but extensionality is not provable

* cvc4': support for equality over uninterpreted types

* lfsc demo: goals in Coq's Prop.

* lfsc demo: goals in Bool.

* Fix issue with existential variables generated by prop2bool.
- prop2bool tactic exported by SMTCoq
- remove useless stuff

* update usage and installation instructions

* Update INSTALL.md

* highlighting

* the tactic: bool2prop.

* clean up

* the tactic smt: very first version.

* smt: return unsolved goals in Prop.

* Show when a certificate cannot be checked when running the tactic instead of at Qed

* Tactic improvements
- Handle negation/True/False in prop/bool conversions tactic.
- Remove alias for farray (this caused problem for matching on this type in tactics).
- Tactic `smt` that combines cvc4 and veriT.
- return subgoals in prop

* test change header

* smt: support for negated goals + some reorganization.

* conflicts resolved + some reorganization.

* a way to solve the issue with ambiguous coercions.

* reorganization.

* small change.

* another small change.

* developer documentation of the tactics.

* developer guide: some improvements.

* developer guide: some more improvements.

* developer guide: some more improvements.

* developer guide: some more improvements.

* pass correct environment for conversion + better error messages

* cleaning

* ReflectFacts added.

* re-organizing developers' guide.

* re-organizing developers' guide.

* re-organizing developers' guide.

* removing unused maps.

* headers.

* artifact readme getting started...

* first attempt

* second...

* third...

* 4th...

* 5th...

* 6th...

* 7th...

* 8th...

* 9th...

* 10th...

* 11th...

* 12th...

* 13th...

* 14th...

* 15th...

* 16th...

* 17th...

* Update artifact.md

Use links to lfsc repository like in the paper

* 18th...

* 19th...

* 20th...

* 21st...

* 22nd...

* 23rd...

* 24th...

* 25th...

* 26th...

* 27th...

* 28th...

* Update artifact.md

Small reorganization

* minor edits

* More minor edits

* revised description of tactics

* Final pass

* typo

* name changed: artifact-readme.md

* file added...

* passwd chaged...

* links...

* removal

* performance statement...

* typos...

* the link to the artifact image updated...

* suggestions by Guy...

* aux files removed...

* clean-up...

* clean-up...

* some small changes...

* small fix...

* additional information on newly created files after running cvc4tocoq script...

* some small fix...

* another small fix...

* typo...

* small fix...

* another small fix...

* fix...

* link to the artifact image...

* We do not want to force vm_cast for the Theorem commands

* no_check variants of the tactics

* TODO: a veriT test does not work anymore

* Compiles with both versions of Coq

* Test of the tactics in real conditions

* Comment on this case study

* an example for the FroCoS paper.

* Fix smt tactic that doesn't return cvc4's subgoals

* readme modifications

* readme modifications 2

* small typo in readme.

* small changes in readme.

* small changes in readme.

* typo in readme.

* Sync with https://github.com/LFSC/smtcoq

* Port to Coq 8.6

* README

* README

* INSTALL

* Missing file

* Yves' proposition for installation instructions

* Updated link to CVC4

* Compiles again with native-coq

* Compiles with both versions of Coq

* Command to bypass typechecking when generating a zchaff theorem

* Solved bug on cuts from Hole

* Counter-models for uninterpreted sorts (improves issue #13)

* OCaml version note (#15)

* update .gitignore

* needs OCaml 4.04.0

* Solving merge issues (under progress)

* Make SmtBtype compile

* Compilation of SmtForm under progress

* Make SmtForm compile

* Make SmtCertif compile

* Make SmtTrace compile

* Make SatAtom compile

* Make smtAtom compile

* Make CnfParser compile

* Make Zchaff compile

* Make VeritSyntax compile

* Make VeritParser compile

* Make lfsc/tosmtcoq compile

* Make smtlib2_genconstr compile

* smtCommand under progress

* smtCommands and verit compile again

* lfsc compiles

* ml4 compiles

* Everything compiles

* All ZChaff unit tests and most verit unit tests (but taut5 and un_menteur) go through

* Most LFSC tests ok; some fail due to the problem of verit; a few fail due to an error "Not_found" to investigate

* Authors and headings

* Compiles with native-coq

* Typo

1 files changed, 1973 insertions, 0 deletions

diff --git a/src/array/FArray_default.v b/src/array/FArray_default.v
new file mode 100644
index 0000000..a8e8f44
--- /dev/null
+++ b/src/array/FArray_default.v
@@ -0,0 +1,1973 @@
+(**************************************************************************)
+(*                                                                        *)
+(*     SMTCoq                                                             *)
+(*     Copyright (C) 2011 - 2019                                          *)
+(*                                                                        *)
+(*     See file "AUTHORS" for the list of authors                         *)
+(*                                                                        *)
+(*   This file is distributed under the terms of the CeCILL-C licence     *)
+(*                                                                        *)
+(**************************************************************************)
+
+
+Require Import Bool OrderedType SMT_classes.
+Require Import ProofIrrelevance.
+
+(** This file formalizes functional arrays with extensionality as specified in
+    SMT-LIB 2. It gives realization to axioms that define the SMT-LIB theory of
+    arrays. For this, it uses a formalization of maps with the same approach as
+    FMaplist excepted that constraints on keys and elements are expressed
+    through the use of typeclasses instead of functors. *)
+
+Set Implicit Arguments.
+
+(** Raw maps (see FMaplist) *)
+Module Raw.
+
+  Section Array.
+
+  Variable key : Type.
+  Variable elt : Type.
+  Variable key_dec : DecType key.
+  Variable key_ord : OrdType key.
+  Variable key_comp : Comparable key.
+  Variable elt_dec : DecType elt.
+  Variable elt_ord : OrdType elt.
+
+  Definition eqb_key (x y : key) : bool := if eq_dec x y then true else false.
+  Definition eqb_elt (x y : elt) : bool := if eq_dec x y then true else false.
+
+  Lemma eqb_key_eq x y : eqb_key x y = true <-> x = y.
+  Proof. unfold eqb_key. case (eq_dec x y); split; easy. Qed.
+
+  Lemma eqb_elt_eq x y : eqb_elt x y = true <-> x = y.
+  Proof. unfold eqb_elt. case (eq_dec x y); split; easy. Qed.
+
+  Hint Immediate eqb_key_eq eqb_elt_eq.
+
+  Definition farray := list (key * elt).
+
+  Definition eqk (a b : (key * elt)) := fst a = fst b.
+  Definition eqe (a b : (key * elt)) := snd a = snd b.
+  Definition eqke (a b : (key * elt)) := fst a = fst b /\ snd a = snd b.
+
+  Definition ltk (a b : (key * elt)) := lt (fst a) (fst b).
+
+  (* Definition ltke (a b : (key * elt)) := *)
+  (*   lt (fst a) (fst b) \/ ( (fst a) = (fst b) /\ lt (snd a) (snd b)). *)
+
+  Hint Unfold ltk (* ltke *) eqk eqke.
+  Hint Extern 2 (eqke ?a ?b) => split.
+
+  Global Instance lt_key_strorder : StrictOrder (lt : key -> key -> Prop).
+  Proof. apply StrictOrder_OrdType. Qed.
+
+  Global Instance lt_elt_strorder : StrictOrder (lt : elt -> elt -> Prop).
+  Proof. apply StrictOrder_OrdType. Qed.
+
+  Global Instance ke_dec : DecType (key * elt).
+  Proof.
+    split; auto.
+    intros; destruct x, y, z.
+    inversion H. inversion H0. trivial.
+    intros; destruct x, y.
+    destruct (eq_dec k k0).
+    destruct (eq_dec e e0).
+    left; rewrite e1, e2; auto.
+    right; unfold not in *. intro; inversion H. exact (n H2).
+    right; unfold not in *. intro; inversion H. exact (n H1).
+  Qed.
+
+  Global Instance ke_ord: OrdType (key * elt).
+  Proof.
+    exists ltk; unfold ltk; intros.
+    apply (lt_trans _ (fst y)); auto.
+    destruct x, y. simpl in H.
+    unfold not. intro. inversion H0.
+    apply (lt_not_eq k k0); auto.
+  Qed.
+
+  (* ltk ignore the second components *)
+
+   Lemma ltk_right_r : forall x k e e', ltk x (k,e) -> ltk x (k,e').
+   Proof. auto. Qed.
+
+   Lemma ltk_right_l : forall x k e e', ltk (k,e) x -> ltk (k,e') x.
+   Proof. auto. Qed.
+   Hint Immediate ltk_right_r ltk_right_l.
+
+  Notation Sort := (sort ltk).
+  Notation Inf := (lelistA (ltk)).
+
+  Definition MapsTo (k:key)(e:elt):= InA eqke (k,e).
+  Definition In k m := exists e:elt, MapsTo k e m.
+
+  Notation NoDupA := (NoDupA eqk).
+
+  Hint Unfold MapsTo In.
+
+  (* Instance ke_ord: OrdType (key * elt). *)
+  (* Proof. *)
+  (*   exists ltke. *)
+  (*   unfold ltke. intros. *)
+  (*   destruct H, H0. *)
+  (*   left; apply (lt_trans _ (fst y)); auto. *)
+  (*   destruct H0. left. rewrite <- H0. assumption. *)
+  (*   destruct H. left. rewrite H. assumption. *)
+  (*   destruct H, H0. *)
+  (*   right. split. *)
+  (*   apply (eq_trans _ (fst y)); trivial. *)
+  (*   apply (lt_trans _ (snd y)); trivial. *)
+  (*   unfold ltke. intros. *)
+  (*   destruct x, y. simpl in H. *)
+  (*   destruct H. *)
+  (*   apply lt_not_eq in H. *)
+  (*   unfold not in *. intro. inversion H0. apply H. trivial. *)
+  (*   destruct H. apply lt_not_eq in H0. unfold not in *. intro.  *)
+  (*   inversion H1. apply H0; trivial. *)
+  (*   intros. *)
+  (*   unfold ltke. *)
+  (*   destruct (compare (fst x) (fst y)). *)
+  (*   apply LT. left; assumption. *)
+  (*   destruct (compare (snd x) (snd y)). *)
+  (*   apply LT. right; split; assumption. *)
+  (*   apply EQ. destruct x, y. simpl in *. rewrite e, e0; trivial. *)
+  (*   apply GT. right; symmetry in e; split; assumption. *)
+  (*   apply GT. left; assumption. *)
+  (* Qed. *)
+
+  (* Hint Immediate ke_ord. *)
+  (* Let ke_ord := ke_ord. *)
+
+  (* Instance keyelt_ord: OrdType (key * elt). *)
+
+
+  (* Variable keyelt_ord : OrdType (key * elt). *)
+   (* eqke is stricter than eqk *)
+
+   Lemma eqke_eqk : forall x x', eqke x x' -> eqk x x'.
+   Proof.
+     unfold eqk, eqke; intuition.
+   Qed.
+
+  (* eqk, eqke are equalities *)
+
+  Lemma eqk_refl : forall e, eqk e e.
+  Proof. auto. Qed.
+
+  Lemma eqke_refl : forall e, eqke e e.
+  Proof. auto. Qed.
+
+  Lemma eqk_sym : forall e e', eqk e e' -> eqk e' e.
+  Proof. auto. Qed.
+
+  Lemma eqke_sym : forall e e', eqke e e' -> eqke e' e.
+  Proof. unfold eqke; intuition. Qed.
+
+  Lemma eqk_trans : forall e e' e'', eqk e e' -> eqk e' e'' -> eqk e e''.
+  Proof. eauto. Qed.
+
+  Lemma eqke_trans : forall e e' e'', eqke e e' -> eqke e' e'' -> eqke e e''.
+  Proof.
+    unfold eqke; intuition; [ eauto | congruence ].
+  Qed.
+
+  Lemma ltk_trans : forall e e' e'', ltk e e' -> ltk e' e'' -> ltk e e''.
+  Proof. eauto. Qed.
+
+  Lemma ltk_not_eqk : forall e e', ltk e e' -> ~ eqk e e'.
+  Proof. unfold ltk, eqk. intros. apply lt_not_eq; auto. Qed.
+
+  Lemma ltk_not_eqke : forall e e', ltk e e' -> ~eqke e e'.
+  Proof.
+    unfold eqke, ltk; intuition; simpl in *; subst.
+    apply lt_not_eq in H. auto.
+  Qed.
+
+  Hint Resolve eqk_trans eqke_trans eqk_refl eqke_refl.
+  Hint Resolve ltk_trans ltk_not_eqk ltk_not_eqke.
+  Hint Immediate eqk_sym eqke_sym.
+
+  Global Instance eqk_equiv : Equivalence eqk.
+  Proof. split; eauto. Qed.
+
+  Global Instance eqke_equiv : Equivalence eqke.
+  Proof. split; eauto. Qed.
+
+  Global Instance ltk_strorder : StrictOrder ltk.
+  Proof.
+    split.
+    unfold Irreflexive, Reflexive, complement.
+    intros. apply lt_not_eq in H; auto.
+    unfold Transitive. intros x y z. apply lt_trans.
+  Qed.
+
+  (* Instance ltke_strorder : StrictOrder ltke. *)
+  (* Proof. *)
+  (*   split. *)
+  (*   unfold Irreflexive, Reflexive, complement. *)
+  (*   intros. apply lt_not_eq in H; auto. *)
+  (*   unfold Transitive. apply lt_trans. *)
+  (* Qed. *)
+
+  Global Instance eq_equiv : @Equivalence (key * elt) eq.
+  Proof.
+    split; auto.
+    unfold Transitive. apply eq_trans.
+  Qed.
+
+  (* Instance ltke_compat : Proper (eq ==> eq ==> iff) ltke. *)
+  (* Proof. *)
+  (*   split; rewrite H, H0; trivial. *)
+  (* Qed. *)
+
+  Global Instance ltk_compat : Proper (eq ==> eq ==> iff) ltk.
+  Proof.
+    split; rewrite H, H0; trivial.
+  Qed.
+
+  Global Instance ltk_compatk : Proper (eqk==>eqk==>iff) ltk.
+  Proof.
+  intros (x,e) (x',e') Hxx' (y,f) (y',f') Hyy'; compute.
+   compute in Hxx'; compute in Hyy'. rewrite Hxx', Hyy'; auto.
+  Qed.
+
+  Global Instance ltk_compat' : Proper (eqke==>eqke==>iff) ltk.
+  Proof.
+  intros (x,e) (x',e') (Hxx',_) (y,f) (y',f') (Hyy',_); compute.
+   compute in Hxx'; compute in Hyy'. rewrite Hxx', Hyy'; auto.
+  Qed.
+
+  Global Instance ltk_asym : Asymmetric ltk.
+  Proof. apply (StrictOrder_Asymmetric ltk_strorder). Qed.
+
+  (* Additional facts *)
+
+  Lemma eqk_not_ltk : forall x x', eqk x x' -> ~ltk x x'.
+  Proof.
+    unfold eqk, ltk.
+    unfold not. intros x x' H.
+    destruct x, x'. simpl in *.
+    intro.
+    symmetry in H.
+    apply lt_not_eq in H. auto.
+    subst. auto.
+  Qed.
+
+  Lemma ltk_eqk : forall e e' e'', ltk e e' -> eqk e' e'' -> ltk e e''.
+  Proof. unfold ltk, eqk. destruct e, e', e''. simpl.
+    intros; subst; trivial.
+  Qed.
+
+  Lemma eqk_ltk : forall e e' e'', eqk e e' -> ltk e' e'' -> ltk e e''.
+  Proof.
+    intros (k,e) (k',e') (k'',e'').
+    unfold ltk, eqk; simpl; intros; subst; trivial.
+  Qed.
+  Hint Resolve eqk_not_ltk.
+  Hint Immediate ltk_eqk eqk_ltk.
+  
+  Lemma InA_eqke_eqk :
+     forall x m, InA eqke x m -> InA eqk x m.
+  Proof.
+    unfold eqke; induction 1; intuition.
+  Qed.
+
+  Hint Resolve InA_eqke_eqk.
+
+  (* Lemma InA_eqk : forall p q m, eqk p q -> InA eqk p m -> InA eqk q m. *)
+  (* Proof. *)
+  (*  intros; apply InA_eqA with p; auto with *. *)
+  (* Qed. *)
+
+  (* Lemma In_eq : forall l x y, eq x y -> InA eqke x l -> InA eqke y l. *)
+  (* Proof. intros. rewrite <- H; auto. Qed. *)
+
+  (* Lemma ListIn_In : forall l x, List.In x l -> InA eqk x l. *)
+  (* Proof. apply In_InA. split; auto. unfold Transitive. *)
+  (*   unfold eqk; intros. rewrite H, <- H0. auto. *)
+  (* Qed. *)
+  
+  (* Lemma Inf_lt : forall l x y, ltk x y -> Inf y l -> Inf x l. *)
+  (* Proof. exact (InfA_ltA ltk_strorder). Qed. *)
+
+  (* Lemma Inf_eq : forall l x y, x = y -> Inf y l -> Inf x l. *)
+  (* Proof. exact (InfA_eqA eq_equiv ltk_compat). Qed. *)
+
+  (* An alternative formulation for [In k l] is [exists e, InA eqk (k,e) l] *)
+
+  Lemma In_alt : forall k l, In k l <-> exists e, InA eqk (k,e) l.
+  Proof.
+  firstorder.
+  exists x; auto.
+  induction H.
+  destruct y.
+  exists e; auto.
+  destruct IHInA as [e H0].
+  exists e; auto.
+  Qed.
+
+  Lemma MapsTo_eq : forall l x y e, eq x y -> MapsTo x e l -> MapsTo y e l.
+  Proof.
+  intros; unfold MapsTo in *; apply InA_eqA with (x,e); eauto with *.
+  Qed.
+
+  Lemma In_eq : forall l x y, eq x y -> In x l -> In y l.
+  Proof.
+  destruct 2 as (e,E); exists e; eapply MapsTo_eq; eauto.
+  Qed.
+
+  Lemma Inf_eq : forall l x x', eqk x x' -> Inf x' l -> Inf x l.
+  Proof. exact (InfA_eqA eqk_equiv ltk_compatk). Qed.
+
+  Lemma Inf_lt : forall l x x', ltk x x' -> Inf x' l -> Inf x l.
+  Proof. exact (InfA_ltA ltk_strorder). Qed.
+
+  Hint Immediate Inf_eq.
+  Hint Resolve Inf_lt.
+
+  Lemma Sort_Inf_In :
+    forall l p q, Sort l -> Inf q l -> InA eqk p l -> ltk q p.
+  Proof.
+    exact (SortA_InfA_InA eqk_equiv ltk_strorder ltk_compatk).
+  Qed.
+
+  Lemma Sort_Inf_NotIn :
+    forall l k e, Sort l -> Inf (k,e) l ->  ~In k l.
+  Proof.
+    intros; red; intros.
+    destruct H1 as [e' H2].
+    elim (@ltk_not_eqk (k,e) (k,e')).
+    eapply Sort_Inf_In; eauto.
+    red; simpl; auto.
+  Qed.
+
+  Hint Resolve Sort_Inf_NotIn.
+
+  Lemma Sort_NoDupA: forall l, Sort l -> NoDupA l.
+  Proof.
+    exact (SortA_NoDupA eqk_equiv ltk_strorder ltk_compatk).
+  Qed.
+
+  Lemma Sort_In_cons_1 : forall e l e', Sort (e::l) -> InA eqk e' l -> ltk e e'.
+  Proof.
+    inversion 1; intros; eapply Sort_Inf_In; eauto.
+  Qed.
+
+  Lemma Sort_In_cons_2 : forall l e e', Sort (e::l) -> InA eqk e' (e::l) ->
+                                   ltk e e' \/ eqk e e'.
+  Proof.
+    inversion_clear 2; auto.
+    left; apply Sort_In_cons_1 with l; auto.
+  Qed.
+
+  Lemma Sort_In_cons_3 :
+    forall x l k e, Sort ((k,e)::l) -> In x l -> ~eq x k.
+  Proof.
+    inversion_clear 1; red; intros.
+    destruct (Sort_Inf_NotIn H0 H1 (In_eq H2 H)).
+  Qed.
+
+  Lemma In_inv : forall k k' e l, In k ((k',e) :: l) -> eq k k' \/ In k l.
+  Proof.
+    inversion 1.
+    inversion_clear H0; eauto.
+    destruct H1; simpl in *; intuition.
+  Qed.
+
+  Lemma In_inv_2 : forall k k' e e' l,
+      InA eqk (k, e) ((k', e') :: l) -> ~ eq k k' -> InA eqk (k, e) l.
+  Proof.
+    inversion_clear 1; compute in H0; intuition.
+  Qed.
+
+  Lemma In_inv_3 : forall x x' l,
+      InA eqke x (x' :: l) -> ~ eqk x x' -> InA eqke x l.
+  Proof.
+    inversion_clear 1; compute in H0; intuition.
+  Qed.
+
+  Hint Resolve In_inv_2 In_inv_3.
+
+  (** * FMAPLIST interface implementaion  *)
+
+  (** * [empty] *)
+
+  Definition empty : farray := nil.
+
+  Definition Empty m := forall (a : key)(e:elt) , ~ MapsTo a e m.
+
+  Lemma empty_1 : Empty empty.
+  Proof.
+    unfold Empty,empty.
+    intros a e.
+    intro abs.
+    inversion abs.
+  Qed.
+  Hint Resolve empty_1.
+
+  Lemma empty_sorted : Sort empty.
+  Proof.
+    unfold empty; auto.
+  Qed.
+
+  Lemma MapsTo_inj : forall x e e' l (Hl:Sort l),
+      MapsTo x e l -> MapsTo x e' l -> e = e'.
+    induction l.
+    - intros. apply empty_1 in H. contradiction.
+    - intros.
+      destruct a as (y, v).
+      pose proof H as HH.
+      pose proof H0 as HH0.
+      unfold MapsTo in H.
+      apply InA_eqke_eqk in H.
+      apply InA_eqke_eqk in H0.
+      apply (Sort_In_cons_2 Hl) in H.
+      apply (Sort_In_cons_2 Hl) in H0.
+      destruct H, H0.
+      + apply ltk_not_eqk in H.
+        apply ltk_not_eqk in H0.
+        assert (~ eqk (x, e) (y, v)). unfold not in *. intros. apply H. now apply eqk_sym.
+        assert (~ eqk (x, e') (y, v)). unfold not in *. intros. apply H. now apply eqk_sym.
+        specialize (In_inv_3 HH0 H2).
+        specialize (In_inv_3 HH H1).
+        inversion_clear Hl.
+        apply (IHl H3).
+      + apply ltk_not_eqk in H.
+        unfold eqk in H, H0; simpl in H, H0. contradiction.
+      + apply ltk_not_eqk in H0.
+        unfold eqk in H, H0; simpl in H, H0. contradiction.
+      + unfold eqk in H, H0. simpl in *. subst.
+        inversion_clear HH.
+        inversion_clear HH0.
+        unfold eqke in *. simpl in *. destruct H, H1; subst; auto.
+        apply InA_eqke_eqk in H1.
+        inversion_clear Hl.
+        specialize (Sort_Inf_In H2 H3 H1).
+        unfold ltk. simpl. intro. apply lt_not_eq in H4. contradiction.
+        apply InA_eqke_eqk in H.
+        inversion_clear Hl.
+        specialize (Sort_Inf_In H1 H2 H).
+        unfold ltk. simpl. intro. apply lt_not_eq in H3. contradiction.
+  Qed.
+
+  (** * [is_empty] *)
+
+  Definition is_empty (l : farray) : bool := if l then true else false.
+
+  Lemma is_empty_1 :forall m, Empty m -> is_empty m = true.
+  Proof.
+    unfold Empty, MapsTo.
+    intros m.
+    case m;auto.
+    intros (k,e) l inlist.
+    absurd (InA eqke (k, e) ((k, e) :: l));auto.
+  Qed.
+
+  Lemma is_empty_2 : forall m, is_empty m = true -> Empty m.
+  Proof.
+    intros m.
+    case m;auto.
+    intros p l abs.
+    inversion abs.
+  Qed.
+
+  (** * [mem] *)
+
+  Function mem (k : key) (s : farray) {struct s} : bool :=
+    match s with
+    | nil => false
+    | (k',_) :: l =>
+      match compare k k' with
+      | LT _ => false
+      | EQ _ => true
+      | GT _ => mem k l
+      end
+    end.
+
+  Lemma mem_1 : forall m (Hm:Sort m) x, In x m -> mem x m = true.
+  Proof.
+    intros m Hm x; generalize Hm; clear Hm.
+    functional induction (mem x m);intros sorted belong1;trivial.
+
+    inversion belong1. inversion H.
+
+    absurd (In x ((k', _x) :: l));try assumption.
+    apply Sort_Inf_NotIn with _x;auto.
+
+    apply IHb.
+    elim (sort_inv sorted);auto.
+    elim (In_inv belong1);auto.
+    intro abs.
+    absurd (eq x k'); auto.
+    symmetry in abs.
+    apply lt_not_eq in abs; auto.
+  Qed.
+
+  Lemma mem_2 : forall m (Hm:Sort m) x, mem x m = true -> In x m.
+  Proof.
+    intros m Hm x; generalize Hm; clear Hm; unfold In,MapsTo.
+    functional induction (mem x m); intros sorted hyp;try ((inversion hyp);fail).
+    exists _x; auto.
+    induction IHb; auto.
+    exists x0; auto.
+    inversion_clear sorted; auto.
+  Qed.
+
+  Lemma mem_3 : forall m (Hm:Sort m) x, mem x m = false -> ~ In x m.
+    intros.
+    rewrite <- not_true_iff_false in H.
+    unfold not in *. intros; apply H.
+    now apply mem_1.
+  Qed.
+
+  (** * [find] *)
+
+  Function find (k:key) (s: farray) {struct s} : option elt :=
+    match s with
+    | nil => None
+    | (k',x)::s' =>
+      match compare k k' with
+      | LT _ => None
+      | EQ _ => Some x
+      | GT _ => find k s'
+      end
+    end.
+
+  Lemma find_2 :  forall m x e, find x m = Some e -> MapsTo x e m.
+  Proof.
+    intros m x. unfold MapsTo.
+    functional induction (find x m);simpl;intros e' eqfind; inversion eqfind; auto.
+  Qed.
+
+  Lemma find_1 :  forall m (Hm:Sort m) x e, MapsTo x e m -> find x m = Some e.
+  Proof.
+    intros m Hm x e; generalize Hm; clear Hm; unfold MapsTo.
+    functional induction (find x m);simpl; subst; try clear H_eq_1.
+
+    inversion 2.
+
+    inversion_clear 2.
+    clear e1;compute in H0; destruct H0.
+    apply lt_not_eq in H; auto. now contradict H.
+
+    clear e1;generalize (Sort_In_cons_1 Hm (InA_eqke_eqk H0)); compute.
+    (* order. *)
+    intros.
+    apply (lt_trans k') in _x; auto.
+    apply lt_not_eq in _x.
+    now contradict _x.
+
+    clear e1;inversion_clear 2.
+    compute in H0; destruct H0; intuition congruence.
+    generalize (Sort_In_cons_1 Hm (InA_eqke_eqk H0)); compute.
+    (* order. *)
+    intros.
+    apply lt_not_eq in H. now contradict H.
+
+    clear e1; do 2 inversion_clear 1; auto.
+    compute in H2; destruct H2.
+    (* order. *)
+    subst. apply lt_not_eq in _x. now contradict _x.
+  Qed.
+
+  (** * [add] *)
+
+  Function add (k : key) (x : elt) (s : farray) {struct s} : farray :=
+    match s with
+    | nil => (k,x) :: nil
+    | (k',y) :: l =>
+      match compare k k' with
+      | LT _ => (k,x)::s
+      | EQ _ => (k,x)::l
+      | GT _ => (k',y) :: add k x l
+      end
+    end.
+
+  Lemma add_1 : forall m x y e, eq x y -> MapsTo y e (add x e m).
+  Proof.
+    intros m x y e; generalize y; clear y.
+    unfold MapsTo.
+    functional induction (add x e m);simpl;auto.
+  Qed.
+
+  Lemma add_2 : forall m x y e e',
+      ~ eq x y -> MapsTo y e m -> MapsTo y e (add x e' m).
+  Proof.
+    intros m x  y e e'.
+    generalize y e; clear y e; unfold MapsTo.
+    functional induction (add x e' m) ;simpl;auto;  clear e0.
+    subst;auto.
+
+    intros y' e'' eqky';  inversion_clear 1;  destruct H0; simpl in *.
+    (* order. *)
+    subst. now contradict eqky'.
+    auto.
+    auto.
+    intros y' e'' eqky'; inversion_clear 1; intuition.
+  Qed.
+
+  Lemma add_3 : forall m x y e e',
+      ~ eq x y -> MapsTo y e (add x e' m) -> MapsTo y e m.
+  Proof.
+    intros m x y e e'. generalize y e; clear y e; unfold MapsTo.
+    functional induction (add x e' m);simpl; intros.
+    apply (In_inv_3 H0); compute; auto.
+    apply (In_inv_3 H0); compute; auto.
+    constructor 2; apply (In_inv_3 H0); compute; auto.
+    inversion_clear H0; auto.
+  Qed.
+
+  Lemma add_Inf : forall (m:farray)(x x':key)(e e':elt),
+      Inf (x',e') m -> ltk (x',e') (x,e) -> Inf (x',e') (add x e m).
+  Proof.
+    induction m.
+    simpl; intuition.
+    intros.
+    destruct a as (x'',e'').
+    inversion_clear H.
+    compute in H0,H1.
+    simpl; case (compare x x''); intuition.
+  Qed.
+  Hint Resolve add_Inf.
+
+  Lemma add_sorted : forall m (Hm:Sort m) x e, Sort (add x e m).
+  Proof.
+    induction m.
+    simpl; intuition.
+    intros.
+    destruct a as (x',e').
+    simpl; case (compare x x'); intuition; inversion_clear Hm; auto.
+    constructor; auto.
+    apply Inf_eq with (x',e'); auto.
+  Qed.
+
+  (** * [remove] *)
+
+  Function remove (k : key) (s : farray) {struct s} : farray :=
+    match s with
+    | nil => nil
+    | (k',x) :: l =>
+      match compare k k' with
+      | LT _ => s
+      | EQ _ => l
+      | GT _ => (k',x) :: remove k l
+      end
+    end.
+
+  Lemma remove_1 : forall m (Hm:Sort m) x y, eq x y -> ~ In y (remove x m).
+  Proof.
+    intros m Hm x y; generalize Hm; clear Hm.
+    functional induction (remove x m);simpl;intros;subst.
+
+    red; inversion 1; inversion H0.
+
+    apply Sort_Inf_NotIn with x0; auto.
+
+    clear e0. inversion Hm. subst.
+    apply Sort_Inf_NotIn with x0; auto.
+
+    (* clear e0;inversion_clear Hm. *)
+    (* apply Sort_Inf_NotIn with x0; auto. *)
+    (* apply Inf_eq with (k',x0);auto; compute; apply eq_trans with x; auto. *)
+
+    clear e0;inversion_clear Hm.
+    assert (notin:~ In y (remove y l)) by auto.
+    intros (x1,abs).
+    inversion_clear abs.
+    compute in H1; destruct H1.
+    subst. apply lt_not_eq in _x; now contradict _x.
+    apply notin; exists x1; auto.
+  Qed.
+
+
+  Lemma remove_2 : forall m (Hm:Sort m) x y e,
+      ~ eq x y -> MapsTo y e m -> MapsTo y e (remove x m).
+  Proof.
+    intros m Hm x y e; generalize Hm; clear Hm; unfold MapsTo.
+    functional induction (remove x m);subst;auto;
+      match goal with
+      | [H: compare _ _ = _ |- _ ] => clear H
+      | _ => idtac
+      end.
+
+    inversion_clear 3; auto.
+    compute in H1; destruct H1.
+    subst; now contradict H.
+    inversion_clear 1; inversion_clear 2; auto.
+  Qed.
+
+  Lemma remove_3 : forall m (Hm:Sort m) x y e,
+      MapsTo y e (remove x m) -> MapsTo y e m.
+  Proof.
+    intros m Hm x y e; generalize Hm; clear Hm; unfold MapsTo.
+    functional induction (remove x m);subst;auto.
+    inversion_clear 1; inversion_clear 1; auto.
+  Qed.
+
+  Lemma remove_4_aux : forall m (Hm:Sort m) x y,
+      ~ eq x y -> In y m -> In y (remove x m).
+  Proof.
+    intros m Hm x y; generalize Hm; clear Hm.
+    functional induction (remove x m);subst;auto;
+      match goal with
+      | [H: compare _ _ = _ |- _ ] => clear H
+      | _ => idtac
+      end.
+    rewrite In_alt.
+    inversion_clear 3; auto.
+    inversion H2.
+    unfold eqk in H3. simpl in H3. subst. now contradict H0.
+    apply In_alt.
+    exists x1. auto.
+    apply lt_not_eq in _x.
+    intros.
+    inversion_clear Hm.
+    inversion_clear H0.
+    unfold MapsTo in H3.
+    apply InA_eqke_eqk in H3.
+    unfold In.
+    destruct (eq_dec k' y).
+    exists x0.
+    apply InA_cons_hd.
+    split; simpl; auto.
+    inversion H3.
+    unfold eqk in H4. simpl in H4; subst. now contradict n.
+    assert ((exists e : elt, MapsTo y e (remove x l)) -> (exists e : elt, MapsTo y e ((k', x0) :: remove x l))).
+    intros.
+    destruct H6. exists x2.
+    apply InA_cons_tl. auto.
+    apply H6.
+    apply IHf; auto.
+    apply In_alt.
+    exists x1. auto.
+  Qed.
+
+  Lemma remove_4 : forall m (Hm:Sort m) x y,
+      ~ eq x y -> In y m <-> In y (remove x m).
+  Proof.
+    split.
+    apply remove_4_aux; auto.
+    revert H.
+    generalize Hm; clear Hm.
+    functional induction (remove x m);subst;auto;
+      match goal with
+      | [H: compare _ _ = _ |- _ ] => clear H
+      | _ => idtac
+      end.
+    intros.
+    (* rewrite In_alt in *. *)
+    destruct H0 as (e, H0).
+    exists e.
+    apply InA_cons_tl. auto.
+    intros.
+    apply lt_not_eq in _x.
+    inversion_clear Hm.
+    apply In_inv in H0.
+    destruct H0.
+    (* destruct (eq_dec k' y). *)
+    exists x0.
+    apply InA_cons_hd. split; simpl; auto.
+    specialize (IHf H1 H H0).
+    inversion IHf.
+    exists x1.
+    apply InA_cons_tl. auto.
+  Qed.
+
+  Lemma remove_Inf : forall (m:farray)(Hm : Sort m)(x x':key)(e':elt),
+      Inf (x',e') m -> Inf (x',e') (remove x m).
+  Proof.
+    induction m.
+    simpl; intuition.
+    intros.
+    destruct a as (x'',e'').
+    inversion_clear H.
+    compute in H0.
+    simpl; case (compare x x''); intuition.
+    inversion_clear Hm.
+    apply Inf_lt with (x'',e''); auto.
+  Qed.
+  Hint Resolve remove_Inf.
+
+  Lemma remove_sorted : forall m (Hm:Sort m) x, Sort (remove x m).
+  Proof.
+    induction m.
+    simpl; intuition.
+    intros.
+    destruct a as (x',e').
+    simpl; case (compare x x'); intuition; inversion_clear Hm; auto.
+  Qed.
+
+  (** * [elements] *)
+
+  Definition elements (m: farray) := m.
+
+  Lemma elements_1 : forall m x e,
+      MapsTo x e m -> InA eqke (x,e) (elements m).
+  Proof.
+    auto.
+  Qed.
+
+  Lemma elements_2 : forall m x e,
+      InA eqke (x,e) (elements m) -> MapsTo x e m.
+  Proof.
+    auto.
+  Qed.
+
+  Lemma elements_3 : forall m (Hm:Sort m), sort ltk (elements m).
+  Proof.
+    auto.
+  Qed.
+
+  Lemma elements_3w : forall m (Hm:Sort m), NoDupA (elements m).
+  Proof.
+    intros.
+    apply Sort_NoDupA.
+    apply elements_3; auto.
+  Qed.
+
+  (** * [fold] *)
+
+  Function fold (A:Type)(f:key->elt->A->A)(m:farray) (acc:A) {struct m} :  A :=
+    match m with
+    | nil => acc
+    | (k,e)::m' => fold f m' (f k e acc)
+    end.
+
+  Lemma fold_1 : forall m (A:Type)(i:A)(f:key->elt->A->A),
+      fold f m i = fold_left (fun a p => f (fst p) (snd p) a) (elements m) i.
+  Proof.
+    intros; functional induction (fold f m i); auto.
+  Qed.
+
+  (** * [equal] *)
+
+  Function equal (cmp:elt->elt->bool)(m m' : farray) {struct m} : bool :=
+    match m, m' with
+    | nil, nil => true
+    | (x,e)::l, (x',e')::l' =>
+      match compare x x' with
+      | EQ _ => cmp e e' && equal cmp l l'
+      | _    => false
+      end
+    | _, _ => false
+    end.
+
+  Definition Equivb cmp m m' :=
+    (forall k, In k m <-> In k m') /\
+    (forall k e e', MapsTo k e m -> MapsTo k e' m' -> cmp e e' = true).
+
+  Lemma equal_1 : forall m (Hm:Sort m) m' (Hm': Sort m') cmp,
+      Equivb cmp m m' -> equal cmp m m' = true.
+  Proof.
+    intros m Hm m' Hm' cmp; generalize Hm Hm'; clear Hm Hm'.
+    functional induction (equal cmp m m'); simpl; subst;auto; unfold Equivb;
+      intuition; subst.
+    match goal with H: compare _ _ = _ |- _ => clear H end.
+    assert (cmp_e_e':cmp e e' = true).
+    apply H1 with x; auto.
+    rewrite cmp_e_e'; simpl.
+    apply IHb; auto.
+    inversion_clear Hm; auto.
+    inversion_clear Hm'; auto.
+    unfold Equivb; intuition.
+    destruct (H0 k).
+    assert (In k ((x,e) ::l)).
+    destruct H as (e'', hyp); exists e''; auto.
+    destruct (In_inv (H2 H4)); auto.
+    inversion_clear Hm.
+    elim (Sort_Inf_NotIn H6 H7).
+    destruct H as (e'', hyp); exists e''; auto.
+    apply MapsTo_eq with k; auto.
+    destruct (H0 k).
+    assert (In k ((x,e') ::l')).
+    destruct H as (e'', hyp); exists e''; auto.
+    destruct (In_inv (H3 H4)); auto.
+    subst.
+    inversion_clear Hm'.
+    now elim (Sort_Inf_NotIn H5 H6).
+    apply H1 with k; destruct (eq_dec x k); auto.
+
+
+    destruct (compare x x') as [Hlt|Heq|Hlt]; try contradiction; clear y.
+    destruct (H0 x).
+    assert (In x ((x',e')::l')).
+    apply H; auto.
+    exists e; auto.
+    destruct (In_inv H3).
+    (* order. *)
+    apply lt_not_eq in Hlt; now contradict Hlt.
+    inversion_clear Hm'.
+    assert (Inf (x,e) l').
+    apply Inf_lt with (x',e'); auto.
+    elim (Sort_Inf_NotIn H5 H7 H4).
+
+    destruct (H0 x').
+    assert (In x' ((x,e)::l)).
+    apply H2; auto.
+    exists e'; auto.
+    destruct (In_inv H3).
+    (* order. *)
+    subst; apply lt_not_eq in Hlt; now contradict Hlt.
+    inversion_clear Hm.
+    assert (Inf (x',e') l).
+    apply Inf_lt with (x,e); auto.
+    elim (Sort_Inf_NotIn H5 H7 H4).
+
+    destruct m;
+      destruct m';try contradiction.
+
+    clear H1;destruct p as (k,e).
+    destruct (H0 k).
+    destruct H1.
+    exists e; auto.
+    inversion H1.
+
+    destruct p as (x,e).
+    destruct (H0 x).
+    destruct H.
+    exists e; auto.
+    inversion H.
+
+    destruct p;destruct p0;contradiction.
+  Qed.
+
+  Lemma equal_2 : forall m (Hm:Sort m) m' (Hm:Sort m') cmp,
+      equal cmp m m' = true -> Equivb cmp m m'.
+  Proof.
+    intros m Hm m' Hm' cmp; generalize Hm Hm'; clear Hm Hm'.
+    functional induction (equal cmp m m'); simpl; subst;auto; unfold Equivb;
+      intuition; try discriminate; subst;
+        try match goal with H: compare _ _ = _ |- _ => clear H end.
+
+    inversion H0.
+
+    inversion_clear Hm;inversion_clear Hm'.
+    destruct (andb_prop _ _ H); clear H.
+    destruct (IHb H1 H3 H6).
+    destruct (In_inv H0).
+    exists e'; constructor; split; trivial; apply eq_trans with x; auto.
+    destruct (H k).
+    destruct (H9 H8) as (e'',hyp).
+    exists e''; auto.
+
+    inversion_clear Hm;inversion_clear Hm'.
+    destruct (andb_prop _ _ H); clear H.
+    destruct (IHb H1 H3 H6).
+    destruct (In_inv H0).
+    exists e; constructor; split; trivial; apply eq_trans with x'; auto.
+    destruct (H k).
+    destruct (H10 H8) as (e'',hyp).
+    exists e''; auto.
+
+    inversion_clear Hm;inversion_clear Hm'.
+    destruct (andb_prop _ _ H); clear H.
+    destruct (IHb H2 H4 H7).
+    inversion_clear H0.
+    destruct H9; simpl in *; subst.
+    inversion_clear H1.
+    destruct H0; simpl in *; subst; auto.
+    elim (Sort_Inf_NotIn H4 H5).
+    exists e'0; apply MapsTo_eq with x; auto.
+      (* order. *)
+    inversion_clear H1.
+    destruct H0; simpl in *; subst; auto.
+    elim (Sort_Inf_NotIn H2 H3).
+    exists e0; apply MapsTo_eq with x; auto.
+    (* order. *)
+    apply H8 with k; auto.
+  Qed.
+
+  (** This lemma isn't part of the spec of [Equivb], but is used in [FMapAVL] *)
+
+  Lemma equal_cons : forall cmp l1 l2 x y, Sort (x::l1) -> Sort (y::l2) ->
+    eqk x y -> cmp (snd x) (snd y) = true ->
+    (Equivb cmp l1 l2 <-> Equivb cmp (x :: l1) (y :: l2)).
+  Proof.
+    intros.
+    inversion H; subst.
+    inversion H0; subst.
+    destruct x; destruct y; compute in H1, H2.
+    split; intros.
+    apply equal_2; auto.
+    simpl.
+    case (compare k k0);
+    subst; intro HH; try (apply lt_not_eq in HH; now contradict HH).
+    rewrite H2; simpl.
+    apply equal_1; auto.
+    apply equal_2; auto.
+    generalize (equal_1 H H0 H3).
+    simpl.
+    case (compare k k0);
+    subst; intro HH; try (apply lt_not_eq in HH; now contradict HH).
+    rewrite H2; simpl; auto.
+  Qed.
+
+End Array.
+
+End Raw.
+
+
+(** * Functional Arrays *)
+
+Section FArray.
+
+  Variable key : Type.
+  Variable elt : Type.
+  Variable key_dec : DecType key.
+  Variable key_ord : OrdType key.
+  Variable key_comp : Comparable key.
+  Variable elt_dec : DecType elt.
+  Variable elt_ord : OrdType elt.
+  Variable elt_comp : Comparable elt.
+  (* Variable key_inh :  Inhabited key. *)
+  (* Variable elt_inh :  Inhabited elt. *)
+
+  Set Implicit Arguments.
+
+  Definition NoDefault l (d:elt) := forall k:key, ~ Raw.MapsTo k d l.
+
+  Record slist :=
+    {this :> Raw.farray key elt;
+     sorted : sort (Raw.ltk key_ord) this;
+     default : elt;
+     nodefault : NoDefault this default;
+    }.
+  Definition farray := slist.
+
+  Lemma empty_nodefault : forall d, NoDefault (Raw.empty key elt) d.
+    unfold NoDefault.
+    intros.
+    apply Raw.empty_1.
+  Qed.
+
+  (** Boolean comparison over elements *)
+  Definition cmp (e e':elt) :=
+    match compare e e' with EQ _ => true | _ => false end.
+
+
+  Lemma cmp_refl : forall e, cmp e e = true.
+    unfold cmp.
+    intros.
+    destruct (compare e e); auto;
+      apply lt_not_eq in l; now contradict l.
+  Qed.
+
+  Lemma remove_nodefault : forall l d (Hd:NoDefault l d) (Hs:Sorted (Raw.ltk key_ord) l) x ,
+      NoDefault (Raw.remove key_comp x l) d.
+  Proof.
+    intros.
+    unfold NoDefault. intros.
+    unfold not. intro.
+    apply Raw.remove_3 in H; auto.
+    now apply Hd in H.
+  Qed.
+
+  Definition raw_add_nodefault (k:key) (x:elt) (default:elt) (l:Raw.farray key elt) :=
+    if cmp x default then
+      if Raw.mem key_comp k l then Raw.remove key_comp k l
+      else l
+    else Raw.add key_comp k x l.
+
+
+  Lemma add_sorted : forall l d (Hs:Sorted (Raw.ltk key_ord) l) x e,
+      Sorted (Raw.ltk key_ord) (raw_add_nodefault x e d l).
+  Proof.
+    intros.
+    unfold raw_add_nodefault.
+    case (cmp e d); auto.
+    case (Raw.mem key_comp x l); auto.
+    apply Raw.remove_sorted; auto.
+    apply Raw.add_sorted; auto.
+  Qed.
+
+  Lemma add_nodefault : forall l d (Hd:NoDefault l d) (Hs:Sorted (Raw.ltk key_ord) l) x e,
+      NoDefault (raw_add_nodefault x e d l) d.
+  Proof.
+    intros.
+    unfold raw_add_nodefault.
+    case_eq (cmp e d); intro; auto.
+    case_eq (Raw.mem key_comp x l); intro; auto.
+    apply remove_nodefault; auto.
+    unfold NoDefault; intros.
+    assert (e <> d).
+      unfold cmp in H.
+      case (compare e d) in H; try now contradict H.
+      apply lt_not_eq in l0; auto.
+      apply lt_not_eq in l0; now auto.
+    destruct (eq_dec k x).
+    - symmetry in e0.
+      apply (Raw.add_1 key_dec key_comp l e) in e0.
+      unfold not; intro.
+      specialize (Raw.add_sorted key_dec key_comp Hs x e).
+      intro Hsadd.
+      specialize (Raw.MapsTo_inj key_dec Hsadd e0 H1).
+      intro. contradiction.
+    - unfold not; intro.
+      assert (x <> k). unfold not in *. intro. apply n. symmetry; auto.
+      specialize (Raw.add_3 key_dec key_comp l e H2 H1).
+      intro. now apply Hd in H3.
+  Qed.
+
+  (* Definition empty : farray := *)
+  (*   Build_slist (Raw.empty_sorted elt key_ord) empty_nodefault. *)
+
+  Definition const_array (default:elt) : farray :=
+    Build_slist
+      (Raw.empty_sorted elt key_ord)
+      (@empty_nodefault default).
+
+  Definition is_const_default m : bool := Raw.is_empty m.(this).
+
+  Definition add x e m : farray :=
+    Build_slist (add_sorted m.(default) m.(sorted) x e)
+                (add_nodefault m.(nodefault) m.(sorted) x e).
+
+  Definition find x m : option elt := Raw.find key_comp x m.(this).
+
+  Definition remove x m : farray :=
+    Build_slist
+      (Raw.remove_sorted key_comp m.(sorted) x)
+      (remove_nodefault m.(nodefault) m.(sorted) x).
+
+  Definition mem x m : bool := Raw.mem key_comp x m.(this).
+  Definition elements m : list (key*elt) := Raw.elements m.(this).
+  Definition cardinal m := length m.(this).
+  Definition fold (A:Type)(f:key->elt->A->A) m (i:A) : A :=
+    Raw.fold f m.(this) i.
+  Definition equal m m' : bool :=
+    if eq_dec m.(default) m'.(default) then
+       Raw.equal key_comp cmp m.(this) m'.(this)
+    else false.
+
+  Definition MapsTo x e m : Prop := Raw.MapsTo x e m.(this).
+  Definition In x m : Prop := Raw.In x m.(this).
+  Definition Empty m : Prop := Raw.Empty m.(this).
+
+  Definition Equal m m' :=
+    m.(default) = m'.(default) /\
+    forall y, find y m = find y m'.
+  
+  Definition Equiv m m' :=
+    m.(default) = m'.(default) /\
+    (forall k, In k m <-> In k m') /\
+    (forall k e e', MapsTo k e m -> MapsTo k e' m' -> e = e').
+  
+  Definition Equivb m m' : Prop :=
+    m.(default) = m'.(default) /\
+    Raw.Equivb cmp m.(this) m'.(this).
+
+  Definition eq_key : (key*elt) -> (key*elt) -> Prop := @Raw.eqk key elt.
+  Definition eq_key_elt : (key*elt) -> (key*elt) -> Prop:= @Raw.eqke key elt.
+  Definition lt_key : (key*elt) -> (key*elt) -> Prop := @Raw.ltk key elt key_ord.
+
+  Lemma MapsTo_1 : forall m x y e, eq x y -> MapsTo x e m -> MapsTo y e m.
+  Proof. intros m.
+    apply (Raw.MapsTo_eq key_dec elt_dec). Qed.
+
+  Lemma mem_1 : forall m x, In x m -> mem x m = true.
+  Proof. intros m; apply (Raw.mem_1); auto. apply m.(sorted). Qed.
+  Lemma mem_2 : forall m x, mem x m = true -> In x m.
+  Proof. intros m; apply (Raw.mem_2); auto. apply m.(sorted). Qed.
+
+  
+  Lemma add_1 : forall m x y e, e <> m.(default) -> eq x y -> MapsTo y e (add x e m).
+  Proof. intros.
+    unfold add, raw_add_nodefault.
+    unfold MapsTo. simpl.
+    case_eq (cmp e m.(default)); intro; auto.
+    unfold cmp in H1. destruct (compare e m.(default)); try now contradict H1.
+    apply Raw.add_1; auto.
+  Qed.
+
+  Lemma add_2 : forall m x y e e', ~ eq x y -> MapsTo y e m -> MapsTo y e (add x e' m).
+  Proof.
+    intros.
+    unfold add, raw_add_nodefault, MapsTo. simpl.
+    case_eq (cmp e' m.(default)); intro; auto.
+    case_eq (Raw.mem key_comp x m); intro; auto.
+    apply (Raw.remove_2 _ m.(sorted)); auto.
+    apply Raw.add_2; auto.
+  Qed.
+
+  Lemma add_3 : forall m x y e e', ~ eq x y -> MapsTo y e (add x e' m) -> MapsTo y e m.
+  Proof.
+    unfold add, raw_add_nodefault, MapsTo. simpl.
+    intros m x y e e'.
+    case_eq (cmp e' m.(default)); intro; auto.
+    case_eq (Raw.mem key_comp x m); intro; auto.
+    intro. apply (Raw.remove_3 _ m.(sorted)); auto.
+    apply Raw.add_3; auto.
+  Qed.
+
+  Lemma remove_1 : forall m x y, eq x y -> ~ In y (remove x m).
+  Proof. intros m; apply Raw.remove_1; auto. apply m.(sorted). Qed.
+
+  Lemma remove_2 : forall m x y e, ~ eq x y -> MapsTo y e m -> MapsTo y e (remove x m).
+  Proof. intros m; apply Raw.remove_2; auto. apply m.(sorted). Qed.
+
+  Lemma remove_3 : forall m x y e, MapsTo y e (remove x m) -> MapsTo y e m.
+  Proof. intros m; apply Raw.remove_3; auto. apply m.(sorted). Qed.
+
+  Lemma find_1 : forall m x e, MapsTo x e m -> find x m = Some e.
+  Proof. intros m; apply Raw.find_1; auto. apply m.(sorted). Qed.
+
+  Lemma find_2 : forall m x e, find x m = Some e -> MapsTo x e m.
+  Proof. intros m; apply Raw.find_2; auto. Qed.
+
+  Lemma elements_1 : forall m x e, MapsTo x e m -> InA eq_key_elt (x,e) (elements m).
+  Proof. intros m; apply Raw.elements_1. Qed.
+
+  Lemma elements_2 : forall m x e, InA eq_key_elt (x,e) (elements m) -> MapsTo x e m.
+  Proof. intros m; apply Raw.elements_2. Qed.
+
+  Lemma elements_3 : forall m, sort lt_key (elements m).
+  Proof. intros m; apply Raw.elements_3; auto. apply m.(sorted). Qed.
+
+  Lemma elements_3w : forall m, NoDupA eq_key (elements m).
+  Proof. intros m; apply (Raw.elements_3w key_dec m.(sorted)). Qed.
+
+  Lemma cardinal_1 : forall m, cardinal m = length (elements m).
+  Proof. intros; reflexivity. Qed.
+
+  Lemma fold_1 : forall m (A : Type) (i : A) (f : key -> elt -> A -> A),
+      fold f m i = fold_left (fun a p => f (fst p) (snd p) a) (elements m) i.
+  Proof. intros m; apply Raw.fold_1. Qed.
+
+  Lemma equal_1 : forall m m', Equivb m m' -> equal m m' = true.
+  Proof. intros m m'; unfold Equivb, equal.
+    case (eq_dec (default m) (default m')); intro H.
+    - intro H0. destruct H0.
+      apply Raw.equal_1; auto. apply m.(sorted). apply  m'.(sorted).
+    - intro H0. destruct H0. now contradict H.
+  Qed.
+
+  
+  Lemma equal_2 : forall m m', equal m m' = true -> Equivb m m'.
+  Proof. intros m m'; unfold Equivb, equal.
+    case (eq_dec (default m) (default m')); intros.
+    - split; auto. 
+      apply Raw.equal_2 in H; auto. apply m.(sorted). apply m'.(sorted).
+    - now contradict H.
+  Qed.
+
+  Fixpoint eq_list (m m' : list (key * elt)) : Prop :=
+    match m, m' with
+    | nil, nil => True
+    | (x,e)::l, (x',e')::l' =>
+      match compare x x' with
+      | EQ _ => eq e e' /\ eq_list l l'
+      | _       => False
+      end
+    | _, _ => False
+    end.
+
+  Definition eq m m' :=
+    if eq_dec m.(default) m'.(default) then
+      eq_list m.(this) m'.(this)
+    else False.
+
+  
+  Lemma nodefault_tail : forall x m d, NoDefault (x :: m) d -> NoDefault m d.
+    unfold NoDefault. unfold not in *. intros.
+    apply (H k). unfold Raw.MapsTo. apply InA_cons_tl. apply H0.
+  Qed.
+
+  Lemma raw_equal_eq : forall a (Ha: Sorted (Raw.ltk key_ord) a) b (Hb: Sorted (Raw.ltk key_ord) b),
+      Raw.equal key_comp cmp a b = true -> a = b.
+  Proof.
+    induction a; intros.
+    simpl in H.
+    case b in *; auto.
+    now contradict H.
+    destruct a as (xa, ea).
+    simpl in H.
+    case b in *.
+    now contradict H.
+    destruct p as (xb, eb).
+    destruct (compare xa xb); auto; try (now contradict H).
+    rewrite andb_true_iff in H. destruct H.
+    unfold cmp in H.
+    destruct (compare ea eb); auto; try (now contradict H).
+    subst. apply f_equal.
+    apply IHa; auto.
+    now inversion Ha.
+    now inversion Hb.
+  Qed.
+
+  Lemma eq_equal : forall m m', eq m m' <-> equal m m' = true.
+  Proof.
+    intros (l,Hl,d,Hd); induction l.
+    intros (l',Hl',d',Hd'); unfold eq, equal; simpl; case (eq_dec d d'); intro;
+      destruct l'; simpl; intuition.
+    intros (l',Hl',d',Hd'); unfold eq. simpl.
+    unfold equal; simpl; case (eq_dec d d'); intro He; simpl; [ | now intuition].
+    destruct l'.
+    destruct a; unfold equal; simpl; intuition.
+    destruct a as (x,e).
+    destruct p as (x',e').
+    unfold equal; simpl.
+    destruct (compare x x') as [Hlt|Heq|Hlt]; simpl; intuition.
+    unfold cmp at 1.
+    case (compare e e');
+    subst x' e'; intro HH; try (apply lt_not_eq in HH; now contradict HH);
+    clear HH; simpl.
+    inversion_clear Hl.
+    inversion_clear Hl'.
+    apply nodefault_tail in Hd.
+    apply nodefault_tail in Hd'.
+    destruct (IHl H Hd (Build_slist H2 Hd')).
+    unfold equal, eq in H5, H4; simpl in H5, H4; subst d'.
+    destruct (eq_dec d d); auto.
+    destruct (andb_prop _ _ H); clear H.
+    generalize H0; unfold cmp.
+    case (compare e e');
+    subst; intro HH; try (apply lt_not_eq in HH; now contradict HH);
+      auto; intro; discriminate.
+    destruct (andb_prop _ _ H); clear H.
+    inversion_clear Hl.
+    inversion_clear Hl'.
+    apply nodefault_tail in Hd.
+    apply nodefault_tail in Hd'.
+    destruct (IHl H Hd (Build_slist H3 Hd')).
+    unfold equal, eq in H5, H6; simpl in H5, H6; subst d'.
+    destruct (eq_dec d d); auto. now contradict n.
+  Qed.
+
+  Lemma eq_1 : forall m m', Equivb m m' -> eq m m'.
+  Proof.
+    intros.
+    generalize (@equal_1 m m').
+    generalize (@eq_equal m m').
+    intuition.
+  Qed.
+
+  Lemma eq_2 : forall m m', eq m m' -> Equivb m m'.
+  Proof.
+    intros.
+    generalize (@equal_2 m m').
+    generalize (@eq_equal m m').
+    intuition.
+  Qed.
+
+  Lemma eqfarray_refl : forall m : farray, eq m m.
+  Proof.
+    intros (m,Hm,d,Hd). unfold eq. simpl.
+    destruct (eq_dec d d); auto.
+    induction m; simpl; auto.
+    destruct a.
+    destruct (compare k k) as [Hlt|Heq|Hlt]; auto.
+    apply lt_not_eq in Hlt. auto.
+    split.
+    apply eq_refl.
+    inversion_clear Hm.
+    apply nodefault_tail in Hd.
+    apply (IHm H Hd).
+    apply lt_not_eq in Hlt. auto.
+  Qed.
+
+  Lemma eqfarray_sym : forall m1 m2 : farray, eq m1 m2 -> eq m2 m1.
+  Proof.
+    unfold eq.
+    intros (m,Hm,d,Hd); induction m;
+      intros (m',Hm',d',Hd'); destruct m'; unfold eq; simpl;
+        destruct (eq_dec d d'); auto; intuition;
+        subst d'; destruct (eq_dec d d) as [He | He]; auto;
+          try destruct a as (x,e); try destruct p as (x',e'); auto; intuition.
+    destruct (compare x x')  as [Hlt|Heq|Hlt]; try easy.
+    inversion_clear Hm; inversion_clear Hm'. destruct H.
+    apply nodefault_tail in Hd. apply nodefault_tail in Hd'.
+    (* intro. destruct H3. *)
+    subst.
+    case (compare x' x');
+    subst; intro HH; try (apply lt_not_eq in HH; now contradict HH).
+    split; auto.
+    specialize (IHm H0 Hd (Build_slist H2 Hd')).
+    simpl in IHm. case (eq_dec d d) in IHm; intuition.
+  Qed.
+
+  Lemma eqfarray_trans : forall m1 m2 m3 : farray, eq m1 m2 -> eq m2 m3 -> eq m1 m3.
+  Proof.
+    unfold eq.
+    intros (m1,Hm1,d1,Hd1); induction m1;
+      intros (m2,Hm2,d2,Hd2); destruct m2;
+        intros (m3,Hm3,d3,Hd3); destruct m3; unfold eq; simpl;
+          destruct (eq_dec d1 d2);
+          destruct (eq_dec d2 d3);
+          destruct (eq_dec d1 d3); simpl in *; subst; intuition;
+          try destruct a as (x,e);
+          try destruct p as (x',e');
+          try destruct p0 as (x'',e''); try contradiction; auto.
+    destruct (compare x x') as [Hlt|Heq|Hlt];
+      destruct (compare x' x'') as [Hlt'|Heq'|Hlt']; try easy.
+    intros; destruct H, H0;  subst.
+    case (compare x'' x'');
+    subst; intro HH; try (apply lt_not_eq in HH; now contradict HH).
+    split; auto.
+    inversion_clear Hm1; inversion_clear Hm2; inversion_clear Hm3.
+    apply nodefault_tail in Hd1.
+    apply nodefault_tail in Hd2.
+    apply nodefault_tail in Hd3.
+    specialize (IHm1 H Hd1 (Build_slist H3 Hd2) (Build_slist H5 Hd3)).
+    simpl in IHm1.
+    case (eq_dec d3 d3) in IHm1; intuition.
+  Qed.
+
+  Fixpoint lt_list (m m' : list (key * elt)) : Prop :=
+    match m, m' with
+    | nil, nil => False
+    | nil, _  => True
+    | _, nil  => False
+    | (x,e)::l, (x',e')::l' =>
+      match compare x x' with
+      | LT _ => True
+      | GT _ => False
+      | EQ _ => lt e e' \/ (e = e' /\ lt_list l l')
+      end
+    end.
+
+  Definition lt_farray m m' :=
+    lt m.(default) m'.(default) \/
+    (m.(default) = m'.(default) /\
+     lt_list m.(this) m'.(this)).
+
+  Lemma lt_farray_trans : forall m1 m2 m3 : farray,
+      lt_farray m1 m2 -> lt_farray m2 m3 -> lt_farray m1 m3.
+  Proof.
+    intros (m1,Hm1,d1,Hd1); induction m1;
+      intros (m2,Hm2,d2,Hd2); destruct m2;
+        intros (m3,Hm3,d3,Hd3); destruct m3; unfold lt_farray; simpl;
+          try destruct a as (x,e);
+          try destruct p as (x',e');
+          try destruct p0 as (x'',e''); try contradiction; intuition; auto;
+            try (left; apply (lt_trans d1 d2 d3); now auto);
+            try (left; subst; now auto);
+            try (right; subst; auto).
+    split; auto.
+    destruct (compare x x') as [Hlt|Heq|Hlt];
+      destruct (compare x' x'') as [Hlt'|Heq'|Hlt'];
+      destruct (compare x x'') as [Hlt''|Heq''|Hlt'']; intros; subst; auto; try easy.
+    apply (lt_trans x') in Hlt; apply lt_not_eq in Hlt.
+    now contradict Hlt. auto.
+    apply (lt_trans x') in Hlt; apply lt_not_eq in Hlt.
+    now contradict Hlt.
+    apply (lt_trans _ x'') ; auto.
+    apply lt_not_eq in Hlt. now contradict Hlt.
+    apply (lt_trans x'') in Hlt; apply lt_not_eq in Hlt.
+    now contradict Hlt. auto.
+    subst.
+    apply lt_not_eq in Hlt'. now contradict Hlt'.
+    apply (lt_trans x'') in Hlt'; apply lt_not_eq in Hlt'.
+    now contradict Hlt'. auto.
+    destruct H2, H3.
+    left; apply lt_trans with e'; auto.
+    left. destruct H0. subst; auto.
+    left. destruct H. subst; auto.
+    right. destruct H, H0. subst; split; auto.
+    inversion_clear Hm1; inversion_clear Hm2; inversion_clear Hm3.
+    apply nodefault_tail in Hd1.
+    apply nodefault_tail in Hd2.
+    apply nodefault_tail in Hd3.
+    specialize (IHm1 H Hd1 (Build_slist H3 Hd2) (Build_slist H5 Hd3)).
+    unfold lt_farray in IHm1. simpl in IHm1. destruct IHm1; auto.
+    apply lt_not_eq in H7. now contradict H7.
+    destruct H7; auto.
+    apply lt_not_eq in Hlt''. now contradict Hlt''.
+  Qed.
+
+  Lemma lt_farray_not_eq : forall m1 m2 : farray, lt_farray m1 m2 -> ~ eq m1 m2.
+  Proof.
+    intros (m1,Hm1,d1,Hd1); induction m1;
+      intros (m2,Hm2,d2,Hd2); destruct m2; unfold eq, lt, lt_farray; simpl;
+        try destruct a as (x,e);
+        try destruct p as (x',e'); try contradiction; auto; intuition;
+          destruct (eq_dec d1 d2); intuition.
+    apply lt_not_eq in H1. now contradict H1.
+    apply lt_not_eq in H1. now contradict H1.
+    destruct (compare x x') as [Hlt|Heq|Hlt]; auto.
+    (* intuition. *)
+    inversion_clear Hm1; inversion_clear Hm2.
+    specialize (nodefault_tail Hd2).
+    specialize (nodefault_tail Hd1). intros.
+    subst.
+    apply (IHm1 H1 H6 (Build_slist H4 H7)); intuition;
+      unfold lt_farray in *; simpl in *;
+        try (apply lt_not_eq in H0; now contradict H0).
+    right; split; auto.
+    unfold eq. simpl.
+    destruct (eq_dec d2 d2); intuition.
+  Qed.
+
+  Definition compare_farray : forall m1 m2, Compare lt_farray eq m1 m2.
+  Proof.
+    intros m1 m2.
+    destruct (compare m1.(default) m2.(default)).
+    - apply LT.
+      unfold lt_farray. simpl; auto.
+    - revert m1 m2 e.
+      intros (m1,Hm1,d1,Hd1); induction m1;
+      intros (m2,Hm2,d2,Hd2); destruct m2; simpl; intro He; subst;
+        [ apply EQ | apply LT | apply GT | ]; auto.
+    (* cmp_solve. *)
+      + unfold eq. simpl. destruct (eq_dec d2 d2); auto.
+      + unfold lt_farray. simpl. right; auto.
+      + unfold lt_farray. simpl. right; auto.
+      + destruct a as (x,e); destruct p as (x',e').
+        destruct (compare x x');
+          [ apply LT | | apply GT ].
+        unfold lt_farray. simpl.
+        destruct (compare x x'); auto.
+        subst. apply lt_not_eq in l; now contradict l.
+        apply (lt_trans x') in l; auto. subst. apply lt_not_eq in l; now contradict l.
+        (* subst. *)
+        destruct (compare e e');
+          [ apply LT | | apply GT ].
+         * unfold lt_farray. simpl.
+           destruct (compare x x'); auto;
+             try (subst; apply lt_not_eq in l0; now contradict l0).
+         * assert (Hm11 : sort (Raw.ltk key_ord) m1).
+           inversion_clear Hm1; auto.
+           assert (Hm22 : sort (Raw.ltk key_ord) m2).
+           inversion_clear Hm2; auto.
+           specialize (nodefault_tail Hd2). specialize (nodefault_tail Hd1).
+           intros Hd11 Hd22.
+           destruct (IHm1 Hm11 Hd11 (Build_slist Hm22 Hd22));
+             [ simpl; auto | apply LT | apply EQ | apply GT ].
+           -- unfold lt_farray in *. simpl in *.
+              destruct (compare x x'); auto;
+                try (subst; apply lt_not_eq in l0; now contradict l0).
+              intuition.
+           -- unfold eq in *. simpl in *.
+              destruct (compare x x'); auto;
+                try (subst; apply lt_not_eq in l; now contradict l).
+              destruct (eq_dec d2 d2); intuition.
+           -- unfold lt_farray in *. simpl in *.
+              destruct (compare x' x); auto;
+                try (subst; apply lt_not_eq in l0; now contradict l0).
+              intuition.
+         * unfold lt_farray in *. simpl.
+           destruct (compare x' x); auto;
+             try (subst; apply lt_not_eq in l0; now contradict l0).
+         * unfold lt_farray in *. simpl.
+           destruct (compare x' x); auto;
+             try (subst; apply lt_not_eq in l; now contradict l).
+           apply (lt_trans x) in l; auto.
+           apply lt_not_eq in l; now contradict l.
+    - apply GT.
+      unfold lt_farray. simpl; auto.
+  Qed.
+
+  Lemma eq_option_alt : forall (elt:Type)(o o':option elt),
+      o=o' <-> (forall e, o=Some e <-> o'=Some e).
+  Proof.
+    split; intros.
+    subst; split; auto.
+    destruct o; destruct o'; try rewrite H; auto.
+    symmetry; rewrite <- H; auto.
+  Qed.
+
+  Lemma find_mapsto_iff : forall m x e, MapsTo x e m <-> find x m = Some e.
+  Proof.
+    split; [apply find_1|apply find_2].
+  Qed.
+
+  Lemma add_neq_mapsto_iff : forall m x y e e',
+      x <> y -> (MapsTo y e' (add x e m)  <-> MapsTo y e' m).
+  Proof.
+    split; [apply add_3|apply add_2]; auto.
+  Qed.
+
+
+  Lemma add_eq_o : forall m x y e,
+      x = y -> e <> m.(default) -> find y (add x e m) = Some e.
+  Proof. intros.
+    apply find_1.
+    apply add_1; auto.
+  Qed.
+
+  Lemma raw_add_d_rem : forall m (Hm: Sorted (Raw.ltk key_ord) m) x d,
+      raw_add_nodefault x d d m = Raw.remove key_comp x m.
+    intros.
+    unfold raw_add_nodefault.
+    rewrite cmp_refl.
+    case_eq (Raw.mem key_comp x m); intro.
+    auto.
+    apply Raw.mem_3 in H; auto.
+    apply raw_equal_eq; auto.
+    apply Raw.remove_sorted; auto.
+    apply Raw.equal_1; auto.
+    apply Raw.remove_sorted; auto.
+    unfold Raw.Equivb.
+    split.
+    intros.
+    destruct (eq_dec x k). subst.
+    split. intro. contradiction.
+    intro. contradict H0.
+    apply Raw.remove_1; auto.
+    apply Raw.remove_4; auto.
+
+    intros.
+    destruct (eq_dec x k).
+    assert (exists e, InA (Raw.eqk (elt:=elt)) (k, e) (Raw.remove key_comp x m)).
+    exists e'. apply Raw.InA_eqke_eqk; auto.
+    rewrite <- Raw.In_alt in H2; auto.
+    contradict H2.
+    apply Raw.remove_1; auto.
+    apply key_comp.
+    apply (Raw.remove_2 key_comp Hm n) in H0.
+    specialize (Raw.remove_sorted key_comp Hm x). intros.
+    specialize (Raw.MapsTo_inj key_dec H2 H0 H1).
+    intro. subst. apply cmp_refl.
+  Qed.
+
+  Lemma add_d_rem : forall m x, add x m.(default) m = remove x m.
+    intros.
+    unfold add, remove.
+    specialize (raw_add_d_rem m.(sorted) x). intro.
+    generalize (add_sorted m.(default) m.(sorted) x m.(default)).
+    generalize (add_nodefault (nodefault m) (sorted m) x m.(default)).
+    generalize (Raw.remove_sorted key_comp (sorted m) x).
+    generalize (remove_nodefault (nodefault m) (sorted m) x).
+    rewrite H.
+    intros H4 H3 H2 H1.
+    rewrite (proof_irrelevance _ H1 H3), (proof_irrelevance _ H2 H4).
+    reflexivity.
+  Qed.
+
+  Lemma add_eq_d : forall m x y,
+      x = y -> find y (add x m.(default) m) = None.
+  Proof.
+    intros.
+    simpl.
+    rewrite add_d_rem.
+    case_eq (find y (remove x m)); auto.
+    intros.
+    apply find_2 in H0.
+    unfold MapsTo, Raw.MapsTo in H0.
+    assert (exists e, InA (Raw.eqk (elt:=elt)) (y, e) (remove x m).(this)).
+    exists e. apply Raw.InA_eqke_eqk in H0. auto.
+    rewrite <- Raw.In_alt in H1; auto.
+    contradict H1.
+    apply remove_1; auto.
+    apply key_comp.
+  Qed.
+
+  Lemma add_neq_o : forall m x y e,
+      ~ x = y -> find y (add x e m) = find y m.
+  Proof.
+    intros. rewrite eq_option_alt. intro e'. rewrite <- 2 find_mapsto_iff.
+    apply add_neq_mapsto_iff; auto.
+  Qed.
+  Hint Resolve add_neq_o.
+
+  Lemma MapsTo_fun : forall m x (e e':elt),
+      MapsTo x e m -> MapsTo x e' m -> e=e'.
+  Proof.
+    intros.
+    generalize (find_1 H) (find_1 H0); clear H H0.
+    intros; rewrite H in H0; injection H0; auto.
+  Qed.
+
+  (** Another characterisation of [Equal] *)
+
+  Lemma Equal_mapsto_iff : forall m1 m2 : farray,
+      Equal m1 m2 <->
+      (m1.(default) = m2.(default) /\ forall k e, MapsTo k e m1 <-> MapsTo k e m2).
+  Proof.
+    intros m1 m2. split.
+    intros Heq.
+    unfold Equal in Heq. destruct Heq as (Hd, Heq).
+    split; auto.
+    intros k e.
+    rewrite 2 find_mapsto_iff, Heq. split; auto.
+    intros (Hd, Hiff).
+    unfold Equal. split; auto.
+    intro k. rewrite eq_option_alt. intro e.
+    rewrite <- 2 find_mapsto_iff; auto.
+  Qed.
+
+  (** * Relations between [Equal], [Equiv] and [Equivb]. *)
+
+  (** First, [Equal] is [Equiv] with Leibniz on elements. *)
+
+  Lemma Equal_Equiv : forall (m m' : farray),
+      Equal m m' <-> Equiv m m'.
+  Proof.
+    intros. rewrite Equal_mapsto_iff. split; intros.
+    destruct H as (Hd, H).
+    split; auto.
+    split. intro k.
+    unfold In, Raw.In.
+    split; intros H0; destruct H0 as (e, H0);
+    exists e; unfold MapsTo in H; [rewrite <- H|rewrite H]; auto.
+    intros; apply MapsTo_fun with m k; auto; rewrite H; auto.
+    unfold Equiv in H. destruct H as (Hd, (Hi, Hm)).
+    split; auto. intros k e. split; intro H.
+    assert (Hin : In k m') by (rewrite <- Hi; exists e; auto).
+    destruct Hin as (e',He').
+    rewrite (Hm k e e'); auto.
+    assert (Hin : In k m) by (rewrite Hi; exists e; auto).
+    destruct Hin as (e',He').
+    rewrite <- (Hm k e' e); auto.
+  Qed.
+
+  Lemma Equiv_Equivb : forall m m', Equiv m m' <-> Equivb m m'.
+  Proof.
+    unfold Equiv, Equivb, Raw.Equivb, cmp; intuition.
+    specialize (H2 k e e' H1 H3).
+    destruct (compare e e'); auto; apply lt_not_eq in l; auto.
+    specialize (H2 k e e' H1 H3).
+    destruct (compare e e'); auto; now contradict H2.
+  Qed.
+
+  (** Composition of the two last results: relation between [Equal]
+    and [Equivb]. *)
+
+  Lemma Equal_Equivb : forall (m m':farray), Equal m m' <-> Equivb m m'.
+  Proof.
+    intros; rewrite Equal_Equiv.
+    apply Equiv_Equivb; auto.
+  Qed.
+
+  (** * Functional arrays with default value *)
+
+  Definition select (a: farray) (i: key) : elt :=
+    match find i a with
+    | Some v => v
+    | None => a.(default)
+    end.
+
+  Definition store (a: farray) (i: key) (v: elt) : farray := add i v a.
+
+  Lemma read_over_same_write : forall a i j v, i = j -> select (store a i v) j = v.
+  Proof.
+    intros a i j v Heq.
+    unfold select, store.
+    case_eq (cmp v a.(default)); intro; auto.
+    unfold cmp in H.
+    case (compare v a.(default)) in H; auto; try now contradict H.
+    rewrite e.
+    rewrite add_eq_d; auto.
+    assert (v <> a.(default)).
+    unfold cmp in H.
+    case (compare v a.(default)) in H; auto; try now contradict H.
+    apply lt_not_eq in l. auto.
+    apply lt_not_eq in l. auto.
+    rewrite (add_eq_o a Heq H0). auto.
+  Qed.
+
+  Lemma read_over_write : forall a i v, select (store a i v) i = v.
+  Proof.
+    intros; apply read_over_same_write; auto.
+  Qed.
+
+  Lemma read_over_other_write : forall a i j v,
+      i <> j -> select (store a i v) j = select a j.
+  Proof.
+    intros a i j v Hneq.
+    unfold select, store.
+    apply (add_neq_o a v) in Hneq.
+    rewrite Hneq. auto.
+  Qed.
+
+  Lemma find_ext_dec:
+    (forall m1 m2: farray, Equal m1 m2 -> (equal m1 m2) = true).
+  Proof. intros.
+    apply Equal_Equivb in H.
+    apply equal_1.
+    exact H.
+  Qed.
+
+  (** Provable only if [elt] is an infinite type *)
+  Lemma extensionnality_eqb : forall a b,
+      (forall i, select a i = select b i) -> equal a b = true.
+  Proof.
+    intros.
+    unfold select in H.
+    (* assert ((exists i : key, find i a = None) -> a.(default) = b.(default)). *)
+    (* { *)
+    (*   intros. destruct H0. *)
+    (*   specialize (H x). *)
+    (*   rewrite H0 in H. *)
+    (*   i. specialize (H i). *)
+      
+    (*   case_eq (find i a); *)
+    (*     case_eq (find i b). *)
+    (*     intros. rewrite H0 in *; rewrite H1 in *. subst; auto. *)
+
+    (* } *)
+    
+    cut (a.(default) = b.(default)). intro Hd.
+    assert (forall i, find i a = find i b).
+    {
+      intro i. specialize (H i).
+      case_eq (find i a); case_eq (find i b);
+        intros; rewrite H0 in *; rewrite H1 in *; subst; auto.
+      + apply find_2 in H1.
+        contradict H1.
+        unfold MapsTo.
+        rewrite <- Hd.
+        apply a.(nodefault).
+      + apply find_2 in H0.
+        contradict H0.
+        unfold MapsTo.
+        rewrite Hd.
+        apply b.(nodefault).
+    }
+    apply find_ext_dec. split; auto.
+    cut (exists k, find k a = None /\ find k b = None). intro.
+    destruct H0 as (k, (Ha, Hb)). specialize (H k).
+    rewrite Ha, Hb in H. auto.
+    destruct a, b; simpl in *.
+    (* No *)
+  Qed.
+
+  Lemma equal_eq : forall a b, equal a b = true -> a = b.
+  Proof. intros. apply eq_equal in H.
+    destruct a as (a, asort, anodef), b as (b, bsort, bnodef).
+    unfold eq in H.
+    revert b bsort bnodef H.
+    induction a; intros; destruct b.
+    rewrite (proof_irrelevance _ asort bsort).
+    rewrite (proof_irrelevance _ anodef bnodef).
+    auto.
+    simpl in H. now contradict H.
+    simpl in H. destruct a; now contradict H.
+    simpl in H. destruct a, p.
+    destruct (compare k k0); auto; try (now contradict H).
+    destruct H.
+    subst.
+    inversion_clear asort.
+    inversion_clear bsort.
+    specialize (nodefault_tail bnodef).
+    specialize (nodefault_tail anodef). intros.
+    specialize (IHa H H4 b H2 H5 H0).
+    inversion IHa. subst.
+    rewrite (proof_irrelevance _ asort bsort).
+    rewrite (proof_irrelevance _ anodef bnodef).
+    reflexivity.
+ Qed.
+
+  Lemma notequal_neq : forall a b, equal a b = false -> a <> b.
+    intros.
+    red. intros.
+    apply not_true_iff_false in H.
+    unfold not in *. intros.
+    apply H. rewrite H0.
+    apply eq_equal. apply eqfarray_refl.
+  Qed.
+
+  Lemma extensionnality : forall a b, (forall i, select a i = select b i) -> a = b.
+  Proof.
+    intros; apply equal_eq; apply extensionnality_eqb; auto.
+  Qed.
+
+(** farray equal in Prop *)
+  Definition equalP (m m' : farray) : Prop :=
+    if equal m m' then True else False.
+
+  Lemma eq_list_refl: forall a, eq_list a a.
+  Proof.
+    intro a.
+    induction a; intros.
+    - now simpl.
+    - simpl. destruct a as (k, e).
+      case_eq (compare k k); intros.
+      + revert H. generalize l.
+        apply lt_not_eq in l. now contradict l.
+      + split; easy.
+      + revert H. generalize l.
+        apply lt_not_eq in l. now contradict l.
+  Qed.
+
+  Lemma equal_refl: forall a, equal a a = true.
+  Proof. intros; apply eq_equal; apply eq_list_refl. Qed.
+
+  Lemma equal_eqP : forall a b, equalP a b <-> a = b.
+  Proof. 
+     intros. split; intro H. unfold equalP in H.
+     case_eq (equal a b); intros; rewrite H0 in H.
+     now apply equal_eq. now contradict H.
+     rewrite H. unfold equalP.
+     now rewrite equal_refl.
+  Qed.
+
+ Lemma equal_B2P: forall (m m' : farray),
+                  equal m m' = true <-> equalP m m'.
+ Proof.
+     intros. split; intros.
+     apply equal_eq in H. rewrite H.
+     unfold equalP. now rewrite equal_refl.
+     apply equal_eqP in H.
+     now rewrite H, equal_refl.
+ Qed.
+
+  Section Classical_extensionnality.
+
+    Require Import Classical_Pred_Type ClassicalEpsilon.
+
+    Lemma extensionnality2 : forall a b, a <> b -> (exists i, select a i <> select b i).
+    Proof.
+      intros.
+      apply not_all_ex_not.
+      unfold not in *.
+      intros. apply H. apply extensionnality; auto.
+    Qed.
+
+    Definition diff_index_p : forall a b, a <> b -> { i | select a i <> select b i } :=
+      (fun a b u => constructive_indefinite_description _ (@extensionnality2 _ _ u)).
+
+    Definition diff_index : forall a b, a <> b -> key :=
+      (fun a b u => proj1_sig (diff_index_p u)).
+
+
+    Example d : forall a b (u:a <> b), let i := diff_index u in select a i <> select b i.
+      unfold diff_index.
+      intros.
+      destruct (diff_index_p u). simpl. auto.
+    Qed.
+
+    Definition diff (a b: farray) : key.
+      case_eq (equal a b); intro.
+      - apply default_value.
+      - apply (diff_index (notequal_neq H)).
+        (* destruct (diff_index_p H). apply x. *)
+    Defined.
+
+   Lemma select_at_diff: forall a b, a <> b ->
+            select a (diff a b) <> select b (diff a b).
+   Proof.
+     intros a b H. unfold diff.
+     assert (equal a b = false).
+     apply not_true_iff_false.
+     red. intro. apply equal_eq in H0. subst. auto.
+     generalize (@notequal_neq a b).
+     rewrite H0.
+     intro.
+     unfold diff_index.
+     destruct (diff_index_p (n Logic.eq_refl)). simpl; auto.
+   Qed.
+
+  End Classical_extensionnality.
+
+End FArray.
+
+Arguments farray _ _ {_} {_}.
+Arguments select {_} {_} {_} {_} {_} _ _.
+Arguments store {_} {_} {_} {_} {_} {_} {_} {_} _ _ _.
+Arguments diff {_} {_} {_} {_} {_} {_} {_} {_} {_} {_} _ _.
+Arguments equal {_} {_} {_} {_} {_} {_} {_}  _ _.
+Arguments equalP {_} {_} {_} {_} {_} {_} {_}  _ _.
+
+
+Notation "a '[' i ']'" := (select a i) (at level 1, format "a [ i ]") : farray_scope.
+Notation "a '[' i '<-' v ']'" := (store a i v)
+   (at level 1, format "a [ i  <-  v ]") : farray_scope.
+
+
+
+(* 
+   Local Variables:
+   coq-load-path: ((rec ".." "SMTCoq"))
+   End: 
+*)