[Why3-club] Question on induction_arg_ty_lex
Jorge Sousa Pinto
jsp at di.uminho.pt
Fri Mar 1 19:24:42 CET 2019
This is a newbie question on using commands to conduct inductive proofs in Why3 1.2.0 (following Jean-Jacques Lévy’s recent question on the same topic, but I can't compare the behaviour with previous versions since this is the first time I use the command language).
Consider for instance a theory containing a function and an inductive predicate for expression evaluation as follows (the missing things are what you would expect):
function eval_f (s:state) (e:expr) : int =
match e with
| Econst n -> n
| Evar x -> get s x
| Ebin e1 op e2 ->
eval_bin (eval_f s e1) op (eval_f s e2)
inductive eval_p state expr int =
| eval_const :
forall s:state, n :int. eval_p s (Econst n) n
| eval_var :
forall s:state, x :ident. eval_p s (Evar x) (get s x)
| eval_bin :
forall s:state, e1 e2 : expr, v1 v2 :int, op :operator.
eval_p s e1 v1 ->
eval_p s e2 v2 ->
eval_p s (Ebin e1 op e2) (eval_bin v1 op v2)
lemma eval_fp : forall e[@induction] :expr, s :state, v :int.
eval_p s e v -> v = eval_f s e
lemma eval_determ : forall e[@induction] :expr, s :state, v1 v2 :int.
eval_p s e v1 -> eval_p s e v2 -> v1 = v2
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);
- 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.
- 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, in the same way that "induction_ty_lex"? I reproduced this phenomemon in several other examples, but this one seemed to be the simplest.
Thank you for any help!
Jorge Sousa Pinto
More information about the Why3-club