Commit 8f71eaa0 authored by MARCHE Claude's avatar MARCHE Claude

proof of binary heaps completed !

. but need further cleaning
parent 3a5f3de8
......@@ -66,6 +66,26 @@ axiom Card_union: forall x y: bag 'a. card (union x y) = (card x) + (card y)
axiom Card_zero_empty : forall x: bag 'a. card (x) = 0 -> x = empty_bag
(* bag difference *)
use import int.MinMax
function diff (bag 'a) (bag 'a) : bag 'a
axiom Diff_occ: forall b1 b2:bag 'a, x:'a.
nb_occ x (diff b1 b2) = max 0 (nb_occ x b1 - nb_occ x b2)
lemma Diff_empty_right: forall b:bag 'a. diff b empty_bag = b
lemma Diff_empty_left: forall b:bag 'a. diff empty_bag b = empty_bag
lemma Diff_add: forall b:bag 'a, x:'a. diff (add x b) (singleton x) = b
lemma Diff_comm: forall b b1 b2:bag 'a.
diff (diff b b1) b2 = diff (diff b b2) b1
lemma Add_diff: forall b:bag 'a, x:'a.
nb_occ x b > 0 -> add x (diff b (singleton x)) = b
end
(*
......
......@@ -3,8 +3,7 @@ theory Bag_integers
(* minimum element of a bag of integers *)
use import int.Int
clone import comparison.MinMax with type t = int, predicate ge = Int.(>=)
use import int.MinMax
use export bag.Bag
function min_bag (bag int) : int
......
......@@ -2,7 +2,7 @@ theory Elements
use import int.Int
use import bag.Bag
use map.Map as A
use import map.Map as A
type array 'a = A.map int 'a
......@@ -29,24 +29,28 @@ lemma Elements_union2 : forall a:array 'a, i j :int.
i < j ->
(elements a i j) = (add (A.get a (j-1)) (elements a i (j-1)))
lemma Elements_remove_last: forall a:array 'a, i j :int.
i < j-1 ->
(elements a i (j-1)) = diff (elements a i j) (singleton (A.get a (j-1)))
lemma Occ_elements: forall a:array 'a, i j n:int.
i <= j < n ->
nb_occ a[j] (elements a i n) > 0
lemma Elements_set_outside : forall a:array 'a, i j:int.
i <= j -> forall k : int. (k < i || k >= j) ->
forall e:'a. (elements (A.set a k e) i j) = (elements a i j)
lemma Elements_union3 : forall a:array 'a, i j:int, e:'a.
i <= j ->
(add e (elements a i j)) = (elements (A.set a j e) i (j+1))
lemma Elements_set2 : forall a:array 'a, i j k:int.
i <= k < j ->
forall e:'a. (add (A.get a k) (elements (A.set a k e) i j)) =
(add e (elements a i j))
lemma Elements_set_inside : forall a:array 'a, i j n: int, e:'a, b:bag 'a.
i <= j < n ->
(elements a i n) = add (A.get a j) b ->
(elements (A.set a j e) i n) = add e b
lemma Elements_set_inside2 : forall a:array 'a, i j n: int, e:'a.
i <= j < n ->
elements (A.set a j e) i n =
add e (diff (elements a i n) (singleton (a[j])))
end
(*
......
......@@ -3,13 +3,16 @@ module Implementation
use import int.Int
use import int.ComputerDivision
use import map.Map
use import heap.Heap
use import heap_model.Model
use import bag_of_integers.Bag_integers
use import elements.Elements
lemma Is_heap_min:
forall a:map, n :int. n > 0 ->
is_heap_array a 0 n -> A.get a 0 = min_bag (model (a, n))
is_heap_array a 0 n -> a[0] = min_bag (model (a, n))
use import module ref.Ref
......@@ -34,9 +37,9 @@ let insert (this : ref logic_heap) (e : int) : unit =
(!i = n ->
is_heap_array !arr 0 n /\
model (!arr, n) = model (a, n)) /\
(!i < n ->
(!i < n ->
is_heap_array !arr 0 (n + 1) /\
A.get !arr !i > e /\
!arr[!i] > e /\
model (!arr, n+1) = add (A.get !arr !i) (model (a, n)))
}
variant { !i }
......@@ -51,7 +54,7 @@ let insert (this : ref logic_heap) (e : int) : unit =
arr := A.set !arr !i e;
this := (!arr, n + 1);
assert { 0 < !i < n -> is_heap !this };
assert { !i < n -> model !this = add e (model (a,n)) }
assert { !i < n -> model !this = add e (model (a,n)) }
{ is_heap !this /\
model !this = add e (model (old !this)) }
......@@ -59,47 +62,48 @@ let extractMin (this : ref logic_heap) : int =
{ model !this <> empty_bag /\ is_heap !this }
let (a, n) = !this in
assert {n > 0};
let arr = ref a in
let min = A.get !arr 0 in
let min = a[0] in
let n' = n-1 in
let last = A.get !arr n' in
let last = a[n'] in
assert { n' > 0 -> nb_occ last (diff (model (a,n))
(singleton min)) > 0 } ;
let arr = ref a in
let i = ref 0 in
try
while ( !i < n') do
invariant {
!i >= 0 /\
0 <= !i /\
(n' > 0 -> !i < n') /\
is_heap_array !arr 0 n' /\
(!i = 0 ->
a = !arr /\
(model !this) = add last (model (a, n'))) /\
(0 < !i < n' ->
add (A.get !arr !i) (model !this) =
add last (add min (model (!arr, n')))) /\
(!i > 0 -> A.get !arr (parent !i) < last) }
(!i = 0 -> !arr = a) /\
(n' > 0 ->
elements !arr 0 n' =
add !arr[!i] (diff (diff (model (a,n))
(singleton last))
(singleton min))) /\
(!i > 0 -> !arr[parent !i] < last) }
variant {n' - !i}
let left = 2 * !i + 1 in
let right = 2 * !i + 2 in
if (left >= n') then raise Break;
let smaller = ref left in
if right < n' then
if A.get !arr left > A.get !arr right
if !arr[left] > !arr[right]
then smaller := right;
if (last <= (A.get !arr !smaller)) then raise Break;
assert {last > (A.get !arr !smaller)};
arr := A.set !arr !i (A.get !arr !smaller);
if last <= !arr[!smaller] then raise Break;
arr := !arr[!i <- !arr[!smaller]];
i := !smaller
done;
assert { model !this = add min (model (!arr,n')) }
with Break ->
assert { add (A.get !arr !i) (model !this) =
add last (add min (model (!arr, n'))) }
assert { n' = 0 }
with Break -> ()
end;
if (!i < n') then
if !i < n' then
begin
arr := A.set !arr !i last;
arr := !arr[!i <- last];
assert { !i > 0 -> is_heap_array !arr 0 n' };
assert { is_heap_array !arr 0 n' };
assert { model !this = add min (model (!arr,n')) }
assert { n' > 0 -> elements !arr 0 n' =
(diff (model (a,n)) (singleton min)) }
end;
this := (!arr, n');
min
......
(* This file is generated by Why3's Coq driver *)
(* Beware! Only edit allowed sections below *)
Require Import ZArith.
Require Import Rbase.
Parameter map : forall (a:Type) (b:Type), Type.
Parameter get: forall (a:Type) (b:Type), (map a b) -> a -> b.
Implicit Arguments get.
Parameter set: forall (a:Type) (b:Type), (map a b) -> a -> b -> (map a b).
Implicit Arguments set.
Axiom Select_eq : forall (a:Type) (b:Type), 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) (b:Type), 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 (b:Type) (a:Type), b -> (map a b).
Set Contextual Implicit.
Implicit Arguments const.
Unset Contextual Implicit.
Axiom Const : forall (b:Type) (a:Type), forall (b1:b) (a1:a), ((get (const(
b1):(map a b)) a1) = b1).
Definition bag (a:Type) := (map a Z).
Axiom occ_non_negative : forall (a:Type), forall (b:(map a Z)) (x:a),
(0%Z <= (get b x))%Z.
Definition eq_bag (a:Type)(a1:(map a Z)) (b:(map a Z)): Prop := forall (x:a),
((get a1 x) = (get b x)).
Implicit Arguments eq_bag.
Axiom bag_extensionality : forall (a:Type), forall (a1:(map a Z)) (b:(map a
Z)), (eq_bag a1 b) -> (a1 = b).
Parameter empty_bag: forall (a:Type), (map a Z).
Set Contextual Implicit.
Implicit Arguments empty_bag.
Unset Contextual Implicit.
Axiom occ_empty : forall (a:Type), forall (x:a), ((get (empty_bag:(map a Z))
x) = 0%Z).
Axiom is_empty : forall (a:Type), forall (b:(map a Z)), (forall (x:a),
((get b x) = 0%Z)) -> (b = (empty_bag:(map a Z))).
Axiom occ_singleton_eq : forall (a:Type), forall (x:a) (y:a), (x = y) ->
((get (set (empty_bag:(map a Z)) x 1%Z) y) = 1%Z).
Axiom occ_singleton_neq : forall (a:Type), forall (x:a) (y:a), (~ (x = y)) ->
((get (set (empty_bag:(map a Z)) x 1%Z) y) = 0%Z).
Parameter union: forall (a:Type), (map a Z) -> (map a Z) -> (map a Z).
Implicit Arguments union.
Axiom occ_union : forall (a:Type), forall (x:a) (a1:(map a Z)) (b:(map a Z)),
((get (union a1 b) x) = ((get a1 x) + (get b x))%Z).
Axiom Union_comm : forall (a:Type), forall (a1:(map a Z)) (b:(map a Z)),
((union a1 b) = (union b a1)).
Axiom Union_identity : forall (a:Type), forall (a1:(map a Z)), ((union a1
(empty_bag:(map a Z))) = a1).
Axiom Union_assoc : forall (a:Type), forall (a1:(map a Z)) (b:(map a Z))
(c:(map a Z)), ((union a1 (union b c)) = (union (union a1 b) c)).
Axiom bag_simpl : forall (a:Type), forall (a1:(map a Z)) (b:(map a Z))
(c:(map a Z)), ((union a1 b) = (union c b)) -> (a1 = c).
Axiom bag_simpl_left : forall (a:Type), forall (a1:(map a Z)) (b:(map a Z))
(c:(map a Z)), ((union a1 b) = (union a1 c)) -> (b = c).
Definition add (a:Type)(x:a) (b:(map a Z)): (map a Z) :=
(union (set (empty_bag:(map a Z)) x 1%Z) b).
Implicit Arguments add.
Axiom occ_add_eq : forall (a:Type), forall (b:(map a Z)) (x:a) (y:a),
(x = y) -> ((get (add x b) x) = ((get b x) + 1%Z)%Z).
Axiom occ_add_neq : forall (a:Type), forall (b:(map a Z)) (x:a) (y:a),
(~ (x = y)) -> ((get (add x b) y) = (get b y)).
Parameter card: forall (a:Type), (map a Z) -> Z.
Implicit Arguments card.
Axiom Card_empty : forall (a:Type), ((card (empty_bag:(map a Z))) = 0%Z).
Axiom Card_singleton : forall (a:Type), forall (x:a),
((card (set (empty_bag:(map a Z)) x 1%Z)) = 1%Z).
Axiom Card_union : forall (a:Type), forall (x:(map a Z)) (y:(map a Z)),
((card (union x y)) = ((card x) + (card y))%Z).
Axiom Card_zero_empty : forall (a:Type), forall (x:(map a Z)),
((card x) = 0%Z) -> (x = (empty_bag:(map a Z))).
Axiom Max_is_ge : forall (x:Z) (y:Z), (x <= (Zmax x y))%Z /\
(y <= (Zmax x y))%Z.
Axiom Max_is_some : forall (x:Z) (y:Z), ((Zmax x y) = x) \/ ((Zmax x y) = y).
Axiom Min_is_le : forall (x:Z) (y:Z), ((Zmin x y) <= x)%Z /\
((Zmin x y) <= y)%Z.
Axiom Min_is_some : forall (x:Z) (y:Z), ((Zmin x y) = x) \/ ((Zmin x y) = y).
Axiom Max_x : forall (x:Z) (y:Z), (y <= x)%Z -> ((Zmax x y) = x).
Axiom Max_y : forall (x:Z) (y:Z), (x <= y)%Z -> ((Zmax x y) = y).
Axiom Min_x : forall (x:Z) (y:Z), (x <= y)%Z -> ((Zmin x y) = x).
Axiom Min_y : forall (x:Z) (y:Z), (y <= x)%Z -> ((Zmin x y) = y).
Axiom Max_sym : forall (x:Z) (y:Z), (y <= x)%Z -> ((Zmax x y) = (Zmax y x)).
Axiom Min_sym : forall (x:Z) (y:Z), (y <= x)%Z -> ((Zmin x y) = (Zmin y x)).
Parameter diff: forall (a:Type), (map a Z) -> (map a Z) -> (map a Z).
Implicit Arguments diff.
Axiom Diff_occ : forall (a:Type), forall (b1:(map a Z)) (b2:(map a Z)) (x:a),
((get (diff b1 b2) x) = (Zmax 0%Z ((get b1 x) - (get b2 x))%Z)).
Axiom Diff_empty_right : forall (a:Type), forall (b:(map a Z)), ((diff b
(empty_bag:(map a Z))) = b).
Axiom Diff_empty_left : forall (a:Type), forall (b:(map a Z)),
((diff (empty_bag:(map a Z)) b) = (empty_bag:(map a Z))).
Axiom Diff_add : forall (a:Type), forall (b:(map a Z)) (x:a), ((diff (add x
b) (set (empty_bag:(map a Z)) x 1%Z)) = b).
(* YOU MAY EDIT THE CONTEXT BELOW *)
(* DO NOT EDIT BELOW *)
Theorem Diff_comm : forall (a:Type), forall (b:(map a Z)) (b1:(map a Z))
(b2:(map a Z)), ((diff (diff b b1) b2) = (diff (diff b b2) b1)).
(* YOU MAY EDIT THE PROOF BELOW *)
intros X b b1 b2.
apply bag_extensionality.
intro x.
repeat rewrite Diff_occ.
generalize (occ_non_negative X b2 x).
generalize (occ_non_negative X b1 x).
generalize (occ_non_negative X b x).
intros O1 O2 O3.
destruct (Zmax_spec 0 (get b x - get b1 x)) as [(H1,R1)|(I1,S1)].
rewrite R1.
destruct (Zmax_spec 0 (get b x - get b2 x)) as [(H2,R2)|(I2,S2)].
rewrite R2.
generalize (Zmax_spec 0 (0 - get b2 x));
generalize (Zmax_spec 0 (0 - get b1 x)); intuition.
rewrite S2.
generalize (Zmax_spec 0 (0 - get b2 x));
generalize (Zmax_spec 0 (get b x - get b2 x - get b1 x)); intuition.
rewrite S1.
destruct (Zmax_spec 0 (get b x - get b2 x)) as [(H2,R2)|(I2,S2)].
rewrite R2.
generalize (Zmax_spec 0 (0 - get b1 x));
generalize (Zmax_spec 0 (get b x - get b1 x - get b2 x)); intuition.
rewrite S2.
generalize (Zmax_spec 0 (get b x - get b1 x - get b2 x));
generalize (Zmax_spec 0 (get b x - get b2 x - get b1 x)); intuition.
Qed.
(* DO NOT EDIT BELOW *)
(* This file is generated by Why3's Coq driver *)
(* Beware! Only edit allowed sections below *)
Require Import ZArith.
Require Import Rbase.
Parameter map : forall (a:Type) (b:Type), Type.
Parameter get: forall (a:Type) (b:Type), (map a b) -> a -> b.
Implicit Arguments get.
Parameter set: forall (a:Type) (b:Type), (map a b) -> a -> b -> (map a b).
Implicit Arguments set.
Axiom Select_eq : forall (a:Type) (b:Type), 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) (b:Type), 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 (b:Type) (a:Type), b -> (map a b).
Set Contextual Implicit.
Implicit Arguments const.
Unset Contextual Implicit.
Axiom Const : forall (b:Type) (a:Type), forall (b1:b) (a1:a), ((get (const(
b1):(map a b)) a1) = b1).
Definition bag (a:Type) := (map a Z).
Axiom occ_non_negative : forall (a:Type), forall (b:(map a Z)) (x:a),
(0%Z <= (get b x))%Z.
Definition eq_bag (a:Type)(a1:(map a Z)) (b:(map a Z)): Prop := forall (x:a),
((get a1 x) = (get b x)).
Implicit Arguments eq_bag.
Axiom bag_extensionality : forall (a:Type), forall (a1:(map a Z)) (b:(map a
Z)), (eq_bag a1 b) -> (a1 = b).
Parameter empty_bag: forall (a:Type), (map a Z).
Set Contextual Implicit.
Implicit Arguments empty_bag.
Unset Contextual Implicit.
Axiom occ_empty : forall (a:Type), forall (x:a), ((get (empty_bag:(map a Z))
x) = 0%Z).
Axiom is_empty : forall (a:Type), forall (b:(map a Z)), (forall (x:a),
((get b x) = 0%Z)) -> (b = (empty_bag:(map a Z))).
Axiom occ_singleton_eq : forall (a:Type), forall (x:a) (y:a), (x = y) ->
((get (set (empty_bag:(map a Z)) x 1%Z) y) = 1%Z).
Axiom occ_singleton_neq : forall (a:Type), forall (x:a) (y:a), (~ (x = y)) ->
((get (set (empty_bag:(map a Z)) x 1%Z) y) = 0%Z).
Parameter union: forall (a:Type), (map a Z) -> (map a Z) -> (map a Z).
Implicit Arguments union.
Axiom occ_union : forall (a:Type), forall (x:a) (a1:(map a Z)) (b:(map a Z)),
((get (union a1 b) x) = ((get a1 x) + (get b x))%Z).
Axiom Union_comm : forall (a:Type), forall (a1:(map a Z)) (b:(map a Z)),
((union a1 b) = (union b a1)).
Axiom Union_identity : forall (a:Type), forall (a1:(map a Z)), ((union a1
(empty_bag:(map a Z))) = a1).
Axiom Union_assoc : forall (a:Type), forall (a1:(map a Z)) (b:(map a Z))
(c:(map a Z)), ((union a1 (union b c)) = (union (union a1 b) c)).
Axiom bag_simpl : forall (a:Type), forall (a1:(map a Z)) (b:(map a Z))
(c:(map a Z)), ((union a1 b) = (union c b)) -> (a1 = c).
Axiom bag_simpl_left : forall (a:Type), forall (a1:(map a Z)) (b:(map a Z))
(c:(map a Z)), ((union a1 b) = (union a1 c)) -> (b = c).
Definition add (a:Type)(x:a) (b:(map a Z)): (map a Z) :=
(union (set (empty_bag:(map a Z)) x 1%Z) b).
Implicit Arguments add.
Axiom occ_add_eq : forall (a:Type), forall (b:(map a Z)) (x:a) (y:a),
(x = y) -> ((get (add x b) x) = ((get b x) + 1%Z)%Z).
Axiom occ_add_neq : forall (a:Type), forall (b:(map a Z)) (x:a) (y:a),
(~ (x = y)) -> ((get (add x b) y) = (get b y)).
Parameter card: forall (a:Type), (map a Z) -> Z.
Implicit Arguments card.
Axiom Card_empty : forall (a:Type), ((card (empty_bag:(map a Z))) = 0%Z).
Axiom Card_singleton : forall (a:Type), forall (x:a),
((card (set (empty_bag:(map a Z)) x 1%Z)) = 1%Z).
Axiom Card_union : forall (a:Type), forall (x:(map a Z)) (y:(map a Z)),
((card (union x y)) = ((card x) + (card y))%Z).
Axiom Card_zero_empty : forall (a:Type), forall (x:(map a Z)),
((card x) = 0%Z) -> (x = (empty_bag:(map a Z))).
Axiom Max_is_ge : forall (x:Z) (y:Z), (x <= (Zmax x y))%Z /\
(y <= (Zmax x y))%Z.
Axiom Max_is_some : forall (x:Z) (y:Z), ((Zmax x y) = x) \/ ((Zmax x y) = y).
Axiom Min_is_le : forall (x:Z) (y:Z), ((Zmin x y) <= x)%Z /\
((Zmin x y) <= y)%Z.
Axiom Min_is_some : forall (x:Z) (y:Z), ((Zmin x y) = x) \/ ((Zmin x y) = y).
Axiom Max_x : forall (x:Z) (y:Z), (y <= x)%Z -> ((Zmax x y) = x).
Axiom Max_y : forall (x:Z) (y:Z), (x <= y)%Z -> ((Zmax x y) = y).
Axiom Min_x : forall (x:Z) (y:Z), (x <= y)%Z -> ((Zmin x y) = x).
Axiom Min_y : forall (x:Z) (y:Z), (y <= x)%Z -> ((Zmin x y) = y).
Axiom Max_sym : forall (x:Z) (y:Z), (y <= x)%Z -> ((Zmax x y) = (Zmax y x)).
Axiom Min_sym : forall (x:Z) (y:Z), (y <= x)%Z -> ((Zmin x y) = (Zmin y x)).
Parameter diff: forall (a:Type), (map a Z) -> (map a Z) -> (map a Z).
Implicit Arguments diff.
Axiom Diff_occ : forall (a:Type), forall (b1:(map a Z)) (b2:(map a Z)) (x:a),
((get (diff b1 b2) x) = (Zmax 0%Z ((get b1 x) - (get b2 x))%Z)).
Axiom Diff_empty_right : forall (a:Type), forall (b:(map a Z)), ((diff b
(empty_bag:(map a Z))) = b).
(* YOU MAY EDIT THE CONTEXT BELOW *)
(* DO NOT EDIT BELOW *)
Theorem Diff_empty_left : forall (a:Type), forall (b:(map a Z)),
((diff (empty_bag:(map a Z)) b) = (empty_bag:(map a Z))).
(* YOU MAY EDIT THE PROOF BELOW *)
intros X b.
apply bag_extensionality.
intro x.
rewrite Diff_occ.
rewrite occ_empty.
generalize (occ_non_negative X b x).
generalize (Zmax_spec 0 (0 - get b x))%Z.
auto with zarith.
Qed.
(* DO NOT EDIT BELOW *)
(* This file is generated by Why3's Coq driver *)
(* Beware! Only edit allowed sections below *)
Require Import ZArith.
Require Import Rbase.
Parameter map : forall (a:Type) (b:Type), Type.
Parameter get: forall (a:Type) (b:Type), (map a b) -> a -> b.
Implicit Arguments get.
Parameter set: forall (a:Type) (b:Type), (map a b) -> a -> b -> (map a b).
Implicit Arguments set.
Axiom Select_eq : forall (a:Type) (b:Type), 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) (b:Type), 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 (b:Type) (a:Type), b -> (map a b).
Set Contextual Implicit.
Implicit Arguments const.
Unset Contextual Implicit.
Axiom Const : forall (b:Type) (a:Type), forall (b1:b) (a1:a), ((get (const(
b1):(map a b)) a1) = b1).
Definition bag (a:Type) := (map a Z).
Axiom occ_non_negative : forall (a:Type), forall (b:(map a Z)) (x:a),
(0%Z <=