Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Beginner problem writing tactic

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Beginner problem writing tactic


Chronological Thread 
  • From: Adam Chlipala <adamc AT csail.mit.edu>
  • To: Rui Baptista <rpgcbaptista AT gmail.com>
  • Cc: "coq-club AT inria.fr" <coq-club AT inria.fr>
  • Subject: Re: [Coq-Club] Beginner problem writing tactic
  • Date: Thu, 01 Aug 2013 20:19:35 -0400

On 08/01/2013 08:09 PM, Rui Baptista wrote:
But the tactic

progress repeat
match goal with
| [H1 : _ |- _] => progress (
apply (proj1 OJQZ) in H1 ||
(apply eq_sym in H1; apply (proj1 OJQZ) in H1; try apply eq_sym in H1))
| [|- _] => progress (
apply (proj2 OJQZ) ||
(apply eq_sym; apply (proj2 OJQZ); try apply eq_sym))
end.

is just the result of "unfolding" rw_aux OJQZ. Why does that one work, but not the other?

I've made the argument of OJQZ implicit just so I could feed it to proj1 and proj2.

When I run your tactic that fails, I literally see an error message saying that the parameter of [OJQZ] can't be inferred, so that seems pretty clearly to be the problem. The extra context of [apply] is sufficient to determine the parameter, perhaps because of some magic in the [apply] implementation that can only be achieved in OCaml, not in your own Ltac definitions.



Archive powered by MHonArc 2.6.18.

Top of Page