coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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.
- [Coq-Club] Beginner problem writing tactic, rpgcbaptista, 08/02/2013
- Re: [Coq-Club] Beginner problem writing tactic, Adam Chlipala, 08/02/2013
- Re: [Coq-Club] Beginner problem writing tactic, Rui Baptista, 08/02/2013
- Re: [Coq-Club] Beginner problem writing tactic, Adam Chlipala, 08/02/2013
- Re: [Coq-Club] Beginner problem writing tactic, Rui Baptista, 08/02/2013
- Re: [Coq-Club] Beginner problem writing tactic, Adam Chlipala, 08/02/2013
Archive powered by MHonArc 2.6.18.