The Coq mailing list

["Chung Kil Hur" <Chung-Kil.Hur AT pps.jussieu.fr>]

Hi Gyesik,

> 
> 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?
> 

You don't need the general proof irrelevance.
You just need a much weaker assumption, the uniqueness of identity 
proof~(UIP), 
or equivalently Streicher's Axiom K, to derive H = refl_equal.
Actually, in Agda, this axiom is internalized (ie, H is convertible to 
refl_equal) and
I heard that it is going to be internalized in a later version of Coq as well.

> 
> 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.
> 

If your question is about rewriting tactics for JMeq, I developed something 
similar.
The library Heq supports rewriting of heterogeneous equality.
You can find it in the following address.
http://www.pps.jussieu.fr/~gil/Heq
But, you should use equality on dependent pairs instead of JMeq, which is 
usually not a big deal.

Cheers,
Chung-Kil Hur