# [Easycrypt-club] How to use local variable in a lemma

François Dupressoir fdupress at gmail.com
Mon Jan 22 11:11:49 CET 2018

```Hello Sarah,

You cannot use local variable x in the statement of a lemma: at the points where the precondition and postcondition are interpreted (semantically), the variable does not exist in memory.

Going slightly further, although EasyCrypt lets you define G as you did, it should have warned that x was used before being defined. This will be problematic for a lot of proofs (in particular anything that involves probabilities will likely be very hard to prove—probabilistic and non-deterministic behaviours do not mix).

So you have two options moving forward:
1) Make x a parameter to procedure G.g (and your statement will then mean what you want);
2) Make x a global variable of module G (and you then need to replace x with G.x in your theorem statement).

That being said, I do not want to necessarily close the discussion on interpreting pure hoare specifications for non-deterministic procedures: if you feel you really need this, please do try and convince us (mostly Pierre-Yves and Benjamin).

Best,
François

From: sarah chabane
Sent: 22 January 2018 10:00
To: easycrypt-club at lists.gforge.inria.fr
Subject: [Easycrypt-club] How to use local variable in a lemma

Hi,
I need to use a local variable of a procedure in a lemma,

for example , for this module :

module G = {
proc g() : int ={
var r, x : int;
if (x < 0) {
r = 5; } else {
r = 10;
}
return r;
}
}.

I want to proof this lemma:

lemma ex : forall v,
hoare [ G.g : v = x ==> if v < 0  then  res = 5 else res <> 5 ].

How can i use the x of the proc G.g ?

Best regards.
Sarah.

-------------- section suivante --------------
Une pièce jointe HTML a été nettoyée...
URL: <http://lists.gforge.inria.fr/pipermail/easycrypt-club/attachments/20180122/f7641db5/attachment.html>
```