The Coq mailing list

[Jonathan Leivent <jonikelee AT gmail.com>]

On 06/08/2015 11:25 AM, Adam Chlipala wrote:
> If some type has decidable equality, then all proofs of the same 
> equality in that type are provably equal.  See this module from the 
> standard library:
>     https://coq.inria.fr/stdlib/Coq.Logic.Eqdep_dec.html

In other words:

Require Import Peano_dec.

Lemma fobar: eq_refl = mult_n_O 1.
apply UIP_nat.
Qed.


> It is also popular to assert as an axiom that all proofs of some 
> equality are equal, though in general that property is independent of 
> Coq's logical theory, I believe.  If you'd like to import that axiom 
> (not needed for your example, since equality on [nat] is decidable), 
> see here:
>     https://coq.inria.fr/stdlib/Coq.Logic.Eqdep.html
>
> On 06/08/2015 11:21 AM, Lars Rasmusson wrote:
> > Hi,
> >
> > this might be trivial, but how would one prove this lemma?
> >
> >     Lemma fobar: eq_refl = mult_n_O 1.
> >
> > The left side is of type 0 = 0 and the right side is of type 0 = 1 * 0.
> >
> > Is the left side equal to the right side, or only of coercible types?
> >
> > As the type eq only has one constructor, shouldn't that make them the 
> > same?