library: map.MapPermut now defined using map.Occ

(that is, using number of occurrences)
No more definition of permutation using inductive predicates.
Impacts array.ArrayPermut; proof sessions updated.
Coq realizations for map.Occ and map.MapPermut;
proof session for array.ArrayPermut in progress
parent 2e20446f
......@@ -865,7 +865,7 @@ COQLIBS_NUMBER = $(addprefix lib/coq/number/, $(COQLIBS_NUMBER_FILES))
COQLIBS_SET_FILES = Set
COQLIBS_SET = $(addprefix lib/coq/set/, $(COQLIBS_SET_FILES))
COQLIBS_MAP_FILES = Map MapPermut MapInjection
COQLIBS_MAP_FILES = Map Occ MapPermut MapInjection
COQLIBS_MAP = $(addprefix lib/coq/map/, $(COQLIBS_MAP_FILES))
COQLIBS_LIST_FILES = List Length Mem Nth NthLength HdTl NthHdTl Append NthLengthAppend Reverse
......
This source diff could not be displayed because it is too large. You can view the blob instead.
......@@ -21,19 +21,24 @@ module Algo64
(* Algorithm 63 *)
val partition (a:array int) (m n:int) (i j:ref int) : unit
val partition (a: array int) (m n: int) (i j: ref int) (ghost x: ref int) :
unit
requires { 0 <= m < n < length a }
writes { a, i, j}
ensures { m <= !j < !i <= n }
ensures { permut_sub (old a) a m (n+1) }
ensures {
exists x:int.
(forall r:int. m <= r <= !j -> a[r] <= x) /\
(forall r:int. !j < r < !i -> a[r] = x) /\
(forall r:int. !i <= r <= n -> a[r] >= x) }
ensures { forall r:int. m <= r <= !j -> a[r] <= !x }
ensures { forall r:int. !j < r < !i -> a[r] = !x }
ensures { forall r:int. !i <= r <= n -> a[r] >= !x }
(* Algorithm 64 *)
predicate qs_partition (t1 t2: array int) (m n i j: int) (x: int) =
permut_sub t1 t2 m (n+1) /\
(forall k:int. m <= k <= j -> t2[k] <= x) /\
(forall k:int. j < k < i -> t2[k] = x) /\
(forall k:int. i <= k <= n -> t2[k] >= x)
let rec quicksort (a:array int) (m n:int) : unit
requires { 0 <= m <= n < length a }
variant { n - m }
......@@ -42,33 +47,16 @@ module Algo64
= if m < n then begin
let i = ref 0 in
let j = ref 0 in
partition a m n i j;
let ghost x = ref 42 in
partition a m n i j x;
'L1: quicksort a m !j;
assert { permut_sub (at a 'L1) a m (n+1) };
assert { forall r:int. !j < r <= n -> a[r] = (at a 'L1)[r] };
assert { forall r:int. m <= r <= !j ->
(exists s:int. m <= s <= !j /\ a[r] = (at a 'L1)[s]) &&
a[r] <= a[!j+1] };
assert { qs_partition (at a 'L1) a m n !i !j !x };
'L2: quicksort a !i n;
assert { permut_sub (at a 'L2) a m (n+1) };
assert { forall r:int. m <= r < !i -> a[r] = (at a 'L2)[r] };
assert { forall r:int. !i <= r <= n ->
(exists s:int. !i <= s <= n /\ a[r] = (at a 'L2)[s]) &&
a[r] >= a[!i-1] };
assert {
forall r s:int. m <= r <= s <= n ->
if r <= !j then
if s <= !j then "a" a[r] <= a[s] else
if s < !i then "b" a[r] <= a[s] else
"c" a[r] <= a[s] else
if r < !i then
if s < !i then "d" a[r] <= a[s] else
"e" a[r] <= a[s] else
"f" a[r] <= a[s] }
assert { qs_partition (at a 'L2) a m n !i !j !x }
end
let qs (a:array int) : unit
ensures { permut_all (old a) a }
ensures { permut_all (old a) a /\ qs_partition (old a) a 0 0 0 0 0 }
ensures { sorted a }
= if length a > 0 then quicksort a 0 (length a - 1)
......
This source diff could not be displayed because it is too large. You can view the blob instead.
......@@ -20,20 +20,19 @@ module Algo65
(* algorithm 63 *)
val partition (a:array int) (m n:int) (i j:ref int) : unit
val partition (a:array int) (m n: int) (i j: ref int) (ghost x: ref int) :
unit
requires { 0 <= m < n < length a }
writes { a, i, j }
ensures { m <= !j < !i <= n }
ensures { permut_sub (old a) a m (n+1) }
ensures {
exists x:int.
(forall r:int. m <= r <= !j -> a[r] <= x) /\
(forall r:int. !j < r < !i -> a[r] = x) /\
(forall r:int. !i <= r <= n -> a[r] >= x) }
ensures { forall r:int. m <= r <= !j -> a[r] <= !x }
ensures { forall r:int. !j < r < !i -> a[r] = !x }
ensures { forall r:int. !i <= r <= n -> a[r] >= !x }
(* Algorithm 65 (fixed version) *)
let rec find (a:array int) (m n:int) (k:int) : unit
let rec find (a:array int) (m n:int) (k:int) : unit
requires { 0 <= m <= k <= n < length a }
variant { n - m }
ensures { permut_sub (old a) a m (n+1) }
......@@ -42,7 +41,8 @@ module Algo65
= if m < n then begin
let i = ref 0 in
let j = ref 0 in
partition a m n i j;
let ghost x = ref 42 in
partition a m n i j x;
'L1:
if k <= !j then find a m !j k;
assert { permut_sub (at a 'L1) a m (n+1) };
......
This source diff could not be displayed because it is too large. You can view the blob instead.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
......@@ -15,7 +15,7 @@ module InsertionSortNaive
use import array.ArraySorted
use import array.ArrayPermut
let sort (a:array int)
let sort (a:array int)
ensures { sorted a }
ensures { permut_all (old a) a }
=
......@@ -68,7 +68,7 @@ module InsertionSortNaiveGen
predicate sorted (a : array elt) =
M.sorted_sub a.elts 0 a.length
let sort (a:array elt)
let sort (a:array elt)
ensures { sorted a }
ensures { permut_all (old a) a }
=
......@@ -161,7 +161,8 @@ end
module InsertionSortParamBad
(* this version is hard to prove because predicate sorted_sub applies to an array instead of a map *)
(* this version is hard to prove because predicate sorted_sub
applies to an array instead of a map *)
use import int.Int
use import ref.Ref
......
This source diff could not be displayed because it is too large. You can view the blob instead.
......@@ -15,6 +15,12 @@ module Quicksort
use import array.ArrayPermut
use import array.ArrayEq
predicate qs_partition (t1 t2: array int) (l m r: int) (v: int) =
permut_sub t1 t2 l r /\
(forall j:int. l <= j < m -> t2[j] < v) /\
(forall j:int. m < j < r -> v <= t2[j]) /\
t2[m] = v
let rec quick_rec (t: array int) (l: int) (r: int) : unit
requires { 0 <= l <= r <= length t }
ensures { sorted_sub t l r }
......@@ -35,19 +41,12 @@ module Quicksort
end
done;
'M: swap t l !m;
assert { permut_sub (at t 'M) t l r };
assert { forall j:int. l <= j < !m -> t[j] < v };
assert { forall j:int. !m < j < r -> t[j] = (at t 'M)[j] };
assert { qs_partition (at t 'M) t l !m r v };
'N: quick_rec t l !m;
assert { permut_sub (at t 'N) t l r };
assert { forall j:int. l <= j < !m -> t[j] < v };
assert { forall j:int. !m <= j < r -> t[j] = (at t 'N)[j] };
assert { qs_partition (at t 'N) t l !m r v };
'O: quick_rec t (!m + 1) r;
assert { permut_sub (at t 'O) t l r };
assert { forall j:int. l <= j <= !m -> t[j] = (at t 'O)[j] };
assert { forall j:int. !m < j < r ->
(exists i:int. !m < i < r /\ t[j] = (at t 'O)[i]) &&
t[j] >= v }
assert { qs_partition (at t 'O) t l !m r v };
assert { qs_partition (at t 'N) t l !m r v }
end
let quicksort (t : array int) =
......
This source diff could not be displayed because it is too large. You can view the blob instead.
This diff is collapsed.
......@@ -5,7 +5,6 @@ Require BuiltIn.
Require int.Int.
Require map.Map.
Require map.MapInjection.
Require map.MapPermut.
(* Why3 assumption *)
Definition unit := unit.
......@@ -41,7 +40,7 @@ Definition set {a:Type} {a_WT:WhyType a} (a1:(@array a a_WT)) (i:Z)
(* Why3 assumption *)
Definition make {a:Type} {a_WT:WhyType a} (n:Z) (v:a): (@array a a_WT) :=
(mk_array n (map.Map.const v:(@map.Map.map Z _ a a_WT))).
(mk_array n (map.Map.const v: (@map.Map.map Z _ a a_WT))).
(* Why3 assumption *)
Definition is_common_prefix (a:(@array Z _)) (x:Z) (y:Z) (l:Z): Prop :=
......@@ -86,6 +85,73 @@ Definition lt (a:(@array Z _)) (x:Z) (y:Z): Prop := let n := (length a) in
Definition range (a:(@array Z _)): Prop := (map.MapInjection.range (elts a)
(length a)).
Parameter occ: forall {a:Type} {a_WT:WhyType a}, a -> (@map.Map.map Z _
a a_WT) -> Z -> Z -> Z.
Axiom occ_empty : forall {a:Type} {a_WT:WhyType a}, forall (v:a)
(m:(@map.Map.map Z _ a a_WT)) (l:Z) (u:Z), (u <= l)%Z -> ((occ v m l
u) = 0%Z).
Axiom occ_right_no_add : forall {a:Type} {a_WT:WhyType a}, forall (v:a)
(m:(@map.Map.map Z _ a a_WT)) (l:Z) (u:Z), (l < u)%Z -> ((~ ((map.Map.get m
(u - 1%Z)%Z) = v)) -> ((occ v m l u) = (occ v m l (u - 1%Z)%Z))).
Axiom occ_right_add : forall {a:Type} {a_WT:WhyType a}, forall (v:a)
(m:(@map.Map.map Z _ a a_WT)) (l:Z) (u:Z), (l < u)%Z -> (((map.Map.get m
(u - 1%Z)%Z) = v) -> ((occ v m l u) = (1%Z + (occ v m l (u - 1%Z)%Z))%Z)).
Axiom occ_bounds : forall {a:Type} {a_WT:WhyType a}, forall (v:a)
(m:(@map.Map.map Z _ a a_WT)) (l:Z) (u:Z), (l < u)%Z -> ((0%Z <= (occ v m l
u))%Z /\ ((occ v m l u) <= (u - l)%Z)%Z).
Axiom occ_append : forall {a:Type} {a_WT:WhyType a}, forall (v:a)
(m:(@map.Map.map Z _ a a_WT)) (l:Z) (mid:Z) (u:Z), ((l <= mid)%Z /\
(mid <= u)%Z) -> ((occ v m l u) = ((occ v m l mid) + (occ v m mid u))%Z).
Axiom occ_neq : forall {a:Type} {a_WT:WhyType a}, forall (v:a)
(m:(@map.Map.map Z _ a a_WT)) (l:Z) (u:Z), (forall (i:Z), ((l <= i)%Z /\
(i < u)%Z) -> ~ ((map.Map.get m i) = v)) -> ((occ v m l u) = 0%Z).
Axiom occ_exists : forall {a:Type} {a_WT:WhyType a}, forall (v:a)
(m:(@map.Map.map Z _ a a_WT)) (l:Z) (u:Z), (0%Z < (occ v m l u))%Z ->
exists i:Z, ((l <= i)%Z /\ (i < u)%Z) /\ ((map.Map.get m i) = v).
Axiom occ_pos : forall {a:Type} {a_WT:WhyType a}, forall (m:(@map.Map.map Z _
a a_WT)) (l:Z) (u:Z) (i:Z), ((l <= i)%Z /\ (i < u)%Z) ->
(0%Z < (occ (map.Map.get m i) m l u))%Z.
(* Why3 assumption *)
Definition permut {a:Type} {a_WT:WhyType a} (m1:(@map.Map.map Z _ a a_WT))
(m2:(@map.Map.map Z _ a a_WT)) (l:Z) (u:Z): Prop := forall (v:a), ((occ v
m1 l u) = (occ v m2 l u)).
Axiom permut_trans : forall {a:Type} {a_WT:WhyType a},
forall (a1:(@map.Map.map Z _ a a_WT)) (a2:(@map.Map.map Z _ a a_WT))
(a3:(@map.Map.map Z _ a a_WT)), forall (l:Z) (u:Z), (permut a1 a2 l u) ->
((permut a2 a3 l u) -> (permut a1 a3 l u)).
Axiom permut_exists : forall {a:Type} {a_WT:WhyType a},
forall (a1:(@map.Map.map Z _ a a_WT)) (a2:(@map.Map.map Z _ a a_WT)) (l:Z)
(u:Z) (i:Z), (permut a1 a2 l u) -> (((l <= i)%Z /\ (i < u)%Z) ->
exists j:Z, ((l <= j)%Z /\ (j < u)%Z) /\ ((map.Map.get a1
j) = (map.Map.get a2 i))).
(* Why3 assumption *)
Definition map_eq_sub {a:Type} {a_WT:WhyType a} (a1:(@map.Map.map Z _
a a_WT)) (a2:(@map.Map.map Z _ a a_WT)) (l:Z) (u:Z): Prop := forall (i:Z),
((l <= i)%Z /\ (i < u)%Z) -> ((map.Map.get a1 i) = (map.Map.get a2 i)).
(* Why3 assumption *)
Definition array_eq_sub {a:Type} {a_WT:WhyType a} (a1:(@array a a_WT))
(a2:(@array a a_WT)) (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))).
(* Why3 assumption *)
Definition array_eq {a:Type} {a_WT:WhyType a} (a1:(@array a a_WT))
(a2:(@array a a_WT)): 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:(@map.Map.map Z _ a a_WT))
(a2:(@map.Map.map Z _ a a_WT)) (l:Z) (u:Z) (i:Z) (j:Z): Prop :=
......@@ -101,51 +167,27 @@ Axiom exchange_set : forall {a:Type} {a_WT:WhyType a},
(map.Map.set (map.Map.set a1 i (map.Map.get a1 j)) j (map.Map.get a1 i)) l
u i j)).
(* Why3 assumption *)
Definition map_eq_sub {a:Type} {a_WT:WhyType a} (a1:(@map.Map.map Z _
a a_WT)) (a2:(@map.Map.map Z _ a a_WT)) (l:Z) (u:Z): Prop := forall (i:Z),
((l <= i)%Z /\ (i < u)%Z) -> ((map.Map.get a1 i) = (map.Map.get a2 i)).
(* Why3 assumption *)
Definition exchange1 {a:Type} {a_WT:WhyType a} (a1:(@array a a_WT))
(a2:(@array a a_WT)) (i:Z) (j:Z): Prop := ((length a1) = (length a2)) /\
(exchange (elts a1) (elts a2) 0%Z (length a1) i j).
(* Why3 assumption *)
Definition array_eq_sub {a:Type} {a_WT:WhyType a} (a1:(@array a a_WT))
(a2:(@array a a_WT)) (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))).
(* Why3 assumption *)
Definition array_eq {a:Type} {a_WT:WhyType a} (a1:(@array a a_WT))
(a2:(@array a a_WT)): Prop := ((length a1) = (length a2)) /\ (map_eq_sub
(elts a1) (elts a2) 0%Z (length a1)).
(* Why3 assumption *)
Definition permut {a:Type} {a_WT:WhyType a} (a1:(@array a a_WT)) (a2:(@array
Definition permut1 {a:Type} {a_WT:WhyType a} (a1:(@array a a_WT)) (a2:(@array
a a_WT)) (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))).
(u <= (length a1))%Z) /\ (permut (elts a1) (elts a2) l u))).
(* Why3 assumption *)
Definition permut_sub {a:Type} {a_WT:WhyType a} (a1:(@array a a_WT))
(a2:(@array a a_WT)) (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
0%Z l) /\ ((permut1 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 a_WT))
(a2:(@array a a_WT)): Prop := ((length a1) = (length a2)) /\
(map.MapPermut.permut (elts a1) (elts a2) 0%Z (length a1)).
Axiom permut_sub_refl : forall {a:Type} {a_WT:WhyType a}, forall (a1:(@array
a a_WT)) (l:Z) (u:Z), ((0%Z <= l)%Z /\ ((l <= u)%Z /\
(u <= (length a1))%Z)) -> (permut_sub a1 a1 l u).
Axiom permut_sub_trans : forall {a:Type} {a_WT:WhyType a}, forall (a1:(@array
a a_WT)) (a2:(@array a a_WT)) (a3:(@array a a_WT)) (l:Z) (u:Z), (permut_sub
a1 a2 l u) -> ((permut_sub a2 a3 l u) -> (permut_sub a1 a3 l u)).
(a2:(@array a a_WT)): Prop := ((length a1) = (length a2)) /\ (permut
(elts a1) (elts a2) 0%Z (length a1)).
Axiom exchange_permut_sub : forall {a:Type} {a_WT:WhyType a},
forall (a1:(@array a a_WT)) (a2:(@array a a_WT)) (i:Z) (j:Z) (l:Z) (u:Z),
......@@ -153,11 +195,6 @@ Axiom exchange_permut_sub : forall {a:Type} {a_WT:WhyType a},
(j < u)%Z) -> ((0%Z <= l)%Z -> ((u <= (length a1))%Z -> (permut_sub a1 a2 l
u))))).
Axiom permut_sub_unmodified : forall {a:Type} {a_WT:WhyType a},
forall (a1:(@array a a_WT)) (a2:(@array a a_WT)) (l:Z) (u:Z), (permut_sub
a1 a2 l u) -> forall (i:Z), (((0%Z <= i)%Z /\ (i < l)%Z) \/ ((u <= i)%Z /\
(i < (length a1))%Z)) -> ((get a2 i) = (get a1 i)).
Axiom permut_sub_weakening : forall {a:Type} {a_WT:WhyType a},
forall (a1:(@array a a_WT)) (a2:(@array a a_WT)) (l1:Z) (u1:Z) (l2:Z)
(u2:Z), (permut_sub a1 a2 l1 u1) -> (((0%Z <= l2)%Z /\ (l2 <= l1)%Z) ->
......@@ -168,25 +205,10 @@ Axiom permut_sub_compose : forall {a:Type} {a_WT:WhyType a},
(l1:Z) (u1:Z) (l2:Z) (u2:Z), (u1 <= l2)%Z -> ((permut_sub a1 a2 l1 u1) ->
((permut_sub a2 a3 l2 u2) -> (permut_sub a1 a3 l1 u2))).
Axiom permut_all_refl : forall {a:Type} {a_WT:WhyType a}, forall (a1:(@array
a a_WT)), (permut_all a1 a1).
Axiom permut_all_trans : forall {a:Type} {a_WT:WhyType a}, forall (a1:(@array
a a_WT)) (a2:(@array a a_WT)) (a3:(@array a a_WT)), (permut_all a1 a2) ->
((permut_all a2 a3) -> (permut_all a1 a3)).
Axiom exchange_permut_all : forall {a:Type} {a_WT:WhyType a},
forall (a1:(@array a a_WT)) (a2:(@array a a_WT)) (i:Z) (j:Z), (exchange1 a1
a2 i j) -> (permut_all a1 a2).
Axiom array_eq_permut_all : forall {a:Type} {a_WT:WhyType a},
forall (a1:(@array a a_WT)) (a2:(@array a a_WT)), (array_eq a1 a2) ->
(permut_all a1 a2).
Axiom permut_sub_permut_all : forall {a:Type} {a_WT:WhyType a},
forall (a1:(@array a a_WT)) (a2:(@array a a_WT)) (l:Z) (u:Z), (permut_sub
a1 a2 l u) -> (permut_all a1 a2).
(* Why3 assumption *)
Definition le (a:(@array Z _)) (x:Z) (y:Z): Prop := (x = y) \/ (lt a x y).
......
......@@ -72,7 +72,7 @@ Defined.
(* Why3 goal *)
Lemma Const : forall {a:Type} {a_WT:WhyType a} {b:Type} {b_WT:WhyType b},
forall (b1:b) (a1:a), ((get (const b1:(@map a a_WT b b_WT)) a1) = b1).
forall (b1:b) (a1:a), ((get (const b1: (@map a a_WT b b_WT)) a1) = b1).
Proof.
easy.
Qed.
......
......@@ -218,7 +218,6 @@ Definition range (a:(@map.Map.map Z _ Z _)) (n:Z): Prop := forall (i:Z),
((0%Z <= i)%Z /\ (i < n)%Z) -> ((0%Z <= (map.Map.get a i))%Z /\
((map.Map.get a i) < n)%Z).
(* Why3 goal *)
Lemma injective_surjective : forall (a:(@map.Map.map Z _ Z _)) (n:Z),
(injective a n) -> ((range a n) -> (surjective a n)).
......
......@@ -4,54 +4,23 @@ Require Import BuiltIn.
Require BuiltIn.
Require int.Int.
Require map.Map.
Require map.Occ.
(* Why3 assumption *)
Definition exchange {a:Type} {a_WT:WhyType a} (a1:(@map.Map.map Z _ a a_WT))
(a2:(@map.Map.map Z _ a a_WT)) (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))))))).
Definition permut {a:Type} {a_WT:WhyType a} (m1:(@map.Map.map Z _ a a_WT))
(m2:(@map.Map.map Z _ a a_WT)) (l:Z) (u:Z): Prop := forall (v:a),
((map.Occ.occ v m1 l u) = (map.Occ.occ v m2 l u)).
(* Why3 goal *)
Lemma exchange_set : forall {a:Type} {a_WT:WhyType a},
forall (a1:(@map.Map.map Z _ a a_WT)) (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)).
intros a a_WT a1 l u i j (h1,h2) (h3,h4).
unfold exchange.
intuition.
rewrite Map.Select_eq; auto.
assert (H: i = j \/ i <> j) by omega.
destruct H.
rewrite H; rewrite Map.Select_eq; auto.
rewrite Map.Select_neq; auto.
rewrite Map.Select_eq; auto.
rewrite Map.Select_neq; auto.
rewrite Map.Select_neq; auto.
Lemma permut_trans : forall {a:Type} {a_WT:WhyType a},
forall (a1:(@map.Map.map Z _ a a_WT)) (a2:(@map.Map.map Z _ a a_WT))
(a3:(@map.Map.map Z _ a a_WT)), forall (l:Z) (u:Z), (permut a1 a2 l u) ->
((permut a2 a3 l u) -> (permut a1 a3 l u)).
intros a a_WT a1 a2 a3 l u h1 h2.
unfold permut in *.
intros. transitivity (Occ.occ v a2 l u); auto.
Qed.
(* Why3 assumption *)
Definition map_eq_sub {a:Type} {a_WT:WhyType a} (a1:(@map.Map.map Z _
a a_WT)) (a2:(@map.Map.map Z _ a a_WT)) (l:Z) (u:Z): Prop := forall (i:Z),
((l <= i)%Z /\ (i < u)%Z) -> ((map.Map.get a1 i) = (map.Map.get a2 i)).
(* Why3 assumption *)
Inductive permut {a:Type} {a_WT:WhyType a} : (@map.Map.map Z _ a a_WT) ->
(@map.Map.map Z _ a a_WT) -> Z -> Z -> Prop :=
| permut_refl : forall (a1:(@map.Map.map Z _ a a_WT)) (a2:(@map.Map.map Z _
a a_WT)), forall (l:Z) (u:Z), (map_eq_sub a1 a2 l u) -> ((@permut _ _)
a1 a2 l u)
| permut_trans : forall (a1:(@map.Map.map Z _ a a_WT)) (a2:(@map.Map.map
Z _ a a_WT)) (a3:(@map.Map.map Z _ a a_WT)), forall (l:Z) (u:Z),
((@permut _ _) a1 a2 l u) -> (((@permut _ _) a2 a3 l u) ->
((@permut _ _) a1 a3 l u))
| permut_exchange : forall (a1:(@map.Map.map Z _ a a_WT)) (a2:(@map.Map.map
Z _ a a_WT)), forall (l:Z) (u:Z) (i:Z) (j:Z), (exchange a1 a2 l u i
j) -> ((@permut _ _) a1 a2 l u).
(* Why3 goal *)
Lemma permut_exists : forall {a:Type} {a_WT:WhyType a},
forall (a1:(@map.Map.map Z _ a a_WT)) (a2:(@map.Map.map Z _ a a_WT)) (l:Z)
......@@ -60,59 +29,12 @@ Lemma permut_exists : forall {a:Type} {a_WT:WhyType a},
j) = (map.Map.get a2 i))).
Proof.
intros a a_WT a1 a2 l u i h1 Hi.
assert ((exists j, (l <= j < u)%Z /\ Map.get a1 j = Map.get a2 i) /\
(exists j, (l <= j < u)%Z /\ Map.get a2 j = Map.get a1 i)).
2: easy.
revert i Hi.
induction h1.
(* refl *)
intros i Hi.
red in H.
split ; exists i ; intuition.
rewrite <- H; auto.
(* trans *)
intros i Hi.
split.
destruct (IHh1_2 i Hi) as ((j&H1&H2),_).
destruct (IHh1_1 j H1) as ((k&H3&H4),_).
exists k.
split ; try easy.
now transitivity (Map.get a2 j).
destruct (IHh1_1 i Hi) as (_,(j&H1&H2)).
destruct (IHh1_2 j H1) as (_,(k&H3&H4)).
exists k.
split ; try easy.
now transitivity (Map.get a2 j).
(* exchange *)
revert H.
unfold exchange.
intros [Hi [Hj [Ha1ia2j [Ha1ja2i H]]]] k Hk.
destruct (Z_eq_dec k i) as [Hki|Hki].
split ;
exists j ;
split ; try easy ;
rewrite Hki ;
intuition.
destruct (Z_eq_dec k j) as [Hkj|Hkj].
split ;
exists i ;
split ; try easy ;
rewrite Hkj ;
apply sym_eq; intuition.
split ;
exists k ;
split ; try easy.
now apply H ; intuition.
now apply sym_eq, H ; intuition.
pose (v := Map.get a2 i).
assert (0 < map.Occ.occ v a2 l u)%Z.
apply map.Occ.occ_pos. assumption.
rewrite <- h1 in H.
generalize (map.Occ.occ_exists v a1 l u H).
intros (j, (hj1,hj2)).
exists j; intuition.
Qed.
(* Unused content named permut_sym
intros a a_WT a1 a2 l u h1.
induction h1; intuition.
apply permut_refl; unfold map_eq_sub in *; intuition.
rewrite <- H; auto.
apply permut_trans with a2; auto.
apply permut_exchange with j i; auto.
intros; rewrite <- H4; auto.
Qed.
*)
(* This file is generated by Why3's Coq-realize driver *)
(* Beware! Only edit allowed sections below *)
Require Import BuiltIn.
Require BuiltIn.
Require int.Int.
Require map.Map.
Require Recdef.
Function occ_ (a:Type) (a_WT:WhyType a) (v:a) (m: @map.Map.map Z _
a a_WT) (l: Z) (delta: Z) {measure Zabs_nat delta } : Z :=
if Z_le_gt_dec delta 0%Z then 0%Z else
((if why_decidable_eq (map.Map.get m (l + delta - 1)%Z) v then 1 else 0) +
occ_ a a_WT v m l (delta-1))%Z.
intros a a_WT _ _ _ delta h.
destruct (Z_le_gt_dec delta 0); intros.
now omega.
now apply Zabs2Nat.inj_lt; omega.
Defined.
(* Why3 goal *)
Definition occ: forall {a:Type} {a_WT:WhyType a}, a -> (@map.Map.map Z _
a a_WT) -> Z -> Z -> Z.
intros a a_WT v m l u.
exact (occ_ a a_WT v m l (u-l)%Z).
Defined.
(* Why3 goal *)
Lemma occ_empty : forall {a:Type} {a_WT:WhyType a}, forall (v:a)
(m:(@map.Map.map Z _ a a_WT)) (l:Z) (u:Z), (u <= l)%Z -> ((occ v m l
u) = 0%Z).
intros a a_WT v m l u h1.
unfold occ. rewrite occ__equation.
destruct (Z_le_gt_dec (u - l) 0)%Z; intros.
now trivial.
omega.
Qed.
(* Why3 goal *)
Lemma occ_right_no_add : forall {a:Type} {a_WT:WhyType a}, forall (v:a)
(m:(@map.Map.map Z _ a a_WT)) (l:Z) (u:Z), (l < u)%Z -> ((~ ((map.Map.get m
(u - 1%Z)%Z) = v)) -> ((occ v m l u) = (occ v m l (u - 1%Z)%Z))).
intros a a_WT v m l u h1 h2.
unfold occ. rewrite occ__equation.
destruct (Z_le_gt_dec (u - l) 0)%Z; intros.
rewrite occ__equation.
destruct (Z_le_gt_dec (u - 1 - l) 0)%Z; intros.
now trivial.
omega.
destruct (why_decidable_eq (Map.get m (l + (u - l) - 1)%Z) v).
replace (l + (u - l) - 1)%Z with (u-1)%Z in e by omega.
intuition.
replace (u - 1 - l)%Z with (u - l - 1)%Z by omega.
ring.
Qed.
(* Why3 goal *)
Lemma occ_right_add : forall {a:Type} {a_WT:WhyType a}, forall (v:a)
(m:(@map.Map.map Z _ a a_WT)) (l:Z) (u:Z), (l < u)%Z -> (((map.Map.get m
(u - 1%Z)%Z) = v) -> ((occ v m l u) = (1%Z + (occ v m l (u - 1%Z)%Z))%Z)).
intros a a_WT v m l u h1 h2.
unfold occ. rewrite occ__equation.
destruct (Z_le_gt_dec (u - l) 0)%Z; intros.
rewrite occ__equation.
destruct (Z_le_gt_dec (u - 1 - l) 0)%Z; intros.
omega.
omega.
destruct (why_decidable_eq (Map.get m (l + (u - l) - 1)%Z) v).
replace (u - 1 - l)%Z with (u - l - 1)%Z by omega.
ring.
replace (l + (u - l) - 1)%Z with (u-1)%Z in n by omega.
intuition.
Qed.
(* Why3 goal *)
Lemma occ_bounds : forall {a:Type} {a_WT:WhyType a}, forall (v:a)
(m:(@map.Map.map Z _ a a_WT)) (l:Z) (u:Z), (l <= u)%Z -> ((0%Z <= (occ v m
l u))%Z /\ ((occ v m l u) <= (u - l)%Z)%Z).
intros a a_WT v m l u h1.
cut (0 <= u - l)%Z. 2: omega.
replace (occ v m l u) with (occ v m l (l + (u - l)))%Z.
pattern (u - l)%Z; apply Z_lt_induction. 2: omega.
intros.
assert (h: (x = 0 \/ x <> 0)%Z) by omega. destruct h.
now rewrite occ_empty; omega.
destruct (why_decidable_eq (Map.get m (l + (x-1))%Z) v).
rewrite occ_right_add.
generalize (H (x-1)%Z); clear H; intros.
assert (0 <= occ v m l (l + (x - 1)) <= x-1)%Z.
apply H; omega.
replace (l + x - 1)%Z with (l+(x-1))%Z by ring.
omega.
omega.
replace (l + x - 1)%Z with (l+(x-1))%Z by ring.
trivial.
rewrite occ_right_no_add.
assert (0 <= occ v m l (l + (x - 1)) <= x-1)%Z.
apply H; omega.
replace (l + x - 1)%Z with (l+(x-1))%Z by ring.
omega.
omega.
replace (l + x - 1)%Z with (l+(x-1))%Z by ring.
trivial.
replace (l + (u-l))%Z with u by ring. trivial.
Qed.
(* Why3 goal *)
Lemma occ_append : forall {a:Type} {a_WT:WhyType a}, forall (v:a)
(m:(@map.Map.map Z _ a a_WT)) (l:Z) (mid:Z) (u:Z), ((l <= mid)%Z /\
(mid <= u)%Z) -> ((occ v m l u) = ((occ v m l mid) + (occ v m mid u))%Z).
intros a a_WT v m l mid u (h1,h2).
cut (0 <= u - mid)%Z. 2: omega.
replace (occ v m l u) with (occ v m l (mid + (u - mid)))%Z.
replace (occ v m mid u) with (occ v m mid (mid + (u - mid)))%Z.
pattern (u - mid)%Z; apply Z_lt_induction. 2: omega.