Verifying insertion sort with Why3.

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

(* Why3 assumption *)
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.
Arguments mk_ref {a}.

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

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

Parameter length: forall {a:Type} {a_WT:WhyType a}, (array a) -> 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:Z) : a :=
  (elts a1) i.

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

Axiom mixfix_lblsmnrb_spec :
  forall {a:Type} {a_WT:WhyType a},
  forall (a1:array a) (i:Z) (v:a),
  ((length (mixfix_lblsmnrb a1 i v)) = (length a1)) /\
  ((elts (mixfix_lblsmnrb a1 i v)) = (map.Map.set (elts a1) i v)).

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

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

(* Why3 assumption *)
Definition sorted (a:array Z) : Prop :=
  forall (i:Z) (j:Z), ((0%Z <= i)%Z /\ ((i <= j)%Z /\ (j < (length a))%Z)) ->
  ((mixfix_lbrb a i) <= (mixfix_lbrb a j))%Z.

Parameter a: array Z.

Axiom H : (1%Z <= (((length a) - 1%Z)%Z + 1%Z)%Z)%Z.

Parameter a1: array Z.

Axiom H1 : ((length a1) = (length a)).

Parameter i: Z.

Axiom H2 : (1%Z <= i)%Z.

Axiom H3 : (i <= ((length a) - 1%Z)%Z)%Z.

Axiom H4 :
  forall (k:Z) (l:Z), ((0%Z <= k)%Z /\ ((k <= l)%Z /\ (l < i)%Z)) ->
  ((mixfix_lbrb a1 k) <= (mixfix_lbrb a1 l))%Z.

Axiom H5 : (0%Z < i)%Z /\ (i < (length a1))%Z.

Parameter j: Z.

Parameter a2: array Z.

Axiom H6 : ((length a2) = (length a1)).

Axiom H7 : (0%Z <= j)%Z.

Axiom H8 : (j <= (i - 1%Z)%Z)%Z.

Axiom H9 :
  forall (k:Z) (l:Z),
  ((0%Z <= k)%Z /\ ((k <= l)%Z /\ (l < (j - 1%Z)%Z)%Z)) ->
  ((mixfix_lbrb a2 k) <= (mixfix_lbrb a2 l))%Z.

Axiom H10 :
  forall (k:Z) (l:Z), ((j < k)%Z /\ ((k <= l)%Z /\ (l < i)%Z)) ->
  ((mixfix_lbrb a2 k) <= (mixfix_lbrb a2 l))%Z.

Axiom H11 :
  forall (k:Z), ((j < k)%Z /\ (k < (i - 1%Z)%Z)%Z) ->
  ((mixfix_lbrb a1 i) <= (mixfix_lbrb a2 k))%Z.

Axiom H12 : (0%Z < j)%Z.

Axiom H13 : ((mixfix_lbrb a1 i) < (mixfix_lbrb a2 j))%Z.

Parameter a3: array Z.

Axiom H14 : ((length a3) = (length a2)).

Axiom H15 :
  ((elts a3) = (map.Map.set (elts a2) (j + 1%Z)%Z (mixfix_lbrb a2 j))).

Axiom H16 : (a3 = (mixfix_lblsmnrb a2 (j + 1%Z)%Z (mixfix_lbrb a2 j))).

Parameter j1: Z.

Axiom H17 : (j1 = (j - 1%Z)%Z).

Axiom H18 : (0%Z <= j1)%Z /\ (j1 <= (i - 1%Z)%Z)%Z.

Parameter k: Z.

Parameter l: Z.

Axiom H19 : (0%Z <= k)%Z.

Axiom H20 : (k <= l)%Z.

Axiom H21 : (l < (j1 - 1%Z)%Z)%Z.

(* Why3 goal *)
Theorem VC_insert_sort : ((mixfix_lbrb a3 k) <= (mixfix_lbrb a3 l))%Z.
Proof.
unfold mixfix_lbrb.
rewrite H15.
pose (setk := Map.set_def (elts a2) (j + 1)%Z (mixfix_lbrb a2 j) k).
pose (l_lt_j1 := H21).
rewrite H17 in l_lt_j1.
pose (l_le_j := Z.lt_le_incl _ _ l_lt_j1).
pose (k_le_j := Int.Trans _ _ _ H20 l_le_j).
destruct setk as [_ case_k_ne_j].

rewrite Z.sub_1_r in k_le_j.
rewrite Z.sub_1_r in k_le_j.
pose (k_le_j1 := Z.le_pred_lt k (Z.pred j) k_le_j).
pose (k_le_j2 := Z.le_pred_lt k j k_le_j1).

rewrite Z.add_1_r in case_k_ne_j.
pose (elts_a2_k := case_k_ne_j (fun k_eq_sj => let sj_le_j := eq_ind k (fun k => (k <= j)%Z) k_le_j2 _ k_eq_sj in Znot_le_succ j sj_le_j)).
rewrite Z.add_1_r.
rewrite elts_a2_k.

pose (setk := Map.set_def (elts a2) (Z.succ j) (mixfix_lbrb a2 j) l).

pose (l_lt_jmm := H21).
rewrite Z.sub_1_r in l_lt_jmm.
rewrite H17 in l_lt_jmm.
rewrite Z.sub_1_r in l_lt_jmm.
pose (l_lt_jm := Z.lt_pred_lt l (Z.pred j) l_lt_jmm).
pose (l_lt_j := Z.lt_pred_lt l j l_lt_jm).

destruct setk as [_ case_l_ne_j].
pose (elts_a2_l := case_l_ne_j (fun l_eq_sj => let sj_lt_j := eq_ind l (fun l => (l < j)%Z) l_lt_j _ l_eq_sj in Z.nlt_succ_diag_l j sj_lt_j)).
rewrite elts_a2_l.

pose (h9 := H9).
unfold mixfix_lbrb in h9.
refine (h9 k l (conj _ _)).
exact H19.

refine (conj H20 _).
rewrite Z.sub_1_r.
exact l_lt_jm.

Qed.