CODEWITHSUNDEEP
automationcoq
Veky
Veky

Reputation: 2745

coq auto says simple apply fails but it works manually

(the exercise is from Software foundations, I can give all relevant definitions but there'll be a lot of them) Consider this:

Goal empty_st =[ X := 1 ]=> (X ↦ 1).
debug auto.    (* (* debug auto: *)
                  * assumption. (*fail*)
                  * intro. (*fail*)
                  * simple apply E_Ass (in core). (*fail*) <- note this fails
                  * simple apply E_Skip (in core). (*fail*) *)
simple apply E_Ass. (* <- but this works *)
Qed.

Usually, my problems with auto are that it fails to find the relevant thing to apply. Here it does that flawlessly, but for some reason fails to apply it. How can I convince it to try harder?

(Yes, it's the same E_Ass. And no, unfolding doesn't help.)

Upvotes: 2

Views: 120

Answers (1)

M Soegtrop
M Soegtrop

Reputation: 1448

It might fail because the conclusion of E_Ass does not immediately match your goal. auto does check this upfront and does not even try to apply a lemma if the conclusion does not directly match. Afair fail includes "didn't try". Even simple_apply does some conversion between the applied lemma and the goal. You can try to add a hint with a variant of E_Ass, which is converted to match the goal. What is the type of E_Ass?

Upvotes: 2

Related Questions