new library witness.Witness

exhibits, constructively, a nonnegative integer n such that p n
whenever we can prove the existence of such an integer
parent 21537ba3
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="5">
<prover id="0" name="Alt-Ergo" version="2.0.0" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="2" name="CVC4" version="1.5" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="4" name="Eprover" version="1.8-001" timelimit="16" steplimit="0" memlimit="1000"/>
<file name="../../../stdlib/witness.mlw" proved="true">
<theory name="Witness" proved="true">
<goal name="VC witness" expl="VC for witness" proved="true">
<transf name="split_vc" proved="true" >
<goal name="VC witness.0" expl="postcondition" proved="true">
<proof prover="2"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC witness.1" expl="postcondition" proved="true">
<proof prover="2"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC witness.2" expl="variant decrease" proved="true">
<proof prover="2"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC witness.3" expl="precondition" proved="true">
<proof prover="2"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="VC witness.4" expl="postcondition" proved="true">
<proof prover="0"><result status="valid" time="0.01" steps="54"/></proof>
</goal>
<goal name="VC witness.5" expl="variant decrease" proved="true">
<transf name="split_vc" proved="true" >
<goal name="VC witness.5.0" expl="VC for witness" proved="true">
<proof prover="2"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="VC witness.5.1" expl="VC for witness" proved="true">
<proof prover="4"><result status="valid" time="13.91"/></proof>
</goal>
</transf>
</goal>
<goal name="VC witness.6" expl="precondition" proved="true">
<proof prover="2"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="VC witness.7" expl="postcondition" proved="true">
<proof prover="2"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="VC witness.8" expl="precondition" proved="true">
<proof prover="2"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="VC witness.9" expl="postcondition" proved="true">
<proof prover="2"><result status="valid" time="0.01"/></proof>
</goal>
</transf>
</goal>
</theory>
</file>
</why3session>
(** {1 Constructive existence of a witness}
Given a predicate [p] over integers and the existence of
a nonnegative integer [n] such that [p n], one can build
a witness using a linear search starting from 0.
The difficulty here is to prove the termination of the
function implementing this linear search. We use a custom
variant predicate and we prove the accessibility of all
integers for which there exists a witnes above.
This proof is adapted from Coq's standard library
(file ConstructiveEpsilon.v contributed by Yevgeniy Makarov
and Jean-François Monin).
*)
module Witness
use import int.Int
use import relations.WellFounded
predicate r (x y: ((int->bool),int)) =
let p, x = x in
let q, y = y in
p = q && x = y+1 > 0 && not (p y)
let witness (p: int -> bool) : int
requires { exists n. n >= 0 /\ p n }
ensures { result >= 0 /\ p result }
= let lemma l1 (x: int)
requires { x >= 0 /\ p x } ensures { acc r (p,x) }
= let lemma l11 (y: (int->bool,int))
requires { r y (p,x) } ensures { acc r y } = () in
() in
let rec lemma l2 (x n: int) variant { n }
requires { x >= 0 /\ n >= 0 /\ p (x + n) }
ensures { acc r (p,x) }
= if n > 0 then l2 (x+1) (n-1) in
let rec search (n: int) : int
requires { n >= 0 /\ exists x. x >= n && p x }
variant { (p,n) with r }
ensures { result >= 0 /\ p result }
= if p n then n else search (n+1) in
search 0
end
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