The Coq mailing list

[Jonathan <jonikelee AT gmail.com>]

On 07/06/2014 02:22 PM, Ömer Sinan Ağacan wrote:

Hi all,

I'm reading CPDT(Certified Programming with Dependent Types) and I'm
typing all the code in the book and following through proofs. I don't
like the book's approach of using magical and non-standard proof
tactics so I'm manually proving parts that are proved using `crush`
and similar tactics.

I did something similar: I used crush first.  After that worked, I'd examine the Ltac code for crush (and its related tactics in Tactics.v, I believe), and see if I could work out how it did what it did.  That way I learned both how to use magical tactics and how to write magical tactics.

It worked mostly fine since I already had basics grasped thanks to
SF(Software Foundations) but now I'm stuck with "dependent destruct"
parts, which I see for the first time.

I pasted the code here http://lpaste.net/107016 .

I am getting errors trying your code.  I had to add "Require Import Arith." - but I still get an error:

Toplevel input, characters 82-83:
Error:
In environment
expDenote : forall t : type, exp t -> typeDenote t
t : type
e : exp t
n : nat
The term "n" has type "nat" while it is expected to have type
 "typeDenote ?9".

The error occurs on what is line 28 in what you posted.  Did you leave out some code from what you posted?

-- Jonathan