Add instances for Coq realizations of option and list. Fix remaining Coq proof.

examples/hashtbl_impl/hashtbl_impl_HashtblImpl_WP_parameter_find_1.v

@@ -6,69 +6,46 @@ 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.
 
-(* 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.
+  | mk_array : Z -> (@map.Map.map Z _ a a_WT) -> 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
+Definition elts {a:Type} {a_WT:WhyType a} (v:(@array a a_WT)): (@map.Map.map
+  Z _ a a_WT) := match v with
   | (mk_array x x1) => x1
   end.
 
 (* Why3 assumption *)
-Definition length {a:Type} {a_WT:WhyType a} (v:(array a)): Z :=
+Definition length {a:Type} {a_WT:WhyType a} (v:(@array a a_WT)): 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 :=
+Definition get {a:Type} {a_WT:WhyType a} (a1:(@array a a_WT)) (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)).
+Definition set {a:Type} {a_WT:WhyType a} (a1:(@array a a_WT)) (i:Z)
+  (v:a): (@array a a_WT) := (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))).
+Definition make {a:Type} {a_WT:WhyType a} (n:Z) (v:a): (@array a a_WT) :=
+  (mk_array n (map.Map.const v:(@map.Map.map Z _ a a_WT))).
 
 Axiom key : Type.
 Parameter key_WhyType : WhyType key.
@@ -85,82 +62,73 @@ 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)))).
+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
+  (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).
+Definition good_data {a:Type} {a_WT:WhyType a} (k:key) (v:a) (m:(@map.Map.map
+  key key_WhyType (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).
+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).
 
 (* 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.
+  | mk_t : Z -> (@array (list (key* a)%type) _) -> (@map.Map.map
+      key key_WhyType (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
+Definition view {a:Type} {a_WT:WhyType a} (v:(@t a a_WT)): (@map.Map.map
+  key key_WhyType (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
+Definition data {a:Type} {a_WT:WhyType a} (v:(@t a a_WT)): (@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 :=
+Definition size {a:Type} {a_WT:WhyType a} (v:(@t a a_WT)): 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) ->
-  let i := (bucket k rho1) in (((0%Z <= i)%Z /\ (i < rho1)%Z) -> let o :=
-  (map.Map.get rho2 i) in forall (result:(option a)),
+  forall (rho:(@map.Map.map key key_WhyType (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) -> let i := (bucket k rho1) in
+  (((0%Z <= i)%Z /\ (i < rho1)%Z) -> let o := (map.Map.get rho2 i) in
+  forall (result:(option a)),
   match result with
-  | None => forall (v:a), ~ (mem (k, v) o)
-  | (Some v) => (mem (k, v) o)
+  | None => forall (v:a), ~ (list.Mem.mem (k, v) o)
+  | (Some v) => (list.Mem.mem (k, v) o)
   end -> (result = (map.Map.get rho k))).
 (* Why3 intros a a_WT k rho rho1 rho2 (((h1,h2),h3),h4) i (h5,h6) o result
         h7. *)
 intros a a_WT k rho rho1 rho2 (((h1,h2),h3),h4) i (h5,h6) o result h7.
 subst i.
 destruct result.
+symmetry.
+now apply h3.
+specialize (h3 k).
 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.
+elim (h7 a0).
+now apply h3.
+easy.
 Qed.
 
 

lib/coq/list/List.v

@@ -3,4 +3,18 @@
 Require Import BuiltIn.
 Require BuiltIn.
 
-
+Global Instance list_WhyType : forall T {T_WT : WhyType T}, WhyType (list T).
+split.
+apply nil.
+induction x as [|xh x] ; intros [|yh y] ; try (now right).
+now left.
+destruct (IHx y) as [->|E].
+destruct (why_decidable_eq xh yh) as [->|Eh].
+now left.
+right.
+contradict Eh.
+now injection Eh.
+right.
+contradict E.
+now injection E.
+Qed.

lib/coq/option/Option.v

@@ -3,4 +3,14 @@
 Require Import BuiltIn.
 Require BuiltIn.
 
-
+Global Instance option_WhyType : forall T {T_WT : WhyType T}, WhyType (option T).
+split.
+apply @None.
+intros [x|] [y|] ; try (now right) ; try (now left).
+destruct (why_decidable_eq x y) as [E|E].
+left.
+now apply f_equal.
+right.
+contradict E.
+now injection E.
+Qed.