Coq to Why3: Proof 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

Hi,
AFAIK you don’t need to translate because Coq is one of the prover supported by why3. You just need to generate coq VCs and prove them by hand. Why3 should remember the proofs (although you might want to save them anyway just in case).