GitLab

Sometimes when we want to prove such functions:

let f x : result
  ensures { forall y. P(x,y) -> Q(x,y) }

We need to prove with a ghost variable, for easing the proof

let f' x (ghost y) : result
  requires { P(x,y) }
  ensures { Q(x,y) }

However it is not possible to prove the first function using the second. We propose to add a new construction which allows it.

let f x : result
  ensures { forall y. P(x,y) -> Q(x,y) }
 =
 forall y requires { P(x,y) } in 
  f' x y

The semantic of this function is not completely clear:

• should a VC be generated to check that it exists such y
• what if the result contains a ghost
• what if there are ghost effect