Commit ff091cb7 authored by MARCHE Claude's avatar MARCHE Claude

New lemma injection_occ moved into stdlib

parent 12ade68a
(* This file is generated by Why3's Coq driver *)
(* Beware! Only edit allowed sections below *)
Require Import BuiltIn.
......
......@@ -4,9 +4,9 @@ Require Import BuiltIn.
Require BuiltIn.
Require int.Int.
Require map.Map.
Require map.MapInjection.
Require map.Occ.
Require map.MapPermut.
Require map.MapInjection.
(* Why3 assumption *)
Definition unit := unit.
......@@ -195,87 +195,6 @@ Definition values (v:suffixArray): (array Z) :=
| (mk_suffixArray x x1) => x
end.
Lemma injective_occ: forall (m: map.Map.map Z Z) n,
map.MapInjection.injective m n <-> forall v, (Occ.occ v m 0 n <= 1)%Z.
intros m n; split.
(* -> *)
intros inj v.
assert (case: (Occ.occ v m 0 n <= 1 \/ Occ.occ v m 0 n >= 2)%Z) by omega. destruct case.
trivial.
destruct (Occ.occ_exists v m 0 n) as (i,(hi1,hi2)). omega.
assert (0 <= Occ.occ v m 0 i)%Z.
generalize (Occ.occ_bounds v m 0 i). omega.
assert (case: (Occ.occ v m 0 i = 0 \/ Occ.occ v m 0 i > 0)%Z) by omega. destruct case.
assert (0 < Occ.occ v m (i+1) n)%Z.
assert (Occ.occ v m 0 n = Occ.occ v m 0 i + Occ.occ v m i n)%Z.
apply Occ.occ_append; omega.
assert (Occ.occ v m i n = Occ.occ v m i (i+1) + Occ.occ v m (i+1) n)%Z.
apply Occ.occ_append; omega.
assert (Occ.occ v m i (i+1) = 1)%Z.
rewrite Occ.occ_right_add.
replace (i+1-1)%Z with i by omega.
rewrite Occ.occ_empty; omega.
omega.
replace (i+1-1)%Z with i by omega. auto.
omega.
destruct (Occ.occ_exists v m (i+1) n) as (j,(hj1,hj2)). omega.
elim (inj i j); omega.
destruct (Occ.occ_exists v m 0 i) as (j,(hj1,hj2)). omega.
elim (inj i j); omega.
(* <- *)
intros occ i j hi hj neq eq.
pose (v := (Map.get m i)).
assert (Occ.occ v m 0 n >= 2)%Z.
assert (Occ.occ v m 0 n = Occ.occ v m 0 i + Occ.occ v m i n)%Z.
apply Occ.occ_append; omega.
assert (Occ.occ v m i n = Occ.occ v m i (i+1) + Occ.occ v m (i+1) n)%Z.
apply Occ.occ_append; omega.
assert (Occ.occ v m i (i+1) = 1)%Z.
rewrite Occ.occ_right_add.
replace (i+1-1)%Z with i by omega.
rewrite Occ.occ_empty; omega.
omega.
replace (i+1-1)%Z with i by omega. auto.
assert (case: (j < i \/ i+1 <= j)%Z) by omega. destruct case.
assert (Occ.occ v m 0 i >= 1)%Z.
assert (Occ.occ v m 0 i = Occ.occ v m 0 j + Occ.occ v m j i)%Z.
apply Occ.occ_append; omega.
assert (Occ.occ v m j i = Occ.occ v m j (j+1) + Occ.occ v m (j+1) i)%Z.
apply Occ.occ_append; omega.
assert (Occ.occ v m j (j+1) = 1)%Z.
rewrite Occ.occ_right_add.
replace (j+1-1)%Z with j by omega.
rewrite Occ.occ_empty; omega.
omega.
replace (j+1-1)%Z with j by omega. auto.
generalize (Occ.occ_bounds v m (i+1) n).
generalize (Occ.occ_bounds v m 0 j).
generalize (Occ.occ_bounds v m (j+1) i).
omega.
generalize (Occ.occ_bounds v m (i+1) n).
omega.
assert (Occ.occ v m (i+1) n >= 1)%Z.
assert (Occ.occ v m (i+1) n = Occ.occ v m (i+1) j + Occ.occ v m j n)%Z.
apply Occ.occ_append; omega.
assert (Occ.occ v m j n = Occ.occ v m j (j+1) + Occ.occ v m (j+1) n)%Z.
apply Occ.occ_append; omega.
assert (Occ.occ v m j (j+1) = 1)%Z.
rewrite Occ.occ_right_add.
replace (j+1-1)%Z with j by omega.
rewrite Occ.occ_empty; omega.
omega.
replace (j+1-1)%Z with j by omega. auto.
generalize (Occ.occ_bounds v m (j+1) n).
generalize (Occ.occ_bounds v m 0 i).
generalize (Occ.occ_bounds v m (i+1) j).
omega.
generalize (Occ.occ_bounds v m 0 i).
omega.
generalize (occ v); omega.
Qed.
(* Why3 goal *)
Theorem permut_permutation : forall (a1:(array Z)) (a2:(array Z)),
((permut_all a1 a2) /\ (permutation (elts a1) (length a1))) -> (permutation
......@@ -289,9 +208,9 @@ red; intros.
generalize (MapPermut.permut_exists _ _ _ _ _ h1b H).
intros (j, (h1,h2)). rewrite <- h2. auto.
(* injective *)
rewrite injective_occ.
rewrite MapInjection.injection_occ.
intros v; rewrite <- h1b.
generalize v; rewrite <- injective_occ.
generalize v; rewrite <- MapInjection.injection_occ.
assumption.
Qed.
......@@ -4,6 +4,7 @@ Require Import BuiltIn.
Require BuiltIn.
Require int.Int.
Require map.Map.
Require map.Occ.
(* preliminaries *)
......@@ -232,3 +233,86 @@ red in h1.
elimtype False; apply h1 with i0 j; clear h1; auto.
Qed.
Import Occ.
(* Why3 goal *)
Lemma injection_occ : forall (m:(map.Map.map Z Z)) (n:Z), (injective m n) <->
forall (v:Z), ((map.Occ.occ v m 0%Z n) <= 1%Z)%Z.
intros m n; split.
(* -> *)
intros inj v.
assert (case: (occ v m 0 n <= 1 \/ occ v m 0 n >= 2)%Z) by omega. destruct case.
trivial.
destruct (occ_exists v m 0 n) as (i,(hi1,hi2)). omega.
assert (0 <= occ v m 0 i)%Z.
generalize (occ_bounds v m 0 i). omega.
assert (case: (occ v m 0 i = 0 \/ occ v m 0 i > 0)%Z) by omega. destruct case.
assert (0 < occ v m (i+1) n)%Z.
assert (occ v m 0 n = occ v m 0 i + occ v m i n)%Z.
apply occ_append; omega.
assert (occ v m i n = occ v m i (i+1) + occ v m (i+1) n)%Z.
apply occ_append; omega.
assert (occ v m i (i+1) = 1)%Z.
rewrite occ_right_add.
replace (i+1-1)%Z with i by omega.
rewrite occ_empty; omega.
omega.
replace (i+1-1)%Z with i by omega. auto.
omega.
destruct (occ_exists v m (i+1) n) as (j,(hj1,hj2)). omega.
elim (inj i j); omega.
destruct (occ_exists v m 0 i) as (j,(hj1,hj2)). omega.
elim (inj i j); omega.
(* <- *)
intros Hocc i j hi hj neq eq.
pose (v := (Map.get m i)).
assert (occ v m 0 n >= 2)%Z.
assert (occ v m 0 n = occ v m 0 i + occ v m i n)%Z.
apply occ_append; omega.
assert (occ v m i n = occ v m i (i+1) + occ v m (i+1) n)%Z.
apply occ_append; omega.
assert (occ v m i (i+1) = 1)%Z.
rewrite occ_right_add.
replace (i+1-1)%Z with i by omega.
rewrite occ_empty; omega.
omega.
replace (i+1-1)%Z with i by omega. auto.
assert (case: (j < i \/ i+1 <= j)%Z) by omega. destruct case.
assert (occ v m 0 i >= 1)%Z.
assert (occ v m 0 i = occ v m 0 j + occ v m j i)%Z.
apply occ_append; omega.
assert (occ v m j i = occ v m j (j+1) + occ v m (j+1) i)%Z.
apply occ_append; omega.
assert (occ v m j (j+1) = 1)%Z.
rewrite occ_right_add.
replace (j+1-1)%Z with j by omega.
rewrite occ_empty; omega.
omega.
replace (j+1-1)%Z with j by omega. auto.
generalize (occ_bounds v m (i+1) n).
generalize (occ_bounds v m 0 j).
generalize (occ_bounds v m (j+1) i).
omega.
generalize (occ_bounds v m (i+1) n).
omega.
assert (occ v m (i+1) n >= 1)%Z.
assert (occ v m (i+1) n = occ v m (i+1) j + occ v m j n)%Z.
apply occ_append; omega.
assert (occ v m j n = occ v m j (j+1) + occ v m (j+1) n)%Z.
apply occ_append; omega.
assert (occ v m j (j+1) = 1)%Z.
rewrite occ_right_add.
replace (j+1-1)%Z with j by omega.
rewrite occ_empty; omega.
omega.
replace (j+1-1)%Z with j by omega. auto.
generalize (occ_bounds v m (j+1) n).
generalize (occ_bounds v m 0 i).
generalize (occ_bounds v m (i+1) j).
omega.
generalize (occ_bounds v m 0 i).
omega.
generalize (Hocc v); omega.
Qed.
......@@ -62,35 +62,6 @@ theory MapEq
end
(** {2 Injectivity and surjectivity for maps (indexed by integers)} *)
theory MapInjection
use import int.Int
use export Map
predicate injective (a: map int int) (n: int) =
forall i j: int. 0 <= i < n -> 0 <= j < n -> i <> j -> a[i] <> a[j]
(** [injective a n] is true when [a] is an injection
on the domain [(0..n-1)] *)
predicate surjective (a: map int int) (n: int) =
forall i: int. 0 <= i < n -> exists j: int. (0 <= j < n /\ a[j] = i)
(** [surjective a n] is true when [a] is a surjection
from [(0..n-1)] to [(0..n-1)] *)
predicate range (a: map int int) (n: int) =
forall i: int. 0 <= i < n -> 0 <= a[i] < n
(** [range a n] is true when [a] maps the domain
[(0..n-1)] into [(0..n-1)] *)
lemma injective_surjective:
forall a: map int int, n: int.
injective a n -> range a n -> surjective a n
(** main lemma: an injection on [(0..n-1)] that
ranges into [(0..n-1)] is also a surjection *)
end
theory MapExchange
use import int.Int
......@@ -264,3 +235,40 @@ theory MapPermut
exists j: int. l <= j < u /\ a1[j] = a2[i]
end
(** {2 Injectivity and surjectivity for maps (indexed by integers)} *)
theory MapInjection
use import int.Int
use export Map
predicate injective (a: map int int) (n: int) =
forall i j: int. 0 <= i < n -> 0 <= j < n -> i <> j -> a[i] <> a[j]
(** [injective a n] is true when [a] is an injection
on the domain [(0..n-1)] *)
predicate surjective (a: map int int) (n: int) =
forall i: int. 0 <= i < n -> exists j: int. (0 <= j < n /\ a[j] = i)
(** [surjective a n] is true when [a] is a surjection
from [(0..n-1)] to [(0..n-1)] *)
predicate range (a: map int int) (n: int) =
forall i: int. 0 <= i < n -> 0 <= a[i] < n
(** [range a n] is true when [a] maps the domain
[(0..n-1)] into [(0..n-1)] *)
lemma injective_surjective:
forall a: map int int, n: int.
injective a n -> range a n -> surjective a n
(** main lemma: an injection on [(0..n-1)] that
ranges into [(0..n-1)] is also a surjection *)
use import Occ
lemma injection_occ:
forall m: map int int, n: int.
injective m n <-> forall v:int. (occ v m 0 n <= 1)
end
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment