hashtbl_impl: functions find, add, and remove

examples/hashtbl_impl.mlw

@@ -88,14 +88,65 @@ module HashtblImpl
     done;
     h.data <- ndata
 
-(*
-  val add (h: t 'a) (k: key) (v: 'a) : unit
-    writes { h.data, h.view }
-    ensures { h.view = Map.set (old h.view) k (Some v) }
+  let rec list_find (k: key) (l: list (key, 'a)) : option 'a
+    variant { l }
+    ensures { match result with
+              | None -> forall v: 'a. not (mem (k, v) l)
+              | Some v -> mem (k, v) l
+              end }
+  =
+    match l with
+    | Nil -> None
+    | Cons (k', v) r -> if k = k' then Some v else list_find k r
+    end
 
-  val find (h: t 'a) (k: key) : option 'a
+  let find (h: t 'a) (k: key) : option 'a
     ensures { result = Map.get h.view k }
-*)
+  =
+    let i = bucket k (length h.data) in
+    list_find k h.data[i]
+
+  let rec list_remove (k: key) (l: list (key, 'a)) : list (key, 'a)
+    variant { l }
+    ensures { forall k': key, v: 'a.
+              mem (k',v) result <-> mem (k',v) l /\ k' <> k }
+  =
+    match l with
+    | Nil -> Nil
+    | Cons ((k', _) as p) r ->
+        if k = k' then list_remove k r else Cons p (list_remove k r)
+    end
+
+  let remove (h: t 'a) (k: key) : unit
+    writes  { h.data.elts, h.view, h.size }
+    ensures { Map.get h.view k = None }
+    ensures { forall k': key. k' <> k ->
+              Map.get h.view k' = Map.get (old h.view) k' }
+  =
+    let i = bucket k (length h.data) in
+    let l = h.data[i] in
+    match list_find k l with
+    | None ->
+        ()
+    | Some _ ->
+        h.data[i] <- list_remove k l;
+        h.size <- h.size - 1;
+        h.view <- Map.set h.view k None
+    end
+
+  let add (h: t 'a) (k: key) (v: 'a) : unit
+    writes  { h.data.elts, h.view, h.size }
+    ensures { Map.get h.view k = Some v }
+    ensures { forall k': key. k' <> k ->
+              Map.get h.view k' = Map.get (old h.view) k' }
+  =
+    abstract if h.size = length h.data then resize h;
+    remove h k;
+    let i = bucket k (length h.data) in
+    h.data[i] <- Cons (k, v) h.data[i];
+    h.size <- h.size + 1;
+    h.view <- Map.set h.view k (Some v)
+
 end
 
 module Bad

examples/hashtbl_impl/hashtbl_impl_HashtblImpl_WP_parameter_add_1.v

+(* This file is generated by Why3's Coq driver *)
+(* Beware! Only edit allowed sections below    *)
+Require Import BuiltIn.
+Require Import ZOdiv.
+Require BuiltIn.
+Require int.Int.
+Require int.Abs.
+Require int.ComputerDivision.
+Require map.Map.
+
+(* Why3 assumption *)
+Definition unit := unit.
+
+(* Why3 assumption *)
+Inductive option
+  (a:Type) {a_WT:WhyType a} :=
+  | None : option a
+  | Some : a -> option a.
+Axiom option_WhyType : forall (a:Type) {a_WT:WhyType a}, WhyType (option a).
+Existing Instance option_WhyType.
+Implicit Arguments None [[a] [a_WT]].
+Implicit Arguments Some [[a] [a_WT]].
+
+(* Why3 assumption *)
+Inductive list
+  (a:Type) {a_WT:WhyType a} :=
+  | Nil : list a
+  | Cons : a -> (list a) -> list a.
+Axiom list_WhyType : forall (a:Type) {a_WT:WhyType a}, WhyType (list a).
+Existing Instance list_WhyType.
+Implicit Arguments Nil [[a] [a_WT]].
+Implicit Arguments Cons [[a] [a_WT]].
+
+(* Why3 assumption *)
+Fixpoint mem {a:Type} {a_WT:WhyType a} (x:a) (l:(list a)) {struct l}: Prop :=
+  match l with
+  | Nil => False
+  | (Cons y r) => (x = y) \/ (mem x r)
+  end.
+
+(* Why3 assumption *)
+Inductive array
+  (a:Type) {a_WT:WhyType a} :=
+  | mk_array : Z -> (map.Map.map Z a) -> array a.
+Axiom array_WhyType : forall (a:Type) {a_WT:WhyType a}, WhyType (array a).
+Existing Instance array_WhyType.
+Implicit Arguments mk_array [[a] [a_WT]].
+
+(* Why3 assumption *)
+Definition elts {a:Type} {a_WT:WhyType a} (v:(array a)): (map.Map.map Z a) :=
+  match v with
+  | (mk_array x x1) => x1
+  end.
+
+(* Why3 assumption *)
+Definition length {a:Type} {a_WT:WhyType a} (v:(array a)): Z :=
+  match v with
+  | (mk_array x x1) => x
+  end.
+
+(* Why3 assumption *)
+Definition get {a:Type} {a_WT:WhyType a} (a1:(array a)) (i:Z): a :=
+  (map.Map.get (elts a1) i).
+
+(* Why3 assumption *)
+Definition set {a:Type} {a_WT:WhyType a} (a1:(array a)) (i:Z) (v:a): (array
+  a) := (mk_array (length a1) (map.Map.set (elts a1) i v)).
+
+(* Why3 assumption *)
+Definition make {a:Type} {a_WT:WhyType a} (n:Z) (v:a): (array a) :=
+  (mk_array n (map.Map.const v:(map.Map.map Z a))).
+
+Axiom key : Type.
+Parameter key_WhyType : WhyType key.
+Existing Instance key_WhyType.
+
+Parameter hash: key -> Z.
+
+Axiom hash_nonneg : forall (k:key), (0%Z <= (hash k))%Z.
+
+(* Why3 assumption *)
+Definition bucket (k:key) (n:Z): Z := (ZOmod (hash k) n).
+
+Axiom bucket_bounds : forall (n:Z), (0%Z < n)%Z -> forall (k:key),
+  (0%Z <= (bucket k n))%Z /\ ((bucket k n) < n)%Z.
+
+(* Why3 assumption *)
+Definition in_data {a:Type} {a_WT:WhyType a} (k:key) (v:a) (d:(array (list
+  (key* a)%type))): Prop := (mem (k, v) (get d (bucket k (length d)))).
+
+(* Why3 assumption *)
+Definition good_data {a:Type} {a_WT:WhyType a} (k:key) (v:a) (m:(map.Map.map
+  key (option a))) (d:(array (list (key* a)%type))): Prop := ((map.Map.get m
+  k) = (Some v)) <-> (in_data k v d).
+
+(* Why3 assumption *)
+Definition good_hash {a:Type} {a_WT:WhyType a} (d:(array (list (key*
+  a)%type))) (i:Z): Prop := forall (k:key) (v:a), (mem (k, v) (get d i)) ->
+  ((bucket k (length d)) = i).
+
+(* Why3 assumption *)
+Inductive t
+  (a:Type) {a_WT:WhyType a} :=
+  | mk_t : Z -> (array (list (key* a)%type)) -> (map.Map.map key (option
+      a)) -> t a.
+Axiom t_WhyType : forall (a:Type) {a_WT:WhyType a}, WhyType (t a).
+Existing Instance t_WhyType.
+Implicit Arguments mk_t [[a] [a_WT]].
+
+(* Why3 assumption *)
+Definition view {a:Type} {a_WT:WhyType a} (v:(t a)): (map.Map.map key (option
+  a)) := match v with
+  | (mk_t x x1 x2) => x2
+  end.
+
+(* Why3 assumption *)
+Definition data {a:Type} {a_WT:WhyType a} (v:(t a)): (array (list (key*
+  a)%type)) := match v with
+  | (mk_t x x1 x2) => x1
+  end.
+
+(* Why3 assumption *)
+Definition size {a:Type} {a_WT:WhyType a} (v:(t a)): Z :=
+  match v with
+  | (mk_t x x1 x2) => x
+  end.
+
+
+Require Import Why3. Ltac ae := why3 "Alt-Ergo,0.95.1," timelimit 3.
+
+(* Why3 goal *)
+Theorem WP_parameter_add : forall {a:Type} {a_WT:WhyType a}, forall (k:key)
+  (v:a), forall (rho:(map.Map.map key (option a))) (rho1:Z)
+  (rho2:(map.Map.map Z (list (key* a)%type))), ((((0%Z < rho1)%Z /\
+  forall (i:Z), ((0%Z <= i)%Z /\ (i < rho1)%Z) -> (good_hash (mk_array rho1
+  rho2) i)) /\ forall (k1:key) (v1:a), (good_data k1 v1 rho (mk_array rho1
+  rho2))) /\ (0%Z <= rho1)%Z) -> forall (rho3:Z) (rho4:(map.Map.map Z (list
+  (key* a)%type))), ((((0%Z < rho3)%Z /\ forall (i:Z), ((0%Z <= i)%Z /\
+  (i < rho3)%Z) -> (good_hash (mk_array rho3 rho4) i)) /\ forall (k1:key)
+  (v1:a), (good_data k1 v1 rho (mk_array rho3 rho4))) /\ (0%Z <= rho3)%Z) ->
+  forall (rho5:(map.Map.map key (option a))) (rho6:(map.Map.map Z (list (key*
+  a)%type))) (rho7:Z), (((((0%Z < rho3)%Z /\ forall (i:Z), ((0%Z <= i)%Z /\
+  (i < rho3)%Z) -> (good_hash (mk_array rho3 rho6) i)) /\ forall (k1:key)
+  (v1:a), (good_data k1 v1 rho5 (mk_array rho3 rho6))) /\ (0%Z <= rho3)%Z) /\
+  (((map.Map.get rho5 k) = (None :(option a))) /\ forall (k':key),
+  (~ (k' = k)) -> ((map.Map.get rho5 k') = (map.Map.get rho k')))) ->
+  (((0%Z <= (bucket k rho3))%Z /\ ((bucket k rho3) < rho3)%Z) ->
+  (((0%Z <= (bucket k rho3))%Z /\ ((bucket k rho3) < rho3)%Z) ->
+  forall (o:(map.Map.map Z (list (key* a)%type))), ((0%Z <= rho3)%Z /\
+  (o = (map.Map.set rho6 (bucket k rho3) (Cons (k, v) (map.Map.get rho6
+  (bucket k rho3)))))) -> forall (rho8:Z), (rho8 = (rho7 + 1%Z)%Z) ->
+  forall (rho9:(map.Map.map key (option a))), (rho9 = (map.Map.set rho5 k
+  (Some v))) -> forall (i:Z), ((0%Z <= i)%Z /\ (i < rho3)%Z) -> (good_hash
+  (mk_array rho3 o) i))).
+intros a a_WT k v rho rho1 rho2 (((h1,h2),h3),h4) rho3 rho4 (((h5,h6),h7),h8)
+rho5 rho6 rho7 ((((h9,h10),h11),h12),(h13,h14)) (h15,h16) (h17,h18) o
+(h19,h20) rho8 h21 rho9 h22 i (h23,h24).
+unfold good_hash in *.
+clear h11.
+generalize (h10 i (conj h23 h24)); clear h10; intro h10.
+subst o; unfold get; simpl.
+intros k0 v0.
+assert (h: (i = bucket k rho3) \/ (i <> bucket k rho3)%Z) by omega.
+destruct h.
+ae.
+ae.
+Qed.
+
+

examples/hashtbl_impl/hashtbl_impl_HashtblImpl_WP_parameter_find_1.v

+(* This file is generated by Why3's Coq driver *)
+(* Beware! Only edit allowed sections below    *)
+Require Import BuiltIn.
+Require Import ZOdiv.
+Require BuiltIn.
+Require int.Int.
+Require int.Abs.
+Require int.ComputerDivision.
+Require map.Map.
+
+(* Why3 assumption *)
+Definition unit := unit.
+
+(* Why3 assumption *)
+Inductive option
+  (a:Type) {a_WT:WhyType a} :=
+  | None : option a
+  | Some : a -> option a.
+Axiom option_WhyType : forall (a:Type) {a_WT:WhyType a}, WhyType (option a).
+Existing Instance option_WhyType.
+Implicit Arguments None [[a] [a_WT]].
+Implicit Arguments Some [[a] [a_WT]].
+
+(* Why3 assumption *)
+Inductive list
+  (a:Type) {a_WT:WhyType a} :=
+  | Nil : list a
+  | Cons : a -> (list a) -> list a.
+Axiom list_WhyType : forall (a:Type) {a_WT:WhyType a}, WhyType (list a).
+Existing Instance list_WhyType.
+Implicit Arguments Nil [[a] [a_WT]].
+Implicit Arguments Cons [[a] [a_WT]].
+
+(* Why3 assumption *)
+Fixpoint mem {a:Type} {a_WT:WhyType a} (x:a) (l:(list a)) {struct l}: Prop :=
+  match l with
+  | Nil => False
+  | (Cons y r) => (x = y) \/ (mem x r)
+  end.
+
+(* Why3 assumption *)
+Inductive array
+  (a:Type) {a_WT:WhyType a} :=
+  | mk_array : Z -> (map.Map.map Z a) -> array a.
+Axiom array_WhyType : forall (a:Type) {a_WT:WhyType a}, WhyType (array a).
+Existing Instance array_WhyType.
+Implicit Arguments mk_array [[a] [a_WT]].
+
+(* Why3 assumption *)
+Definition elts {a:Type} {a_WT:WhyType a} (v:(array a)): (map.Map.map Z a) :=
+  match v with
+  | (mk_array x x1) => x1
+  end.
+
+(* Why3 assumption *)
+Definition length {a:Type} {a_WT:WhyType a} (v:(array a)): Z :=
+  match v with
+  | (mk_array x x1) => x
+  end.
+
+(* Why3 assumption *)
+Definition get {a:Type} {a_WT:WhyType a} (a1:(array a)) (i:Z): a :=
+  (map.Map.get (elts a1) i).
+
+(* Why3 assumption *)
+Definition set {a:Type} {a_WT:WhyType a} (a1:(array a)) (i:Z) (v:a): (array
+  a) := (mk_array (length a1) (map.Map.set (elts a1) i v)).
+
+(* Why3 assumption *)
+Definition make {a:Type} {a_WT:WhyType a} (n:Z) (v:a): (array a) :=
+  (mk_array n (map.Map.const v:(map.Map.map Z a))).
+
+Axiom key : Type.
+Parameter key_WhyType : WhyType key.
+Existing Instance key_WhyType.
+
+Parameter hash: key -> Z.
+
+Axiom hash_nonneg : forall (k:key), (0%Z <= (hash k))%Z.
+
+(* Why3 assumption *)
+Definition bucket (k:key) (n:Z): Z := (ZOmod (hash k) n).
+
+Axiom bucket_bounds : forall (n:Z), (0%Z < n)%Z -> forall (k:key),
+  (0%Z <= (bucket k n))%Z /\ ((bucket k n) < n)%Z.
+
+(* Why3 assumption *)
+Definition in_data {a:Type} {a_WT:WhyType a} (k:key) (v:a) (d:(array (list
+  (key* a)%type))): Prop := (mem (k, v) (get d (bucket k (length d)))).
+
+(* Why3 assumption *)
+Definition good_data {a:Type} {a_WT:WhyType a} (k:key) (v:a) (m:(map.Map.map
+  key (option a))) (d:(array (list (key* a)%type))): Prop := ((map.Map.get m
+  k) = (Some v)) <-> (in_data k v d).
+
+(* Why3 assumption *)
+Definition good_hash {a:Type} {a_WT:WhyType a} (d:(array (list (key*
+  a)%type))) (i:Z): Prop := forall (k:key) (v:a), (mem (k, v) (get d i)) ->
+  ((bucket k (length d)) = i).
+
+(* Why3 assumption *)
+Inductive t
+  (a:Type) {a_WT:WhyType a} :=
+  | mk_t : Z -> (array (list (key* a)%type)) -> (map.Map.map key (option
+      a)) -> t a.
+Axiom t_WhyType : forall (a:Type) {a_WT:WhyType a}, WhyType (t a).
+Existing Instance t_WhyType.
+Implicit Arguments mk_t [[a] [a_WT]].
+
+(* Why3 assumption *)
+Definition view {a:Type} {a_WT:WhyType a} (v:(t a)): (map.Map.map key (option
+  a)) := match v with
+  | (mk_t x x1 x2) => x2
+  end.
+
+(* Why3 assumption *)
+Definition data {a:Type} {a_WT:WhyType a} (v:(t a)): (array (list (key*
+  a)%type)) := match v with
+  | (mk_t x x1 x2) => x1
+  end.
+
+(* Why3 assumption *)
+Definition size {a:Type} {a_WT:WhyType a} (v:(t a)): Z :=
+  match v with
+  | (mk_t x x1 x2) => x
+  end.
+
+(* Why3 goal *)
+Theorem WP_parameter_find : forall {a:Type} {a_WT:WhyType a}, forall (k:key),
+  forall (rho:(map.Map.map key (option a))) (rho1:Z) (rho2:(map.Map.map Z
+  (list (key* a)%type))), ((((0%Z < rho1)%Z /\ forall (i:Z), ((0%Z <= i)%Z /\
+  (i < rho1)%Z) -> (good_hash (mk_array rho1 rho2) i)) /\ forall (k1:key)
+  (v:a), (good_data k1 v rho (mk_array rho1 rho2))) /\ (0%Z <= rho1)%Z) ->
+  (((0%Z <= (bucket k rho1))%Z /\ ((bucket k rho1) < rho1)%Z) -> let o :=
+  (map.Map.get rho2 (bucket k rho1)) in forall (result:(option a)),
+  match result with
+  | None => forall (v:a), ~ (mem (k, v) o)
+  | (Some v) => (mem (k, v) o)
+  end -> (result = (map.Map.get rho k))).
+intros a a_WT k rho rho1 rho2 (((h1,h2),h3),h4) (h5,h6) o result h7.
+destruct result.
+unfold good_data in h3.
+generalize (h3 k); clear h3.
+destruct (Map.get rho k).
+auto.
+intro h; generalize (h a0); clear h.
+intuition.
+unfold in_data in H.
+unfold get in H; simpl in H.
+generalize (h7 a0); clear h7.
+intuition.
+subst o.
+generalize (h3 k); clear h3.
+intro h; generalize (h a0); clear h; intro h.
+unfold good_data in h.
+destruct (Map.get rho k).
+symmetry.
+intuition.
+symmetry.
+intuition.
+Qed.
+
+

examples/hashtbl_impl/hashtbl_impl_HashtblImpl_WP_parameter_remove_1.v

+(* This file is generated by Why3's Coq driver *)
+(* Beware! Only edit allowed sections below    *)
+Require Import BuiltIn.
+Require Import ZOdiv.
+Require BuiltIn.
+Require int.Int.
+Require int.Abs.
+Require int.ComputerDivision.
+Require map.Map.
+
+(* Why3 assumption *)
+Definition unit := unit.
+
+(* Why3 assumption *)
+Inductive option
+  (a:Type) {a_WT:WhyType a} :=
+  | None : option a
+  | Some : a -> option a.
+Axiom option_WhyType : forall (a:Type) {a_WT:WhyType a}, WhyType (option a).
+Existing Instance option_WhyType.
+Implicit Arguments None [[a] [a_WT]].
+Implicit Arguments Some [[a] [a_WT]].
+
+(* Why3 assumption *)
+Inductive list
+  (a:Type) {a_WT:WhyType a} :=
+  | Nil : list a
+  | Cons : a -> (list a) -> list a.
+Axiom list_WhyType : forall (a:Type) {a_WT:WhyType a}, WhyType (list a).
+Existing Instance list_WhyType.
+Implicit Arguments Nil [[a] [a_WT]].
+Implicit Arguments Cons [[a] [a_WT]].
+
+(* Why3 assumption *)
+Fixpoint mem {a:Type} {a_WT:WhyType a} (x:a) (l:(list a)) {struct l}: Prop :=
+  match l with
+  | Nil => False
+  | (Cons y r) => (x = y) \/ (mem x r)
+  end.
+
+(* Why3 assumption *)
+Inductive array
+  (a:Type) {a_WT:WhyType a} :=
+  | mk_array : Z -> (map.Map.map Z a) -> array a.
+Axiom array_WhyType : forall (a:Type) {a_WT:WhyType a}, WhyType (array a).
+Existing Instance array_WhyType.
+Implicit Arguments mk_array [[a] [a_WT]].
+
+(* Why3 assumption *)
+Definition elts {a:Type} {a_WT:WhyType a} (v:(array a)): (map.Map.map Z a) :=
+  match v with
+  | (mk_array x x1) => x1
+  end.
+
+(* Why3 assumption *)
+Definition length {a:Type} {a_WT:WhyType a} (v:(array a)): Z :=
+  match v with
+  | (mk_array x x1) => x
+  end.
+
+(* Why3 assumption *)
+Definition get {a:Type} {a_WT:WhyType a} (a1:(array a)) (i:Z): a :=
+  (map.Map.get (elts a1) i).
+
+(* Why3 assumption *)
+Definition set {a:Type} {a_WT:WhyType a} (a1:(array a)) (i:Z) (v:a): (array
+  a) := (mk_array (length a1) (map.Map.set (elts a1) i v)).
+
+(* Why3 assumption *)
+Definition make {a:Type} {a_WT:WhyType a} (n:Z) (v:a): (array a) :=
+  (mk_array n (map.Map.const v:(map.Map.map Z a))).
+
+Axiom key : Type.
+Parameter key_WhyType : WhyType key.
+Existing Instance key_WhyType.
+
+Parameter hash: key -> Z.
+
+Axiom hash_nonneg : forall (k:key), (0%Z <= (hash k))%Z.
+
+(* Why3 assumption *)
+Definition bucket (k:key) (n:Z): Z := (ZOmod (hash k) n).
+
+Axiom bucket_bounds : forall (n:Z), (0%Z < n)%Z -> forall (k:key),
+  (0%Z <= (bucket k n))%Z /\ ((bucket k n) < n)%Z.
+
+(* Why3 assumption *)
+Definition in_data {a:Type} {a_WT:WhyType a} (k:key) (v:a) (d:(array (list
+  (key* a)%type))): Prop := (mem (k, v) (get d (bucket k (length d)))).
+
+(* Why3 assumption *)
+Definition good_data {a:Type} {a_WT:WhyType a} (k:key) (v:a) (m:(map.Map.map
+  key (option a))) (d:(array (list (key* a)%type))): Prop := ((map.Map.get m
+  k) = (Some v)) <-> (in_data k v d).
+
+(* Why3 assumption *)
+Definition good_hash {a:Type} {a_WT:WhyType a} (d:(array (list (key*
+  a)%type))) (i:Z): Prop := forall (k:key) (v:a), (mem (k, v) (get d i)) ->
+  ((bucket k (length d)) = i).
+
+(* Why3 assumption *)
+Inductive t
+  (a:Type) {a_WT:WhyType a} :=
+  | mk_t : Z -> (array (list (key* a)%type)) -> (map.Map.map key (option
+      a)) -> t a.
+Axiom t_WhyType : forall (a:Type) {a_WT:WhyType a}, WhyType (t a).
+Existing Instance t_WhyType.
+Implicit Arguments mk_t [[a] [a_WT]].
+
+(* Why3 assumption *)
+Definition view {a:Type} {a_WT:WhyType a} (v:(t a)): (map.Map.map key (option
+  a)) := match v with
+  | (mk_t x x1 x2) => x2
+  end.
+
+(* Why3 assumption *)
+Definition data {a:Type} {a_WT:WhyType a} (v:(t a)): (array (list (key*
+  a)%type)) := match v with
+  | (mk_t x x1 x2) => x1
+  end.
+
+(* Why3 assumption *)
+Definition size {a:Type} {a_WT:WhyType a} (v:(t a)): Z :=
+  match v with
+  | (mk_t x x1 x2) => x
+  end.
+
+(* Why3 goal *)
+Theorem WP_parameter_remove : forall {a:Type} {a_WT:WhyType a},
+  forall (k:key), forall (rho:(map.Map.map key (option a))) (rho1:Z)
+  (rho2:(map.Map.map Z (list (key* a)%type))), ((((0%Z < rho1)%Z /\
+  forall (i:Z), ((0%Z <= i)%Z /\ (i < rho1)%Z) -> (good_hash (mk_array rho1
+  rho2) i)) /\ forall (k1:key) (v:a), (good_data k1 v rho (mk_array rho1
+  rho2))) /\ (0%Z <= rho1)%Z) -> (((0%Z <= (bucket k rho1))%Z /\ ((bucket k
+  rho1) < rho1)%Z) -> let l := (map.Map.get rho2 (bucket k rho1)) in
+  forall (result:(option a)),
+  match result with
+  | None => forall (v:a), ~ (mem (k, v) l)
+  | (Some v) => (mem (k, v) l)
+  end ->
+  match result with
+  | None => ((map.Map.get rho k) = (None :(option a)))
+  | (Some _) => True
+  end).
+intros a a_WT k rho rho1 rho2 (((h1,h2),h3),h4) (h5,h6) l result h7.
+destruct result; auto.
+subst l.
+unfold good_data in h3.
+generalize (h3 k); clear h3; intro h3.
+destruct (Map.get rho k); intuition.
+generalize (h3 a0); clear h3; intro h3.
+generalize (h7 a0); clear h7; intro h7.
+intuition.
+Qed.
+
+