Commit 04d17bbf authored by François Bobot's avatar François Bobot

verifythis_PrefixSumRec completely proved

parent c989ee59
(*
VerifyThis @ FM2012: Problem 2
http://fm2012.verifythis.org/challenges
*)
module PrefixSumRec
use import int.Int
use import int.ComputerDivision
use import int.Power
use import array.Array
use import array.ArraySum
(** Shortcuts *)
function go_left (left right:int) : int =
let space = right - left in left - div space 2
lemma go_left_bounds:
forall left right:int.
0 <= left /\ left + 1 < right /\ right - left <= left ->
0 <= go_left left right < left
function go_right (left right:int) : int =
let space = right - left in right - div space 2
lemma go_right_bounds:
forall left right:int.
0 <= left /\ left + 1 < right /\ right - left <= left ->
left <= go_right left right < right
(** Needed for the proof of phase1_frame and phase1_frame2 *)
lemma Div_mod_2:
forall x:int. x >= 0 -> x >= 2 * div x 2 >= x-1
(** The step must be a power of 2 *)
predicate is_power_of_2 (x:int) = exists k:int. (k >= 0 /\ x = power 2 k)
(** Needed for proving is_power_of_2_1. Can it be added to the theory Power? *)
lemma is_power_of_2_0: forall k:int. k > 0 -> power 2 k = 2 * (power 2 (k-1))
lemma is_power_of_2_1: forall x:int. is_power_of_2 x -> x > 1 -> 2 * (div x 2) = x
(** Describe the result of the first function. The second function traverse the array in the same way
than the first function so it can use the ind uctive . *)
inductive phase1 (left:int) (right:int) (a0: array int) (a: array int) =
| Leaf : forall left right:int, a0 a : array int.
right = left + 1 ->
a[left] = a0[left] ->
phase1 left right a0 a
| Node : forall left right:int, a0 a : array int.
right > left + 1 ->
phase1 (go_left left right) left a0 a ->
phase1 (go_right left right) right a0 a ->
a[left] = sum a0 (left-(right-left)+1) (left+1) ->
phase1 left right a0 a
(** Frame properties of the inductive *)
lemma phase1_frame: (** forward *)
forall left right:int, a0 a a' : array int.
(forall i:int. left-(right-left) < i < right ->
a[i] = a'[i]) ->
phase1 left right a0 a -> phase1 left right a0 a'
lemma phase1_frame2: (** backward *)
forall left right:int, a0 a0' a : array int.
(forall i:int. left-(right-left) < i < right ->
a0[i] = a0'[i]) ->
phase1 left right a0 a -> phase1 left right a0' a
(** First function *)
let rec upsweep (left:int) (right:int) (a : array int) : unit =
{ 0 <= left < right < a.length /\ -1 <= left - (right - left) /\ is_power_of_2 (right - left) }
'Init:
let space = right - left in
if right > left+1 then
begin
upsweep (left - div space 2) left a;
upsweep (right - div space 2) right a;
assert { phase1 (left - div space 2) left (at a 'Init) a };
assert { phase1 (right - div space 2) right (at a 'Init) a };
assert { a[left] = sum (at a 'Init) (left-(right-left)+1) (left+1)};
assert { a[right] = sum (at a 'Init) (left+1) (right+1)}
end;
a[right] <- a[left] + a[right];
assert { right > left+1 -> phase1 (left - div space 2) left (at a 'Init) a };
assert { right > left+1 -> phase1 (right - div space 2) right (at a 'Init) a }
{
let space = right - left in
phase1 left right (old a) a /\
a[right] = sum (old a) (left-(right-left)+1) (right+1) /\
(forall i: int. i <= left-space -> a[i] = (old a)[i]) /\
(forall i: int. i > right -> a[i] = (old a)[i])
}
(** What we really want to prove *)
predicate partial_sum (left:int) (right:int) (a0 a : array int) =
forall i : int. (left-(right-left)) < i <= right -> a[i] = sum a0 0 i
(** BUG of why3ml? a0 can't be set as ghost: vty_value mismatch *)
let rec downsweep (left:int) (right:int) ((*ghost*) a0 : array int) (a : array int) : unit =
{ 0 <= left < right < a.length /\ -1 <= left - (right - left) /\
is_power_of_2 (right - left) /\
a[right] = sum a0 0 (left-(right-left) + 1) /\
phase1 left right a0 a
}
'Init:
let tmp = a[right] in
assert { a[right] = sum a0 0 (left-(right-left) + 1) };
assert { a[left] = sum a0 (left-(right-left)+1) (left+1) };
a[right] <- a[right] + a[left];
assert { a[right] = sum a0 0 (left + 1) };
a[left] <- tmp;
assert { a[right] = sum a0 0 (left + 1) };
if right > left+1 then
let space = right - left in
begin
assert { phase1 (go_left left right) left a0 (at a 'Init) };
assert { phase1 (go_right left right) right a0 (at a 'Init) };
assert { phase1 (go_right left right) right a0 a };
downsweep (left - div space 2) left a0 a;
assert { a[right] = sum a0 0 (left + 1) };
downsweep (right - div space 2) right a0 a;
assert { partial_sum (left - div space 2) left a0 a };
assert { partial_sum (right - div space 2) right a0 a }
end;
()
{
partial_sum left right a0 a /\
(forall i: int. i <= left-(right-left) -> a[i] = (old a)[i]) /\
(forall i: int. i > right -> a[i] = (old a)[i])
}
let main () :unit =
{}
let a = make 8 0 in
'Init:
a[0] <- 3; a[1] <- 1; a[2] <- 7; a[3] <- 0; a[4] <- 4; a[5] <- 1;
a[6] <- 6; a[7] <- 3;
let a0 = copy a in (** TODO make it as ghost *)
assert { power 2 2 = 4 };
upsweep 3 7 a;
a[7] <- 0;
downsweep 3 7 a0 a;
assert { a[0] = 0 };
assert { a[1] = 3 };
assert { a[2] = 4 };
assert { a[3] = 11 };
assert { a[4] = 11 };
assert { a[5] = 15 };
assert { a[6] = 16 };
assert { a[7] = 22 }
{}
end
(* This file is generated by Why3's Coq driver *)
(* Beware! Only edit allowed sections below *)
Require Import BuiltIn.
Require Import ZOdiv.
Require BuiltIn.
Require int.Int.
Require int.Abs.
Require int.ComputerDivision.
(* Why3 assumption *)
Definition unit := unit.
Parameter map : forall (a:Type) {a_WT:WhyType a} (b:Type) {b_WT:WhyType b},
Type.
Axiom map_WhyType : forall (a:Type) {a_WT:WhyType a}
(b:Type) {b_WT:WhyType b}, WhyType (map a b).
Existing Instance map_WhyType.
Parameter get: forall {a:Type} {a_WT:WhyType a} {b:Type} {b_WT:WhyType b},
(map a b) -> a -> b.
Parameter set: forall {a:Type} {a_WT:WhyType a} {b:Type} {b_WT:WhyType b},
(map a b) -> a -> b -> (map a b).
Axiom Select_eq : forall {a:Type} {a_WT:WhyType a} {b:Type} {b_WT:WhyType b},
forall (m:(map a b)), forall (a1:a) (a2:a), forall (b1:b), (a1 = a2) ->
((get (set m a1 b1) a2) = b1).
Axiom Select_neq : forall {a:Type} {a_WT:WhyType a}
{b:Type} {b_WT:WhyType b}, forall (m:(map a b)), forall (a1:a) (a2:a),
forall (b1:b), (~ (a1 = a2)) -> ((get (set m a1 b1) a2) = (get m a2)).
Parameter const: forall {a:Type} {a_WT:WhyType a} {b:Type} {b_WT:WhyType b},
b -> (map a b).
Axiom Const : forall {a:Type} {a_WT:WhyType a} {b:Type} {b_WT:WhyType b},
forall (b1:b) (a1:a), ((get (const b1:(map a b)) a1) = b1).
(* Why3 assumption *)
Inductive array (a:Type) {a_WT:WhyType a} :=
| mk_array : BuiltIn.int -> (map BuiltIn.int 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] [a_WT]].
(* Why3 assumption *)
Definition elts {a:Type} {a_WT:WhyType a}(v:(array a)): (map BuiltIn.int
a) := match v with
| (mk_array x x1) => x1
end.
(* Why3 assumption *)
Definition length {a:Type} {a_WT:WhyType a}(v:(array a)): BuiltIn.int :=
match v with
| (mk_array x x1) => x
end.
(* Why3 assumption *)
Definition get1 {a:Type} {a_WT:WhyType a}(a1:(array a)) (i:BuiltIn.int): a :=
(get (elts a1) i).
(* Why3 assumption *)
Definition set1 {a:Type} {a_WT:WhyType a}(a1:(array a)) (i:BuiltIn.int)
(v:a): (array a) := (mk_array (length a1) (set (elts a1) i v)).
(* Why3 assumption *)
Definition container := (map BuiltIn.int BuiltIn.int).
Parameter sum: (map BuiltIn.int BuiltIn.int) -> BuiltIn.int -> BuiltIn.int ->
BuiltIn.int.
Axiom Sum_def_empty : forall (c:(map BuiltIn.int BuiltIn.int))
(i:BuiltIn.int) (j:BuiltIn.int), (j <= i)%Z -> ((sum c i j) = 0%Z).
Axiom Sum_def_non_empty : forall (c:(map BuiltIn.int BuiltIn.int))
(i:BuiltIn.int) (j:BuiltIn.int), (i < j)%Z -> ((sum c i j) = ((get c
i) + (sum c (i + 1%Z)%Z j))%Z).
Axiom Sum_right_extension : forall (c:(map BuiltIn.int BuiltIn.int))
(i:BuiltIn.int) (j:BuiltIn.int), (i < j)%Z -> ((sum c i j) = ((sum c i
(j - 1%Z)%Z) + (get c (j - 1%Z)%Z))%Z).
Axiom Sum_transitivity : forall (c:(map BuiltIn.int BuiltIn.int))
(i:BuiltIn.int) (k:BuiltIn.int) (j:BuiltIn.int), ((i <= k)%Z /\
(k <= j)%Z) -> ((sum c i j) = ((sum c i k) + (sum c k j))%Z).
Axiom Sum_eq : forall (c1:(map BuiltIn.int BuiltIn.int)) (c2:(map BuiltIn.int
BuiltIn.int)) (i:BuiltIn.int) (j:BuiltIn.int), (forall (k:BuiltIn.int),
((i <= k)%Z /\ (k < j)%Z) -> ((get c1 k) = (get c2 k))) -> ((sum c1 i
j) = (sum c2 i j)).
(* Why3 assumption *)
Definition sum1(a:(array BuiltIn.int)) (l:BuiltIn.int)
(h:BuiltIn.int): BuiltIn.int := (sum (elts a) l h).
(* Why3 assumption *)
Definition go_left(left1:BuiltIn.int) (right1:BuiltIn.int): BuiltIn.int :=
let space := (right1 - left1)%Z in (left1 - (ZOdiv space 2%Z))%Z.
Axiom go_left_bounds : forall (left1:BuiltIn.int) (right1:BuiltIn.int),
((0%Z <= left1)%Z /\ (((left1 + 1%Z)%Z < right1)%Z /\
((right1 - left1)%Z <= left1)%Z)) -> ((0%Z <= (go_left left1 right1))%Z /\
((go_left left1 right1) < left1)%Z).
(* Why3 assumption *)
Definition go_right(left1:BuiltIn.int) (right1:BuiltIn.int): BuiltIn.int :=
let space := (right1 - left1)%Z in (right1 - (ZOdiv space 2%Z))%Z.
Axiom go_right_bounds : forall (left1:BuiltIn.int) (right1:BuiltIn.int),
((0%Z <= left1)%Z /\ (((left1 + 1%Z)%Z < right1)%Z /\
((right1 - left1)%Z <= left1)%Z)) -> ((left1 <= (go_right left1
right1))%Z /\ ((go_right left1 right1) < right1)%Z).
(* Why3 assumption *)
Inductive phase1 : BuiltIn.int -> BuiltIn.int -> (array BuiltIn.int)
-> (array BuiltIn.int) -> Prop :=
| Leaf : forall (left1:BuiltIn.int) (right1:BuiltIn.int) (a0:(array
BuiltIn.int)) (a:(array BuiltIn.int)), (right1 = (left1 + 1%Z)%Z) ->
(((get1 a left1) = (get1 a0 left1)) -> (phase1 left1 right1 a0 a))
| Node : forall (left1:BuiltIn.int) (right1:BuiltIn.int) (a0:(array
BuiltIn.int)) (a:(array BuiltIn.int)), ((left1 + 1%Z)%Z < right1)%Z ->
((phase1 (go_left left1 right1) left1 a0 a) -> ((phase1 (go_right left1
right1) right1 a0 a) -> (((get1 a left1) = (sum1 a0
((left1 - (right1 - left1)%Z)%Z + 1%Z)%Z (left1 + 1%Z)%Z)) ->
(phase1 left1 right1 a0 a)))).
Axiom Div_mod_2 : forall (x:BuiltIn.int), (0%Z <= x)%Z ->
(((2%Z * (ZOdiv x 2%Z))%Z <= x)%Z /\
((x - 1%Z)%Z <= (2%Z * (ZOdiv x 2%Z))%Z)%Z).
Axiom phase1_frame : forall (left1:BuiltIn.int) (right1:BuiltIn.int)
(a0:(array BuiltIn.int)) (a:(array BuiltIn.int)) (a':(array BuiltIn.int)),
(forall (i:BuiltIn.int), (((left1 - (right1 - left1)%Z)%Z < i)%Z /\
(i < right1)%Z) -> ((get1 a i) = (get1 a' i))) -> ((phase1 left1 right1 a0
a) -> (phase1 left1 right1 a0 a')).
Require Import Why3.
(* Why3 goal *)
Theorem phase1_frame2 : forall (left1:BuiltIn.int) (right1:BuiltIn.int)
(a0:(array BuiltIn.int)) (a0':(array BuiltIn.int)) (a:(array BuiltIn.int)),
(forall (i:BuiltIn.int), (((left1 - (right1 - left1)%Z)%Z < i)%Z /\
(i < right1)%Z) -> ((get1 a0 i) = (get1 a0' i))) -> ((phase1 left1 right1
a0 a) -> (phase1 left1 right1 a0' a)).
intros left1 right1 a0 a0' a h1 h2.
induction h2; why3 "z3".
Qed.
(* This file is generated by Why3's Coq driver *)
(* Beware! Only edit allowed sections below *)
Require Import BuiltIn.
Require Import ZOdiv.
Require BuiltIn.
Require int.Int.
Require int.Abs.
Require int.ComputerDivision.
(* Why3 assumption *)
Definition unit := unit.
Parameter map : forall (a:Type) {a_WT:WhyType a} (b:Type) {b_WT:WhyType b},
Type.
Axiom map_WhyType : forall (a:Type) {a_WT:WhyType a}
(b:Type) {b_WT:WhyType b}, WhyType (map a b).
Existing Instance map_WhyType.
Parameter get: forall {a:Type} {a_WT:WhyType a} {b:Type} {b_WT:WhyType b},
(map a b) -> a -> b.
Parameter set: forall {a:Type} {a_WT:WhyType a} {b:Type} {b_WT:WhyType b},
(map a b) -> a -> b -> (map a b).
Axiom Select_eq : forall {a:Type} {a_WT:WhyType a} {b:Type} {b_WT:WhyType b},
forall (m:(map a b)), forall (a1:a) (a2:a), forall (b1:b), (a1 = a2) ->
((get (set m a1 b1) a2) = b1).
Axiom Select_neq : forall {a:Type} {a_WT:WhyType a}
{b:Type} {b_WT:WhyType b}, forall (m:(map a b)), forall (a1:a) (a2:a),
forall (b1:b), (~ (a1 = a2)) -> ((get (set m a1 b1) a2) = (get m a2)).
Parameter const: forall {a:Type} {a_WT:WhyType a} {b:Type} {b_WT:WhyType b},
b -> (map a b).
Axiom Const : forall {a:Type} {a_WT:WhyType a} {b:Type} {b_WT:WhyType b},
forall (b1:b) (a1:a), ((get (const b1:(map a b)) a1) = b1).
(* Why3 assumption *)
Inductive array (a:Type) {a_WT:WhyType a} :=
| mk_array : BuiltIn.int -> (map BuiltIn.int 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] [a_WT]].
(* Why3 assumption *)
Definition elts {a:Type} {a_WT:WhyType a}(v:(array a)): (map BuiltIn.int
a) := match v with
| (mk_array x x1) => x1
end.
(* Why3 assumption *)
Definition length {a:Type} {a_WT:WhyType a}(v:(array a)): BuiltIn.int :=
match v with
| (mk_array x x1) => x
end.
(* Why3 assumption *)
Definition get1 {a:Type} {a_WT:WhyType a}(a1:(array a)) (i:BuiltIn.int): a :=
(get (elts a1) i).
(* Why3 assumption *)
Definition set1 {a:Type} {a_WT:WhyType a}(a1:(array a)) (i:BuiltIn.int)
(v:a): (array a) := (mk_array (length a1) (set (elts a1) i v)).
(* Why3 assumption *)
Definition container := (map BuiltIn.int BuiltIn.int).
Parameter sum: (map BuiltIn.int BuiltIn.int) -> BuiltIn.int -> BuiltIn.int ->
BuiltIn.int.
Axiom Sum_def_empty : forall (c:(map BuiltIn.int BuiltIn.int))
(i:BuiltIn.int) (j:BuiltIn.int), (j <= i)%Z -> ((sum c i j) = 0%Z).
Axiom Sum_def_non_empty : forall (c:(map BuiltIn.int BuiltIn.int))
(i:BuiltIn.int) (j:BuiltIn.int), (i < j)%Z -> ((sum c i j) = ((get c
i) + (sum c (i + 1%Z)%Z j))%Z).
Axiom Sum_right_extension : forall (c:(map BuiltIn.int BuiltIn.int))
(i:BuiltIn.int) (j:BuiltIn.int), (i < j)%Z -> ((sum c i j) = ((sum c i
(j - 1%Z)%Z) + (get c (j - 1%Z)%Z))%Z).
Axiom Sum_transitivity : forall (c:(map BuiltIn.int BuiltIn.int))
(i:BuiltIn.int) (k:BuiltIn.int) (j:BuiltIn.int), ((i <= k)%Z /\
(k <= j)%Z) -> ((sum c i j) = ((sum c i k) + (sum c k j))%Z).
Axiom Sum_eq : forall (c1:(map BuiltIn.int BuiltIn.int)) (c2:(map BuiltIn.int
BuiltIn.int)) (i:BuiltIn.int) (j:BuiltIn.int), (forall (k:BuiltIn.int),
((i <= k)%Z /\ (k < j)%Z) -> ((get c1 k) = (get c2 k))) -> ((sum c1 i
j) = (sum c2 i j)).
(* Why3 assumption *)
Definition sum1(a:(array BuiltIn.int)) (l:BuiltIn.int)
(h:BuiltIn.int): BuiltIn.int := (sum (elts a) l h).
(* Why3 assumption *)
Definition go_left(left1:BuiltIn.int) (right1:BuiltIn.int): BuiltIn.int :=
let space := (right1 - left1)%Z in (left1 - (ZOdiv space 2%Z))%Z.
Axiom go_left_bounds : forall (left1:BuiltIn.int) (right1:BuiltIn.int),
((0%Z <= left1)%Z /\ (((left1 + 1%Z)%Z < right1)%Z /\
((right1 - left1)%Z <= left1)%Z)) -> ((0%Z <= (go_left left1 right1))%Z /\
((go_left left1 right1) < left1)%Z).
(* Why3 assumption *)
Definition go_right(left1:BuiltIn.int) (right1:BuiltIn.int): BuiltIn.int :=
let space := (right1 - left1)%Z in (right1 - (ZOdiv space 2%Z))%Z.
Axiom go_right_bounds : forall (left1:BuiltIn.int) (right1:BuiltIn.int),
((0%Z <= left1)%Z /\ (((left1 + 1%Z)%Z < right1)%Z /\
((right1 - left1)%Z <= left1)%Z)) -> ((left1 <= (go_right left1
right1))%Z /\ ((go_right left1 right1) < right1)%Z).
(* Why3 assumption *)
Inductive phase1 : BuiltIn.int -> BuiltIn.int -> (array BuiltIn.int)
-> (array BuiltIn.int) -> Prop :=
| Leaf : forall (left1:BuiltIn.int) (right1:BuiltIn.int) (a0:(array
BuiltIn.int)) (a:(array BuiltIn.int)), (right1 = (left1 + 1%Z)%Z) ->
(((get1 a left1) = (get1 a0 left1)) -> (phase1 left1 right1 a0 a))
| Node : forall (left1:BuiltIn.int) (right1:BuiltIn.int) (a0:(array
BuiltIn.int)) (a:(array BuiltIn.int)), ((left1 + 1%Z)%Z < right1)%Z ->
((phase1 (go_left left1 right1) left1 a0 a) -> ((phase1 (go_right left1
right1) right1 a0 a) -> (((get1 a left1) = (sum1 a0
((left1 - (right1 - left1)%Z)%Z + 1%Z)%Z (left1 + 1%Z)%Z)) ->
(phase1 left1 right1 a0 a)))).
Axiom Div_mod_2 : forall (x:BuiltIn.int), (0%Z <= x)%Z ->
(((2%Z * (ZOdiv x 2%Z))%Z <= x)%Z /\
((x - 1%Z)%Z <= (2%Z * (ZOdiv x 2%Z))%Z)%Z).
Require Import Why3.
(* Why3 goal *)
Theorem phase1_frame : forall (left1:BuiltIn.int) (right1:BuiltIn.int)
(a0:(array BuiltIn.int)) (a:(array BuiltIn.int)) (a':(array BuiltIn.int)),
(forall (i:BuiltIn.int), (((left1 - (right1 - left1)%Z)%Z < i)%Z /\
(i < right1)%Z) -> ((get1 a i) = (get1 a' i))) -> ((phase1 left1 right1 a0
a) -> (phase1 left1 right1 a0 a')).
intros left1 right1 a0 a a' h1 h2.
induction h2.
why3 "cvc3".
why3 "z3".
Qed.
(* This file is generated by Why3's Coq driver *)
(* Beware! Only edit allowed sections below *)
Require Import BuiltIn.
Require Import ZOdiv.
Require BuiltIn.
Require int.Int.
Require int.Abs.
Require int.ComputerDivision.
Require int.Power.
(* Why3 assumption *)
Definition unit := unit.
Parameter map : forall (a:Type) {a_WT:WhyType a} (b:Type) {b_WT:WhyType b},
Type.
Axiom map_WhyType : forall (a:Type) {a_WT:WhyType a}
(b:Type) {b_WT:WhyType b}, WhyType (map a b).
Existing Instance map_WhyType.
Parameter get: forall {a:Type} {a_WT:WhyType a} {b:Type} {b_WT:WhyType b},
(map a b) -> a -> b.
Parameter set: forall {a:Type} {a_WT:WhyType a} {b:Type} {b_WT:WhyType b},
(map a b) -> a -> b -> (map a b).
Axiom Select_eq : forall {a:Type} {a_WT:WhyType a} {b:Type} {b_WT:WhyType b},
forall (m:(map a b)), forall (a1:a) (a2:a), forall (b1:b), (a1 = a2) ->
((get (set m a1 b1) a2) = b1).
Axiom Select_neq : forall {a:Type} {a_WT:WhyType a}
{b:Type} {b_WT:WhyType b}, forall (m:(map a b)), forall (a1:a) (a2:a),
forall (b1:b), (~ (a1 = a2)) -> ((get (set m a1 b1) a2) = (get m a2)).
Parameter const: forall {a:Type} {a_WT:WhyType a} {b:Type} {b_WT:WhyType b},
b -> (map a b).
Axiom Const : forall {a:Type} {a_WT:WhyType a} {b:Type} {b_WT:WhyType b},
forall (b1:b) (a1:a), ((get (const b1:(map a b)) a1) = b1).
(* Why3 assumption *)
Inductive array (a:Type) {a_WT:WhyType a} :=
| mk_array : BuiltIn.int -> (map BuiltIn.int 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] [a_WT]].
(* Why3 assumption *)
Definition elts {a:Type} {a_WT:WhyType a}(v:(array a)): (map BuiltIn.int
a) := match v with
| (mk_array x x1) => x1
end.
(* Why3 assumption *)
Definition length {a:Type} {a_WT:WhyType a}(v:(array a)): BuiltIn.int :=
match v with
| (mk_array x x1) => x
end.
(* Why3 assumption *)
Definition get1 {a:Type} {a_WT:WhyType a}(a1:(array a)) (i:BuiltIn.int): a :=
(get (elts a1) i).
(* Why3 assumption *)
Definition set1 {a:Type} {a_WT:WhyType a}(a1:(array a)) (i:BuiltIn.int)
(v:a): (array a) := (mk_array (length a1) (set (elts a1) i v)).
(* Why3 assumption *)
Definition container := (map BuiltIn.int BuiltIn.int).
Parameter sum: (map BuiltIn.int BuiltIn.int) -> BuiltIn.int -> BuiltIn.int ->
BuiltIn.int.
Axiom Sum_def_empty : forall (c:(map BuiltIn.int BuiltIn.int))
(i:BuiltIn.int) (j:BuiltIn.int), (j <= i)%Z -> ((sum c i j) = 0%Z).
Axiom Sum_def_non_empty : forall (c:(map BuiltIn.int BuiltIn.int))
(i:BuiltIn.int) (j:BuiltIn.int), (i < j)%Z -> ((sum c i j) = ((get c
i) + (sum c (i + 1%Z)%Z j))%Z).
Axiom Sum_right_extension : forall (c:(map BuiltIn.int BuiltIn.int))
(i:BuiltIn.int) (j:BuiltIn.int), (i < j)%Z -> ((sum c i j) = ((sum c i
(j - 1%Z)%Z) + (get c (j - 1%Z)%Z))%Z).
Axiom Sum_transitivity : forall (c:(map BuiltIn.int BuiltIn.int))
(i:BuiltIn.int) (k:BuiltIn.int) (j:BuiltIn.int), ((i <= k)%Z /\
(k <= j)%Z) -> ((sum c i j) = ((sum c i k) + (sum c k j))%Z).
Axiom Sum_eq : forall (c1:(map BuiltIn.int BuiltIn.int)) (c2:(map BuiltIn.int
BuiltIn.int)) (i:BuiltIn.int) (j:BuiltIn.int), (forall (k:BuiltIn.int),
((i <= k)%Z /\ (k < j)%Z) -> ((get c1 k) = (get c2 k))) -> ((sum c1 i
j) = (sum c2 i j)).
(* Why3 assumption *)
Definition sum1(a:(array BuiltIn.int)) (l:BuiltIn.int)
(h:BuiltIn.int): BuiltIn.int := (sum (elts a) l h).
(* Why3 assumption *)
Definition go_left(left1:BuiltIn.int) (right1:BuiltIn.int): BuiltIn.int :=
let space := (right1 - left1)%Z in (left1 - (ZOdiv space 2%Z))%Z.
Axiom go_left_bounds : forall (left1:BuiltIn.int) (right1:BuiltIn.int),
((0%Z <= left1)%Z /\ (((left1 + 1%Z)%Z < right1)%Z /\
((right1 - left1)%Z <= left1)%Z)) -> ((0%Z <= (go_left left1 right1))%Z /\
((go_left left1 right1) < left1)%Z).
(* Why3 assumption *)
Definition go_right(left1:BuiltIn.int) (right1:BuiltIn.int): BuiltIn.int :=
let space := (right1 - left1)%Z in (right1 - (ZOdiv space 2%Z))%Z.
Axiom go_right_bounds : forall (left1:BuiltIn.int) (right1:BuiltIn.int),
((0%Z <= left1)%Z /\ (((left1 + 1%Z)%Z < right1)%Z /\
((right1 - left1)%Z <= left1)%Z)) -> ((left1 <= (go_right left1
right1))%Z /\ ((go_right left1 right1) < right1)%Z).
Axiom Div_mod_2 : forall (x:BuiltIn.int), (0%Z <= x)%Z ->
(((2%Z * (ZOdiv x 2%Z))%Z <= x)%Z /\
((x - 1%Z)%Z <= (2%Z * (ZOdiv x 2%Z))%Z)%Z).
(* Why3 assumption *)
Definition is_power_of_2(x:BuiltIn.int): Prop := exists k:BuiltIn.int,
(0%Z <= k)%Z /\ (x = (int.Power.power 2%Z k)).
Axiom is_power_of_2_1 : forall (x:BuiltIn.int), (is_power_of_2 x) ->
((1%Z < x)%Z -> ((2%Z * (ZOdiv x 2%Z))%Z = x)).
Axiom is_power_of_2_2 : forall (x:BuiltIn.int), (is_power_of_2 x) ->
((1%Z < x)%Z -> (is_power_of_2 (ZOdiv x 2%Z))).
Axiom is_power_of_2_3 : forall (x:BuiltIn.int), (is_power_of_2 x) ->
(0%Z < x)%Z.
(* Why3 assumption *)
Inductive phase1 : BuiltIn.int -> BuiltIn.int -> (array BuiltIn.int)
-> (array BuiltIn.int) -> Prop :=
| Leaf : forall (left1:BuiltIn.int) (right1:BuiltIn.int) (a0:(array
BuiltIn.int)) (a:(array BuiltIn.int)), (right1 = (left1 + 1%Z)%Z) ->
(((get1 a left1) = (get1 a0 left1)) -> (phase1 left1 right1 a0 a))
| Node : forall (left1:BuiltIn.int) (right1:BuiltIn.int) (a0:(array
BuiltIn.int)) (a:(array BuiltIn.int)), ((left1 + 1%Z)%Z < right1)%Z ->
((phase1 (go_left left1 right1) left1 a0 a) -> ((phase1 (go_right left1
right1) right1 a0 a) -> (((get1 a left1) = (sum1 a0
((left1 - (right1 - left1)%Z)%Z + 1%Z)%Z (left1 + 1%Z)%Z)) ->
(phase1 left1 right1 a0 a)))).
Axiom phase1_frame : forall (left1:BuiltIn.int) (right1:BuiltIn.int)
(a0:(array BuiltIn.int)) (a:(array BuiltIn.int)) (a':(array BuiltIn.int)),
(forall (i:BuiltIn.int), (((left1 - (right1 - left1)%Z)%Z < i)%Z /\
(i < right1)%Z) -> ((get1 a i) = (get1 a' i))) -> ((phase1 left1 right1 a0
a) -> (phase1 left1 right1 a0 a')).
Axiom phase1_frame2 : forall (left1:BuiltIn.int) (right1:BuiltIn.int)
(a0:(array BuiltIn.int)) (a0':(array BuiltIn.int)) (a:(array BuiltIn.int)),
(forall (i:BuiltIn.int), (((left1 - (right1 - left1)%Z)%Z < i)%Z /\
(i < right1)%Z) -> ((get1 a0 i) = (get1 a0' i))) -> ((phase1 left1 right1
a0 a) -> (phase1 left1 right1 a0' a)).
(* Why3 assumption *)