Fix some Coq realizations.

lib/coq/int/Int.v

@@ -15,22 +15,27 @@ Require Import BuiltIn.
 Require BuiltIn.
 
 (* Why3 comment *)
-(* infix_ls is replaced with (x < x1)%Z by the coq driver *)
-
-(* Why3 goal *)
-Lemma infix_lseq_def : forall (x:Z) (y:Z), (x <= y)%Z <-> ((x < y)%Z \/
-  (x = y)).
-exact Zle_lt_or_eq_iff.
-Qed.
+(* prefix_mn is replaced with (-x)%Z by the coq driver *)
 
 (* Why3 comment *)
 (* infix_pl is replaced with (x + x1)%Z by the coq driver *)
 
 (* Why3 comment *)
-(* prefix_mn is replaced with (-x)%Z by the coq driver *)
+(* infix_as is replaced with (x * x1)%Z by the coq driver *)
 
 (* Why3 comment *)
-(* infix_as is replaced with (x * x1)%Z by the coq driver *)
+(* infix_ls is replaced with (x < x1)%Z by the coq driver *)
+
+(* Why3 goal *)
+Lemma infix_mn_def : forall (x:Z) (y:Z), ((x - y)%Z = (x + (-y)%Z)%Z).
+reflexivity.
+Qed.
+
+(* Why3 goal *)
+Lemma infix_lseq_def : forall (x:Z) (y:Z), (x <= y)%Z <-> ((x < y)%Z \/
+  (x = y)).
+exact Zle_lt_or_eq_iff.
+Qed.
 
 (* Why3 goal *)
 Lemma Assoc : forall (x:Z) (y:Z) (z:Z),
@@ -96,11 +101,6 @@ intros x y z.
 apply Zmult_plus_distr_l.
 Qed.
 
-(* Why3 goal *)
-Lemma infix_mn_def : forall (x:Z) (y:Z), ((x - y)%Z = (x + (-y)%Z)%Z).
-reflexivity.
-Qed.
-
 (* Why3 goal *)
 Lemma Comm1 : forall (x:Z) (y:Z), ((x * y)%Z = (y * x)%Z).
 Proof.

lib/coq/list/List.v

@@ -14,7 +14,25 @@
 Require Import BuiltIn.
 Require BuiltIn.
 
+(* Why3 assumption *)
+Definition is_nil {a:Type} {a_WT:WhyType a} (l:(list a)): Prop :=
+  match l with
+  | Init.Datatypes.nil => True
+  | (Init.Datatypes.cons _ _) => False
+  end.
+
+(* Why3 goal *)
+Lemma is_nil_spec : forall {a:Type} {a_WT:WhyType a}, forall (l:(list a)),
+  (is_nil l) <-> (l = Init.Datatypes.nil).
+Proof.
+intros a a_WT l.
+split.
+now destruct l.
+now intros ->.
+Qed.
+
 Global Instance list_WhyType : forall T {T_WT : WhyType T}, WhyType (list T).
+Proof.
 split.
 apply nil.
 induction x as [|xh x] ; intros [|yh y] ; try (now right).

lib/coq/map/Const.v

@@ -13,22 +13,23 @@
 (* Beware! Only edit allowed sections below    *)
 Require Import BuiltIn.
 Require BuiltIn.
+Require HighOrd.
 Require map.Map.
 
 (* Why3 goal *)
 Definition const: forall {a:Type} {a_WT:WhyType a} {b:Type} {b_WT:WhyType b},
-  b -> (map.Map.map a b).
+  b -> (a -> b).
+Proof.
 intros a a_WT b b_WT v.
 intros i.
 exact v.
 Defined.
 
 (* Why3 goal *)
-Lemma Const : forall {a:Type} {a_WT:WhyType a} {b:Type} {b_WT:WhyType b},
-  forall (b1:b) (a1:a), ((map.Map.get (const b1: (map.Map.map a b))
-  a1) = b1).
+Lemma const_def : forall {a:Type} {a_WT:WhyType a} {b:Type} {b_WT:WhyType b},
+  forall (v:b), forall (us:a), (((const v: (a -> b)) us) = v).
+Proof.
 intros a a_WT b b_WT b1 a1.
-unfold const.
-auto.
+reflexivity.
 Qed.
 

lib/coq/map/Map.v

@@ -13,6 +13,7 @@
 (* Beware! Only edit allowed sections below    *)
 Require Import BuiltIn.
 Require BuiltIn.
+Require HighOrd.
 
 (* This file is generated by Why3's Coq-realize driver *)
 (* Beware! Only edit allowed sections below    *)
@@ -21,11 +22,8 @@ Require BuiltIn.
 
 Require Import ClassicalEpsilon.
 
-(* Why3 goal *)
-Definition map : forall (a:Type) (b:Type), Type.
-intros.
-exact (a -> b).
-Defined.
+(* Why3 assumption *)
+Definition map (a:Type) (b:Type) := (a -> b).
 
 Global Instance map_WhyType : forall (a:Type) {a_WT:WhyType a} (b:Type) {b_WT:WhyType b}, WhyType (map a b).
 Proof.
@@ -36,16 +34,10 @@ intros x y.
 apply excluded_middle_informative.
 Qed.
 
-(* Why3 goal *)
-Definition get: forall {a:Type} {a_WT:WhyType a} {b:Type} {b_WT:WhyType b},
-  (map a b) -> a -> b.
-intros a a_WT b b_WT m x.
-exact (m x).
-Defined.
-
 (* Why3 goal *)
 Definition set: forall {a:Type} {a_WT:WhyType a} {b:Type} {b_WT:WhyType b},
-  (map a b) -> a -> b -> (map a b).
+  (a -> b) -> a -> b -> (a -> b).
+Proof.
 intros a a_WT b b_WT m x y.
 intros x'.
 destruct (why_decidable_eq x x') as [H|H].
@@ -54,22 +46,18 @@ exact (m x').
 Defined.
 
 (* Why3 goal *)
-Lemma Select_eq : forall {a:Type} {a_WT:WhyType a} {b:Type} {b_WT:WhyType b},
-  forall (m:(map a b)), forall (a1:a) (a2:a), forall (b1:b), (a1 = a2) ->
-  ((get (set m a1 b1) a2) = b1).
-Proof.
-intros a a_WT b b_WT m a1 a2 b1 h1.
-unfold get, set.
-now case why_decidable_eq.
-Qed.
-
-(* Why3 goal *)
-Lemma Select_neq : forall {a:Type} {a_WT:WhyType a}
-  {b:Type} {b_WT:WhyType b}, forall (m:(map a b)), forall (a1:a) (a2:a),
-  forall (b1:b), (~ (a1 = a2)) -> ((get (set m a1 b1) a2) = (get m a2)).
+Lemma set_def : forall {a:Type} {a_WT:WhyType a} {b:Type} {b_WT:WhyType b},
+  forall (f:(a -> b)) (x:a) (v:b), forall (y:a), ((y = x) -> (((set f x v)
+  y) = v)) /\ ((~ (y = x)) -> (((set f x v) y) = (f y))).
 Proof.
-intros a a_WT b b_WT m a1 a2 b1 h1.
-unfold get, set.
-now case why_decidable_eq.
+intros a a_WT b b_WT f x v y.
+unfold set.
+case why_decidable_eq.
+intros <-.
+easy.
+intros H.
+split ; intros H'.
+now elim H.
+easy.
 Qed.
 

lib/coq/number/Divisibility.v

@@ -22,13 +22,22 @@ Require number.Parity.
 (* Hack so that Why3 does not override the notation below.
 
 (* Why3 assumption *)
-Definition divides (d:Z) (n:Z): Prop := exists q:Z, (n = (q * d)%Z).
+Definition divides (d:Z) (n:Z): Prop := ((d = 0%Z) -> (n = 0%Z)) /\
+  ((~ (d = 0%Z)) -> ((ZArith.BinInt.Z.rem n d) = 0%Z)).
 
 *)
 
 Require Import Znumtheory.
 Notation divides := Zdivide (only parsing).
 
+(* Why3 goal *)
+Lemma divides_spec : forall (d:Z) (n:Z), (divides d n) <-> exists q:Z,
+  (n = (q * d)%Z).
+Proof.
+intros d n.
+easy.
+Qed.
+
 (* Why3 goal *)
 Lemma divides_refl : forall (n:Z), (divides n n).
 Proof.

lib/coq/number/Parity.v

@@ -17,9 +17,6 @@ Require int.Int.
 Require int.Abs.
 Require int.ComputerDivision.
 
-(* Why3 assumption *)
-Definition unit := unit.
-
 (* Why3 assumption *)
 Definition even (n:Z): Prop := exists k:Z, (n = (2%Z * k)%Z).
 

lib/coq/option/Option.v

@@ -14,7 +14,25 @@
 Require Import BuiltIn.
 Require BuiltIn.
 
+(* Why3 assumption *)
+Definition is_none {a:Type} {a_WT:WhyType a} (o:(option a)): Prop :=
+  match o with
+  | Init.Datatypes.None => True
+  | (Init.Datatypes.Some _) => False
+  end.
+
+(* Why3 goal *)
+Lemma is_none_spec : forall {a:Type} {a_WT:WhyType a}, forall (o:(option a)),
+  (is_none o) <-> (o = Init.Datatypes.None).
+Proof.
+intros a a_WT o.
+split.
+now destruct o.
+now intros ->.
+Qed.
+
 Global Instance option_WhyType : forall T {T_WT : WhyType T}, WhyType (option T).
+Proof.
 split.
 apply @None.
 intros [x|] [y|] ; try (now right) ; try (now left).

lib/coq/real/Real.v

@@ -15,22 +15,23 @@ Require Import BuiltIn.
 Require BuiltIn.
 
 (* Why3 comment *)
-(* infix_ls is replaced with (x < x1)%R by the coq driver *)
-
-(* Why3 goal *)
-Lemma infix_lseq_def : forall (x:R) (y:R), (x <= y)%R <-> ((x < y)%R \/
-  (x = y)).
-reflexivity.
-Qed.
+(* prefix_mn is replaced with (-x)%R by the coq driver *)
 
 (* Why3 comment *)
 (* infix_pl is replaced with (x + x1)%R by the coq driver *)
 
 (* Why3 comment *)
-(* prefix_mn is replaced with (-x)%R by the coq driver *)
+(* infix_as is replaced with (x * x1)%R by the coq driver *)
 
 (* Why3 comment *)
-(* infix_as is replaced with (x * x1)%R by the coq driver *)
+(* infix_ls is replaced with (x < x1)%R by the coq driver *)
+
+(* Why3 goal *)
+Lemma infix_lseq_def : forall (x:R) (y:R), (x <= y)%R <-> ((x < y)%R \/
+  (x = y)).
+Proof.
+reflexivity.
+Qed.
 
 (* Why3 goal *)
 Lemma Assoc : forall (x:R) (y:R) (z:R),
@@ -92,11 +93,6 @@ intros x y z.
 apply Rmult_plus_distr_r.
 Qed.
 
-(* Why3 goal *)
-Lemma infix_mn_def : forall (x:R) (y:R), ((x - y)%R = (x + (-y)%R)%R).
-reflexivity.
-Qed.
-
 (* Why3 goal *)
 Lemma Comm1 : forall (x:R) (y:R), ((x * y)%R = (y * x)%R).
 Proof.
@@ -122,12 +118,20 @@ Qed.
 (* Why3 goal *)
 Lemma Inverse : forall (x:R), (~ (x = 0%R)) ->
   ((x * (Reals.Rdefinitions.Rinv x))%R = 1%R).
+Proof.
 exact Rinv_r.
 Qed.
 
+(* Why3 goal *)
+Lemma infix_mn_def : forall (x:R) (y:R), ((x - y)%R = (x + (-y)%R)%R).
+Proof.
+reflexivity.
+Qed.
+
 (* Why3 goal *)
 Lemma infix_sl_def : forall (x:R) (y:R),
   ((x / y)%R = (x * (Reals.Rdefinitions.Rinv y))%R).
+Proof.
 reflexivity.
 Qed.
 

lib/coq/real/RealInfix.v

@@ -15,3 +15,10 @@ Require Import BuiltIn.
 Require BuiltIn.
 Require real.Real.
 
+(* Why3 goal *)
+Lemma infix_mndt_def : forall (x:R) (y:R), ((x - y)%R = (x + (-y)%R)%R).
+Proof.
+intros x y.
+reflexivity.
+Qed.
+

lib/coq/set/Set.v

@@ -13,234 +13,238 @@
 (* Beware! Only edit allowed sections below    *)
 Require Import BuiltIn.
 Require BuiltIn.
+Require HighOrd.
+Require map.Map.
+Require map.Const.
 
 Require Import ClassicalEpsilon.
 
 Lemma predicate_extensionality:
-  forall A (P Q : A -> Prop),
-    (forall x, P x <-> Q x) -> P = Q.
+  forall A (P Q : A -> bool),
+    (forall x, P x = Q x) -> P = Q.
 Admitted.
-(* "it is folklore that the two together are consistent" *)
 
-(* Why3 goal *)
-Definition set : forall (a:Type), Type.
-intros.
-exact (a -> Prop).
-Defined.
+(* Why3 assumption *)
+Definition set (a:Type) := (a -> bool).
 
 Global Instance set_WhyType : forall (a:Type) {a_WT:WhyType a}, WhyType (set a).
 Proof.
 intros.
 split.
-exact (fun _ => False).
+exact (fun _ => false).
 intros x y.
 apply excluded_middle_informative.
 Qed.
 
-(* Why3 goal *)
-Definition mem: forall {a:Type} {a_WT:WhyType a}, a -> (set a) -> Prop.
-intros a a_WT x s.
-exact (s x).
-Defined.
+(* Why3 assumption *)
+Definition mem {a:Type} {a_WT:WhyType a} (x:a) (s:(a -> bool)): Prop := ((s
+  x) = true).
 
 Hint Unfold mem.
 
 (* Why3 assumption *)
-Definition infix_eqeq {a:Type} {a_WT:WhyType a} (s1:(set a)) (s2:(set
-  a)): Prop := forall (x:a), (mem x s1) <-> (mem x s2).
+Definition infix_eqeq {a:Type} {a_WT:WhyType a} (s1:(a -> bool)) (s2:(a ->
+  bool)): Prop := forall (x:a), (mem x s1) <-> (mem x s2).
 
 Notation "x == y" := (infix_eqeq x y) (at level 70, no associativity).
 
 (* Why3 goal *)
-Lemma extensionality : forall {a:Type} {a_WT:WhyType a}, forall (s1:(set a))
-  (s2:(set a)), (infix_eqeq s1 s2) -> (s1 = s2).
+Lemma extensionality : forall {a:Type} {a_WT:WhyType a}, forall (s1:(a ->
+  bool)) (s2:(a -> bool)), (infix_eqeq s1 s2) -> (s1 = s2).
 Proof.
 intros a a_WT s1 s2 h1.
-now apply predicate_extensionality.
+apply predicate_extensionality.
+intros x.
+generalize (h1 x).
+unfold mem.
+intros [h2 h3].
+destruct (s1 x).
+now rewrite h2.
+destruct (s2 x).
+now apply h3.
+easy.
 Qed.
 
 (* Why3 assumption *)
-Definition subset {a:Type} {a_WT:WhyType a} (s1:(set a)) (s2:(set
-  a)): Prop := forall (x:a), (mem x s1) -> (mem x s2).
+Definition subset {a:Type} {a_WT:WhyType a} (s1:(a -> bool)) (s2:(a ->
+  bool)): Prop := forall (x:a), (mem x s1) -> (mem x s2).
 
 (* Why3 goal *)
-Lemma subset_refl : forall {a:Type} {a_WT:WhyType a}, forall (s:(set a)),
+Lemma subset_refl : forall {a:Type} {a_WT:WhyType a}, forall (s:(a -> bool)),
   (subset s s).
 Proof.
 now intros a a_WT s x.
 Qed.
 
 (* Why3 goal *)
-Lemma subset_trans : forall {a:Type} {a_WT:WhyType a}, forall (s1:(set a))
-  (s2:(set a)) (s3:(set a)), (subset s1 s2) -> ((subset s2 s3) -> (subset s1
-  s3)).
+Lemma subset_trans : forall {a:Type} {a_WT:WhyType a}, forall (s1:(a ->
+  bool)) (s2:(a -> bool)) (s3:(a -> bool)), (subset s1 s2) -> ((subset s2
+  s3) -> (subset s1 s3)).
 Proof.
 intros a a_WT s1 s2 s3 h1 h2 x H.
 now apply h2, h1.
 Qed.
 
-(* Why3 goal *)
-Definition empty: forall {a:Type} {a_WT:WhyType a}, (set a).
-intros.
-exact (fun _ => False).
-Defined.
-
 (* Why3 assumption *)
-Definition is_empty {a:Type} {a_WT:WhyType a} (s:(set a)): Prop :=
+Definition is_empty {a:Type} {a_WT:WhyType a} (s:(a -> bool)): Prop :=
   forall (x:a), ~ (mem x s).
 
 (* Why3 goal *)
-Lemma empty_def1 : forall {a:Type} {a_WT:WhyType a}, (is_empty (empty : (set
-  a))).
+Lemma mem_empty : forall {a:Type} {a_WT:WhyType a}, (is_empty
+  (map.Const.const false: (a -> bool))).
 Proof.
 now intros a a_WT x.
 Qed.
 
 (* Why3 goal *)
-Lemma mem_empty : forall {a:Type} {a_WT:WhyType a}, forall (x:a), ~ (mem x
-  (empty : (set a))).
-Proof.
-now intros a a_WT x.
-Qed.
-
-(* Why3 goal *)
-Definition add: forall {a:Type} {a_WT:WhyType a}, a -> (set a) -> (set a).
-intros 
+Lemma add_spec : forall {a:Type} {a_WT:WhyType a}, forall (x:a) (s:(a ->
+  bool)), forall (y:a), (mem y (map.Map.set s x true)) <-> ((y = x) \/ (mem y
+  s)).