From 17d699907b3a34fab5499c105c50a327f2a198ba Mon Sep 17 00:00:00 2001
From: JeanChristophe Filliatre
Date: Sun, 17 Jun 2018 11:09:22 +0200
Subject: [PATCH] library: two versions of witness
the constructive version is now in witness.Nat
the nonconstructive version is witness.Witness

examples/stdlib/witness/why3session.xml  2 +
stdlib/witness.mlw  23 ++++++++++++++++++
2 files changed, 19 insertions(+), 6 deletions()
diff git a/examples/stdlib/witness/why3session.xml b/examples/stdlib/witness/why3session.xml
index 0711aa251..ba4cb01af 100644
 a/examples/stdlib/witness/why3session.xml
+++ b/examples/stdlib/witness/why3session.xml
@@ 6,7 +6,7 @@

+
diff git a/stdlib/witness.mlw b/stdlib/witness.mlw
index 441b976b7..c7c9e7df7 100644
 a/stdlib/witness.mlw
+++ b/stdlib/witness.mlw
@@ 1,12 +1,23 @@
(** {1 Constructive existence of a witness}
+(** {1 Witnesses of existential proofs} *)
+
+(** {2 Nonconstructive existence of a witness} *)
+
+module Witness
+
+ val ghost function witness (p: 'a > bool) : 'a
+ requires { exists x. p x }
+ ensures { p result }
+
+end
+
+(** {2 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
+ The difficulty here is to prove termination. We use a custom
variant predicate and we prove the accessibility of all
integers for which there exists a witnes above.
@@ 15,17 +26,19 @@
and JeanFrançois Monin).
*)
module Witness
+module Nat
use int.Int
use relations.WellFounded
+ (** since a custom variant relation has to be a toplevel predicate symbol,
+ we store the predicate `p` inside the variant expression *)
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
+ let function witness (p: int > bool) : int
requires { exists n. n >= 0 /\ p n }
ensures { result >= 0 /\ p result }
= let lemma l1 (x: int)

2.24.1