The Coq mailing list

[roconnor AT theorem.ca]

On Thu, 20 Mar 2008, Edsko de Vries wrote:

>  Eval compute in g 0.
>
> we get
>
>     = match

As Adam noted, the problem is that minus_n_n is opaque, and is not 
available for computation.  These sorts of type-casts are a bit of a 
problem in Coq.  I would be inclined to write my own transparent version 
of minus_n_n, but I'm not sure if there are better ideas.

> whereas I'd much rather just get T0! I'm not sure what to do to make it
> give me T0. Also, I'd like to be able to prove the following lemma:
>
>  Lemma l1 : forall n, g n = T0.

We can prove something more general.

Require Import Eqdep_dec.
Lemma l1 : forall x : T 0, T0 = x.
intros n.
change (T0) with (eq_rec 0 T T0 0 (refl_equal 0)).
generalize (refl_equal 0).
revert n.
set (z:=0).
unfold z at 2 5.
generalize z.
clear z.
intros z [] e.
pattern e.
apply (K_dec).
 intros x y.
 destruct (eq_nat_dec x y); auto.
reflexivity.
Qed.

Maybe more clever Coq people know how to make a shorter proof.

--
Russell O'Connor                                      <http://r6.ca/>
``All talk about `theft,''' the general counsel of the American Graphophone
Company wrote, ``is the merest claptrap, for there exists no property in
ideas musical, literary or artistic, except as defined by statute.''