Commit 7a7fccd6 authored by Andrei Paskevich's avatar Andrei Paskevich

update sessions

parent d2cc224b
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 @@ ...@@ -24,10 +24,10 @@
locfile="../arm.mlw" locfile="../arm.mlw"
loclnum="16" loccnumb="6" loccnume="20" loclnum="16" loccnumb="6" loccnume="20"
expl="VC for insertion_sort" expl="VC for insertion_sort"
sum="7748fd507776784f81c6745ae3a11c7f" sum="b316e30c82ef0fd3831a4b3ad8e0525d"
proved="false" proved="false"
expanded="false" expanded="false"
shape="iainfix <=V5c10iainfix <agetV13V11agetV13ainfix -V11c1ainfix <V18V11Aainfix <=c0V11Aainfix <=ainfix *c2V15ainfix +ainfix *ainfix -V5c2ainfix -V5c1ainfix *c2ainfix -V5V18Aainvamk arrayV0V17Aainfix <=V18V5Aainfix <=c1V18Iainfix =V18ainfix -V11c1FIainfix =V17asetV16ainfix -V11c1agetV13V11FAainfix <ainfix -V11c1V0Aainfix <=c0ainfix -V11c1Iainfix =V16asetV13V11agetV13ainfix -V11c1FAainfix <V11V0Aainfix <=c0V11Aainfix <ainfix -V11c1V0Aainfix <=c0ainfix -V11c1Aainfix <V11V0Aainfix <=c0V11Iainfix =V15ainfix +V12c1Fainfix <ainfix -c10V19ainfix -c10V5Aainfix <=c0ainfix -c10V5Aainfix <=ainfix *c2V12ainfix *ainfix -V19c2ainfix -V19c1Aainfix =V10ainfix -V19c2AainvV14Aainfix <=V19c11Aainfix <=c2V19Iainfix =V19ainfix +V5c1FAainfix <V11V0Aainfix <=c0V11Aainfix <ainfix -V11c1V0Aainfix <=c0ainfix -V11c1Iainfix <=ainfix *c2V12ainfix +ainfix *ainfix -V5c2ainfix -V5c1ainfix *c2ainfix -V5V11AainvV14Aainfix <=V11V5Aainfix <=c1V11Lamk arrayV0V13FAainfix <=ainfix *c2V6ainfix +ainfix *ainfix -V5c2ainfix -V5c1ainfix *c2ainfix -V5V5AainvV9Aainfix <=V5V5Aainfix <=c1V5Iainfix =V10ainfix +V7c1Fainfix <=V6c45Aainfix =V7c9Iainfix <=ainfix *c2V6ainfix *ainfix -V5c2ainfix -V5c1Aainfix =V7ainfix -V5c2AainvV9Aainfix <=V5c11Aainfix <=c2V5Lamk arrayV0V8FAainfix <=ainfix *c2V1ainfix *ainfix -c2c2ainfix -c2c1Aainfix =V2ainfix -c2c2AainvV4Aainfix <=c2c11Aainfix <=c2c2Iainfix =V1c0Aainfix =V2c0AainvV4Lamk arrayV0V3FF"> shape="iainfix <=V5c10iainfix <agetV13V11agetV13ainfix -V11c1ainfix <V18V11Aainfix <=c0V11Aainfix <=ainfix *c2V15ainfix +ainfix *ainfix -V5c2ainfix -V5c1ainfix *c2ainfix -V5V18Aainvamk arrayV0V17Aainfix <=V18V5Aainfix <=c1V18Iainfix =V18ainfix -V11c1FIainfix =V17asetV16ainfix -V11c1agetV13V11Aainfix <=c0V0FAainfix <ainfix -V11c1V0Aainfix <=c0ainfix -V11c1Iainfix =V16asetV13V11agetV13ainfix -V11c1Aainfix <=c0V0FAainfix <V11V0Aainfix <=c0V11Aainfix <ainfix -V11c1V0Aainfix <=c0ainfix -V11c1Aainfix <V11V0Aainfix <=c0V11Iainfix =V15ainfix +V12c1Fainfix <ainfix -c10V19ainfix -c10V5Aainfix <=c0ainfix -c10V5Aainfix <=ainfix *c2V12ainfix *ainfix -V19c2ainfix -V19c1Aainfix =V10ainfix -V19c2AainvV14Aainfix <=V19c11Aainfix <=c2V19Iainfix =V19ainfix +V5c1FAainfix <V11V0Aainfix <=c0V11Aainfix <ainfix -V11c1V0Aainfix <=c0ainfix -V11c1Aainfix <=c0V0Iainfix <=ainfix *c2V12ainfix +ainfix *ainfix -V5c2ainfix -V5c1ainfix *c2ainfix -V5V11AainvV14Aainfix <=V11V5Aainfix <=c1V11Lamk arrayV0V13FAainfix <=ainfix *c2V6ainfix +ainfix *ainfix -V5c2ainfix -V5c1ainfix *c2ainfix -V5V5AainvV9Aainfix <=V5V5Aainfix <=c1V5Iainfix =V10ainfix +V7c1Fainfix <=V6c45Aainfix =V7c9Aainfix <=c0V0Iainfix <=ainfix *c2V6ainfix *ainfix -V5c2ainfix -V5c1Aainfix =V7ainfix -V5c2AainvV9Aainfix <=V5c11Aainfix <=c2V5Lamk arrayV0V8FAainfix <=ainfix *c2V1ainfix *ainfix -c2c2ainfix -c2c1Aainfix =V2ainfix -c2c2AainvV4Aainfix <=c2c11Aainfix <=c2c2Iainfix =V1c0Aainfix =V2c0AainvV4Aainfix <=c0V0Lamk arrayV0V3FF">
<label <label
name="expl:VC for insertion_sort"/> name="expl:VC for insertion_sort"/>
</goal> </goal>
......
...@@ -24,10 +24,10 @@ ...@@ -24,10 +24,10 @@
locfile="../assigning_meanings_to_programs.mlw" locfile="../assigning_meanings_to_programs.mlw"
loclnum="12" loccnumb="6" loccnume="9" loclnum="12" loccnumb="6" loccnume="9"
expl="VC for sum" expl="VC for sum"
sum="00e2802392a17c1b774dc7fe33cef4a1" sum="ffd9a7dd39188363294776b2c47e64ce"
proved="true" proved="true"
expanded="true" expanded="true"
shape="iainfix &lt;=V4V1ainfix &lt;ainfix -V1V6ainfix -V1V4Aainfix &lt;=c0ainfix -V1V4Aainfix =V5asumV2c1V6Aainfix &lt;=V6ainfix +V1c1Aainfix &lt;=c1V6Iainfix =V6ainfix +V4c1FIainfix =V5ainfix +V3agetV2V4FAainfix &lt;V4V0Aainfix &lt;=c0V4ainfix =V3asumV2c1ainfix +V1c1Iainfix =V3asumV2c1V4Aainfix &lt;=V4ainfix +V1c1Aainfix &lt;=c1V4FAainfix =c0asumV2c1c1Aainfix &lt;=c1ainfix +V1c1Aainfix &lt;=c1c1Iainfix &lt;V1V0Aainfix &lt;=c0V1FF"> shape="iainfix &lt;=V4V1ainfix &lt;ainfix -V1V6ainfix -V1V4Aainfix &lt;=c0ainfix -V1V4Aainfix =V5asumV2c1V6Aainfix &lt;=V6ainfix +V1c1Aainfix &lt;=c1V6Iainfix =V6ainfix +V4c1FIainfix =V5ainfix +V3agetV2V4FAainfix &lt;V4V0Aainfix &lt;=c0V4ainfix =V3asumV2c1ainfix +V1c1Iainfix =V3asumV2c1V4Aainfix &lt;=V4ainfix +V1c1Aainfix &lt;=c1V4FAainfix =c0asumV2c1c1Aainfix &lt;=c1ainfix +V1c1Aainfix &lt;=c1c1Iainfix &lt;V1V0Aainfix &lt;=c0V1Aainfix &lt;=c0V0FF">
<label <label
name="expl:VC for sum"/> name="expl:VC for sum"/>
<proof <proof
......
...@@ -24,10 +24,10 @@ ...@@ -24,10 +24,10 @@
locfile="../binary_search.mlw" locfile="../binary_search.mlw"
loclnum="17" loccnumb="6" loccnume="19" loclnum="17" loccnumb="6" loccnume="19"
expl="VC for binary_search" expl="VC for binary_search"
sum="9f60cf065e425aed250128303946138f" sum="7117980790d0ae65ea9a63dcdb93b30e"
proved="true" proved="true"
expanded="true" expanded="true"
shape="iainfix &lt;=V4V3iainfix &lt;agetV2ainfix +V4adivainfix -V3V4c2V1ainfix &lt;ainfix -V3V5ainfix -V3V4Aainfix &lt;=c0ainfix -V3V4Aainfix &lt;=V6V3Aainfix &lt;=V5V6Iainfix =agetV2V6V1Iainfix &lt;V6V0Aainfix &lt;=c0V6FAainfix &lt;V3V0Aainfix &lt;=c0V5Iainfix =V5ainfix +ainfix +V4adivainfix -V3V4c2c1Fiainfix &gt;agetV2ainfix +V4adivainfix -V3V4c2V1ainfix &lt;ainfix -V7V4ainfix -V3V4Aainfix &lt;=c0ainfix -V3V4Aainfix &lt;=V8V7Aainfix &lt;=V4V8Iainfix =agetV2V8V1Iainfix &lt;V8V0Aainfix &lt;=c0V8FAainfix &lt;V7V0Aainfix &lt;=c0V4Iainfix =V7ainfix -ainfix +V4adivainfix -V3V4c2c1Fainfix =agetV2ainfix +V4adivainfix -V3V4c2V1Aainfix &lt;ainfix +V4adivainfix -V3V4c2V0Aainfix &lt;=c0ainfix +V4adivainfix -V3V4c2Aainfix &lt;ainfix +V4adivainfix -V3V4c2V0Aainfix &lt;=c0ainfix +V4adivainfix -V3V4c2Aainfix &lt;ainfix +V4adivainfix -V3V4c2V0Aainfix &lt;=c0ainfix +V4adivainfix -V3V4c2Aainfix &lt;=ainfix +V4adivainfix -V3V4c2V3Aainfix &lt;=V4ainfix +V4adivainfix -V3V4c2ainfix =agetV2V9V1NIainfix &lt;V9V0Aainfix &lt;=c0V9FIainfix &lt;=V10V3Aainfix &lt;=V4V10Iainfix =agetV2V10V1Iainfix &lt;V10V0Aainfix &lt;=c0V10FAainfix &lt;V3V0Aainfix &lt;=c0V4FAainfix &lt;=V11ainfix -V0c1Aainfix &lt;=c0V11Iainfix =agetV2V11V1Iainfix &lt;V11V0Aainfix &lt;=c0V11FAainfix &lt;ainfix -V0c1V0Aainfix &lt;=c0c0Iainfix &lt;=agetV2V12agetV2V13Iainfix &lt;V13V0Aainfix &lt;=V12V13Aainfix &lt;=c0V12FFF"> shape="iainfix &lt;=V4V3iainfix &lt;agetV2ainfix +V4adivainfix -V3V4c2V1ainfix &lt;ainfix -V3V5ainfix -V3V4Aainfix &lt;=c0ainfix -V3V4Aainfix &lt;=V6V3Aainfix &lt;=V5V6Iainfix =agetV2V6V1Iainfix &lt;V6V0Aainfix &lt;=c0V6FAainfix &lt;V3V0Aainfix &lt;=c0V5Iainfix =V5ainfix +ainfix +V4adivainfix -V3V4c2c1Fiainfix &gt;agetV2ainfix +V4adivainfix -V3V4c2V1ainfix &lt;ainfix -V7V4ainfix -V3V4Aainfix &lt;=c0ainfix -V3V4Aainfix &lt;=V8V7Aainfix &lt;=V4V8Iainfix =agetV2V8V1Iainfix &lt;V8V0Aainfix &lt;=c0V8FAainfix &lt;V7V0Aainfix &lt;=c0V4Iainfix =V7ainfix -ainfix +V4adivainfix -V3V4c2c1Fainfix =agetV2ainfix +V4adivainfix -V3V4c2V1Aainfix &lt;ainfix +V4adivainfix -V3V4c2V0Aainfix &lt;=c0ainfix +V4adivainfix -V3V4c2Aainfix &lt;ainfix +V4adivainfix -V3V4c2V0Aainfix &lt;=c0ainfix +V4adivainfix -V3V4c2Aainfix &lt;ainfix +V4adivainfix -V3V4c2V0Aainfix &lt;=c0ainfix +V4adivainfix -V3V4c2Aainfix &lt;=ainfix +V4adivainfix -V3V4c2V3Aainfix &lt;=V4ainfix +V4adivainfix -V3V4c2ainfix =agetV2V9V1NIainfix &lt;V9V0Aainfix &lt;=c0V9FIainfix &lt;=V10V3Aainfix &lt;=V4V10Iainfix =agetV2V10V1Iainfix &lt;V10V0Aainfix &lt;=c0V10FAainfix &lt;V3V0Aainfix &lt;=c0V4FAainfix &lt;=V11ainfix -V0c1Aainfix &lt;=c0V11Iainfix =agetV2V11V1Iainfix &lt;V11V0Aainfix &lt;=c0V11FAainfix &lt;ainfix -V0c1V0Aainfix &lt;=c0c0Iainfix &lt;=agetV2V12agetV2V13Iainfix &lt;V13V0Aainfix &lt;=V12V13Aainfix &lt;=c0V12FAainfix &lt;=c0V0FF">
<label <label
name="expl:VC for binary_search"/> name="expl:VC for binary_search"/>
<proof <proof
...@@ -59,10 +59,10 @@ ...@@ -59,10 +59,10 @@
locfile="../binary_search.mlw" locfile="../binary_search.mlw"
loclnum="60" loccnumb="6" loccnume="19" loclnum="60" loccnumb="6" loccnume="19"
expl="VC for binary_search" expl="VC for binary_search"
sum="16ce454ae5e4d3346ff4a9dd4f84fba0" sum="8bdc6aca362ddf7404a2f2d93ea218ed"
proved="true" proved="true"
expanded="true" expanded="true"
shape="iainfix &lt;=V4V3iainfix &lt;agetV2V5V1ainfix &lt;ainfix -V3V6ainfix -V3V4Aainfix &lt;=c0ainfix -V3V4Aainfix &lt;=V7V3Aainfix &lt;=V6V7Iainfix =agetV2V7V1Iainfix &lt;V7V0Aainfix &lt;=c0V7FAainfix &lt;V3V0Aainfix &lt;=c0V6Iainfix =V6ainfix +V5c1Fiainfix &gt;agetV2V5V1ainfix &lt;ainfix -V8V4ainfix -V3V4Aainfix &lt;=c0ainfix -V3V4Aainfix &lt;=V9V8Aainfix &lt;=V4V9Iainfix =agetV2V9V1Iainfix &lt;V9V0Aainfix &lt;=c0V9FAainfix &lt;V8V0Aainfix &lt;=c0V4Iainfix =V8ainfix -V5c1Fainfix =agetV2V5V1Aainfix &lt;V5V0Aainfix &lt;=c0V5Aainfix &lt;V5V0Aainfix &lt;=c0V5Aainfix &lt;V5V0Aainfix &lt;=c0V5Iainfix &lt;=V5V3Aainfix &lt;=V4V5FAainfix &lt;=V4V3ainfix =agetV2V10V1NIainfix &lt;V10V0Aainfix &lt;=c0V10FIainfix &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;=c0V13FFF"> shape="iainfix &lt;=V4V3iainfix &lt;agetV2V5V1ainfix &lt;ainfix -V3V6ainfix -V3V4Aainfix &lt;=c0ainfix -V3V4Aainfix &lt;=V7V3Aainfix &lt;=V6V7Iainfix =agetV2V7V1Iainfix &lt;V7V0Aainfix &lt;=c0V7FAainfix &lt;V3V0Aainfix &lt;=c0V6Iainfix =V6ainfix +V5c1Fiainfix &gt;agetV2V5V1ainfix &lt;ainfix -V8V4ainfix -V3V4Aainfix &lt;=c0ainfix -V3V4Aainfix &lt;=V9V8Aainfix &lt;=V4V9Iainfix =agetV2V9V1Iainfix &lt;V9V0Aainfix &lt;=c0V9FAainfix &lt;V8V0Aainfix &lt;=c0V4Iainfix =V8ainfix -V5c1Fainfix =agetV2V5V1Aainfix &lt;V5V0Aainfix &lt;=c0V5Aainfix &lt;V5V0Aainfix &lt;=c0V5Aainfix &lt;V5V0Aainfix &lt;=c0V5Iainfix &lt;=V5V3Aainfix &lt;=V4V5FAainfix &lt;=V4V3ainfix =agetV2V10V1NIainfix &lt;V10V0Aainfix &lt;=c0V10FIainfix &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">
<label <label
name="expl:VC for binary_search"/> name="expl:VC for binary_search"/>
<proof <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 *)
(* Beware! Only edit allowed sections below *)
Require Import BuiltIn.
Require BuiltIn.
Require int.Int.
Require map.Map.
(* Why3 assumption *)
Definition unit := unit.
(* Why3 assumption *)
Inductive ref (a:Type) {a_WT:WhyType a} :=
| mk_ref : a -> ref a.
Axiom ref_WhyType : forall (a:Type) {a_WT:WhyType a}, WhyType (ref a).
Existing Instance ref_WhyType.
Implicit Arguments mk_ref [[a] [a_WT]].
(* Why3 assumption *)
Definition contents {a:Type} {a_WT:WhyType a}(v:(ref a)): a :=
match v with
| (mk_ref x) => x
end.
(* Why3 assumption *)
Inductive array (a:Type) {a_WT:WhyType a} :=
| mk_array : Z -> (map.Map.map Z 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.Map.map Z a) :=
match v with
| (mk_array x x1) => x1
end.
(* Why3 assumption *)
Definition length {a:Type} {a_WT:WhyType a}(v:(array a)): 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 :=
(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)).
(* 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))).
(* Why3 assumption *)
Definition decrease1(a:(array Z)): Prop := forall (i:Z), ((0%Z <= i)%Z /\
(i < ((length a) - 1%Z)%Z)%Z) -> (((get a i) - 1%Z)%Z <= (get a
(i + 1%Z)%Z))%Z.
Axiom decrease1_induction : forall (a:(array Z)), (decrease1 a) ->
forall (i:Z) (j:Z), (((0%Z <= i)%Z /\ (i <= j)%Z) /\ (j < (length a))%Z) ->
((((get a i) + i)%Z - j)%Z <= (get a j))%Z.
(* Why3 goal *)
Theorem WP_parameter_search_rec : forall (a:Z) (i:Z), forall (a1:(map.Map.map
Z Z)), let a2 := (mk_array a a1) in (((decrease1 a2) /\ (0%Z <= i)%Z) ->
((i < a)%Z -> (((0%Z <= i)%Z /\ (i < a)%Z) -> ((~ ((map.Map.get a1
i) = 0%Z)) -> (((0%Z <= i)%Z /\ (i < a)%Z) -> ((0%Z < (map.Map.get a1
i))%Z -> (((0%Z <= i)%Z /\ (i < a)%Z) -> let o := (map.Map.get a1 i) in
(((decrease1 a2) /\ (0%Z <= (i + o)%Z)%Z) -> forall (result:Z),
(((result = (-1%Z)%Z) /\ forall (j:Z), (((i + o)%Z <= j)%Z /\ (j < a)%Z) ->
~ ((map.Map.get a1 j) = 0%Z)) \/ ((((i + o)%Z <= result)%Z /\
(result < a)%Z) /\ (((map.Map.get a1 result) = 0%Z) /\ forall (j:Z),
(((i + o)%Z <= j)%Z /\ (j < result)%Z) -> ~ ((map.Map.get a1
j) = 0%Z)))) -> (((result = (-1%Z)%Z) /\ forall (j:Z), ((i <= j)%Z /\
(j < a)%Z) -> ~ ((map.Map.get a1 j) = 0%Z)) \/ (((i <= result)%Z /\
(result < a)%Z) /\ (((map.Map.get a1 result) = 0%Z) /\ forall (j:Z),
((i <= j)%Z /\ (j < result)%Z) -> ~ ((map.Map.get a1 j) = 0%Z)))))))))))).
Proof.
intuition.
intuition.
left; intuition.
destruct (Z_lt_le_dec j (i + Map.get a1 i)) as [case|case].
generalize (decrease1_induction (mk_array a a1) H5 i j); unfold get; simpl; intuition.
apply H14 with j; auto.
right; intuition.
destruct (Z_lt_le_dec j (i + Map.get a1 i)) as [case|case].
generalize (decrease1_induction (mk_array a a1) H5 i j); unfold get; simpl; intuition.
apply H16 with j; auto.
Qed.
This diff is collapsed.
...@@ -4,6 +4,7 @@ Require Import BuiltIn. ...@@ -4,6 +4,7 @@ Require Import BuiltIn.
Require BuiltIn. Require BuiltIn.
Require int.Int. Require int.Int.
Require int.MinMax. Require int.MinMax.
Require map.Map.
(* Why3 assumption *) (* Why3 assumption *)
Definition unit := unit. Definition unit := unit.
...@@ -155,40 +156,15 @@ Definition contents {a:Type} {a_WT:WhyType a}(v:(ref a)): a := ...@@ -155,40 +156,15 @@ Definition contents {a:Type} {a_WT:WhyType a}(v:(ref a)): a :=
| (mk_ref x) => x | (mk_ref x) => x
end. end.
Axiom map : forall (a:Type) {a_WT:WhyType a} (b:Type) {b_WT:WhyType b}, Type.
Parameter 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 *) (* Why3 assumption *)
Inductive array (a:Type) {a_WT:WhyType a} := Inductive array (a:Type) {a_WT:WhyType a} :=
| mk_array : Z -> (map Z a) -> array a. | mk_array : Z -> (map.Map.map Z a) -> array a.
Axiom array_WhyType : forall (a:Type) {a_WT:WhyType a}, WhyType (array a). Axiom array_WhyType : forall (a:Type) {a_WT:WhyType a}, WhyType (array a).
Existing Instance array_WhyType. Existing Instance array_WhyType.
Implicit Arguments mk_array [[a] [a_WT]]. Implicit Arguments mk_array [[a] [a_WT]].
(* Why3 assumption *) (* Why3 assumption *)
Definition elts {a:Type} {a_WT:WhyType a}(v:(array a)): (map Z a) := Definition elts {a:Type} {a_WT:WhyType a}(v:(array a)): (map.Map.map Z a) :=
match v with match v with
| (mk_array x x1) => x1 | (mk_array x x1) => x1
end. end.
...@@ -200,16 +176,16 @@ Definition length1 {a:Type} {a_WT:WhyType a}(v:(array a)): Z := ...@@ -200,16 +176,16 @@ Definition length1 {a:Type} {a_WT:WhyType a}(v:(array a)): Z :=
end. end.
(* Why3 assumption *) (* Why3 assumption *)
Definition get1 {a:Type} {a_WT:WhyType a}(a1:(array a)) (i:Z): a := Definition get {a:Type} {a_WT:WhyType a}(a1:(array a)) (i:Z): a :=
(get (elts a1) i). (map.Map.get (elts a1) i).
(* Why3 assumption *) (* Why3 assumption *)
Definition set1 {a:Type} {a_WT:WhyType a}(a1:(array a)) (i:Z) (v:a): (array Definition set {a:Type} {a_WT:WhyType a}(a1:(array a)) (i:Z) (v:a): (array
a) := (mk_array (length1 a1) (set (elts a1) i v)). a) := (mk_array (length1 a1) (map.Map.set (elts a1) i v)).
(* Why3 assumption *) (* Why3 assumption *)
Definition make {a:Type} {a_WT:WhyType a}(n:Z) (v:a): (array a) := Definition make {a:Type} {a_WT:WhyType a}(n:Z) (v:a): (array a) :=
(mk_array n (const v:(map Z a))). (mk_array n (map.Map.const v:(map.Map.map Z a))).
Parameter suffix: (array char) -> Z -> (list char). Parameter suffix: (array char) -> Z -> (list char).
...@@ -217,7 +193,7 @@ Axiom suffix_nil : forall (a:(array char)), ((suffix a ...@@ -217,7 +193,7 @@ Axiom suffix_nil : forall (a:(array char)), ((suffix a
(length1 a)) = (Nil :(list char))). (length1 a)) = (Nil :(list char))).
Axiom suffix_cons : forall (a:(array char)) (i:Z), ((0%Z <= i)%Z /\ Axiom suffix_cons : forall (a:(array char)) (i:Z), ((0%Z <= i)%Z /\
(i < (length1 a))%Z) -> ((suffix a i) = (Cons (get1 a i) (suffix a (i < (length1 a))%Z) -> ((suffix a i) = (Cons (get a i) (suffix a
(i + 1%Z)%Z))). (i + 1%Z)%Z))).
Axiom suffix_length : forall (a:(array char)) (i:Z), ((0%Z <= i)%Z /\ Axiom suffix_length : forall (a:(array char)) (i:Z), ((0%Z <= i)%Z /\
...@@ -232,21 +208,24 @@ Ltac ae := why3 "alt-ergo" timelimit 3. ...@@ -232,21 +208,24 @@ Ltac ae := why3 "alt-ergo" timelimit 3.
Open Scope Z_scope. Open Scope Z_scope.
(* Why3 goal *) (* Why3 goal *)
Theorem WP_parameter_distance : forall (w1:Z) (w2:Z), forall (w21:(map Z Theorem WP_parameter_distance : forall (w1:Z) (w2:Z),
char)) (w11:(map Z char)), let w22 := (mk_array w2 w21) in let w12 := forall (w21:(map.Map.map Z char)) (w11:(map.Map.map Z char)), let w22 :=
(mk_array w1 w11) in (((0%Z <= w1)%Z /\ (0%Z <= w2)%Z) -> (mk_array w2 w21) in let w12 := (mk_array w1 w11) in (((0%Z <= w1)%Z /\
((0%Z <= (w2 + 1%Z)%Z)%Z -> ((0%Z <= w2)%Z -> forall (t:(map Z Z)), (0%Z <= w2)%Z) -> ((0%Z <= (w2 + 1%Z)%Z)%Z -> ((0%Z <= (w2 + 1%Z)%Z)%Z ->
(forall (j:Z), ((0%Z <= j)%Z /\ (j < (w2 + 1%Z)%Z)%Z) -> ((get t ((0%Z <= w2)%Z -> forall (t:(map.Map.map Z Z)), (forall (j:Z),
j) = (w2 - j)%Z)) -> ((0%Z <= (w1 - 1%Z)%Z)%Z -> forall (t1:(map Z Z)), ((0%Z <= j)%Z /\ (j < (w2 + 1%Z)%Z)%Z) -> ((map.Map.get t
forall (i:Z), ((i <= (w1 - 1%Z)%Z)%Z /\ (0%Z <= i)%Z) -> ((forall (j:Z), j) = (w2 - j)%Z)) -> ((0%Z <= (w1 - 1%Z)%Z)%Z -> forall (t1:(map.Map.map Z
((0%Z <= j)%Z /\ (j <= w2)%Z) -> (min_dist (suffix w12 (i + 1%Z)%Z) Z)), forall (i:Z), ((i <= (w1 - 1%Z)%Z)%Z /\ (0%Z <= i)%Z) ->
(suffix w22 j) (get t1 j))) -> (((0%Z <= w2)%Z /\ (w2 < (w2 + 1%Z)%Z)%Z) -> ((forall (j:Z), ((0%Z <= j)%Z /\ (j <= w2)%Z) -> (min_dist (suffix w12
(i + 1%Z)%Z) (suffix w22 j) (map.Map.get t1 j))) ->
(((0%Z <= (w2 + 1%Z)%Z)%Z /\ ((0%Z <= w2)%Z /\ (w2 < (w2 + 1%Z)%Z)%Z)) ->
(((0%Z <= w2)%Z /\ (w2 < (w2 + 1%Z)%Z)%Z) -> (((0%Z <= w2)%Z /\ (((0%Z <= w2)%Z /\ (w2 < (w2 + 1%Z)%Z)%Z) -> (((0%Z <= w2)%Z /\
(w2 < (w2 + 1%Z)%Z)%Z) -> forall (t2:(map Z Z)), (t2 = (set t1 w2 ((get t1 (w2 < (w2 + 1%Z)%Z)%Z) -> forall (t2:(map.Map.map Z Z)),
w2) + 1%Z)%Z)) -> (((w2 - 1%Z)%Z < 0%Z)%Z -> forall (j:Z), ((0%Z <= j)%Z /\ ((0%Z <= (w2 + 1%Z)%Z)%Z /\ (t2 = (map.Map.set t1 w2 ((map.Map.get t1
(j <= w2)%Z) -> (min_dist (suffix w12 ((i - 1%Z)%Z + 1%Z)%Z) (suffix w22 j) w2) + 1%Z)%Z))) -> (((w2 - 1%Z)%Z < 0%Z)%Z -> forall (j:Z),
(get t2 j))))))))))). ((0%Z <= j)%Z /\ (j <= w2)%Z) -> (min_dist (suffix w12
intros w1 w2 w21 w11 w22 w12 (h1,h2) h3 h4 t h5 h6 t1 i (h7,h8) h9 (h10,h11) ((i - 1%Z)%Z + 1%Z)%Z) (suffix w22 j) (map.Map.get t2 j)))))))))))).
intros w1 w2 w21 w11 w22 w12 (h1,h2) h3 h4 _ t h5 h6 t1 i (h7,h8) h9 (h10,h11)
(h12,h13) (h14,h15) t2 h16 h17 j (h18,h19). (h12,h13) (h14,h15) t2 h16 h17 j (h18,h19).
replace (i-1+1) with i by omega. replace (i-1+1) with i by omega.
rewrite suffix_cons. rewrite suffix_cons.
......
...@@ -207,32 +207,35 @@ Definition min_suffix(a1:(array char)) (a2:(array char)) (i:Z) (j:Z) ...@@ -207,32 +207,35 @@ Definition min_suffix(a1:(array char)) (a2:(array char)) (i:Z) (j:Z)
Theorem WP_parameter_distance : forall (w1:Z) (w2:Z), Theorem WP_parameter_distance : forall (w1:Z) (w2:Z),
forall (w21:(map.Map.map Z char)) (w11:(map.Map.map Z char)), let w22 := forall (w21:(map.Map.map Z char)) (w11:(map.Map.map Z char)), let w22 :=
(mk_array w2 w21) in let w12 := (mk_array w1 w11) in (((0%Z <= w1)%Z /\ (mk_array w2 w21) in let w12 := (mk_array w1 w11) in (((0%Z <= w1)%Z /\
(0%Z <= w2)%Z) -> ((0%Z <= (w2 + 1%Z)%Z)%Z -> ((0%Z <= w2)%Z -> (0%Z <= w2)%Z) -> ((0%Z <= (w2 + 1%Z)%Z)%Z -> ((0%Z <= (w2 + 1%Z)%Z)%Z ->
forall (t:(map.Map.map Z Z)), (forall (j:Z), ((0%Z <= j)%Z /\ ((0%Z <= w2)%Z -> forall (t:(map.Map.map Z Z)), (forall (j:Z),
(j < (w2 + 1%Z)%Z)%Z) -> ((map.Map.get t j) = (w2 - j)%Z)) -> ((0%Z <= j)%Z /\ (j < (w2 + 1%Z)%Z)%Z) -> ((map.Map.get t
((0%Z <= (w1 - 1%Z)%Z)%Z -> forall (t1:(map.Map.map Z Z)), forall (i:Z), j) = (w2 - j)%Z)) -> ((0%Z <= (w1 - 1%Z)%Z)%Z -> forall (t1:(map.Map.map Z
((i <= (w1 - 1%Z)%Z)%Z /\ (0%Z <= i)%Z) -> ((forall (j:Z), ((0%Z <= j)%Z /\ Z)), forall (i:Z), ((i <= (w1 - 1%Z)%Z)%Z /\ (0%Z <= i)%Z) ->
(j <= w2)%Z) -> (min_dist (suffix w12 (i + 1%Z)%Z) (suffix w22 j) ((forall (j:Z), ((0%Z <= j)%Z /\ (j <= w2)%Z) -> (min_dist (suffix w12
(map.Map.get t1 j))) -> (((0%Z <= w2)%Z /\ (w2 < (w2 + 1%Z)%Z)%Z) -> (i + 1%Z)%Z) (suffix w22 j) (map.Map.get t1 j))) ->
(((0%Z <= (w2 + 1%Z)%Z)%Z /\ ((0%Z <= w2)%Z /\ (w2 < (w2 + 1%Z)%Z)%Z)) ->
(((0%Z <= w2)%Z /\ (w2 < (w2 + 1%Z)%Z)%Z) -> (((0%Z <= w2)%Z /\ (((0%Z <= w2)%Z /\ (w2 < (w2 + 1%Z)%Z)%Z) -> (((0%Z <= w2)%Z /\
(w2 < (w2 + 1%Z)%Z)%Z) -> forall (t2:(map.Map.map Z Z)), (w2 < (w2 + 1%Z)%Z)%Z) -> forall (t2:(map.Map.map Z Z)),
(t2 = (map.Map.set t1 w2 ((map.Map.get t1 w2) + 1%Z)%Z)) -> ((0%Z <= (w2 + 1%Z)%Z)%Z /\ (t2 = (map.Map.set t1 w2 ((map.Map.get t1
((0%Z <= (w2 - 1%Z)%Z)%Z -> forall (oldt:Z) (t3:(map.Map.map Z Z)), w2) + 1%Z)%Z))) -> ((0%Z <= (w2 - 1%Z)%Z)%Z -> forall (oldt:Z)
forall (j:Z), ((j <= (w2 - 1%Z)%Z)%Z /\ (0%Z <= j)%Z) -> ((((forall (k:Z), (t3:(map.Map.map Z Z)), forall (j:Z), ((j <= (w2 - 1%Z)%Z)%Z /\
((j < k)%Z /\ (k <= w2)%Z) -> (min_dist (suffix w12 i) (suffix w22 k) (0%Z <= j)%Z) -> ((((forall (k:Z), ((j < k)%Z /\ (k <= w2)%Z) ->
(map.Map.get t3 k))) /\ forall (k:Z), ((0%Z <= k)%Z /\ (k <= j)%Z) -> (min_dist (suffix w12 i) (suffix w22 k) (map.Map.get t3 k))) /\
(min_dist (suffix w12 (i + 1%Z)%Z) (suffix w22 k) (map.Map.get t3 k))) /\ forall (k:Z), ((0%Z <= k)%Z /\ (k <= j)%Z) -> (min_dist (suffix w12
(min_dist (suffix w12 (i + 1%Z)%Z) (suffix w22 (j + 1%Z)%Z) oldt)) -> (i + 1%Z)%Z) (suffix w22 k) (map.Map.get t3 k))) /\ (min_dist (suffix w12
(((0%Z <= j)%Z /\ (j < (w2 + 1%Z)%Z)%Z) -> forall (oldt1:Z), (i + 1%Z)%Z) (suffix w22 (j + 1%Z)%Z) oldt)) ->
(oldt1 = (map.Map.get t3 j)) -> (((0%Z <= j)%Z /\ (j < w2)%Z) -> (((0%Z <= (w2 + 1%Z)%Z)%Z /\ ((0%Z <= j)%Z /\ (j < (w2 + 1%Z)%Z)%Z)) ->
(((0%Z <= i)%Z /\ (i < w1)%Z) -> ((~ ((map.Map.get w11 forall (oldt1:Z), (oldt1 = (map.Map.get t3 j)) -> (((0%Z <= j)%Z /\
(j < w2)%Z) -> (((0%Z <= i)%Z /\ (i < w1)%Z) -> ((~ ((map.Map.get w11
i) = (map.Map.get w21 j))) -> (((0%Z <= (j + 1%Z)%Z)%Z /\ i) = (map.Map.get w21 j))) -> (((0%Z <= (j + 1%Z)%Z)%Z /\
((j + 1%Z)%Z < (w2 + 1%Z)%Z)%Z) -> (((0%Z <= j)%Z /\ ((j + 1%Z)%Z < (w2 + 1%Z)%Z)%Z) -> (((0%Z <= j)%Z /\
(j < (w2 + 1%Z)%Z)%Z) -> (((0%Z <= j)%Z /\ (j < (w2 + 1%Z)%Z)%Z) -> (j < (w2 + 1%Z)%Z)%Z) -> (((0%Z <= j)%Z /\ (j < (w2 + 1%Z)%Z)%Z) ->
forall (t4:(map.Map.map Z Z)), (t4 = (map.Map.set t3 j forall (t4:(map.Map.map Z Z)), ((0%Z <= (w2 + 1%Z)%Z)%Z /\
((Zmin (map.Map.get t3 j) (map.Map.get t3 (j + 1%Z)%Z)) + 1%Z)%Z)) -> (t4 = (map.Map.set t3 j ((Zmin (map.Map.get t3 j) (map.Map.get t3
forall (k:Z), (((j - 1%Z)%Z < k)%Z /\ (k <= w2)%Z) -> (min_dist (suffix w12 (j + 1%Z)%Z)) + 1%Z)%Z))) -> forall (k:Z), (((j - 1%Z)%Z < k)%Z /\
i) (suffix w22 k) (map.Map.get t4 k))))))))))))))))))). (k <= w2)%Z) -> (min_dist (suffix w12 i) (suffix w22 k) (map.Map.get t4
k)))))))))))))))))))).
Proof. Proof.
intuition. intuition.
intuition. intuition.
...@@ -252,17 +255,17 @@ assert (k=j \/ j<k)%Z by omega. intuition. ...@@ -252,17 +255,17 @@ assert (k=j \/ j<k)%Z by omega. intuition.
2: unfold length1; simpl; omega. 2: unfold length1; simpl; omega.
subst. subst.
assert (min_suffix (mk_array w1 w11) (mk_array w2 w21) i (k+1) (Map.get t3 (k+1)))%Z; auto with *. assert (min_suffix (mk_array w1 w11) (mk_array w2 w21) i (k+1) (Map.get t3 (k+1)))%Z; auto with *.
apply H18; auto with *. apply H21; auto with *.
rewrite <- (suffix_cons _ k). rewrite <- (suffix_cons _ k).
subst. subst.
assert (min_suffix (mk_array w1 w11) (mk_array w2 w21) (i + 1) k (Map.get t3 k)); auto with *. assert (min_suffix (mk_array w1 w11) (mk_array w2 w21) (i + 1) k (Map.get t3 k)); auto with *.
apply H23; auto with *. apply H26; auto with *.
unfold length1; simpl; omega. unfold length1; simpl; omega.
(* j<k *) (* j<k *)
subst. subst.
rewrite Map.Select_neq; try omega. rewrite Map.Select_neq; try omega.
assert (min_suffix (mk_array w1 w11) (mk_array w2 w21) i k (Map.get t3 k)); auto with *. assert (min_suffix (mk_array w1 w11) (mk_array w2 w21) i k (Map.get t3 k)); auto with *.
apply H18; auto with *. apply H21; auto with *.
Qed. Qed.
This source diff could not be displayed because it is too large. You can view the blob instead.
...@@ -65,10 +65,10 @@ ...@@ -65,10 +65,10 @@
locfile="../fill.mlw" locfile="../fill.mlw"
loclnum="25" loccnumb="10" loccnume="14" loclnum="25" loccnumb="10" loccnume="14"
expl="VC for fill" expl="VC for fill"
sum="4235fe223126421752857d12549df16f" sum="2c41683326e31d89e21c5359ac913c2e"
proved="true" proved="true"
expanded="true" expanded="true"
shape="CV0aNullacontainsV0agetV3V4Iainfix &lt;V4V2Aainfix &lt;=V2V4FAainfix =agetV3V5agetV3V5Iainfix &lt;V5V2Aainfix &lt;=c0V5FAainfix &lt;=V2V1Aainfix &lt;=V2V2aNodeVVViainfix =V10V1NacontainsV0agetV12V14Iainfix &lt;V14V13Aainfix &lt;=V2V14FAainfix =agetV12V15agetV3V15Iainfix &lt;V15V2Aainfix &lt;=c0V15FAainfix &lt;=V13V1Aainfix &lt;=V2V13IacontainsV8agetV12V16Iainfix &lt;V16V13Aainfix &lt;=ainfix +V10c1V16FAainfix =agetV12V17agetV11V17Iainfix &lt;V17ainfix +V10c1Aainfix &lt;=c0V17FAainfix &lt;=V13V1Aainfix &lt;=ainfix +V10c1V13FFAainfix &lt;=ainfix +V10c1V1Aainfix &lt;=c0ainfix +V10c1Aainfix &lt;asizeV8asizeV0Aainfix &lt;=c0asizeV0Iainfix =V11asetV9V10V7FAainfix &lt;V10V1Aainfix &lt;=c0V10acontainsV0agetV9V18Iainfix &lt;V18V10Aainfix &lt;=V2V18FAainfix =agetV9V19agetV3V19Iainfix &lt;V19V2Aainfix &lt;=c0V19FAainfix &lt;=V10V1Aainfix &lt;=V2V10IacontainsV6agetV9V20Iainfix &lt;V20V10Aainfix &lt;=V2V20FAainfix =agetV9V21agetV3V21Iainfix &lt;V21V2Aainfix &lt;=c0V21FAainfix &lt;=V10V1Aainfix &lt;=V2V10FFAainfix &lt;=V2V1Aainfix &lt;=c0V2Aainfix &lt;asizeV6asizeV0Aainfix &lt;=c0asizeV0Iainfix &lt;=V2V1Aainfix &lt;=c0V2FF"> shape="CV0aNullacontainsV0agetV3V4Iainfix &lt;V4V2Aainfix &lt;=V2V4FAainfix =agetV3V5agetV3V5Iainfix &lt;V5V2Aainfix &lt;=c0V5FAainfix &lt;=V2V1Aainfix &lt;=V2V2aNodeVVViainfix =V10V1NacontainsV0agetV12V14Iainfix &lt;V14V13Aainfix &lt;=V2V14FAainfix =agetV12V15agetV3V15Iainfix &lt;V15V2Aainfix &lt;=c0V15FAainfix &lt;=V13V1Aainfix &lt;=V2V13IacontainsV8agetV12V16Iainfix &lt;V16V13Aainfix &lt;=ainfix +V10c1V16FAainfix =agetV12V17agetV11V17Iainfix &lt;V17ainfix +V10c1Aainfix &lt;=c0V17FAainfix &lt;=V13V1Aainfix &lt;=ainfix +V10c1V13Aainfix &lt;=c0V1FFAainfix &lt;=ainfix +V10c1V1Aainfix &lt;=c0ainfix +V10c1Aainfix &lt;asizeV8asizeV0Aainfix &lt;=c0asizeV0Iainfix =V11asetV9V10V7Aainfix &lt;=c0V1FAainfix &lt;V10V1Aainfix &lt;=c0V10acontainsV0agetV9V18Iainfix &lt;V18V10Aainfix &lt;=V2V18FAainfix =agetV9V19agetV3V19Iainfix &lt;V19V2Aainfix &lt;=c0V19FAainfix &lt;=V10V1Aainfix &lt;=V2V10IacontainsV6agetV9V20Iainfix &lt;V20V10Aainfix &lt;=V2V20FAainfix =agetV9V21agetV3V21Iainfix &lt;V21V2Aainfix &lt;=c0V21FAainfix &lt;=V10V1Aainfix &lt;=V2V10Aainfix &lt;=c0V1FFAainfix &lt;=V2V1Aainfix &lt;=c0V2Aainfix &lt;asizeV6asizeV0Aainfix &lt;=c0asizeV0Iainfix &lt;=V2V1Aainfix &lt;=c0V2Aainfix &lt;=c0V1FF">
<label <label
name="expl:VC for fill"/> name="expl:VC for fill"/>
<proof <proof
......
...@@ -181,28 +181,30 @@ Definition termination(i:Z) (j:Z) (i0:Z) (j0:Z) (r:Z) (a:(array Z)): Prop := ...@@ -181,28 +181,30 @@ Definition termination(i:Z) (j:Z) (i0:Z) (j0:Z) (r:Z) (a:(array Z)): Prop :=
(* Why3 goal *) (* Why3 goal *)
Theorem WP_parameter_find : forall (a:Z), forall (a1:(map.Map.map Z Z)), Theorem WP_parameter_find : forall (a:Z), forall (a1:(map.Map.map Z Z)),
let a2 := (mk_array a a1) in ((a = (usN + 1%Z)%Z) -> forall (n:Z) (m:Z) let a2 := (mk_array a a1) in (((0%Z <= a)%Z /\ (a = (usN + 1%Z)%Z)) ->
(a3:(map.Map.map Z Z)), let a4 := (mk_array a a3) in (((m_invariant m forall (n:Z) (m:Z) (a3:(map.Map.map Z Z)), let a4 := (mk_array a a3) in
a4) /\ ((n_invariant n a4) /\ ((permut a4 a2) /\ ((1%Z <= m)%Z /\ (((m_invariant m a4) /\ ((n_invariant n a4) /\ ((permut a4 a2) /\
(n <= usN)%Z)))) -> ((m < n)%Z -> (((0%Z <= f)%Z /\ (f < a)%Z) -> let r := ((1%Z <= m)%Z /\ (n <= usN)%Z)))) -> ((m < n)%Z -> (((0%Z <= a)%Z /\
(map.Map.get a3 f) in forall (j:Z) (i:Z) (a5:(map.Map.map Z Z)), let a6 := ((0%Z <= f)%Z /\ (f < a)%Z)) -> let r := (map.Map.get a3 f) in forall (j:Z)
(mk_array a a5) in (((i_invariant m n i r a6) /\ ((j_invariant m n j r (i:Z) (a5:(map.Map.map Z Z)), let a6 := (mk_array a a5) in (((i_invariant m
a6) /\ ((m_invariant m a6) /\ ((n_invariant n a6) /\ ((0%Z <= j)%Z /\ n i r a6) /\ ((j_invariant m n j r a6) /\ ((m_invariant m a6) /\
((i <= (usN + 1%Z)%Z)%Z /\ ((termination i j m n r a6) /\ (permut a6 ((n_invariant n a6) /\ ((0%Z <= j)%Z /\ ((i <= (usN + 1%Z)%Z)%Z /\
a2)))))))) -> ((i <= j)%Z -> forall (i1:Z), ((i_invariant m n i1 r a6) /\ ((termination i j m n r a6) /\ (permut a6 a2)))))))) -> ((i <= j)%Z ->
(((i <= i1)%Z /\ (i1 <= n)%Z) /\ (termination i1 j m n r a6))) -> forall (i1:Z), ((i_invariant m n i1 r a6) /\ (((i <= i1)%Z /\
(((0%Z <= i1)%Z /\ (i1 < a)%Z) -> ((~ ((map.Map.get a5 i1) < r)%Z) -> (i1 <= n)%Z) /\ (termination i1 j m n r a6))) -> (((0%Z <= a)%Z /\
((0%Z <= i1)%Z /\ (i1 < a)%Z)) -> ((~ ((map.Map.get a5 i1) < r)%Z) ->
forall (j1:Z), ((j_invariant m n j1 r a6) /\ ((j1 <= j)%Z /\ forall (j1:Z), ((j_invariant m n j1 r a6) /\ ((j1 <= j)%Z /\
((m <= j1)%Z /\ (termination i1 j1 m n r a6)))) -> (((0%Z <= j1)%Z /\ ((m <= j1)%Z /\ (termination i1 j1 m n r a6)))) -> (((0%Z <= j1)%Z /\
(j1 < a)%Z) -> ((~ (r < (map.Map.get a5 j1))%Z) -> ((((map.Map.get a5 (j1 < a)%Z) -> ((~ (r < (map.Map.get a5 j1))%Z) -> ((((map.Map.get a5
j1) <= r)%Z /\ (r <= (map.Map.get a5 i1))%Z) -> ((i1 <= j1)%Z -> j1) <= r)%Z /\ (r <= (map.Map.get a5 i1))%Z) -> ((i1 <= j1)%Z ->
(((0%Z <= i1)%Z /\ (i1 < a)%Z) -> (((0%Z <= j1)%Z /\ (j1 < a)%Z) -> (((0%Z <= i1)%Z /\ (i1 < a)%Z) -> (((0%Z <= j1)%Z /\ (j1 < a)%Z) ->
(((0%Z <= i1)%Z /\ (i1 < a)%Z) -> forall (a7:(map.Map.map Z Z)), (((0%Z <= i1)%Z /\ (i1 < a)%Z) -> forall (a7:(map.Map.map Z Z)),
(a7 = (map.Map.set a5 i1 (map.Map.get a5 j1))) -> (((0%Z <= j1)%Z /\ ((0%Z <= a)%Z /\ (a7 = (map.Map.set a5 i1 (map.Map.get a5 j1)))) ->
(j1 < a)%Z) -> forall (a8:(map.Map.map Z Z)), let a9 := (mk_array a a8) in (((0%Z <= j1)%Z /\ (j1 < a)%Z) -> forall (a8:(map.Map.map Z Z)), let a9 :=
((a8 = (map.Map.set a7 j1 (map.Map.get a5 i1))) -> ((exchange a8 a5 i1 (mk_array a a8) in (((0%Z <= a)%Z /\ (a8 = (map.Map.set a7 j1
j1) -> (((map.Map.get a8 i1) <= r)%Z -> ((r <= (map.Map.get a8 j1))%Z -> (map.Map.get a5 i1)))) -> ((exchange a8 a5 i1 j1) -> (((map.Map.get a8
forall (i2:Z), (i2 = (i1 + 1%Z)%Z) -> forall (j2:Z), (j2 = (j1 - 1%Z)%Z) -> i1) <= r)%Z -> ((r <= (map.Map.get a8 j1))%Z -> forall (i2:Z),
(i2 = (i1 + 1%Z)%Z) -> forall (j2:Z), (j2 = (j1 - 1%Z)%Z) ->
((i_invariant m n i2 r a9) /\ ((j_invariant m n j2 r a9) /\ ((m_invariant m ((i_invariant m n i2 r a9) /\ ((j_invariant m n j2 r a9) /\ ((m_invariant m
a9) /\ ((n_invariant n a9) /\ ((0%Z <= j2)%Z /\ ((i2 <= (usN + 1%Z)%Z)%Z /\ a9) /\ ((n_invariant n a9) /\ ((0%Z <= j2)%Z /\ ((i2 <= (usN + 1%Z)%Z)%Z /\
((termination i2 j2 m n r a9) /\ (permut a9 a2)))))))))))))))))))))))))))). ((termination i2 j2 m n r a9) /\ (permut a9 a2)))))))))))))))))))))))))))).
...@@ -211,7 +213,7 @@ intuition. ...@@ -211,7 +213,7 @@ intuition.
intuition. intuition.
(* i_invariant *) (* i_invariant *)
red; intuition. red; intuition.
red in H20. intuition. red in H22. intuition.
unfold get; simpl. unfold get; simpl.
assert (h: (p < i1 \/ p = i1)%Z) by omega. assert (h: (p < i1 \/ p = i1)%Z) by omega.
destruct h. destruct h.
...@@ -219,8 +221,8 @@ subst a8. ...@@ -219,8 +221,8 @@ subst a8.
rewrite Map.Select_neq; try omega. rewrite Map.Select_neq; try omega.
subst a7. subst a7.
rewrite Map.Select_neq; try omega. rewrite Map.Select_neq; try omega.
red in H20. red in H22.
unfold get in H20; simpl in H20. intuition. unfold get in H22; simpl in H22. intuition.
subst p a8. subst p a8.
assert (h: (i1 = j1 \/ i1 <> j1)%Z) by omega. assert (h: (i1 = j1 \/ i1 <> j1)%Z) by omega.
destruct h. destruct h.
...@@ -230,21 +232,21 @@ rewrite Map.Select_neq; try omega. ...@@ -230,21 +232,21 @@ rewrite Map.Select_neq; try omega.
subst a7. subst a7.
rewrite Map.Select_eq; try omega. rewrite Map.Select_eq; try omega.
unfold get; simpl. unfold get; simpl.
red in H20; unfold get in H20; simpl in H20; intuition. red in H22; unfold get in H22; simpl in H22; intuition.
assert (h: (i1 < j1 \/ i1 = j1)%Z) by omega. destruct h. assert (h: (i1 < j1 \/ i1 = j1)%Z) by omega. destruct h.
exists j1. exists j1.
split. red in H32; omega. split. red in H35; omega.
subst a8; rewrite Map.Select_eq; try omega. subst a8; rewrite Map.Select_eq; try omega.
assert (h: (j1 < n)%Z) by omega. assert (h: (j1 < n)%Z) by omega.
exists (j1+1)%Z. exists (j1+1)%Z.
split. omega. split. omega.