Commit e3bc6d2e authored by MARCHE Claude's avatar MARCHE Claude
Browse files

Fix Coq proofs after the change in MapPermut theory

parent db6311c5
(* 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.
Require int.Int.
Require map.Map.
Require map.MapPermut.
(* Why3 assumption *)
Definition unit := unit.
Definition unit := unit.
(* Why3 assumption *)
Inductive ref (a:Type) {a_WT:WhyType a} :=
......@@ -16,127 +17,85 @@ 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 :=
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} :=
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) :=
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 :=
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 :=
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
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) :=
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 exchange {a:Type} {a_WT:WhyType a}(a1:(map.Map.map Z a))
(a2:(map.Map.map Z a)) (i:Z) (j:Z): Prop := ((map.Map.get a1
i) = (map.Map.get a2 j)) /\ (((map.Map.get a2 i) = (map.Map.get a1 j)) /\
forall (k: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)), forall (i:Z) (j:Z), (exchange a1
(map.Map.set (map.Map.set a1 i (map.Map.get a1 j)) j (map.Map.get a1 i)) i
j).
(* Why3 assumption *)
Inductive permut_sub{a:Type} {a_WT:WhyType a} : (map.Map.map Z a)
-> (map.Map.map Z a) -> Z -> Z -> Prop :=
| permut_refl : forall (a1:(map.Map.map Z a)), forall (l:Z) (u:Z),
(permut_sub a1 a1 l u)
| permut_sym : forall (a1:(map.Map.map Z a)) (a2:(map.Map.map Z a)),
forall (l:Z) (u:Z), (permut_sub a1 a2 l u) -> (permut_sub a2 a1 l u)
| permut_trans : forall (a1:(map.Map.map Z a)) (a2:(map.Map.map Z a))
(a3:(map.Map.map Z a)), forall (l:Z) (u:Z), (permut_sub a1 a2 l u) ->
((permut_sub a2 a3 l u) -> (permut_sub a1 a3 l u))
| permut_exchange : forall (a1:(map.Map.map Z a)) (a2:(map.Map.map Z a)),
forall (l:Z) (u:Z) (i:Z) (j:Z), ((l <= i)%Z /\ (i < u)%Z) ->
(((l <= j)%Z /\ (j < u)%Z) -> ((exchange a1 a2 i j) -> (permut_sub a1
a2 l u))).
Axiom permut_weakening : forall {a:Type} {a_WT:WhyType a},
forall (a1:(map.Map.map Z a)) (a2:(map.Map.map Z a)), forall (l1:Z) (r1:Z)
(l2:Z) (r2:Z), (((l1 <= l2)%Z /\ (l2 <= r2)%Z) /\ (r2 <= r1)%Z) ->
((permut_sub a1 a2 l2 r2) -> (permut_sub a1 a2 l1 r1)).
Axiom permut_eq : forall {a:Type} {a_WT:WhyType a}, forall (a1:(map.Map.map Z
a)) (a2:(map.Map.map Z a)), forall (l:Z) (u:Z), (permut_sub a1 a2 l u) ->
forall (i:Z), ((i < l)%Z \/ (u <= i)%Z) -> ((map.Map.get a2
i) = (map.Map.get a1 i)).
Axiom permut_exists : forall {a:Type} {a_WT:WhyType a},
forall (a1:(map.Map.map Z a)) (a2:(map.Map.map Z a)), forall (l:Z) (u:Z),
(permut_sub a1 a2 l u) -> forall (i:Z), ((l <= i)%Z /\ (i < u)%Z) ->
exists j:Z, ((l <= j)%Z /\ (j < u)%Z) /\ ((map.Map.get a2
i) = (map.Map.get a1 j)).
Definition exchange {a:Type} {a_WT:WhyType a} (a1:(array a)) (a2:(array a))
(i:Z) (j:Z): Prop := (map.MapPermut.exchange (elts a1) (elts a2) i j).
(* Why3 assumption *)
Definition exchange1 {a:Type} {a_WT:WhyType a}(a1:(array a)) (a2:(array a))
(i:Z) (j:Z): Prop := (exchange (elts a1) (elts a2) i j).
Definition permut_sub {a:Type} {a_WT:WhyType a} (a1:(array a)) (a2:(array a))
(l:Z) (u:Z): Prop := (map.MapPermut.permut_sub (elts a1) (elts a2) l u).
(* Why3 assumption *)
Definition permut_sub1 {a:Type} {a_WT:WhyType a}(a1:(array a)) (a2:(array a))
(l:Z) (u:Z): Prop := (permut_sub (elts a1) (elts a2) l u).
(* Why3 assumption *)
Definition permut {a:Type} {a_WT:WhyType a}(a1:(array a)) (a2:(array
a)): Prop := ((length a1) = (length a2)) /\ (permut_sub (elts a1) (elts a2)
0%Z (length a1)).
Definition permut {a:Type} {a_WT:WhyType a} (a1:(array a)) (a2:(array
a)): Prop := ((length a1) = (length a2)) /\ (map.MapPermut.permut_sub
(elts a1) (elts a2) 0%Z (length a1)).
Axiom exchange_permut : forall {a:Type} {a_WT:WhyType a}, forall (a1:(array
a)) (a2:(array a)) (i:Z) (j:Z), (exchange1 a1 a2 i j) ->
a)) (a2:(array a)) (i:Z) (j:Z), (exchange a1 a2 i j) ->
(((length a1) = (length a2)) -> (((0%Z <= i)%Z /\ (i < (length a1))%Z) ->
(((0%Z <= j)%Z /\ (j < (length a1))%Z) -> (permut a1 a2)))).
Axiom permut_sym1 : forall {a:Type} {a_WT:WhyType a}, forall (a1:(array a))
Axiom permut_sym : forall {a:Type} {a_WT:WhyType a}, forall (a1:(array a))
(a2:(array a)), (permut a1 a2) -> (permut a2 a1).
Axiom permut_trans1 : forall {a:Type} {a_WT:WhyType a}, forall (a1:(array a))
(a2:(array a)) (a3:(array a)), (permut a1 a2) -> ((permut a2 a3) ->
(permut a1 a3)).
Axiom permut_trans : forall {a:Type} {a_WT:WhyType a}, forall (a1:(array a))
(a2:(array a)) (a3:(array a)), (permut a1 a2) -> ((permut a2 a3) -> (permut
a1 a3)).
(* Why3 assumption *)
Definition map_eq_sub {a:Type} {a_WT:WhyType a}(a1:(map.Map.map Z a))
Definition map_eq_sub {a:Type} {a_WT:WhyType a} (a1:(map.Map.map Z a))
(a2:(map.Map.map Z a)) (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)) (a2:(array
Definition array_eq_sub {a:Type} {a_WT:WhyType a} (a1:(array a)) (a2:(array
a)) (l:Z) (u:Z): Prop := (map_eq_sub (elts a1) (elts a2) l u).
(* Why3 assumption *)
Definition array_eq {a:Type} {a_WT:WhyType a}(a1:(array a)) (a2:(array
Definition array_eq {a:Type} {a_WT:WhyType a} (a1:(array a)) (a2:(array
a)): Prop := ((length a1) = (length a2)) /\ (array_eq_sub a1 a2 0%Z
(length a1)).
Axiom array_eq_sub_permut : forall {a:Type} {a_WT:WhyType a},
forall (a1:(array a)) (a2:(array a)) (l:Z) (u:Z), (array_eq_sub a1 a2 l
u) -> (permut_sub1 a1 a2 l u).
u) -> (permut_sub a1 a2 l u).
Axiom array_eq_permut : forall {a:Type} {a_WT:WhyType a}, forall (a1:(array
a)) (a2:(array a)), (array_eq a1 a2) -> (permut a1 a2).
......@@ -148,37 +107,39 @@ Parameter f: Z.
Axiom f_N_range : (1%Z <= f)%Z /\ (f <= usN)%Z.
(* Why3 assumption *)
Definition found(a:(array Z)): Prop := forall (p:Z) (q:Z), ((((1%Z <= p)%Z /\
(p <= f)%Z) /\ (f <= q)%Z) /\ (q <= usN)%Z) -> (((get a p) <= (get a
f))%Z /\ ((get a f) <= (get a q))%Z).
Definition found (a:(array Z)): Prop := forall (p:Z) (q:Z),
((((1%Z <= p)%Z /\ (p <= f)%Z) /\ (f <= q)%Z) /\ (q <= usN)%Z) -> (((get a
p) <= (get a f))%Z /\ ((get a f) <= (get a q))%Z).
(* Why3 assumption *)
Definition m_invariant(m:Z) (a:(array Z)): Prop := (m <= f)%Z /\ forall (p:Z)
(q:Z), ((((1%Z <= p)%Z /\ (p < m)%Z) /\ (m <= q)%Z) /\ (q <= usN)%Z) ->
((get a p) <= (get a q))%Z.
Definition m_invariant (m:Z) (a:(array Z)): Prop := (m <= f)%Z /\
forall (p:Z) (q:Z), ((((1%Z <= p)%Z /\ (p < m)%Z) /\ (m <= q)%Z) /\
(q <= usN)%Z) -> ((get a p) <= (get a q))%Z.
(* Why3 assumption *)
Definition n_invariant(n:Z) (a:(array Z)): Prop := (f <= n)%Z /\ forall (p:Z)
(q:Z), ((((1%Z <= p)%Z /\ (p <= n)%Z) /\ (n < q)%Z) /\ (q <= usN)%Z) ->
((get a p) <= (get a q))%Z.
Definition n_invariant (n:Z) (a:(array Z)): Prop := (f <= n)%Z /\
forall (p:Z) (q:Z), ((((1%Z <= p)%Z /\ (p <= n)%Z) /\ (n < q)%Z) /\
(q <= usN)%Z) -> ((get a p) <= (get a q))%Z.
(* Why3 assumption *)
Definition i_invariant(m:Z) (n:Z) (i:Z) (r:Z) (a:(array Z)): Prop :=
Definition i_invariant (m:Z) (n:Z) (i:Z) (r:Z) (a:(array Z)): Prop :=
(m <= i)%Z /\ ((forall (p:Z), ((1%Z <= p)%Z /\ (p < i)%Z) -> ((get a
p) <= r)%Z) /\ ((i <= n)%Z -> exists p:Z, ((i <= p)%Z /\ (p <= n)%Z) /\
(r <= (get a p))%Z)).
(* Why3 assumption *)
Definition j_invariant(m:Z) (n:Z) (j:Z) (r:Z) (a:(array Z)): Prop :=
Definition j_invariant (m:Z) (n:Z) (j:Z) (r:Z) (a:(array Z)): Prop :=
(j <= n)%Z /\ ((forall (q:Z), ((j < q)%Z /\ (q <= usN)%Z) -> (r <= (get a
q))%Z) /\ ((m <= j)%Z -> exists q:Z, ((m <= q)%Z /\ (q <= j)%Z) /\ ((get a
q) <= r)%Z)).
(* Why3 assumption *)
Definition termination(i:Z) (j:Z) (i0:Z) (j0:Z) (r:Z) (a:(array Z)): Prop :=
Definition termination (i:Z) (j:Z) (i0:Z) (j0:Z) (r:Z) (a:(array Z)): Prop :=
((i0 < i)%Z /\ (j < j0)%Z) \/ (((i <= f)%Z /\ (f <= j)%Z) /\ ((get a
f) = r)).
Import MapPermut.
(* Why3 goal *)
Theorem WP_parameter_find : forall (a:Z), forall (a1:(map.Map.map Z Z)),
let a2 := (mk_array a a1) in (((0%Z <= a)%Z /\ (a = (usN + 1%Z)%Z)) ->
......@@ -202,12 +163,17 @@ Theorem WP_parameter_find : forall (a:Z), forall (a1:(map.Map.map Z Z)),
((0%Z <= a)%Z /\ (a7 = (map.Map.set a5 i1 (map.Map.get a5 j1)))) ->
(((0%Z <= j1)%Z /\ (j1 < a)%Z) -> forall (a8:(map.Map.map Z Z)), let a9 :=
(mk_array a a8) in (((0%Z <= a)%Z /\ (a8 = (map.Map.set a7 j1
(map.Map.get a5 i1)))) -> ((exchange a8 a5 i1 j1) -> (((map.Map.get a8
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) ->
(map.Map.get a5 i1)))) -> ((map.MapPermut.exchange a8 a5 i1 j1) ->
(((map.Map.get a8 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
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)))))))))))))))))))))))))))).
(* intros a a1 a2 (h1,h2) n m a3 a4 (h3,(h4,(h5,(h6,h7)))) h8 (h9,(h10,h11))
r j i a5 a6 (h12,(h13,(h14,(h15,(h16,(h17,(h18,h19))))))) h20 i1
(h21,((h22,h23),h24)) (h25,(h26,h27)) h28 j1 (h29,(h30,(h31,h32)))
(h33,h34) h35 (h36,h37) h38 (h39,h40) (h41,h42) (h43,h44) a7 (h45,h46)
(h47,h48) a8 a9 (h49,h50) h51 h52 h53 i2 h54 j2 h55. *)
(* YOU MAY EDIT THE PROOF BELOW *)
intuition.
intuition.
......
......@@ -16,7 +16,7 @@
<prover
id="3"
name="Coq"
version="8.3pl4"/>
version="8.4"/>
<prover
id="4"
name="Z3"
......@@ -173,7 +173,7 @@
expl="7. precondition"
sum="dfdf99084dba7091e045407eacb47864"
proved="true"
expanded="true"
expanded="false"
shape="ainfix &lt;V12V0Aainfix &lt;=c0V12Iainfix &lt;=c0V0IaterminationV12V8V4V3V7V11Aainfix &lt;=V12V3Aainfix &lt;=V9V12Aai_invariantV4V3V12V7V11FIainfix &lt;=V9V8IapermutV11V2AaterminationV9V8V4V3V7V11Aainfix &lt;=V9ainfix +a_Nc1Aainfix &lt;=c0V8Aan_invariantV3V11Aam_invariantV4V11Aaj_invariantV4V3V8V7V11Aai_invariantV4V3V9V7V11Lamk arrayV0V10FLagetV5afIainfix &lt;afV0Aainfix &lt;=c0afAainfix &lt;=c0V0Iainfix &lt;V4V3Iainfix &lt;=V3a_NAainfix &lt;=c1V4AapermutV6V2Aan_invariantV3V6Aam_invariantV4V6Lamk arrayV0V5FIainfix =V0ainfix +a_Nc1Aainfix &lt;=c0V0Lamk arrayV0V1FF">
<label
name="expl:VC for find"/>
......@@ -188,7 +188,7 @@
<transf
name="split_goal"
proved="true"
expanded="true">
expanded="false">
<goal
name="WP_parameter find.7.1"
locfile="../find.mlw"
......@@ -254,14 +254,14 @@
expl="8. loop invariant preservation"
sum="5f67d1e477b65899ccf7d0389fe76545"
proved="true"
expanded="true"
expanded="false"
shape="aterminationV13V8V4V3V7V11Aainfix &lt;=V13V3Aainfix &lt;=V9V13Aai_invariantV4V3V13V7V11Iainfix =V13ainfix +V12c1FIainfix &lt;agetV10V12V7Iainfix &lt;V12V0Aainfix &lt;=c0V12Aainfix &lt;=c0V0IaterminationV12V8V4V3V7V11Aainfix &lt;=V12V3Aainfix &lt;=V9V12Aai_invariantV4V3V12V7V11FIainfix &lt;=V9V8IapermutV11V2AaterminationV9V8V4V3V7V11Aainfix &lt;=V9ainfix +a_Nc1Aainfix &lt;=c0V8Aan_invariantV3V11Aam_invariantV4V11Aaj_invariantV4V3V8V7V11Aai_invariantV4V3V9V7V11Lamk arrayV0V10FLagetV5afIainfix &lt;afV0Aainfix &lt;=c0afAainfix &lt;=c0V0Iainfix &lt;V4V3Iainfix &lt;=V3a_NAainfix &lt;=c1V4AapermutV6V2Aan_invariantV3V6Aam_invariantV4V6Lamk arrayV0V5FIainfix =V0ainfix +a_Nc1Aainfix &lt;=c0V0Lamk arrayV0V1FF">
<label
name="expl:VC for find"/>
<transf
name="split_goal"
proved="true"
expanded="true">
expanded="false">
<goal
name="WP_parameter find.8.1"
locfile="../find.mlw"
......@@ -419,14 +419,14 @@
expl="12. loop invariant preservation"
sum="f605f388325411d7176890209f3d88e6"
proved="true"
expanded="true"
expanded="false"
shape="aterminationV12V14V4V3V7V11Aainfix &lt;=V4V14Aainfix &lt;=V14V8Aaj_invariantV4V3V14V7V11Iainfix =V14ainfix -V13c1FIainfix &lt;V7agetV10V13Iainfix &lt;V13V0Aainfix &lt;=c0V13IaterminationV12V13V4V3V7V11Aainfix &lt;=V4V13Aainfix &lt;=V13V8Aaj_invariantV4V3V13V7V11FIainfix &lt;agetV10V12V7NIainfix &lt;V12V0Aainfix &lt;=c0V12Aainfix &lt;=c0V0IaterminationV12V8V4V3V7V11Aainfix &lt;=V12V3Aainfix &lt;=V9V12Aai_invariantV4V3V12V7V11FIainfix &lt;=V9V8IapermutV11V2AaterminationV9V8V4V3V7V11Aainfix &lt;=V9ainfix +a_Nc1Aainfix &lt;=c0V8Aan_invariantV3V11Aam_invariantV4V11Aaj_invariantV4V3V8V7V11Aai_invariantV4V3V9V7V11Lamk arrayV0V10FLagetV5afIainfix &lt;afV0Aainfix &lt;=c0afAainfix &lt;=c0V0Iainfix &lt;V4V3Iainfix &lt;=V3a_NAainfix &lt;=c1V4AapermutV6V2Aan_invariantV3V6Aam_invariantV4V6Lamk arrayV0V5FIainfix =V0ainfix +a_Nc1Aainfix &lt;=c0V0Lamk arrayV0V1FF">
<label
name="expl:VC for find"/>
<transf
name="split_goal"
proved="true"
expanded="true">
expanded="false">
<goal
name="WP_parameter find.12.1"
locfile="../find.mlw"
......@@ -696,7 +696,7 @@
expl="22. loop invariant preservation"
sum="b786b9e9c91207dc316c364b14eea1f6"
proved="true"
expanded="true"
expanded="false"
shape="apermutV16V2AaterminationV17V18V4V3V7V16Aainfix &lt;=V17ainfix +a_Nc1Aainfix &lt;=c0V18Aan_invariantV3V16Aam_invariantV4V16Aaj_invariantV4V3V18V7V16Aai_invariantV4V3V17V7V16Iainfix =V18ainfix -V13c1FIainfix =V17ainfix +V12c1FIainfix &lt;=V7agetV15V13Iainfix &lt;=agetV15V12V7IaexchangeV15V10V12V13Iainfix =V15asetV14V13agetV10V12Aainfix &lt;=c0V0Lamk arrayV0V15FIainfix &lt;V13V0Aainfix &lt;=c0V13Iainfix =V14asetV10V12agetV10V13Aainfix &lt;=c0V0FIainfix &lt;V12V0Aainfix &lt;=c0V12Iainfix &lt;V13V0Aainfix &lt;=c0V13Iainfix &lt;V12V0Aainfix &lt;=c0V12Iainfix &lt;=V12V13Iainfix &lt;=V7agetV10V12Aainfix &lt;=agetV10V13V7Iainfix &lt;V7agetV10V13NIainfix &lt;V13V0Aainfix &lt;=c0V13IaterminationV12V13V4V3V7V11Aainfix &lt;=V4V13Aainfix &lt;=V13V8Aaj_invariantV4V3V13V7V11FIainfix &lt;agetV10V12V7NIainfix &lt;V12V0Aainfix &lt;=c0V12Aainfix &lt;=c0V0IaterminationV12V8V4V3V7V11Aainfix &lt;=V12V3Aainfix &lt;=V9V12Aai_invariantV4V3V12V7V11FIainfix &lt;=V9V8IapermutV11V2AaterminationV9V8V4V3V7V11Aainfix &lt;=V9ainfix +a_Nc1Aainfix &lt;=c0V8Aan_invariantV3V11Aam_invariantV4V11Aaj_invariantV4V3V8V7V11Aai_invariantV4V3V9V7V11Lamk arrayV0V10FLagetV5afIainfix &lt;afV0Aainfix &lt;=c0afAainfix &lt;=c0V0Iainfix &lt;V4V3Iainfix &lt;=V3a_NAainfix &lt;=c1V4AapermutV6V2Aan_invariantV3V6Aam_invariantV4V6Lamk arrayV0V5FIainfix =V0ainfix +a_Nc1Aainfix &lt;=c0V0Lamk arrayV0V1FF">
<label
name="expl:VC for find"/>
......@@ -707,7 +707,7 @@
edited="find_WP_FIND_WP_parameter_find_4.v"
obsolete="false"
archived="false">
<result status="valid" time="6.55"/>
<result status="valid" time="9.36"/>
</proof>
</goal>
<goal
......@@ -837,14 +837,14 @@
expl="29. loop invariant preservation"
sum="8ec7acbd78a580d60812d9f56d571f13"
proved="true"
expanded="true"
expanded="false"
shape="ainfix &lt;=V3a_NAainfix &lt;=c1V12AapermutV11V2Aan_invariantV3V11Aam_invariantV12V11Iainfix =V12V9FIainfix &lt;=V9afIainfix &lt;=afV8NIainfix &lt;V8V3Aainfix &lt;V4V9Iainfix &lt;=V9V8NIapermutV11V2AaterminationV9V8V4V3V7V11Aainfix &lt;=V9ainfix +a_Nc1Aainfix &lt;=c0V8Aan_invariantV3V11Aam_invariantV4V11Aaj_invariantV4V3V8V7V11Aai_invariantV4V3V9V7V11Lamk arrayV0V10FLagetV5afIainfix &lt;afV0Aainfix &lt;=c0afAainfix &lt;=c0V0Iainfix &lt;V4V3Iainfix &lt;=V3a_NAainfix &lt;=c1V4AapermutV6V2Aan_invariantV3V6Aam_invariantV4V6Lamk arrayV0V5FIainfix =V0ainfix +a_Nc1Aainfix &lt;=c0V0Lamk arrayV0V1FF">
<label
name="expl:VC for find"/>
<transf
name="split_goal"
proved="true"
expanded="true">
expanded="false">
<goal
name="WP_parameter find.29.1"
locfile="../find.mlw"
......
(* 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.
Require int.Int.
Require map.Map.
Require map.MapPermut.
(* Why3 assumption *)
Definition unit := unit.
Definition unit := unit.
(* Why3 assumption *)
Inductive ref (a:Type) {a_WT:WhyType a} :=
......@@ -16,127 +17,85 @@ 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 :=
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} :=
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) :=
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 :=
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 :=
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
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) :=
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 exchange {a:Type} {a_WT:WhyType a}(a1:(map.Map.map Z a))
(a2:(map.Map.map Z a)) (i:Z) (j:Z): Prop := ((map.Map.get a1
i) = (map.Map.get a2 j)) /\ (((map.Map.get a2 i) = (map.Map.get a1 j)) /\
forall (k: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)), forall (i:Z) (j:Z), (exchange a1
(map.Map.set (map.Map.set a1 i (map.Map.get a1 j)) j (map.Map.get a1 i)) i
j).
Definition exchange {a:Type} {a_WT:WhyType a} (a1:(array a)) (a2:(array a))
(i:Z) (j:Z): Prop := (map.MapPermut.exchange (elts a1) (elts a2) i j).
(* Why3 assumption *)
Inductive permut_sub{a:Type} {a_WT:WhyType a} : (map.Map.map Z a)
-> (map.Map.map Z a) -> Z -> Z -> Prop :=
| permut_refl : forall (a1:(map.Map.map Z a)), forall (l:Z) (u:Z),
(permut_sub a1 a1 l u)
| permut_sym : forall (a1:(map.Map.map Z a)) (a2:(map.Map.map Z a)),
forall (l:Z) (u:Z), (permut_sub a1 a2 l u) -> (permut_sub a2 a1 l u)
| permut_trans : forall (a1:(map.Map.map Z a)) (a2:(map.Map.map Z a))
(a3:(map.Map.map Z a)), forall (l:Z) (u:Z), (permut_sub a1 a2 l u) ->
((permut_sub a2 a3 l u) -> (permut_sub a1 a3 l u))
| permut_exchange : forall (a1:(map.Map.map Z a)) (a2:(map.Map.map Z a)),
forall (l:Z) (u:Z) (i:Z) (j:Z), ((l <= i)%Z /\ (i < u)%Z) ->
(((l <= j)%Z /\ (j < u)%Z) -> ((exchange a1 a2 i j) -> (permut_sub a1
a2 l u))).
Axiom permut_weakening : forall {a:Type} {a_WT:WhyType a},
forall (a1:(map.Map.map Z a)) (a2:(map.Map.map Z a)), forall (l1:Z) (r1:Z)
(l2:Z) (r2:Z), (((l1 <= l2)%Z /\ (l2 <= r2)%Z) /\ (r2 <= r1)%Z) ->
((permut_sub a1 a2 l2 r2) -> (permut_sub a1 a2 l1 r1)).
Axiom permut_eq : forall {a:Type} {a_WT:WhyType a}, forall (a1:(map.Map.map Z
a)) (a2:(map.Map.map Z a)), forall (l:Z) (u:Z), (permut_sub a1 a2 l u) ->
forall (i:Z), ((i < l)%Z \/ (u <= i)%Z) -> ((map.Map.get a2
i) = (map.Map.get a1 i)).
Axiom permut_exists : forall {a:Type} {a_WT:WhyType a},
forall (a1:(map.Map.map Z a)) (a2:(map.Map.map Z a)), forall (l:Z) (u:Z),
(permut_sub a1 a2 l u) -> forall (i:Z), ((l <= i)%Z /\ (i < u)%Z) ->
exists j:Z, ((l <= j)%Z /\ (j < u)%Z) /\ ((map.Map.get a2
i) = (map.Map.get a1 j)).
Definition permut_sub {a:Type} {a_WT:WhyType a} (a1:(array a)) (a2:(array a))
(l:Z) (u:Z): Prop := (map.MapPermut.permut_sub (elts a1) (elts a2) l u).
(* Why3 assumption *)
Definition exchange1 {a:Type} {a_WT:WhyType a}(a1:(array a)) (a2:(array a))
(i:Z) (j:Z): Prop := (exchange (elts a1) (elts a2) i j).
(* Why3 assumption *)
Definition permut_sub1 {a:Type} {a_WT:WhyType a}(a1:(array a)) (a2:(array a))
(l:Z) (u:Z): Prop := (permut_sub (elts a1) (elts a2) l u).
(* Why3 assumption *)
Definition permut {a:Type} {a_WT:WhyType a}(a1:(array a)) (a2:(array
a)): Prop := ((length a1) = (length a2)) /\ (permut_sub (elts a1) (elts a2)
0%Z (length a1)).
Definition permut {a:Type} {a_WT:WhyType a} (a1:(array a)) (a2:(array
a)): Prop := ((length a1) = (length a2)) /\ (map.MapPermut.permut_sub
(elts a1) (elts a2) 0%Z (length a1)).
Axiom exchange_permut : forall {a:Type} {a_WT:WhyType a}, forall (a1:(array
a)) (a2:(array a)) (i:Z) (j:Z), (exchange1 a1 a2 i j) ->
a)) (a2:(array a)) (i:Z) (j:Z), (exchange a1 a2 i j) ->
(((length a1) = (length a2)) -> (((0%Z <= i)%Z /\ (i < (length a1))%Z) ->
(((0%Z <= j)%Z /\ (j < (length a1))%Z) -> (permut a1 a2)))).
Axiom permut_sym1 : forall {a:Type} {a_WT:WhyType a}, forall (a1:(array a))
Axiom permut_sym : forall {a:Type} {a_WT:WhyType a}, forall (a1:(array a))
(a2:(array a)), (permut a1 a2) -> (permut a2 a1).
Axiom permut_trans1 : forall {a:Type} {a_WT:WhyType a}, forall (a1:(array a))
(a2:(array a)) (a3:(array a)), (permut a1 a2) -> ((permut a2 a3) ->
(permut a1 a3)).
Axiom permut_trans : forall {a:Type} {a_WT:WhyType a}, forall (a1:(array a))
(a2:(array a)) (a3:(array a)), (permut a1 a2) -> ((permut a2 a3) -> (permut
a1 a3)).
(* Why3 assumption *)
Definition map_eq_sub {a:Type} {a_WT:WhyType a}(a1:(map.Map.map Z a))
Definition map_eq_sub {a:Type} {a_WT:WhyType a} (a1:(map.Map.map Z a))
(a2:(map.Map.map Z a)) (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)) (a2:(array
Definition array_eq_sub {a:Type} {a_WT:WhyType a} (a1:(array a)) (a2:(array
a)) (l:Z) (u:Z): Prop := (map_eq_sub (elts a1) (elts a2) l u).
(* Why3 assumption *)
Definition array_eq {a:Type} {a_WT:WhyType a}(a1:(array a)) (a2:(array
Definition array_eq {a:Type} {a_WT:WhyType a} (a1:(array a)) (a2:(array
a)): Prop := ((length a1) = (length a2)) /\ (array_eq_sub a1 a2 0%Z
(length a1)).
Axiom array_eq_sub_permut : forall {a:Type} {a_WT:WhyType a},
forall (a1:(array a)) (a2:(array a)) (l:Z) (u:Z), (array_eq_sub a1 a2 l
u) -> (permut_sub1 a1 a2 l u).
u) -> (permut_sub a1 a2 l u).
Axiom array_eq_permut : forall {a:Type} {a_WT:WhyType a}, forall (a1:(array
a)) (a2:(array a)), (array_eq a1 a2) -> (permut a1 a2).
......@@ -148,9 +107,9 @@ Existing Instance elt_WhyType.
Parameter le: elt -> elt -> Prop.
(* Why3 assumption *)
Definition sorted_sub(a:(map.Map.map Z elt)) (l:Z) (u:Z): Prop :=
forall (i1:Z) (i2:Z), (((l <= i1)%Z /\ (i1 <= i2)%Z) /\ (i2 < u)%Z) ->
(le (map.Map.get a i1) (map.Map.get a i2)).
Definition sorted_sub (a:(map.Map.map Z elt)) (l:Z) (u:Z): Prop :=
forall (i1:Z) (i2:Z), (((l <= i1)%Z /\ (i1 <= i2)%Z) /\ (i2 < u)%Z) -> (le
(map.Map.get a i1) (map.Map.get a i2)).
Axiom le_refl : forall (x:elt), (le x x).
......@@ -160,13 +119,15 @@ Axiom le_trans : forall (x:elt) (y:elt) (z:elt), ((le x y) /\ (le y z)) ->
(le x z).
(* Why3 assumption *)