coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Edsko de Vries <devriese AT cs.tcd.ie>
- To: coq-club AT pauillac.inria.fr
- Subject: [Coq-Club] Heterogeneous equality?
- Date: Thu, 20 Mar 2008 17:00:16 +0000
- List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>
Hi,
I am stuck in a definition, and I think it's got something to do with
heterogeneous equality. Here is a simplified version of the problem.
Suppose we have some dependent data type:
Require Import Arith.
Section test.
Inductive T : nat -> Set :=
T0 : T 0.
Now we define the following two functions f and g. Both these functions
return element T0 (so they return the same term), but with a different
type.
Definition f (n : nat) : T (n - n).
intro n.
rewrite <- minus_n_n.
exact T0.
Defined.
Definition g (n : nat) : T 0.
intro n.
rewrite (minus_n_n n).
exact (f n).
Defined.
If we now do
Eval compute in g 0.
we get
= match
match minus_n_n 0 in (_ = y) return (y = 0) with
| refl_equal => refl_equal 0
end in (_ = y) return (T y)
with
| refl_equal =>
match minus_n_n 0 in (_ = y) return (T y) with
| refl_equal => T0
end
end
: T 0
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.
but I'm not sure to prove that, either. Proving just this lemma without
being able to do the 'Eval compute' thing would be unfortunate. In the
real development, the actual datatype and function definitions are
obviously much more interesting and being able to do 'Eval compute' to
figure out what the functions return would be very useful.
Any help would be appreciated!
Thanks,
Edsko
- [Coq-Club] Heterogeneous equality?, Edsko de Vries
- Re: [Coq-Club] Heterogeneous equality?, Adam Chlipala
- Re: [Coq-Club] Heterogeneous equality?,
roconnor
- Re: [Coq-Club] Heterogeneous equality?,
Adam Chlipala
- Re: [Coq-Club] Heterogeneous equality?, roconnor
- Re: [Coq-Club] Heterogeneous equality?, Edsko de Vries
- Re: [Coq-Club] Heterogeneous equality?,
Adam Chlipala
Archive powered by MhonArc 2.6.16.