[Why3-club] Question on induction_arg_ty_lex

Jorge Sousa Pinto jsp at di.uminho.pt
Mon Mar 4 15:20:44 CET 2019


Hi, 

> On Mar 4, 2019, at 10:21, Sylvain Dailler <sylvain.dailler at inria.fr> wrote:
> 
> Hello,
> 
> 
>> I get the following behaviour:
>> 
>> - Both lemmas can be proved with the command "induction_ty_lex"
>> (eval_fp can also be proved with induction_pr);
> 
> The two transformations induction_pr and induction_ty_lex do not work in the same way. induction_ty_lex performs an induction on "e" of type "expr" (induction on a datastructure). "induction_pr" does an induction on the inductive predicate "eval_p" which turns out to allow proving your lemma too.

Yes, I had understood that. I just mentioned induction_pr in passing, it wasn’t relevant for my question, which was about induction_arg_ty_lex. 

>> - For eval_fp, typing "intros e” and then "induction_arg_ty_lex e" produces exactly the same goal as "induction_ty_lex", using structural induction on e — from what I understand this is the expected behaviour of this command.
> 
> Yes, in this case, "induction_arg_ty_lex" seems to work.
> 
>> - However, for eval_determ, "induction_arg_ty_lex e" does not produce any useful transformation (it just reintroduces e in the goal).
>> My question is, why is "induction_arg_ty_lex e" not transforming the goal in the second case,
> 
> Sorry, I was not clear in my answer to Jean-Jacques Lévy. The reason is most likely that there is a bug in this transformation: we will investigate and return to you.

Understood, thank you! 

Best,
Jorge





More information about the Why3-club mailing list