why3/examples/stdlib/array/array_ArrayPermut_permut_sub_weakening_2.v

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

Axiom array : forall (a:Type), Type.
Parameter array_WhyType :
  forall (a:Type) {a_WT:WhyType a}, WhyType (array a).
Existing Instance array_WhyType.

Parameter elts:
  forall {a:Type} {a_WT:WhyType a}, array a -> Numbers.BinNums.Z -> a.

Parameter length:
  forall {a:Type} {a_WT:WhyType a}, array a -> Numbers.BinNums.Z.

Axiom array'invariant :
  forall {a:Type} {a_WT:WhyType a},
  forall (self:array a), (0%Z <= (length self))%Z.

(* Why3 assumption *)
Definition mixfix_lbrb {a:Type} {a_WT:WhyType a} (a1:array a)
    (i:Numbers.BinNums.Z) : a :=
  elts a1 i.

Parameter mixfix_lblsmnrb:
  forall {a:Type} {a_WT:WhyType a}, array a -> Numbers.BinNums.Z -> a ->
  array a.

Axiom mixfix_lblsmnrb'spec'0 :
  forall {a:Type} {a_WT:WhyType a},
  forall (a1:array a) (i:Numbers.BinNums.Z) (v:a),
  ((length (mixfix_lblsmnrb a1 i v)) = (length a1)).

Axiom mixfix_lblsmnrb'spec :
  forall {a:Type} {a_WT:WhyType a},
  forall (a1:array a) (i:Numbers.BinNums.Z) (v:a),
  ((elts (mixfix_lblsmnrb a1 i v)) = (map.Map.set (elts a1) i v)).

Parameter make:
  forall {a:Type} {a_WT:WhyType a}, Numbers.BinNums.Z -> a -> array a.

Axiom make_spec :
  forall {a:Type} {a_WT:WhyType a},
  forall (n:Numbers.BinNums.Z) (v:a), (0%Z <= n)%Z ->
  (forall (i:Numbers.BinNums.Z), (0%Z <= i)%Z /\ (i < n)%Z ->
   ((mixfix_lbrb (make n v) i) = v)) /\
  ((length (make n v)) = n).

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

(* Why3 assumption *)
Definition array_eq_sub {a:Type} {a_WT:WhyType a} (a1:array a) (a2:array a)
    (l:Numbers.BinNums.Z) (u:Numbers.BinNums.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.

(* Why3 assumption *)
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).

(* Why3 assumption *)
Definition exchange {a:Type} {a_WT:WhyType a} (a1:Numbers.BinNums.Z -> a)
    (a2:Numbers.BinNums.Z -> a) (l:Numbers.BinNums.Z) (u:Numbers.BinNums.Z)
    (i:Numbers.BinNums.Z) (j:Numbers.BinNums.Z) : Prop :=
  ((l <= i)%Z /\ (i < u)%Z) /\
  ((l <= j)%Z /\ (j < u)%Z) /\
  ((a1 i) = (a2 j)) /\
  ((a1 j) = (a2 i)) /\
  (forall (k:Numbers.BinNums.Z), (l <= k)%Z /\ (k < u)%Z -> ~ (k = i) ->
   ~ (k = j) -> ((a1 k) = (a2 k))).

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

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

(* Why3 assumption *)
Definition permut {a:Type} {a_WT:WhyType a} (a1:array a) (a2:array a)
    (l:Numbers.BinNums.Z) (u:Numbers.BinNums.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.

(* Why3 assumption *)
Definition permut_sub {a:Type} {a_WT:WhyType a} (a1:array a) (a2:array a)
    (l:Numbers.BinNums.Z) (u:Numbers.BinNums.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).

(* Why3 assumption *)
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:Numbers.BinNums.Z)
    (j:Numbers.BinNums.Z) (l:Numbers.BinNums.Z) (u:Numbers.BinNums.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_trans :
  forall {a:Type} {a_WT:WhyType a},
  forall (a1:array a) (a2:array a) (a3:array a) (l:Numbers.BinNums.Z)
    (u:Numbers.BinNums.Z),
  (0%Z <= l)%Z -> (u <= (length a1))%Z -> permut_sub a1 a2 l u ->
  permut_sub a2 a3 l u -> permut_sub a1 a3 l u.

(* Why3 goal *)
Theorem permut_sub_weakening {a:Type} {a_WT:WhyType a} :
  forall (a1:array a) (a2:array a) (l1:Numbers.BinNums.Z)
    (u1:Numbers.BinNums.Z) (l2:Numbers.BinNums.Z) (u2:Numbers.BinNums.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.
(* Why3 intros a1 a2 l1 u1 l2 u2 h1 (h2,h3) (h4,h5). *)
intros a1 a2 l1 u1 l2 u2 h1 (h2,h3) (h4,h5).
unfold permut_sub in *.
destruct h1 as (eql,(h1,eqr)).
unfold map_eq_sub in *.
split.
(* eq left *)
intros. apply eql; auto with zarith.
split.
(* permut *)
unfold permut in *.
destruct h1 as (h1,(h1a,(h1b,h1c))).
repeat split; try assumption. auto with zarith. auto with zarith.
unfold MapPermut.permut in *.
intros v.
generalize (Z_le_dec l1 u1); intros [c|c].
(* l1 <= u1 *)
assert (Occ.occ v (elts a1) l2 u2 = Occ.occ v (elts a1) l2 l1 + Occ.occ v (elts a1) l1 u2)%Z. 
  apply Occ.occ_append. auto with zarith.
assert (Occ.occ v (elts a1) l1 u2 = Occ.occ v (elts a1) l1 u1 + Occ.occ v (elts a1) u1 u2)%Z. 
  apply Occ.occ_append. auto with zarith.
assert (Occ.occ v (elts a2) l2 u2 = Occ.occ v (elts a2) l2 l1 + Occ.occ v (elts a2) l1 u2)%Z. 
  apply Occ.occ_append. auto with zarith.
assert (Occ.occ v (elts a2) l1 u2 = Occ.occ v (elts a2) l1 u1 + Occ.occ v (elts a2) u1 u2)%Z. 
  apply Occ.occ_append. auto with zarith.
assert (Occ.occ v (elts a1) l2 l1 = Occ.occ v (elts a2) l2 l1).
  apply Occ.occ_eq. intros; apply eql; auto with zarith.
assert (Occ.occ v (elts a1) u1 u2 = Occ.occ v (elts a2) u1 u2).
  apply Occ.occ_eq. intros; apply eqr; auto with zarith.
generalize (h1c v); auto with zarith.
(* u1 < l1 *)
apply Occ.occ_eq.
intros i hi.
generalize (Z_lt_dec i l1); intros [h|h].
apply eql; auto with zarith.
apply eqr; auto with zarith.
(* eq right *)
intros; apply eqr; auto with zarith.
Qed.