reorganize examples/

- all programs with sessions are in examples/
- all programs without sessions are in examples/in_progress/
  (if you have private sessions for those, just move them there)
- all pure logical problems are in logic/
  (to simplify bench scripts and gallery building; they are few anyway)
- all OCaml programs are in examples/use_api/
- all strange stuff is in examples/misc/
  (most of it should probably go)
- Claude's solutions for Foveoos 2011 are in examples/foveoos11-cm/
  (why do we need two sets of solutions for quite simple problems?)
- hoare_logic, bitvectors, vacid_0_binary_heaps are in examples/

Bench scripts and documentation are updated.
Also, bench/bench is simplified a little bit.

examples/decrease1/decrease1_Decrease1_decrease1_induction_2.v

@@ -0,0 +1,87 @@
+(* This file is generated by Why3's Coq driver *)
+(* Beware! Only edit allowed sections below    *)
+Require Import BuiltIn.
+Require BuiltIn.
+Require int.Int.
+Require map.Map.
+
+(* Why3 assumption *)
+Definition unit  := unit.
+
+(* Why3 assumption *)
+Inductive ref (a:Type) {a_WT:WhyType a} :=
+  | mk_ref : a -> ref a.
+Axiom ref_WhyType : forall (a:Type) {a_WT:WhyType a}, WhyType (ref a).
+Existing Instance ref_WhyType.
+Implicit Arguments mk_ref [[a] [a_WT]].
+
+(* Why3 assumption *)
+Definition contents {a:Type} {a_WT:WhyType a}(v:(ref a)): a :=
+  match v with
+  | (mk_ref x) => x
+  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))).
+
+(* Why3 assumption *)
+Definition decrease1(a:(array Z)): Prop := forall (i:Z), ((0%Z <= i)%Z /\
+  (i < ((length a) - 1%Z)%Z)%Z) -> (((get a i) - 1%Z)%Z <= (get a
+  (i + 1%Z)%Z))%Z.
+
+
+(* Why3 goal *)
+Theorem decrease1_induction : forall (a:(array Z)), (decrease1 a) ->
+  forall (i:Z) (j:Z), (((0%Z <= i)%Z /\ (i <= j)%Z) /\ (j < (length a))%Z) ->
+  ((((get a i) + i)%Z - j)%Z <= (get a j))%Z.
+(* YOU MAY EDIT THE PROOF BELOW *)
+unfold decrease1.
+intros a Ha i j Hij.
+generalize Hij; pattern j.
+apply (Zlt_lower_bound_ind _ i).
+2: omega.
+intuition.
+assert (x = i \/ i < x)%Z by omega.
+destruct H4.
+subst x.
+ring_simplify.
+omega.
+apply Zle_trans with (get a (x-1) - 1)%Z.
+assert (i <= x-1 < x)%Z by omega.
+assert (0 <= i <= x-1 /\ x-1 < length a)%Z by omega.
+generalize (H (x-1)%Z H8 H9); clear H; intuition.
+apply Zle_trans with (get a (x-1+1))%Z.
+apply (Ha (x-1)%Z); omega.
+ring_simplify (x-1+1)%Z.
+omega.
+Qed.
+
+

examples/decrease1/decrease1_WP_Decrease1_WP_parameter_search_rec_1.v

@@ -0,0 +1,93 @@
+(* This file is generated by Why3's Coq driver *)
+(* Beware! Only edit allowed sections below    *)
+Require Import BuiltIn.
+Require BuiltIn.
+Require int.Int.
+Require map.Map.
+
+(* Why3 assumption *)
+Definition unit  := unit.
+
+(* Why3 assumption *)
+Inductive ref (a:Type) {a_WT:WhyType a} :=
+  | mk_ref : a -> ref a.
+Axiom ref_WhyType : forall (a:Type) {a_WT:WhyType a}, WhyType (ref a).
+Existing Instance ref_WhyType.
+Implicit Arguments mk_ref [[a] [a_WT]].
+
+(* Why3 assumption *)
+Definition contents {a:Type} {a_WT:WhyType a}(v:(ref a)): a :=
+  match v with
+  | (mk_ref x) => x
+  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))).
+
+(* Why3 assumption *)
+Definition decrease1(a:(array Z)): Prop := forall (i:Z), ((0%Z <= i)%Z /\
+  (i < ((length a) - 1%Z)%Z)%Z) -> (((get a i) - 1%Z)%Z <= (get a
+  (i + 1%Z)%Z))%Z.
+
+Axiom decrease1_induction : forall (a:(array Z)), (decrease1 a) ->
+  forall (i:Z) (j:Z), (((0%Z <= i)%Z /\ (i <= j)%Z) /\ (j < (length a))%Z) ->
+  ((((get a i) + i)%Z - j)%Z <= (get a j))%Z.
+
+
+(* Why3 goal *)
+Theorem WP_parameter_search_rec : forall (a:Z) (i:Z), forall (a1:(map.Map.map
+  Z Z)), let a2 := (mk_array a a1) in (((decrease1 a2) /\ (0%Z <= i)%Z) ->
+  ((i < a)%Z -> (((0%Z <= i)%Z /\ (i < a)%Z) -> ((~ ((map.Map.get a1
+  i) = 0%Z)) -> (((0%Z <= i)%Z /\ (i < a)%Z) -> ((0%Z < (map.Map.get a1
+  i))%Z -> (((0%Z <= i)%Z /\ (i < a)%Z) -> let o := (map.Map.get a1 i) in
+  (((decrease1 a2) /\ (0%Z <= (i + o)%Z)%Z) -> forall (result:Z),
+  (((result = (-1%Z)%Z) /\ forall (j:Z), (((i + o)%Z <= j)%Z /\ (j < a)%Z) ->
+  ~ ((map.Map.get a1 j) = 0%Z)) \/ ((((i + o)%Z <= result)%Z /\
+  (result < a)%Z) /\ (((map.Map.get a1 result) = 0%Z) /\ forall (j:Z),
+  (((i + o)%Z <= j)%Z /\ (j < result)%Z) -> ~ ((map.Map.get a1
+  j) = 0%Z)))) -> (((result = (-1%Z)%Z) /\ forall (j:Z), ((i <= j)%Z /\
+  (j < a)%Z) -> ~ ((map.Map.get a1 j) = 0%Z)) \/ (((i <= result)%Z /\
+  (result < a)%Z) /\ (((map.Map.get a1 result) = 0%Z) /\ forall (j:Z),
+  ((i <= j)%Z /\ (j < result)%Z) -> ~ ((map.Map.get a1 j) = 0%Z)))))))))))).
+Proof.
+intuition.
+intuition.
+left; intuition.
+destruct (Z_lt_le_dec j (i + Map.get a1 i)) as [case|case].
+generalize (decrease1_induction (mk_array a a1) H5 i j); unfold get; simpl; intuition.
+apply H14 with j; auto.
+right; intuition.
+destruct (Z_lt_le_dec j (i + Map.get a1 i)) as [case|case].
+generalize (decrease1_induction (mk_array a a1) H5 i j); unfold get; simpl; intuition.
+apply H16 with j; auto.
+Qed.
+
+