coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Yucheng Zhang <yczhang89 AT gmail.com>
- To: Math Prover <mathprover AT gmail.com>
- Cc: "coq-club AT inria.fr" <coq-club AT inria.fr>
- Subject: Re: [Coq-Club] Destructing a "nat" into 0, 1, 2, 3, ..., k-1 and ">= k"
- Date: Sat, 1 Jun 2013 15:24:34 +0800
On Jun 1, 2013, at 3:12 PM, Math Prover
<mathprover AT gmail.com>
wrote:
> Another stupid question from me:
>
> (1) "magic n 10"
> (2) "magic n (length (1::2::3::4::5::6::7::8::9::10::nil))"
>
> (1) works. (2) somehow does not work. Is there somewhat I can embed a
> simpl/compute/cbv somewhere so that "length (1::2::...::nil))" gets
> simplified to 10 before it hits ltac (or have ltac handle this case as
> well?)
After some digging into the Coq Reference Manual, I found out we can do this:
Ltac magic n k :=
match eval compute in k with
| O => idtac
| S ?k' => destruct n; [ | magic n k' ]
end.
- [Coq-Club] Destructing a "nat" into 0, 1, 2, 3, ..., k-1 and ">= k", Math Prover, 06/01/2013
- [Coq-Club] Re: Destructing a "nat" into 0, 1, 2, 3, ..., k-1 and ">= k", Math Prover, 06/01/2013
- Re: [Coq-Club] Destructing a "nat" into 0, 1, 2, 3, ..., k-1 and ">= k", Yucheng Zhang, 06/01/2013
- Re: [Coq-Club] Destructing a "nat" into 0, 1, 2, 3, ..., k-1 and ">= k", Math Prover, 06/01/2013
- Re: [Coq-Club] Destructing a "nat" into 0, 1, 2, 3, ..., k-1 and ">= k", Pierre Courtieu, 06/03/2013
- Re: [Coq-Club] Destructing a "nat" into 0, 1, 2, 3, ..., k-1 and ">= k", Math Prover, 06/03/2013
- Re: [Coq-Club] Destructing a "nat" into 0, 1, 2, 3, ..., k-1 and ">= k", Math Prover, 06/03/2013
- Re: [Coq-Club] Destructing a "nat" into 0, 1, 2, 3, ..., k-1 and ">= k", Yucheng Zhang, 06/03/2013
- Re: [Coq-Club] Destructing a "nat" into 0, 1, 2, 3, ..., k-1 and ">= k", Math Prover, 06/03/2013
- Re: [Coq-Club] Destructing a "nat" into 0, 1, 2, 3, ..., k-1 and ">= k", Yucheng Zhang, 06/03/2013
- Re: [Coq-Club] Destructing a "nat" into 0, 1, 2, 3, ..., k-1 and ">= k", Pierre Courtieu, 06/03/2013
- Re: [Coq-Club] Destructing a "nat" into 0, 1, 2, 3, ..., k-1 and ">= k", Math Prover, 06/01/2013
- Re: [Coq-Club] Destructing a "nat" into 0, 1, 2, 3, ..., k-1 and ">= k", gallais, 06/03/2013
- Re: [Coq-Club] Destructing a "nat" into 0, 1, 2, 3, ..., k-1 and ">= k", Vincent Demange, 06/03/2013
Archive powered by MHonArc 2.6.18.