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

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

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 Hll´ Huu´ Hlu_sorted.
unfold sorted_sub2 => i1 i2 [Hl1i1i2 Hi2u].
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 Hll´ Huu´ Hlu_dsorted.
unfold map_dsorted_sub => i1 i2 [Hl1i1i2 Hi2u].
apply Hlu_dsorted.
by omega.
Qed.

Lemma sorted_sub_empty: forall (a:(map.Map.map Z Z)) (l:Z),
  sorted_sub2 a l l.
Proof.
move=> a l.
unfold sorted_sub2.
move=> i1 i2 [Hli1i2 Hi2l].
have Hfalse: (l < l)%Z.
- omega.
apply Zlt_irrefl in Hfalse.
inversion Hfalse.
Qed.

Lemma dsorted_sub_empty: forall (a:(map.Map.map Z Z)) (l:Z),
  map_dsorted_sub a l l.
Proof.
move=> a l.
unfold map_dsorted_sub.
move=> i1 i2 [Hli1i2 Hi2l].
have Hfalse: (l < l)%Z.
- omega.
apply Zlt_irrefl in Hfalse.
inversion Hfalse.
Qed.

Theorem map_bitonic_decr : forall (a:(map.Map.map Z Z)) (l:Z) (u:Z),
  (map_bitonic_sub a l u) -> (map_bitonic_sub a l (u - 1%Z)%Z).
Proof.
 move=> a l u Hlu_bitonic.
unfold map_bitonic_sub => Hlu1.
unfold map_bitonic_sub in Hlu_bitonic.
have Hlu: (l < u)%Z.
- by omega.
apply Hlu_bitonic in Hlu.
move: Hlu=> [j [Hlju [Hlj_sorted Hju_dsorted]]].
move: Hlju => [Hlj Hju].
apply (Zle_lt_or_eq j u) in Hju.
case: Hju => [Hj_lt_u | Hj_eq_u].
- exists j.
  split.
  + omega.
  + split.
    - exact Hlj_sorted.
    - apply (dsorted_sub_weakening a j u).
      + omega.
      + have H:(u <= u + 1)%Z.
        - by apply Z.le_succ_diag_r.
        omega.
      + exact Hju_dsorted.
- exists (u-1)%Z.
  split.
  + omega.
  + split.
    - apply (sorted_sub_weakening a l u).
      + omega.
      + omega.
      + rewrite - Hj_eq_u.
        exact Hlj_sorted.
    - by apply dsorted_sub_empty.
Qed.