The Coq mailing list

[Yves Bertot <Yves.Bertot AT sophia.inria.fr>]

Gyesik Lee wrote:
> 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?
>   
Just for this question, proof irrelevance is only used to prove that H 
is equal to refl_equal x.  So a restricted statement, strong enough for 
this result, may be used to avoid general proof irrelevance.

For instance, for any type t with a decidable equality (teq:forall x 
y:t, {x=y}+{x<>y}), you can prove the
following statement: forall x:t, forall p1 p2: x= x, p1 = p2, and this 
is enough to solve your problem.

Yves