Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Is eq_refl = mult_n_O 1 provable?

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Is eq_refl = mult_n_O 1 provable?


Chronological Thread 
  • From: Jonathan Leivent <jonikelee AT gmail.com>
  • To: coq-club AT inria.fr
  • Subject: Re: [Coq-Club] Is eq_refl = mult_n_O 1 provable?
  • Date: Mon, 08 Jun 2015 11:38:33 -0400



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?





Archive powered by MHonArc 2.6.18.

Top of Page