[Why3-club] Question on induction_arg_ty_lex
Sylvain Dailler
sylvain.dailler at inria.fr
Mon Mar 4 11:21:16 CET 2019
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.
>
> - 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