stdlib/witness.mlw

   1
   2 (** {1 Witnesses of existential proofs} *)
   3
   4 (** {2 Non-constructive existence of a witness} *)
   5
   6 module Witness
   7
   8   val ghost function witness (p: 'a -> bool) : 'a
   9     requires { exists x. p x }
  10     ensures  { p result }
  11
  12 end
  13
  14 (** {2 Constructive existence of a witness}
  15
  16     Given a predicate `p` over integers and the existence of
  17     a nonnegative integer `n` such that `p n`, one can build
  18     a witness using a linear search starting from 0.
  19
  20     The difficulty here is to prove termination. We use a custom
  21     variant predicate and we prove the accessibility of all
  22     integers for which there exists a witnes above.
  23
  24     This proof is adapted from Coq's standard library
  25     (file ConstructiveEpsilon.v contributed by Yevgeniy Makarov
  26     and Jean-François Monin).
  27 *)
  28
  29 module Nat
  30
  31   use int.Int
  32   use relations.WellFounded
  33
  34   (** since a custom variant relation has to be a toplevel predicate symbol,
  35       we store the predicate `p` inside the variant expression *)
  36   predicate r (x y: ((int->bool),int)) =
  37     let p, x = x in
  38     let q, y = y in
  39     p = q && x = y+1 > 0 && not (p y)
  40
  41   let function witness (p: int -> bool) : int
  42     requires { exists n. n >= 0 /\ p n }
  43     ensures  { result >= 0 /\ p result }
  44   = let lemma l1 (x: int)
  45       requires { x >= 0 /\ p x } ensures { acc r (p,x) }
  46       = let lemma l11 (y: (int->bool,int))
  47           requires { r y (p,x) } ensures { acc r y } = () in
  48       () in
  49     let rec lemma l2 (x n: int) variant { n }
  50       requires { x >= 0 /\ n >= 0 /\ p (x + n) }
  51       ensures  { acc r (p,x) }
  52       = if n > 0 then l2 (x+1) (n-1) in
  53     let rec search (n: int) : int
  54       requires { n >= 0 /\ exists x. x >= n && p x }
  55       variant  { (p,n) with r }
  56       ensures  { result >= 0 /\ p result }
  57       = if p n then n else search (n+1) in
  58     search 0
  59
  60 end