Commit 717baeab authored by Andrei Paskevich's avatar Andrei Paskevich

do not refresh non-aliased regions at the start of a function WP

parent fda65f6b
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.
......@@ -24,10 +24,10 @@
locfile="../assigning_meanings_to_programs.mlw"
loclnum="12" loccnumb="6" loccnume="9"
expl="VC for sum"
sum="e0ca4e8622864551ab60bb029148376f"
sum="9ce3e09613751b22aec78ab286a1ccb3"
proved="true"
expanded="true"
shape="iainfix =V3asumV2c1ainfix +V1c1ainfix <ainfix -V1V6ainfix -V1V4Aainfix <=c0ainfix -V1V4Aainfix =V5asumV2c1V6Aainfix <=V6ainfix +V1c1Aainfix <=c1V6Iainfix =V6ainfix +V4c1FIainfix =V5ainfix +V3agetV2V4FAainfix <V4V0Aainfix <=c0V4ainfix <=V4V1Iainfix =V3asumV2c1V4Aainfix <=V4ainfix +V1c1Aainfix <=c1V4FAainfix =c0asumV2c1c1Aainfix <=c1ainfix +V1c1Aainfix <=c1c1Iainfix <V1V0Aainfix <=c0V1Aainfix <=c0V0FF">
shape="iainfix =V3asumV1c1ainfix +V2c1ainfix <ainfix -V2V6ainfix -V2V4Aainfix <=c0ainfix -V2V4Aainfix =V5asumV1c1V6Aainfix <=V6ainfix +V2c1Aainfix <=c1V6Iainfix =V6ainfix +V4c1FIainfix =V5ainfix +V3agetV1V4FAainfix <V4V0Aainfix <=c0V4ainfix <=V4V2Iainfix =V3asumV1c1V4Aainfix <=V4ainfix +V2c1Aainfix <=c1V4FAainfix =c0asumV1c1c1Aainfix <=c1ainfix +V2c1Aainfix <=c1c1Iainfix <V2V0Aainfix <=c0V2Aainfix <=c0V0F">
<label
name="expl:VC for sum"/>
<proof
......
(* This file is generated by Why3's Coq driver *)
(* This file is generated by Why3's Coq 8.4 driver *)
(* Beware! Only edit allowed sections below *)
Require Import BuiltIn.
Require BuiltIn.
......@@ -60,6 +60,12 @@ Parameter remove: forall {a:Type} {a_WT:WhyType a}, a -> (@set a a_WT)
Axiom remove_def1 : forall {a:Type} {a_WT:WhyType a}, forall (x:a) (y:a)
(s:(@set a a_WT)), (mem x (remove y s)) <-> ((~ (x = y)) /\ (mem x s)).
Axiom add_remove : forall {a:Type} {a_WT:WhyType a}, forall (x:a) (s:(@set
a a_WT)), (mem x s) -> ((add x (remove x s)) = s).
Axiom remove_add : forall {a:Type} {a_WT:WhyType a}, forall (x:a) (s:(@set
a a_WT)), ((remove x (add x s)) = (remove x s)).
Axiom subset_remove : forall {a:Type} {a_WT:WhyType a}, forall (x:a) (s:(@set
a a_WT)), (subset (remove x s) s).
......@@ -349,10 +355,10 @@ Ltac ae := why3 "alt-ergo".
Require Import Classical.
(* Why3 goal *)
Theorem WP_parameter_relax : forall (u:vertex) (v:vertex) (pass:Z) (via:(@set
(vertex* vertex)%type _)), forall (m:(@map.Map.map vertex vertex_WhyType
t t_WhyType)), ((((1%Z < pass)%Z \/ (1%Z = pass)) /\ ((mem (u, v) edges) /\
~ (mem (u, v) via))) /\ forall (v1:vertex), (mem v1 vertices) ->
Theorem WP_parameter_relax : forall (m:(@map.Map.map vertex vertex_WhyType
t t_WhyType)) (u:vertex) (v:vertex) (pass:Z) (via:(@set (vertex*
vertex)%type _)), ((((1%Z < pass)%Z \/ (1%Z = pass)) /\ ((mem (u, v)
edges) /\ ~ (mem (u, v) via))) /\ forall (v1:vertex), (mem v1 vertices) ->
match (map.Map.get m
v1) with
| (Finite n) => (exists l:(list vertex), (path s l v1) /\ ((path_weight l
......@@ -384,8 +390,7 @@ Theorem WP_parameter_relax : forall (u:vertex) (v:vertex) (pass:Z) (via:(@set
v1) = n)
| Infinite => True
end).
(* Why3 intros u v pass via m ((h1,(h2,h3)),h4) h5 m1 h6 v1 h7. *)
intros u v pass via m ((hpass, (h1, h2)), h3).
intros m u v pass via ((hpass, (h1, h2)), h3).
destruct (Map.get m u) as [] _eqn. 2:intuition.
intros hlt m1 eqm1 v1 hv1.
destruct (classic (v1 = v)) as [h|h].
......
This diff is collapsed.
......@@ -24,10 +24,10 @@
locfile="../binary_search.mlw"
loclnum="17" loccnumb="6" loccnume="19"
expl="VC for binary_search"
sum="56a7828114cad28fdbf0f3086ba665f0"
sum="08847e78e28f9e02c4b8da41705b16fc"
proved="true"
expanded="true"
shape="iNainfix =agetV2V5V1Iainfix &lt;V5V0Aainfix &lt;=c0V5Fiiainfix =agetV2V6V1Aainfix &lt;V6V0Aainfix &lt;=c0V6ainfix &lt;ainfix -V7V4ainfix -V3V4Aainfix &lt;=c0ainfix -V3V4Aainfix &lt;=V8V7Aainfix &lt;=V4V8Iainfix =agetV2V8V1Iainfix &lt;V8V0Aainfix &lt;=c0V8FAainfix &lt;V7V0Aainfix &lt;=c0V4Iainfix =V7ainfix -V6c1Fainfix &gt;agetV2V6V1Aainfix &lt;V6V0Aainfix &lt;=c0V6ainfix &lt;ainfix -V3V9ainfix -V3V4Aainfix &lt;=c0ainfix -V3V4Aainfix &lt;=V10V3Aainfix &lt;=V9V10Iainfix =agetV2V10V1Iainfix &lt;V10V0Aainfix &lt;=c0V10FAainfix &lt;V3V0Aainfix &lt;=c0V9Iainfix =V9ainfix +V6c1Fainfix &lt;agetV2V6V1Aainfix &lt;V6V0Aainfix &lt;=c0V6Aainfix &lt;=V6V3Aainfix &lt;=V4V6Lainfix +V4adivainfix -V3V4c2ainfix &lt;=V4V3Iainfix &lt;=V11V3Aainfix &lt;=V4V11Iainfix =agetV2V11V1Iainfix &lt;V11V0Aainfix &lt;=c0V11FAainfix &lt;V3V0Aainfix &lt;=c0V4FAainfix &lt;=V12ainfix -V0c1Aainfix &lt;=c0V12Iainfix =agetV2V12V1Iainfix &lt;V12V0Aainfix &lt;=c0V12FAainfix &lt;ainfix -V0c1V0Aainfix &lt;=c0c0Iainfix &lt;=agetV2V13agetV2V14Iainfix &lt;V14V0Aainfix &lt;=V13V14Aainfix &lt;=c0V13FAainfix &lt;=c0V0FF">
shape="iNainfix =agetV1V5V2Iainfix &lt;V5V0Aainfix &lt;=c0V5Fiiainfix =agetV1V6V2Aainfix &lt;V6V0Aainfix &lt;=c0V6ainfix &lt;ainfix -V7V4ainfix -V3V4Aainfix &lt;=c0ainfix -V3V4Aainfix &lt;=V8V7Aainfix &lt;=V4V8Iainfix =agetV1V8V2Iainfix &lt;V8V0Aainfix &lt;=c0V8FAainfix &lt;V7V0Aainfix &lt;=c0V4Iainfix =V7ainfix -V6c1Fainfix &gt;agetV1V6V2Aainfix &lt;V6V0Aainfix &lt;=c0V6ainfix &lt;ainfix -V3V9ainfix -V3V4Aainfix &lt;=c0ainfix -V3V4Aainfix &lt;=V10V3Aainfix &lt;=V9V10Iainfix =agetV1V10V2Iainfix &lt;V10V0Aainfix &lt;=c0V10FAainfix &lt;V3V0Aainfix &lt;=c0V9Iainfix =V9ainfix +V6c1Fainfix &lt;agetV1V6V2Aainfix &lt;V6V0Aainfix &lt;=c0V6Aainfix &lt;=V6V3Aainfix &lt;=V4V6Lainfix +V4adivainfix -V3V4c2ainfix &lt;=V4V3Iainfix &lt;=V11V3Aainfix &lt;=V4V11Iainfix =agetV1V11V2Iainfix &lt;V11V0Aainfix &lt;=c0V11FAainfix &lt;V3V0Aainfix &lt;=c0V4FAainfix &lt;=V12ainfix -V0c1Aainfix &lt;=c0V12Iainfix =agetV1V12V2Iainfix &lt;V12V0Aainfix &lt;=c0V12FAainfix &lt;ainfix -V0c1V0Aainfix &lt;=c0c0Iainfix &lt;=agetV1V13agetV1V14Iainfix &lt;V14V0Aainfix &lt;=V13V14Aainfix &lt;=c0V13FAainfix &lt;=c0V0F">
<label
name="expl:VC for binary_search"/>
<proof
......@@ -59,10 +59,10 @@
locfile="../binary_search.mlw"
loclnum="60" loccnumb="6" loccnume="19"
expl="VC for binary_search"
sum="469d933c0ef6d53b10a8af8040766229"
sum="7302df6e214500c9c3bd1a2ae61f34ce"
proved="true"
expanded="true"
shape="iNainfix =agetV2V5V1Iainfix &lt;V5V0Aainfix &lt;=c0V5Fiiainfix =agetV2V6V1Aainfix &lt;V6V0Aainfix &lt;=c0V6ainfix &lt;ainfix -V7V4ainfix -V3V4Aainfix &lt;=c0ainfix -V3V4Aainfix &lt;=V8V7Aainfix &lt;=V4V8Iainfix =agetV2V8V1Iainfix &lt;V8V0Aainfix &lt;=c0V8FAainfix &lt;V7V0Aainfix &lt;=c0V4Iainfix =V7ainfix -V6c1Fainfix &gt;agetV2V6V1Aainfix &lt;V6V0Aainfix &lt;=c0V6ainfix &lt;ainfix -V3V9ainfix -V3V4Aainfix &lt;=c0ainfix -V3V4Aainfix &lt;=V10V3Aainfix &lt;=V9V10Iainfix =agetV2V10V1Iainfix &lt;V10V0Aainfix &lt;=c0V10FAainfix &lt;V3V0Aainfix &lt;=c0V9Iainfix =V9ainfix +V6c1Fainfix &lt;agetV2V6V1Aainfix &lt;V6V0Aainfix &lt;=c0V6Iainfix &lt;=V6V3Aainfix &lt;=V4V6FAainfix &lt;=V4V3ainfix &lt;=V4V3Iainfix &lt;=V11V3Aainfix &lt;=V4V11Iainfix =agetV2V11V1Iainfix &lt;V11V0Aainfix &lt;=c0V11FAainfix &lt;V3V0Aainfix &lt;=c0V4FAainfix &lt;=V12ainfix -V0c1Aainfix &lt;=c0V12Iainfix =agetV2V12V1Iainfix &lt;V12V0Aainfix &lt;=c0V12FAainfix &lt;ainfix -V0c1V0Aainfix &lt;=c0c0Iainfix &lt;=agetV2V13agetV2V14Iainfix &lt;V14V0Aainfix &lt;=V13V14Aainfix &lt;=c0V13FAainfix &lt;=c0V0FF">
shape="iNainfix =agetV1V5V2Iainfix &lt;V5V0Aainfix &lt;=c0V5Fiiainfix =agetV1V6V2Aainfix &lt;V6V0Aainfix &lt;=c0V6ainfix &lt;ainfix -V7V4ainfix -V3V4Aainfix &lt;=c0ainfix -V3V4Aainfix &lt;=V8V7Aainfix &lt;=V4V8Iainfix =agetV1V8V2Iainfix &lt;V8V0Aainfix &lt;=c0V8FAainfix &lt;V7V0Aainfix &lt;=c0V4Iainfix =V7ainfix -V6c1Fainfix &gt;agetV1V6V2Aainfix &lt;V6V0Aainfix &lt;=c0V6ainfix &lt;ainfix -V3V9ainfix -V3V4Aainfix &lt;=c0ainfix -V3V4Aainfix &lt;=V10V3Aainfix &lt;=V9V10Iainfix =agetV1V10V2Iainfix &lt;V10V0Aainfix &lt;=c0V10FAainfix &lt;V3V0Aainfix &lt;=c0V9Iainfix =V9ainfix +V6c1Fainfix &lt;agetV1V6V2Aainfix &lt;V6V0Aainfix &lt;=c0V6Iainfix &lt;=V6V3Aainfix &lt;=V4V6FAainfix &lt;=V4V3ainfix &lt;=V4V3Iainfix &lt;=V11V3Aainfix &lt;=V4V11Iainfix =agetV1V11V2Iainfix &lt;V11V0Aainfix &lt;=c0V11FAainfix &lt;V3V0Aainfix &lt;=c0V4FAainfix &lt;=V12ainfix -V0c1Aainfix &lt;=c0V12Iainfix =agetV1V12V2Iainfix &lt;V12V0Aainfix &lt;=c0V12FAainfix &lt;ainfix -V0c1V0Aainfix &lt;=c0c0Iainfix &lt;=agetV1V13agetV1V14Iainfix &lt;V14V0Aainfix &lt;=V13V14Aainfix &lt;=c0V13FAainfix &lt;=c0V0F">
<label
name="expl:VC for binary_search"/>
<proof
......@@ -86,10 +86,10 @@
locfile="../binary_search.mlw"
loclnum="100" loccnumb="6" loccnume="19"
expl="VC for binary_search"
sum="b4024703c302726d0965763f55ca4a89"
sum="65cd85f330f0ad5752c4568a313833cc"
proved="true"
expanded="true"
shape="iNainfix =agetV2V5V1Iainfix &lt;V5V0Aainfix &lt;=c0V5Fiiainfix =agetV2V7V1Aainfix &lt;V7V0Aainfix &lt;=c0V7ainfix &lt;ainfix -V8V4ainfix -V3V4Aainfix &lt;=c0ainfix -V3V4Aainfix &lt;=V9V8Aainfix &lt;=V4V9Iainfix =agetV2V9V1Iainfix &lt;V9V0Aainfix &lt;=c0V9FAainfix &lt;V8V0Aainfix &lt;=c0V4Iainfix =V8ainfix -V7c1FAainfix &lt;=ainfix -V7c1amax_intAainfix &lt;=amin_intainfix -V7c1ainfix &gt;agetV2V7V1Aainfix &lt;V7V0Aainfix &lt;=c0V7ainfix &lt;ainfix -V3V10ainfix -V3V4Aainfix &lt;=c0ainfix -V3V4Aainfix &lt;=V11V3Aainfix &lt;=V10V11Iainfix =agetV2V11V1Iainfix &lt;V11V0Aainfix &lt;=c0V11FAainfix &lt;V3V0Aainfix &lt;=c0V10Iainfix =V10ainfix +V7c1FAainfix &lt;=ainfix +V7c1amax_intAainfix &lt;=amin_intainfix +V7c1ainfix &lt;agetV2V7V1Aainfix &lt;V7V0Aainfix &lt;=c0V7Aainfix &lt;=V7V3Aainfix &lt;=V4V7Lainfix +V4V6Aainfix &lt;=ainfix +V4V6amax_intAainfix &lt;=amin_intainfix +V4V6Ladivainfix -V3V4c2Aainfix &lt;=ainfix -V3V4amax_intAainfix &lt;=amin_intainfix -V3V4ainfix &lt;=V4V3Iainfix &lt;=V12V3Aainfix &lt;=V4V12Iainfix =agetV2V12V1Iainfix &lt;V12V0Aainfix &lt;=c0V12FAainfix &lt;V3V0Aainfix &lt;=c0V4FAainfix &lt;=V13ainfix -V0c1Aainfix &lt;=c0V13Iainfix =agetV2V13V1Iainfix &lt;V13V0Aainfix &lt;=c0V13FAainfix &lt;ainfix -V0c1V0Aainfix &lt;=c0c0Aainfix &lt;=ainfix -V0c1amax_intAainfix &lt;=amin_intainfix -V0c1Iainfix &lt;=agetV2V14agetV2V15Iainfix &lt;V15V0Aainfix &lt;=V14V15Aainfix &lt;=c0V14FAainfix &lt;=V0amax_intAainfix &lt;=c0V0FF">
shape="iNainfix =agetV1V5V2Iainfix &lt;V5V0Aainfix &lt;=c0V5Fiiainfix =agetV1V7V2Aainfix &lt;V7V0Aainfix &lt;=c0V7ainfix &lt;ainfix -V8V4ainfix -V3V4Aainfix &lt;=c0ainfix -V3V4Aainfix &lt;=V9V8Aainfix &lt;=V4V9Iainfix =agetV1V9V2Iainfix &lt;V9V0Aainfix &lt;=c0V9FAainfix &lt;V8V0Aainfix &lt;=c0V4Iainfix =V8ainfix -V7c1FAainfix &lt;=ainfix -V7c1amax_intAainfix &lt;=amin_intainfix -V7c1ainfix &gt;agetV1V7V2Aainfix &lt;V7V0Aainfix &lt;=c0V7ainfix &lt;ainfix -V3V10ainfix -V3V4Aainfix &lt;=c0ainfix -V3V4Aainfix &lt;=V11V3Aainfix &lt;=V10V11Iainfix =agetV1V11V2Iainfix &lt;V11V0Aainfix &lt;=c0V11FAainfix &lt;V3V0Aainfix &lt;=c0V10Iainfix =V10ainfix +V7c1FAainfix &lt;=ainfix +V7c1amax_intAainfix &lt;=amin_intainfix +V7c1ainfix &lt;agetV1V7V2Aainfix &lt;V7V0Aainfix &lt;=c0V7Aainfix &lt;=V7V3Aainfix &lt;=V4V7Lainfix +V4V6Aainfix &lt;=ainfix +V4V6amax_intAainfix &lt;=amin_intainfix +V4V6Ladivainfix -V3V4c2Aainfix &lt;=ainfix -V3V4amax_intAainfix &lt;=amin_intainfix -V3V4ainfix &lt;=V4V3Iainfix &lt;=V12V3Aainfix &lt;=V4V12Iainfix =agetV1V12V2Iainfix &lt;V12V0Aainfix &lt;=c0V12FAainfix &lt;V3V0Aainfix &lt;=c0V4FAainfix &lt;=V13ainfix -V0c1Aainfix &lt;=c0V13Iainfix =agetV1V13V2Iainfix &lt;V13V0Aainfix &lt;=c0V13FAainfix &lt;ainfix -V0c1V0Aainfix &lt;=c0c0Aainfix &lt;=ainfix -V0c1amax_intAainfix &lt;=amin_intainfix -V0c1Iainfix &lt;=agetV1V14agetV1V15Iainfix &lt;V15V0Aainfix &lt;=V14V15Aainfix &lt;=c0V14FAainfix &lt;=V0amax_intAainfix &lt;=c0V0F">
<label
name="expl:VC for binary_search"/>
<proof
......
This diff is collapsed.
This source diff could not be displayed because it is too large. You can view the blob instead.
This diff is collapsed.
This source diff could not be displayed because it is too large. You can view the blob instead.
......@@ -65,10 +65,10 @@
locfile="../fill.mlw"
loclnum="25" loccnumb="10" loccnume="14"
expl="VC for fill"
sum="5df68a32d3f9841b38b6a7d3c14662ce"
sum="0b3b1c0d5b82819f85c764c60b0fee14"
proved="true"
expanded="true"
shape="CacontainsV0agetV3V4Iainfix &lt;V4V2Aainfix &lt;=V2V4FAainfix =agetV3V5agetV3V5Iainfix &lt;V5V2Aainfix &lt;=c0V5FAainfix &lt;=V2V1Aainfix &lt;=V2V2aNulliacontainsV0agetV9V11Iainfix &lt;V11V10Aainfix &lt;=V2V11FAainfix =agetV9V12agetV3V12Iainfix &lt;V12V2Aainfix &lt;=c0V12FAainfix &lt;=V10V1Aainfix &lt;=V2V10acontainsV0agetV15V17Iainfix &lt;V17V16Aainfix &lt;=V2V17FAainfix =agetV15V18agetV3V18Iainfix &lt;V18V2Aainfix &lt;=c0V18FAainfix &lt;=V16V1Aainfix &lt;=V2V16IacontainsV8agetV15V19Iainfix &lt;V19V16Aainfix &lt;=V14V19FAainfix =agetV15V20agetV13V20Iainfix &lt;V20V14Aainfix &lt;=c0V20FAainfix &lt;=V16V1Aainfix &lt;=V14V16Aainfix &lt;=c0V1FFAainfix &lt;=V14V1Aainfix &lt;=c0V14Aainfix &lt;asizeV8asizeV0Aainfix &lt;=c0asizeV0Lainfix +V10c1Iainfix =V13asetV9V10V7Aainfix &lt;=c0V1FAainfix &lt;V10V1Aainfix &lt;=c0V10Nainfix =V10V1IacontainsV6agetV9V21Iainfix &lt;V21V10Aainfix &lt;=V2V21FAainfix =agetV9V22agetV3V22Iainfix &lt;V22V2Aainfix &lt;=c0V22FAainfix &lt;=V10V1Aainfix &lt;=V2V10Aainfix &lt;=c0V1FFAainfix &lt;=V2V1Aainfix &lt;=c0V2Aainfix &lt;asizeV6asizeV0Aainfix &lt;=c0asizeV0aNodeVVVV0Iainfix &lt;=V2V1Aainfix &lt;=c0V2Aainfix &lt;=c0V1FF">
shape="CacontainsV0agetV2V4Iainfix &lt;V4V3Aainfix &lt;=V3V4FAainfix =agetV2V5agetV2V5Iainfix &lt;V5V3Aainfix &lt;=c0V5FAainfix &lt;=V3V1Aainfix &lt;=V3V3aNulliacontainsV0agetV9V11Iainfix &lt;V11V10Aainfix &lt;=V3V11FAainfix =agetV9V12agetV2V12Iainfix &lt;V12V3Aainfix &lt;=c0V12FAainfix &lt;=V10V1Aainfix &lt;=V3V10acontainsV0agetV15V17Iainfix &lt;V17V16Aainfix &lt;=V3V17FAainfix =agetV15V18agetV2V18Iainfix &lt;V18V3Aainfix &lt;=c0V18FAainfix &lt;=V16V1Aainfix &lt;=V3V16IacontainsV8agetV15V19Iainfix &lt;V19V16Aainfix &lt;=V14V19FAainfix =agetV15V20agetV13V20Iainfix &lt;V20V14Aainfix &lt;=c0V20FAainfix &lt;=V16V1Aainfix &lt;=V14V16Aainfix &lt;=c0V1FFAainfix &lt;=V14V1Aainfix &lt;=c0V14Aainfix &lt;asizeV8asizeV0Aainfix &lt;=c0asizeV0Lainfix +V10c1Iainfix =V13asetV9V10V7Aainfix &lt;=c0V1FAainfix &lt;V10V1Aainfix &lt;=c0V10Nainfix =V10V1IacontainsV6agetV9V21Iainfix &lt;V21V10Aainfix &lt;=V3V21FAainfix =agetV9V22agetV2V22Iainfix &lt;V22V3Aainfix &lt;=c0V22FAainfix &lt;=V10V1Aainfix &lt;=V3V10Aainfix &lt;=c0V1FFAainfix &lt;=V3V1Aainfix &lt;=c0V3Aainfix &lt;asizeV6asizeV0Aainfix &lt;=c0asizeV0aNodeVVVV0Iainfix &lt;=V3V1Aainfix &lt;=c0V3Aainfix &lt;=c0V1F">
<label
name="expl:VC for fill"/>
<proof
......
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
......@@ -28,10 +28,10 @@
locfile="../array_max.mlw"
loclnum="21" loccnumb="6" loccnume="9"
expl="VC for max"
sum="5ed42e90bbec3cbdc0758b633b7d78a7"
sum="c3ec2b5cc0b8c3ed0c6ab2fadf5dc1bc"
proved="true"
expanded="true"
shape="iainfix &lt;=agetV1V4agetV1V3Iainfix &lt;V4V0Aainfix &lt;=c0V4FAainfix &lt;V3V0Aainfix &lt;=c0V3iainfix &lt;ainfix -V5V3ainfix -V2V3Aainfix &lt;=c0ainfix -V2V3Aainfix &lt;=agetV1V6amaxagetV1V3agetV1V5Iainfix &lt;V6V0Aainfix &lt;V5V6Oainfix &lt;V6V3Aainfix &lt;=c0V6FAainfix &lt;V5V0Aainfix &lt;=V3V5Aainfix &lt;=c0V3Iainfix =V5ainfix -V2c1Fainfix &lt;ainfix -V2V7ainfix -V2V3Aainfix &lt;=c0ainfix -V2V3Aainfix &lt;=agetV1V8amaxagetV1V7agetV1V2Iainfix &lt;V8V0Aainfix &lt;V2V8Oainfix &lt;V8V7Aainfix &lt;=c0V8FAainfix &lt;V2V0Aainfix &lt;=V7V2Aainfix &lt;=c0V7Iainfix =V7ainfix +V3c1Fainfix &lt;=agetV1V3agetV1V2Aainfix &lt;V3V0Aainfix &lt;=c0V3Aainfix &lt;V2V0Aainfix &lt;=c0V2Nainfix =V3V2Iainfix &lt;=agetV1V9amaxagetV1V3agetV1V2Iainfix &lt;V9V0Aainfix &lt;V2V9Oainfix &lt;V9V3Aainfix &lt;=c0V9FAainfix &lt;V2V0Aainfix &lt;=V3V2Aainfix &lt;=c0V3FAainfix &lt;=agetV1V10amaxagetV1c0agetV1ainfix -V0c1Iainfix &lt;V10V0Aainfix &lt;ainfix -V0c1V10Oainfix &lt;V10c0Aainfix &lt;=c0V10FAainfix &lt;ainfix -V0c1V0Aainfix &lt;=c0ainfix -V0c1Aainfix &lt;=c0c0Iainfix &lt;c0V0Aainfix &lt;=c0V0FF">
shape="iainfix &lt;=agetV1V4agetV1V3Iainfix &lt;V4V0Aainfix &lt;=c0V4FAainfix &lt;V3V0Aainfix &lt;=c0V3iainfix &lt;ainfix -V5V3ainfix -V2V3Aainfix &lt;=c0ainfix -V2V3Aainfix &lt;=agetV1V6amaxagetV1V3agetV1V5Iainfix &lt;V6V0Aainfix &lt;V5V6Oainfix &lt;V6V3Aainfix &lt;=c0V6FAainfix &lt;V5V0Aainfix &lt;=V3V5Aainfix &lt;=c0V3Iainfix =V5ainfix -V2c1Fainfix &lt;ainfix -V2V7ainfix -V2V3Aainfix &lt;=c0ainfix -V2V3Aainfix &lt;=agetV1V8amaxagetV1V7agetV1V2Iainfix &lt;V8V0Aainfix &lt;V2V8Oainfix &lt;V8V7Aainfix &lt;=c0V8FAainfix &lt;V2V0Aainfix &lt;=V7V2Aainfix &lt;=c0V7Iainfix =V7ainfix +V3c1Fainfix &lt;=agetV1V3agetV1V2Aainfix &lt;V3V0Aainfix &lt;=c0V3Aainfix &lt;V2V0Aainfix &lt;=c0V2Nainfix =V3V2Iainfix &lt;=agetV1V9amaxagetV1V3agetV1V2Iainfix &lt;V9V0Aainfix &lt;V2V9Oainfix &lt;V9V3Aainfix &lt;=c0V9FAainfix &lt;V2V0Aainfix &lt;=V3V2Aainfix &lt;=c0V3FAainfix &lt;=agetV1V10amaxagetV1c0agetV1ainfix -V0c1Iainfix &lt;V10V0Aainfix &lt;ainfix -V0c1V10Oainfix &lt;V10c0Aainfix &lt;=c0V10FAainfix &lt;ainfix -V0c1V0Aainfix &lt;=c0ainfix -V0c1Aainfix &lt;=c0c0Iainfix &lt;c0V0Aainfix &lt;=c0V0F">
<label
name="expl:VC for max"/>
<proof
......
......@@ -35,10 +35,10 @@
locfile="../duplets.mlw"
loclnum="43" loccnumb="6" loccnume="12"
expl="VC for duplet"
sum="b41a7cf20b4225ab9f2aa039728fabc4"
sum="da16a325dd41dd659b5e6a62813bdfb9"
proved="true"
expanded="true"
shape="fINais_dupletV3V5V6INCfaNoneainfix =V7agetV2V5aSomeVV1Iainfix &lt;V6V0Aainfix &lt;V5V6Aainfix &lt;V5ainfix +V4c1Aainfix &lt;=c0V5FAiNais_dupletV3V12V13INCfaNoneainfix =V14agetV2V12aSomeVV1Iainfix &lt;V13V0Aainfix &lt;V12V13Aainfix &lt;V12ainfix +V8c1Aainfix &lt;=c0V12FINais_dupletV3V8V15Iainfix &lt;V15ainfix +V10c1Aainfix &lt;V8V15FAiNais_dupletV3V8V17Iainfix &lt;V17ainfix +V16c1Aainfix &lt;V8V17FNCfaNoneainfix =V20agetV2V18aSomeVV1Aais_dupletV3V18V19Iainfix =V19V16Aainfix =V18V8Fainfix =agetV2V16V9Aainfix &lt;V16V0Aainfix &lt;=c0V16INais_dupletV3V8V21Iainfix &lt;V21V16Aainfix &lt;V8V21FIainfix &lt;=V16V10Aainfix &lt;=V11V16FANais_dupletV3V8V22Iainfix &lt;V22V11Aainfix &lt;V8V22FIainfix &lt;=V11V10ANais_dupletV3V23V24INCfaNoneainfix =V25agetV2V23aSomeVV1Iainfix &lt;V24V0Aainfix &lt;V23V24Aainfix &lt;V23ainfix +V8c1Aainfix &lt;=c0V23FIainfix &gt;V11V10Lainfix +V8c1Lainfix -V0c1Nais_dupletV3V26V27INCfaNoneainfix =V28agetV2V26aSomeVV1Iainfix &lt;V27V0Aainfix &lt;V26V27Aainfix &lt;V26ainfix +V8c1Aainfix &lt;=c0V26FCfaNoneainfix =V29V9aSomeVV1LagetV2V8Aainfix &lt;V8V0Aainfix &lt;=c0V8INais_dupletV3V30V31INCfaNoneainfix =V32agetV2V30aSomeVV1Iainfix &lt;V31V0Aainfix &lt;V30V31Aainfix &lt;V30V8Aainfix &lt;=c0V30FIainfix &lt;=V8V4Aainfix &lt;=c0V8FANais_dupletV3V33V34INCfaNoneainfix =V35agetV2V33aSomeVV1Iainfix &lt;V34V0Aainfix &lt;V33V34Aainfix &lt;V33c0Aainfix &lt;=c0V33FIainfix &lt;=c0V4AfIainfix &gt;c0V4Lainfix -V0c2INCfaNoneainfix =V38agetV2V36aSomeVV1Aais_dupletV3V36V37EAainfix &lt;=c2V0Aainfix &lt;=c0V0Lamk arrayV0V2FF">
shape="fINais_dupletV3V5V6INCfaNoneainfix =V7agetV1V5aSomeVV2Iainfix &lt;V6V0Aainfix &lt;V5V6Aainfix &lt;V5ainfix +V4c1Aainfix &lt;=c0V5FAiNais_dupletV3V12V13INCfaNoneainfix =V14agetV1V12aSomeVV2Iainfix &lt;V13V0Aainfix &lt;V12V13Aainfix &lt;V12ainfix +V8c1Aainfix &lt;=c0V12FINais_dupletV3V8V15Iainfix &lt;V15ainfix +V10c1Aainfix &lt;V8V15FAiNais_dupletV3V8V17Iainfix &lt;V17ainfix +V16c1Aainfix &lt;V8V17FNCfaNoneainfix =V20agetV1V18aSomeVV2Aais_dupletV3V18V19Iainfix =V19V16Aainfix =V18V8Fainfix =agetV1V16V9Aainfix &lt;V16V0Aainfix &lt;=c0V16INais_dupletV3V8V21Iainfix &lt;V21V16Aainfix &lt;V8V21FIainfix &lt;=V16V10Aainfix &lt;=V11V16FANais_dupletV3V8V22Iainfix &lt;V22V11Aainfix &lt;V8V22FIainfix &lt;=V11V10ANais_dupletV3V23V24INCfaNoneainfix =V25agetV1V23aSomeVV2Iainfix &lt;V24V0Aainfix &lt;V23V24Aainfix &lt;V23ainfix +V8c1Aainfix &lt;=c0V23FIainfix &gt;V11V10Lainfix +V8c1Lainfix -V0c1Nais_dupletV3V26V27INCfaNoneainfix =V28agetV1V26aSomeVV2Iainfix &lt;V27V0Aainfix &lt;V26V27Aainfix &lt;V26ainfix +V8c1Aainfix &lt;=c0V26FCfaNoneainfix =V29V9aSomeVV2LagetV1V8Aainfix &lt;V8V0Aainfix &lt;=c0V8INais_dupletV3V30V31INCfaNoneainfix =V32agetV1V30aSomeVV2Iainfix &lt;V31V0Aainfix &lt;V30V31Aainfix &lt;V30V8Aainfix &lt;=c0V30FIainfix &lt;=V8V4Aainfix &lt;=c0V8FANais_dupletV3V33V34INCfaNoneainfix =V35agetV1V33aSomeVV2Iainfix &lt;V34V0Aainfix &lt;V33V34Aainfix &lt;V33c0Aainfix &lt;=c0V33FIainfix &lt;=c0V4AfIainfix &gt;c0V4Lainfix -V0c2INCfaNoneainfix =V38agetV1V36aSomeVV2Aais_dupletV3V36V37EAainfix &lt;=c2V0Aainfix &lt;=c0V0Lamk arrayV0V1F">
<label
name="expl:VC for duplet"/>
<proof
......@@ -63,10 +63,10 @@
locfile="../duplets.mlw"
loclnum="74" loccnumb="6" loccnume="13"
expl="VC for duplets"
sum="5b32d6254bf85f82fcee6b1f8aaf4928"
sum="4658940c6746265baf8a378b2918b363"
proved="true"
expanded="true"
shape="Nainfix =agetV1V3agetV1V5Aais_dupletV2V5V6Aais_dupletV2V3V4INainfix =agetV1V4agetV1V5Aais_dupletV2V5V6FANainfix =agetV1V4agetV1V7Aais_dupletV2V7V8EAainfix &lt;=c2V0Aainfix &lt;V4V0Aainfix &lt;=c0V4Iais_dupletV2V3V4FAais_dupletV2V9V10EAainfix &lt;=c2V0INainfix =agetV1V11agetV1V13Aais_dupletV2V13V14Aais_dupletV2V11V12EAainfix &lt;=c4V0Aainfix &lt;=c0V0Lamk arrayV0V1FF">
shape="Nainfix =agetV1V3agetV1V5Aais_dupletV2V5V6Aais_dupletV2V3V4INainfix =agetV1V4agetV1V5Aais_dupletV2V5V6FANainfix =agetV1V4agetV1V7Aais_dupletV2V7V8EAainfix &lt;=c2V0Aainfix &lt;V4V0Aainfix &lt;=c0V4Iais_dupletV2V3V4FAais_dupletV2V9V10EAainfix &lt;=c2V0INainfix =agetV1V11agetV1V13Aais_dupletV2V13V14Aais_dupletV2V11V12EAainfix &lt;=c4V0Aainfix &lt;=c0V0Lamk arrayV0V1F">
<label
name="expl:VC for duplets"/>
<proof
......
This source diff could not be displayed because it is too large. You can view the blob instead.
(* This file is generated by Why3's Coq driver *)
(* This file is generated by Why3's Coq 8.4 driver *)
(* Beware! Only edit allowed sections below *)
Require Import BuiltIn.
Require Import ZOdiv.
......@@ -6,69 +6,46 @@ Require BuiltIn.
Require int.Int.
Require int.Abs.
Require int.ComputerDivision.
Require option.Option.
Require list.List.
Require list.Mem.
Require map.Map.
(* Why3 assumption *)
Definition unit := unit.
(* Why3 assumption *)
Inductive option
(a:Type) {a_WT:WhyType a} :=
| None : option a
| Some : a -> option a.
Axiom option_WhyType : forall (a:Type) {a_WT:WhyType a}, WhyType (option a).
Existing Instance option_WhyType.
Implicit Arguments None [[a] [a_WT]].
Implicit Arguments Some [[a] [a_WT]].
(* Why3 assumption *)
Inductive list
(a:Type) {a_WT:WhyType a} :=
| Nil : list a
| Cons : a -> (list a) -> list a.
Axiom list_WhyType : forall (a:Type) {a_WT:WhyType a}, WhyType (list a).
Existing Instance list_WhyType.
Implicit Arguments Nil [[a] [a_WT]].
Implicit Arguments Cons [[a] [a_WT]].
(* Why3 assumption *)
Fixpoint mem {a:Type} {a_WT:WhyType a} (x:a) (l:(list a)) {struct l}: Prop :=
match l with
| Nil => False
| (Cons y r) => (x = y) \/ (mem x r)
end.
(* Why3 assumption *)
Inductive array
(a:Type) {a_WT:WhyType a} :=
| mk_array : Z -> (map.Map.map Z a) -> array a.
| mk_array : Z -> (@map.Map.map Z _ a a_WT) -> 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.Map.map Z a) :=
match v with
Definition elts {a:Type} {a_WT:WhyType a} (v:(@array a a_WT)): (@map.Map.map
Z _ a a_WT) := match v with
| (mk_array x x1) => x1
end.
(* Why3 assumption *)
Definition length {a:Type} {a_WT:WhyType a} (v:(array a)): Z :=
Definition length {a:Type} {a_WT:WhyType a} (v:(@array a a_WT)): Z :=
match v with
| (mk_array x x1) => x
end.
(* Why3 assumption *)
Definition get {a:Type} {a_WT:WhyType a} (a1:(array a)) (i:Z): a :=
Definition get {a:Type} {a_WT:WhyType a} (a1:(@array a a_WT)) (i:Z): a :=
(map.Map.get (elts a1) i).
(* Why3 assumption *)
Definition set {a:Type} {a_WT:WhyType a} (a1:(array a)) (i:Z) (v:a): (array
a) := (mk_array (length a1) (map.Map.set (elts a1) i v)).
Definition set {a:Type} {a_WT:WhyType a} (a1:(@array a a_WT)) (i:Z)
(v:a): (@array a a_WT) := (mk_array (length a1) (map.Map.set (elts a1) i
v)).
(* Why3 assumption *)
Definition make {a:Type} {a_WT:WhyType a} (n:Z) (v:a): (array a) :=
(mk_array n (map.Map.const v:(map.Map.map Z a))).
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))).
Axiom key : Type.
Parameter key_WhyType : WhyType key.
......@@ -85,42 +62,43 @@ Axiom bucket_bounds : forall (n:Z), (0%Z < n)%Z -> forall (k:key),
(0%Z <= (bucket k n))%Z /\ ((bucket k n) < n)%Z.
(* Why3 assumption *)
Definition in_data {a:Type} {a_WT:WhyType a} (k:key) (v:a) (d:(array (list
(key* a)%type))): Prop := (mem (k, v) (get d (bucket k (length d)))).
Definition in_data {a:Type} {a_WT:WhyType a} (k:key) (v:a) (d:(@array
(list (key* a)%type) _)): Prop := (list.Mem.mem (k, v) (get d (bucket k
(length d)))).
(* Why3 assumption *)
Definition good_data {a:Type} {a_WT:WhyType a} (k:key) (v:a) (m:(map.Map.map
key (option a))) (d:(array (list (key* a)%type))): Prop := ((map.Map.get m
k) = (Some v)) <-> (in_data k v d).
Definition good_data {a:Type} {a_WT:WhyType a} (k:key) (v:a) (m:(@map.Map.map
key key_WhyType (option a) _)) (d:(@array (list (key* a)%type) _)): Prop :=
((map.Map.get m k) = (Some v)) <-> (in_data k v d).
(* Why3 assumption *)
Definition good_hash {a:Type} {a_WT:WhyType a} (d:(array (list (key*
a)%type))) (i:Z): Prop := forall (k:key) (v:a), (mem (k, v) (get d i)) ->
((bucket k (length d)) = i).
Definition good_hash {a:Type} {a_WT:WhyType a} (d:(@array (list (key*
a)%type) _)) (i:Z): Prop := forall (k:key) (v:a), (list.Mem.mem (k, v)
(get d i)) -> ((bucket k (length d)) = i).
(* Why3 assumption *)
Inductive t
(a:Type) {a_WT:WhyType a} :=
| mk_t : Z -> (array (list (key* a)%type)) -> (map.Map.map key (option
a)) -> t a.
| mk_t : Z -> (@array (list (key* a)%type) _) -> (@map.Map.map
key key_WhyType (option a) _) -> t a.
Axiom t_WhyType : forall (a:Type) {a_WT:WhyType a}, WhyType (t a).
Existing Instance t_WhyType.
Implicit Arguments mk_t [[a] [a_WT]].
(* Why3 assumption *)
Definition view {a:Type} {a_WT:WhyType a} (v:(t a)): (map.Map.map key (option
a)) := match v with
Definition view {a:Type} {a_WT:WhyType a} (v:(@t a a_WT)): (@map.Map.map
key key_WhyType (option a) _) := match v with
| (mk_t x x1 x2) => x2
end.
(* Why3 assumption *)
Definition data {a:Type} {a_WT:WhyType a} (v:(t a)): (array (list (key*
a)%type)) := match v with
Definition data {a:Type} {a_WT:WhyType a} (v:(@t a a_WT)): (@array
(list (key* a)%type) _) := match v with
| (mk_t x x1 x2) => x1
end.
(* Why3 assumption *)
Definition size {a:Type} {a_WT:WhyType a} (v:(t a)): Z :=
Definition size {a:Type} {a_WT:WhyType a} (v:(@t a a_WT)): Z :=
match v with
| (mk_t x x1 x2) => x
end.
......@@ -128,32 +106,30 @@ Definition size {a:Type} {a_WT:WhyType a} (v:(t a)): Z :=
Require Import Why3. Ltac ae := why3 "Alt-Ergo,0.95.1," timelimit 3.
(* Why3 goal *)
Theorem WP_parameter_add : forall {a:Type} {a_WT:WhyType a}, forall (k:key)
(v:a), forall (rho:(map.Map.map key (option a))) (rho1:Z)
(rho2:(map.Map.map Z (list (key* a)%type))), ((((0%Z < rho1)%Z /\
forall (i:Z), ((0%Z <= i)%Z /\ (i < rho1)%Z) -> (good_hash (mk_array rho1
rho2) i)) /\ forall (k1:key) (v1:a), (good_data k1 v1 rho (mk_array rho1
rho2))) /\ (0%Z <= rho1)%Z) -> forall (rho3:Z) (rho4:(map.Map.map Z (list
(key* a)%type))), ((((0%Z < rho3)%Z /\ forall (i:Z), ((0%Z <= i)%Z /\
(i < rho3)%Z) -> (good_hash (mk_array rho3 rho4) i)) /\ forall (k1:key)
(v1:a), (good_data k1 v1 rho (mk_array rho3 rho4))) /\ (0%Z <= rho3)%Z) ->
forall (rho5:(map.Map.map key (option a))) (rho6:(map.Map.map Z (list (key*
a)%type))) (rho7:Z), (((((0%Z < rho3)%Z /\ forall (i:Z), ((0%Z <= i)%Z /\
(i < rho3)%Z) -> (good_hash (mk_array rho3 rho6) i)) /\ forall (k1:key)
(v1:a), (good_data k1 v1 rho5 (mk_array rho3 rho6))) /\ (0%Z <= rho3)%Z) /\
(((map.Map.get rho5 k) = (None :(option a))) /\ forall (k':key),
(~ (k' = k)) -> ((map.Map.get rho5 k') = (map.Map.get rho k')))) ->
let i := (bucket k rho3) in (((0%Z <= i)%Z /\ (i < rho3)%Z) ->
(((0%Z <= i)%Z /\ (i < rho3)%Z) -> forall (o:(map.Map.map Z (list (key*
a)%type))), ((0%Z <= rho3)%Z /\ (o = (map.Map.set rho6 i (Cons (k, v)
(map.Map.get rho6 i))))) -> forall (rho8:Z), (rho8 = (rho7 + 1%Z)%Z) ->
forall (rho9:(map.Map.map key (option a))), (rho9 = (map.Map.set rho5 k
(Some v))) -> forall (i1:Z), ((0%Z <= i1)%Z /\ (i1 < rho3)%Z) -> (good_hash
(mk_array rho3 o) i1))).
(* Why3 intros a a_WT k v rho rho1 rho2 (((h1,h2),h3),h4) rho3 rho4
(((h5,h6),h7),h8) rho5 rho6 rho7 ((((h9,h10),h11),h12),(h13,h14)) i
(h15,h16) (h17,h18) o (h19,h20) rho8 h21 rho9 h22 i1 (h23,h24). *)
intros a a_WT k v rho rho1 rho2 (((h1,h2),h3),h4) rho3 rho4 (((h5,h6),h7),h8)
Theorem WP_parameter_add : forall {a:Type} {a_WT:WhyType a}, forall (h:Z)
(h1:(@map.Map.map Z _ (list (key* a)%type) _)) (h2:(@map.Map.map
key key_WhyType (option a) _)) (k:key) (v:a), ((((0%Z < h)%Z /\
forall (i:Z), ((0%Z <= i)%Z /\ (i < h)%Z) -> (good_hash (mk_array h h1)
i)) /\ forall (k1:key) (v1:a), (good_data k1 v1 h2 (mk_array h h1))) /\
(0%Z <= h)%Z) -> forall (rho:Z) (rho1:(@map.Map.map Z _ (list (key*
a)%type) _)), ((((0%Z < rho)%Z /\ forall (i:Z), ((0%Z <= i)%Z /\
(i < rho)%Z) -> (good_hash (mk_array rho rho1) i)) /\ forall (k1:key)
(v1:a), (good_data k1 v1 h2 (mk_array rho rho1))) /\ (0%Z <= rho)%Z) ->
forall (rho2:(@map.Map.map key key_WhyType (option a) _))
(rho3:(@map.Map.map Z _ (list (key* a)%type) _)) (rho4:Z),
(((((0%Z < rho)%Z /\ forall (i:Z), ((0%Z <= i)%Z /\ (i < rho)%Z) ->
(good_hash (mk_array rho rho3) i)) /\ forall (k1:key) (v1:a), (good_data k1
v1 rho2 (mk_array rho rho3))) /\ (0%Z <= rho)%Z) /\ (((map.Map.get rho2
k) = None) /\ forall (k':key), (~ (k' = k)) -> ((map.Map.get rho2
k') = (map.Map.get h2 k')))) -> let i := (bucket k rho) in
(((0%Z <= i)%Z /\ (i < rho)%Z) -> (((0%Z <= i)%Z /\ (i < rho)%Z) ->
forall (o:(@map.Map.map Z _ (list (key* a)%type) _)), ((0%Z <= rho)%Z /\
(o = (map.Map.set rho3 i (cons (k, v) (map.Map.get rho3 i))))) ->
forall (rho5:Z), (rho5 = (rho4 + 1%Z)%Z) -> forall (rho6:(@map.Map.map
key key_WhyType (option a) _)), (rho6 = (map.Map.set rho2 k (Some v))) ->
forall (i1:Z), ((0%Z <= i1)%Z /\ (i1 < rho)%Z) -> (good_hash (mk_array rho
o) i1))).
intros a a_WT rho rho1 rho2 k v (((h1,h2),h3),h4) rho3 rho4 (((h5,h6),h7),h8)
rho5 rho6 rho7 ((((h9,h10),h11),h12),(h13,h14)) i1 (h15,h16) (h17,h18) o
(h19,h20) rho8 h21 rho9 h22 i (h23,h24).
subst i1.
......
(* This file is generated by Why3's Coq driver *)
(* This file is generated by Why3's Coq 8.4 driver *)
(* Beware! Only edit allowed sections below *)
Require Import BuiltIn.
Require Import ZOdiv.
......@@ -104,28 +104,25 @@ Definition size {a:Type} {a_WT:WhyType a} (v:(@t a a_WT)): Z :=
end.
(* Why3 goal *)
Theorem WP_parameter_find : forall {a:Type} {a_WT:WhyType a}, forall (k:key),
forall (rho:(@map.Map.map key key_WhyType (option a) _)) (rho1:Z)
(rho2:(@map.Map.map Z _ (list (key* a)%type) _)), ((((0%Z < rho1)%Z /\
forall (i:Z), ((0%Z <= i)%Z /\ (i < rho1)%Z) -> (good_hash (mk_array rho1
rho2) i)) /\ forall (k1:key) (v:a), (good_data k1 v rho (mk_array rho1
rho2))) /\ (0%Z <= rho1)%Z) -> let i := (bucket k rho1) in
(((0%Z <= i)%Z /\ (i < rho1)%Z) -> let o := (map.Map.get rho2 i) in
forall (result:(option a)),
Theorem WP_parameter_find : forall {a:Type} {a_WT:WhyType a}, forall (h:Z)
(h1:(@map.Map.map Z _ (list (key* a)%type) _)) (h2:(@map.Map.map
key key_WhyType (option a) _)) (k:key), ((((0%Z < h)%Z /\ forall (i:Z),
((0%Z <= i)%Z /\ (i < h)%Z) -> (good_hash (mk_array h h1) i)) /\
forall (k1:key) (v:a), (good_data k1 v h2 (mk_array h h1))) /\
(0%Z <= h)%Z) -> let i := (bucket k h) in (((0%Z <= i)%Z /\ (i < h)%Z) ->
let o := (map.Map.get h1 i) in forall (result:(option a)),
match result with
| None => forall (v:a), ~ (list.Mem.mem (k, v) o)
| (Some v) => (list.Mem.mem (k, v) o)
end -> (result = (map.Map.get rho k))).
(* Why3 intros a a_WT k rho rho1 rho2 (((h1,h2),h3),h4) i (h5,h6) o result
h7. *)
intros a a_WT k rho rho1 rho2 (((h1,h2),h3),h4) i (h5,h6) o result h7.
end -> (result = (map.Map.get h2 k))).
intros a a_WT rho rho1 rho2 k (((h1,h2),h3),h4) i (h5,h6) o result h7.
subst i.
destruct result.
symmetry.
now apply h3.
specialize (h3 k).
unfold good_data in h3.
destruct (Map.get rho k).
destruct (Map.get rho2 k).
elim (h7 a0).
now apply h3.
easy.
......
(* This file is generated by Why3's Coq driver *)
(* This file is generated by Why3's Coq 8.4 driver *)
(* Beware! Only edit allowed sections below *)
Require Import BuiltIn.
Require Import ZOdiv.
......@@ -6,69 +6,46 @@ Require BuiltIn.
Require int.Int.
Require int.Abs.
Require int.ComputerDivision.
Require option.Option.
Require list.List.
Require list.Mem.
Require map.Map.
(* Why3 assumption *)
Definition unit := unit.
(* Why3 assumption *)
Inductive option
(a:Type) {a_WT:WhyType a} :=
| None : option a
| Some : a -> option a.
Axiom option_WhyType : forall (a:Type) {a_WT:WhyType a}, WhyType (option a).
Existing Instance option_WhyType.
Implicit Arguments None [[a] [a_WT]].
Implicit Arguments Some [[a] [a_WT]].
(* Why3 assumption *)
Inductive list
(a:Type) {a_WT:WhyType a} :=
| Nil : list a
| Cons : a -> (list a) -> list a.
Axiom list_WhyType : forall (a:Type) {a_WT:WhyType a}, WhyType (list a).
Existing Instance list_WhyType.
Implicit Arguments Nil [[a] [a_WT]].
Implicit Arguments Cons [[a] [a_WT]].
(* Why3 assumption *)
Fixpoint mem {a:Type} {a_WT:WhyType a} (x:a) (l:(list a)) {struct l}: Prop :=
match l with
| Nil => False
| (Cons y r) => (x = y) \/ (mem x r)
end.
(* Why3 assumption *)
Inductive array
(a:Type) {a_WT:WhyType a} :=
| mk_array : Z -> (map.Map.map Z a) -> array a.
| mk_array : Z -> (@map.Map.map Z _ a a_WT) -> 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.Map.map Z a) :=
match v with
Definition elts {a:Type} {a_WT:WhyType a} (v:(@array a a_WT)): (@map.Map.map
Z _ a a_WT) := match v with
| (mk_array x x1) => x1
end.
(* Why3 assumption *)
Definition length {a:Type} {a_WT:WhyType a} (v:(array a)): Z :=
Definition length {a:Type} {a_WT:WhyType a} (v:(@array a a_WT)): Z :=
match v with
| (mk_array x x1) => x
end.
(* Why3 assumption *)
Definition get {a:Type} {a_WT:WhyType a} (a1:(array a)) (i:Z): a :=
Definition get {a:Type} {a_WT:WhyType a} (a1:(@array a a_WT)) (i:Z): a :=
(map.Map.get (elts a1) i).
(* Why3 assumption *)
Definition set {a:Type} {a_WT:WhyType a} (a1:(array a)) (i:Z) (v:a): (array
a) := (mk_array (length a1) (map.Map.set (elts a1) i v)).
Definition set {a:Type} {a_WT:WhyType a} (a1:(@array a a_WT)) (i:Z)
(v:a): (@array a a_WT) := (mk_array (length a1) (map.Map.set (elts a1) i
v)).
(* Why3 assumption *)
Definition make {a:Type} {a_WT:WhyType a} (n:Z) (v:a): (array a) :=
(mk_array n (map.Map.const v:(map.Map.map Z a))).
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))).
Axiom key : Type.
Parameter key_WhyType : WhyType key.
......@@ -85,72 +62,70 @@ Axiom bucket_bounds : forall (n:Z), (0%Z < n)%Z -> forall (k:key),
(0%Z <= (bucket k n))%Z /\ ((bucket k n) < n)%Z.
(* Why3 assumption *)
Definition in_data {a:Type} {a_WT:WhyType a} (k:key) (v:a) (d:(array (list
(key* a)%type))): Prop := (mem (k, v) (get d (bucket k (length d)))).
Definition in_data {a:Type} {a_WT:WhyType a} (k:key) (v:a) (d:(@array
(list (key* a)%type) _)): Prop := (list.Mem.mem (k, v) (get d (bucket k
(length d)))).
(* Why3 assumption *)
Definition good_data {a:Type} {a_WT:WhyType a} (k:key) (v:a) (m:(map.Map.map
key (option a))) (d:(array (list (key* a)%type))): Prop := ((map.Map.get m
k) = (Some v)) <-> (in_data k v d).
Definition good_data {a:Type} {a_WT:WhyType a} (k:key) (v:a) (m:(@map.Map.map
key key_WhyType (option a) _)) (d:(@array (list (key* a)%type) _)): Prop :=
((map.Map.get m k) = (Some v)) <-> (in_data k v d).
(* Why3 assumption *)
Definition good_hash {a:Type} {a_WT:WhyType a} (d:(array (list (key*
a)%type))) (i:Z): Prop := forall (k:key) (v:a), (mem (k, v) (get d i)) ->
((bucket k (length d)) = i).
Definition good_hash {a:Type} {a_WT:WhyType a} (d:(@array (list (key*
a)%type) _)) (i:Z): Prop := forall (k:key) (v:a), (list.Mem.mem (k, v)
(get d i)) -> ((bucket k (length d)) = i).
(* Why3 assumption *)
Inductive t
(a:Type) {a_WT:WhyType a} :=
| mk_t : Z -> (array (list (key* a)%type)) -> (map.Map.map key (option
a)) -> t a.
| mk_t : Z -> (@array (list (key* a)%type) _) -> (@map.Map.map
key key_WhyType (option a) _) -> t a.
Axiom t_WhyType : forall (a:Type) {a_WT:WhyType a}, WhyType (t a).
Existing Instance t_WhyType.
Implicit Arguments mk_t [[a] [a_WT]].
(* Why3 assumption *)
Definition view {a:Type} {a_WT:WhyType a} (v:(t a)): (map.Map.map key (option
a)) := match v with
Definition view {a:Type} {a_WT:WhyType a} (v:(@t a a_WT)): (@map.Map.map
key key_WhyType (option a) _) := match v with
| (mk_t x x1 x2) => x2
end.
(* Why3 assumption *)
Definition data {a:Type} {a_WT:WhyType a} (v:(t a)): (array (list (key*
a)%type)) := match v with
Definition data {a:Type} {a_WT:WhyType a} (v:(@t a a_WT)): (@array
(list (key* a)%type) _) := match v with
| (mk_t x x1 x2) => x1
end.
(* Why3 assumption *)
Definition size {a:Type} {a_WT:WhyType a} (v:(t a)): Z :=
Definition size {a:Type} {a_WT:WhyType a} (v:(@t a a_WT)): Z :=
match v with
| (mk_t x x1 x2) => x
end.
(* Why3 goal *)
Theorem WP_parameter_remove : forall {a:Type} {a_WT:WhyType a},
forall (k:key), forall (rho:(map.Map.map key (option a))) (rho1:Z)
(rho2:(map.Map.map Z (list (key* a)%type))), ((((0%Z < rho1)%Z /\
forall (i:Z), ((0%Z <= i)%Z /\ (i < rho1)%Z) -> (good_hash (mk_array rho1
rho2) i)) /\ forall (k1:key) (v:a), (good_data k1 v rho (mk_array rho1