Skip to content

GitLab

why3
why3
Commit 5307d60a authored by Jean-Christophe Filliâtre's avatar Jean-Christophe Filliâtre
Browse files
Options

updated proof sessions

parent b9ffc04c
Expand all Hide whitespace changes
Inline Side-by-side
Showing with 934 additions and 571 deletions
examples/programs/euler001/why3session.xml
View file @ 5307d60a
......@@ -3,91 +3,55 @@
<why3session name="examples/programs/euler001/why3session.xml">
<file name="../euler001.mlw" verified="false" expanded="true">
<theory name="SumMultiple" verified="false" expanded="true">
<goal name="div_minus1_1" sum="f5f3412d9b58086a6e9b482e89262ec3" proved="false" expanded="true">
<proof prover="cvc3" timelimit="2" edited="" obsolete="false">
<result status="timeout" time="2.40"/>
</proof>
<proof prover="alt-ergo" timelimit="2" edited="" obsolete="false">
<result status="unknown" time="0.22"/>
</proof>
<proof prover="simplify" timelimit="2" edited="" obsolete="false">
<result status="unknown" time="0.06"/>
</proof>
<proof prover="z3" timelimit="2" edited="" obsolete="false">
<result status="unknown" time="4.31"/>
</proof>
<goal name="div_minus1_1" sum="799200a5112f46b45ab595bbe99aa9fe" proved="false" expanded="true">
</goal>
<goal name="div_minus1_2" sum="58b4c2b7cc926f7281ef2d9806046849" proved="false" expanded="true">
<proof prover="cvc3" timelimit="2" edited="" obsolete="false">
<result status="timeout" time="2.30"/>
</proof>
<proof prover="alt-ergo" timelimit="2" edited="" obsolete="false">
<result status="unknown" time="0.24"/>
</proof>
<proof prover="simplify" timelimit="2" edited="" obsolete="false">
<result status="unknown" time="0.04"/>
</proof>
<proof prover="z3" timelimit="2" edited="" obsolete="false">
<result status="unknown" time="1.45"/>
</proof>
<goal name="div_minus1_2" sum="7b0639aa2f9bead033faaeae5c5303fe" proved="false" expanded="true">
</goal>
<goal name="mod_15" sum="e2d678bf333354c7d41e3255a00ce78b" proved="true" expanded="true">
<goal name="mod_15" sum="e5478c4f7dd1e8e51f1b59c6f48d52b7" proved="true" expanded="true">
<proof prover="cvc3" timelimit="2" edited="" obsolete="false">
<result status="valid" time="0.06"/>
<result status="valid" time="0.04"/>
</proof>
<proof prover="alt-ergo" timelimit="2" edited="" obsolete="false">
<result status="valid" time="0.13"/>
<result status="valid" time="0.11"/>
</proof>
<proof prover="z3" timelimit="2" edited="" obsolete="false">
<result status="valid" time="0.44"/>
<result status="valid" time="0.02"/>
</proof>
</goal>
<goal name="Closed_formula_0" sum="bedb2551f46c9bf80e4fd6d1cddcc221" proved="true" expanded="true">
<goal name="Closed_formula_0" sum="a49fafd7dea8767fc52287a6d759cc28" proved="true" expanded="true">
<proof prover="cvc3" timelimit="2" edited="" obsolete="false">
<result status="valid" time="0.08"/>
<result status="valid" time="0.03"/>
</proof>
<proof prover="alt-ergo" timelimit="2" edited="" obsolete="false">
<result status="valid" time="0.02"/>
<result status="valid" time="0.01"/>
</proof>
<proof prover="z3" timelimit="2" edited="" obsolete="false">
<result status="valid" time="0.02"/>
<result status="valid" time="0.00"/>
</proof>
</goal>
<goal name="Closed_formula_n_1" sum="07cd7a1e0916a0fd5db441ad655752d4" proved="true" expanded="true">
<goal name="Closed_formula_n_1" sum="53f650c14f94ca7656e6b83261ea0a3d" proved="true" expanded="true">
<proof prover="cvc3" timelimit="2" edited="" obsolete="false">
<result status="valid" time="0.17"/>
<result status="valid" time="0.12"/>
</proof>
<proof prover="simplify" timelimit="2" edited="" obsolete="false">
<result status="valid" time="0.03"/>
<result status="valid" time="0.00"/>
</proof>
</goal>
<goal name="Closed_formula_n_2" sum="9f118f99f106bbd45be20274179078b5" proved="false" expanded="true">
<proof prover="cvc3" timelimit="2" edited="" obsolete="false">
<result status="timeout" time="2.09"/>
</proof>
<proof prover="alt-ergo" timelimit="2" edited="" obsolete="false">
<result status="timeout" time="2.09"/>
</proof>
<proof prover="simplify" timelimit="2" edited="" obsolete="false">
<result status="timeout" time="2.09"/>
</proof>
<proof prover="z3" timelimit="2" edited="" obsolete="false">
<result status="timeout" time="5.08"/>
</proof>
<goal name="Closed_formula_n_2" sum="ce02a5758f2253ac1e0edc7f916ce957" proved="false" expanded="true">
</goal>
<goal name="Closed_formula" sum="6a9095ec398278b6e7fa407e16f64039" proved="true" expanded="true">
<goal name="Closed_formula" sum="aa724d9368ec95db9867b2ea2062c3a0" proved="true" expanded="true">
<proof prover="cvc3" timelimit="2" edited="" obsolete="false">
<result status="valid" time="0.02"/>
<result status="valid" time="0.01"/>
</proof>
<proof prover="simplify" timelimit="2" edited="" obsolete="false">
<result status="valid" time="0.04"/>
<result status="valid" time="0.03"/>
</proof>
</goal>
</theory>
<theory name="WP Euler001" verified="true" expanded="true">
<goal name="WP_parameter solve" expl="normal postcondition" sum="dd6f0e34463bcfbf4b3ca11577b727c6" proved="true" expanded="true">
<goal name="WP_parameter solve" expl="normal postcondition" sum="1d462fc3346a429205b44caaf3f0a839" proved="true" expanded="true">
<proof prover="cvc3" timelimit="2" edited="" obsolete="false">
<result status="valid" time="0.46"/>
<result status="valid" time="0.51"/>
</proof>
<proof prover="simplify" timelimit="2" edited="" obsolete="false">
<result status="valid" time="0.10"/>
......
examples/programs/fib_memo/why3session.xml
View file @ 5307d60a
......@@ -3,12 +3,12 @@
<why3session name="examples/programs/fib_memo/why3session.xml">
<file name="../fib_memo.mlw" verified="true" expanded="true">
<theory name="WP M" verified="true" expanded="true">
<goal name="WP_parameter fibo" expl="correctness of parameter fibo" sum="75546b1b867d7e220a43a0f9c16568a2" proved="true" expanded="true">
<goal name="WP_parameter fibo" expl="correctness of parameter fibo" sum="f0a3a1ac8674e9e268ae11f8df9ff39d" proved="true" expanded="true">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.03"/>
<result status="valid" time="0.02"/>
</proof>
</goal>
<goal name="WP_parameter memo_fibo" expl="correctness of parameter memo_fibo" sum="743b19a4394b2b79b9ef838a624045c7" proved="true" expanded="true">
<goal name="WP_parameter memo_fibo" expl="correctness of parameter memo_fibo" sum="9373cd2e2bcff22cf5eaa6b757149684" proved="true" expanded="true">
<transf name="split_goal" proved="true" expanded="true">
<goal name="WP_parameter memo_fibo.1" expl="normal postcondition" sum="935d25dee5b707cf0bd087e131e709da" proved="true" expanded="true">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
......
examples/programs/flag.mlw
View file @ 5307d60a
......@@ -10,7 +10,7 @@ module Flag
type color = Blue | White | Red
predicate monochrome (a:array color) (i:int) (j:int) (c:color) =
forall k:int. i<=k<j -> a[k]=c
forall k:int. i <= k < j -> a[k]=c
let swap (a:array color) (i:int) (j:int) =
{ 0 <= i < length a /\ 0 <= j < length a }
......
examples/programs/insertion_sort/insertion_sort_InsertionSort_WP_parameter_insertion_sort_2.v → examples/programs/flag/flag_WP_Flag_WP_parameter_dutch_flag_1.v
View file @ 5307d60a
......@@ -4,9 +4,9 @@ Require Import ZArith.
Require Import Rbase.
Definition unit := unit.
Parameter label : Type.
Parameter mark : Type.
Parameter at1: forall (a:Type), a -> label -> a.
Parameter at1: forall (a:Type), a -> mark -> a.
Implicit Arguments at1.
......@@ -76,15 +76,6 @@ Definition set1 (a:Type)(a1:(array a)) (i:Z) (v:a): (array a) :=
end.
Implicit Arguments set1.
Definition sorted_sub(a:(map Z Z)) (l:Z) (u:Z): Prop := forall (i1:Z) (i2:Z),
(((l <= i1)%Z /\ (i1 <= i2)%Z) /\ (i2 < u)%Z) -> ((get a i1) <= (get a
i2))%Z.
Definition sorted_sub1(a:(array Z)) (l:Z) (u:Z): Prop := (sorted_sub (elts a)
l u).
Definition sorted(a:(array Z)): Prop := (sorted_sub (elts a) 0%Z (length a)).
Definition map_eq_sub (a:Type)(a1:(map Z a)) (a2:(map Z a)) (l:Z)
(u:Z): Prop := forall (i:Z), ((l <= i)%Z /\ (i < u)%Z) -> ((get a1
i) = (get a2 i)).
......@@ -156,37 +147,42 @@ Axiom array_eq_sub_permut : forall (a:Type), forall (a1:(array a)) (a2:(array
Axiom array_eq_permut : forall (a:Type), forall (a1:(array a)) (a2:(array
a)), (array_eq a1 a2) -> (permut a1 a2).
Theorem WP_parameter_insertion_sort : forall (a:Z), forall (a1:(map Z Z)),
let a2 := (mk_array a a1) in ((1%Z <= (a - 1%Z)%Z)%Z -> forall (a3:(map Z
Z)), let a4 := (mk_array a a3) in forall (i:Z), ((1%Z <= i)%Z /\
(i <= (a - 1%Z)%Z)%Z) -> (((sorted_sub a3 0%Z i) /\ (permut a4 a2)) ->
(((0%Z <= i)%Z /\ (i < a)%Z) -> let result := (get a3 i) in
((((0%Z <= i)%Z /\ (i <= i)%Z) /\ ((permut (set1 a4 i result) a2) /\
((forall (k1:Z) (k2:Z), (((0%Z <= k1)%Z /\ (k1 <= k2)%Z) /\ (k2 <= i)%Z) ->
((~ (k1 = i)) -> ((~ (k2 = i)) -> ((get a3 k1) <= (get a3 k2))%Z))) /\
forall (k:Z), (((i + 1%Z)%Z <= k)%Z /\ (k <= i)%Z) -> (result < (get a3
k))%Z))) -> forall (j:Z), forall (a5:(map Z Z)), let a6 := (mk_array a
a5) in ((((0%Z <= j)%Z /\ (j <= i)%Z) /\ ((permut (set1 a6 j result) a2) /\
((forall (k1:Z) (k2:Z), (((0%Z <= k1)%Z /\ (k1 <= k2)%Z) /\ (k2 <= i)%Z) ->
((~ (k1 = j)) -> ((~ (k2 = j)) -> ((get a5 k1) <= (get a5 k2))%Z))) /\
forall (k:Z), (((j + 1%Z)%Z <= k)%Z /\ (k <= i)%Z) -> (result < (get a5
k))%Z))) -> ((0%Z < j)%Z -> (((0%Z <= (j - 1%Z)%Z)%Z /\
((j - 1%Z)%Z < a)%Z) -> ((result < (get a5 (j - 1%Z)%Z))%Z ->
(((0%Z <= (j - 1%Z)%Z)%Z /\ ((j - 1%Z)%Z < a)%Z) -> (((0%Z <= j)%Z /\
(j < a)%Z) -> forall (a7:(map Z Z)), (a7 = (set a5 j (get a5
(j - 1%Z)%Z))) -> ((exchange match (set1 (mk_array a a7) (j - 1%Z)%Z
result) with
| mk_array _ elts1 => elts1
end match (set1 a6 j result) with
| mk_array _ elts1 => elts1
end (j - 1%Z)%Z j) -> forall (j1:Z), (j1 = (j - 1%Z)%Z) -> forall (k1:Z)
(k2:Z), (((0%Z <= k1)%Z /\ (k1 <= k2)%Z) /\ (k2 <= i)%Z) ->
((~ (k1 = j1)) -> ((~ (k2 = j1)) -> ((get a7 k1) <= (get a7
k2))%Z))))))))))))).
Inductive color :=
| Blue : color
| White : color
| Red : color .
Definition monochrome(a:(array color)) (i:Z) (j:Z) (c:color): Prop :=
forall (k:Z), ((i <= k)%Z /\ (k < j)%Z) -> ((get1 a k) = c).
Theorem WP_parameter_dutch_flag : forall (a:Z), forall (n:Z), forall (a1:(map
Z color)), ((0%Z <= n)%Z /\ (a = n)) -> forall (r:Z), forall (i:Z),
forall (b:Z), forall (a2:(map Z color)), let a3 := (mk_array a a2) in
((((((0%Z <= b)%Z /\ (b <= i)%Z) /\ (i <= r)%Z) /\ (r <= n)%Z) /\
((monochrome a3 0%Z b (Blue )) /\ ((monochrome a3 b i (White )) /\
((monochrome a3 r n (Red )) /\ ((a = n) /\ (permut_sub a2 a1 0%Z n)))))) ->
((i < r)%Z -> (((0%Z <= i)%Z /\ (i < a)%Z) -> match (get a2
i) with
| Blue => True
| White => True
| Red => forall (r1:Z), (r1 = (r - 1%Z)%Z) -> ((((0%Z <= r1)%Z /\
(r1 < a)%Z) /\ ((0%Z <= i)%Z /\ (i < a)%Z)) -> forall (a4:(map Z
color)), (exchange a4 a2 r1 i) -> (monochrome (mk_array a a4) r1 n
(Red )))
end))).
(* YOU MAY EDIT THE PROOF BELOW *)
intuition.
intuition.
unfold exchange; intuition.
destruct (get a2 i); intuition.
red; intros.
subst r1.
assert (h: (k = r-1 \/ r <= k < n)%Z) by omega.
destruct h.
subst k.
unfold get1.
auto.
unfold get1; simpl.
rewrite H21; try omega.
apply H5; omega.
Qed.
(* DO NOT EDIT BELOW *)
......
examples/programs/flag/flag_WP_Flag_WP_parameter_dutch_flag_2.v 0 → 100644
View file @ 5307d60a
(* This file is generated by Why3's Coq driver *)
(* Beware! Only edit allowed sections below *)
Require Import ZArith.
Require Import Rbase.
Definition unit := unit.
Parameter mark : Type.
Parameter at1: forall (a:Type), a -> mark -> a.
Implicit Arguments at1.
Parameter old: forall (a:Type), a -> a.
Implicit Arguments old.
Inductive ref (a:Type) :=
| mk_ref : a -> ref a.
Implicit Arguments mk_ref.
Definition contents (a:Type)(u:(ref a)): a :=
match u with
| mk_ref contents1 => contents1
end.
Implicit Arguments contents.
Parameter map : forall (a:Type) (b:Type), Type.
Parameter get: forall (a:Type) (b:Type), (map a b) -> a -> b.
Implicit Arguments get.
Parameter set: forall (a:Type) (b:Type), (map a b) -> a -> b -> (map a b).
Implicit Arguments set.
Axiom Select_eq : forall (a:Type) (b:Type), 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) (b:Type), 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 (b:Type) (a:Type), b -> (map a b).
Set Contextual Implicit.
Implicit Arguments const.
Unset Contextual Implicit.
Axiom Const : forall (b:Type) (a:Type), forall (b1:b) (a1:a), ((get (const(
b1):(map a b)) a1) = b1).
Inductive array (a:Type) :=
| mk_array : Z -> (map Z a) -> array a.
Implicit Arguments mk_array.
Definition elts (a:Type)(u:(array a)): (map Z a) :=
match u with
| mk_array _ elts1 => elts1
end.
Implicit Arguments elts.
Definition length (a:Type)(u:(array a)): Z :=
match u with
| mk_array length1 _ => length1
end.
Implicit Arguments length.
Definition get1 (a:Type)(a1:(array a)) (i:Z): a := (get (elts a1) i).
Implicit Arguments get1.
Definition set1 (a:Type)(a1:(array a)) (i:Z) (v:a): (array a) :=
match a1 with
| mk_array xcl0 _ => (mk_array xcl0 (set (elts a1) i v))
end.
Implicit Arguments set1.
Definition map_eq_sub (a:Type)(a1:(map Z a)) (a2:(map Z a)) (l:Z)
(u:Z): Prop := forall (i:Z), ((l <= i)%Z /\ (i < u)%Z) -> ((get a1
i) = (get a2 i)).
Implicit Arguments map_eq_sub.
Definition exchange (a:Type)(a1:(map Z a)) (a2:(map Z a)) (i:Z)
(j:Z): Prop := ((get a1 i) = (get a2 j)) /\ (((get a2 i) = (get a1 j)) /\
forall (k:Z), ((~ (k = i)) /\ ~ (k = j)) -> ((get a1 k) = (get a2 k))).
Implicit Arguments exchange.
Axiom exchange_set : forall (a:Type), forall (a1:(map Z a)), forall (i:Z)
(j:Z), (exchange a1 (set (set a1 i (get a1 j)) j (get a1 i)) i j).
Inductive permut_sub{a:Type} : (map Z a) -> (map Z a) -> Z -> Z -> Prop :=
| permut_refl : forall (a1:(map Z a)) (a2:(map Z a)), forall (l:Z) (u:Z),
(map_eq_sub a1 a2 l u) -> (permut_sub a1 a2 l u)
| permut_sym : forall (a1:(map Z a)) (a2:(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 Z a)) (a2:(map Z a)) (a3:(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 Z a)) (a2:(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))).
Implicit Arguments permut_sub.
Axiom permut_weakening : forall (a:Type), forall (a1:(map Z a)) (a2:(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), forall (a1:(map Z a)) (a2:(map Z a)),
forall (l:Z) (u:Z), (l <= u)%Z -> ((permut_sub a1 a2 l u) -> forall (i:Z),
((i < l)%Z \/ (u <= i)%Z) -> ((get a2 i) = (get a1 i))).
Axiom permut_exists : forall (a:Type), forall (a1:(map Z a)) (a2:(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) /\ ((get a2
i) = (get a1 j)).
Definition exchange1 (a:Type)(a1:(array a)) (a2:(array a)) (i:Z)
(j:Z): Prop := (exchange (elts a1) (elts a2) i j).
Implicit Arguments exchange1.
Definition permut_sub1 (a:Type)(a1:(array a)) (a2:(array a)) (l:Z)
(u:Z): Prop := (permut_sub (elts a1) (elts a2) l u).
Implicit Arguments permut_sub1.
Definition permut (a:Type)(a1:(array a)) (a2:(array a)): Prop :=
((length a1) = (length a2)) /\ (permut_sub (elts a1) (elts a2) 0%Z
(length a1)).
Implicit Arguments permut.
Axiom exchange_permut : forall (a:Type), forall (a1:(array a)) (a2:(array a))
(i:Z) (j:Z), (exchange1 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)))).
Definition array_eq_sub (a:Type)(a1:(array a)) (a2:(array a)) (l:Z)
(u:Z): Prop := (map_eq_sub (elts a1) (elts a2) l u).
Implicit Arguments array_eq_sub.
Definition array_eq (a:Type)(a1:(array a)) (a2:(array a)): Prop :=
((length a1) = (length a2)) /\ (array_eq_sub a1 a2 0%Z (length a1)).
Implicit Arguments array_eq.
Axiom array_eq_sub_permut : forall (a:Type), forall (a1:(array a)) (a2:(array
a)) (l:Z) (u:Z), (array_eq_sub a1 a2 l u) -> (permut_sub1 a1 a2 l u).
Axiom array_eq_permut : forall (a:Type), forall (a1:(array a)) (a2:(array
a)), (array_eq a1 a2) -> (permut a1 a2).
Inductive color :=
| Blue : color
| White : color
| Red : color .
Definition monochrome(a:(array color)) (i:Z) (j:Z) (c:color): Prop :=
forall (k:Z), ((i <= k)%Z /\ (k < j)%Z) -> ((get1 a k) = c).
Theorem WP_parameter_dutch_flag : forall (a:Z), forall (n:Z), forall (a1:(map
Z color)), ((0%Z <= n)%Z /\ (a = n)) -> forall (r:Z), forall (i:Z),
forall (b:Z), forall (a2:(map Z color)), let a3 := (mk_array a a2) in
((((((0%Z <= b)%Z /\ (b <= i)%Z) /\ (i <= r)%Z) /\ (r <= n)%Z) /\
((monochrome a3 0%Z b (Blue )) /\ ((monochrome a3 b i (White )) /\
((monochrome a3 r n (Red )) /\ ((a = n) /\ (permut_sub a2 a1 0%Z n)))))) ->
((i < r)%Z -> (((0%Z <= i)%Z /\ (i < a)%Z) -> match (get a2
i) with
| Blue => (((0%Z <= b)%Z /\ (b < a)%Z) /\ ((0%Z <= i)%Z /\
(i < a)%Z)) -> forall (a4:(map Z color)), (exchange a4 a2 b i) ->
forall (b1:Z), (b1 = (b + 1%Z)%Z) -> forall (i1:Z),
(i1 = (i + 1%Z)%Z) -> (monochrome (mk_array a a4) 0%Z b1 (Blue ))
| White => True
| Red => True
end))).
(* YOU MAY EDIT THE PROOF BELOW *)
unfold exchange; intuition.
destruct (get a2 i); intuition.
red; intros.
subst b1 i1.
assert (h: (0 <= k < b \/ k=b)%Z) by omega.
destruct h.
unfold get1; simpl.
rewrite H20; try omega.
apply H4; omega.
subst k; auto.
Qed.
(* DO NOT EDIT BELOW *)
examples/programs/flag/flag_WP_Flag_WP_parameter_dutch_flag_3.v 0 → 100644
View file @ 5307d60a
(* This file is generated by Why3's Coq driver *)
(* Beware! Only edit allowed sections below *)
Require Import ZArith.
Require Import Rbase.
Definition unit := unit.
Parameter mark : Type.
Parameter at1: forall (a:Type), a -> mark -> a.
Implicit Arguments at1.
Parameter old: forall (a:Type), a -> a.
Implicit Arguments old.
Inductive ref (a:Type) :=
| mk_ref : a -> ref a.
Implicit Arguments mk_ref.
Definition contents (a:Type)(u:(ref a)): a :=
match u with
| mk_ref contents1 => contents1
end.
Implicit Arguments contents.
Parameter map : forall (a:Type) (b:Type), Type.
Parameter get: forall (a:Type) (b:Type), (map a b) -> a -> b.
Implicit Arguments get.
Parameter set: forall (a:Type) (b:Type), (map a b) -> a -> b -> (map a b).
Implicit Arguments set.
Axiom Select_eq : forall (a:Type) (b:Type), 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) (b:Type), 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 (b:Type) (a:Type), b -> (map a b).
Set Contextual Implicit.
Implicit Arguments const.
Unset Contextual Implicit.
Axiom Const : forall (b:Type) (a:Type), forall (b1:b) (a1:a), ((get (const(
b1):(map a b)) a1) = b1).
Inductive array (a:Type) :=
| mk_array : Z -> (map Z a) -> array a.
Implicit Arguments mk_array.
Definition elts (a:Type)(u:(array a)): (map Z a) :=
match u with
| mk_array _ elts1 => elts1
end.
Implicit Arguments elts.
Definition length (a:Type)(u:(array a)): Z :=
match u with
| mk_array length1 _ => length1
end.
Implicit Arguments length.
Definition get1 (a:Type)(a1:(array a)) (i:Z): a := (get (elts a1) i).
Implicit Arguments get1.
Definition set1 (a:Type)(a1:(array a)) (i:Z) (v:a): (array a) :=
match a1 with
| mk_array xcl0 _ => (mk_array xcl0 (set (elts a1) i v))
end.
Implicit Arguments set1.
Definition map_eq_sub (a:Type)(a1:(map Z a)) (a2:(map Z a)) (l:Z)
(u:Z): Prop := forall (i:Z), ((l <= i)%Z /\ (i < u)%Z) -> ((get a1
i) = (get a2 i)).
Implicit Arguments map_eq_sub.
Definition exchange (a:Type)(a1:(map Z a)) (a2:(map Z a)) (i:Z)
(j:Z): Prop := ((get a1 i) = (get a2 j)) /\ (((get a2 i) = (get a1 j)) /\
forall (k:Z), ((~ (k = i)) /\ ~ (k = j)) -> ((get a1 k) = (get a2 k))).
Implicit Arguments exchange.
Axiom exchange_set : forall (a:Type), forall (a1:(map Z a)), forall (i:Z)
(j:Z), (exchange a1 (set (set a1 i (get a1 j)) j (get a1 i)) i j).
Inductive permut_sub{a:Type} : (map Z a) -> (map Z a) -> Z -> Z -> Prop :=
| permut_refl : forall (a1:(map Z a)) (a2:(map Z a)), forall (l:Z) (u:Z),
(map_eq_sub a1 a2 l u) -> (permut_sub a1 a2 l u)
| permut_sym : forall (a1:(map Z a)) (a2:(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 Z a)) (a2:(map Z a)) (a3:(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 Z a)) (a2:(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))).
Implicit Arguments permut_sub.
Axiom permut_weakening : forall (a:Type), forall (a1:(map Z a)) (a2:(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), forall (a1:(map Z a)) (a2:(map Z a)),
forall (l:Z) (u:Z), (l <= u)%Z -> ((permut_sub a1 a2 l u) -> forall (i:Z),
((i < l)%Z \/ (u <= i)%Z) -> ((get a2 i) = (get a1 i))).
Axiom permut_exists : forall (a:Type), forall (a1:(map Z a)) (a2:(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) /\ ((get a2
i) = (get a1 j)).
Definition exchange1 (a:Type)(a1:(array a)) (a2:(array a)) (i:Z)
(j:Z): Prop := (exchange (elts a1) (elts a2) i j).
Implicit Arguments exchange1.
Definition permut_sub1 (a:Type)(a1:(array a)) (a2:(array a)) (l:Z)
(u:Z): Prop := (permut_sub (elts a1) (elts a2) l u).