(* This file is generated by Why3's Coq driver *)
(* Beware! Only edit allowed sections below    *)
Require Import BuiltIn.
Require BuiltIn.
Require int.Int.

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

Axiom map : forall (a:Type) {a_WT:WhyType a} (b:Type) {b_WT:WhyType b}, Type.
Parameter map_WhyType : forall (a:Type) {a_WT:WhyType a}
  (b:Type) {b_WT:WhyType b}, WhyType (map a b).
Existing Instance map_WhyType.

Parameter get: forall {a:Type} {a_WT:WhyType a} {b:Type} {b_WT:WhyType b},
  (map a b) -> a -> b.

Parameter set: forall {a:Type} {a_WT:WhyType a} {b:Type} {b_WT:WhyType b},
  (map a b) -> a -> b -> (map a b).

Axiom 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).

Axiom 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)).

Parameter const: forall {a:Type} {a_WT:WhyType a} {b:Type} {b_WT:WhyType b},
  b -> (map a b).

Axiom Const : forall {a:Type} {a_WT:WhyType a} {b:Type} {b_WT:WhyType b},
  forall (b1:b) (a1:a), ((get (const b1:(map a b)) a1) = b1).

(* Why3 assumption *)
Inductive array (a:Type) {a_WT:WhyType a} :=
  | mk_array : Z -> (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 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 get1 {a:Type} {a_WT:WhyType a}(a1:(array a)) (i:Z): a :=
  (get (elts a1) i).

(* Why3 assumption *)
Definition set1 {a:Type} {a_WT:WhyType a}(a1:(array a)) (i:Z) (v:a): (array
  a) := (mk_array (length a1) (set (elts a1) i v)).

(* Why3 assumption *)
Definition make {a:Type} {a_WT:WhyType a}(n:Z) (v:a): (array a) :=
  (mk_array n (const v:(map Z a))).

(* Why3 assumption *)
Definition array_bounded(a:(array Z)) (b:Z): Prop := forall (i:Z),
  ((0%Z <= i)%Z /\ (i < (length a))%Z) -> ((0%Z <= (get1 a i))%Z /\ ((get1 a
  i) < b)%Z).

(* Why3 assumption *)
Definition map_eq_sub {a:Type} {a_WT:WhyType a}(a1:(map Z a)) (a2:(map Z a))
  (l:Z) (u:Z): Prop := forall (i:Z), ((l <= i)%Z /\ (i < u)%Z) -> ((get a1
  i) = (get a2 i)).

(* Why3 assumption *)
Definition exchange {a:Type} {a_WT:WhyType a}(a1:(map Z a)) (a2:(map Z a))
  (i:Z) (j:Z): Prop := ((get a1 i) = (get a2 j)) /\ (((get a2 i) = (get a1
  j)) /\ forall (k:Z), ((~ (k = i)) /\ ~ (k = j)) -> ((get a1 k) = (get a2
  k))).

Axiom exchange_set : forall {a:Type} {a_WT:WhyType a}, forall (a1:(map Z a)),
  forall (i:Z) (j:Z), (exchange a1 (set (set a1 i (get a1 j)) j (get a1 i)) i
  j).

(* Why3 assumption *)
Inductive permut_sub{a:Type} {a_WT:WhyType a}  : (map Z a) -> (map Z a) -> Z
  -> Z -> Prop :=
  | permut_refl : forall (a1:(map Z a)) (a2:(map Z a)), forall (l:Z) (u:Z),
      (map_eq_sub a1 a2 l u) -> (permut_sub a1 a2 l u)
  | permut_sym : forall (a1:(map Z a)) (a2:(map Z a)), forall (l:Z) (u:Z),
      (permut_sub a1 a2 l u) -> (permut_sub a2 a1 l u)
  | permut_trans : forall (a1:(map Z a)) (a2:(map Z a)) (a3:(map Z a)),
      forall (l:Z) (u:Z), (permut_sub a1 a2 l u) -> ((permut_sub a2 a3 l
      u) -> (permut_sub a1 a3 l u))
  | permut_exchange : forall (a1:(map Z a)) (a2:(map Z a)), forall (l:Z)
      (u:Z) (i:Z) (j:Z), ((l <= i)%Z /\ (i < u)%Z) -> (((l <= j)%Z /\
      (j < u)%Z) -> ((exchange a1 a2 i j) -> (permut_sub a1 a2 l u))).

Axiom permut_weakening : forall {a:Type} {a_WT:WhyType a}, forall (a1:(map Z
  a)) (a2:(map Z a)), forall (l1:Z) (r1:Z) (l2:Z) (r2:Z), (((l1 <= l2)%Z /\
  (l2 <= r2)%Z) /\ (r2 <= r1)%Z) -> ((permut_sub a1 a2 l2 r2) ->
  (permut_sub a1 a2 l1 r1)).

Axiom permut_eq : forall {a:Type} {a_WT:WhyType a}, forall (a1:(map Z a))
  (a2:(map Z a)), forall (l:Z) (u:Z), (permut_sub a1 a2 l u) -> forall (i:Z),
  ((i < l)%Z \/ (u <= i)%Z) -> ((get a2 i) = (get a1 i)).

Axiom permut_exists : forall {a:Type} {a_WT:WhyType a}, forall (a1:(map Z a))
  (a2:(map Z a)), forall (l:Z) (u:Z), (permut_sub a1 a2 l u) -> forall (i:Z),
  ((l <= i)%Z /\ (i < u)%Z) -> exists j:Z, ((l <= j)%Z /\ (j < u)%Z) /\
  ((get a2 i) = (get a1 j)).

(* Why3 assumption *)
Definition exchange1 {a:Type} {a_WT:WhyType a}(a1:(array a)) (a2:(array a))
  (i:Z) (j:Z): Prop := (exchange (elts a1) (elts a2) i j).

(* Why3 assumption *)
Definition permut_sub1 {a:Type} {a_WT:WhyType a}(a1:(array a)) (a2:(array a))
  (l:Z) (u:Z): Prop := (permut_sub (elts a1) (elts a2) l u).

(* Why3 assumption *)
Definition permut {a:Type} {a_WT:WhyType a}(a1:(array a)) (a2:(array
  a)): Prop := ((length a1) = (length a2)) /\ (permut_sub (elts a1) (elts a2)
  0%Z (length a1)).

Axiom exchange_permut : forall {a:Type} {a_WT:WhyType a}, forall (a1:(array
  a)) (a2:(array a)) (i:Z) (j:Z), (exchange1 a1 a2 i j) ->
  (((length a1) = (length a2)) -> (((0%Z <= i)%Z /\ (i < (length a1))%Z) ->
  (((0%Z <= j)%Z /\ (j < (length a1))%Z) -> (permut a1 a2)))).

Axiom permut_sym1 : forall {a:Type} {a_WT:WhyType a}, forall (a1:(array a))
  (a2:(array a)), (permut a1 a2) -> (permut a2 a1).

Axiom permut_trans1 : forall {a:Type} {a_WT:WhyType a}, forall (a1:(array a))
  (a2:(array a)) (a3:(array a)), (permut a1 a2) -> ((permut a2 a3) ->
  (permut a1 a3)).

(* Why3 assumption *)
Definition array_eq_sub {a:Type} {a_WT:WhyType a}(a1:(array a)) (a2:(array
  a)) (l:Z) (u:Z): Prop := (map_eq_sub (elts a1) (elts a2) l u).

(* Why3 assumption *)
Definition array_eq {a:Type} {a_WT:WhyType a}(a1:(array a)) (a2:(array
  a)): Prop := ((length a1) = (length a2)) /\ (array_eq_sub a1 a2 0%Z
  (length a1)).

Axiom array_eq_sub_permut : forall {a:Type} {a_WT:WhyType a},
  forall (a1:(array a)) (a2:(array a)) (l:Z) (u:Z), (array_eq_sub a1 a2 l
  u) -> (permut_sub1 a1 a2 l u).

Axiom array_eq_permut : forall {a:Type} {a_WT:WhyType a}, forall (a1:(array
  a)) (a2:(array a)), (array_eq a1 a2) -> (permut a1 a2).

Axiom permut_bounded : forall (a1:(array Z)) (a2:(array Z)) (n:Z),
  ((permut a1 a2) /\ (array_bounded a1 n)) -> (array_bounded a2 n).

(* Why3 assumption *)
Definition is_common_prefix(a:(array Z)) (x:Z) (y:Z) (l:Z): Prop :=
  (0%Z <= l)%Z /\ (((x + l)%Z <= (length a))%Z /\
  (((y + l)%Z <= (length a))%Z /\ forall (i:Z), ((0%Z <= i)%Z /\
  (i < l)%Z) -> ((get1 a (x + i)%Z) = (get1 a (y + i)%Z)))).

Axiom common_prefix_eq : forall (a:(array Z)) (x:Z), ((0%Z <= x)%Z /\
  (x < (length a))%Z) -> (is_common_prefix a x x ((length a) - x)%Z).

Axiom common_prefix_eq2 : forall (a:(array Z)) (x:Z), ((0%Z <= x)%Z /\
  (x < (length a))%Z) -> ~ (is_common_prefix a x x
  (((length a) - x)%Z + 1%Z)%Z).

Axiom not_common_prefix_if_last_different : forall (a:(array Z)) (x:Z) (y:Z)
  (l:Z), ((0%Z < l)%Z /\ (((x + l)%Z < (length a))%Z /\
  (((y + l)%Z < (length a))%Z /\ ~ ((get1 a (x + (l - 1%Z)%Z)%Z) = (get1 a
  (y + (l - 1%Z)%Z)%Z))))) -> ~ (is_common_prefix a x y l).

Parameter longest_common_prefix: (array Z) -> Z -> Z -> Z.

Axiom lcp_spec : forall (a:(array Z)) (x:Z) (y:Z) (l:Z), (((0%Z <= x)%Z /\
  (x < (length a))%Z) /\ ((0%Z <= y)%Z /\ (y < (length a))%Z)) ->
  ((l = (longest_common_prefix a x y)) <-> ((is_common_prefix a x y l) /\
  ~ (is_common_prefix a x y (l + 1%Z)%Z))).

Axiom lcp_is_cp : forall (a:(array Z)) (x:Z) (y:Z), (((0%Z <= x)%Z /\
  (x < (length a))%Z) /\ ((0%Z <= y)%Z /\ (y < (length a))%Z)) ->
  (is_common_prefix a x y (longest_common_prefix a x y)).

Axiom lcp_eq : forall (a:(array Z)) (x:Z) (y:Z), (((0%Z <= x)%Z /\
  (x < (length a))%Z) /\ ((0%Z <= y)%Z /\ (y < (length a))%Z)) ->
  forall (i:Z), ((0%Z <= i)%Z /\ (i < (longest_common_prefix a x y))%Z) ->
  ((get1 a (x + i)%Z) = (get1 a (y + i)%Z)).

Axiom lcp_refl : forall (a:(array Z)) (x:Z), ((0%Z <= x)%Z /\
  (x < (length a))%Z) -> ((longest_common_prefix a x
  x) = ((length a) - x)%Z).

(* 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 *)
Definition le(a:(array Z)) (x:Z) (y:Z): Prop := let n := (length a) in
  (((0%Z <= x)%Z /\ (x < n)%Z) /\ (((0%Z <= y)%Z /\ (y < n)%Z) /\ let l :=
  (longest_common_prefix a x y) in (((x + l)%Z = n) \/ (((x + l)%Z < n)%Z /\
  (((y + l)%Z < n)%Z /\ ((get1 a (x + l)%Z) <= (get1 a (y + l)%Z))%Z))))).

Axiom le_refl : forall (a:(array Z)) (x:Z), ((0%Z <= x)%Z /\
  (x < (length a))%Z) -> (le a x x).

Axiom le_trans : forall (a:(array Z)) (x:Z) (y:Z) (z:Z), (((0%Z <= x)%Z /\
  (x < (length a))%Z) /\ (((0%Z <= y)%Z /\ (y < (length a))%Z) /\
  (((0%Z <= z)%Z /\ (z < (length a))%Z) /\ ((le a x y) /\ (le a y z))))) ->
  (le a x z).

(* Why3 assumption *)
Definition sorted_sub(a:(array Z)) (data:(array Z)) (l:Z) (u:Z): Prop :=
  forall (i1:Z) (i2:Z), (((l <= i1)%Z /\ (i1 <= i2)%Z) /\ (i2 < u)%Z) ->
  (le a (get1 data i1) (get1 data i2)).

Axiom sorted_bounded : forall (a:(array Z)) (data:(array Z)) (l:Z) (u:Z)
  (i:Z), (((l <= i)%Z /\ (i < u)%Z) /\ (sorted_sub a data l u)) ->
  ((0%Z <= (get1 data i))%Z /\ ((get1 data i) < (length a))%Z).

Axiom sorted_le : forall (a:(array Z)) (data:(array Z)) (l:Z) (u:Z) (i:Z)
  (x:Z), (((l <= i)%Z /\ (i < u)%Z) /\ ((sorted_sub a data l u) /\ (le a x
  (get1 data l)))) -> (le a x (get1 data i)).

Axiom sorted_ge : forall (a:(array Z)) (data:(array Z)) (l:Z) (u:Z) (i:Z)
  (x:Z), ((sorted_sub a data l u) /\ ((le a (get1 data (u - 1%Z)%Z) x) /\
  ((l <= i)%Z /\ (i < u)%Z))) -> (le a (get1 data i) x).

Axiom sorted_sub_sub : forall (a:(array Z)) (data:(array Z)) (l:Z) (u:Z)
  (l':Z) (u':Z), ((l <= l')%Z /\ (u' <= u)%Z) -> ((sorted_sub a data l u) ->
  (sorted_sub a data l' u')).

Axiom sorted_sub_add : forall (a:(array Z)) (data:(array Z)) (l:Z) (u:Z),
  ((sorted_sub a data (l + 1%Z)%Z u) /\ (le a (get1 data l) (get1 data
  (l + 1%Z)%Z))) -> (sorted_sub a data l u).

Axiom sorted_sub_concat : forall (a:(array Z)) (data:(array Z)) (l:Z) (m:Z)
  (u:Z), (((l <= m)%Z /\ (m <= u)%Z) /\ ((sorted_sub a data l m) /\
  ((sorted_sub a data m u) /\ (le a (get1 data (m - 1%Z)%Z) (get1 data
  m))))) -> (sorted_sub a data l u).

Axiom sorted_sub_set : forall (a:(array Z)) (data:(array Z)) (l:Z) (u:Z)
  (i:Z) (v:Z), ((sorted_sub a data l u) /\ (u <= i)%Z) -> (sorted_sub a
  (set1 data i v) l u).

Axiom sorted_sub_set2 : forall (a:(array Z)) (data:(array Z)) (l:Z) (u:Z)
  (i:Z) (v:Z), ((sorted_sub a data l u) /\ (u <= i)%Z) -> (sorted_sub a
  (mk_array (length a) (set (elts data) i v)) l u).

(* Why3 assumption *)
Definition sorted(a:(array Z)) (data:(array Z)): Prop := (sorted_sub a data
  0%Z (length data)).

Require Import Why3.
Ltac ae := why3 "alt-ergo" timelimit 3.

(* Why3 goal *)
Theorem WP_parameter_sort : forall (a:Z) (data:Z), forall (data1:(map Z Z))
  (a1:(map Z Z)), let data2 := (mk_array data data1) in let a2 := (mk_array a
  a1) in ((array_bounded data2 a) -> ((0%Z <= (data - 1%Z)%Z)%Z ->
  forall (data3:(map Z Z)), let data4 := (mk_array data data3) in
  forall (i:Z), ((0%Z <= i)%Z /\ (i <= (data - 1%Z)%Z)%Z) -> ((((permut data2
  data4) /\ (sorted_sub a2 data4 0%Z i)) /\ (array_bounded data4 a)) ->
  forall (j:Z) (data5:(map Z Z)), let data6 := (mk_array data data5) in
  ((((((((0%Z <= j)%Z /\ (j <= i)%Z) /\ (permut data2 data6)) /\
  (sorted_sub a2 data6 0%Z j)) /\ (sorted_sub a2 data6 j (i + 1%Z)%Z)) /\
  forall (k1:Z) (k2:Z), (((0%Z <= k1)%Z /\ (k1 < j)%Z) /\
  (((j + 1%Z)%Z <= k2)%Z /\ (k2 <= i)%Z)) -> (le a2 (get data5 k1) (get data5
  k2))) /\ (array_bounded data6 a)) -> ((0%Z < j)%Z -> (((0%Z <= j)%Z /\
  (j < data)%Z) -> let o := (get data5 j) in (((0%Z <= (j - 1%Z)%Z)%Z /\
  ((j - 1%Z)%Z < data)%Z) -> let o1 := (get data5 (j - 1%Z)%Z) in
  ((((0%Z <= o1)%Z /\ (o1 < a)%Z) /\ ((0%Z <= o)%Z /\ (o < a)%Z)) ->
  forall (o2:Z), ((((o2 = 0%Z) -> (o1 = o)) /\ ((o2 < 0%Z)%Z -> (le a2 o1
  o))) /\ ((0%Z < o2)%Z -> (le a2 o o1))) -> ((0%Z < o2)%Z -> ((le a2
  (get data5 j) (get data5 (j - 1%Z)%Z)) -> (((0%Z <= j)%Z /\
  (j < data)%Z) -> ((sorted_sub a2 data6 0%Z (j - 1%Z)%Z) ->
  (((0%Z <= (j - 1%Z)%Z)%Z /\ ((j - 1%Z)%Z < data)%Z) -> (((0%Z <= j)%Z /\
  (j < data)%Z) -> forall (data7:(map Z Z)), (data7 = (set data5 j (get data5
  (j - 1%Z)%Z))) -> ((sorted_sub a2 (mk_array data data7) 0%Z (j - 1%Z)%Z) ->
  (((0%Z <= (j - 1%Z)%Z)%Z /\ ((j - 1%Z)%Z < data)%Z) -> forall (data8:(map Z
  Z)), (data8 = (set data7 (j - 1%Z)%Z (get data5 j))) -> ((le a2 (get data8
  (j - 1%Z)%Z) (get data8 j)) -> ((forall (k:Z), ((j <= k)%Z /\
  (k <= i)%Z) -> (le a2 (get data8 j) (get data8 k))) -> ((exchange data5
  data8 (j - 1%Z)%Z j) -> (sorted_sub a2 (mk_array data data8) 0%Z
  (j - 1%Z)%Z)))))))))))))))))))).
intros a data data1 a1 data2 a2 h1 h2 data3 data4 i (h3,h4) ((h5,h6),h7) j
data5 data6 ((((((h8,h9),h10),h11),h12),h13),h14) h15 (h16,h17) o (h18,h19)
o1 ((h20,h21),(h22,h23)) o2 ((h24,h25),h26) h27 h28 (h29,h30) h31 (h32,h33)
(h34,h35) data7 h36 h37 (h38,h39) data8 h40 h41 h42 h43.
red; red in h37.
unfold get1 in h37 |- *.
simpl in *.
ae.
Qed.