hashtbl_impl_HashtblImpl_WP_parameter_remove_2.v 4.09 KB
Newer Older
Andrei Paskevich's avatar
Andrei Paskevich committed
1
(* This file is generated by Why3's Coq driver *)
2 3 4 5 6 7 8 9 10 11 12 13 14 15
(* Beware! Only edit allowed sections below    *)
Require Import BuiltIn.
Require BuiltIn.
Require int.Int.
Require int.Abs.
Require int.ComputerDivision.
Require option.Option.
Require list.List.
Require list.Mem.
Require map.Map.

(* Why3 assumption *)
Definition unit := unit.

Andrei Paskevich's avatar
Andrei Paskevich committed
16 17 18 19
Axiom qtmark : Type.
Parameter qtmark_WhyType : WhyType qtmark.
Existing Instance qtmark_WhyType.

20
(* Why3 assumption *)
Andrei Paskevich's avatar
Andrei Paskevich committed
21 22
Inductive array (a:Type) :=
  | mk_array : Z -> (map.Map.map Z a) -> array a.
23 24
Axiom array_WhyType : forall (a:Type) {a_WT:WhyType a}, WhyType (array a).
Existing Instance array_WhyType.
Andrei Paskevich's avatar
Andrei Paskevich committed
25
Implicit Arguments mk_array [[a]].
26 27

(* Why3 assumption *)
Andrei Paskevich's avatar
Andrei Paskevich committed
28 29
Definition elts {a:Type} {a_WT:WhyType a} (v:(array a)): (map.Map.map Z a) :=
  match v with
30 31 32 33
  | (mk_array x x1) => x1
  end.

(* Why3 assumption *)
Andrei Paskevich's avatar
Andrei Paskevich committed
34
Definition length {a:Type} {a_WT:WhyType a} (v:(array a)): Z :=
35 36 37 38 39
  match v with
  | (mk_array x x1) => x
  end.

(* Why3 assumption *)
Andrei Paskevich's avatar
Andrei Paskevich committed
40
Definition get {a:Type} {a_WT:WhyType a} (a1:(array a)) (i:Z): a :=
41 42 43
  (map.Map.get (elts a1) i).

(* Why3 assumption *)
Andrei Paskevich's avatar
Andrei Paskevich committed
44 45
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)).
46 47

(* Why3 assumption *)
Andrei Paskevich's avatar
Andrei Paskevich committed
48 49
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))).
50 51 52 53 54 55 56 57 58 59

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 *)
Andrei Paskevich's avatar
Andrei Paskevich committed
60
Definition bucket (k:key) (n:Z): Z := (ZArith.BinInt.Z.rem (hash k) n).
61 62 63 64 65

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 *)
Andrei Paskevich's avatar
Andrei Paskevich committed
66 67
Definition in_data {a:Type} {a_WT:WhyType a} (k:key) (v:a) (d:(array
  (list (key* a)%type))): Prop := (list.Mem.mem (k, v) (get d (bucket k
68 69 70
  (length d)))).

(* Why3 assumption *)
Andrei Paskevich's avatar
Andrei Paskevich committed
71 72 73
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) = (Init.Datatypes.Some v)) <-> (in_data k v d).
74 75

(* Why3 assumption *)
Andrei Paskevich's avatar
Andrei Paskevich committed
76 77 78
Definition good_hash {a:Type} {a_WT:WhyType a} (d:(array (list (key*
  a)%type))) (i:Z): Prop := forall (k:key) (v:a), (list.Mem.mem (k, v) (get d
  i)) -> ((bucket k (length d)) = i).
79 80 81

(* Why3 assumption *)
Inductive t
Andrei Paskevich's avatar
Andrei Paskevich committed
82 83 84
  (a:Type) :=
  | mk_t : Z -> (array (list (key* a)%type)) -> (map.Map.map key
      (option a)) -> t a.
85 86
Axiom t_WhyType : forall (a:Type) {a_WT:WhyType a}, WhyType (t a).
Existing Instance t_WhyType.
Andrei Paskevich's avatar
Andrei Paskevich committed
87
Implicit Arguments mk_t [[a]].
88 89

(* Why3 assumption *)
Andrei Paskevich's avatar
Andrei Paskevich committed
90 91
Definition view {a:Type} {a_WT:WhyType a} (v:(t a)): (map.Map.map key
  (option a)) := match v with
92 93 94 95
  | (mk_t x x1 x2) => x2
  end.

(* Why3 assumption *)
Andrei Paskevich's avatar
Andrei Paskevich committed
96 97
Definition data {a:Type} {a_WT:WhyType a} (v:(t a)): (array (list (key*
  a)%type)) := match v with
98 99 100 101
  | (mk_t x x1 x2) => x1
  end.

(* Why3 assumption *)
Andrei Paskevich's avatar
Andrei Paskevich committed
102
Definition size {a:Type} {a_WT:WhyType a} (v:(t a)): Z :=
103 104 105 106 107 108
  match v with
  | (mk_t x x1 x2) => x
  end.

(* Why3 goal *)
Theorem WP_parameter_remove : forall {a:Type} {a_WT:WhyType a}, forall (h:Z)
Andrei Paskevich's avatar
Andrei Paskevich committed
109 110 111 112 113 114
  (h1:(map.Map.map Z (list (key* a)%type))) (h2:(map.Map.map key (option a)))
  (k:key), (((0%Z < h)%Z /\ ((forall (i:Z), ((0%Z <= i)%Z /\ (i < h)%Z) ->
  (good_hash (mk_array h h1) i)) /\ forall (k1:key) (v:a), (good_data k1 v h2
  (mk_array h h1)))) /\ (0%Z <= h)%Z) -> let i := (bucket k h) in
  (((0%Z <= i)%Z /\ (i < h)%Z) -> let l := (map.Map.get h1 i) in
  forall (result:(option a)),
115
  match result with
Andrei Paskevich's avatar
Andrei Paskevich committed
116 117 118 119 120 121
  | Init.Datatypes.None => forall (v:a), ~ (list.Mem.mem (k, v) l)
  | (Init.Datatypes.Some v) => (list.Mem.mem (k, v) l)
  end -> ((result = Init.Datatypes.None) -> ((map.Map.get h2
  k) = Init.Datatypes.None))).
(* Why3 intros a a_WT h h1 h2 k ((h1,(h2,h3)),h4) i (h5,h6) l result h7 h8. *)
intros a a_WT rho rho1 rho2 k ((h1,(h2,h3)),h4) i (h5,h6) l result h7 h8.
122
subst i.
Andrei Paskevich's avatar
Andrei Paskevich committed
123
subst result.
124 125 126 127 128 129 130 131 132
subst l.
unfold good_data in h3.
generalize (h3 k); clear h3; intro h3.
destruct (Map.get rho2 k); intuition.
generalize (h3 a0); clear h3; intro h3.
generalize (h7 a0); clear h7; intro h7.
intuition.
Qed.