[Why3-club] Question on induction_arg_ty_lex

Sylvain Dailler sylvain.dailler at inria.fr
Mon Mar 4 11:21:16 CET 2019


> 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.

> - 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.

>   in the same way that "induction_ty_lex"? I reproduced this phenomemon in several other examples, but this one seemed to be the simplest.

To our knowledge, "induction_ty_lex" has a correct behavior. I recommend 
to replace the occurences of "induction_arg_ty_lex" with 
"induction_ty_lex" until we solve the bug for "induction_arg_ty_lex".

Best regards,

Sylvain Dailler

More information about the Why3-club mailing list