The Coq mailing list

[Gyesik Lee <gslee AT ropas.snu.ac.kr>]

Hi,

I have encountered 3 three cases which I could handle with some
reflection, but I think it would be interesting, not just for me, to
know how you would solve them.

Here are the three.

1) For a term construction, assume you have used eq_rect with a proof
H as in the following

eq_rect x P t x H

But if H is not syntactically equal to refl_equal, then simpl tactic
won't convert the term above to t.
Is proof-irrelevance necessary to get the reduction?

2) It's about eq's polymorphism.

Coq complained once that [nat = nat] is different from [nat = nat].
Then using Set Printing All, I found out Coq was right because

@eq Set nat nat and @eq Type nat nat are syntactically different.

However how should I understand this apart from that syntactic inequality?

3) Assume the goal is to show

JMeq t s

and you know t = t'. Is there any tactic which functions like rewrite
for the usual equality?
You could work with JMeq_ind, and there are some explanations in
CoqArt, Section 8.2.7, how to deal with it.
But I am wondering if some tactics have been developed in the meantime.

Thanks for any comments in advance.

Gyesik