completed proof session for library array

in particular, consistency of ArrayPermut is now ensured
parent 87354afa
This source diff could not be displayed because it is too large. You can view the blob instead.
......@@ -20,7 +20,7 @@
locfile="../algo64.mlw"
loclnum="42" loccnumb="10" loccnume="19"
expl="VC for quicksort"
sum="f043ca9eecd283c33d3aa095f417529e"
sum="e35b0a38cfcc5561e3cdee6d65d70f37"
proved="true"
expanded="true"
shape="iasorted_subV1V2ainfix +V3c1Aapermut_subV4V4V2ainfix +V3c1asorted_subV11V2ainfix +V3c1Aapermut_subV4V12V2ainfix +V3c1Aaqs_partitionV10V12V2V3V6V5c42Iasorted_subV11V6ainfix +V3c1Aapermut_subV10V12V6ainfix +V3c1Aainfix <=c0V0Lamk arrayV0V11FAainfix <V3V0Aainfix <=V6V3Aainfix <=c0V6Aainfix <ainfix -V3V6ainfix -V3V2Aainfix <=c0ainfix -V3V2Aaqs_partitionV8V10V2V3V6V5c42Iasorted_subV9V2ainfix +V5c1Aapermut_subV8V10V2ainfix +V5c1Aainfix <=c0V0Lamk arrayV0V9FAainfix <V5V0Aainfix <=V2V5Aainfix <=c0V2Aainfix <ainfix -V5V2ainfix -V3V2Aainfix <=c0ainfix -V3V2Iainfix >=agetV7V13c42Iainfix <=V13V3Aainfix <=V6V13FAainfix =agetV7V14c42Iainfix <V14V6Aainfix <V5V14FAainfix <=agetV7V15c42Iainfix <=V15V5Aainfix <=V2V15FAapermut_subV4V8V2ainfix +V3c1Aainfix <=V6V3Aainfix <V5V6Aainfix <=V2V5Aainfix <=c0V0Lamk arrayV0V7FAainfix <V3V0Aainfix <V2V3Aainfix <=c0V2ainfix <V2V3Iainfix <V3V0Aainfix <=V2V3Aainfix <=c0V2Aainfix <=c0V0Lamk arrayV0V1F">
......@@ -35,7 +35,7 @@
locfile="../algo64.mlw"
loclnum="42" loccnumb="10" loccnume="19"
expl="1. precondition"
sum="baec3fa427ab9f37e9870b6b2a87406b"
sum="1f818119f549fd3aa39712ef78dab021"
proved="true"
expanded="false"
shape="preconditionainfix <V3V0Aainfix <V2V3Aainfix <=c0V2Iainfix <V2V3Iainfix <V3V0Aainfix <=V2V3Aainfix <=c0V2Aainfix <=c0V0Lamk arrayV0V1F">
......@@ -55,7 +55,7 @@
locfile="../algo64.mlw"
loclnum="42" loccnumb="10" loccnume="19"
expl="2. variant decrease"
sum="61b814478a17acf70c264f5b499fcf68"
sum="c603e9c4679d7be7e14531f5504353b6"
proved="true"
expanded="false"
shape="variant decreaseainfix <ainfix -V5V2ainfix -V3V2Aainfix <=c0ainfix -V3V2Iainfix >=agetV7V9c42Iainfix <=V9V3Aainfix <=V6V9FAainfix =agetV7V10c42Iainfix <V10V6Aainfix <V5V10FAainfix <=agetV7V11c42Iainfix <=V11V5Aainfix <=V2V11FAapermut_subV4V8V2ainfix +V3c1Aainfix <=V6V3Aainfix <V5V6Aainfix <=V2V5Aainfix <=c0V0Lamk arrayV0V7FIainfix <V3V0Aainfix <V2V3Aainfix <=c0V2Iainfix <V2V3Iainfix <V3V0Aainfix <=V2V3Aainfix <=c0V2Aainfix <=c0V0Lamk arrayV0V1F">
......@@ -75,7 +75,7 @@
locfile="../algo64.mlw"
loclnum="42" loccnumb="10" loccnume="19"
expl="3. precondition"
sum="e1bf5835eed6c1a7ce4b27ed2653b028"
sum="776d62f711ad32b74cb6219bae655abf"
proved="true"
expanded="false"
shape="preconditionainfix <V5V0Aainfix <=V2V5Aainfix <=c0V2Iainfix >=agetV7V9c42Iainfix <=V9V3Aainfix <=V6V9FAainfix =agetV7V10c42Iainfix <V10V6Aainfix <V5V10FAainfix <=agetV7V11c42Iainfix <=V11V5Aainfix <=V2V11FAapermut_subV4V8V2ainfix +V3c1Aainfix <=V6V3Aainfix <V5V6Aainfix <=V2V5Aainfix <=c0V0Lamk arrayV0V7FIainfix <V3V0Aainfix <V2V3Aainfix <=c0V2Iainfix <V2V3Iainfix <V3V0Aainfix <=V2V3Aainfix <=c0V2Aainfix <=c0V0Lamk arrayV0V1F">
......@@ -95,7 +95,7 @@
locfile="../algo64.mlw"
loclnum="42" loccnumb="10" loccnume="19"
expl="4. assertion"
sum="d3e70c476739ee31ff1e2a95036a92aa"
sum="0c538e6162e3250c4d1c543725b37a6c"
proved="true"
expanded="false"
shape="assertionaqs_partitionV8V10V2V3V6V5c42Iasorted_subV9V2ainfix +V5c1Aapermut_subV8V10V2ainfix +V5c1Aainfix <=c0V0Lamk arrayV0V9FIainfix <V5V0Aainfix <=V2V5Aainfix <=c0V2Iainfix >=agetV7V11c42Iainfix <=V11V3Aainfix <=V6V11FAainfix =agetV7V12c42Iainfix <V12V6Aainfix <V5V12FAainfix <=agetV7V13c42Iainfix <=V13V5Aainfix <=V2V13FAapermut_subV4V8V2ainfix +V3c1Aainfix <=V6V3Aainfix <V5V6Aainfix <=V2V5Aainfix <=c0V0Lamk arrayV0V7FIainfix <V3V0Aainfix <V2V3Aainfix <=c0V2Iainfix <V2V3Iainfix <V3V0Aainfix <=V2V3Aainfix <=c0V2Aainfix <=c0V0Lamk arrayV0V1F">
......@@ -115,7 +115,7 @@
locfile="../algo64.mlw"
loclnum="42" loccnumb="10" loccnume="19"
expl="5. variant decrease"
sum="5903ec9535586c4861b3d99dcb5d8704"
sum="52c1f43c0f3ca61ec2dbcc10b2dc82e7"
proved="true"
expanded="false"
shape="variant decreaseainfix <ainfix -V3V6ainfix -V3V2Aainfix <=c0ainfix -V3V2Iaqs_partitionV8V10V2V3V6V5c42Iasorted_subV9V2ainfix +V5c1Aapermut_subV8V10V2ainfix +V5c1Aainfix <=c0V0Lamk arrayV0V9FIainfix <V5V0Aainfix <=V2V5Aainfix <=c0V2Iainfix >=agetV7V11c42Iainfix <=V11V3Aainfix <=V6V11FAainfix =agetV7V12c42Iainfix <V12V6Aainfix <V5V12FAainfix <=agetV7V13c42Iainfix <=V13V5Aainfix <=V2V13FAapermut_subV4V8V2ainfix +V3c1Aainfix <=V6V3Aainfix <V5V6Aainfix <=V2V5Aainfix <=c0V0Lamk arrayV0V7FIainfix <V3V0Aainfix <V2V3Aainfix <=c0V2Iainfix <V2V3Iainfix <V3V0Aainfix <=V2V3Aainfix <=c0V2Aainfix <=c0V0Lamk arrayV0V1F">
......@@ -135,7 +135,7 @@
locfile="../algo64.mlw"
loclnum="42" loccnumb="10" loccnume="19"
expl="6. precondition"
sum="b0224b26d7c793c8b9c6e798c4554e08"
sum="196affa0195b238cc77863b613388948"
proved="true"
expanded="false"
shape="preconditionainfix <V3V0Aainfix <=V6V3Aainfix <=c0V6Iaqs_partitionV8V10V2V3V6V5c42Iasorted_subV9V2ainfix +V5c1Aapermut_subV8V10V2ainfix +V5c1Aainfix <=c0V0Lamk arrayV0V9FIainfix <V5V0Aainfix <=V2V5Aainfix <=c0V2Iainfix >=agetV7V11c42Iainfix <=V11V3Aainfix <=V6V11FAainfix =agetV7V12c42Iainfix <V12V6Aainfix <V5V12FAainfix <=agetV7V13c42Iainfix <=V13V5Aainfix <=V2V13FAapermut_subV4V8V2ainfix +V3c1Aainfix <=V6V3Aainfix <V5V6Aainfix <=V2V5Aainfix <=c0V0Lamk arrayV0V7FIainfix <V3V0Aainfix <V2V3Aainfix <=c0V2Iainfix <V2V3Iainfix <V3V0Aainfix <=V2V3Aainfix <=c0V2Aainfix <=c0V0Lamk arrayV0V1F">
......@@ -155,7 +155,7 @@
locfile="../algo64.mlw"
loclnum="42" loccnumb="10" loccnume="19"
expl="7. assertion"
sum="ef1b2c49464f03bc88f8b524e37fe0e7"
sum="b6304fb1a587b252f32f8ba5993eb223"
proved="true"
expanded="false"
shape="assertionaqs_partitionV10V12V2V3V6V5c42Iasorted_subV11V6ainfix +V3c1Aapermut_subV10V12V6ainfix +V3c1Aainfix <=c0V0Lamk arrayV0V11FIainfix <V3V0Aainfix <=V6V3Aainfix <=c0V6Iaqs_partitionV8V10V2V3V6V5c42Iasorted_subV9V2ainfix +V5c1Aapermut_subV8V10V2ainfix +V5c1Aainfix <=c0V0Lamk arrayV0V9FIainfix <V5V0Aainfix <=V2V5Aainfix <=c0V2Iainfix >=agetV7V13c42Iainfix <=V13V3Aainfix <=V6V13FAainfix =agetV7V14c42Iainfix <V14V6Aainfix <V5V14FAainfix <=agetV7V15c42Iainfix <=V15V5Aainfix <=V2V15FAapermut_subV4V8V2ainfix +V3c1Aainfix <=V6V3Aainfix <V5V6Aainfix <=V2V5Aainfix <=c0V0Lamk arrayV0V7FIainfix <V3V0Aainfix <V2V3Aainfix <=c0V2Iainfix <V2V3Iainfix <V3V0Aainfix <=V2V3Aainfix <=c0V2Aainfix <=c0V0Lamk arrayV0V1F">
......@@ -167,7 +167,7 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="2.01"/>
<result status="valid" time="2.76"/>
</proof>
</goal>
<goal
......@@ -175,7 +175,7 @@
locfile="../algo64.mlw"
loclnum="42" loccnumb="10" loccnume="19"
expl="8. postcondition"
sum="5315ed698b5d8ed526953991c4358f71"
sum="b193f4b5ea77b7165cabb8807c6c6572"
proved="true"
expanded="false"
shape="postconditionapermut_subV4V12V2ainfix +V3c1Iaqs_partitionV10V12V2V3V6V5c42Iasorted_subV11V6ainfix +V3c1Aapermut_subV10V12V6ainfix +V3c1Aainfix &lt;=c0V0Lamk arrayV0V11FIainfix &lt;V3V0Aainfix &lt;=V6V3Aainfix &lt;=c0V6Iaqs_partitionV8V10V2V3V6V5c42Iasorted_subV9V2ainfix +V5c1Aapermut_subV8V10V2ainfix +V5c1Aainfix &lt;=c0V0Lamk arrayV0V9FIainfix &lt;V5V0Aainfix &lt;=V2V5Aainfix &lt;=c0V2Iainfix &gt;=agetV7V13c42Iainfix &lt;=V13V3Aainfix &lt;=V6V13FAainfix =agetV7V14c42Iainfix &lt;V14V6Aainfix &lt;V5V14FAainfix &lt;=agetV7V15c42Iainfix &lt;=V15V5Aainfix &lt;=V2V15FAapermut_subV4V8V2ainfix +V3c1Aainfix &lt;=V6V3Aainfix &lt;V5V6Aainfix &lt;=V2V5Aainfix &lt;=c0V0Lamk arrayV0V7FIainfix &lt;V3V0Aainfix &lt;V2V3Aainfix &lt;=c0V2Iainfix &lt;V2V3Iainfix &lt;V3V0Aainfix &lt;=V2V3Aainfix &lt;=c0V2Aainfix &lt;=c0V0Lamk arrayV0V1F">
......@@ -195,7 +195,7 @@
locfile="../algo64.mlw"
loclnum="42" loccnumb="10" loccnume="19"
expl="9. postcondition"
sum="6ebdeca09c4e0b5cb6f7f4ed95839824"
sum="61a4f820061df46df3597a58f9ad22df"
proved="true"
expanded="false"
shape="postconditionasorted_subV11V2ainfix +V3c1Iaqs_partitionV10V12V2V3V6V5c42Iasorted_subV11V6ainfix +V3c1Aapermut_subV10V12V6ainfix +V3c1Aainfix &lt;=c0V0Lamk arrayV0V11FIainfix &lt;V3V0Aainfix &lt;=V6V3Aainfix &lt;=c0V6Iaqs_partitionV8V10V2V3V6V5c42Iasorted_subV9V2ainfix +V5c1Aapermut_subV8V10V2ainfix +V5c1Aainfix &lt;=c0V0Lamk arrayV0V9FIainfix &lt;V5V0Aainfix &lt;=V2V5Aainfix &lt;=c0V2Iainfix &gt;=agetV7V13c42Iainfix &lt;=V13V3Aainfix &lt;=V6V13FAainfix =agetV7V14c42Iainfix &lt;V14V6Aainfix &lt;V5V14FAainfix &lt;=agetV7V15c42Iainfix &lt;=V15V5Aainfix &lt;=V2V15FAapermut_subV4V8V2ainfix +V3c1Aainfix &lt;=V6V3Aainfix &lt;V5V6Aainfix &lt;=V2V5Aainfix &lt;=c0V0Lamk arrayV0V7FIainfix &lt;V3V0Aainfix &lt;V2V3Aainfix &lt;=c0V2Iainfix &lt;V2V3Iainfix &lt;V3V0Aainfix &lt;=V2V3Aainfix &lt;=c0V2Aainfix &lt;=c0V0Lamk arrayV0V1F">
......@@ -215,7 +215,7 @@
locfile="../algo64.mlw"
loclnum="42" loccnumb="10" loccnume="19"
expl="10. postcondition"
sum="f4aaa70b41b128d8f6dd9fed2fa2efcb"
sum="fbd9c334154c5d6e15c0277ed0249b45"
proved="true"
expanded="false"
shape="postconditionapermut_subV4V4V2ainfix +V3c1INainfix &lt;V2V3Iainfix &lt;V3V0Aainfix &lt;=V2V3Aainfix &lt;=c0V2Aainfix &lt;=c0V0Lamk arrayV0V1F">
......@@ -235,7 +235,7 @@
locfile="../algo64.mlw"
loclnum="42" loccnumb="10" loccnume="19"
expl="11. postcondition"
sum="f961cba67d14248c04b5027e2abec1e5"
sum="b9ffe8049897cbb8388bec6a64ebcee2"
proved="true"
expanded="false"
shape="postconditionasorted_subV1V2ainfix +V3c1INainfix &lt;V2V3Iainfix &lt;V3V0Aainfix &lt;=V2V3Aainfix &lt;=c0V2Aainfix &lt;=c0V0Lamk arrayV0V1F">
......@@ -257,7 +257,7 @@
locfile="../algo64.mlw"
loclnum="58" loccnumb="6" loccnume="8"
expl="VC for qs"
sum="620e6ca3e385dbb67091edda8b3f4874"
sum="17f4d68797b4d32c933dc3a0d50d1db8"
proved="true"
expanded="false"
shape="iasorted_subV1c0V0Aapermut_allV2V2asorted_subV4c0V0Aapermut_allV2V5Iasorted_subV4c0ainfix +V3c1Aapermut_subV2V5c0ainfix +V3c1Aainfix &lt;=c0V0Lamk arrayV0V4FAainfix &lt;V3V0Aainfix &lt;=c0V3Aainfix &lt;=c0c0Lainfix -V0c1ainfix &gt;V0c0Iainfix &lt;=c0V0Lamk arrayV0V1F">
......@@ -272,7 +272,7 @@
locfile="../algo64.mlw"
loclnum="58" loccnumb="6" loccnume="8"
expl="1. precondition"
sum="cfeef4869dd91a4c4eaa642d6b6837c8"
sum="eb77a1cc047df2f046733ed7101ffe74"
proved="true"
expanded="false"
shape="preconditionainfix &lt;V3V0Aainfix &lt;=c0V3Aainfix &lt;=c0c0Lainfix -V0c1Iainfix &gt;V0c0Iainfix &lt;=c0V0Lamk arrayV0V1F">
......@@ -292,7 +292,7 @@
locfile="../algo64.mlw"
loclnum="58" loccnumb="6" loccnume="8"
expl="2. postcondition"
sum="dd935033668b4af88b757f7e24d45909"
sum="a7a844ad33c4aeb3c3202614f0177666"
proved="true"
expanded="false"
shape="postconditionapermut_allV2V5Iasorted_subV4c0ainfix +V3c1Aapermut_subV2V5c0ainfix +V3c1Aainfix &lt;=c0V0Lamk arrayV0V4FIainfix &lt;V3V0Aainfix &lt;=c0V3Aainfix &lt;=c0c0Lainfix -V0c1Iainfix &gt;V0c0Iainfix &lt;=c0V0Lamk arrayV0V1F">
......@@ -312,7 +312,7 @@
locfile="../algo64.mlw"
loclnum="58" loccnumb="6" loccnume="8"
expl="3. postcondition"
sum="50540c91c27a7611995c0c91ae4874e7"
sum="7d4d8c2c6ffba710eeec4c1bfa496bfd"
proved="true"
expanded="false"
shape="postconditionasorted_subV4c0V0Iasorted_subV4c0ainfix +V3c1Aapermut_subV2V5c0ainfix +V3c1Aainfix &lt;=c0V0Lamk arrayV0V4FIainfix &lt;V3V0Aainfix &lt;=c0V3Aainfix &lt;=c0c0Lainfix -V0c1Iainfix &gt;V0c0Iainfix &lt;=c0V0Lamk arrayV0V1F">
......@@ -332,7 +332,7 @@
locfile="../algo64.mlw"
loclnum="58" loccnumb="6" loccnume="8"
expl="4. postcondition"
sum="6f46afd8f3a5e8f82e38d25f39b37c0a"
sum="23aa129e449a2b3b2ddef5b4cf2c5c6c"
proved="true"
expanded="false"
shape="postconditionapermut_allV2V2INainfix &gt;V0c0Iainfix &lt;=c0V0Lamk arrayV0V1F">
......@@ -352,7 +352,7 @@
locfile="../algo64.mlw"
loclnum="58" loccnumb="6" loccnume="8"
expl="5. postcondition"
sum="cf95c3c36f0ec712ce8df01b60098dec"
sum="5bc276fb733c13e0a0d893bc2416f31a"
proved="true"
expanded="false"
shape="postconditionasorted_subV1c0V0INainfix &gt;V0c0Iainfix &lt;=c0V0Lamk arrayV0V1F">
......
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
(* This file is generated by Why3's Coq 8.4 driver *)
(* Beware! Only edit allowed sections below *)
Require Import BuiltIn.
Require BuiltIn.
Require int.Int.
Require map.Map.
Require map.Occ.
Require map.MapPermut.
(* Why3 assumption *)
Definition unit := unit.
(* Why3 assumption *)
Inductive array
(a:Type) {a_WT:WhyType 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 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 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 a_WT)) (i:Z): a :=
(map.Map.get (elts a1) i).
(* Why3 assumption *)
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 a_WT) :=
(mk_array n (map.Map.const v: (@map.Map.map Z _ a a_WT))).
(* 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 :=
((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))))))).
Axiom 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)).
(* 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 permut {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))).
(* 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
(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)).
(* Why3 goal *)
Theorem 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),
(exchange1 a1 a2 i j) -> (((l <= i)%Z /\ (i < u)%Z) -> (((l <= j)%Z /\
(j < u)%Z) -> ((0%Z <= l)%Z -> ((u <= (length a1))%Z -> (permut_sub a1 a2 l
u))))).
intros a a_WT a1 a2 i j l u h1 (h2,h3) (h4,h5) h6 h7.
destruct h1 as (h11,h12).
destruct h12 as (ha,(hb,(hc,(hd,he)))).
red. repeat split.
(* eq_sub *)
red. intros. apply he; omega.
assumption. assumption. omega. omega. assumption.
(* permut *)
red. intro v.
assert (Occ.occ v (elts a1) i (i+1) + Occ.occ v (elts a1) j (j+1)
= Occ.occ v (elts a2) i (i+1) + Occ.occ v (elts a2) j (j+1))%Z.
destruct (why_decidable_eq (Map.get (elts a1) i) v).
rewrite Occ.occ_right_add. 2: omega. 2: ring_simplify (i+1-1)%Z; assumption.
rewrite (Occ.occ_right_add v (elts a2) j). 2: omega.
2: ring_simplify (j+1-1)%Z; rewrite <- hc; assumption.
ring_simplify (i+1-1)%Z. ring_simplify (j+1-1)%Z.
rewrite Occ.occ_empty. 2: omega. rewrite (Occ.occ_empty v (elts a2) j). 2: omega.
destruct (why_decidable_eq (Map.get (elts a1) j) v).
rewrite Occ.occ_right_add. 2: omega. 2: ring_simplify (j+1-1)%Z; assumption.
rewrite (Occ.occ_right_add v (elts a2) i). 2: omega.
2: ring_simplify (i+1-1)%Z; rewrite <- hd; assumption.
ring_simplify (i+1-1)%Z. ring_simplify (j+1-1)%Z.
rewrite Occ.occ_empty. 2: omega. rewrite (Occ.occ_empty v (elts a2) i). 2: omega.
ring.
rewrite Occ.occ_right_no_add. 2: omega. 2: ring_simplify (j+1-1)%Z; assumption.
rewrite (Occ.occ_right_no_add v (elts a2) i). 2: omega.
2: ring_simplify (i+1-1)%Z; rewrite <- hd; assumption.
ring_simplify (i+1-1)%Z. ring_simplify (j+1-1)%Z.
rewrite Occ.occ_empty. 2: omega. rewrite (Occ.occ_empty v (elts a2) i). 2: omega.
ring.
rewrite Occ.occ_right_no_add. 2: omega. 2: ring_simplify (i+1-1)%Z; assumption.
rewrite (Occ.occ_right_no_add v (elts a2) j). 2: omega.
2: ring_simplify (j+1-1)%Z; rewrite <- hc; assumption.
rewrite Occ.occ_empty. 2: omega. rewrite (Occ.occ_empty v (elts a2) j). 2: omega.
destruct (why_decidable_eq (Map.get (elts a1) j) v).
rewrite Occ.occ_right_add. 2: omega. 2: ring_simplify (j+1-1)%Z; assumption.
rewrite (Occ.occ_right_add v (elts a2) i). 2: omega.
2: ring_simplify (i+1-1)%Z; rewrite <- hd; assumption.
ring_simplify (i+1-1)%Z. ring_simplify (j+1-1)%Z.
rewrite Occ.occ_empty. 2: omega. rewrite (Occ.occ_empty v (elts a2) i). 2: omega.
ring.
rewrite Occ.occ_right_no_add. 2: omega. 2: ring_simplify (j+1-1)%Z; assumption.
rewrite (Occ.occ_right_no_add v (elts a2) i). 2: omega.
2: ring_simplify (i+1-1)%Z; rewrite <- hd; assumption.
ring_simplify (i+1-1)%Z. ring_simplify (j+1-1)%Z.
rewrite Occ.occ_empty. 2: omega. rewrite (Occ.occ_empty v (elts a2) i). 2: omega.
ring.
assert (c: (i < j \/ i = j \/ j < i)%Z) by omega. destruct c as [c|c].
(* i < j *)
assert (Occ.occ v (elts a1) l u = Occ.occ v (elts a1) l i + Occ.occ v (elts a1) i u)%Z.
apply Occ.occ_append. omega.
assert (Occ.occ v (elts a1) i u = Occ.occ v (elts a1) i (i+1) + Occ.occ v (elts a1) (i+1) u)%Z.
apply Occ.occ_append. omega.
assert (Occ.occ v (elts a1) (i+1) u = Occ.occ v (elts a1) (i+1) j + Occ.occ v (elts a1) j u)%Z.
apply Occ.occ_append. omega.
assert (Occ.occ v (elts a1) j u = Occ.occ v (elts a1) j (j+1) + Occ.occ v (elts a1) (j+1) u)%Z.
apply Occ.occ_append. omega.
assert (Occ.occ v (elts a2) l u = Occ.occ v (elts a2) l i + Occ.occ v (elts a2) i u)%Z.
apply Occ.occ_append. omega.
assert (Occ.occ v (elts a2) i u = Occ.occ v (elts a2) i (i+1) + Occ.occ v (elts a2) (i+1) u)%Z.
apply Occ.occ_append. omega.
assert (Occ.occ v (elts a2) (i+1) u = Occ.occ v (elts a2) (i+1) j + Occ.occ v (elts a2) j u)%Z.
apply Occ.occ_append. omega.
assert (Occ.occ v (elts a2) j u = Occ.occ v (elts a2) j (j+1) + Occ.occ v (elts a2) (j+1) u)%Z.
apply Occ.occ_append. omega.
assert (Occ.occ v (elts a1) l i = Occ.occ v (elts a2) l i).
apply Occ.occ_eq. intros. apply he; omega.
assert (Occ.occ v (elts a1) (i+1) j = Occ.occ v (elts a2) (i+1) j).
apply Occ.occ_eq. intros; apply he; omega.
assert (Occ.occ v (elts a1) (j+1) u = Occ.occ v (elts a2) (j+1) u).
apply Occ.occ_eq. intros; apply he; omega.
omega.
(* i = j *)
destruct c.
subst j.
apply Occ.occ_eq.
intros k hk.
assert (c: (k=i \/ k <>i)%Z) by omega. destruct c.
subst k. assumption.
apply he. omega. assumption. assumption.
(* j < i *)
assert (Occ.occ v (elts a1) l u = Occ.occ v (elts a1) l j + Occ.occ v (elts a1) j u)%Z.
apply Occ.occ_append. omega.
assert (Occ.occ v (elts a1) j u = Occ.occ v (elts a1) j (j+1) + Occ.occ v (elts a1) (j+1) u)%Z.
apply Occ.occ_append. omega.
assert (Occ.occ v (elts a1) (j+1) u = Occ.occ v (elts a1) (j+1) i + Occ.occ v (elts a1) i u)%Z.
apply Occ.occ_append. omega.
assert (Occ.occ v (elts a1) i u = Occ.occ v (elts a1) i (i+1) + Occ.occ v (elts a1) (i+1) u)%Z.
apply Occ.occ_append. omega.
assert (Occ.occ v (elts a2) l u = Occ.occ v (elts a2) l j + Occ.occ v (elts a2) j u)%Z.
apply Occ.occ_append. omega.
assert (Occ.occ v (elts a2) j u = Occ.occ v (elts a2) j (j+1) + Occ.occ v (elts a2) (j+1) u)%Z.
apply Occ.occ_append. omega.
assert (Occ.occ v (elts a2) (j+1) u = Occ.occ v (elts a2) (j+1) i + Occ.occ v (elts a2) i u)%Z.
apply Occ.occ_append. omega.
assert (Occ.occ v (elts a2) i u = Occ.occ v (elts a2) i (i+1) + Occ.occ v (elts a2) (i+1) u)%Z.
apply Occ.occ_append. omega.
assert (Occ.occ v (elts a1) l j = Occ.occ v (elts a2) l j).
apply Occ.occ_eq. intros. apply he; omega.
assert (Occ.occ v (elts a1) (j+1) i = Occ.occ v (elts a2) (j+1) i).
apply Occ.occ_eq. intros; apply he; omega.
assert (Occ.occ v (elts a1) (i+1) u = Occ.occ v (elts a2) (i+1) u).
apply Occ.occ_eq. intros; apply he; omega.
omega.
(* eq_sub *)
red. intros. apply he; omega.
Qed.
......@@ -96,52 +96,54 @@ 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)).
(* Require Import Why3. Ltac ae := why3 "Alt-Ergo,0.95.2," timelimit 3. *)
(* Why3 goal *)
Theorem exchange_permut_sub : forall {a:Type} {a_WT:WhyType a},
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),
(exchange1 a1 a2 i j) -> (((l <= i)%Z /\ (i < u)%Z) -> (((l <= j)%Z /\
(j < u)%Z) -> ((0%Z <= l)%Z -> ((u <= (length a1))%Z -> (permut_sub a1 a2 l
u))))).
(* Why3 intros a a_WT a1 a2 i j l u h1 (h2,h3) (h4,h5) h6 h7. *)
intros a a_WT a1 a2 i j l u h1 (h2,h3) (h4,h5) h6 h7.
destruct h1 as (h11,h12).
destruct h12 as (ha,(hb,(hc,(hd,he)))).
red. repeat split.
(* eq_sub *)
red. intros. apply he; omega.
assumption. assumption. omega. omega. assumption.
(* Why3 goal *)
Theorem 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) ->
(((u1 <= u2)%Z /\ (u2 <= (length a1))%Z) -> (permut_sub a1 a2 l2 u2))).
(* Why3 intros a a_WT a1 a2 l1 u1 l2 u2 h1 (h2,h3) (h4,h5). *)
intros a a_WT a1 a2 l1 u1 l2 u2 h1 (h2,h3) (h4,h5).
unfold permut_sub in *.
destruct h1 as (eql,(h1,eqr)).
unfold map_eq_sub in *.
split.
(* eq left *)
intros. apply eql; omega.
split.
(* permut *)
red. intro v.
assert (c: (i < j \/ i = j \/ j < i)%Z) by omega. destruct c as [c|c].
(* i < j *)
assert (Occ.occ v (elts a1) l u = Occ.occ v (elts a1) l i + Occ.occ v (elts a1) i u)%Z.
unfold permut in *.
destruct h1 as (h1,(h1a,(h1b,h1c))).
repeat split; try assumption. omega. omega.
unfold MapPermut.permut in *.
intros v.
assert (c: (l1 <= u1 \/ u1 < l1)%Z) by omega. destruct c.
(* l1 <= u1 *)
assert (Occ.occ v (elts a1) l2 u2 = Occ.occ v (elts a1) l2 l1 + Occ.occ v (elts a1) l1 u2)%Z.
apply Occ.occ_append. omega.
assert (Occ.occ v (elts a1) i u = Occ.occ v (elts a1) i (i+1) + Occ.occ v (elts a1) (i+1) u)%Z.
assert (Occ.occ v (elts a1) l1 u2 = Occ.occ v (elts a1) l1 u1 + Occ.occ v (elts a1) u1 u2)%Z.
apply Occ.occ_append. omega.
assert (Occ.occ v (elts a1) (i+1) u = Occ.occ v (elts a1) (i+1) j + Occ.occ v (elts a1) j u)%Z.
assert (Occ.occ v (elts a2) l2 u2 = Occ.occ v (elts a2) l2 l1 + Occ.occ v (elts a2) l1 u2)%Z.
apply Occ.occ_append. omega.
assert (Occ.occ v (elts a1) j u = Occ.occ v (elts a1) j (j+1) + Occ.occ v (elts a1) (j+1) u)%Z.
assert (Occ.occ v (elts a2) l1 u2 = Occ.occ v (elts a2) l1 u1 + Occ.occ v (elts a2) u1 u2)%Z.
apply Occ.occ_append. omega.
assert (Occ.occ v (elts a1) l i = Occ.occ v (elts a2) l i).
apply Occ.occ_eq. intros. apply he; omega.
admit. (*TODO*)
(* i = j *)
destruct c.
subst j.
assert (Occ.occ v (elts a1) l2 l1 = Occ.occ v (elts a2) l2 l1).
apply Occ.occ_eq. intros; apply eql; omega.
assert (Occ.occ v (elts a1) u1 u2 = Occ.occ v (elts a2) u1 u2).
apply Occ.occ_eq. intros; apply eqr; omega.
generalize (h1c v); omega.
(* u1 < l1 *)
apply Occ.occ_eq.
intros k hk.
assert (c: (k=i \/ k <>i)%Z) by omega. destruct c.
subst k. assumption.
apply he. omega. assumption. assumption.
(* j < i *)
admit. (*TODO*)
(* eq_sub *)
red. intros. apply he; omega.
intros i hi.
assert (c: (i < l1 \/ u1 <= i)%Z) by omega. destruct c.
apply eql; omega.
apply eqr; omega.
(* eq right *)
intros; apply eqr; omega.
Qed.
......@@ -7,23 +7,15 @@
version="0.95.2"/>
<prover
id="1"
name="CVC3"
version="2.4.1"/>
<prover
id="2"
name="CVC4"
version="1.3"/>
<prover
id="3"
name="Z3"
version="3.2"/>
<prover
id="4"
name="Z3"
version="4.3.1"/>
id="2"
name="Coq"
version="8.4pl2"/>
<file
name="../../../modules/array.mlw"
verified="false"
verified="true"
expanded="true">
<theory
name="Array"
......@@ -51,7 +43,7 @@
<result status="valid" time="0.01"/>
</proof>
<proof
prover="2"
prover="1"
timelimit="5"
memlimit="1000"
obsolete="false"
......@@ -79,7 +71,7 @@
<result status="valid" time="0.02"/>
</proof>
<proof
prover="2"
prover="1"
timelimit="5"
memlimit="1000"
obsolete="false"
......@@ -107,7 +99,7 @@
<result status="valid" time="0.02"/>
</proof>
<proof
prover="2"
prover="1"
timelimit="5"
memlimit="1000"
obsolete="false"
......@@ -141,313 +133,72 @@
name="ArrayPermut"
locfile="../../../modules/array.mlw"
loclnum="161" loccnumb="7" loccnume="18"
verified="false"