Coq to Why3: Proof of aux lemma of function correction

Miscellaneous
1

Hi! I know this probably isn’t the right place to ask this, but I can’t get an answer at stackOverflow and Why3 doesn’t really have a community or an easy way to ask questions…

So I have this proof in Coq:

Lemma executeCompile : forall (state:M.t Z) (ins:aexp) (p:list insSt) (stack:list Z),
  execute state stack (compile ins ++ p) = execute state ((aeval ins state)::stack) p.
Proof.
  intros state ins. induction ins;intros p stack;simpl.
  - reflexivity. 
  - reflexivity.
  - Check app_assoc_reverse. rewrite app_assoc_reverse. rewrite IHins.
      simpl. reflexivity.
  - rewrite app_assoc_reverse. rewrite IHins1.
      rewrite app_assoc_reverse. rewrite IHins2.
      simpl. reflexivity.
  - rewrite app_assoc_reverse. rewrite IHins1.
      rewrite app_assoc_reverse. rewrite IHins2.
      simpl. reflexivity.
  - rewrite app_assoc_reverse. rewrite IHins1.
      rewrite app_assoc_reverse. rewrite IHins2.
      simpl. reflexivity. 
Qed.

And I have the same one in Why3:

lemma compile_correct_aux : forall a : aexp, s  state, st : stack, p : prog.
  execute s st (compile a ++ p) = execute s (Cons (aeval a s) st) p

But, for some reason, Why3 can’t seem to prove it… Is there a way to sort of “translate” Coq’s proof into Why3 “language”?

Thank you!

2

Why3 has coq mode for vérification conditions but unlike with automated provers it does not try to prove them. You need to write the proofs by yourself in the generated files.