coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Jonathan Leivent <jonikelee AT gmail.com>
- To: coq-club AT inria.fr
- Subject: Re: [Coq-Club] Question about tacargs
- Date: Sun, 3 Apr 2016 17:29:57 -0400
- Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=jonikelee AT gmail.com; spf=Pass smtp.mailfrom=jonikelee AT gmail.com; spf=None smtp.helo=postmaster AT mail-qg0-f54.google.com
- Ironport-phdr: 9a23:a6pdERVwFKfCyM0r3BAPXyng643V8LGtZVwlr6E/grcLSJyIuqrYZheOt8tkgFKBZ4jH8fUM07OQ6PCwHzdeqs7Y+Fk5M7VyFDY9wf0MmAIhBMPXQWbaF9XNKxIAIcJZSVV+9Gu6O0UGUOz3ZlnVv2HgpWVKQka3CwN5K6zPF5LIiIzvjqbpq82VOFsD3GP1SIgxBSv1hD2ZjtMRj4pmJ/R54TryiVwMRd5rw3h1L0mYhRf265T41pdi9yNNp6BprJYYAu2pN5g/GLdfFXEtN30/zMztrxjKCwWVtVUGVWBDsB1OChTF5ReyeprwrCb8qqIp2i6cPM77Sb05cTun5qZvDhTvjXFUZHYC7GjLh5ko3+pgqxW7qkknzg==
On 04/03/2016 05:17 PM, scott constable wrote:
In the following, why does attempt1 succeed, whereas attempt2 fails? I
followed
through with the Ltac debugger, and found that extractor' is never executed
after intros, but I cannot come up with an explanation as to why.
Try rewriting exactor' as:
Ltac exactor' := idtac;
match goal with
| [ H : ?P |- ?P ] => exact H
| _ => idtac
end.
What's happening with the original exactor' is that because it's body a raw match tactical, it can be evaluated in the arg position of my_solve prior to calling my_solve - and it evaluates to the tactic idtac there (because the intros haven't happened yet). In exactor, the try tactical prevents this early evaluation. In the above rewrite of exactor', the sequence tactical ";" prevents the early evaluation.
-- Jonathan
Ltac my_solve m :=
intros; m.
Ltac exactor := try
match goal with
| [ H : ?P |- ?P ] => exact H
end.
Ltac exactor' :=
match goal with
| [ H : ?P |- ?P ] => exact H
| _ => idtac
end.
Theorem attempt1 : forall (A : Type) (x y : A),
x = y -> x = y.
Proof. my_solve exactor. Qed.
Theorem attempt2 : forall (A : Type) (x y : A),
x = y -> x = y.
Proof. my_solve exactor'. Qed.
Thanks in advance,
~Scott Constable
- [Coq-Club] Question about tacargs, scott constable, 04/03/2016
- Re: [Coq-Club] Question about tacargs, Jonathan Leivent, 04/03/2016
- Re: [Coq-Club] Question about tacargs, scott constable, 04/04/2016
- Re: [Coq-Club] Question about tacargs, Jonathan Leivent, 04/04/2016
- Re: [Coq-Club] Question about tacargs, scott constable, 04/04/2016
- Re: [Coq-Club] Question about tacargs, Jonathan Leivent, 04/03/2016
Archive powered by MHonArc 2.6.18.