(*
 * This code was developped by IDEALX (http://IDEALX.org/) and
 * contributors (their names can be found in the CONTRIBUTORS file). It 
 * is released under the terms of the BSD license (see LICENCE file
 * for details). 
*)


(******************************************************************
 *          	      ASSOCIATIVE ARRAYS V0.1 (April 2001)
 *
 *
 ******************************************************************
 *
 *   We define the associative array (key -> value associations) 
 * datatype as list of couples, providing definitions of standards 
 * operations such as adding, deleting. 
 *   
 *   We introduce predicates for membership of a key and of couples. 
 *   
 *   Finally we define a search operator ("find") which returns the 
 * value associated with a key or the "none" option (see file 
 * Option.v which should be part of this contribution) on failure.
 * 
 *   Lemmas we prove about these concepts were motivated by our 
 * needs at the moment we created this file. We hope they'll suit 
 * your needs too but anyway, feel free to communicate any wish 
 *  or remark.
 *
 ******************************************************************)

Unset Standard Proposition Elimination Names.









Section associative_arrays.

Set Asymmetric Patterns.
Set Strict Implicit.
Unset Implicit Arguments.

Require Import List.
Require Import Option.

Variable K : Set. 
Variable V : Set. 

Hypothesis Keq_dec : forall x y : K, {x = y} + {x <> y}.


Record Tuple : Set := mkTuple {k : K; v : V}.




(**************************************************)
(* Definitions                                    *)
(**************************************************)



Definition assoc := list Tuple.  
(* <Warning> : Syntax is discontinued *) 


Definition assoc_empty := nil (A:=Tuple).


(* search function : locate a value by its key *)
Fixpoint assoc_find (l : assoc) : K -> option V :=
  fun k0 : K =>
  match l with
  | nil => none V
  | mkTuple k v :: l' =>
      match Keq_dec k k0 with
      | left _ => some V v
      | right _ => assoc_find l' k0
      end
  end.


(* function to add an entry in an array:  may replace an existing entry
  if the key is already present in the array *)
Fixpoint assoc_add (l : assoc) : K -> V -> assoc :=
  fun (k0 : K) (v0 : V) =>
  match l with
  | nil => mkTuple k0 v0 :: nil
  | mkTuple k v :: l' =>
      match Keq_dec k k0 with
      | left _ => mkTuple k0 v0 :: l'
      | _ => mkTuple k v :: assoc_add l' k0 v0
      end
  end.


(* remove an entry from an array or do nothing if the key isn't
    present in the array *) 
Fixpoint assoc_delete (l : assoc) : K -> assoc :=
  fun k0 : K =>
  match l with
  | nil => nil (A:=Tuple)
  | mkTuple k v :: l' =>
      match Keq_dec k k0 with
      | left _ => assoc_delete l' k0
      | _ => mkTuple k v :: assoc_delete l' k0
      end
  end.


(* tests the existence of a key in an array *)
Definition assoc_mem (l : assoc) (k : K) : Prop :=
  match assoc_find l k with
  | some _ => True
  | _ => False
  end.


(* tests the existence of the specified tuple in an array *)
Definition assoc_hasmem (l : assoc) (k : K) (v : V) : Prop :=
  match assoc_find l k with
  | some v' => v = v'
  | _ => False
  end.


(* definition of equal functions from keys to values option *)
Definition assoc_eqm (f1 f2 : K -> option V) := forall k : K, f1 k = f2 k.
 

(* definition of almost-everywhere-equal functions from keys 
  to values option *)
Definition assoc_almost_eqm (k0 : K) (f1 f2 : K -> option V) :=
  forall k : K, k <> k0 -> f1 k = f2 k.




(**************************************************)
(* Some properties about eqm functions            *)
(**************************************************)



Lemma assoc_almost_eqm_trans :
 forall (k : K) (f1 f2 f3 : K -> option V),
 assoc_almost_eqm k f1 f2 ->
 assoc_almost_eqm k f2 f3 -> assoc_almost_eqm k f1 f3.

Proof.
(* Goal: forall (k : K) (f1 f2 f3 : forall _ : K, option V) (_ : assoc_almost_eqm k f1 f2) (_ : assoc_almost_eqm k f2 f3), assoc_almost_eqm k f1 f3 *)
  intros k0 f1 f2 f3.
(* Goal: assoc_almost_eqm k0 (assoc_find (@cons Tuple a l)) (assoc_find (@cons Tuple a l')) *)
  unfold assoc_almost_eqm in |- *.
(* Goal: forall (_ : forall (k : K) (_ : not (@eq K k k0)), @eq (option V) (f1 k) (f2 k)) (_ : forall (k : K) (_ : not (@eq K k k0)), @eq (option V) (f2 k) (f3 k)) (k : K) (_ : not (@eq K k k0)), @eq (option V) (f1 k) (f3 k) *)
  intros H1 H2.
(* Goal: forall (k : K) (_ : not (@eq K k k0)), @eq (option V) (f1 k) (f3 k) *)
  intros k1 Kdiff.
(* Goal: @eq (option V) (f1 k1) (f3 k1) *)
  replace (f1 k1) with (f2 k1).
(* Goal: @eq (option V) (f2 k1) (f3 k1) *)
(* Goal: @eq (option V) (f2 k1) (f1 k1) *)
  apply H2.
(* Goal: assoc_almost_eqm k0 (assoc_find l) (assoc_find (@cons Tuple (mkTuple k0 v') l)) *)
(* Goal: assoc_almost_eqm k0 (assoc_find (@cons Tuple (mkTuple k0 v0) l)) (assoc_find l) *)
(* Goal: assoc_almost_eqm k0 (assoc_find l) (assoc_find (@cons Tuple (mkTuple k0 v') l)) *)
  assumption.

(* Goal: @eq (option V) (f2 k1) (f1 k1) *)
  elim H1.
(* Goal: forall (k : K) (v : V) (k0 : K), @eq (option V) (assoc_find (@cons Tuple (mkTuple k v) (@nil Tuple)) k0) (assoc_find (@cons Tuple (mkTuple k v) (@nil Tuple)) k0) *)
(* Goal: forall (k : K) (v : V), assoc_eqm (assoc_find (@cons Tuple (mkTuple k v) (@cons Tuple a t))) (assoc_find (assoc_add (@cons Tuple a t) k v)) *)
  trivial.

(* Goal: forall (k : K) (v : V) (k0 : K), @eq (option V) (assoc_find (@cons Tuple (mkTuple k v) (@nil Tuple)) k0) (assoc_find (@cons Tuple (mkTuple k v) (@nil Tuple)) k0) *)
(* Goal: forall (k : K) (v : V), assoc_eqm (assoc_find (@cons Tuple (mkTuple k v) (@cons Tuple a t))) (assoc_find (assoc_add (@cons Tuple a t) k v)) *)
  trivial.
Qed.


Lemma assoc_almost_eqm_sym :
 forall (k : K) (f1 f2 : K -> option V),
 assoc_almost_eqm k f1 f2 -> assoc_almost_eqm k f2 f1.

Proof.
(* Goal: forall (k : K) (f1 f2 : forall _ : K, option V) (_ : assoc_almost_eqm k f1 f2), assoc_almost_eqm k f2 f1 *)
  intros k0 f1 f2.
(* Goal: assoc_almost_eqm k0 (assoc_find (@cons Tuple a l)) (assoc_find (@cons Tuple a l')) *)
  unfold assoc_almost_eqm in |- *.
(* Goal: forall (_ : forall (k : K) (_ : not (@eq K k k0)), @eq (option V) (f1 k) (f2 k)) (k : K) (_ : not (@eq K k k0)), @eq (option V) (f2 k) (f1 k) *)
  intro H.
(* Goal: forall (k : K) (_ : not (@eq K k k0)), @eq (option V) (f2 k) (f1 k) *)
  intros k1 kdiff.
(* Goal: @eq (option V) (some V v1) (some V v0) *)
(* Goal: forall _ : not (@eq K k0 k1), @eq (option V) (some V v1) (some V v1) *)
(* Goal: forall _ : not (@eq K k1 k2), @eq (option V) (if Keq_dec k0 k2 then some V v0 else (fix assoc_find (l : assoc) (k0 : K) {struct l} : option V := match l with | nil => none V | cons ({| k := k; v := v |} as t) l' => if Keq_dec k k0 then some V v else assoc_find l' k0 end) l k2) (if Keq_dec k0 k2 then some V v0 else (fix assoc_find (l : assoc) (k0 : K) {struct l} : option V := match l with | nil => none V | cons ({| k := k; v := v |} as t) l' => if Keq_dec k k0 then some V v else assoc_find l' k0 end) l k2) *)
  elim H.
(* Goal: forall (k : K) (v : V) (k0 : K), @eq (option V) (assoc_find (@cons Tuple (mkTuple k v) (@nil Tuple)) k0) (assoc_find (@cons Tuple (mkTuple k v) (@nil Tuple)) k0) *)
(* Goal: forall (k : K) (v : V), assoc_eqm (assoc_find (@cons Tuple (mkTuple k v) (@cons Tuple a t))) (assoc_find (assoc_add (@cons Tuple a t) k v)) *)
  trivial.

(* Goal: forall (k : K) (v : V) (k0 : K), @eq (option V) (assoc_find (@cons Tuple (mkTuple k v) (@nil Tuple)) k0) (assoc_find (@cons Tuple (mkTuple k v) (@nil Tuple)) k0) *)
(* Goal: forall (k : K) (v : V), assoc_eqm (assoc_find (@cons Tuple (mkTuple k v) (@cons Tuple a t))) (assoc_find (assoc_add (@cons Tuple a t) k v)) *)
  trivial.
Qed.


Lemma assoc_eqm_trans :
 forall f1 f2 f3 : K -> option V,
 assoc_eqm f1 f2 -> assoc_eqm f2 f3 -> assoc_eqm f1 f3.

Proof.
(* Goal: forall (f1 f2 f3 : forall _ : K, option V) (_ : assoc_eqm f1 f2) (_ : assoc_eqm f2 f3), assoc_eqm f1 f3 *)
intros f1 f2 f3.
(* Goal: forall _ : assoc_eqm (assoc_find (@cons Tuple (mkTuple k' v') l0)) (assoc_find (assoc_add l0 k' v')), @eq (option V) (assoc_find (@cons Tuple (mkTuple k' v') l0) k0) (assoc_find (assoc_add l0 k' v') k0) *)
(* Goal: assoc_eqm (assoc_find (@cons Tuple (mkTuple k' v') l0)) (assoc_find (assoc_add l0 k' v')) *)
unfold assoc_eqm in |- *.
(* Goal: forall (_ : forall k : K, @eq (option V) (f1 k) (f2 k)) (_ : forall k : K, @eq (option V) (f2 k) (f3 k)) (k : K), @eq (option V) (f1 k) (f3 k) *)
intros H1 H2 k0.
(* Goal: @eq (option V) (f1 k0) (f3 k0) *)
transitivity (f2 k0).
(* Goal: forall (k : K) (v : V) (k0 : K), @eq (option V) (assoc_find (@cons Tuple (mkTuple k v) (@nil Tuple)) k0) (assoc_find (@cons Tuple (mkTuple k v) (@nil Tuple)) k0) *)
(* Goal: forall (k : K) (v : V), assoc_eqm (assoc_find (@cons Tuple (mkTuple k v) (@cons Tuple a t))) (assoc_find (assoc_add (@cons Tuple a t) k v)) *)
elim H1; trivial.
 
(* Goal: forall (k : K) (v : V) (k0 : K), @eq (option V) (assoc_find (@cons Tuple (mkTuple k v) (@nil Tuple)) k0) (assoc_find (@cons Tuple (mkTuple k v) (@nil Tuple)) k0) *)
(* Goal: forall (k : K) (v : V), assoc_eqm (assoc_find (@cons Tuple (mkTuple k v) (@cons Tuple a t))) (assoc_find (assoc_add (@cons Tuple a t) k v)) *)
elim H2; trivial.
Qed.




(**************************************************)
(* assoc_find properties                          *)
(**************************************************)



Lemma assoc_semfind_nil :
 assoc_eqm (assoc_find assoc_empty) (fun k : K => none V).

Proof.
(* Goal: forall _ : match assoc_find (@cons Tuple (mkTuple k' v') l0) k0 with | @none _ => False | @some _ v' => @eq V v0 v' end, @eq K k' k0 *)
(* Goal: @eq (option V) (assoc_find (@cons Tuple (mkTuple k' v') l0) k0) (assoc_find (assoc_add l0 k' v') k0) *)
  simpl in |- *.
(* Goal: forall _ : assoc_eqm (assoc_find (@cons Tuple (mkTuple k' v') l0)) (assoc_find (assoc_add l0 k' v')), @eq (option V) (assoc_find (@cons Tuple (mkTuple k' v') l0) k0) (assoc_find (assoc_add l0 k' v') k0) *)
(* Goal: assoc_eqm (assoc_find (@cons Tuple (mkTuple k' v') l0)) (assoc_find (assoc_add l0 k' v')) *)
  unfold assoc_eqm in |- *.
(* Goal: forall (k : K) (v : V) (k0 : K), @eq (option V) (assoc_find (@cons Tuple (mkTuple k v) (@nil Tuple)) k0) (assoc_find (@cons Tuple (mkTuple k v) (@nil Tuple)) k0) *)
(* Goal: forall (k : K) (v : V), assoc_eqm (assoc_find (@cons Tuple (mkTuple k v) (@cons Tuple a t))) (assoc_find (assoc_add (@cons Tuple a t) k v)) *)
  trivial.
Qed.


Lemma assoc_semfind_cons_1 :
 forall (k : K) (v : V) (l : assoc),
 assoc_almost_eqm k (assoc_find (mkTuple k v :: l)) (assoc_find l).

Proof.
(* Goal: forall (_ : not (@eq K k' k0)) (_ : @eq (option V) (some V v0) (assoc_find l0 k0)), @eq K k' k0 *)
(* Goal: @eq (option V) (assoc_find (@cons Tuple (mkTuple k' v') l0) k0) (assoc_find (assoc_add l0 k' v') k0) *)
intros.
(* Goal: assoc_almost_eqm k0 (assoc_find (@cons Tuple a l)) (assoc_find (@cons Tuple a l')) *)
unfold assoc_almost_eqm in |- *.
(* Goal: forall (_ : not (@eq K k' k0)) (_ : @eq (option V) (some V v0) (assoc_find l0 k0)), @eq K k' k0 *)
(* Goal: @eq (option V) (assoc_find (@cons Tuple (mkTuple k' v') l0) k0) (assoc_find (assoc_add l0 k' v') k0) *)
intros.
(* Goal: @eq (option V) (assoc_find (@cons Tuple (mkTuple k0 v0) l) k1) (assoc_find l k1) *)
unfold assoc_find at 1 in |- *.
(* Goal: forall _ : not (@eq K k0 k1), not match (if Keq_dec k0 k1 then some V v0 else assoc_find (assoc_delete l0 k1) k1) with | @none _ => False | @some _ v' => @eq V v1 v' end *)
case (Keq_dec k0 k1).
(* Goal: forall (_ : forall (k : K) (_ : not (@eq K k k')), @eq (option V) (assoc_find l k) (assoc_find l' k)) (_ : match assoc_find l' k0 with | @none _ => False | @some _ v' => @eq V v0 v' end), match assoc_find l k0 with | @none _ => False | @some _ v' => @eq V v0 v' end *)
(* Goal: assoc_almost_eqm k' (assoc_find l) (assoc_find l') *)
intro.
(* Goal: @eq (option V) (some V v1) (some V v0) *)
(* Goal: forall _ : not (@eq K k0 k1), @eq (option V) (some V v1) (some V v1) *)
(* Goal: forall _ : not (@eq K k1 k2), @eq (option V) (if Keq_dec k0 k2 then some V v0 else (fix assoc_find (l : assoc) (k0 : K) {struct l} : option V := match l with | nil => none V | cons ({| k := k; v := v |} as t) l' => if Keq_dec k k0 then some V v else assoc_find l' k0 end) l k2) (if Keq_dec k0 k2 then some V v0 else (fix assoc_find (l : assoc) (k0 : K) {struct l} : option V := match l with | nil => none V | cons ({| k := k; v := v |} as t) l' => if Keq_dec k k0 then some V v else assoc_find l' k0 end) l k2) *)
elim H.
(* Goal: @eq K k1 k0 *)
(* Goal: forall _ : not (@eq K k0 k1), @eq (option V) ((fix assoc_find (l : assoc) (k0 : K) {struct l} : option V := match l with | nil => none V | cons ({| k := k; v := v |} as t) l' => if Keq_dec k k0 then some V v else assoc_find l' k0 end) l k1) (assoc_find l k1) *)
rewrite <- e.
(* Goal: forall (k : K) (v : V) (k0 : K), @eq (option V) (assoc_find (@cons Tuple (mkTuple k v) (@nil Tuple)) k0) (assoc_find (@cons Tuple (mkTuple k v) (@nil Tuple)) k0) *)
(* Goal: forall (k : K) (v : V), assoc_eqm (assoc_find (@cons Tuple (mkTuple k v) (@cons Tuple a t))) (assoc_find (assoc_add (@cons Tuple a t) k v)) *)
trivial.
(* Goal: forall (_ : not (@eq K k' k0)) (_ : @eq (option V) (some V v0) (assoc_find l0 k0)), @eq K k' k0 *)
(* Goal: @eq (option V) (assoc_find (@cons Tuple (mkTuple k' v') l0) k0) (assoc_find (assoc_add l0 k' v') k0) *)
intros.
(* Goal: forall (k : K) (v : V) (k0 : K), @eq (option V) (assoc_find (@cons Tuple (mkTuple k v) (@nil Tuple)) k0) (assoc_find (@cons Tuple (mkTuple k v) (@nil Tuple)) k0) *)
(* Goal: forall (k : K) (v : V), assoc_eqm (assoc_find (@cons Tuple (mkTuple k v) (@cons Tuple a t))) (assoc_find (assoc_add (@cons Tuple a t) k v)) *)
trivial.
Qed.


Lemma assoc_semfind_cons_2 :
 forall (k : K) (v : V) (l : assoc),
 assoc_find (mkTuple k v :: l) k = some V v.

Proof.
(* Goal: @eq (option V) (assoc_find (@cons Tuple (mkTuple k1 v1) (@cons Tuple (mkTuple k0 v0) l)) k2) (assoc_find (@cons Tuple (mkTuple k0 v0) (@cons Tuple (mkTuple k1 v1) l)) k2) *)
unfold assoc_find in |- *.
(* Goal: forall (_ : not (@eq K k' k0)) (_ : @eq (option V) (some V v0) (assoc_find l0 k0)), @eq K k' k0 *)
(* Goal: @eq (option V) (assoc_find (@cons Tuple (mkTuple k' v') l0) k0) (assoc_find (assoc_add l0 k' v') k0) *)
intros.
(* Goal: @eq (option V) (if Keq_dec k0 k0 then some V v0 else (fix assoc_find (l : assoc) (k0 : K) {struct l} : option V := match l with | nil => none V | cons ({| k := k; v := v |} as t) l' => if Keq_dec k k0 then some V v else assoc_find l' k0 end) l k0) (some V v0) *)
case (Keq_dec k0 k0).
(* Goal: forall (_ : @eq K k' k0) (_ : @eq V v0 v'), @eq K k' k0 *)
(* Goal: forall (_ : not (@eq K k' k0)) (_ : match assoc_find l0 k0 with | @none _ => False | @some _ v' => @eq V v0 v' end), @eq K k' k0 *)
(* Goal: @eq (option V) (assoc_find (@cons Tuple (mkTuple k' v') l0) k0) (assoc_find (assoc_add l0 k' v') k0) *)
auto.
(* Goal: forall (_ : forall (k : K) (_ : not (@eq K k k')), @eq (option V) (assoc_find l k) (assoc_find l' k)) (_ : match assoc_find l' k0 with | @none _ => False | @some _ v' => @eq V v0 v' end), match assoc_find l k0 with | @none _ => False | @some _ v' => @eq V v0 v' end *)
(* Goal: assoc_almost_eqm k' (assoc_find l) (assoc_find l') *)
intro.
(* Goal: @eq (option V) ((fix assoc_find (l : assoc) (k0 : K) {struct l} : option V := match l with | nil => none V | cons ({| k := k; v := v |} as t) l' => if Keq_dec k k0 then some V v else assoc_find l' k0 end) l k0) (some V v0) *)
elim n.
(* Goal: forall (_ : @eq K k' k0) (_ : @eq V v0 v'), @eq K k' k0 *)
(* Goal: forall (_ : not (@eq K k' k0)) (_ : match assoc_find l0 k0 with | @none _ => False | @some _ v' => @eq V v0 v' end), @eq K k' k0 *)
(* Goal: @eq (option V) (assoc_find (@cons Tuple (mkTuple k' v') l0) k0) (assoc_find (assoc_add l0 k' v') k0) *)
auto.
Qed.


Lemma assoc_semfind_change_valeur :
 forall (k : K) (v v' : V) (l : assoc),
 assoc_almost_eqm k (assoc_find (mkTuple k v :: l))
   (assoc_find (mkTuple k v' :: l)).

Proof.
(* Goal: forall (_ : not (@eq K k' k0)) (_ : @eq (option V) (some V v0) (assoc_find l0 k0)), @eq K k' k0 *)
(* Goal: @eq (option V) (assoc_find (@cons Tuple (mkTuple k' v') l0) k0) (assoc_find (assoc_add l0 k' v') k0) *)
intros.
(* Goal: assoc_almost_eqm k0 (assoc_find (@cons Tuple (mkTuple k0 v0) l)) (assoc_find (@cons Tuple (mkTuple k0 v') l)) *)
cut (assoc_almost_eqm k0 (assoc_find l) (assoc_find (mkTuple k0 v' :: l))).
(* Goal: forall _ : assoc_almost_eqm k0 (assoc_find l) (assoc_find (@cons Tuple (mkTuple k0 v') l)), assoc_almost_eqm k0 (assoc_find (@cons Tuple (mkTuple k0 v0) l)) (assoc_find (@cons Tuple (mkTuple k0 v') l)) *)
(* Goal: assoc_almost_eqm k0 (assoc_find l) (assoc_find (@cons Tuple (mkTuple k0 v') l)) *)
cut (assoc_almost_eqm k0 (assoc_find (mkTuple k0 v0 :: l)) (assoc_find l)).
(* Goal: forall (_ : not (@eq K k' k0)) (_ : @eq (option V) (some V v0) (assoc_find l0 k0)), @eq K k' k0 *)
(* Goal: @eq (option V) (assoc_find (@cons Tuple (mkTuple k' v') l0) k0) (assoc_find (assoc_add l0 k' v') k0) *)
intros.
(* Goal: assoc_almost_eqm k0 (assoc_find (@cons Tuple (mkTuple k0 v0) l)) (assoc_find (@cons Tuple (mkTuple k0 v') l)) *)
(* Goal: assoc_almost_eqm k0 (assoc_find (@cons Tuple (mkTuple k0 v0) l)) (assoc_find l) *)
(* Goal: assoc_almost_eqm k0 (assoc_find l) (assoc_find (@cons Tuple (mkTuple k0 v') l)) *)
apply assoc_almost_eqm_trans with (assoc_find l).
(* Goal: assoc_almost_eqm k0 (assoc_find l) (assoc_find (@cons Tuple (mkTuple k0 v') l)) *)
(* Goal: assoc_almost_eqm k0 (assoc_find (@cons Tuple (mkTuple k0 v0) l)) (assoc_find l) *)
(* Goal: assoc_almost_eqm k0 (assoc_find l) (assoc_find (@cons Tuple (mkTuple k0 v') l)) *)
assumption.
 
(* Goal: assoc_almost_eqm k0 (assoc_find l) (assoc_find (@cons Tuple (mkTuple k0 v') l)) *)
(* Goal: assoc_almost_eqm k0 (assoc_find (@cons Tuple (mkTuple k0 v0) l)) (assoc_find l) *)
(* Goal: assoc_almost_eqm k0 (assoc_find l) (assoc_find (@cons Tuple (mkTuple k0 v') l)) *)
assumption.
 
(* Goal: assoc_almost_eqm k0 (assoc_find (@cons Tuple (mkTuple k0 v') l)) (assoc_find l) *)
apply assoc_semfind_cons_1.
 
(* Goal: assoc_almost_eqm k' (assoc_find l') (assoc_find l) *)
apply assoc_almost_eqm_sym.
(* Goal: assoc_almost_eqm k0 (assoc_find (@cons Tuple (mkTuple k0 v') l)) (assoc_find l) *)
apply assoc_semfind_cons_1.
Qed.


Lemma assoc_semfind_increase_1 :
 forall (a : Tuple) (l l' : assoc),
 assoc_eqm (assoc_find l) (assoc_find l') ->
 assoc_eqm (assoc_find (a :: l)) (assoc_find (a :: l')).

Proof.
(* Goal: forall _ : assoc_eqm (assoc_find (@cons Tuple (mkTuple k' v') l0)) (assoc_find (assoc_add l0 k' v')), @eq (option V) (assoc_find (@cons Tuple (mkTuple k' v') l0) k0) (assoc_find (assoc_add l0 k' v') k0) *)
(* Goal: assoc_eqm (assoc_find (@cons Tuple (mkTuple k' v') l0)) (assoc_find (assoc_add l0 k' v')) *)
unfold assoc_eqm in |- *.
(* Goal: forall (_ : not (@eq K k' k0)) (_ : @eq (option V) (some V v0) (assoc_find l0 k0)), @eq K k' k0 *)
(* Goal: @eq (option V) (assoc_find (@cons Tuple (mkTuple k' v') l0) k0) (assoc_find (assoc_add l0 k' v') k0) *)
intros.
induction  a as (k1, v0).
unfold assoc_find in |- *; case (Keq_dec k1 k0); fold assoc_find in |- *;
(* Goal: forall (_ : @eq K k' k0) (_ : @eq V v0 v'), @eq K k' k0 *)
(* Goal: forall (_ : not (@eq K k' k0)) (_ : match assoc_find l0 k0 with | @none _ => False | @some _ v' => @eq V v0 v' end), @eq K k' k0 *)
(* Goal: @eq (option V) (assoc_find (@cons Tuple (mkTuple k' v') l0) k0) (assoc_find (assoc_add l0 k' v') k0) *)
 auto.
Qed.


Lemma assoc_semfind_increase_2 :
 forall (k : K) (a : Tuple) (l l' : assoc),
 assoc_almost_eqm k (assoc_find l) (assoc_find l') ->
 assoc_almost_eqm k (assoc_find (a :: l)) (assoc_find (a :: l')).

Proof.
(* Goal: forall (_ : not (@eq K k' k0)) (_ : @eq (option V) (some V v0) (assoc_find l0 k0)), @eq K k' k0 *)
(* Goal: @eq (option V) (assoc_find (@cons Tuple (mkTuple k' v') l0) k0) (assoc_find (assoc_add l0 k' v') k0) *)
intros.
(* Goal: assoc_almost_eqm k0 (assoc_find (@cons Tuple a l)) (assoc_find (@cons Tuple a l')) *)
unfold assoc_almost_eqm in |- *.
(* Goal: forall (_ : not (@eq K k' k0)) (_ : @eq (option V) (some V v0) (assoc_find l0 k0)), @eq K k' k0 *)
(* Goal: @eq (option V) (assoc_find (@cons Tuple (mkTuple k' v') l0) k0) (assoc_find (assoc_add l0 k' v') k0) *)
intros.
(* Goal: @eq (option V) (assoc_find (@cons Tuple (mkTuple k1 v1) (@cons Tuple (mkTuple k0 v0) l)) k2) (assoc_find (@cons Tuple (mkTuple k0 v0) (@cons Tuple (mkTuple k1 v1) l)) k2) *)
unfold assoc_find in |- *.
induction  a as (k2, v0).
(* Goal: forall _ : match assoc_find (if Keq_dec k2 k1 then @cons Tuple (mkTuple k1 v1) l else @cons Tuple (mkTuple k2 v2) (assoc_add l k1 v1)) k0 with | @none _ => False | @some _ v' => @eq V v0 v' end, or match (if Keq_dec k2 k0 then some V v2 else assoc_find l k0) with | @none _ => False | @some _ v' => @eq V v0 v' end (and (@eq K k0 k1) (@eq V v0 v1)) *)
case (Keq_dec k2 k1).
(* Goal: forall (k : K) (v : V) (k0 : K), @eq (option V) (assoc_find (@cons Tuple (mkTuple k v) (@nil Tuple)) k0) (assoc_find (@cons Tuple (mkTuple k v) (@nil Tuple)) k0) *)
(* Goal: forall (k : K) (v : V), assoc_eqm (assoc_find (@cons Tuple (mkTuple k v) (@cons Tuple a t))) (assoc_find (assoc_add (@cons Tuple a t) k v)) *)
trivial.
(* Goal: forall _ : not (@eq K k2 k1), @eq (option V) ((fix assoc_find (l : assoc) (k0 : K) {struct l} : option V := match l with | nil => none V | cons ({| k := k; v := v |} as t) l' => if Keq_dec k k0 then some V v else assoc_find l' k0 end) l k1) ((fix assoc_find (l : assoc) (k0 : K) {struct l} : option V := match l with | nil => none V | cons ({| k := k; v := v |} as t) l' => if Keq_dec k k0 then some V v else assoc_find l' k0 end) l' k1) *)
fold assoc_find in |- *.
(* Goal: forall (_ : forall (k : K) (_ : not (@eq K k k')), @eq (option V) (assoc_find l k) (assoc_find l' k)) (_ : match assoc_find l' k0 with | @none _ => False | @some _ v' => @eq V v0 v' end), match assoc_find l k0 with | @none _ => False | @some _ v' => @eq V v0 v' end *)
(* Goal: assoc_almost_eqm k' (assoc_find l) (assoc_find l') *)
intro.
(* Goal: @eq (option V) (some V v1) (some V v0) *)
(* Goal: forall _ : not (@eq K k0 k1), @eq (option V) (some V v1) (some V v1) *)
(* Goal: forall _ : not (@eq K k1 k2), @eq (option V) (if Keq_dec k0 k2 then some V v0 else (fix assoc_find (l : assoc) (k0 : K) {struct l} : option V := match l with | nil => none V | cons ({| k := k; v := v |} as t) l' => if Keq_dec k k0 then some V v else assoc_find l' k0 end) l k2) (if Keq_dec k0 k2 then some V v0 else (fix assoc_find (l : assoc) (k0 : K) {struct l} : option V := match l with | nil => none V | cons ({| k := k; v := v |} as t) l' => if Keq_dec k k0 then some V v else assoc_find l' k0 end) l k2) *)
elim H.
(* Goal: forall (k : K) (v : V) (k0 : K), @eq (option V) (assoc_find (@cons Tuple (mkTuple k v) (@nil Tuple)) k0) (assoc_find (@cons Tuple (mkTuple k v) (@nil Tuple)) k0) *)
(* Goal: forall (k : K) (v : V), assoc_eqm (assoc_find (@cons Tuple (mkTuple k v) (@cons Tuple a t))) (assoc_find (assoc_add (@cons Tuple a t) k v)) *)
trivial.
(* Goal: forall (k : K) (v : V) (k0 : K), @eq (option V) (assoc_find (@cons Tuple (mkTuple k v) (@nil Tuple)) k0) (assoc_find (@cons Tuple (mkTuple k v) (@nil Tuple)) k0) *)
(* Goal: forall (k : K) (v : V), assoc_eqm (assoc_find (@cons Tuple (mkTuple k v) (@cons Tuple a t))) (assoc_find (assoc_add (@cons Tuple a t) k v)) *)
trivial.
Qed.


Lemma assoc_semfind_commute :
 forall (k0 k1 : K) (v0 v1 : V) (l : assoc),
 k0 <> k1 ->
 assoc_eqm (assoc_find (mkTuple k1 v1 :: mkTuple k0 v0 :: l))
   (assoc_find (mkTuple k0 v0 :: mkTuple k1 v1 :: l)).

Proof.
(* Goal: forall _ : assoc_eqm (assoc_find (@cons Tuple (mkTuple k' v') l0)) (assoc_find (assoc_add l0 k' v')), @eq (option V) (assoc_find (@cons Tuple (mkTuple k' v') l0) k0) (assoc_find (assoc_add l0 k' v') k0) *)
(* Goal: assoc_eqm (assoc_find (@cons Tuple (mkTuple k' v') l0)) (assoc_find (assoc_add l0 k' v')) *)
  intros. unfold assoc_eqm in |- *. intros. unfold assoc_find in |- *.
(* Goal: @eq (option V) (if Keq_dec k1 k2 then some V v1 else if Keq_dec k0 k2 then some V v0 else (fix assoc_find (l : assoc) (k0 : K) {struct l} : option V := match l with | nil => none V | cons ({| k := k; v := v |} as t) l' => if Keq_dec k k0 then some V v else assoc_find l' k0 end) l k2) (if Keq_dec k0 k2 then some V v0 else if Keq_dec k1 k2 then some V v1 else (fix assoc_find (l : assoc) (k0 : K) {struct l} : option V := match l with | nil => none V | cons ({| k := k; v := v |} as t) l' => if Keq_dec k k0 then some V v else assoc_find l' k0 end) l k2) *)
  case (Keq_dec k1 k2).
(* Goal: forall (_ : forall (k : K) (_ : not (@eq K k k')), @eq (option V) (assoc_find l k) (assoc_find l' k)) (_ : match assoc_find l' k0 with | @none _ => False | @some _ v' => @eq V v0 v' end), match assoc_find l k0 with | @none _ => False | @some _ v' => @eq V v0 v' end *)
(* Goal: assoc_almost_eqm k' (assoc_find l) (assoc_find l') *)
  intro.
(* Goal: @eq (option V) (some V v1) (if Keq_dec k0 k2 then some V v0 else some V v1) *)
(* Goal: forall _ : not (@eq K k1 k2), @eq (option V) (if Keq_dec k0 k2 then some V v0 else (fix assoc_find (l : assoc) (k0 : K) {struct l} : option V := match l with | nil => none V | cons ({| k := k; v := v |} as t) l' => if Keq_dec k k0 then some V v else assoc_find l' k0 end) l k2) (if Keq_dec k0 k2 then some V v0 else (fix assoc_find (l : assoc) (k0 : K) {struct l} : option V := match l with | nil => none V | cons ({| k := k; v := v |} as t) l' => if Keq_dec k k0 then some V v else assoc_find l' k0 end) l k2) *)
  replace k2 with k1.
(* Goal: forall _ : not (@eq K k0 k1), not match (if Keq_dec k0 k1 then some V v0 else assoc_find (assoc_delete l0 k1) k1) with | @none _ => False | @some _ v' => @eq V v1 v' end *)
  case (Keq_dec k0 k1).
(* Goal: forall (_ : forall (k : K) (_ : not (@eq K k k')), @eq (option V) (assoc_find l k) (assoc_find l' k)) (_ : match assoc_find l' k0 with | @none _ => False | @some _ v' => @eq V v0 v' end), match assoc_find l k0 with | @none _ => False | @some _ v' => @eq V v0 v' end *)
(* Goal: assoc_almost_eqm k' (assoc_find l) (assoc_find l') *)
  intro.
(* Goal: @eq (option V) (some V v1) (some V v0) *)
(* Goal: forall _ : not (@eq K k0 k1), @eq (option V) (some V v1) (some V v1) *)
(* Goal: forall _ : not (@eq K k1 k2), @eq (option V) (if Keq_dec k0 k2 then some V v0 else (fix assoc_find (l : assoc) (k0 : K) {struct l} : option V := match l with | nil => none V | cons ({| k := k; v := v |} as t) l' => if Keq_dec k k0 then some V v else assoc_find l' k0 end) l k2) (if Keq_dec k0 k2 then some V v0 else (fix assoc_find (l : assoc) (k0 : K) {struct l} : option V := match l with | nil => none V | cons ({| k := k; v := v |} as t) l' => if Keq_dec k k0 then some V v else assoc_find l' k0 end) l k2) *)
  elim H.
(* Goal: forall (k : K) (v : V) (k0 : K), @eq (option V) (assoc_find (@cons Tuple (mkTuple k v) (@nil Tuple)) k0) (assoc_find (@cons Tuple (mkTuple k v) (@nil Tuple)) k0) *)
(* Goal: forall (k : K) (v : V), assoc_eqm (assoc_find (@cons Tuple (mkTuple k v) (@cons Tuple a t))) (assoc_find (assoc_add (@cons Tuple a t) k v)) *)
  trivial.

(* Goal: forall (k : K) (v : V) (k0 : K), @eq (option V) (assoc_find (@cons Tuple (mkTuple k v) (@nil Tuple)) k0) (assoc_find (@cons Tuple (mkTuple k v) (@nil Tuple)) k0) *)
(* Goal: forall (k : K) (v : V), assoc_eqm (assoc_find (@cons Tuple (mkTuple k v) (@cons Tuple a t))) (assoc_find (assoc_add (@cons Tuple a t) k v)) *)
  trivial.
 
(* Goal: forall (_ : forall (k : K) (_ : not (@eq K k k')), @eq (option V) (assoc_find l k) (assoc_find l' k)) (_ : match assoc_find l' k0 with | @none _ => False | @some _ v' => @eq V v0 v' end), match assoc_find l k0 with | @none _ => False | @some _ v' => @eq V v0 v' end *)
(* Goal: assoc_almost_eqm k' (assoc_find l) (assoc_find l') *)
  intro.
(* Goal: @eq (option V) (if Keq_dec k0 k2 then some V v0 else (fix assoc_find (l : assoc) (k0 : K) {struct l} : option V := match l with | nil => none V | cons ({| k := k; v := v |} as t) l' => if Keq_dec k k0 then some V v else assoc_find l' k0 end) l k2) (if Keq_dec k0 k2 then some V v0 else (fix assoc_find (l : assoc) (k0 : K) {struct l} : option V := match l with | nil => none V | cons ({| k := k; v := v |} as t) l' => if Keq_dec k k0 then some V v else assoc_find l' k0 end) l k2) *)
  case (Keq_dec k0 k2).
(* Goal: forall (k : K) (v : V) (k0 : K), @eq (option V) (assoc_find (@cons Tuple (mkTuple k v) (@nil Tuple)) k0) (assoc_find (@cons Tuple (mkTuple k v) (@nil Tuple)) k0) *)
(* Goal: forall (k : K) (v : V), assoc_eqm (assoc_find (@cons Tuple (mkTuple k v) (@cons Tuple a t))) (assoc_find (assoc_add (@cons Tuple a t) k v)) *)
  trivial.

(* Goal: forall (_ : forall (k : K) (_ : not (@eq K k k')), @eq (option V) (assoc_find l k) (assoc_find l' k)) (_ : match assoc_find l' k0 with | @none _ => False | @some _ v' => @eq V v0 v' end), match assoc_find l k0 with | @none _ => False | @some _ v' => @eq V v0 v' end *)
(* Goal: assoc_almost_eqm k' (assoc_find l) (assoc_find l') *)
  intro.
(* Goal: forall (k : K) (v : V) (k0 : K), @eq (option V) (assoc_find (@cons Tuple (mkTuple k v) (@nil Tuple)) k0) (assoc_find (@cons Tuple (mkTuple k v) (@nil Tuple)) k0) *)
(* Goal: forall (k : K) (v : V), assoc_eqm (assoc_find (@cons Tuple (mkTuple k v) (@cons Tuple a t))) (assoc_find (assoc_add (@cons Tuple a t) k v)) *)
  trivial.
Qed.


Lemma assoc_hasmem_find :
 forall (l : assoc) (k : K) (v : V),
 assoc_hasmem l k v -> assoc_find l k = some V v.

Proof.
(* Goal: forall (l : assoc) (k : K) (v v' : V) (_ : assoc_hasmem l k v) (_ : assoc_hasmem l k v'), @eq V v' v *)
unfold assoc_hasmem in |- *.
(* Goal: forall (l : assoc) (k : K) (v : V) (_ : match assoc_find l k with | @none _ => False | @some _ v' => @eq V v v' end), @eq (option V) (assoc_find l k) (some V v) *)
intros l k0 v0.
(* Goal: forall (v _ : V) (_ : match assoc_find l k0 with | @none _ => False | @some _ v'0 => @eq V v v'0 end) (_ : not match assoc_find l k0 with | @none _ => False | @some _ v'0 => @eq V v v'0 end), @eq K k1 k0 *)
(* Goal: @eq (option V) (assoc_find l k0) (assoc_find (assoc_delete l k1) k0) *)
(* Goal: assoc_almost_eqm k1 (assoc_find l) (assoc_find (assoc_delete l k1)) *)
case (assoc_find l k0).
(* Goal: forall (_ : @eq K k' k0) (_ : @eq V v0 v'), @eq K k' k0 *)
(* Goal: forall (_ : not (@eq K k' k0)) (_ : match assoc_find l0 k0 with | @none _ => False | @some _ v' => @eq V v0 v' end), @eq K k' k0 *)
(* Goal: @eq (option V) (assoc_find (@cons Tuple (mkTuple k' v') l0) k0) (assoc_find (assoc_add l0 k' v') k0) *)
auto.
(* Goal: forall (_ : not (@eq K k' k0)) (_ : @eq (option V) (some V v0) (assoc_find l0 k0)), @eq K k' k0 *)
(* Goal: @eq (option V) (assoc_find (@cons Tuple (mkTuple k' v') l0) k0) (assoc_find (assoc_add l0 k' v') k0) *)
intros.
(* Goal: @eq V v1 v0 *)
(* Goal: @eq V v1 v0 *)
contradiction.
(* Goal: forall (_ : not (@eq K k' k0)) (_ : @eq (option V) (some V v0) (assoc_find l0 k0)), @eq K k' k0 *)
(* Goal: @eq (option V) (assoc_find (@cons Tuple (mkTuple k' v') l0) k0) (assoc_find (assoc_add l0 k' v') k0) *)
intros.
(* Goal: assoc_almost_eqm k' (assoc_find l) (assoc_find l') *)
rewrite H.
(* Goal: forall (_ : @eq K k' k0) (_ : @eq V v0 v'), @eq K k' k0 *)
(* Goal: forall (_ : not (@eq K k' k0)) (_ : match assoc_find l0 k0 with | @none _ => False | @some _ v' => @eq V v0 v' end), @eq K k' k0 *)
(* Goal: @eq (option V) (assoc_find (@cons Tuple (mkTuple k' v') l0) k0) (assoc_find (assoc_add l0 k' v') k0) *)
auto.
Qed.


Lemma assoc_find_hasmem :
 forall (l : assoc) (k : K) (v : V),
 assoc_find l k = some V v -> assoc_hasmem l k v.

Proof.
(* Goal: forall (_ : @eq K k' k0) (_ : @eq V v0 v'), @eq K k' k0 *)
(* Goal: forall (_ : not (@eq K k' k0)) (_ : match assoc_find l0 k0 with | @none _ => False | @some _ v' => @eq V v0 v' end), @eq K k' k0 *)
(* Goal: @eq (option V) (assoc_find (@cons Tuple (mkTuple k' v') l0) k0) (assoc_find (assoc_add l0 k' v') k0) *)
unfold assoc_hasmem in |- *; intros; rewrite H; auto.
Qed.


Lemma assoc_find_none_hasmem :
 forall (l : assoc) (k : K) (v : V),
 assoc_find l k = none V -> forall v : V, ~ assoc_hasmem l k v.

Proof.
(* Goal: forall (l : assoc) (k : K) (_ : V) (_ : @eq (option V) (assoc_find l k) (none V)) (v0 : V), not (assoc_hasmem l k v0) *)
unfold not in |- *; intros; absurd (assoc_find l k0 = some V v1).
(* Goal: not (@eq (option V) (assoc_find l k0) (some V v1)) *)
(* Goal: @eq (option V) (assoc_find l k0) (some V v1) *)
rewrite H; discriminate.
(* Goal: assoc_almost_eqm k0 (assoc_find l) (assoc_find (@cons Tuple (mkTuple k0 v') l)) *)
(* Goal: assoc_almost_eqm k0 (assoc_find (@cons Tuple (mkTuple k0 v0) l)) (assoc_find l) *)
(* Goal: assoc_almost_eqm k0 (assoc_find l) (assoc_find (@cons Tuple (mkTuple k0 v') l)) *)
apply assoc_hasmem_find; assumption.
Qed.


Lemma assoc_find_mem :
 forall (l : assoc) (k : K) (v : V),
 assoc_find l k = some V v -> assoc_mem l k.

Proof.
(* Goal: forall (_ : @eq K k' k0) (_ : @eq V v0 v'), @eq K k' k0 *)
(* Goal: forall (_ : not (@eq K k' k0)) (_ : match assoc_find l0 k0 with | @none _ => False | @some _ v' => @eq V v0 v' end), @eq K k' k0 *)
(* Goal: @eq (option V) (assoc_find (@cons Tuple (mkTuple k' v') l0) k0) (assoc_find (assoc_add l0 k' v') k0) *)
unfold assoc_mem in |- *; intros; rewrite H; simpl in |- *; auto.
Qed.




(**************************************************)
(* mem/hasmem connectivity                        *)
(**************************************************)



Lemma assoc_hasmem_mem :
 forall (l : assoc) (k : K) (v : V), assoc_hasmem l k v -> assoc_mem l k.

Proof.
(* Goal: forall (_ : not (@eq K k' k0)) (_ : @eq (option V) (some V v0) (assoc_find l0 k0)), @eq K k' k0 *)
(* Goal: @eq (option V) (assoc_find (@cons Tuple (mkTuple k' v') l0) k0) (assoc_find (assoc_add l0 k' v') k0) *)
intros.
(* Goal: assoc_mem l k0 *)
cut (assoc_find l k0 = some V v0).
(* Goal: forall (_ : forall (k : K) (_ : not (@eq K k k')), @eq (option V) (assoc_find l k) (assoc_find l' k)) (_ : match assoc_find l' k0 with | @none _ => False | @some _ v' => @eq V v0 v' end), match assoc_find l k0 with | @none _ => False | @some _ v' => @eq V v0 v' end *)
(* Goal: assoc_almost_eqm k' (assoc_find l) (assoc_find l') *)
intro.
(* Goal: forall _ : assoc_mem (assoc_delete l k') k0, assoc_mem l k0 *)
unfold assoc_mem in |- *.
(* Goal: @eq (option V) (some V v0) (some V v') *)
(* Goal: @eq K k' k0 *)
rewrite H0.
(* Goal: forall (_ : @eq K k' k0) (_ : @eq V v0 v'), @eq K k' k0 *)
(* Goal: forall (_ : not (@eq K k' k0)) (_ : match assoc_find l0 k0 with | @none _ => False | @some _ v' => @eq V v0 v' end), @eq K k' k0 *)
(* Goal: @eq (option V) (assoc_find (@cons Tuple (mkTuple k' v') l0) k0) (assoc_find (assoc_add l0 k' v') k0) *)
auto.
(* Goal: @eq (option V) (assoc_find (assoc_delete l k') k0) (some V v0) *)
apply assoc_hasmem_find.
(* Goal: forall (_ : @eq K k' k0) (_ : @eq V v0 v'), @eq K k' k0 *)
(* Goal: forall (_ : not (@eq K k' k0)) (_ : match assoc_find l0 k0 with | @none _ => False | @some _ v' => @eq V v0 v' end), @eq K k' k0 *)
(* Goal: @eq (option V) (assoc_find (@cons Tuple (mkTuple k' v') l0) k0) (assoc_find (assoc_add l0 k' v') k0) *)
auto.
Qed.


Lemma assoc_mem_hasmem :
 forall (l : assoc) (k : K),
 assoc_mem l k -> exists v : V, assoc_hasmem l k v.

Proof.
(* Goal: forall (l : assoc) (k : K) (_ : assoc_mem l k), @ex V (fun v : V => assoc_hasmem l k v) *)
simple induction l.
(* Goal: forall (_ : @eq K k' k0) (_ : @eq V v0 v'), @eq K k' k0 *)
(* Goal: forall (_ : not (@eq K k' k0)) (_ : match assoc_find l0 k0 with | @none _ => False | @some _ v' => @eq V v0 v' end), @eq K k' k0 *)
(* Goal: @eq (option V) (assoc_find (@cons Tuple (mkTuple k' v') l0) k0) (assoc_find (assoc_add l0 k' v') k0) *)
simpl in |- *; unfold assoc_mem in |- *; simpl in |- *; auto.
(* Goal: @eq V v1 v0 *)
(* Goal: @eq V v1 v0 *)
intros; contradiction.
(* Goal: forall _ : match assoc_find (@cons Tuple (mkTuple k' v') l0) k0 with | @none _ => False | @some _ v' => @eq V v0 v' end, @eq K k' k0 *)
(* Goal: @eq (option V) (assoc_find (@cons Tuple (mkTuple k' v') l0) k0) (assoc_find (assoc_add l0 k' v') k0) *)
intros; unfold assoc_hasmem in |- *; simpl in |- *.
induction  a as (k1, v0).
(* Goal: forall _ : match (if Keq_dec k1 k0 then some V v1 else assoc_find l k0) with | @none _ => False | @some _ v' => @eq V v0 v' end, @eq V v0 v1 *)
(* Goal: forall (_ : not (@eq K k2 k0)) (_ : @eq K k2 k1) (_ : match assoc_find (@cons Tuple (mkTuple k1 v1) l) k0 with | @none _ => False | @some _ v' => @eq V v0 v' end), or match assoc_find l k0 with | @none _ => False | @some _ v' => @eq V v0 v' end (and (@eq K k0 k1) (@eq V v0 v1)) *)
(* Goal: forall (_ : not (@eq K k2 k1)) (_ : match assoc_find (@cons Tuple (mkTuple k2 v2) (assoc_add l k1 v1)) k0 with | @none _ => False | @some _ v' => @eq V v0 v' end), or match (if Keq_dec k2 k0 then some V v2 else assoc_find l k0) with | @none _ => False | @some _ v' => @eq V v0 v' end (and (@eq K k0 k1) (@eq V v0 v1)) *)
case (Keq_dec k1 k0).
(* Goal: forall (_ : @eq K k' k0) (_ : @eq V v0 v'), @eq K k' k0 *)
(* Goal: forall (_ : not (@eq K k' k0)) (_ : match assoc_find l0 k0 with | @none _ => False | @some _ v' => @eq V v0 v' end), @eq K k' k0 *)
(* Goal: @eq (option V) (assoc_find (@cons Tuple (mkTuple k' v') l0) k0) (assoc_find (assoc_add l0 k' v') k0) *)
intros; split with v0; auto.
(* Goal: forall (_ : @eq K k' k0) (_ : @eq V v0 v'), @eq K k' k0 *)
(* Goal: forall (_ : not (@eq K k' k0)) (_ : match assoc_find l0 k0 with | @none _ => False | @some _ v' => @eq V v0 v' end), @eq K k' k0 *)
(* Goal: @eq (option V) (assoc_find (@cons Tuple (mkTuple k' v') l0) k0) (assoc_find (assoc_add l0 k' v') k0) *)
intros; unfold assoc_hasmem in H; apply H; auto.
(* Goal: forall _ : match assoc_find (@cons Tuple (mkTuple k' v') l0) k0 with | @none _ => False | @some _ v' => @eq V v0 v' end, @eq K k' k0 *)
(* Goal: @eq (option V) (assoc_find (@cons Tuple (mkTuple k' v') l0) k0) (assoc_find (assoc_add l0 k' v') k0) *)
generalize H0; unfold assoc_mem in |- *; simpl in |- *.
(* Goal: forall (_ : @eq K k' k0) (_ : @eq V v0 v'), @eq K k' k0 *)
(* Goal: forall (_ : not (@eq K k' k0)) (_ : match assoc_find l0 k0 with | @none _ => False | @some _ v' => @eq V v0 v' end), @eq K k' k0 *)
(* Goal: @eq (option V) (assoc_find (@cons Tuple (mkTuple k' v') l0) k0) (assoc_find (assoc_add l0 k' v') k0) *)
case (Keq_dec k1 k0); auto.
(* Goal: assoc_almost_eqm k0 (assoc_find l) (assoc_find (@cons Tuple (mkTuple k0 v') l)) *)
(* Goal: assoc_almost_eqm k0 (assoc_find (@cons Tuple (mkTuple k0 v0) l)) (assoc_find l) *)
(* Goal: assoc_almost_eqm k0 (assoc_find l) (assoc_find (@cons Tuple (mkTuple k0 v') l)) *)
intro; absurd (k1 = k0); assumption.
Qed.




(**************************************************)
(* assoc_add properties                           *)
(**************************************************)



Lemma assoc_add_egale_cons :
 forall (t : assoc) (k : K) (v : V),
 assoc_eqm (assoc_find (mkTuple k v :: t)) (assoc_find (assoc_add t k v)).

Proof.
(* Goal: forall (_ : forall (k : K) (_ : not (@eq K k k')), @eq (option V) (assoc_find l k) (assoc_find l' k)) (_ : match assoc_find l' k0 with | @none _ => False | @some _ v' => @eq V v0 v' end), match assoc_find l k0 with | @none _ => False | @some _ v' => @eq V v0 v' end *)
(* Goal: assoc_almost_eqm k' (assoc_find l) (assoc_find l') *)
intro.
induction  t as [| a t Hrect].
(* Goal: forall (k : K) (v : V), assoc_eqm (assoc_find (@cons Tuple (mkTuple k v) (@nil Tuple))) (assoc_find (assoc_add (@nil Tuple) k v)) *)
(* Goal: forall (k : K) (v : V), assoc_eqm (assoc_find (@cons Tuple (mkTuple k v) (@cons Tuple a t))) (assoc_find (assoc_add (@cons Tuple a t) k v)) *)
unfold assoc_add, assoc_eqm in |- *.
(* Goal: forall (k : K) (v : V) (k0 : K), @eq (option V) (assoc_find (@cons Tuple (mkTuple k v) (@nil Tuple)) k0) (assoc_find (@cons Tuple (mkTuple k v) (@nil Tuple)) k0) *)
(* Goal: forall (k : K) (v : V), assoc_eqm (assoc_find (@cons Tuple (mkTuple k v) (@cons Tuple a t))) (assoc_find (assoc_add (@cons Tuple a t) k v)) *)
trivial.
 
induction  a as (k0, v0).
(* Goal: forall (k : K) (v : V), assoc_eqm (assoc_find (@cons Tuple (mkTuple k v) (@cons Tuple (mkTuple k0 v0) t))) (assoc_find (assoc_add (@cons Tuple (mkTuple k0 v0) t) k v)) *)
unfold assoc_add in |- *.
(* Goal: forall (_ : not (@eq K k' k0)) (_ : @eq (option V) (some V v0) (assoc_find l0 k0)), @eq K k' k0 *)
(* Goal: @eq (option V) (assoc_find (@cons Tuple (mkTuple k' v') l0) k0) (assoc_find (assoc_add l0 k' v') k0) *)
intros.
(* Goal: forall _ : not (@eq K k0 k1), not match (if Keq_dec k0 k1 then some V v0 else assoc_find (assoc_delete l0 k1) k1) with | @none _ => False | @some _ v' => @eq V v1 v' end *)
case (Keq_dec k0 k1).
(* Goal: forall _ : @eq K k0 k1, assoc_eqm (assoc_find (@cons Tuple (mkTuple k1 v1) (@cons Tuple (mkTuple k0 v0) t))) (assoc_find (@cons Tuple (mkTuple k1 v1) t)) *)
(* Goal: forall _ : not (@eq K k0 k1), assoc_eqm (assoc_find (@cons Tuple (mkTuple k1 v1) (@cons Tuple (mkTuple k0 v0) t))) (assoc_find (@cons Tuple (mkTuple k0 v0) ((fix assoc_add (l : assoc) (k0 : K) (v0 : V) {struct l} : assoc := match l with | nil => @cons Tuple (mkTuple k0 v0) (@nil Tuple) | cons ({| k := k; v := v |} as t) l' => if Keq_dec k k0 then @cons Tuple (mkTuple k0 v0) l' else @cons Tuple (mkTuple k v) (assoc_add l' k0 v0) end) t k1 v1))) *)
intro; replace k1 with k0.
(* Goal: forall _ : assoc_eqm (assoc_find (@cons Tuple (mkTuple k' v') l0)) (assoc_find (assoc_add l0 k' v')), @eq (option V) (assoc_find (@cons Tuple (mkTuple k' v') l0) k0) (assoc_find (assoc_add l0 k' v') k0) *)
(* Goal: assoc_eqm (assoc_find (@cons Tuple (mkTuple k' v') l0)) (assoc_find (assoc_add l0 k' v')) *)
unfold assoc_eqm in |- *.
(* Goal: forall (_ : forall (k : K) (_ : not (@eq K k k')), @eq (option V) (assoc_find l k) (assoc_find l' k)) (_ : match assoc_find l' k0 with | @none _ => False | @some _ v' => @eq V v0 v' end), match assoc_find l k0 with | @none _ => False | @some _ v' => @eq V v0 v' end *)
(* Goal: assoc_almost_eqm k' (assoc_find l) (assoc_find l') *)
intro.
(* Goal: forall (k : K) (v : V) (k0 : K), @eq (option V) (assoc_find (@cons Tuple (mkTuple k v) (@nil Tuple)) k0) (assoc_find (@cons Tuple (mkTuple k v) (@nil Tuple)) k0) *)
(* Goal: forall (k : K) (v : V), assoc_eqm (assoc_find (@cons Tuple (mkTuple k v) (@cons Tuple a t))) (assoc_find (assoc_add (@cons Tuple a t) k v)) *)
unfold assoc_find in |- *; case (Keq_dec k0 k2); trivial.
 
(* Goal: forall _ : not (@eq K k0 k1), assoc_eqm (assoc_find (@cons Tuple (mkTuple k1 v1) (@cons Tuple (mkTuple k0 v0) t))) (assoc_find (@cons Tuple (mkTuple k0 v0) ((fix assoc_add (l : assoc) (k0 : K) (v0 : V) {struct l} : assoc := match l with | nil => @cons Tuple (mkTuple k0 v0) (@nil Tuple) | cons ({| k := k; v := v |} as t) l' => if Keq_dec k k0 then @cons Tuple (mkTuple k0 v0) l' else @cons Tuple (mkTuple k v) (assoc_add l' k0 v0) end) t k1 v1))) *)
fold assoc_add in |- *.
(* Goal: forall (_ : forall (k : K) (_ : not (@eq K k k')), @eq (option V) (assoc_find l k) (assoc_find l' k)) (_ : match assoc_find l' k0 with | @none _ => False | @some _ v' => @eq V v0 v' end), match assoc_find l k0 with | @none _ => False | @some _ v' => @eq V v0 v' end *)
(* Goal: assoc_almost_eqm k' (assoc_find l) (assoc_find l') *)
intro.
(* Goal: assoc_eqm (assoc_find (@cons Tuple (mkTuple k1 v1) (@cons Tuple (mkTuple k0 v0) t))) (assoc_find (@cons Tuple (mkTuple k0 v0) (assoc_add t k1 v1))) *)
apply assoc_eqm_trans with (assoc_find (mkTuple k0 v0 :: mkTuple k1 v1 :: t)).
(* Goal: forall (_ : @eq K k' k0) (_ : @eq V v0 v'), @eq K k' k0 *)
(* Goal: forall (_ : not (@eq K k' k0)) (_ : match assoc_find l0 k0 with | @none _ => False | @some _ v' => @eq V v0 v' end), @eq K k' k0 *)
(* Goal: @eq (option V) (assoc_find (@cons Tuple (mkTuple k' v') l0) k0) (assoc_find (assoc_add l0 k' v') k0) *)
apply assoc_semfind_commute; auto.
 
(* Goal: assoc_eqm (assoc_find (@cons Tuple (mkTuple k0 v0) (@cons Tuple (mkTuple k1 v1) t))) (assoc_find (@cons Tuple (mkTuple k0 v0) (assoc_add t k1 v1))) *)
apply assoc_semfind_increase_1; apply Hrect.
Qed.


Lemma assoc_add_correct_1 :
 forall (k : K) (v : V) (t : assoc),
 assoc_almost_eqm k (assoc_find (assoc_add t k v)) (assoc_find t).

Proof.
(* Goal: forall (_ : not (@eq K k' k0)) (_ : @eq (option V) (some V v0) (assoc_find l0 k0)), @eq K k' k0 *)
(* Goal: @eq (option V) (assoc_find (@cons Tuple (mkTuple k' v') l0) k0) (assoc_find (assoc_add l0 k' v') k0) *)
intros; unfold assoc_almost_eqm in |- *; intros.
replace (assoc_find (assoc_add t k0 v0) k1) with
 (assoc_find (mkTuple k0 v0 :: t) k1).
(* Goal: forall _ : match assoc_find (@cons Tuple (mkTuple k' v') l0) k0 with | @none _ => False | @some _ v' => @eq V v0 v' end, @eq K k' k0 *)
(* Goal: @eq (option V) (assoc_find (@cons Tuple (mkTuple k' v') l0) k0) (assoc_find (assoc_add l0 k' v') k0) *)
  simpl in |- *. case (Keq_dec k0 k1).
(* Goal: forall (_ : @eq K k' k0) (_ : @eq V v0 v'), @eq K k' k0 *)
(* Goal: forall (_ : not (@eq K k' k0)) (_ : match assoc_find l0 k0 with | @none _ => False | @some _ v' => @eq V v0 v' end), @eq K k' k0 *)
(* Goal: @eq (option V) (assoc_find (@cons Tuple (mkTuple k' v') l0) k0) (assoc_find (assoc_add l0 k' v') k0) *)
    intro; absurd (k1 = k0); auto.
(* Goal: forall (_ : @eq K k' k0) (_ : @eq V v0 v'), @eq K k' k0 *)
(* Goal: forall (_ : not (@eq K k' k0)) (_ : match assoc_find l0 k0 with | @none _ => False | @some _ v' => @eq V v0 v' end), @eq K k' k0 *)
(* Goal: @eq (option V) (assoc_find (@cons Tuple (mkTuple k' v') l0) k0) (assoc_find (assoc_add l0 k' v') k0) *)
    auto.
  cut
   (assoc_eqm (assoc_find (mkTuple k0 v0 :: t))
      (assoc_find (assoc_add t k0 v0))).
(* Goal: forall (_ : @eq K k' k0) (_ : @eq V v0 v'), @eq K k' k0 *)
(* Goal: forall (_ : not (@eq K k' k0)) (_ : match assoc_find l0 k0 with | @none _ => False | @some _ v' => @eq V v0 v' end), @eq K k' k0 *)
(* Goal: @eq (option V) (assoc_find (@cons Tuple (mkTuple k' v') l0) k0) (assoc_find (assoc_add l0 k' v') k0) *)
    unfold assoc_eqm in |- *; auto.
(* Goal: assoc_eqm (assoc_find (@cons Tuple (mkTuple k' v') l0)) (assoc_find (assoc_add l0 k' v')) *)
    apply assoc_add_egale_cons.
Qed.


Lemma assoc_add_correct_2 :
 forall (k : K) (v : V) (t : assoc),
 assoc_find (assoc_add t k v) k = some V v.

Proof.
(* Goal: forall (_ : not (@eq K k' k0)) (_ : @eq (option V) (some V v0) (assoc_find l0 k0)), @eq K k' k0 *)
(* Goal: @eq (option V) (assoc_find (@cons Tuple (mkTuple k' v') l0) k0) (assoc_find (assoc_add l0 k' v') k0) *)
intros.
(* Goal: @eq (option V) (assoc_find (assoc_add t k0 v0) k0) (some V v0) *)
transitivity (assoc_find (mkTuple k0 v0 :: t) k0).
(* Goal: @eq (option V) (assoc_find (assoc_add t k0 v0) k0) (assoc_find (@cons Tuple (mkTuple k0 v0) t) k0) *)
(* Goal: @eq (option V) (assoc_find (@cons Tuple (mkTuple k0 v0) t) k0) (some V v0) *)
elim assoc_add_egale_cons.
(* Goal: forall (_ : @eq K k' k0) (_ : @eq V v0 v'), @eq K k' k0 *)
(* Goal: forall (_ : not (@eq K k' k0)) (_ : match assoc_find l0 k0 with | @none _ => False | @some _ v' => @eq V v0 v' end), @eq K k' k0 *)
(* Goal: @eq (option V) (assoc_find (@cons Tuple (mkTuple k' v') l0) k0) (assoc_find (assoc_add l0 k' v') k0) *)
auto.
(* Goal: @eq (option V) (assoc_find (@cons Tuple (mkTuple k0 v0) t) k0) (some V v0) *)
apply assoc_semfind_cons_2.
Qed.


Lemma assoc_add_correct_3 :
 forall (k : K) (v : V) (t : assoc), assoc_hasmem (assoc_add t k v) k v.

Proof.
(* Goal: forall (_ : not (@eq K k' k0)) (_ : @eq (option V) (some V v0) (assoc_find l0 k0)), @eq K k' k0 *)
(* Goal: @eq (option V) (assoc_find (@cons Tuple (mkTuple k' v') l0) k0) (assoc_find (assoc_add l0 k' v') k0) *)
intros.
(* Goal: forall (l : assoc) (k : K) (v v' : V) (_ : assoc_hasmem l k v) (_ : assoc_hasmem l k v'), @eq V v' v *)
unfold assoc_hasmem in |- *.
(* Goal: match assoc_find (assoc_add t k0 v0) k0 with | @none _ => False | @some _ v' => @eq V v0 v' end *)
replace (assoc_find (assoc_add t k0 v0) k0) with (some V v0).
(* Goal: forall (_ : @eq K k' k0) (_ : @eq V v0 v'), @eq K k' k0 *)
(* Goal: forall (_ : not (@eq K k' k0)) (_ : match assoc_find l0 k0 with | @none _ => False | @some _ v' => @eq V v0 v' end), @eq K k' k0 *)
(* Goal: @eq (option V) (assoc_find (@cons Tuple (mkTuple k' v') l0) k0) (assoc_find (assoc_add l0 k' v') k0) *)
auto.
symmetry  in |- *.
(* Goal: @eq (option V) (assoc_find (assoc_add l0 k0 v') k0) (some V v') *)
(* Goal: @eq K k' k0 *)
apply assoc_add_correct_2.
Qed.


Lemma assoc_add_correct_4 :
 forall (k : K) (v : V) (t : assoc), assoc_mem (assoc_add t k v) k.

Proof.
(* Goal: forall (_ : not (@eq K k' k0)) (_ : @eq (option V) (some V v0) (assoc_find l0 k0)), @eq K k' k0 *)
(* Goal: @eq (option V) (assoc_find (@cons Tuple (mkTuple k' v') l0) k0) (assoc_find (assoc_add l0 k' v') k0) *)
intros.
(* Goal: assoc_mem (assoc_add t k0 v0) k0 *)
apply assoc_hasmem_mem with v0.
(* Goal: assoc_hasmem (assoc_add t k0 v0) k0 v0 *)
apply assoc_add_correct_3.
Qed.




(**************************************************)
(* assoc_del properties                           *)
(**************************************************)



Lemma assoc_del_correct_1 :
 forall (l : assoc) (k : K), assoc_find (assoc_delete l k) k = none V.

Proof.
(* Goal: forall (_ : @eq K k' k0) (_ : @eq V v0 v'), @eq K k' k0 *)
(* Goal: forall (_ : not (@eq K k' k0)) (_ : match assoc_find l0 k0 with | @none _ => False | @some _ v' => @eq V v0 v' end), @eq K k' k0 *)
(* Goal: @eq (option V) (assoc_find (@cons Tuple (mkTuple k' v') l0) k0) (assoc_find (assoc_add l0 k' v') k0) *)
simple induction l; simpl in |- *; auto.
(* Goal: forall _ : match assoc_find (@cons Tuple (mkTuple k' v') l0) k0 with | @none _ => False | @some _ v' => @eq V v0 v' end, @eq K k' k0 *)
(* Goal: @eq (option V) (assoc_find (@cons Tuple (mkTuple k' v') l0) k0) (assoc_find (assoc_add l0 k' v') k0) *)
simple induction a; simpl in |- *.
(* Goal: forall (_ : not (@eq K k' k0)) (_ : @eq (option V) (some V v0) (assoc_find l0 k0)), @eq K k' k0 *)
(* Goal: @eq (option V) (assoc_find (@cons Tuple (mkTuple k' v') l0) k0) (assoc_find (assoc_add l0 k' v') k0) *)
intros.
(* Goal: forall (_ : @eq K k' k0) (_ : @eq V v0 v'), @eq K k' k0 *)
(* Goal: forall (_ : not (@eq K k' k0)) (_ : match assoc_find l0 k0 with | @none _ => False | @some _ v' => @eq V v0 v' end), @eq K k' k0 *)
(* Goal: @eq (option V) (assoc_find (@cons Tuple (mkTuple k' v') l0) k0) (assoc_find (assoc_add l0 k' v') k0) *)
case (Keq_dec k0 k1); auto.
(* Goal: forall _ : match assoc_find (@cons Tuple (mkTuple k' v') l0) k0 with | @none _ => False | @some _ v' => @eq V v0 v' end, @eq K k' k0 *)
(* Goal: @eq (option V) (assoc_find (@cons Tuple (mkTuple k' v') l0) k0) (assoc_find (assoc_add l0 k' v') k0) *)
intro; simpl in |- *.
(* Goal: forall (_ : @eq K k' k0) (_ : @eq V v0 v'), @eq K k' k0 *)
(* Goal: forall (_ : not (@eq K k' k0)) (_ : match assoc_find l0 k0 with | @none _ => False | @some _ v' => @eq V v0 v' end), @eq K k' k0 *)
(* Goal: @eq (option V) (assoc_find (@cons Tuple (mkTuple k' v') l0) k0) (assoc_find (assoc_add l0 k' v') k0) *)
case (Keq_dec k0 k1); auto.
(* Goal: assoc_almost_eqm k0 (assoc_find l) (assoc_find (@cons Tuple (mkTuple k0 v') l)) *)
(* Goal: assoc_almost_eqm k0 (assoc_find (@cons Tuple (mkTuple k0 v0) l)) (assoc_find l) *)
(* Goal: assoc_almost_eqm k0 (assoc_find l) (assoc_find (@cons Tuple (mkTuple k0 v') l)) *)
intro; absurd (k0 = k1); assumption.
Qed.


Lemma assoc_del_correct_2 :
 forall (l : assoc) (k : K) (v : V), ~ assoc_hasmem (assoc_delete l k) k v.

Proof.
(* Goal: forall (_ : @eq K k' k0) (_ : @eq V v0 v'), @eq K k' k0 *)
(* Goal: forall (_ : not (@eq K k' k0)) (_ : match assoc_find l0 k0 with | @none _ => False | @some _ v' => @eq V v0 v' end), @eq K k' k0 *)
(* Goal: @eq (option V) (assoc_find (@cons Tuple (mkTuple k' v') l0) k0) (assoc_find (assoc_add l0 k' v') k0) *)
simple induction l; simpl in |- *; auto.
(* Goal: forall (_ : not (@eq K k' k0)) (_ : @eq (option V) (some V v0) (assoc_find l0 k0)), @eq K k' k0 *)
(* Goal: @eq (option V) (assoc_find (@cons Tuple (mkTuple k' v') l0) k0) (assoc_find (assoc_add l0 k' v') k0) *)
simple induction a; simpl in |- *; intros.
(* Goal: forall _ : not (@eq K k0 k1), not match (if Keq_dec k0 k1 then some V v0 else assoc_find (assoc_delete l0 k1) k1) with | @none _ => False | @some _ v' => @eq V v1 v' end *)
case (Keq_dec k0 k1).
(* Goal: forall _ : @eq K k1 k0, not (assoc_mem (assoc_delete l0 k0) k0) *)
(* Goal: forall _ : not (@eq K k1 k0), not (assoc_mem (@cons Tuple (mkTuple k1 v0) (assoc_delete l0 k0)) k0) *)
intros; apply H.
(* Goal: forall (l : assoc) (k : K) (v v' : V) (_ : assoc_hasmem l k v) (_ : assoc_hasmem l k v'), @eq V v' v *)
unfold assoc_hasmem in |- *.
(* Goal: forall _ : match assoc_find (@cons Tuple (mkTuple k' v') l0) k0 with | @none _ => False | @some _ v' => @eq V v0 v' end, @eq K k' k0 *)
(* Goal: @eq (option V) (assoc_find (@cons Tuple (mkTuple k' v') l0) k0) (assoc_find (assoc_add l0 k' v') k0) *)
simpl in |- *.
(* Goal: forall _ : not (@eq K k0 k1), not match (if Keq_dec k0 k1 then some V v0 else assoc_find (assoc_delete l0 k1) k1) with | @none _ => False | @some _ v' => @eq V v1 v' end *)
case (Keq_dec k0 k1).
(* Goal: forall (_ : @eq K k' k0) (_ : @eq V v0 v'), @eq K k' k0 *)
(* Goal: forall (_ : not (@eq K k' k0)) (_ : match assoc_find l0 k0 with | @none _ => False | @some _ v' => @eq V v0 v' end), @eq K k' k0 *)
(* Goal: @eq (option V) (assoc_find (@cons Tuple (mkTuple k' v') l0) k0) (assoc_find (assoc_add l0 k' v') k0) *)
auto.
(* Goal: forall (_ : not (@eq K k' k0)) (_ : @eq (option V) (some V v0) (assoc_find l0 k0)), @eq K k' k0 *)
(* Goal: @eq (option V) (assoc_find (@cons Tuple (mkTuple k' v') l0) k0) (assoc_find (assoc_add l0 k' v') k0) *)
intros.
replace
 match assoc_find (assoc_delete l0 k1) k1 with
 | none => False
 | some v' => v1 = v'
 end with (assoc_hasmem (assoc_delete l0 k1) k1 v1).
(* Goal: not (assoc_hasmem (assoc_delete l0 k1) k1 v1) *)
(* Goal: @eq Prop (assoc_hasmem (assoc_delete l0 k1) k1 v1) match assoc_find (assoc_delete l0 k1) k1 with | @none _ => False | @some _ v' => @eq V v1 v' end *)
apply H.
(* Goal: forall (k : K) (v : V) (k0 : K), @eq (option V) (assoc_find (@cons Tuple (mkTuple k v) (@nil Tuple)) k0) (assoc_find (@cons Tuple (mkTuple k v) (@nil Tuple)) k0) *)
(* Goal: forall (k : K) (v : V), assoc_eqm (assoc_find (@cons Tuple (mkTuple k v) (@cons Tuple a t))) (assoc_find (assoc_add (@cons Tuple a t) k v)) *)
unfold assoc_hasmem in |- *; trivial.
Qed.


Lemma assoc_del_correct_3 :
 forall (l : assoc) (k : K), ~ assoc_mem (assoc_delete l k) k.

Proof.
(* Goal: forall (_ : @eq K k' k0) (_ : @eq V v0 v'), @eq K k' k0 *)
(* Goal: forall (_ : not (@eq K k' k0)) (_ : match assoc_find l0 k0 with | @none _ => False | @some _ v' => @eq V v0 v' end), @eq K k' k0 *)
(* Goal: @eq (option V) (assoc_find (@cons Tuple (mkTuple k' v') l0) k0) (assoc_find (assoc_add l0 k' v') k0) *)
simple induction l; auto.
intros; simpl in |- *; induction  a as (k1, v0).
(* Goal: forall _ : match (if Keq_dec k1 k0 then some V v1 else assoc_find l k0) with | @none _ => False | @some _ v' => @eq V v0 v' end, @eq V v0 v1 *)
(* Goal: forall (_ : not (@eq K k2 k0)) (_ : @eq K k2 k1) (_ : match assoc_find (@cons Tuple (mkTuple k1 v1) l) k0 with | @none _ => False | @some _ v' => @eq V v0 v' end), or match assoc_find l k0 with | @none _ => False | @some _ v' => @eq V v0 v' end (and (@eq K k0 k1) (@eq V v0 v1)) *)
(* Goal: forall (_ : not (@eq K k2 k1)) (_ : match assoc_find (@cons Tuple (mkTuple k2 v2) (assoc_add l k1 v1)) k0 with | @none _ => False | @some _ v' => @eq V v0 v' end), or match (if Keq_dec k2 k0 then some V v2 else assoc_find l k0) with | @none _ => False | @some _ v' => @eq V v0 v' end (and (@eq K k0 k1) (@eq V v0 v1)) *)
  case (Keq_dec k1 k0).
(* Goal: forall _ : @eq K k1 k0, not (assoc_mem (assoc_delete l0 k0) k0) *)
(* Goal: forall _ : not (@eq K k1 k0), not (assoc_mem (@cons Tuple (mkTuple k1 v0) (assoc_delete l0 k0)) k0) *)
    intros; apply H.
(* Goal: forall _ : match (if Keq_dec k1 k0 then some V v1 else assoc_find l k0) with | @none _ => False | @some _ v' => @eq V v0 v' end, @eq V v0 v1 *)
(* Goal: forall (_ : not (@eq K k2 k0)) (_ : @eq K k2 k1) (_ : match assoc_find (@cons Tuple (mkTuple k1 v1) l) k0 with | @none _ => False | @some _ v' => @eq V v0 v' end), or match assoc_find l k0 with | @none _ => False | @some _ v' => @eq V v0 v' end (and (@eq K k0 k1) (@eq V v0 v1)) *)
(* Goal: forall (_ : not (@eq K k2 k1)) (_ : match assoc_find (@cons Tuple (mkTuple k2 v2) (assoc_add l k1 v1)) k0 with | @none _ => False | @some _ v' => @eq V v0 v' end), or match (if Keq_dec k2 k0 then some V v2 else assoc_find l k0) with | @none _ => False | @some _ v' => @eq V v0 v' end (and (@eq K k0 k1) (@eq V v0 v1)) *)
    intros; unfold assoc_mem in |- *; simpl in |- *; case (Keq_dec k1 k0).
(* Goal: assoc_almost_eqm k0 (assoc_find l) (assoc_find (@cons Tuple (mkTuple k0 v') l)) *)
(* Goal: assoc_almost_eqm k0 (assoc_find (@cons Tuple (mkTuple k0 v0) l)) (assoc_find l) *)
(* Goal: assoc_almost_eqm k0 (assoc_find l) (assoc_find (@cons Tuple (mkTuple k0 v') l)) *)
       intros; absurd (k1 = k0); assumption.
(* Goal: forall (_ : @eq K k' k0) (_ : @eq V v0 v'), @eq K k' k0 *)
(* Goal: forall (_ : not (@eq K k' k0)) (_ : match assoc_find l0 k0 with | @none _ => False | @some _ v' => @eq V v0 v' end), @eq K k' k0 *)
(* Goal: @eq (option V) (assoc_find (@cons Tuple (mkTuple k' v') l0) k0) (assoc_find (assoc_add l0 k' v') k0) *)
       unfold assoc_mem in H; intros; apply H; auto.
Qed.


Lemma assoc_semfind_del :
 forall (l : assoc) (k : K),
 assoc_almost_eqm k (assoc_find l) (assoc_find (assoc_delete l k)).

Proof.
(* Goal: forall (_ : @eq K k' k0) (_ : @eq V v0 v'), @eq K k' k0 *)
(* Goal: forall (_ : not (@eq K k' k0)) (_ : match assoc_find l0 k0 with | @none _ => False | @some _ v' => @eq V v0 v' end), @eq K k' k0 *)
(* Goal: @eq (option V) (assoc_find (@cons Tuple (mkTuple k' v') l0) k0) (assoc_find (assoc_add l0 k' v') k0) *)
unfold assoc_almost_eqm in |- *; simple induction l; auto.
intros; induction  a as (k2, v0); simpl in |- *; case (Keq_dec k2 k1);
(* Goal: forall _ : match (if Keq_dec k2 k0 then some V v1 else assoc_find l k0) with | @none _ => False | @some _ v' => @eq V v0 v' end, or match assoc_find l k0 with | @none _ => False | @some _ v' => @eq V v0 v' end (and (@eq K k0 k2) (@eq V v0 v1)) *)
(* Goal: forall (_ : not (@eq K k2 k1)) (_ : match assoc_find (@cons Tuple (mkTuple k2 v2) (assoc_add l k1 v1)) k0 with | @none _ => False | @some _ v' => @eq V v0 v' end), or match (if Keq_dec k2 k0 then some V v2 else assoc_find l k0) with | @none _ => False | @some _ v' => @eq V v0 v' end (and (@eq K k0 k1) (@eq V v0 v1)) *)
 case (Keq_dec k2 k0).
(* Goal: forall (_ : @eq K k' k0) (_ : @eq V v0 v'), @eq K k' k0 *)
(* Goal: forall (_ : not (@eq K k' k0)) (_ : match assoc_find l0 k0 with | @none _ => False | @some _ v' => @eq V v0 v' end), @eq K k' k0 *)
(* Goal: @eq (option V) (assoc_find (@cons Tuple (mkTuple k' v') l0) k0) (assoc_find (assoc_add l0 k' v') k0) *)
intros; absurd (k1 = k0); auto. transitivity k2; auto.
(* Goal: forall _ : match assoc_find (@cons Tuple (mkTuple k' v') l0) k0 with | @none _ => False | @some _ v' => @eq V v0 v' end, @eq K k' k0 *)
(* Goal: @eq (option V) (assoc_find (@cons Tuple (mkTuple k' v') l0) k0) (assoc_find (assoc_add l0 k' v') k0) *)
intros. simpl in |- *. case (Keq_dec k2 k1); auto.
(* Goal: assoc_almost_eqm k0 (assoc_find l) (assoc_find (@cons Tuple (mkTuple k0 v') l)) *)
(* Goal: assoc_almost_eqm k0 (assoc_find (@cons Tuple (mkTuple k0 v0) l)) (assoc_find l) *)
(* Goal: assoc_almost_eqm k0 (assoc_find l) (assoc_find (@cons Tuple (mkTuple k0 v') l)) *)
   intros; absurd (k2 = k1); assumption.
(* Goal: assoc_almost_eqm k0 (assoc_find l) (assoc_find (@cons Tuple (mkTuple k0 v') l)) *)
(* Goal: assoc_almost_eqm k0 (assoc_find (@cons Tuple (mkTuple k0 v0) l)) (assoc_find l) *)
(* Goal: assoc_almost_eqm k0 (assoc_find l) (assoc_find (@cons Tuple (mkTuple k0 v') l)) *)
intros; apply H; assumption.
(* Goal: forall _ : match assoc_find (@cons Tuple (mkTuple k' v') l0) k0 with | @none _ => False | @some _ v' => @eq V v0 v' end, @eq K k' k0 *)
(* Goal: @eq (option V) (assoc_find (@cons Tuple (mkTuple k' v') l0) k0) (assoc_find (assoc_add l0 k' v') k0) *)
intros; simpl in |- *. case (Keq_dec k2 k1).
(* Goal: assoc_almost_eqm k0 (assoc_find l) (assoc_find (@cons Tuple (mkTuple k0 v') l)) *)
(* Goal: assoc_almost_eqm k0 (assoc_find (@cons Tuple (mkTuple k0 v0) l)) (assoc_find l) *)
(* Goal: assoc_almost_eqm k0 (assoc_find l) (assoc_find (@cons Tuple (mkTuple k0 v') l)) *)
   intros; absurd (k2 = k1); assumption.
(* Goal: forall (_ : @eq K k' k0) (_ : @eq V v0 v'), @eq K k' k0 *)
(* Goal: forall (_ : not (@eq K k' k0)) (_ : match assoc_find l0 k0 with | @none _ => False | @some _ v' => @eq V v0 v' end), @eq K k' k0 *)
(* Goal: @eq (option V) (assoc_find (@cons Tuple (mkTuple k' v') l0) k0) (assoc_find (assoc_add l0 k' v') k0) *)
   intro; apply H; auto.
Qed.


Lemma assoc_del_decrease_1 :
 forall (l : assoc) (k k' : K),
 assoc_find l k = none V -> assoc_find (assoc_delete l k') k = none V.

Proof.
(* Goal: forall (_ : @eq K k' k0) (_ : @eq V v0 v'), @eq K k' k0 *)
(* Goal: forall (_ : not (@eq K k' k0)) (_ : match assoc_find l0 k0 with | @none _ => False | @some _ v' => @eq V v0 v' end), @eq K k' k0 *)
(* Goal: @eq (option V) (assoc_find (@cons Tuple (mkTuple k' v') l0) k0) (assoc_find (assoc_add l0 k' v') k0) *)
simple induction l; simpl in |- *; auto.
(* Goal: forall (_ : not (@eq K k' k0)) (_ : @eq (option V) (some V v0) (assoc_find l0 k0)), @eq K k' k0 *)
(* Goal: @eq (option V) (assoc_find (@cons Tuple (mkTuple k' v') l0) k0) (assoc_find (assoc_add l0 k' v') k0) *)
simple induction a; simpl in |- *; intros.
(* Goal: @eq K k' k0 *)
generalize H0.
(* Goal: forall _ : match assoc_find (@cons Tuple (mkTuple k' v') l0) k0 with | @none _ => False | @some _ v' => @eq V v0 v' end, @eq K k' k0 *)
(* Goal: @eq (option V) (assoc_find (@cons Tuple (mkTuple k' v') l0) k0) (assoc_find (assoc_add l0 k' v') k0) *)
case (Keq_dec k0 k1); simpl in |- *.
(* Goal: forall (_ : not (@eq K k' k0)) (_ : @eq (option V) (some V v0) (assoc_find l0 k0)), @eq K k' k0 *)
(* Goal: @eq (option V) (assoc_find (@cons Tuple (mkTuple k' v') l0) k0) (assoc_find (assoc_add l0 k' v') k0) *)
intros.
(* Goal: @eq (option V) (assoc_find (if Keq_dec k0 k' then assoc_delete l0 k' else @cons Tuple (mkTuple k0 v0) (assoc_delete l0 k')) k1) (none V) *)
(* Goal: forall (_ : not (@eq K k0 k1)) (_ : @eq (option V) (assoc_find l0 k1) (none V)), @eq (option V) (assoc_find (if Keq_dec k0 k' then assoc_delete l0 k' else @cons Tuple (mkTuple k0 v0) (assoc_delete l0 k')) k1) (none V) *)
discriminate H1.
(* Goal: forall (_ : not (@eq K k' k0)) (_ : @eq (option V) (some V v0) (assoc_find l0 k0)), @eq K k' k0 *)
(* Goal: @eq (option V) (assoc_find (@cons Tuple (mkTuple k' v') l0) k0) (assoc_find (assoc_add l0 k' v') k0) *)
intros; case (Keq_dec k0 k'); intros.
(* Goal: assoc_almost_eqm k0 (assoc_find l) (assoc_find (@cons Tuple (mkTuple k0 v') l)) *)
(* Goal: assoc_almost_eqm k0 (assoc_find (@cons Tuple (mkTuple k0 v0) l)) (assoc_find l) *)
(* Goal: assoc_almost_eqm k0 (assoc_find l) (assoc_find (@cons Tuple (mkTuple k0 v') l)) *)
  apply H; assumption.
(* Goal: forall (_ : not (@eq K k' k0)) (_ : @eq (option V) (some V v0) (assoc_find l0 k0)), @eq K k' k0 *)
(* Goal: @eq (option V) (assoc_find (@cons Tuple (mkTuple k' v') l0) k0) (assoc_find (assoc_add l0 k' v') k0) *)
  simpl in |- *; case (Keq_dec k0 k1); intros.
(* Goal: assoc_almost_eqm k0 (assoc_find l) (assoc_find (@cons Tuple (mkTuple k0 v') l)) *)
(* Goal: assoc_almost_eqm k0 (assoc_find (@cons Tuple (mkTuple k0 v0) l)) (assoc_find l) *)
(* Goal: assoc_almost_eqm k0 (assoc_find l) (assoc_find (@cons Tuple (mkTuple k0 v') l)) *)
    absurd (k0 = k1); assumption.
(* Goal: assoc_almost_eqm k0 (assoc_find l) (assoc_find (@cons Tuple (mkTuple k0 v') l)) *)
(* Goal: assoc_almost_eqm k0 (assoc_find (@cons Tuple (mkTuple k0 v0) l)) (assoc_find l) *)
(* Goal: assoc_almost_eqm k0 (assoc_find l) (assoc_find (@cons Tuple (mkTuple k0 v') l)) *)
    apply H; assumption.
Qed.


Lemma assoc_del_decrease_2 :
 forall (l : assoc) (k k' : K) (v : V),
 assoc_find (assoc_delete l k') k = some V v -> assoc_find l k = some V v.

Proof.
(* Goal: forall (_ : not (@eq K k' k0)) (_ : @eq (option V) (some V v0) (assoc_find l0 k0)), @eq K k' k0 *)
(* Goal: @eq (option V) (assoc_find (@cons Tuple (mkTuple k' v') l0) k0) (assoc_find (assoc_add l0 k' v') k0) *)
intros.
(* Goal: forall _ : match assoc_find (@cons Tuple (mkTuple k' v') l0) k0 with | @none _ => False | @some _ v' => @eq V v0 v' end, @eq K k' k0 *)
(* Goal: @eq (option V) (assoc_find (@cons Tuple (mkTuple k' v') l0) k0) (assoc_find (assoc_add l0 k' v') k0) *)
induction  l as [| a l Hrecl]; simpl in |- *.
(* Goal: @eq (option V) (none V) (some V v0) *)
(* Goal: @eq (option V) match a with | {| k := k; v := v |} => if Keq_dec k k0 then some V v else assoc_find l k0 end (some V v0) *)
generalize H; simpl in |- *; intro myhyp; discriminate myhyp.
induction  a as (k1, v1).
(* Goal: forall _ : match (if Keq_dec k1 k0 then some V v1 else assoc_find l k0) with | @none _ => False | @some _ v' => @eq V v0 v' end, @eq V v0 v1 *)
(* Goal: forall (_ : not (@eq K k2 k0)) (_ : @eq K k2 k1) (_ : match assoc_find (@cons Tuple (mkTuple k1 v1) l) k0 with | @none _ => False | @some _ v' => @eq V v0 v' end), or match assoc_find l k0 with | @none _ => False | @some _ v' => @eq V v0 v' end (and (@eq K k0 k1) (@eq V v0 v1)) *)
(* Goal: forall (_ : not (@eq K k2 k1)) (_ : match assoc_find (@cons Tuple (mkTuple k2 v2) (assoc_add l k1 v1)) k0 with | @none _ => False | @some _ v' => @eq V v0 v' end), or match (if Keq_dec k2 k0 then some V v2 else assoc_find l k0) with | @none _ => False | @some _ v' => @eq V v0 v' end (and (@eq K k0 k1) (@eq V v0 v1)) *)
case (Keq_dec k1 k0).
(* Goal: forall (_ : forall (k : K) (_ : not (@eq K k k')), @eq (option V) (assoc_find l k) (assoc_find l' k)) (_ : match assoc_find l' k0 with | @none _ => False | @some _ v' => @eq V v0 v' end), match assoc_find l k0 with | @none _ => False | @some _ v' => @eq V v0 v' end *)
(* Goal: assoc_almost_eqm k' (assoc_find l) (assoc_find l') *)
intro.
(* Goal: forall (_ : @eq K k' k0) (_ : @eq V v0 v'), @eq K k' k0 *)
(* Goal: forall (_ : not (@eq K k' k0)) (_ : match assoc_find l0 k0 with | @none _ => False | @some _ v' => @eq V v0 v' end), @eq K k' k0 *)
(* Goal: @eq (option V) (assoc_find (@cons Tuple (mkTuple k' v') l0) k0) (assoc_find (assoc_add l0 k' v') k0) *)
transitivity (assoc_find (assoc_delete (mkTuple k1 v1 :: l) k') k0); auto.
(* Goal: @eq (option V) (some V v1) (assoc_find (assoc_delete (@cons Tuple (mkTuple k1 v1) l) k') k0) *)
(* Goal: forall _ : not (@eq K k1 k0), @eq (option V) (assoc_find l k0) (some V v0) *)
rewrite e.
(* Goal: forall _ : match assoc_find (@cons Tuple (mkTuple k' v') l0) k0 with | @none _ => False | @some _ v' => @eq V v0 v' end, @eq K k' k0 *)
(* Goal: @eq (option V) (assoc_find (@cons Tuple (mkTuple k' v') l0) k0) (assoc_find (assoc_add l0 k' v') k0) *)
simpl in |- *.
(* Goal: @eq (option V) (some V v1) (assoc_find (if Keq_dec k0 k' then assoc_delete l k' else @cons Tuple (mkTuple k0 v1) (assoc_delete l k')) k0) *)
(* Goal: forall _ : not (@eq K k1 k0), @eq (option V) (assoc_find l k0) (some V v0) *)
case (Keq_dec k0 k').
(* Goal: forall (_ : forall (k : K) (_ : not (@eq K k k')), @eq (option V) (assoc_find l k) (assoc_find l' k)) (_ : match assoc_find l' k0 with | @none _ => False | @some _ v' => @eq V v0 v' end), match assoc_find l k0 with | @none _ => False | @some _ v' => @eq V v0 v' end *)
(* Goal: assoc_almost_eqm k' (assoc_find l) (assoc_find l') *)
intro.
(* Goal: @eq (option V) (some V v1) (assoc_find (assoc_delete l k') k0) *)
(* Goal: forall _ : not (@eq K k0 k'), @eq (option V) (some V v1) (assoc_find (@cons Tuple (mkTuple k0 v1) (assoc_delete l k')) k0) *)
(* Goal: forall _ : not (@eq K k1 k0), @eq (option V) (assoc_find l k0) (some V v0) *)
rewrite e in H.
(* Goal: @eq (option V) (some V v1) (assoc_find (assoc_delete l k') k0) *)
(* Goal: forall _ : not (@eq K k0 k'), @eq (option V) (some V v1) (assoc_find (@cons Tuple (mkTuple k0 v1) (assoc_delete l k')) k0) *)
(* Goal: forall _ : not (@eq K k1 k0), @eq (option V) (assoc_find l k0) (some V v0) *)
rewrite e0 in H.
(* Goal: @eq (option V) (some V v1) (assoc_find (assoc_delete l k') k0) *)
(* Goal: forall _ : not (@eq K k0 k'), @eq (option V) (some V v1) (assoc_find (@cons Tuple (mkTuple k0 v1) (assoc_delete l k')) k0) *)
(* Goal: forall _ : not (@eq K k1 k0), @eq (option V) (assoc_find l k0) (some V v0) *)
absurd (assoc_find (assoc_delete (mkTuple k' v1 :: l) k') k' = none V).
(* Goal: not (@eq (option V) (assoc_find (assoc_delete (@cons Tuple (mkTuple k' v1) l) k') k') (none V)) *)
(* Goal: @eq (option V) (assoc_find (assoc_delete (@cons Tuple (mkTuple k' v1) l) k') k') (none V) *)
(* Goal: forall _ : not (@eq K k0 k'), @eq (option V) (some V v1) (assoc_find (@cons Tuple (mkTuple k0 v1) (assoc_delete l k')) k0) *)
(* Goal: forall _ : not (@eq K k1 k0), @eq (option V) (assoc_find l k0) (some V v0) *)
unfold not in |- *; rewrite H; intro myhyp; discriminate myhyp.
(* Goal: forall (_ : @eq K k' k0) (_ : @eq V v0 v'), @eq K k' k0 *)
(* Goal: forall (_ : not (@eq K k' k0)) (_ : match assoc_find l0 k0 with | @none _ => False | @some _ v' => @eq V v0 v' end), @eq K k' k0 *)
(* Goal: @eq (option V) (assoc_find (@cons Tuple (mkTuple k' v') l0) k0) (assoc_find (assoc_add l0 k' v') k0) *)
apply assoc_del_correct_1; auto.
(* Goal: forall _ : match assoc_find (@cons Tuple (mkTuple k' v') l0) k0 with | @none _ => False | @some _ v' => @eq V v0 v' end, @eq K k' k0 *)
(* Goal: @eq (option V) (assoc_find (@cons Tuple (mkTuple k' v') l0) k0) (assoc_find (assoc_add l0 k' v') k0) *)
intros; simpl in |- *. case (Keq_dec k0 k0); auto.
(* Goal: forall (_ : @eq K k' k0) (_ : @eq V v0 v'), @eq K k' k0 *)
(* Goal: forall (_ : not (@eq K k' k0)) (_ : match assoc_find l0 k0 with | @none _ => False | @some _ v' => @eq V v0 v' end), @eq K k' k0 *)
(* Goal: @eq (option V) (assoc_find (@cons Tuple (mkTuple k' v') l0) k0) (assoc_find (assoc_add l0 k' v') k0) *)
intro; absurd (k0 = k0); auto.
(* Goal: forall _ : not (@eq K k1 k0), @eq (option V) (assoc_find l k0) (some V v0) *)
intro; apply Hrecl.
(* Goal: forall (_ : @eq K k' k0) (_ : @eq V v0 v'), @eq K k' k0 *)
(* Goal: forall (_ : not (@eq K k' k0)) (_ : match assoc_find l0 k0 with | @none _ => False | @some _ v' => @eq V v0 v' end), @eq K k' k0 *)
(* Goal: @eq (option V) (assoc_find (@cons Tuple (mkTuple k' v') l0) k0) (assoc_find (assoc_add l0 k' v') k0) *)
  transitivity (assoc_find (assoc_delete (mkTuple k1 v1 :: l) k') k0); auto.
(* Goal: forall _ : match assoc_find (@cons Tuple (mkTuple k' v') l0) k0 with | @none _ => False | @some _ v' => @eq V v0 v' end, @eq K k' k0 *)
(* Goal: @eq (option V) (assoc_find (@cons Tuple (mkTuple k' v') l0) k0) (assoc_find (assoc_add l0 k' v') k0) *)
simpl in |- *.
(* Goal: forall (_ : @eq K k' k0) (_ : @eq V v0 v'), @eq K k' k0 *)
(* Goal: forall (_ : not (@eq K k' k0)) (_ : match assoc_find l0 k0 with | @none _ => False | @some _ v' => @eq V v0 v' end), @eq K k' k0 *)
(* Goal: @eq (option V) (assoc_find (@cons Tuple (mkTuple k' v') l0) k0) (assoc_find (assoc_add l0 k' v') k0) *)
case (Keq_dec k1 k'); auto.
(* Goal: forall _ : match assoc_find (@cons Tuple (mkTuple k' v') l0) k0 with | @none _ => False | @some _ v' => @eq V v0 v' end, @eq K k' k0 *)
(* Goal: @eq (option V) (assoc_find (@cons Tuple (mkTuple k' v') l0) k0) (assoc_find (assoc_add l0 k' v') k0) *)
simpl in |- *.
(* Goal: forall (_ : forall (k : K) (_ : not (@eq K k k')), @eq (option V) (assoc_find l k) (assoc_find l' k)) (_ : match assoc_find l' k0 with | @none _ => False | @some _ v' => @eq V v0 v' end), match assoc_find l k0 with | @none _ => False | @some _ v' => @eq V v0 v' end *)
(* Goal: assoc_almost_eqm k' (assoc_find l) (assoc_find l') *)
intro.
(* Goal: forall _ : match (if Keq_dec k1 k0 then some V v1 else assoc_find l k0) with | @none _ => False | @some _ v' => @eq V v0 v' end, @eq V v0 v1 *)
(* Goal: forall (_ : not (@eq K k2 k0)) (_ : @eq K k2 k1) (_ : match assoc_find (@cons Tuple (mkTuple k1 v1) l) k0 with | @none _ => False | @some _ v' => @eq V v0 v' end), or match assoc_find l k0 with | @none _ => False | @some _ v' => @eq V v0 v' end (and (@eq K k0 k1) (@eq V v0 v1)) *)
(* Goal: forall (_ : not (@eq K k2 k1)) (_ : match assoc_find (@cons Tuple (mkTuple k2 v2) (assoc_add l k1 v1)) k0 with | @none _ => False | @some _ v' => @eq V v0 v' end), or match (if Keq_dec k2 k0 then some V v2 else assoc_find l k0) with | @none _ => False | @some _ v' => @eq V v0 v' end (and (@eq K k0 k1) (@eq V v0 v1)) *)
case (Keq_dec k1 k0).
(* Goal: assoc_almost_eqm k0 (assoc_find l) (assoc_find (@cons Tuple (mkTuple k0 v') l)) *)
(* Goal: assoc_almost_eqm k0 (assoc_find (@cons Tuple (mkTuple k0 v0) l)) (assoc_find l) *)
(* Goal: assoc_almost_eqm k0 (assoc_find l) (assoc_find (@cons Tuple (mkTuple k0 v') l)) *)
intro; absurd (k1 = k0); assumption.
(* Goal: forall (_ : @eq K k' k0) (_ : @eq V v0 v'), @eq K k' k0 *)
(* Goal: forall (_ : not (@eq K k' k0)) (_ : match assoc_find l0 k0 with | @none _ => False | @some _ v' => @eq V v0 v' end), @eq K k' k0 *)
(* Goal: @eq (option V) (assoc_find (@cons Tuple (mkTuple k' v') l0) k0) (assoc_find (assoc_add l0 k' v') k0) *)
auto.
Qed.


Lemma assoc_del_decrease_3 :
 forall (l : assoc) (k k' : K) (v v' : V),
 assoc_find l k = some V v ->
 assoc_find (assoc_delete l k') k = some V v' -> v = v'.

Proof.
(* Goal: forall (_ : not (@eq K k' k0)) (_ : @eq (option V) (some V v0) (assoc_find l0 k0)), @eq K k' k0 *)
(* Goal: @eq (option V) (assoc_find (@cons Tuple (mkTuple k' v') l0) k0) (assoc_find (assoc_add l0 k' v') k0) *)
intros.
(* Goal: @eq V v0 v' *)
cut (assoc_find l k0 = some V v').
(* Goal: forall (_ : @eq K k' k0) (_ : @eq V v0 v'), @eq K k' k0 *)
(* Goal: forall (_ : not (@eq K k' k0)) (_ : match assoc_find l0 k0 with | @none _ => False | @some _ v' => @eq V v0 v' end), @eq K k' k0 *)
(* Goal: @eq (option V) (assoc_find (@cons Tuple (mkTuple k' v') l0) k0) (assoc_find (assoc_add l0 k' v') k0) *)
rewrite H; auto.
(* Goal: forall _ : @eq (option V) (some V v0) (some V v'), @eq V v0 v' *)
(* Goal: @eq (option V) (assoc_find l k0) (some V v') *)
intro INJ; injection INJ.
(* Goal: forall (_ : @eq K k' k0) (_ : @eq V v0 v'), @eq K k' k0 *)
(* Goal: forall (_ : not (@eq K k' k0)) (_ : match assoc_find l0 k0 with | @none _ => False | @some _ v' => @eq V v0 v' end), @eq K k' k0 *)
(* Goal: @eq (option V) (assoc_find (@cons Tuple (mkTuple k' v') l0) k0) (assoc_find (assoc_add l0 k' v') k0) *)
auto.
(* Goal: assoc_almost_eqm k0 (assoc_find l) (assoc_find (@cons Tuple (mkTuple k0 v') l)) *)
(* Goal: assoc_almost_eqm k0 (assoc_find (@cons Tuple (mkTuple k0 v0) l)) (assoc_find l) *)
(* Goal: assoc_almost_eqm k0 (assoc_find l) (assoc_find (@cons Tuple (mkTuple k0 v') l)) *)
apply assoc_del_decrease_2 with k'; assumption.
Qed.


Lemma assoc_del_correct_4 :
 forall (l : assoc) (k k' : K) (v : V),
 ~ assoc_hasmem l k v -> ~ assoc_hasmem (assoc_delete l k') k v.

Proof.
(* Goal: forall (_ : @eq K k' k0) (_ : @eq V v0 v'), @eq K k' k0 *)
(* Goal: forall (_ : not (@eq K k' k0)) (_ : match assoc_find l0 k0 with | @none _ => False | @some _ v' => @eq V v0 v' end), @eq K k' k0 *)
(* Goal: @eq (option V) (assoc_find (@cons Tuple (mkTuple k' v') l0) k0) (assoc_find (assoc_add l0 k' v') k0) *)
intros; intro; absurd (assoc_hasmem l k0 v0); auto.
(* Goal: assoc_hasmem l k0 v0 *)
apply assoc_find_hasmem.
(* Goal: @eq (option V) (assoc_find l k0) (some V v0) *)
apply assoc_del_decrease_2 with k'.
(* Goal: @eq (option V) (assoc_find (assoc_delete l k') k0) (some V v0) *)
apply assoc_hasmem_find.
(* Goal: forall (_ : @eq K k' k0) (_ : @eq V v0 v'), @eq K k' k0 *)
(* Goal: forall (_ : not (@eq K k' k0)) (_ : match assoc_find l0 k0 with | @none _ => False | @some _ v' => @eq V v0 v' end), @eq K k' k0 *)
(* Goal: @eq (option V) (assoc_find (@cons Tuple (mkTuple k' v') l0) k0) (assoc_find (assoc_add l0 k' v') k0) *)
auto.
Qed.


Lemma assoc_del_correct_5 :
 forall (l : assoc) (k k' : K),
 ~ assoc_mem l k -> ~ assoc_mem (assoc_delete l k') k.

Proof.
(* Goal: forall (_ : @eq K k' k0) (_ : @eq V v0 v'), @eq K k' k0 *)
(* Goal: forall (_ : not (@eq K k' k0)) (_ : match assoc_find l0 k0 with | @none _ => False | @some _ v' => @eq V v0 v' end), @eq K k' k0 *)
(* Goal: @eq (option V) (assoc_find (@cons Tuple (mkTuple k' v') l0) k0) (assoc_find (assoc_add l0 k' v') k0) *)
intros; intro; absurd (assoc_mem l k0); auto.
(* Goal: assoc_mem l k0 *)
cut (exists v : V, assoc_hasmem (assoc_delete l k') k0 v).
(* Goal: forall (_ : @eq K k' k0) (_ : @eq V v0 v'), @eq K k' k0 *)
(* Goal: forall (_ : not (@eq K k' k0)) (_ : match assoc_find l0 k0 with | @none _ => False | @some _ v' => @eq V v0 v' end), @eq K k' k0 *)
(* Goal: @eq (option V) (assoc_find (@cons Tuple (mkTuple k' v') l0) k0) (assoc_find (assoc_add l0 k' v') k0) *)
intro EXISTS; elim EXISTS; intros; apply assoc_hasmem_mem with x; auto.
apply assoc_find_hasmem; apply assoc_del_decrease_2 with k';
(* Goal: assoc_almost_eqm k0 (assoc_find l) (assoc_find (@cons Tuple (mkTuple k0 v') l)) *)
(* Goal: assoc_almost_eqm k0 (assoc_find (@cons Tuple (mkTuple k0 v0) l)) (assoc_find l) *)
(* Goal: assoc_almost_eqm k0 (assoc_find l) (assoc_find (@cons Tuple (mkTuple k0 v') l)) *)
 apply assoc_hasmem_find; assumption.
(* Goal: assoc_almost_eqm k0 (assoc_find l) (assoc_find (@cons Tuple (mkTuple k0 v') l)) *)
(* Goal: assoc_almost_eqm k0 (assoc_find (@cons Tuple (mkTuple k0 v0) l)) (assoc_find l) *)
(* Goal: assoc_almost_eqm k0 (assoc_find l) (assoc_find (@cons Tuple (mkTuple k0 v') l)) *)
apply assoc_mem_hasmem; assumption.
Qed.




(**************************************************)
(*  some decidability properties                  *)
(**************************************************)



Lemma assoc_mem_dec :
 forall (l : assoc) (k : K), {assoc_mem l k} + {~ assoc_mem l k}.

Proof.
(* Goal: forall (v _ : V) (_ : match assoc_find l k0 with | @none _ => False | @some _ v'0 => @eq V v v'0 end) (_ : not match assoc_find l k0 with | @none _ => False | @some _ v'0 => @eq V v v'0 end), @eq K k1 k0 *)
(* Goal: @eq (option V) (assoc_find l k0) (assoc_find (assoc_delete l k1) k0) *)
(* Goal: assoc_almost_eqm k1 (assoc_find l) (assoc_find (assoc_delete l k1)) *)
unfold assoc_mem in |- *; intros; case (assoc_find l k0).
(* Goal: forall (_ : @eq K k' k0) (_ : @eq V v0 v'), @eq K k' k0 *)
(* Goal: forall (_ : not (@eq K k' k0)) (_ : match assoc_find l0 k0 with | @none _ => False | @some _ v' => @eq V v0 v' end), @eq K k' k0 *)
(* Goal: @eq (option V) (assoc_find (@cons Tuple (mkTuple k' v') l0) k0) (assoc_find (assoc_add l0 k' v') k0) *)
right; auto.
(* Goal: forall (_ : @eq K k' k0) (_ : @eq V v0 v'), @eq K k' k0 *)
(* Goal: forall (_ : not (@eq K k' k0)) (_ : match assoc_find l0 k0 with | @none _ => False | @some _ v' => @eq V v0 v' end), @eq K k' k0 *)
(* Goal: @eq (option V) (assoc_find (@cons Tuple (mkTuple k' v') l0) k0) (assoc_find (assoc_add l0 k' v') k0) *)
left; auto.
Qed.


Lemma assoc_hasmem_dec :
 forall (Veq_dec : forall x y : V, {x = y} + {x <> y}) 
   (l : assoc) (k : K) (v : V), {assoc_hasmem l k v} + {~ assoc_hasmem l k v}.

Proof.
(* Goal: forall (v _ : V) (_ : match assoc_find l k0 with | @none _ => False | @some _ v'0 => @eq V v v'0 end) (_ : not match assoc_find l k0 with | @none _ => False | @some _ v'0 => @eq V v v'0 end), @eq K k1 k0 *)
(* Goal: @eq (option V) (assoc_find l k0) (assoc_find (assoc_delete l k1) k0) *)
(* Goal: assoc_almost_eqm k1 (assoc_find l) (assoc_find (assoc_delete l k1)) *)
intros; unfold assoc_hasmem in |- *; case (assoc_find l k0).
(* Goal: forall (_ : @eq K k' k0) (_ : @eq V v0 v'), @eq K k' k0 *)
(* Goal: forall (_ : not (@eq K k' k0)) (_ : match assoc_find l0 k0 with | @none _ => False | @some _ v' => @eq V v0 v' end), @eq K k' k0 *)
(* Goal: @eq (option V) (assoc_find (@cons Tuple (mkTuple k' v') l0) k0) (assoc_find (assoc_add l0 k' v') k0) *)
right; auto.
(* Goal: forall v : V, sumbool (@eq V v0 v) (not (@eq V v0 v)) *)
intros; apply Veq_dec.
Qed.


Lemma assoc_hasmem_ex_dec :
 forall (Veq_dec : forall x y : V, {x = y} + {x <> y}) 
   (l : assoc) (k : K) (v : V),
 {(exists v : V, assoc_hasmem l k v)} +
 {~ (exists v : V, assoc_hasmem l k v)}.

Proof.
(* Goal: forall (_ : not (@eq K k' k0)) (_ : @eq (option V) (some V v0) (assoc_find l0 k0)), @eq K k' k0 *)
(* Goal: @eq (option V) (assoc_find (@cons Tuple (mkTuple k' v') l0) k0) (assoc_find (assoc_add l0 k' v') k0) *)
intros.
(* Goal: forall (l : assoc) (k : K) (v v' : V) (_ : assoc_hasmem l k v) (_ : assoc_hasmem l k v'), @eq V v' v *)
unfold assoc_hasmem in |- *.
(* Goal: forall (v _ : V) (_ : match assoc_find l k0 with | @none _ => False | @some _ v'0 => @eq V v v'0 end) (_ : not match assoc_find l k0 with | @none _ => False | @some _ v'0 => @eq V v v'0 end), @eq K k1 k0 *)
(* Goal: @eq (option V) (assoc_find l k0) (assoc_find (assoc_delete l k1) k0) *)
(* Goal: assoc_almost_eqm k1 (assoc_find l) (assoc_find (assoc_delete l k1)) *)
case (assoc_find l k0).
(* Goal: sumbool (@ex V (fun _ : V => False)) (not (@ex V (fun _ : V => False))) *)
(* Goal: forall v : V, sumbool (@ex V (fun v0 : V => @eq V v0 v)) (not (@ex V (fun v0 : V => @eq V v0 v))) *)
right.
(* Goal: forall (_ : forall (k : K) (_ : not (@eq K k k')), @eq (option V) (assoc_find l k) (assoc_find l' k)) (_ : match assoc_find l' k0 with | @none _ => False | @some _ v' => @eq V v0 v' end), match assoc_find l k0 with | @none _ => False | @some _ v' => @eq V v0 v' end *)
(* Goal: assoc_almost_eqm k' (assoc_find l) (assoc_find l') *)
intro.
(* Goal: forall (_ : @eq K k' k0) (_ : @eq V v0 v'), @eq K k' k0 *)
(* Goal: forall (_ : not (@eq K k' k0)) (_ : match assoc_find l0 k0 with | @none _ => False | @some _ v' => @eq V v0 v' end), @eq K k' k0 *)
(* Goal: @eq (option V) (assoc_find (@cons Tuple (mkTuple k' v') l0) k0) (assoc_find (assoc_add l0 k' v') k0) *)
elim H; auto.
(* Goal: forall (_ : forall (k : K) (_ : not (@eq K k k')), @eq (option V) (assoc_find l k) (assoc_find l' k)) (_ : match assoc_find l' k0 with | @none _ => False | @some _ v' => @eq V v0 v' end), match assoc_find l k0 with | @none _ => False | @some _ v' => @eq V v0 v' end *)
(* Goal: assoc_almost_eqm k' (assoc_find l) (assoc_find l') *)
intro.
(* Goal: sumbool (@ex V (fun v : V => @eq V v v1)) (not (@ex V (fun v : V => @eq V v v1))) *)
left.
(* Goal: @ex V (fun v : V => @eq V v v1) *)
split with v1.
(* Goal: forall (_ : @eq K k' k0) (_ : @eq V v0 v'), @eq K k' k0 *)
(* Goal: forall (_ : not (@eq K k' k0)) (_ : match assoc_find l0 k0 with | @none _ => False | @some _ v' => @eq V v0 v' end), @eq K k' k0 *)
(* Goal: @eq (option V) (assoc_find (@cons Tuple (mkTuple k' v') l0) k0) (assoc_find (assoc_add l0 k' v') k0) *)
auto.
Qed.


Lemma assoc_add_mem_choice :
 forall (b0 b : assoc) (k k0 : K) (v0 : V),
 b = assoc_add b0 k0 v0 -> assoc_mem b k -> assoc_mem b0 k \/ k = k0.

Proof.
(* Goal: assoc_almost_eqm k' (assoc_find l) (assoc_find l') *)
intros until 1. rewrite H. unfold assoc_mem in |- *.
replace (assoc_find (assoc_add b0 k1 v0) k0) with
 (assoc_find (mkTuple k1 v0 :: b0) k0).
(* Goal: forall _ : match assoc_find (@cons Tuple (mkTuple k' v') l0) k0 with | @none _ => False | @some _ v' => @eq V v0 v' end, @eq K k' k0 *)
(* Goal: @eq (option V) (assoc_find (@cons Tuple (mkTuple k' v') l0) k0) (assoc_find (assoc_add l0 k' v') k0) *)
  simpl in |- *. case (Keq_dec k1 k0).
(* Goal: forall (_ : @eq K k' k0) (_ : @eq V v0 v'), @eq K k' k0 *)
(* Goal: forall (_ : not (@eq K k' k0)) (_ : match assoc_find l0 k0 with | @none _ => False | @some _ v' => @eq V v0 v' end), @eq K k' k0 *)
(* Goal: @eq (option V) (assoc_find (@cons Tuple (mkTuple k' v') l0) k0) (assoc_find (assoc_add l0 k' v') k0) *)
    intros; right; auto.
(* Goal: forall (_ : @eq K k' k0) (_ : @eq V v0 v'), @eq K k' k0 *)
(* Goal: forall (_ : not (@eq K k' k0)) (_ : match assoc_find l0 k0 with | @none _ => False | @some _ v' => @eq V v0 v' end), @eq K k' k0 *)
(* Goal: @eq (option V) (assoc_find (@cons Tuple (mkTuple k' v') l0) k0) (assoc_find (assoc_add l0 k' v') k0) *)
    intros; left; auto.
  cut
   (assoc_eqm (assoc_find (mkTuple k1 v0 :: b0))
      (assoc_find (assoc_add b0 k1 v0))).
(* Goal: forall (_ : @eq K k' k0) (_ : @eq V v0 v'), @eq K k' k0 *)
(* Goal: forall (_ : not (@eq K k' k0)) (_ : match assoc_find l0 k0 with | @none _ => False | @some _ v' => @eq V v0 v' end), @eq K k' k0 *)
(* Goal: @eq (option V) (assoc_find (@cons Tuple (mkTuple k' v') l0) k0) (assoc_find (assoc_add l0 k' v') k0) *)
    unfold assoc_eqm in |- *; auto.
(* Goal: forall (_ : @eq K k' k0) (_ : @eq V v0 v'), @eq K k' k0 *)
(* Goal: forall (_ : not (@eq K k' k0)) (_ : match assoc_find l0 k0 with | @none _ => False | @some _ v' => @eq V v0 v' end), @eq K k' k0 *)
(* Goal: @eq (option V) (assoc_find (@cons Tuple (mkTuple k' v') l0) k0) (assoc_find (assoc_add l0 k' v') k0) *)
    apply assoc_add_egale_cons; auto.
Qed.


Lemma assoc_add_hasmem_choice :
 forall (b0 b : assoc) (k k0 : K) (v v0 : V),
 b = assoc_add b0 k0 v0 ->
 assoc_hasmem b k v -> assoc_hasmem b0 k v \/ k = k0 /\ v = v0. 

Proof.
(* Goal: forall (b0 b : assoc) (k k0 : K) (v v0 : V) (_ : @eq assoc b (assoc_add b0 k0 v0)) (_ : assoc_hasmem b k v), or (assoc_hasmem b0 k v) (and (@eq K k k0) (@eq V v v0)) *)
simple induction b0.
intros; right; rewrite H in H0; generalize H0; simpl in |- *;
(* Goal: forall _ : match assoc_find (@cons Tuple (mkTuple k' v') l0) k0 with | @none _ => False | @some _ v' => @eq V v0 v' end, @eq K k' k0 *)
(* Goal: @eq (option V) (assoc_find (@cons Tuple (mkTuple k' v') l0) k0) (assoc_find (assoc_add l0 k' v') k0) *)
 unfold assoc_hasmem in |- *; simpl in |- *.
(* Goal: forall (_ : @eq K k' k0) (_ : @eq V v0 v'), @eq K k' k0 *)
(* Goal: forall (_ : not (@eq K k' k0)) (_ : match assoc_find l0 k0 with | @none _ => False | @some _ v' => @eq V v0 v' end), @eq K k' k0 *)
(* Goal: @eq (option V) (assoc_find (@cons Tuple (mkTuple k' v') l0) k0) (assoc_find (assoc_add l0 k' v') k0) *)
case (Keq_dec k1 k0); auto.
(* Goal: @eq V v1 v0 *)
(* Goal: @eq V v1 v0 *)
intros; contradiction.

(* Goal: forall _ : match assoc_find (@cons Tuple (mkTuple k' v') l0) k0 with | @none _ => False | @some _ v' => @eq V v0 v' end, @eq K k' k0 *)
(* Goal: @eq (option V) (assoc_find (@cons Tuple (mkTuple k' v') l0) k0) (assoc_find (assoc_add l0 k' v') k0) *)
intros until 2; unfold assoc_hasmem in |- *; simpl in |- *.
induction  a as (k2, v2).
(* Goal: forall _ : match assoc_find (@cons Tuple (mkTuple k' v') l0) k0 with | @none _ => False | @some _ v' => @eq V v0 v' end, @eq K k' k0 *)
(* Goal: @eq (option V) (assoc_find (@cons Tuple (mkTuple k' v') l0) k0) (assoc_find (assoc_add l0 k' v') k0) *)
rewrite H0; simpl in |- *.
(* Goal: forall _ : match assoc_find (if Keq_dec k2 k1 then @cons Tuple (mkTuple k1 v1) l else @cons Tuple (mkTuple k2 v2) (assoc_add l k1 v1)) k0 with | @none _ => False | @some _ v' => @eq V v0 v' end, or match (if Keq_dec k2 k0 then some V v2 else assoc_find l k0) with | @none _ => False | @some _ v' => @eq V v0 v' end (and (@eq K k0 k1) (@eq V v0 v1)) *)
case (Keq_dec k2 k1).
(* Goal: forall _ : match (if Keq_dec k2 k0 then some V v1 else assoc_find l k0) with | @none _ => False | @some _ v' => @eq V v0 v' end, or match assoc_find l k0 with | @none _ => False | @some _ v' => @eq V v0 v' end (and (@eq K k0 k2) (@eq V v0 v1)) *)
(* Goal: forall (_ : not (@eq K k2 k1)) (_ : match assoc_find (@cons Tuple (mkTuple k2 v2) (assoc_add l k1 v1)) k0 with | @none _ => False | @some _ v' => @eq V v0 v' end), or match (if Keq_dec k2 k0 then some V v2 else assoc_find l k0) with | @none _ => False | @some _ v' => @eq V v0 v' end (and (@eq K k0 k1) (@eq V v0 v1)) *)
case (Keq_dec k2 k0).
(* Goal: sumbool (@ex V (fun _ : V => False)) (not (@ex V (fun _ : V => False))) *)
(* Goal: forall v : V, sumbool (@ex V (fun v0 : V => @eq V v0 v)) (not (@ex V (fun v0 : V => @eq V v0 v))) *)
intros; right.
(* Goal: and (@eq K k0 k1) (@eq V v0 v1) *)
(* Goal: forall (_ : not (@eq K k2 k0)) (_ : @eq K k2 k1) (_ : match assoc_find (@cons Tuple (mkTuple k1 v1) l) k0 with | @none _ => False | @some _ v' => @eq V v0 v' end), or match assoc_find l k0 with | @none _ => False | @some _ v' => @eq V v0 v' end (and (@eq K k0 k1) (@eq V v0 v1)) *)
(* Goal: forall (_ : not (@eq K k2 k1)) (_ : match assoc_find (@cons Tuple (mkTuple k2 v2) (assoc_add l k1 v1)) k0 with | @none _ => False | @some _ v' => @eq V v0 v' end), or match (if Keq_dec k2 k0 then some V v2 else assoc_find l k0) with | @none _ => False | @some _ v' => @eq V v0 v' end (and (@eq K k0 k1) (@eq V v0 v1)) *)
split.
(* Goal: forall (_ : @eq K k' k0) (_ : @eq V v0 v'), @eq K k' k0 *)
(* Goal: forall (_ : not (@eq K k' k0)) (_ : match assoc_find l0 k0 with | @none _ => False | @some _ v' => @eq V v0 v' end), @eq K k' k0 *)
(* Goal: @eq (option V) (assoc_find (@cons Tuple (mkTuple k' v') l0) k0) (assoc_find (assoc_add l0 k' v') k0) *)
transitivity k2; auto.

(* Goal: forall _ : match assoc_find (@cons Tuple (mkTuple k' v') l0) k0 with | @none _ => False | @some _ v' => @eq V v0 v' end, @eq K k' k0 *)
(* Goal: @eq (option V) (assoc_find (@cons Tuple (mkTuple k' v') l0) k0) (assoc_find (assoc_add l0 k' v') k0) *)
generalize H1; simpl in |- *.
(* Goal: forall _ : match (if Keq_dec k1 k0 then some V v1 else assoc_find l k0) with | @none _ => False | @some _ v' => @eq V v0 v' end, @eq V v0 v1 *)
(* Goal: forall (_ : not (@eq K k2 k0)) (_ : @eq K k2 k1) (_ : match assoc_find (@cons Tuple (mkTuple k1 v1) l) k0 with | @none _ => False | @some _ v' => @eq V v0 v' end), or match assoc_find l k0 with | @none _ => False | @some _ v' => @eq V v0 v' end (and (@eq K k0 k1) (@eq V v0 v1)) *)
(* Goal: forall (_ : not (@eq K k2 k1)) (_ : match assoc_find (@cons Tuple (mkTuple k2 v2) (assoc_add l k1 v1)) k0 with | @none _ => False | @some _ v' => @eq V v0 v' end), or match (if Keq_dec k2 k0 then some V v2 else assoc_find l k0) with | @none _ => False | @some _ v' => @eq V v0 v' end (and (@eq K k0 k1) (@eq V v0 v1)) *)
case (Keq_dec k1 k0).
(* Goal: forall (_ : @eq K k' k0) (_ : @eq V v0 v'), @eq K k' k0 *)
(* Goal: forall (_ : not (@eq K k' k0)) (_ : match assoc_find l0 k0 with | @none _ => False | @some _ v' => @eq V v0 v' end), @eq K k' k0 *)
(* Goal: @eq (option V) (assoc_find (@cons Tuple (mkTuple k' v') l0) k0) (assoc_find (assoc_add l0 k' v') k0) *)
auto.

(* Goal: forall (_ : @eq K k' k0) (_ : @eq V v0 v'), @eq K k' k0 *)
(* Goal: forall (_ : not (@eq K k' k0)) (_ : match assoc_find l0 k0 with | @none _ => False | @some _ v' => @eq V v0 v' end), @eq K k' k0 *)
(* Goal: @eq (option V) (assoc_find (@cons Tuple (mkTuple k' v') l0) k0) (assoc_find (assoc_add l0 k' v') k0) *)
intro; absurd (k0 = k1); auto.
(* Goal: forall (_ : @eq K k' k0) (_ : @eq V v0 v'), @eq K k' k0 *)
(* Goal: forall (_ : not (@eq K k' k0)) (_ : match assoc_find l0 k0 with | @none _ => False | @some _ v' => @eq V v0 v' end), @eq K k' k0 *)
(* Goal: @eq (option V) (assoc_find (@cons Tuple (mkTuple k' v') l0) k0) (assoc_find (assoc_add l0 k' v') k0) *)
transitivity k2; auto.

(* Goal: forall _ : match assoc_find (@cons Tuple (mkTuple k' v') l0) k0 with | @none _ => False | @some _ v' => @eq V v0 v' end, @eq K k' k0 *)
(* Goal: @eq (option V) (assoc_find (@cons Tuple (mkTuple k' v') l0) k0) (assoc_find (assoc_add l0 k' v') k0) *)
intros until 2; rewrite <- e; simpl in |- *.
(* Goal: forall _ : match (if Keq_dec k2 k0 then some V v1 else assoc_find l k0) with | @none _ => False | @some _ v' => @eq V v0 v' end, or match assoc_find l k0 with | @none _ => False | @some _ v' => @eq V v0 v' end (and (@eq K k0 k2) (@eq V v0 v1)) *)
(* Goal: forall (_ : not (@eq K k2 k1)) (_ : match assoc_find (@cons Tuple (mkTuple k2 v2) (assoc_add l k1 v1)) k0 with | @none _ => False | @some _ v' => @eq V v0 v' end), or match (if Keq_dec k2 k0 then some V v2 else assoc_find l k0) with | @none _ => False | @some _ v' => @eq V v0 v' end (and (@eq K k0 k1) (@eq V v0 v1)) *)
case (Keq_dec k2 k0).
(* Goal: assoc_almost_eqm k0 (assoc_find l) (assoc_find (@cons Tuple (mkTuple k0 v') l)) *)
(* Goal: assoc_almost_eqm k0 (assoc_find (@cons Tuple (mkTuple k0 v0) l)) (assoc_find l) *)
(* Goal: assoc_almost_eqm k0 (assoc_find l) (assoc_find (@cons Tuple (mkTuple k0 v') l)) *)
  intro; absurd (k2 = k0); assumption.
(* Goal: assoc_almost_eqm k0 (assoc_find l) (assoc_find (@cons Tuple (mkTuple k0 v') l)) *)
(* Goal: assoc_almost_eqm k0 (assoc_find (@cons Tuple (mkTuple k0 v0) l)) (assoc_find l) *)
(* Goal: assoc_almost_eqm k0 (assoc_find l) (assoc_find (@cons Tuple (mkTuple k0 v') l)) *)
  intros; left; assumption.

(* Goal: forall _ : match assoc_find (@cons Tuple (mkTuple k' v') l0) k0 with | @none _ => False | @some _ v' => @eq V v0 v' end, @eq K k' k0 *)
(* Goal: @eq (option V) (assoc_find (@cons Tuple (mkTuple k' v') l0) k0) (assoc_find (assoc_add l0 k' v') k0) *)
simpl in |- *.
(* Goal: forall _ : match assoc_find (@cons Tuple (mkTuple k' v') l0) k0 with | @none _ => False | @some _ v' => @eq V v0 v' end, @eq K k' k0 *)
(* Goal: @eq (option V) (assoc_find (@cons Tuple (mkTuple k' v') l0) k0) (assoc_find (assoc_add l0 k' v') k0) *)
case (Keq_dec k2 k0); simpl in |- *.
(* Goal: forall (_ : @eq K k' k0) (_ : @eq V v0 v'), @eq K k' k0 *)
(* Goal: forall (_ : not (@eq K k' k0)) (_ : match assoc_find l0 k0 with | @none _ => False | @some _ v' => @eq V v0 v' end), @eq K k' k0 *)
(* Goal: @eq (option V) (assoc_find (@cons Tuple (mkTuple k' v') l0) k0) (assoc_find (assoc_add l0 k' v') k0) *)
tauto.

(* Goal: forall (_ : @eq K k' k0) (_ : @eq V v0 v'), @eq K k' k0 *)
(* Goal: forall (_ : not (@eq K k' k0)) (_ : match assoc_find l0 k0 with | @none _ => False | @some _ v' => @eq V v0 v' end), @eq K k' k0 *)
(* Goal: @eq (option V) (assoc_find (@cons Tuple (mkTuple k' v') l0) k0) (assoc_find (assoc_add l0 k' v') k0) *)
intros; unfold assoc_hasmem in H; apply H with (assoc_add l k1 v1); auto.
Qed.




(**************************************************)
(* some invariant properties about add and delete *)
(**************************************************)



(* add/mem ******************************)
Lemma assoc_add_mem_invar :
 forall (l l' : assoc) (k k' : K) (v : V),
 l' = assoc_add l k' v -> k' <> k -> assoc_mem l k -> assoc_mem l' k.

Proof.
(* Goal: forall (l l' : assoc) (k k' : K) (v : V) (_ : @eq assoc l' (assoc_delete l k')) (_ : not (@eq K k' k)) (_ : not (assoc_hasmem l' k v)), not (assoc_hasmem l k v) *)
intros until 2.
(* Goal: forall _ : assoc_hasmem l' k0 v0, assoc_hasmem l k0 v0 *)
cut (assoc_almost_eqm k' (assoc_find l) (assoc_find l')).
(* Goal: forall (_ : assoc_almost_eqm k' (assoc_find l) (assoc_find l')) (_ : assoc_mem l' k0), assoc_mem l k0 *)
(* Goal: assoc_almost_eqm k' (assoc_find l) (assoc_find l') *)
unfold assoc_almost_eqm, assoc_mem in |- *.
(* Goal: forall (_ : forall (k : K) (_ : not (@eq K k k')), @eq (option V) (assoc_find l k) (assoc_find l' k)) (_ : match assoc_find l' k0 with | @none _ => False | @some _ v' => @eq V v0 v' end), match assoc_find l k0 with | @none _ => False | @some _ v' => @eq V v0 v' end *)
(* Goal: assoc_almost_eqm k' (assoc_find l) (assoc_find l') *)
intro.
(* Goal: forall _ : match assoc_find l k0 with | @none _ => False | @some _ v' => @eq V v0 v' end, match assoc_find l' k0 with | @none _ => False | @some _ v' => @eq V v0 v' end *)
(* Goal: assoc_almost_eqm k' (assoc_find l) (assoc_find l') *)
replace (assoc_find l' k0) with (assoc_find l k0).
(* Goal: forall (_ : @eq K k' k0) (_ : @eq V v0 v'), @eq K k' k0 *)
(* Goal: forall (_ : not (@eq K k' k0)) (_ : match assoc_find l0 k0 with | @none _ => False | @some _ v' => @eq V v0 v' end), @eq K k' k0 *)
(* Goal: @eq (option V) (assoc_find (@cons Tuple (mkTuple k' v') l0) k0) (assoc_find (assoc_add l0 k' v') k0) *)
auto.
(* Goal: forall (_ : @eq K k' k0) (_ : @eq V v0 v'), @eq K k' k0 *)
(* Goal: forall (_ : not (@eq K k' k0)) (_ : match assoc_find l0 k0 with | @none _ => False | @some _ v' => @eq V v0 v' end), @eq K k' k0 *)
(* Goal: @eq (option V) (assoc_find (@cons Tuple (mkTuple k' v') l0) k0) (assoc_find (assoc_add l0 k' v') k0) *)
apply H1; auto.
(* Goal: assoc_almost_eqm k' (assoc_find l) (assoc_find l') *)
rewrite H.
(* Goal: assoc_almost_eqm k' (assoc_find l') (assoc_find l) *)
apply assoc_almost_eqm_sym.
(* Goal: assoc_almost_eqm k' (assoc_find (assoc_add l k' v')) (assoc_find l) *)
apply assoc_add_correct_1.
Qed.


Lemma assoc_add_mem_invar_contrap :
 forall (l l' : assoc) (k k' : K) (v : V),
 l' = assoc_add l k' v -> k' <> k -> assoc_mem l' k -> assoc_mem l k.

Proof.
(* Goal: forall (l l' : assoc) (k k' : K) (v : V) (_ : @eq assoc l' (assoc_delete l k')) (_ : not (@eq K k' k)) (_ : not (assoc_hasmem l' k v)), not (assoc_hasmem l k v) *)
intros until 2.
(* Goal: forall _ : assoc_hasmem l' k0 v0, assoc_hasmem l k0 v0 *)
cut (assoc_almost_eqm k' (assoc_find l) (assoc_find l')).
(* Goal: forall (_ : assoc_almost_eqm k' (assoc_find l) (assoc_find l')) (_ : assoc_mem l' k0), assoc_mem l k0 *)
(* Goal: assoc_almost_eqm k' (assoc_find l) (assoc_find l') *)
unfold assoc_almost_eqm, assoc_mem in |- *.
(* Goal: forall (_ : forall (k : K) (_ : not (@eq K k k')), @eq (option V) (assoc_find l k) (assoc_find l' k)) (_ : match assoc_find l' k0 with | @none _ => False | @some _ v' => @eq V v0 v' end), match assoc_find l k0 with | @none _ => False | @some _ v' => @eq V v0 v' end *)
(* Goal: assoc_almost_eqm k' (assoc_find l) (assoc_find l') *)
intro.
(* Goal: forall _ : match assoc_find l k0 with | @none _ => False | @some _ v' => @eq V v0 v' end, match assoc_find l' k0 with | @none _ => False | @some _ v' => @eq V v0 v' end *)
(* Goal: assoc_almost_eqm k' (assoc_find l) (assoc_find l') *)
replace (assoc_find l' k0) with (assoc_find l k0).
(* Goal: forall (_ : @eq K k' k0) (_ : @eq V v0 v'), @eq K k' k0 *)
(* Goal: forall (_ : not (@eq K k' k0)) (_ : match assoc_find l0 k0 with | @none _ => False | @some _ v' => @eq V v0 v' end), @eq K k' k0 *)
(* Goal: @eq (option V) (assoc_find (@cons Tuple (mkTuple k' v') l0) k0) (assoc_find (assoc_add l0 k' v') k0) *)
auto.

(* Goal: forall (_ : @eq K k' k0) (_ : @eq V v0 v'), @eq K k' k0 *)
(* Goal: forall (_ : not (@eq K k' k0)) (_ : match assoc_find l0 k0 with | @none _ => False | @some _ v' => @eq V v0 v' end), @eq K k' k0 *)
(* Goal: @eq (option V) (assoc_find (@cons Tuple (mkTuple k' v') l0) k0) (assoc_find (assoc_add l0 k' v') k0) *)
apply H1; auto.

(* Goal: assoc_almost_eqm k' (assoc_find l) (assoc_find l') *)
rewrite H.
(* Goal: assoc_almost_eqm k' (assoc_find l') (assoc_find l) *)
apply assoc_almost_eqm_sym.
(* Goal: assoc_almost_eqm k' (assoc_find (assoc_add l k' v')) (assoc_find l) *)
apply assoc_add_correct_1.
Qed.


Lemma assoc_add_not_mem_invar :
 forall (l l' : assoc) (k k' : K) (v' : V),
 l' = assoc_add l k' v' -> k' <> k -> ~ assoc_mem l k -> ~ assoc_mem l' k.

Proof.
(* Goal: forall (l l' : assoc) (k k' : K) (v : V) (_ : @eq assoc l' (assoc_delete l k')) (_ : not (@eq K k' k)) (_ : not (assoc_hasmem l' k v)), not (assoc_hasmem l k v) *)
intros until 2.
(* Goal: forall _ : not (assoc_hasmem l' k0 v0), not (assoc_hasmem l k0 v0) *)
cut (assoc_almost_eqm k' (assoc_find l') (assoc_find l)).
(* Goal: forall (_ : assoc_almost_eqm k' (assoc_find l') (assoc_find l)) (_ : not (assoc_mem l' k0)), not (assoc_mem l k0) *)
(* Goal: assoc_almost_eqm k' (assoc_find l') (assoc_find l) *)
unfold assoc_mem, assoc_almost_eqm in |- *.
(* Goal: forall (_ : not (@eq K k' k0)) (_ : @eq (option V) (some V v0) (assoc_find l0 k0)), @eq K k' k0 *)
(* Goal: @eq (option V) (assoc_find (@cons Tuple (mkTuple k' v') l0) k0) (assoc_find (assoc_add l0 k' v') k0) *)
intros. replace (assoc_find l' k0) with (assoc_find l k0); auto.
(* Goal: forall (_ : @eq K k' k0) (_ : @eq V v0 v'), @eq K k' k0 *)
(* Goal: forall (_ : not (@eq K k' k0)) (_ : match assoc_find l0 k0 with | @none _ => False | @some _ v' => @eq V v0 v' end), @eq K k' k0 *)
(* Goal: @eq (option V) (assoc_find (@cons Tuple (mkTuple k' v') l0) k0) (assoc_find (assoc_add l0 k' v') k0) *)
  symmetry  in |- *; apply H1; auto.
(* Goal: assoc_almost_eqm k' (assoc_find l) (assoc_find l') *)
rewrite H. apply assoc_add_correct_1.
Qed.


Lemma assoc_add_not_mem_invar_contrap :
 forall (l l' : assoc) (k k' : K) (v' : V),
 l' = assoc_add l k' v' -> k' <> k -> ~ assoc_mem l' k -> ~ assoc_mem l k.

Proof.
(* Goal: forall (l l' : assoc) (k k' : K) (v : V) (_ : @eq assoc l' (assoc_delete l k')) (_ : not (@eq K k' k)) (_ : not (assoc_hasmem l' k v)), not (assoc_hasmem l k v) *)
intros until 2.
(* Goal: forall _ : not (assoc_hasmem l' k0 v0), not (assoc_hasmem l k0 v0) *)
cut (assoc_almost_eqm k' (assoc_find l') (assoc_find l)).
(* Goal: forall (_ : assoc_almost_eqm k' (assoc_find l') (assoc_find l)) (_ : not (assoc_mem l' k0)), not (assoc_mem l k0) *)
(* Goal: assoc_almost_eqm k' (assoc_find l') (assoc_find l) *)
unfold assoc_mem, assoc_almost_eqm in |- *.
(* Goal: forall (_ : not (@eq K k' k0)) (_ : @eq (option V) (some V v0) (assoc_find l0 k0)), @eq K k' k0 *)
(* Goal: @eq (option V) (assoc_find (@cons Tuple (mkTuple k' v') l0) k0) (assoc_find (assoc_add l0 k' v') k0) *)
intros.
(* Goal: forall (_ : @eq K k' k0) (_ : @eq V v0 v'), @eq K k' k0 *)
(* Goal: forall (_ : not (@eq K k' k0)) (_ : match assoc_find l0 k0 with | @none _ => False | @some _ v' => @eq V v0 v' end), @eq K k' k0 *)
(* Goal: @eq (option V) (assoc_find (@cons Tuple (mkTuple k' v') l0) k0) (assoc_find (assoc_add l0 k' v') k0) *)
replace (assoc_find l k0) with (assoc_find l' k0); auto.

(* Goal: assoc_almost_eqm k' (assoc_find l) (assoc_find l') *)
rewrite H.
(* Goal: assoc_almost_eqm k' (assoc_find (assoc_add l k' v')) (assoc_find l) *)
apply assoc_add_correct_1.
Qed.


(* add/hasmem ******************************)

Lemma assoc_add_hasmem_invar :
 forall (l l' : assoc) (k k' : K) (v v' : V),
 l' = assoc_add l k' v' ->
 k' <> k -> assoc_hasmem l k v -> assoc_hasmem l' k v.

Proof.
(* Goal: forall (l l' : assoc) (k k' : K) (v : V) (_ : @eq assoc l' (assoc_delete l k')) (_ : not (@eq K k' k)) (_ : not (assoc_hasmem l' k v)), not (assoc_hasmem l k v) *)
intros until 2.
(* Goal: forall _ : assoc_hasmem l' k0 v0, assoc_hasmem l k0 v0 *)
cut (assoc_almost_eqm k' (assoc_find l) (assoc_find l')).
(* Goal: forall (_ : assoc_almost_eqm k' (assoc_find l) (assoc_find l')) (_ : assoc_hasmem l' k0 v0), assoc_hasmem l k0 v0 *)
(* Goal: assoc_almost_eqm k' (assoc_find l) (assoc_find l') *)
  unfold assoc_almost_eqm, assoc_hasmem in |- *.
(* Goal: forall (_ : forall (k : K) (_ : not (@eq K k k')), @eq (option V) (assoc_find l k) (assoc_find l' k)) (_ : match assoc_find l' k0 with | @none _ => False | @some _ v' => @eq V v0 v' end), match assoc_find l k0 with | @none _ => False | @some _ v' => @eq V v0 v' end *)
(* Goal: assoc_almost_eqm k' (assoc_find l) (assoc_find l') *)
  intro. replace (assoc_find l' k0) with (assoc_find l k0).
(* Goal: forall (_ : @eq K k' k0) (_ : @eq V v0 v'), @eq K k' k0 *)
(* Goal: forall (_ : not (@eq K k' k0)) (_ : match assoc_find l0 k0 with | @none _ => False | @some _ v' => @eq V v0 v' end), @eq K k' k0 *)
(* Goal: @eq (option V) (assoc_find (@cons Tuple (mkTuple k' v') l0) k0) (assoc_find (assoc_add l0 k' v') k0) *)
     auto.
(* Goal: forall (_ : @eq K k' k0) (_ : @eq V v0 v'), @eq K k' k0 *)
(* Goal: forall (_ : not (@eq K k' k0)) (_ : match assoc_find l0 k0 with | @none _ => False | @some _ v' => @eq V v0 v' end), @eq K k' k0 *)
(* Goal: @eq (option V) (assoc_find (@cons Tuple (mkTuple k' v') l0) k0) (assoc_find (assoc_add l0 k' v') k0) *)
     apply H1; auto.
(* Goal: assoc_almost_eqm k' (assoc_find l) (assoc_find l') *)
  rewrite H.
(* Goal: assoc_almost_eqm k' (assoc_find l') (assoc_find l) *)
  apply assoc_almost_eqm_sym.
(* Goal: assoc_almost_eqm k' (assoc_find (assoc_add l k' v')) (assoc_find l) *)
  apply assoc_add_correct_1.

Qed.


Lemma assoc_add_hasmem_invar_contrap :
 forall (l l' : assoc) (k k' : K) (v v' : V),
 l' = assoc_add l k' v' ->
 k' <> k -> assoc_hasmem l' k v -> assoc_hasmem l k v.

Proof.
(* Goal: forall (l l' : assoc) (k k' : K) (v : V) (_ : @eq assoc l' (assoc_delete l k')) (_ : not (@eq K k' k)) (_ : not (assoc_hasmem l' k v)), not (assoc_hasmem l k v) *)
intros until 2.
(* Goal: forall _ : assoc_hasmem l' k0 v0, assoc_hasmem l k0 v0 *)
cut (assoc_almost_eqm k' (assoc_find l) (assoc_find l')).
(* Goal: forall (_ : assoc_almost_eqm k' (assoc_find l) (assoc_find l')) (_ : assoc_hasmem l' k0 v0), assoc_hasmem l k0 v0 *)
(* Goal: assoc_almost_eqm k' (assoc_find l) (assoc_find l') *)
unfold assoc_almost_eqm, assoc_hasmem in |- *.
(* Goal: forall (_ : forall (k : K) (_ : not (@eq K k k')), @eq (option V) (assoc_find l k) (assoc_find l' k)) (_ : match assoc_find l' k0 with | @none _ => False | @some _ v' => @eq V v0 v' end), match assoc_find l k0 with | @none _ => False | @some _ v' => @eq V v0 v' end *)
(* Goal: assoc_almost_eqm k' (assoc_find l) (assoc_find l') *)
intro.
(* Goal: forall _ : match assoc_find l k0 with | @none _ => False | @some _ v' => @eq V v0 v' end, match assoc_find l' k0 with | @none _ => False | @some _ v' => @eq V v0 v' end *)
(* Goal: assoc_almost_eqm k' (assoc_find l) (assoc_find l') *)
replace (assoc_find l' k0) with (assoc_find l k0).
(* Goal: forall (_ : @eq K k' k0) (_ : @eq V v0 v'), @eq K k' k0 *)
(* Goal: forall (_ : not (@eq K k' k0)) (_ : match assoc_find l0 k0 with | @none _ => False | @some _ v' => @eq V v0 v' end), @eq K k' k0 *)
(* Goal: @eq (option V) (assoc_find (@cons Tuple (mkTuple k' v') l0) k0) (assoc_find (assoc_add l0 k' v') k0) *)
auto.

(* Goal: forall (_ : @eq K k' k0) (_ : @eq V v0 v'), @eq K k' k0 *)
(* Goal: forall (_ : not (@eq K k' k0)) (_ : match assoc_find l0 k0 with | @none _ => False | @some _ v' => @eq V v0 v' end), @eq K k' k0 *)
(* Goal: @eq (option V) (assoc_find (@cons Tuple (mkTuple k' v') l0) k0) (assoc_find (assoc_add l0 k' v') k0) *)
apply H1; auto.

(* Goal: assoc_almost_eqm k' (assoc_find l) (assoc_find l') *)
rewrite H.
(* Goal: assoc_almost_eqm k' (assoc_find l') (assoc_find l) *)
apply assoc_almost_eqm_sym.
(* Goal: assoc_almost_eqm k' (assoc_find (assoc_add l k' v')) (assoc_find l) *)
apply assoc_add_correct_1.
Qed.


Lemma assoc_add_not_hasmem_invar :
 forall (l l' : assoc) (k k' : K) (v v' : V),
 l' = assoc_add l k' v' ->
 k' <> k -> ~ assoc_hasmem l k v -> ~ assoc_hasmem l' k v.

Proof.
(* Goal: forall (l l' : assoc) (k k' : K) (v : V) (_ : @eq assoc l' (assoc_delete l k')) (_ : not (@eq K k' k)) (_ : not (assoc_hasmem l' k v)), not (assoc_hasmem l k v) *)
intros until 2.
(* Goal: forall _ : not (assoc_hasmem l' k0 v0), not (assoc_hasmem l k0 v0) *)
cut (assoc_almost_eqm k' (assoc_find l') (assoc_find l)).
(* Goal: forall (_ : not (@eq K k' k0)) (_ : @eq (option V) (some V v0) (assoc_find l0 k0)), @eq K k' k0 *)
(* Goal: @eq (option V) (assoc_find (@cons Tuple (mkTuple k' v') l0) k0) (assoc_find (assoc_add l0 k' v') k0) *)
unfold assoc_hasmem, assoc_almost_eqm in |- *; intros.
(* Goal: forall _ : match assoc_find l k0 with | @none _ => False | @some _ v' => @eq V v0 v' end, match assoc_find l' k0 with | @none _ => False | @some _ v' => @eq V v0 v' end *)
(* Goal: assoc_almost_eqm k' (assoc_find l) (assoc_find l') *)
replace (assoc_find l' k0) with (assoc_find l k0).
(* Goal: forall (_ : @eq K k' k0) (_ : @eq V v0 v'), @eq K k' k0 *)
(* Goal: forall (_ : not (@eq K k' k0)) (_ : match assoc_find l0 k0 with | @none _ => False | @some _ v' => @eq V v0 v' end), @eq K k' k0 *)
(* Goal: @eq (option V) (assoc_find (@cons Tuple (mkTuple k' v') l0) k0) (assoc_find (assoc_add l0 k' v') k0) *)
auto.

(* Goal: forall (_ : @eq K k' k0) (_ : @eq V v0 v'), @eq K k' k0 *)
(* Goal: forall (_ : not (@eq K k' k0)) (_ : match assoc_find l0 k0 with | @none _ => False | @some _ v' => @eq V v0 v' end), @eq K k' k0 *)
(* Goal: @eq (option V) (assoc_find (@cons Tuple (mkTuple k' v') l0) k0) (assoc_find (assoc_add l0 k' v') k0) *)
symmetry  in |- *; apply H1; auto.

(* Goal: assoc_almost_eqm k' (assoc_find l) (assoc_find l') *)
rewrite H.
(* Goal: assoc_almost_eqm k' (assoc_find (assoc_add l k' v')) (assoc_find l) *)
apply assoc_add_correct_1.
Qed.


Lemma assoc_add_not_hasmem_invar_contrap :
 forall (l l' : assoc) (k k' : K) (v v' : V),
 l' = assoc_add l k' v' ->
 k' <> k -> ~ assoc_hasmem l' k v -> ~ assoc_hasmem l k v.

Proof.
(* Goal: forall (l l' : assoc) (k k' : K) (v : V) (_ : @eq assoc l' (assoc_delete l k')) (_ : not (@eq K k' k)) (_ : not (assoc_hasmem l' k v)), not (assoc_hasmem l k v) *)
intros until 2.
(* Goal: forall _ : not (assoc_hasmem l' k0 v0), not (assoc_hasmem l k0 v0) *)
cut (assoc_almost_eqm k' (assoc_find l') (assoc_find l)).
(* Goal: forall (_ : not (@eq K k' k0)) (_ : @eq (option V) (some V v0) (assoc_find l0 k0)), @eq K k' k0 *)
(* Goal: @eq (option V) (assoc_find (@cons Tuple (mkTuple k' v') l0) k0) (assoc_find (assoc_add l0 k' v') k0) *)
unfold assoc_hasmem, assoc_almost_eqm in |- *; intros.
(* Goal: not match assoc_find l k0 with | @none _ => False | @some _ v => True end *)
(* Goal: assoc_almost_eqm k' (assoc_find l') (assoc_find l) *)
replace (assoc_find l k0) with (assoc_find l' k0).
(* Goal: forall (_ : @eq K k' k0) (_ : @eq V v0 v'), @eq K k' k0 *)
(* Goal: forall (_ : not (@eq K k' k0)) (_ : match assoc_find l0 k0 with | @none _ => False | @some _ v' => @eq V v0 v' end), @eq K k' k0 *)
(* Goal: @eq (option V) (assoc_find (@cons Tuple (mkTuple k' v') l0) k0) (assoc_find (assoc_add l0 k' v') k0) *)
auto.

(* Goal: forall (_ : @eq K k' k0) (_ : @eq V v0 v'), @eq K k' k0 *)
(* Goal: forall (_ : not (@eq K k' k0)) (_ : match assoc_find l0 k0 with | @none _ => False | @some _ v' => @eq V v0 v' end), @eq K k' k0 *)
(* Goal: @eq (option V) (assoc_find (@cons Tuple (mkTuple k' v') l0) k0) (assoc_find (assoc_add l0 k' v') k0) *)
apply H1; auto.

(* Goal: assoc_almost_eqm k' (assoc_find l) (assoc_find l') *)
rewrite H.
(* Goal: assoc_almost_eqm k' (assoc_find (assoc_add l k' v')) (assoc_find l) *)
apply assoc_add_correct_1.
Qed.


(* del/mem ******************************)

Lemma assoc_del_mem_invar :
 forall (l l' : assoc) (k k' : K),
 l' = assoc_delete l k' -> k' <> k -> assoc_mem l k -> assoc_mem l' k.

Proof.
(* Goal: forall (_ : not (@eq K k' k0)) (_ : @eq (option V) (some V v0) (assoc_find l0 k0)), @eq K k' k0 *)
(* Goal: @eq (option V) (assoc_find (@cons Tuple (mkTuple k' v') l0) k0) (assoc_find (assoc_add l0 k' v') k0) *)
intros until 2. rewrite H. unfold assoc_mem in |- *. intros.
(* Goal: forall (_ : @eq K k' k0) (_ : @eq V v0 v'), @eq K k' k0 *)
(* Goal: forall (_ : not (@eq K k' k0)) (_ : match assoc_find l0 k0 with | @none _ => False | @some _ v' => @eq V v0 v' end), @eq K k' k0 *)
(* Goal: @eq (option V) (assoc_find (@cons Tuple (mkTuple k' v') l0) k0) (assoc_find (assoc_add l0 k' v') k0) *)
replace (assoc_find (assoc_delete l k') k0) with (assoc_find l k0); auto.
(* Goal: @eq (option V) (assoc_find l k0) (assoc_find (assoc_delete l k') k0) *)
cut (assoc_almost_eqm k' (assoc_find l) (assoc_find (assoc_delete l k'))).
(* Goal: forall (_ : @eq K k' k0) (_ : @eq V v0 v'), @eq K k' k0 *)
(* Goal: forall (_ : not (@eq K k' k0)) (_ : match assoc_find l0 k0 with | @none _ => False | @some _ v' => @eq V v0 v' end), @eq K k' k0 *)
(* Goal: @eq (option V) (assoc_find (@cons Tuple (mkTuple k' v') l0) k0) (assoc_find (assoc_add l0 k' v') k0) *)
  unfold assoc_almost_eqm in |- *; intros; apply H2; auto.
(* Goal: assoc_almost_eqm k1 (assoc_find l) (assoc_find (assoc_delete l k1)) *)
  apply assoc_semfind_del.
Qed.



Lemma assoc_del_mem_invar_contrap :
 forall (l l' : assoc) (k k' : K),
 l' = assoc_delete l k' -> k' <> k -> assoc_mem l' k -> assoc_mem l k.

Proof.
(* Goal: forall (_ : not (@eq K k' k0)) (_ : @eq (option V) (some V v0) (assoc_find l0 k0)), @eq K k' k0 *)
(* Goal: @eq (option V) (assoc_find (@cons Tuple (mkTuple k' v') l0) k0) (assoc_find (assoc_add l0 k' v') k0) *)
intros until 2. rewrite H. unfold assoc_mem in |- *. intros.
(* Goal: forall (_ : @eq K k' k0) (_ : @eq V v0 v'), @eq K k' k0 *)
(* Goal: forall (_ : not (@eq K k' k0)) (_ : match assoc_find l0 k0 with | @none _ => False | @some _ v' => @eq V v0 v' end), @eq K k' k0 *)
(* Goal: @eq (option V) (assoc_find (@cons Tuple (mkTuple k' v') l0) k0) (assoc_find (assoc_add l0 k' v') k0) *)
replace (assoc_find l k0) with (assoc_find (assoc_delete l k') k0); auto.
symmetry  in |- *.
(* Goal: @eq (option V) (assoc_find l k0) (assoc_find (assoc_delete l k') k0) *)
cut (assoc_almost_eqm k' (assoc_find l) (assoc_find (assoc_delete l k'))).
(* Goal: forall (_ : @eq K k' k0) (_ : @eq V v0 v'), @eq K k' k0 *)
(* Goal: forall (_ : not (@eq K k' k0)) (_ : match assoc_find l0 k0 with | @none _ => False | @some _ v' => @eq V v0 v' end), @eq K k' k0 *)
(* Goal: @eq (option V) (assoc_find (@cons Tuple (mkTuple k' v') l0) k0) (assoc_find (assoc_add l0 k' v') k0) *)
  unfold assoc_almost_eqm in |- *; intros; apply H2; auto.
(* Goal: assoc_almost_eqm k1 (assoc_find l) (assoc_find (assoc_delete l k1)) *)
  apply assoc_semfind_del.
Qed.


Lemma assoc_del_not_mem_invar :
 forall (l l' : assoc) (k k' : K),
 l' = assoc_delete l k' -> k' <> k -> ~ assoc_mem l k -> ~ assoc_mem l' k.

Proof.
(* Goal: forall (l l' : assoc) (k k' : K) (v : V) (_ : @eq assoc l' (assoc_delete l k')) (_ : not (@eq K k' k)) (_ : not (assoc_hasmem l' k v)), not (assoc_hasmem l k v) *)
intros until 2.
(* Goal: forall _ : not (assoc_hasmem l' k0 v0), not (assoc_hasmem l k0 v0) *)
cut (assoc_almost_eqm k' (assoc_find l') (assoc_find l)).
(* Goal: forall (_ : not (@eq K k' k0)) (_ : @eq (option V) (some V v0) (assoc_find l0 k0)), @eq K k' k0 *)
(* Goal: @eq (option V) (assoc_find (@cons Tuple (mkTuple k' v') l0) k0) (assoc_find (assoc_add l0 k' v') k0) *)
unfold assoc_mem, assoc_almost_eqm in |- *; intros.
(* Goal: forall _ : match assoc_find l k0 with | @none _ => False | @some _ v' => @eq V v0 v' end, match assoc_find l' k0 with | @none _ => False | @some _ v' => @eq V v0 v' end *)
(* Goal: assoc_almost_eqm k' (assoc_find l) (assoc_find l') *)
replace (assoc_find l' k0) with (assoc_find l k0).
(* Goal: forall (_ : @eq K k' k0) (_ : @eq V v0 v'), @eq K k' k0 *)
(* Goal: forall (_ : not (@eq K k' k0)) (_ : match assoc_find l0 k0 with | @none _ => False | @some _ v' => @eq V v0 v' end), @eq K k' k0 *)
(* Goal: @eq (option V) (assoc_find (@cons Tuple (mkTuple k' v') l0) k0) (assoc_find (assoc_add l0 k' v') k0) *)
auto.
(* Goal: forall (_ : @eq K k' k0) (_ : @eq V v0 v'), @eq K k' k0 *)
(* Goal: forall (_ : not (@eq K k' k0)) (_ : match assoc_find l0 k0 with | @none _ => False | @some _ v' => @eq V v0 v' end), @eq K k' k0 *)
(* Goal: @eq (option V) (assoc_find (@cons Tuple (mkTuple k' v') l0) k0) (assoc_find (assoc_add l0 k' v') k0) *)
symmetry  in |- *; apply H1; auto.
(* Goal: assoc_almost_eqm k' (assoc_find l') (assoc_find l) *)
apply assoc_almost_eqm_sym.
(* Goal: assoc_almost_eqm k1 (assoc_find l) (assoc_find (assoc_delete l k1)) *)
rewrite H; apply assoc_semfind_del.
Qed.


Lemma assoc_del_not_mem_invar_contrap :
 forall (l l' : assoc) (k k' : K),
 l' = assoc_delete l k' -> k' <> k -> ~ assoc_mem l' k -> ~ assoc_mem l k.

Proof.
(* Goal: forall (l l' : assoc) (k k' : K) (v : V) (_ : @eq assoc l' (assoc_delete l k')) (_ : not (@eq K k' k)) (_ : not (assoc_hasmem l' k v)), not (assoc_hasmem l k v) *)
intros until 2.
(* Goal: forall _ : not (assoc_hasmem l' k0 v0), not (assoc_hasmem l k0 v0) *)
cut (assoc_almost_eqm k' (assoc_find l') (assoc_find l)).
(* Goal: forall (_ : not (@eq K k' k0)) (_ : @eq (option V) (some V v0) (assoc_find l0 k0)), @eq K k' k0 *)
(* Goal: @eq (option V) (assoc_find (@cons Tuple (mkTuple k' v') l0) k0) (assoc_find (assoc_add l0 k' v') k0) *)
unfold assoc_mem, assoc_almost_eqm in |- *; intros.
(* Goal: not match assoc_find l k0 with | @none _ => False | @some _ v => True end *)
(* Goal: assoc_almost_eqm k' (assoc_find l') (assoc_find l) *)
replace (assoc_find l k0) with (assoc_find l' k0).
(* Goal: forall (_ : @eq K k' k0) (_ : @eq V v0 v'), @eq K k' k0 *)
(* Goal: forall (_ : not (@eq K k' k0)) (_ : match assoc_find l0 k0 with | @none _ => False | @some _ v' => @eq V v0 v' end), @eq K k' k0 *)
(* Goal: @eq (option V) (assoc_find (@cons Tuple (mkTuple k' v') l0) k0) (assoc_find (assoc_add l0 k' v') k0) *)
auto.
(* Goal: forall (_ : @eq K k' k0) (_ : @eq V v0 v'), @eq K k' k0 *)
(* Goal: forall (_ : not (@eq K k' k0)) (_ : match assoc_find l0 k0 with | @none _ => False | @some _ v' => @eq V v0 v' end), @eq K k' k0 *)
(* Goal: @eq (option V) (assoc_find (@cons Tuple (mkTuple k' v') l0) k0) (assoc_find (assoc_add l0 k' v') k0) *)
apply H1; auto.
(* Goal: assoc_almost_eqm k' (assoc_find l') (assoc_find l) *)
apply assoc_almost_eqm_sym.
(* Goal: assoc_almost_eqm k1 (assoc_find l) (assoc_find (assoc_delete l k1)) *)
rewrite H; apply assoc_semfind_del.
Qed.



(* del/hasmem ******************************)

Lemma assoc_del_hasmem_invar :
 forall (l l' : assoc) (k k' : K) (v : V),
 l' = assoc_delete l k' ->
 k' <> k -> assoc_hasmem l k v -> assoc_hasmem l' k v.

Proof.
(* Goal: forall (l l' : assoc) (k k' : K) (v : V) (_ : @eq assoc l' (assoc_delete l k')) (_ : not (@eq K k' k)) (_ : not (assoc_hasmem l' k v)), not (assoc_hasmem l k v) *)
intros until 2.
(* Goal: forall _ : assoc_hasmem l' k0 v0, assoc_hasmem l k0 v0 *)
cut (assoc_almost_eqm k' (assoc_find l) (assoc_find l')).
(* Goal: forall (_ : assoc_almost_eqm k' (assoc_find l) (assoc_find l')) (_ : assoc_hasmem l' k0 v0), assoc_hasmem l k0 v0 *)
(* Goal: assoc_almost_eqm k' (assoc_find l) (assoc_find l') *)
  unfold assoc_almost_eqm, assoc_hasmem in |- *.
(* Goal: forall (_ : forall (k : K) (_ : not (@eq K k k')), @eq (option V) (assoc_find l k) (assoc_find l' k)) (_ : match assoc_find l' k0 with | @none _ => False | @some _ v' => @eq V v0 v' end), match assoc_find l k0 with | @none _ => False | @some _ v' => @eq V v0 v' end *)
(* Goal: assoc_almost_eqm k' (assoc_find l) (assoc_find l') *)
  intro. replace (assoc_find l' k0) with (assoc_find l k0).
(* Goal: forall (_ : @eq K k' k0) (_ : @eq V v0 v'), @eq K k' k0 *)
(* Goal: forall (_ : not (@eq K k' k0)) (_ : match assoc_find l0 k0 with | @none _ => False | @some _ v' => @eq V v0 v' end), @eq K k' k0 *)
(* Goal: @eq (option V) (assoc_find (@cons Tuple (mkTuple k' v') l0) k0) (assoc_find (assoc_add l0 k' v') k0) *)
     auto.
(* Goal: forall (_ : @eq K k' k0) (_ : @eq V v0 v'), @eq K k' k0 *)
(* Goal: forall (_ : not (@eq K k' k0)) (_ : match assoc_find l0 k0 with | @none _ => False | @some _ v' => @eq V v0 v' end), @eq K k' k0 *)
(* Goal: @eq (option V) (assoc_find (@cons Tuple (mkTuple k' v') l0) k0) (assoc_find (assoc_add l0 k' v') k0) *)
     apply H1; auto.
(* Goal: assoc_almost_eqm k' (assoc_find l) (assoc_find l') *)
  rewrite H.
(* Goal: assoc_almost_eqm k1 (assoc_find l) (assoc_find (assoc_delete l k1)) *)
  apply assoc_semfind_del.
Qed.


Lemma assoc_del_hasmem_invar_contrap :
 forall (l l' : assoc) (k k' : K) (v : V),
 l' = assoc_delete l k' ->
 k' <> k -> assoc_hasmem l' k v -> assoc_hasmem l k v.

Proof.
(* Goal: forall (l l' : assoc) (k k' : K) (v : V) (_ : @eq assoc l' (assoc_delete l k')) (_ : not (@eq K k' k)) (_ : not (assoc_hasmem l' k v)), not (assoc_hasmem l k v) *)
intros until 2.
(* Goal: forall _ : assoc_hasmem l' k0 v0, assoc_hasmem l k0 v0 *)
cut (assoc_almost_eqm k' (assoc_find l) (assoc_find l')).
(* Goal: forall (_ : assoc_almost_eqm k' (assoc_find l) (assoc_find l')) (_ : assoc_hasmem l' k0 v0), assoc_hasmem l k0 v0 *)
(* Goal: assoc_almost_eqm k' (assoc_find l) (assoc_find l') *)
unfold assoc_almost_eqm, assoc_hasmem in |- *.
(* Goal: forall (_ : forall (k : K) (_ : not (@eq K k k')), @eq (option V) (assoc_find l k) (assoc_find l' k)) (_ : match assoc_find l' k0 with | @none _ => False | @some _ v' => @eq V v0 v' end), match assoc_find l k0 with | @none _ => False | @some _ v' => @eq V v0 v' end *)
(* Goal: assoc_almost_eqm k' (assoc_find l) (assoc_find l') *)
intro.
(* Goal: forall (_ : @eq K k' k0) (_ : @eq V v0 v'), @eq K k' k0 *)
(* Goal: forall (_ : not (@eq K k' k0)) (_ : match assoc_find l0 k0 with | @none _ => False | @some _ v' => @eq V v0 v' end), @eq K k' k0 *)
(* Goal: @eq (option V) (assoc_find (@cons Tuple (mkTuple k' v') l0) k0) (assoc_find (assoc_add l0 k' v') k0) *)
replace (assoc_find l' k0) with (assoc_find l k0); auto.

(* Goal: assoc_almost_eqm k1 (assoc_find l) (assoc_find (assoc_delete l k1)) *)
rewrite H; apply assoc_semfind_del.
Qed.


Lemma assoc_del_not_hasmem_invar :
 forall (l l' : assoc) (k k' : K) (v : V),
 l' = assoc_delete l k' ->
 k' <> k -> ~ assoc_hasmem l k v -> ~ assoc_hasmem l' k v.

Proof.
(* Goal: forall (l l' : assoc) (k k' : K) (v : V) (_ : @eq assoc l' (assoc_delete l k')) (_ : not (@eq K k' k)) (_ : not (assoc_hasmem l' k v)), not (assoc_hasmem l k v) *)
intros until 2.
(* Goal: forall _ : not (assoc_hasmem l' k0 v0), not (assoc_hasmem l k0 v0) *)
cut (assoc_almost_eqm k' (assoc_find l') (assoc_find l)).
(* Goal: forall (_ : not (@eq K k' k0)) (_ : @eq (option V) (some V v0) (assoc_find l0 k0)), @eq K k' k0 *)
(* Goal: @eq (option V) (assoc_find (@cons Tuple (mkTuple k' v') l0) k0) (assoc_find (assoc_add l0 k' v') k0) *)
unfold assoc_hasmem, assoc_almost_eqm in |- *; intros.
(* Goal: forall (_ : @eq K k' k0) (_ : @eq V v0 v'), @eq K k' k0 *)
(* Goal: forall (_ : not (@eq K k' k0)) (_ : match assoc_find l0 k0 with | @none _ => False | @some _ v' => @eq V v0 v' end), @eq K k' k0 *)
(* Goal: @eq (option V) (assoc_find (@cons Tuple (mkTuple k' v') l0) k0) (assoc_find (assoc_add l0 k' v') k0) *)
replace (assoc_find l' k0) with (assoc_find l k0); auto.
(* Goal: forall (_ : @eq K k' k0) (_ : @eq V v0 v'), @eq K k' k0 *)
(* Goal: forall (_ : not (@eq K k' k0)) (_ : match assoc_find l0 k0 with | @none _ => False | @some _ v' => @eq V v0 v' end), @eq K k' k0 *)
(* Goal: @eq (option V) (assoc_find (@cons Tuple (mkTuple k' v') l0) k0) (assoc_find (assoc_add l0 k' v') k0) *)
symmetry  in |- *; apply H1; auto.

(* Goal: assoc_almost_eqm k' (assoc_find l') (assoc_find l) *)
apply assoc_almost_eqm_sym.
(* Goal: assoc_almost_eqm k1 (assoc_find l) (assoc_find (assoc_delete l k1)) *)
rewrite H; apply assoc_semfind_del.
Qed.


Lemma assoc_del_not_hasmem_invar_contrap :
 forall (l l' : assoc) (k k' : K) (v : V),
 l' = assoc_delete l k' ->
 k' <> k -> ~ assoc_hasmem l' k v -> ~ assoc_hasmem l k v.

Proof.
(* Goal: forall (l l' : assoc) (k k' : K) (v : V) (_ : @eq assoc l' (assoc_delete l k')) (_ : not (@eq K k' k)) (_ : not (assoc_hasmem l' k v)), not (assoc_hasmem l k v) *)
intros until 2.
(* Goal: forall _ : not (assoc_hasmem l' k0 v0), not (assoc_hasmem l k0 v0) *)
cut (assoc_almost_eqm k' (assoc_find l') (assoc_find l)).
(* Goal: forall (_ : not (@eq K k' k0)) (_ : @eq (option V) (some V v0) (assoc_find l0 k0)), @eq K k' k0 *)
(* Goal: @eq (option V) (assoc_find (@cons Tuple (mkTuple k' v') l0) k0) (assoc_find (assoc_add l0 k' v') k0) *)
unfold assoc_hasmem, assoc_almost_eqm in |- *; intros.
(* Goal: forall (_ : @eq K k' k0) (_ : @eq V v0 v'), @eq K k' k0 *)
(* Goal: forall (_ : not (@eq K k' k0)) (_ : match assoc_find l0 k0 with | @none _ => False | @some _ v' => @eq V v0 v' end), @eq K k' k0 *)
(* Goal: @eq (option V) (assoc_find (@cons Tuple (mkTuple k' v') l0) k0) (assoc_find (assoc_add l0 k' v') k0) *)
replace (assoc_find l k0) with (assoc_find l' k0); auto.

(* Goal: assoc_almost_eqm k' (assoc_find l') (assoc_find l) *)
apply assoc_almost_eqm_sym.
(* Goal: assoc_almost_eqm k1 (assoc_find l) (assoc_find (assoc_delete l k1)) *)
rewrite H; apply assoc_semfind_del.
Qed.




(**************************************************)
(* miscellanous                                   *)
(**************************************************)



Lemma assoc_unique_key :
 forall (l : assoc) (k : K) (v v' : V),
 assoc_hasmem l k v -> assoc_hasmem l k v' -> v' = v.

Proof.
(* Goal: forall (l : assoc) (k : K) (v v' : V) (_ : assoc_hasmem l k v) (_ : assoc_hasmem l k v'), @eq V v' v *)
unfold assoc_hasmem in |- *.
(* Goal: forall (l : assoc) (k : K) (v v' : V) (_ : match assoc_find l k with | @none _ => False | @some _ v'0 => @eq V v v'0 end) (_ : match assoc_find l k with | @none _ => False | @some _ v'0 => @eq V v' v'0 end), @eq V v' v *)
intros l k0 v0 v1.
(* Goal: forall (_ : not (@eq K k' k0)) (_ : @eq (option V) (some V v0) (assoc_find l0 k0)), @eq K k' k0 *)
(* Goal: @eq (option V) (assoc_find (@cons Tuple (mkTuple k' v') l0) k0) (assoc_find (assoc_add l0 k' v') k0) *)
case (assoc_find l k0); intros.
(* Goal: @eq V v1 v0 *)
(* Goal: @eq V v1 v0 *)
  contradiction.
(* Goal: forall (_ : @eq K k' k0) (_ : @eq V v0 v'), @eq K k' k0 *)
(* Goal: forall (_ : not (@eq K k' k0)) (_ : match assoc_find l0 k0 with | @none _ => False | @some _ v' => @eq V v0 v' end), @eq K k' k0 *)
(* Goal: @eq (option V) (assoc_find (@cons Tuple (mkTuple k' v') l0) k0) (assoc_find (assoc_add l0 k' v') k0) *)
  transitivity v2; auto.
Qed.


Lemma assoc_add_find_effect :
 forall (l0 l1 : assoc) (k k' : K) (v v' : V),
 none V = assoc_find l0 k ->
 some V v = assoc_find l1 k -> l1 = assoc_add l0 k' v' -> k' = k /\ v' = v.

Proof.
(* Goal: forall (_ : not (@eq K k' k0)) (_ : @eq (option V) (some V v0) (assoc_find l0 k0)), @eq K k' k0 *)
(* Goal: @eq (option V) (assoc_find (@cons Tuple (mkTuple k' v') l0) k0) (assoc_find (assoc_add l0 k' v') k0) *)
intros.
(* Goal: @eq K k' k0 *)
rewrite H1 in H0.
(* Goal: and (@eq K k' k0) (@eq V v' v0) *)
 cut (k' = k0).
(* Goal: forall (_ : @eq K k' k0) (_ : @eq V v0 v'), @eq K k' k0 *)
(* Goal: forall (_ : not (@eq K k' k0)) (_ : match assoc_find l0 k0 with | @none _ => False | @some _ v' => @eq V v0 v' end), @eq K k' k0 *)
(* Goal: @eq (option V) (assoc_find (@cons Tuple (mkTuple k' v') l0) k0) (assoc_find (assoc_add l0 k' v') k0) *)
 split; auto.
(* Goal: @eq V v' v0 *)
(* Goal: @eq K k' k0 *)
 cut (some V v0 = some V v').
(* Goal: forall (_ : not (@eq K k' k0)) (_ : @eq (option V) (some V v0) (assoc_find l0 k0)), @eq K k' k0 *)
(* Goal: @eq (option V) (assoc_find (@cons Tuple (mkTuple k' v') l0) k0) (assoc_find (assoc_add l0 k' v') k0) *)
 intros. injection H3. auto.
(* Goal: @eq (option V) (some V v0) (some V v') *)
(* Goal: @eq K k' k0 *)
 rewrite H0. rewrite H2. apply assoc_add_correct_2.

(* Goal: @eq K k' k0 *)
generalize H0.
replace (assoc_find (assoc_add l0 k' v') k0) with
 (assoc_find (mkTuple k' v' :: l0) k0).
(* Goal: forall _ : match assoc_find (@cons Tuple (mkTuple k' v') l0) k0 with | @none _ => False | @some _ v' => @eq V v0 v' end, @eq K k' k0 *)
(* Goal: @eq (option V) (assoc_find (@cons Tuple (mkTuple k' v') l0) k0) (assoc_find (assoc_add l0 k' v') k0) *)
simpl in |- *. case (Keq_dec k' k0).
(* Goal: forall (_ : @eq K k' k0) (_ : @eq V v0 v'), @eq K k' k0 *)
(* Goal: forall (_ : not (@eq K k' k0)) (_ : match assoc_find l0 k0 with | @none _ => False | @some _ v' => @eq V v0 v' end), @eq K k' k0 *)
(* Goal: @eq (option V) (assoc_find (@cons Tuple (mkTuple k' v') l0) k0) (assoc_find (assoc_add l0 k' v') k0) *)
  auto.
(* Goal: forall (_ : not (@eq K k' k0)) (_ : @eq (option V) (some V v0) (assoc_find l0 k0)), @eq K k' k0 *)
(* Goal: @eq (option V) (assoc_find (@cons Tuple (mkTuple k' v') l0) k0) (assoc_find (assoc_add l0 k' v') k0) *)
  intros. absurd (none V = some V v0).
(* Goal: not (@eq (option V) (none V) (some V v0)) *)
(* Goal: @eq (option V) (none V) (some V v0) *)
(* Goal: @eq (option V) (assoc_find (@cons Tuple (mkTuple k' v') l0) k0) (assoc_find (assoc_add l0 k' v') k0) *)
    unfold not in |- *; intro DISCR; discriminate DISCR.
(* Goal: forall (k : K) (v : V) (k0 : K), @eq (option V) (assoc_find (@cons Tuple (mkTuple k v) (@nil Tuple)) k0) (assoc_find (@cons Tuple (mkTuple k v) (@nil Tuple)) k0) *)
(* Goal: forall (k : K) (v : V), assoc_eqm (assoc_find (@cons Tuple (mkTuple k v) (@cons Tuple a t))) (assoc_find (assoc_add (@cons Tuple a t) k v)) *)
    rewrite H2; rewrite H; trivial.

cut
 (assoc_eqm (assoc_find (mkTuple k' v' :: l0))
    (assoc_find (assoc_add l0 k' v'))).
(* Goal: forall _ : assoc_eqm (assoc_find (@cons Tuple (mkTuple k' v') l0)) (assoc_find (assoc_add l0 k' v')), @eq (option V) (assoc_find (@cons Tuple (mkTuple k' v') l0) k0) (assoc_find (assoc_add l0 k' v') k0) *)
(* Goal: assoc_eqm (assoc_find (@cons Tuple (mkTuple k' v') l0)) (assoc_find (assoc_add l0 k' v')) *)
unfold assoc_eqm in |- *.
(* Goal: forall (_ : @eq K k' k0) (_ : @eq V v0 v'), @eq K k' k0 *)
(* Goal: forall (_ : not (@eq K k' k0)) (_ : match assoc_find l0 k0 with | @none _ => False | @some _ v' => @eq V v0 v' end), @eq K k' k0 *)
(* Goal: @eq (option V) (assoc_find (@cons Tuple (mkTuple k' v') l0) k0) (assoc_find (assoc_add l0 k' v') k0) *)
  auto.
(* Goal: assoc_eqm (assoc_find (@cons Tuple (mkTuple k' v') l0)) (assoc_find (assoc_add l0 k' v')) *)
  apply assoc_add_egale_cons.
Qed.


Lemma assoc_add_mem_effect :
 forall (l0 l1 : assoc) (k k' : K) (v : V),
 ~ assoc_mem l0 k -> assoc_mem l1 k -> l1 = assoc_add l0 k' v -> k' = k.

Proof.
(* Goal: forall (_ : not (@eq K k' k0)) (_ : @eq (option V) (some V v0) (assoc_find l0 k0)), @eq K k' k0 *)
(* Goal: @eq (option V) (assoc_find (@cons Tuple (mkTuple k' v') l0) k0) (assoc_find (assoc_add l0 k' v') k0) *)
unfold assoc_mem in |- *; intros.
(* Goal: @eq K k' k0 *)
rewrite H1 in H0. generalize H0.
replace (assoc_find (assoc_add l0 k' v0) k0) with
 (assoc_find (mkTuple k' v0 :: l0) k0).
(* Goal: forall _ : match assoc_find (@cons Tuple (mkTuple k' v') l0) k0 with | @none _ => False | @some _ v' => @eq V v0 v' end, @eq K k' k0 *)
(* Goal: @eq (option V) (assoc_find (@cons Tuple (mkTuple k' v') l0) k0) (assoc_find (assoc_add l0 k' v') k0) *)
simpl in |- *. case (Keq_dec k' k0). auto.

(* Goal: assoc_almost_eqm k0 (assoc_find l) (assoc_find (@cons Tuple (mkTuple k0 v') l)) *)
(* Goal: assoc_almost_eqm k0 (assoc_find (@cons Tuple (mkTuple k0 v0) l)) (assoc_find l) *)
(* Goal: assoc_almost_eqm k0 (assoc_find l) (assoc_find (@cons Tuple (mkTuple k0 v') l)) *)
intros; absurd (assoc_mem l0 k0); unfold assoc_mem in |- *; assumption.

cut
 (assoc_eqm (assoc_find (mkTuple k' v0 :: l0))
    (assoc_find (assoc_add l0 k' v0))).
(* Goal: forall (_ : @eq K k' k0) (_ : @eq V v0 v'), @eq K k' k0 *)
(* Goal: forall (_ : not (@eq K k' k0)) (_ : match assoc_find l0 k0 with | @none _ => False | @some _ v' => @eq V v0 v' end), @eq K k' k0 *)
(* Goal: @eq (option V) (assoc_find (@cons Tuple (mkTuple k' v') l0) k0) (assoc_find (assoc_add l0 k' v') k0) *)
unfold assoc_eqm in |- *; auto.

(* Goal: assoc_eqm (assoc_find (@cons Tuple (mkTuple k' v') l0)) (assoc_find (assoc_add l0 k' v')) *)
apply assoc_add_egale_cons.
Qed.


Lemma assoc_add_hasmem_effect :
 forall (l0 l1 : assoc) (k k' : K) (v v' : V),
 ~ assoc_hasmem l0 k v ->
 assoc_hasmem l1 k v -> l1 = assoc_add l0 k' v' -> k' = k /\ v' = v.

Proof.
(* Goal: forall (_ : not (@eq K k' k0)) (_ : @eq (option V) (some V v0) (assoc_find l0 k0)), @eq K k' k0 *)
(* Goal: @eq (option V) (assoc_find (@cons Tuple (mkTuple k' v') l0) k0) (assoc_find (assoc_add l0 k' v') k0) *)
unfold assoc_hasmem in |- *; intros.
(* Goal: and (@eq K k' k0) (@eq V v' v0) *)
cut (k' = k0).
(* Goal: forall (_ : @eq K k' k0) (_ : @eq V v0 v'), @eq K k' k0 *)
(* Goal: forall (_ : not (@eq K k' k0)) (_ : match assoc_find l0 k0 with | @none _ => False | @some _ v' => @eq V v0 v' end), @eq K k' k0 *)
(* Goal: @eq (option V) (assoc_find (@cons Tuple (mkTuple k' v') l0) k0) (assoc_find (assoc_add l0 k' v') k0) *)
  split; auto.
generalize H0; rewrite H1; rewrite H2;
 replace (assoc_find (assoc_add l0 k0 v') k0) with (some V v'); 
(* Goal: forall (_ : @eq K k' k0) (_ : @eq V v0 v'), @eq K k' k0 *)
(* Goal: forall (_ : not (@eq K k' k0)) (_ : match assoc_find l0 k0 with | @none _ => False | @some _ v' => @eq V v0 v' end), @eq K k' k0 *)
(* Goal: @eq (option V) (assoc_find (@cons Tuple (mkTuple k' v') l0) k0) (assoc_find (assoc_add l0 k' v') k0) *)
 auto.
(* Goal: @eq (option V) (assoc_find (assoc_add l0 k0 v') k0) (some V v') *)
(* Goal: @eq K k' k0 *)
symmetry  in |- *; apply assoc_add_correct_2.
(* Goal: @eq K k' k0 *)
generalize H0; rewrite H1.
replace (assoc_find (assoc_add l0 k' v') k0) with
 (assoc_find (mkTuple k' v' :: l0) k0).
(* Goal: forall _ : match assoc_find (@cons Tuple (mkTuple k' v') l0) k0 with | @none _ => False | @some _ v' => @eq V v0 v' end, @eq K k' k0 *)
(* Goal: @eq (option V) (assoc_find (@cons Tuple (mkTuple k' v') l0) k0) (assoc_find (assoc_add l0 k' v') k0) *)
simpl in |- *. case (Keq_dec k' k0). auto.

intros; absurd (assoc_hasmem l0 k0 v0); unfold assoc_hasmem in |- *;
(* Goal: assoc_almost_eqm k0 (assoc_find l) (assoc_find (@cons Tuple (mkTuple k0 v') l)) *)
(* Goal: assoc_almost_eqm k0 (assoc_find (@cons Tuple (mkTuple k0 v0) l)) (assoc_find l) *)
(* Goal: assoc_almost_eqm k0 (assoc_find l) (assoc_find (@cons Tuple (mkTuple k0 v') l)) *)
 assumption.

cut
 (assoc_eqm (assoc_find (mkTuple k' v' :: l0))
    (assoc_find (assoc_add l0 k' v'))).
(* Goal: forall (_ : @eq K k' k0) (_ : @eq V v0 v'), @eq K k' k0 *)
(* Goal: forall (_ : not (@eq K k' k0)) (_ : match assoc_find l0 k0 with | @none _ => False | @some _ v' => @eq V v0 v' end), @eq K k' k0 *)
(* Goal: @eq (option V) (assoc_find (@cons Tuple (mkTuple k' v') l0) k0) (assoc_find (assoc_add l0 k' v') k0) *)
  unfold assoc_eqm in |- *; auto.
(* Goal: assoc_eqm (assoc_find (@cons Tuple (mkTuple k' v') l0)) (assoc_find (assoc_add l0 k' v')) *)
  apply assoc_add_egale_cons.

Qed.


Lemma assoc_del_mem_effect :
 forall (l : assoc) (k k' : K),
 assoc_mem l k -> ~ assoc_mem (assoc_delete l k') k -> k' = k.

Proof.
intros l k0 k1;
 cut (assoc_almost_eqm k1 (assoc_find l) (assoc_find (assoc_delete l k1))).
(* Goal: forall _ : assoc_mem (assoc_delete l k') k0, assoc_mem l k0 *)
unfold assoc_almost_eqm in |- *; unfold assoc_mem in |- *.
(* Goal: forall (_ : @eq K k' k0) (_ : @eq V v0 v'), @eq K k' k0 *)
(* Goal: forall (_ : not (@eq K k' k0)) (_ : match assoc_find l0 k0 with | @none _ => False | @some _ v' => @eq V v0 v' end), @eq K k' k0 *)
(* Goal: @eq (option V) (assoc_find (@cons Tuple (mkTuple k' v') l0) k0) (assoc_find (assoc_add l0 k' v') k0) *)
case (Keq_dec k1 k0); auto.
  intros until 2;
   replace (assoc_find (assoc_delete l k1) k0) with (assoc_find l k0).
(* Goal: forall (v _ : V) (_ : match assoc_find l k0 with | @none _ => False | @some _ v'0 => @eq V v v'0 end) (_ : not match assoc_find l k0 with | @none _ => False | @some _ v'0 => @eq V v v'0 end), @eq K k1 k0 *)
(* Goal: @eq (option V) (assoc_find l k0) (assoc_find (assoc_delete l k1) k0) *)
(* Goal: assoc_almost_eqm k1 (assoc_find l) (assoc_find (assoc_delete l k1)) *)
    case (assoc_find l k0).
(* Goal: @eq V v1 v0 *)
(* Goal: @eq V v1 v0 *)
      intros; contradiction.
(* Goal: forall (_ : @eq K k' k0) (_ : @eq V v0 v'), @eq K k' k0 *)
(* Goal: forall (_ : not (@eq K k' k0)) (_ : match assoc_find l0 k0 with | @none _ => False | @some _ v' => @eq V v0 v' end), @eq K k' k0 *)
(* Goal: @eq (option V) (assoc_find (@cons Tuple (mkTuple k' v') l0) k0) (assoc_find (assoc_add l0 k' v') k0) *)
      unfold not in |- *; tauto.
(* Goal: forall (_ : @eq K k' k0) (_ : @eq V v0 v'), @eq K k' k0 *)
(* Goal: forall (_ : not (@eq K k' k0)) (_ : match assoc_find l0 k0 with | @none _ => False | @some _ v' => @eq V v0 v' end), @eq K k' k0 *)
(* Goal: @eq (option V) (assoc_find (@cons Tuple (mkTuple k' v') l0) k0) (assoc_find (assoc_add l0 k' v') k0) *)
    apply H; auto.
(* Goal: assoc_almost_eqm k1 (assoc_find l) (assoc_find (assoc_delete l k1)) *)
  apply assoc_semfind_del.
Qed.


Lemma assoc_del_hasmem_effect :
 forall (l : assoc) (k k' : K) (v v' : V),
 assoc_hasmem l k v -> ~ assoc_hasmem (assoc_delete l k') k v -> k' = k.

Proof.
intros l k0 k1;
 cut (assoc_almost_eqm k1 (assoc_find l) (assoc_find (assoc_delete l k1))).
(* Goal: forall (l : assoc) (k : K) (v v' : V) (_ : assoc_hasmem l k v) (_ : assoc_hasmem l k v'), @eq V v' v *)
unfold assoc_almost_eqm in |- *; unfold assoc_hasmem in |- *.
(* Goal: forall (_ : @eq K k' k0) (_ : @eq V v0 v'), @eq K k' k0 *)
(* Goal: forall (_ : not (@eq K k' k0)) (_ : match assoc_find l0 k0 with | @none _ => False | @some _ v' => @eq V v0 v' end), @eq K k' k0 *)
(* Goal: @eq (option V) (assoc_find (@cons Tuple (mkTuple k' v') l0) k0) (assoc_find (assoc_add l0 k' v') k0) *)
case (Keq_dec k1 k0); auto.
intros until 2;
 replace (assoc_find (assoc_delete l k1) k0) with (assoc_find l k0).
(* Goal: forall (v _ : V) (_ : match assoc_find l k0 with | @none _ => False | @some _ v'0 => @eq V v v'0 end) (_ : not match assoc_find l k0 with | @none _ => False | @some _ v'0 => @eq V v v'0 end), @eq K k1 k0 *)
(* Goal: @eq (option V) (assoc_find l k0) (assoc_find (assoc_delete l k1) k0) *)
(* Goal: assoc_almost_eqm k1 (assoc_find l) (assoc_find (assoc_delete l k1)) *)
case (assoc_find l k0).
(* Goal: @eq V v1 v0 *)
(* Goal: @eq V v1 v0 *)
intros; contradiction.

(* Goal: forall (_ : @eq K k' k0) (_ : @eq V v0 v'), @eq K k' k0 *)
(* Goal: forall (_ : not (@eq K k' k0)) (_ : match assoc_find l0 k0 with | @none _ => False | @some _ v' => @eq V v0 v' end), @eq K k' k0 *)
(* Goal: @eq (option V) (assoc_find (@cons Tuple (mkTuple k' v') l0) k0) (assoc_find (assoc_add l0 k' v') k0) *)
unfold not in |- *; tauto.

(* Goal: forall (_ : @eq K k' k0) (_ : @eq V v0 v'), @eq K k' k0 *)
(* Goal: forall (_ : not (@eq K k' k0)) (_ : match assoc_find l0 k0 with | @none _ => False | @some _ v' => @eq V v0 v' end), @eq K k' k0 *)
(* Goal: @eq (option V) (assoc_find (@cons Tuple (mkTuple k' v') l0) k0) (assoc_find (assoc_add l0 k' v') k0) *)
apply H; auto.

(* Goal: assoc_almost_eqm k1 (assoc_find l) (assoc_find (assoc_delete l k1)) *)
apply assoc_semfind_del.
Qed.




End associative_arrays.



















