Commit 3180aa4b authored by Jean-Christophe Filliâtre's avatar Jean-Christophe Filliâtre
Browse files

gallery: dirichlet renamed into pigeonhole

(there is already something called dirichlet in the gallery)
parent f1363461
...@@ -3,7 +3,7 @@ ...@@ -3,7 +3,7 @@
Proved using a lemma function. *) Proved using a lemma function. *)
module Dirichlet module Pigeonhole
use import HighOrd use import HighOrd
use import int.Int use import int.Int
...@@ -19,7 +19,7 @@ module Dirichlet ...@@ -19,7 +19,7 @@ module Dirichlet
variant { n } variant { n }
= if n = 0 then empty else add (n-1) (below (n-1)) = if n = 0 then empty else add (n-1) (below (n-1))
let lemma dirichlet (n m: int) (f: int -> int) let lemma pigeonhole (n m: int) (f: int -> int)
requires { 0 <= m < n } requires { 0 <= m < n }
requires { forall i. 0 <= i < n -> 0 <= f i < m } requires { forall i. 0 <= i < n -> 0 <= f i < m }
ensures { exists i1, i2. 0 <= i1 < i2 < n /\ f i1 = f i2 } ensures { exists i1, i2. 0 <= i1 < i2 < n /\ f i1 = f i2 }
......
...@@ -4,44 +4,44 @@ ...@@ -4,44 +4,44 @@
<why3session shape_version="4"> <why3session shape_version="4">
<prover id="0" name="Alt-Ergo" version="0.99.1" timelimit="6" memlimit="1000"/> <prover id="0" name="Alt-Ergo" version="0.99.1" timelimit="6" memlimit="1000"/>
<prover id="6" name="Alt-Ergo" version="0.95.1" timelimit="6" memlimit="1000"/> <prover id="6" name="Alt-Ergo" version="0.95.1" timelimit="6" memlimit="1000"/>
<file name="../dirichlet.mlw" expanded="true"> <file name="../pigeonhole.mlw" expanded="true">
<theory name="Dirichlet" sum="8ee565a294b83da869ffcfd8fb11b973" expanded="true"> <theory name="Pigeonhole" sum="8ee565a294b83da869ffcfd8fb11b973" expanded="true">
<goal name="WP_parameter below" expl="VC for below" expanded="true"> <goal name="WP_parameter below" expl="VC for below" expanded="true">
<proof prover="6"><result status="valid" time="0.01" steps="75"/></proof> <proof prover="6"><result status="valid" time="0.01" steps="75"/></proof>
</goal> </goal>
<goal name="WP_parameter dirichlet" expl="VC for dirichlet" expanded="true"> <goal name="WP_parameter pigeonhole" expl="VC for pigeonhole" expanded="true">
<transf name="split_goal_wp" expanded="true"> <transf name="split_goal_wp" expanded="true">
<goal name="WP_parameter dirichlet.1" expl="1. precondition"> <goal name="WP_parameter pigeonhole.1" expl="1. precondition">
<proof prover="0"><result status="valid" time="0.02" steps="3"/></proof> <proof prover="0"><result status="valid" time="0.02" steps="3"/></proof>
</goal> </goal>
<goal name="WP_parameter dirichlet.2" expl="2. assertion"> <goal name="WP_parameter pigeonhole.2" expl="2. assertion">
<proof prover="0"><result status="valid" time="0.01" steps="4"/></proof> <proof prover="0"><result status="valid" time="0.01" steps="4"/></proof>
</goal> </goal>
<goal name="WP_parameter dirichlet.3" expl="3. unreachable point"> <goal name="WP_parameter pigeonhole.3" expl="3. unreachable point">
<proof prover="0"><result status="valid" time="0.02" steps="5"/></proof> <proof prover="0"><result status="valid" time="0.02" steps="5"/></proof>
</goal> </goal>
<goal name="WP_parameter dirichlet.4" expl="4. loop invariant init"> <goal name="WP_parameter pigeonhole.4" expl="4. loop invariant init">
<proof prover="0"><result status="valid" time="0.01" steps="7"/></proof> <proof prover="0"><result status="valid" time="0.01" steps="7"/></proof>
</goal> </goal>
<goal name="WP_parameter dirichlet.5" expl="5. loop invariant init"> <goal name="WP_parameter pigeonhole.5" expl="5. loop invariant init">
<proof prover="0"><result status="valid" time="0.01" steps="8"/></proof> <proof prover="0"><result status="valid" time="0.01" steps="8"/></proof>
</goal> </goal>
<goal name="WP_parameter dirichlet.6" expl="6. postcondition"> <goal name="WP_parameter pigeonhole.6" expl="6. postcondition">
<proof prover="6"><result status="valid" time="0.02" steps="22"/></proof> <proof prover="6"><result status="valid" time="0.02" steps="22"/></proof>
</goal> </goal>
<goal name="WP_parameter dirichlet.7" expl="7. loop invariant preservation"> <goal name="WP_parameter pigeonhole.7" expl="7. loop invariant preservation">
<proof prover="0"><result status="valid" time="0.01" steps="11"/></proof> <proof prover="0"><result status="valid" time="0.01" steps="11"/></proof>
</goal> </goal>
<goal name="WP_parameter dirichlet.8" expl="8. loop invariant preservation"> <goal name="WP_parameter pigeonhole.8" expl="8. loop invariant preservation">
<proof prover="0"><result status="valid" time="0.02" steps="53"/></proof> <proof prover="0"><result status="valid" time="0.02" steps="53"/></proof>
</goal> </goal>
<goal name="WP_parameter dirichlet.9" expl="9. precondition"> <goal name="WP_parameter pigeonhole.9" expl="9. precondition">
<proof prover="0"><result status="valid" time="0.00" steps="5"/></proof> <proof prover="0"><result status="valid" time="0.00" steps="5"/></proof>
</goal> </goal>
<goal name="WP_parameter dirichlet.10" expl="10. assertion"> <goal name="WP_parameter pigeonhole.10" expl="10. assertion">
<proof prover="0"><result status="valid" time="0.02" steps="28"/></proof> <proof prover="0"><result status="valid" time="0.02" steps="28"/></proof>
</goal> </goal>
<goal name="WP_parameter dirichlet.11" expl="11. unreachable point"> <goal name="WP_parameter pigeonhole.11" expl="11. unreachable point">
<proof prover="0"><result status="valid" time="0.01" steps="9"/></proof> <proof prover="0"><result status="valid" time="0.01" steps="9"/></proof>
</goal> </goal>
</transf> </transf>
......
(** Random Access Lists. (** Random Access Lists.
(Okasaki, "Purely Functional Data Structures", 10.1.2.)
The code below uses polymorphic recursion (both in the logic The code below uses polymorphic recursion (both in the logic
and in the programs). and in the programs).
BUGS: Author: Jean-Christophe Filliâtre (CNRS)
- induction_ty_lex has no effect on a goal involving polymorphic recursion
- a lemma function is not allowed to perform polymorphic recursion?
*) *)
module RandomAccessList module RandomAccessList
...@@ -24,13 +22,13 @@ module RandomAccessList ...@@ -24,13 +22,13 @@ module RandomAccessList
| Zero (ral ('a, 'a)) | Zero (ral ('a, 'a))
| One 'a (ral ('a, 'a)) | One 'a (ral ('a, 'a))
function flatten (l: list ('a , 'a)) : list 'a function flatten (l: list ('a, 'a)) : list 'a
= match l with = match l with
| Nil -> Nil | Nil -> Nil
| Cons (x, y) l1 -> Cons x (Cons y (flatten l1)) | Cons (x, y) l1 -> Cons x (Cons y (flatten l1))
end end
let rec lemma length_flatten (l:list ('a,'a)) let rec lemma length_flatten (l:list ('a, 'a))
ensures { length (flatten l) = 2 * length l } ensures { length (flatten l) = 2 * length l }
variant { l } variant { l }
= match l with = match l with
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment