Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Question about tacargs

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Question about tacargs


Chronological Thread 
  • 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




Archive powered by MHonArc 2.6.18.

Top of Page