Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Destructing a "nat" into 0, 1, 2, 3, ..., k-1 and ">= k"

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Destructing a "nat" into 0, 1, 2, 3, ..., k-1 and ">= k"


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



Archive powered by MHonArc 2.6.18.

Top of Page