# Library msort_MergeSort_map_bitonic_incr_1

Require Import BuiltIn.
Require BuiltIn.
Require int.Int.
Require int.Abs.
Require int.EuclideanDivision.
Require int.Div2.
Require map.Map.
Require map.Occ.
Require map.MapPermut.

Definition unit := unit.

Axiom qtmark : Type.
Parameter qtmark_WhyType : WhyType qtmark.
Existing Instance qtmark_WhyType.

Inductive ref (a:Type) :=
| 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]].

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

Inductive array (a:Type) :=
| 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]].

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 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 := ((length a1) = (length a2)) /\ (((0%Z <= l)%Z /\
(l <= (length a1))%Z) /\ (((0%Z <= u)%Z /\ (u <= (length a1))%Z) /\
(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)) /\ (map_eq_sub (elts a1) (elts a2)
0%Z (length a1)).

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

Axiom exchange_set : forall {a:Type} {a_WT:WhyType a},
forall (a1:(map.Map.map Z a)) (l:Z) (u:Z) (i:Z) (j:Z), ((l <= i)%Z /\
(i < u)%Z) -> (((l <= j)%Z /\ (j < u)%Z) -> (exchange a1
(map.Map.set (map.Map.set a1 i (map.Map.get a1 j)) j (map.Map.get a1 i)) l
u i j)).

Definition exchange1 {a:Type} {a_WT:WhyType a} (a1:(array a)) (a2:(array a))
(i:Z) (j:Z): Prop := ((length a1) = (length a2)) /\ (exchange (elts a1)
(elts a2) 0%Z (length a1) i j).

Definition permut {a:Type} {a_WT:WhyType a} (a1:(array a)) (a2:(array a))
(l:Z) (u:Z): Prop := ((length a1) = (length a2)) /\ (((0%Z <= l)%Z /\
(l <= (length a1))%Z) /\ (((0%Z <= u)%Z /\ (u <= (length a1))%Z) /\
(map.MapPermut.permut (elts a1) (elts a2) l u))).

Definition permut_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) 0%Z l) /\ ((permut a1
a2 l u) /\ (map_eq_sub (elts a1) (elts a2) u (length a1))).

Definition permut_all {a:Type} {a_WT:WhyType a} (a1:(array a)) (a2:(array
a)): Prop := ((length a1) = (length a2)) /\ (map.MapPermut.permut (elts a1)
(elts a2) 0%Z (length a1)).

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

Axiom permut_sub_weakening : forall {a:Type} {a_WT:WhyType a},
forall (a1:(array a)) (a2:(array a)) (l1:Z) (u1:Z) (l2:Z) (u2:Z),
(permut_sub a1 a2 l1 u1) -> (((0%Z <= l2)%Z /\ (l2 <= l1)%Z) ->
(((u1 <= u2)%Z /\ (u2 <= (length a1))%Z) -> (permut_sub a1 a2 l2 u2))).

Axiom exchange_permut_all : forall {a:Type} {a_WT:WhyType a},
forall (a1:(array a)) (a2:(array a)) (i:Z) (j:Z), (exchange1 a1 a2 i j) ->
(permut_all a1 a2).

Definition sorted_sub2 (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 map_eq_sub_rev_offset (a1:(map.Map.map Z Z)) (a2:(map.Map.map Z
Z)) (l:Z) (u:Z) (offset:Z): Prop := forall (i:Z), ((l <= i)%Z /\
(i < u)%Z) -> ((map.Map.get a1 i) = (map.Map.get a2
((((offset + l)%Z + u)%Z - 1%Z)%Z - i)%Z)).

Definition array_eq_sub_rev_offset (a1:(array Z)) (a2:(array Z)) (l:Z) (u:Z)
(offset:Z): Prop := (map_eq_sub_rev_offset (elts a1) (elts a2) l u offset).

Definition map_dsorted_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 i2) <= (map.Map.get a i1))%Z.

Definition dsorted_sub (a:(array Z)) (l:Z) (u:Z): Prop := (map_dsorted_sub
(elts a) l u).

Definition map_bitonic_sub (a:(map.Map.map Z Z)) (l:Z) (u:Z): Prop :=
(l < u)%Z -> exists i:Z, ((l <= i)%Z /\ (i <= u)%Z) /\ ((sorted_sub2 a l
i) /\ (map_dsorted_sub a i u)).

Definition bitonic (a:(array Z)) (l:Z) (u:Z): Prop := (map_bitonic_sub
(elts a) l u).

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

Lemma sorted_sub_weakening: forall (a:(map.Map.map Z Z)) (l:Z) (u:Z) (:Z)(:Z), (l <= )%Z -> ( <= u)%Z -> sorted_sub2 a l u -> sorted_sub2 a .
Proof.
move=> a l u Hl_le_l´ Hu´_le_u Hlu_sorted.
unfold sorted_sub2 => i1 i2 [Hl´_le_i1 Hi1_le_i2_lt_u´].
apply Hlu_sorted.
by omega.
Qed.

Lemma dsorted_sub_weakening: forall (a:(map.Map.map Z Z)) (l:Z) (u:Z) (:Z) (:Z), (l <= )%Z -> ( <= u)%Z -> map_dsorted_sub a l u -> map_dsorted_sub a .
Proof.
move=> a l u Hl_le_l´ Hu´_le_u Hlu_dsorted.
unfold map_dsorted_sub => i1 i2 [Hl´_le_i1 Hi1_le_i2_lt_u].
apply Hlu_dsorted.
by omega.
Qed.

Lemma sorted_sub_diag: forall (a:(map.Map.map Z Z)) (l:Z),
sorted_sub2 a l l.
Proof.
move=> a l.
unfold sorted_sub2 => i1 i2 [Hl_le_i1 Hi1_le_i2_lt_l].
have Hl_lt_l: (l < l)%Z.
- by omega.
by apply Zlt_irrefl in Hl_lt_l.
Qed.

Theorem map_bitonic_incr : forall (a:(map.Map.map Z Z)) (l:Z) (u:Z),
(map_bitonic_sub a l u) -> (map_bitonic_sub a (l + 1%Z)%Z u).

Proof.
move=> a l u Hlu_bitonic.
unfold map_bitonic_sub => Hl1_lt_u.
unfold map_bitonic_sub in Hlu_bitonic.
have Hl_lt_u: (l < u)%Z.
- by omega.
apply Hlu_bitonic in Hl_lt_u.
move: Hl_lt_u=> [j [Hl_le_j_le_u [Hlj_sorted Hju_dsorted]]].
move: Hl_le_j_le_u => [Hl_le_j Hj_le_u].
apply (Zle_lt_or_eq l j) in Hl_le_j.
case: Hl_le_j => [Hl_lt_j | Hl_eq_j].
- exists j.
split.
+ by omega.
+ split.
- apply (sorted_sub_weakening a l j).
+ by apply (Z.le_succ_diag_r).
+ reflexivity.
+ exact Hlj_sorted.
- exact Hju_dsorted.
- exists (l+1)%Z.
split.
+ by omega.
+ split.
- by apply sorted_sub_diag.
- apply (dsorted_sub_weakening a l u).
+ by omega.
+ by omega.
+ rewrite Hl_eq_j.
exact Hju_dsorted.
Qed.