The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

It only works if the type has decidable equality.  list nat has decidable equality.   It is also decidable whether or not a list of any type is nil, or not.  If you instead try (feq : Set::nil = Set::nil -> T), you will find that it does not work.  If you try (feq : Set = Set -> T) it will not work.  If you try (feq : list nat = list nat -> T), it will not work.  If you try (feq : S = S -> T) it will not work.  If you try (feq : eq_refl 0 = eq_refl 0 -> T), it may or may not work (this still has decidable equality, but it is more complicated).

On Wed, Aug 17, 2016 at 12:04 PM Soegtrop, Michael <michael.soegtrop AT intel.com> wrote:

Dear Jason, Jonathan,

thanks for the solution and explanation.

I experimented a bit. I think that this works for any literal term of any type, even if it doesn't have decidable equality. E.g.:

Open Scope list_scope.

Lemma TestNatList: forall (T : Type) (feq : 3::nil=3::nil->T) (H1 : 3::nil=3::nil), feq eq_refl = feq H1.
Proof.
  intros.
  refine (match H1 with
          | eq_refl _ => _
          end).
  reflexivity.
Qed.

The resulting proof term is lengthy. I guess the decidable equality is required if the value compared is not a literal, but a parameter.

Best regards,

Michael
Intel Deutschland GmbH
Registered Address: Am Campeon 10-12, 85579 Neubiberg, Germany
Tel: +49 89 99 8853-0, www.intel.de
Managing Directors: Christin Eisenschmid, Christian Lamprechter
Chairperson of the Supervisory Board: Nicole Lau
Registered Office: Munich
Commercial Register: Amtsgericht Muenchen HRB 186928