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

Jean-Jacques Levy jean-jacques.levy at inria.fr
Fri Feb 22 15:27:57 CET 2019


ok.. merci. Mais en mettant l’attribut [@induction] (nouvelle syntaxe), je dois faire induction_ty_lex et destruct l2 !! 

Why3.1.2.0 serait-il un (autre) nouveau nom pour Coq ?

A+, -JJ-

> Le 22 févr. 2019 à 14:56, Sylvain Dailler <sylvain.dailler at inria.fr> a écrit :
> 
> 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