[Why3-club] how to pass arguments to commands in IDE 1.2.0

Sylvain Dailler sylvain.dailler at inria.fr
Fri Feb 22 14:56:42 CET 2019


On 22/02/2019 13:50, Jean-Jacques Levy wrote:
> Dear Friends,
>
> in why3.1.2.0, I cannot succeed in passing an argument to command in line 0/0/0 !!
> -------------------------
> goal list_simpl_r :
>    forall l1:list 'a, l2:list 'a, l:list 'a. (l1 ++ l) = (l2 ++ l) -> l1 = l2
> -------------------------
> Following hypothesis was not found: l1

If you want to use a transformation with arguments, you currently need 
to have "l1" in the context: that's what the error tells you. You can do 
"intros l1" for that.

This particular transformation seems to not be doing what is expected: 
we will investigate if we can improve it or remove it in future versions.

> Transformation failed:
> induction_arg_ty_lex  l1
>
> induction_arg_ty_lex
> type: lsymbol -> list task
> induction_arg_ty_lex <ls> performs induction_ty_lex on ls.
> -------------------------
> In why3.0.88.3, it was simple induction_ty_lex on ‘l1’ with keyword "induction"
> and if induction is done on l2, then generalization is lost.

I think you can still use induction with induction_ty_lex as you did in 
0.88. In your example, add the attribute [@induction]:

-------------------------
goal list_simpl_r :
   forall l1 [@induction]:list 'a, l2:list 'a, l:list 'a. (l1 ++ l) = (l2 ++ l) -> l1 = l2
-------------------------

and call "induction_ty_lex". This should give you the same result as 
version 0.88.

Hope this can help,
Sylvain



More information about the Why3-club mailing list