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: rpgcbaptista AT gmail.com
  • Cc: coq-club AT inria.fr
  • Subject: Re: [Coq-Club] Beginner problem writing tactic
  • Date: Thu, 01 Aug 2013 19:36:03 -0400

On 08/01/2013 07:30 PM,
rpgcbaptista AT gmail.com
wrote:
Axiom OJQZ : forall {i1}, 0 = + i1<-> False.

[...]

rw_aux OJQZ. (*<- This fails *)

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. (*<- This works even though it's just the body of rw_aux *)

Could this be because of the implicit argument of [OJQZ]? The extra context provided by, e.g., the immediate use of [proj1] and [proj2] might be helping type inference work.



Archive powered by MHonArc 2.6.18.

Top of Page