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) (l´:Z)(u´:Z),
(l <= l´)%Z -> (u´ <= u)%Z -> sorted_sub2 a l u -> sorted_sub2 a l´ u´.
Proof.
move=> a l u 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) (l´:Z) (u´:Z),
(l <= l´)%Z -> (u´ <= u)%Z -> map_dsorted_sub a l u -> map_dsorted_sub a l´ u´.
Proof.
move=> a l u 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.
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) (l´:Z)(u´:Z),
(l <= l´)%Z -> (u´ <= u)%Z -> sorted_sub2 a l u -> sorted_sub2 a l´ u´.
Proof.
move=> a l u 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) (l´:Z) (u´:Z),
(l <= l´)%Z -> (u´ <= u)%Z -> map_dsorted_sub a l u -> map_dsorted_sub a l´ u´.
Proof.
move=> a l u 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.