Library quicksort3_QuickSort_WP_parameter_quick_sort1_1

Require Import BuiltIn.
Require BuiltIn.
Require int.Int.
Require map.Map.
Require map.MapPermut.

Definition unit := unit.

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]].

Definition contents {a:Type} {a_WT:WhyType a} (v:(ref a)): a :=
  match v with
  | (mk_ref x) => x
  end.

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]].

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.

Definition length {a:Type} {a_WT:WhyType a} (v:(array a)): Z :=
  match v with
  | (mk_array x x1) => x
  end.

Definition get {a:Type} {a_WT:WhyType a} (a1:(array a)) (i:Z): a :=
  (map.Map.get (elts a1) i).

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 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 sorted_sub (a:(map.Map.map Z Z)) (l:Z) (u:Z): Prop :=
  forall (i1:Z) (i2:Z), (((l <= i1)%Z /\ (i1 <= i2)%Z) /\ (i2 < u)%Z) ->
  ((map.Map.get a i1) <= (map.Map.get a i2))%Z.

Definition sorted_sub1 (a:(array Z)) (l:Z) (u:Z): Prop := (sorted_sub
  (elts a) l u).

Definition sorted (a:(array Z)): Prop := (sorted_sub (elts a) 0%Z
  (length a)).

Definition exchange {a:Type} {a_WT:WhyType a} (a1:(array a)) (a2:(array a))
  (i:Z) (j:Z): Prop := (map.MapPermut.exchange (elts a1) (elts a2) i j).

Definition permut_sub {a:Type} {a_WT:WhyType a} (a1:(array a)) (a2:(array a))
  (l:Z) (u:Z): Prop := (map.MapPermut.permut_sub (elts a1) (elts a2) l u).

Definition permut {a:Type} {a_WT:WhyType a} (a1:(array a)) (a2:(array
  a)): Prop := ((length a1) = (length a2)) /\ (map.MapPermut.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), (exchange 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_sym : forall {a:Type} {a_WT:WhyType a}, forall (a1:(array a))
  (a2:(array a)), (permut a1 a2) -> (permut a2 a1).

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

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

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

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

Definition div_sub (a:(array Z)) (l:Z) (m:Z) (u:Z): Prop := (forall (i:Z),
  ((l <= i)%Z /\ (i < m)%Z) -> ((get a i) <= (get a m))%Z) /\ forall (j:Z),
  (((m + 1%Z)%Z <= j)%Z /\ (j < u)%Z) -> ((get a m) <= (get a j))%Z.

Axiom sorted_div_sorted_sub : forall (a:(array Z)), forall (l:Z) (m:Z) (u:Z),
  (sorted_sub1 a l m) -> ((div_sub a l m u) -> ((sorted_sub1 a (m + 1%Z)%Z
  u) -> (sorted_sub1 a l u))).

Require Import ssreflect.
Ltac compress :=
  repeat (match goal with [H1: ?A, H2: ?A |- _] => clear H2 end).

Lemma losorted_hipermut_losorted (a1 a2: Map.map int int) (l m u: int) :
  sorted_sub a1 l (m-1) -> MapPermut.permut_sub a1 a2 m u -> sorted_sub a2 l (m-1).
Proof.
 move=> a1_losorted a1_hipermut.
 unfold sorted_sub => l1 l2 [[hll1 hl1l2] l2m].
 rewrite !(MapPermut.permut_eq a1 a2 m u); [ | |omega | | omega].
 - by apply a1_losorted; [omega].
 - exact a1_hipermut.
 - exact a1_hipermut.
Qed.

Lemma sorted_array_to_sorted_map (a1: array int) (a2: Map.map int int):
  forall l u: int, a2 = elts a1 -> sorted_sub1 a1 l u = sorted_sub a2 l u.
Proof.
 move=> l u eq.
 unfold sorted_sub1.
 by rewrite eq //.
Qed.

Theorem WP_parameter_quick_sort1 : forall (a:Z) (lo:Z) (hi:Z),
  forall (a1:(map.Map.map Z Z)), ((0%Z <= a)%Z /\ (((0%Z <= lo)%Z /\
  (lo <= a)%Z) /\ ((0%Z <= hi)%Z /\ (hi <= a)%Z))) ->
  ((lo < (hi - 1%Z)%Z)%Z -> (((lo + 1%Z)%Z <= (hi - 1%Z)%Z)%Z -> forall (i:Z)
  (a2:(map.Map.map Z Z)), (((((lo < i)%Z /\
  (i <= ((hi - 1%Z)%Z + 1%Z)%Z)%Z) /\ forall (k:Z), (((lo + 1%Z)%Z <= k)%Z /\
  (k < i)%Z) -> ((map.Map.get a2 k) <= (map.Map.get a2 lo))%Z) /\
  forall (k':Z), ((i <= k')%Z /\ (k' < ((hi - 1%Z)%Z + 1%Z)%Z)%Z) ->
  ((map.Map.get a2 lo) <= (map.Map.get a2 k'))%Z) /\
  (map.MapPermut.permut_sub a1 a2 (lo + 1%Z)%Z hi)) -> (((0%Z <= a)%Z /\
  (((0%Z <= lo)%Z /\ (lo < a)%Z) /\ ((0%Z <= (i - 1%Z)%Z)%Z /\
  ((i - 1%Z)%Z < a)%Z))) -> forall (a3:(map.Map.map Z Z)), ((0%Z <= a)%Z /\
  (map.MapPermut.exchange a2 a3 lo (i - 1%Z)%Z)) -> ((div_sub (mk_array a a3)
  lo (i - 1%Z)%Z hi) -> ((((0%Z <= lo)%Z /\ (lo <= a)%Z) /\
  ((0%Z <= (i - 1%Z)%Z)%Z /\ ((i - 1%Z)%Z <= a)%Z)) ->
  forall (a4:(map.Map.map Z Z)), ((0%Z <= a)%Z /\ ((sorted_sub a4 lo
  (i - 1%Z)%Z) /\ (map.MapPermut.permut_sub a3 a4 lo (i - 1%Z)%Z))) ->
  ((((0%Z <= i)%Z /\ (i <= a)%Z) /\ ((0%Z <= hi)%Z /\ (hi <= a)%Z)) ->
  forall (a5:(map.Map.map Z Z)), ((0%Z <= a)%Z /\ ((sorted_sub a5 i hi) /\
  (map.MapPermut.permut_sub a4 a5 i hi))) -> ((div_sub (mk_array a a5) lo
  (i - 1%Z)%Z hi) -> (sorted_sub a5 lo hi)))))))).

move=> a lo hi a1 [h1 [[h2 h3] [h4 h5]]] h6 h7 i a2 [[[[h8 h9] h10]
h11] a1_to_a2] [h13 [[h14 h15] [h16 h17]]] a3 [h18 a2_to_a3] h20 [[h21
h22] [h23 h24]] a4 [h25 [a4_losorted a3_to_a4]] [[h28 h29] [h30 h31]]
a5 [h32 [a5_hisorted a4_hipermut]] a5_div; compress.

pose m5 := mk_array (hi-lo) a5.
rewrite -(sorted_array_to_sorted_map m5 a5) //=.
apply (sorted_div_sorted_sub m5 lo (i-1) hi).
- rewrite (sorted_array_to_sorted_map m5 a5) //=.
  apply (losorted_hipermut_losorted a4 a5 lo i hi).
  + exact a4_losorted.
  + exact a4_hipermut.
- exact a5_div.
- rewrite Z.sub_add.
  rewrite (sorted_array_to_sorted_map m5 a5); [ | reflexivity].
  exact a5_hisorted.
Qed.