hash tables: completed proof

examples/programs/hash_tables.mlw

@@ -69,10 +69,16 @@ module HashTableImpl
     forall k: 'a, v: 'b, l: list ('a, 'b).
     occurs_first k v l -> mem (k, v) l
 
+  lemma cons_occurs_first:
+    forall k1: 'a, v1: 'b, l: list ('a, 'b). occurs_first k1 v1 l ->
+    forall k: 'a, v: 'b. k <> k1 -> occurs_first k1 v1 (Cons (k,v) l)
+
   predicate valid (h: t 'a 'b) =
     length h.data > 0 /\
+    (* h[k]=v iff (k,v) is the first pair for k in the bucket for k *)
     (forall k: 'a, v: 'b.
        get h k = Some v <-> occurs_first k v h.data[idx h k]) /\
+    (* a pair (k,v) is always stored in the right bucket *)
     (forall k: 'a, v: 'b.
      forall i: int. 0 <= i < length h.data ->
        mem (k,v) h.data[i] -> i = idx h k)

examples/programs/hash_tables/hash_tables_WP_HashTableImpl_WP_parameter_add_1.v

+(* This file is generated by Why3's Coq driver *)
+(* Beware! Only edit allowed sections below    *)
+Require Import ZArith.
+Require Import Rbase.
+Require Import ZOdiv.
+Definition unit  := unit.
+
+Parameter qtmark : Type.
+
+Parameter at1: forall (a:Type), a -> qtmark -> a.
+
+Implicit Arguments at1.
+
+Parameter old: forall (a:Type), a -> a.
+
+Implicit Arguments old.
+
+Definition implb(x:bool) (y:bool): bool := match (x,
+  y) with
+  | (true, false) => false
+  | (_, _) => true
+  end.
+
+Inductive option (a:Type) :=
+  | None : option a
+  | Some : a -> option a.
+Set Contextual Implicit.
+Implicit Arguments None.
+Unset Contextual Implicit.
+Implicit Arguments Some.
+
+Axiom Abs_le : forall (x:Z) (y:Z), ((Zabs x) <= y)%Z <-> (((-y)%Z <= x)%Z /\
+  (x <= y)%Z).
+
+Parameter map : forall (a:Type) (b:Type), Type.
+
+Parameter get: forall (a:Type) (b:Type), (map a b) -> a -> b.
+
+Implicit Arguments get.
+
+Parameter set: forall (a:Type) (b:Type), (map a b) -> a -> b -> (map a b).
+
+Implicit Arguments set.
+
+Axiom Select_eq : forall (a:Type) (b:Type), forall (m:(map a b)),
+  forall (a1:a) (a2:a), forall (b1:b), (a1 = a2) -> ((get (set m a1 b1)
+  a2) = b1).
+
+Axiom Select_neq : forall (a:Type) (b:Type), forall (m:(map a b)),
+  forall (a1:a) (a2:a), forall (b1:b), (~ (a1 = a2)) -> ((get (set m a1 b1)
+  a2) = (get m a2)).
+
+Parameter const: forall (b:Type) (a:Type), b -> (map a b).
+
+Set Contextual Implicit.
+Implicit Arguments const.
+Unset Contextual Implicit.
+
+Axiom Const : forall (b:Type) (a:Type), forall (b1:b) (a1:a),
+  ((get (const b1:(map a b)) a1) = b1).
+
+Inductive list (a:Type) :=
+  | Nil : list a
+  | Cons : a -> (list a) -> list a.
+Set Contextual Implicit.
+Implicit Arguments Nil.
+Unset Contextual Implicit.
+Implicit Arguments Cons.
+
+Set Implicit Arguments.
+Fixpoint mem (a:Type)(x:a) (l:(list a)) {struct l}: Prop :=
+  match l with
+  | Nil => False
+  | (Cons y r) => (x = y) \/ (mem x r)
+  end.
+Unset Implicit Arguments.
+
+Inductive array (a:Type) :=
+  | mk_array : Z -> (map Z a) -> array a.
+Implicit Arguments mk_array.
+
+Definition elts (a:Type)(u:(array a)): (map Z a) :=
+  match u with
+  | (mk_array _ elts1) => elts1
+  end.
+Implicit Arguments elts.
+
+Definition length (a:Type)(u:(array a)): Z :=
+  match u with
+  | (mk_array length1 _) => length1
+  end.
+Implicit Arguments length.
+
+Definition get1 (a:Type)(a1:(array a)) (i:Z): a := (get (elts a1) i).
+Implicit Arguments get1.
+
+Definition set1 (a:Type)(a1:(array a)) (i:Z) (v:a): (array a) :=
+  match a1 with
+  | (mk_array xcl0 _) => (mk_array xcl0 (set (elts a1) i v))
+  end.
+Implicit Arguments set1.
+
+Inductive t (a:Type)
+  (b:Type) :=
+  | mk_t : (map a (option b)) -> (array (list (a* b)%type)) -> t a b.
+Implicit Arguments mk_t.
+
+Definition contents (a:Type) (b:Type)(u:(t a b)): (map a (option b)) :=
+  match u with
+  | (mk_t contents1 _) => contents1
+  end.
+Implicit Arguments contents.
+
+Definition data (a:Type) (b:Type)(u:(t a b)): (array (list (a* b)%type)) :=
+  match u with
+  | (mk_t _ data1) => data1
+  end.
+Implicit Arguments data.
+
+Definition get2 (a:Type) (b:Type)(h:(t a b)) (k:a): (option b) :=
+  (get (contents h) k).
+Implicit Arguments get2.
+
+Parameter hash: forall (a:Type), a -> Z.
+
+Implicit Arguments hash.
+
+Definition idx (a:Type) (b:Type)(h:(t a b)) (k:a): Z :=
+  (ZOmod (Zabs (hash k)) (length (data h))).
+Implicit Arguments idx.
+
+Set Implicit Arguments.
+Fixpoint occurs_first (a:Type) (b:Type)(k:a) (v:b) (l:(list (a*
+  b)%type)) {struct l}: Prop :=
+  match l with
+  | Nil => False
+  | (Cons (kqt, vqt) r) => ((k = kqt) /\ (v = vqt)) \/ ((~ (k = kqt)) /\
+      (occurs_first k v r))
+  end.
+Unset Implicit Arguments.
+
+Axiom mem_occurs_first : forall (a:Type) (b:Type), forall (k:a) (v:b)
+  (l:(list (a* b)%type)), (occurs_first k v l) -> (mem (k, v) l).
+
+Axiom cons_occurs_first : forall (a:Type) (b:Type), forall (k1:a) (v1:b)
+  (l:(list (a* b)%type)), (occurs_first k1 v1 l) -> forall (k:a) (v:b),
+  (~ (k = k1)) -> (occurs_first k1 v1 (Cons (k, v) l)).
+
+Definition valid (a:Type) (b:Type)(h:(t a b)): Prop :=
+  (0%Z <  (length (data h)))%Z /\ ((forall (k:a) (v:b), ((get2 h
+  k) = (Some v)) <-> (occurs_first k v (get1 (data h) (idx h k)))) /\
+  forall (k:a) (v:b), forall (i:Z), ((0%Z <= i)%Z /\
+  (i <  (length (data h)))%Z) -> ((mem (k, v) (get1 (data h) i)) ->
+  (i = (idx h k)))).
+Implicit Arguments valid.
+
+Axiom idx_bounds : forall (a:Type) (b:Type), forall (h:(t a b)), (valid h) ->
+  forall (k:a), (0%Z <= (idx h k))%Z /\ ((idx h k) <  (length (data h)))%Z.
+
+(* YOU MAY EDIT THE CONTEXT BELOW *)
+Require Import Classical.
+(* DO NOT EDIT BELOW *)
+
+Theorem WP_parameter_add : forall (a:Type) (b:Type), forall (h:Z),
+  forall (k:a), forall (v:b), forall (rho:(map Z (list (a* b)%type))),
+  forall (rho1:(map a (option b))), ((0%Z <  (length (data (mk_t rho1
+  (mk_array h rho)))))%Z /\ ((forall (k1:a) (v1:b), ((get2 (mk_t rho1
+  (mk_array h rho)) k1) = (Some v1)) <-> (occurs_first k1 v1
+  (get1 (data (mk_t rho1 (mk_array h rho))) (idx (mk_t rho1 (mk_array h rho))
+  k1)))) /\ forall (k1:a) (v1:b), forall (i:Z), ((0%Z <= i)%Z /\
+  (i <  (length (data (mk_t rho1 (mk_array h rho)))))%Z) -> ((mem (k1, v1)
+  (get1 (data (mk_t rho1 (mk_array h rho))) i)) -> (i = (idx (mk_t rho1
+  (mk_array h rho)) k1))))) -> ((((0%Z <  (ZOmod (Zabs (hash k)) h))%Z \/
+  (0%Z = (ZOmod (Zabs (hash k)) h))) /\
+  ((ZOmod (Zabs (hash k)) h) <  h)%Z) ->
+  ((((0%Z <  (ZOmod (Zabs (hash k)) h))%Z \/
+  (0%Z = (ZOmod (Zabs (hash k)) h))) /\
+  ((ZOmod (Zabs (hash k)) h) <  h)%Z) -> forall (x:(map Z (list (a*
+  b)%type))), (x = (set rho (ZOmod (Zabs (hash k)) h) (Cons (k, v) (get rho
+  (ZOmod (Zabs (hash k)) h))))) -> forall (rho2:(map a (option b))),
+  (rho2 = (set rho1 k (Some v))) -> forall (k1:a) (v1:b), ((get2 (mk_t rho2
+  (mk_array h x)) k1) = (Some v1)) -> (occurs_first k1 v1
+  (get1 (data (mk_t rho2 (mk_array h x))) (idx (mk_t rho2 (mk_array h x))
+  k1))))).
+(* YOU MAY EDIT THE PROOF BELOW *)
+unfold get1; simpl; intros.
+assert (case: (k1=k \/ k1<>k)) by apply classic; destruct case.
+(* k1 = k *)
+subst k1.
+subst rho2.
+unfold get2 in H4; simpl in H4.
+rewrite Select_eq in H4; auto.
+injection H4; intro; subst v1; clear H4.
+unfold idx; simpl.
+subst x; rewrite Select_eq.
+red; intuition.
+auto.
+(* k1 <> k *)
+subst rho2.
+unfold idx; simpl.
+unfold get2 in H4; simpl in H4.
+rewrite Select_neq in H4; auto.
+subst x.
+set (i := (Zabs (hash k) mod h)).
+set (i1 := (Zabs (hash k1) mod h)).
+assert (case: (i1=i \/ i1<>i)) by omega; destruct case.
+(* i1 = i *)
+subst i1.
+rewrite Select_eq; auto.
+simpl.
+right; split; auto.
+destruct H.
+destruct H3.
+rewrite <- H2.
+destruct (H3 k1 v1); clear H3.
+unfold idx in H7; simpl in H7.
+subst i.
+apply H7.
+unfold get2; simpl.
+auto.
+(* i1 <> i *)
+rewrite Select_neq; auto.
+destruct H.
+destruct H3.
+destruct (H3 k1 v1); clear H3.
+unfold idx in H7; simpl in H7.
+subst i1.
+apply H7.
+unfold get2; simpl.
+auto.
+Qed.
+(* DO NOT EDIT BELOW *)
+
+

examples/programs/hash_tables/hash_tables_WP_HashTableImpl_WP_parameter_add_2.v

+(* This file is generated by Why3's Coq driver *)
+(* Beware! Only edit allowed sections below    *)
+Require Import ZArith.
+Require Import Rbase.
+Require Import ZOdiv.
+Definition unit  := unit.
+
+Parameter qtmark : Type.
+
+Parameter at1: forall (a:Type), a -> qtmark -> a.
+
+Implicit Arguments at1.
+
+Parameter old: forall (a:Type), a -> a.
+
+Implicit Arguments old.
+
+Definition implb(x:bool) (y:bool): bool := match (x,
+  y) with
+  | (true, false) => false
+  | (_, _) => true
+  end.
+
+Inductive option (a:Type) :=
+  | None : option a
+  | Some : a -> option a.
+Set Contextual Implicit.
+Implicit Arguments None.
+Unset Contextual Implicit.
+Implicit Arguments Some.
+
+Axiom Abs_le : forall (x:Z) (y:Z), ((Zabs x) <= y)%Z <-> (((-y)%Z <= x)%Z /\
+  (x <= y)%Z).
+
+Parameter map : forall (a:Type) (b:Type), Type.
+
+Parameter get: forall (a:Type) (b:Type), (map a b) -> a -> b.
+
+Implicit Arguments get.
+
+Parameter set: forall (a:Type) (b:Type), (map a b) -> a -> b -> (map a b).
+
+Implicit Arguments set.
+
+Axiom Select_eq : forall (a:Type) (b:Type), forall (m:(map a b)),
+  forall (a1:a) (a2:a), forall (b1:b), (a1 = a2) -> ((get (set m a1 b1)
+  a2) = b1).
+
+Axiom Select_neq : forall (a:Type) (b:Type), forall (m:(map a b)),
+  forall (a1:a) (a2:a), forall (b1:b), (~ (a1 = a2)) -> ((get (set m a1 b1)
+  a2) = (get m a2)).
+
+Parameter const: forall (b:Type) (a:Type), b -> (map a b).
+
+Set Contextual Implicit.
+Implicit Arguments const.
+Unset Contextual Implicit.
+
+Axiom Const : forall (b:Type) (a:Type), forall (b1:b) (a1:a),
+  ((get (const b1:(map a b)) a1) = b1).
+
+Inductive list (a:Type) :=
+  | Nil : list a
+  | Cons : a -> (list a) -> list a.
+Set Contextual Implicit.
+Implicit Arguments Nil.
+Unset Contextual Implicit.
+Implicit Arguments Cons.
+
+Set Implicit Arguments.
+Fixpoint mem (a:Type)(x:a) (l:(list a)) {struct l}: Prop :=
+  match l with
+  | Nil => False
+  | (Cons y r) => (x = y) \/ (mem x r)
+  end.
+Unset Implicit Arguments.
+
+Inductive array (a:Type) :=
+  | mk_array : Z -> (map Z a) -> array a.
+Implicit Arguments mk_array.
+
+Definition elts (a:Type)(u:(array a)): (map Z a) :=
+  match u with
+  | (mk_array _ elts1) => elts1
+  end.
+Implicit Arguments elts.
+
+Definition length (a:Type)(u:(array a)): Z :=
+  match u with
+  | (mk_array length1 _) => length1
+  end.
+Implicit Arguments length.
+
+Definition get1 (a:Type)(a1:(array a)) (i:Z): a := (get (elts a1) i).
+Implicit Arguments get1.
+
+Definition set1 (a:Type)(a1:(array a)) (i:Z) (v:a): (array a) :=
+  match a1 with
+  | (mk_array xcl0 _) => (mk_array xcl0 (set (elts a1) i v))
+  end.
+Implicit Arguments set1.
+
+Inductive t (a:Type)
+  (b:Type) :=
+  | mk_t : (map a (option b)) -> (array (list (a* b)%type)) -> t a b.
+Implicit Arguments mk_t.
+
+Definition contents (a:Type) (b:Type)(u:(t a b)): (map a (option b)) :=
+  match u with
+  | (mk_t contents1 _) => contents1
+  end.
+Implicit Arguments contents.
+
+Definition data (a:Type) (b:Type)(u:(t a b)): (array (list (a* b)%type)) :=
+  match u with
+  | (mk_t _ data1) => data1
+  end.
+Implicit Arguments data.
+
+Definition get2 (a:Type) (b:Type)(h:(t a b)) (k:a): (option b) :=
+  (get (contents h) k).
+Implicit Arguments get2.
+
+Parameter hash: forall (a:Type), a -> Z.
+
+Implicit Arguments hash.
+
+Definition idx (a:Type) (b:Type)(h:(t a b)) (k:a): Z :=
+  (ZOmod (Zabs (hash k)) (length (data h))).
+Implicit Arguments idx.
+
+Set Implicit Arguments.
+Fixpoint occurs_first (a:Type) (b:Type)(k:a) (v:b) (l:(list (a*
+  b)%type)) {struct l}: Prop :=
+  match l with
+  | Nil => False
+  | (Cons (kqt, vqt) r) => ((k = kqt) /\ (v = vqt)) \/ ((~ (k = kqt)) /\
+      (occurs_first k v r))
+  end.
+Unset Implicit Arguments.
+
+Axiom mem_occurs_first : forall (a:Type) (b:Type), forall (k:a) (v:b)
+  (l:(list (a* b)%type)), (occurs_first k v l) -> (mem (k, v) l).
+
+Axiom cons_occurs_first : forall (a:Type) (b:Type), forall (k1:a) (v1:b)
+  (l:(list (a* b)%type)), (occurs_first k1 v1 l) -> forall (k:a) (v:b),
+  (~ (k = k1)) -> (occurs_first k1 v1 (Cons (k, v) l)).
+
+Definition valid (a:Type) (b:Type)(h:(t a b)): Prop :=
+  (0%Z <  (length (data h)))%Z /\ ((forall (k:a) (v:b), ((get2 h
+  k) = (Some v)) <-> (occurs_first k v (get1 (data h) (idx h k)))) /\
+  forall (k:a) (v:b), forall (i:Z), ((0%Z <= i)%Z /\
+  (i <  (length (data h)))%Z) -> ((mem (k, v) (get1 (data h) i)) ->
+  (i = (idx h k)))).
+Implicit Arguments valid.
+
+Axiom idx_bounds : forall (a:Type) (b:Type), forall (h:(t a b)), (valid h) ->
+  forall (k:a), (0%Z <= (idx h k))%Z /\ ((idx h k) <  (length (data h)))%Z.
+
+(* YOU MAY EDIT THE CONTEXT BELOW *)
+Require Import Classical.
+(* DO NOT EDIT BELOW *)
+
+Theorem WP_parameter_add : forall (a:Type) (b:Type), forall (h:Z),
+  forall (k:a), forall (v:b), forall (rho:(map Z (list (a* b)%type))),
+  forall (rho1:(map a (option b))), ((0%Z <  (length (data (mk_t rho1
+  (mk_array h rho)))))%Z /\ ((forall (k1:a) (v1:b), ((get2 (mk_t rho1
+  (mk_array h rho)) k1) = (Some v1)) <-> (occurs_first k1 v1
+  (get1 (data (mk_t rho1 (mk_array h rho))) (idx (mk_t rho1 (mk_array h rho))
+  k1)))) /\ forall (k1:a) (v1:b), forall (i:Z), ((0%Z <= i)%Z /\
+  (i <  (length (data (mk_t rho1 (mk_array h rho)))))%Z) -> ((mem (k1, v1)
+  (get1 (data (mk_t rho1 (mk_array h rho))) i)) -> (i = (idx (mk_t rho1
+  (mk_array h rho)) k1))))) -> ((((0%Z <  (ZOmod (Zabs (hash k)) h))%Z \/
+  (0%Z = (ZOmod (Zabs (hash k)) h))) /\
+  ((ZOmod (Zabs (hash k)) h) <  h)%Z) ->
+  ((((0%Z <  (ZOmod (Zabs (hash k)) h))%Z \/
+  (0%Z = (ZOmod (Zabs (hash k)) h))) /\
+  ((ZOmod (Zabs (hash k)) h) <  h)%Z) -> forall (x:(map Z (list (a*
+  b)%type))), (x = (set rho (ZOmod (Zabs (hash k)) h) (Cons (k, v) (get rho
+  (ZOmod (Zabs (hash k)) h))))) -> forall (rho2:(map a (option b))),
+  (rho2 = (set rho1 k (Some v))) -> forall (k1:a) (v1:b), forall (i:Z),
+  ((0%Z <= i)%Z /\ (i <  (length (data (mk_t rho2 (mk_array h x)))))%Z) ->
+  ((mem (k1, v1) (get1 (data (mk_t rho2 (mk_array h x))) i)) ->
+  (i = (idx (mk_t rho2 (mk_array h x)) k1))))).
+(* YOU MAY EDIT THE PROOF BELOW *)
+intros.
+set (ik := (Zabs (hash k) mod h)).
+simpl in H4.
+assert (case: (i = ik \/ i<>ik)) by omega; destruct case.
+(* i = ik *)
+subst rho2.
+simpl in H5.
+subst x.
+unfold get1 in H5; simpl in H5.
+rewrite Select_eq in H5; auto.
+unfold idx; simpl.
+assert (case: (k1,v1)=(k,v) \/ (k1,v1)<>(k,v)) by apply classic; destruct case.
+(* k1,v1 = k,v *)
+injection H2; intros; subst. auto.
+(* k1,v1 <> k,v *)
+inversion H5.
+absurd ((k1,v1)=(k,v)); auto.
+fold mem in H3.
+destruct H.
+destruct H7.
+clear H7.
+simpl in H8.
+subst ik.
+apply (H8 k1 v1 i); auto.
+subst i; unfold get1; simpl.
+assumption.
+(* i <> ik *)
+subst x.
+unfold idx; simpl.
+unfold get1 in H5; simpl in H5.
+rewrite Select_neq in H5; auto.
+destruct H.
+destruct H2.
+clear H2.
+simpl in H7.
+apply (H7 k1 v1 i); auto.
+Qed.
+(* DO NOT EDIT BELOW *)
+
+