coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Amin Timany <amintimany AT gmail.com>
- To: coq-club AT inria.fr
- Subject: Re: [Coq-Club] Getting tactics in terms to fire later?
- Date: Wed, 1 Jun 2016 15:36:57 +0200
- Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=amintimany AT gmail.com; spf=Pass smtp.mailfrom=amintimany AT gmail.com; spf=None smtp.helo=postmaster AT mail-wm0-f53.google.com
- Ironport-phdr: 9a23:6NYOWBHEvFHLzOiriWRIxp1GYnF86YWxBRYc798ds5kLTJ75pMmwAkXT6L1XgUPTWs2DsrQf27uQ7v+rBDxIyK3CmU5BWaQEbwUCh8QSkl5oK+++Imq/EsTXaTcnFt9JTl5v8iLzG0FUHMHjew+a+SXqvnYsExnyfTB4Ov7yUtaLyZ/nhqbvpNaOM01hv3mUX/BbFF2OtwLft80b08NJC50a7V/3mEZOYPlc3mhyJFiezF7W78a0+4N/oWwL46pyv50IbaKvdKMhCLdcET4OMmYv5cStuwOQYxGI4y41V2QQ2iZJBgHD/VmuV5LwtDf7s+N7yQGVOMT3SfY/XjH0vPQjcwPhlCpSb21xy2rQkMEl1K8=
Hi,
It seems that the problem here is that Coq is trying to determine the implicit argument (the type of the list) of cons by type checking “it”. So, you can try casting the type of “it” to the desired type as Jonathan suggests or fix the implicit argument of cons.
Definition bar : nat := foo ((it : nat) :: nil).
Definition bar : nat := foo (@cons nat it nil).
I’m not sure whether this is the kind of solution you are looking for or not.
— Amin
On 01 Jun 2016, at 15:24, Jonathan Leivent <jonikelee AT gmail.com> wrote:
On 06/01/2016 01:22 AM, Gregory Malecha wrote:Hello --
I'm wondering if anyone has a trick to get tactics-in-terms to fire later?
Here's a somewhat contrived example:
Definition foo (ls : list nat) : nat := 0.
Ltac try_something :=
lazymatch goal with
| |- nat => exact 0
| |- bool => exact true
end.
Notation "'it'" := ltac:(try_something) (at level 0).
Definition bar : nat := foo (it :: nil).
In the last line, we know that the type of 'it' should be [nat] since [foo]
takes an argument of type [list nat]. However, when the Ltac actually
fires, the goal is a unification variable and therefore neither of branches
of the [lazymatch] matches.
Any hackish tricks to get this to work? Possibly something involving
'Program' or canonical structures?
About tactic-in-term: one can force it to see an instantiated conclusion only by (that I know of) a cast. In other words, if you can do "ltac:(tac):T", then tac will see T instead of an evar as the conclusion. However, I don't see how to use that fact to help you here.
-- Jonathan
- [Coq-Club] Getting tactics in terms to fire later?, Gregory Malecha, 06/01/2016
- RE: [Coq-Club] Getting tactics in terms to fire later?, Soegtrop, Michael, 06/01/2016
- Re: [Coq-Club] Getting tactics in terms to fire later?, Beta Ziliani, 06/01/2016
- RE: [Coq-Club] Getting tactics in terms to fire later?, Soegtrop, Michael, 06/01/2016
- Re: [Coq-Club] Getting tactics in terms to fire later?, Beta Ziliani, 06/01/2016
- Re: [Coq-Club] Getting tactics in terms to fire later?, Jonathan Leivent, 06/01/2016
- Re: [Coq-Club] Getting tactics in terms to fire later?, Amin Timany, 06/01/2016
- Re: [Coq-Club] Getting tactics in terms to fire later?, Matthieu Sozeau, 06/01/2016
- Re: [Coq-Club] Getting tactics in terms to fire later?, Gregory Malecha, 06/01/2016
- Re: [Coq-Club] Getting tactics in terms to fire later?, Matthieu Sozeau, 06/01/2016
- Re: [Coq-Club] Getting tactics in terms to fire later?, Amin Timany, 06/01/2016
- RE: [Coq-Club] Getting tactics in terms to fire later?, Soegtrop, Michael, 06/01/2016
Archive powered by MHonArc 2.6.18.