The Coq mailing list

[Adam Megacz <megacz AT cs.berkeley.edu>]

Damien Pous 
<Damien.Pous AT ens-lyon.fr>
 writes:
> Inductive test : Z -> Set :=
> | up   : forall z, test (z+1) -> test z
> | down : forall z, test (z-1) -> test z.

Thanks Damien, that works in my simplified example, but not in the much
more complicated one that I actually care about -- in that case the
parameter simply cannot be made recursively uniform.


Adam Chlipala 
<adam AT chlipala.net>
 writes:
> It's not clear what else to do instead.  Updating types of
> variables "in place" is undecidable in the general case, since
> higher-order unification reduces to it. 

Yeah, I had a nagging suspicion that modifying the context might somehow
make typechecking undecidable.

> "Adding equalities" could be done in general, but Coq typing right now
> includes no notion of "equalities in the context."

True, this would require granting blessed status to [Coq.Init.Logic.eq].
But so far it's the only workable solution I've seen.

> In your particular example, however you slice it, you seem to be
> expecting Coq to apply the identity [n + 1 - 1 = n] automatically.

Hrm, thanks for taking the time to reply, Adam, but the question was
about the relationship between [z0] and [z], not betwen [z] and [z+1-1]
-- check the third paragraph of my post.

  - a