[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 mailing list