The Coq mailing list

[Jean-Marie Madiot <jmadiot AT CS.Princeton.EDU>]

More precisely (my guess is) that it works when "being equal to the given *element* of the type" is decidable (or more simply, can be done with a finite pattern matching term).

For exemple, equality on streams is not decidable, but we can decide equality to a finite stream.  And the same refine tactic works.  However, try it with an infinite stream, and it fails to help.

CoInductive stream :=

  | nil : stream

  | cons : nat -> stream -> stream.

Lemma test1 :

  forall (T : Type)

    (feq : cons 3 nil = cons 3 nil -> T)

    (H1 : cons 3 nil = cons 3 nil),

    feq eq_refl = feq H1.

Proof.

  intros T feq H.

  refine (match H with eq_refl _ => _ end).

  reflexivity.

Qed.

Lemma test2 :

  forall (T : Type)

    (feq : (cofix x := cons 3 x) = (cofix x := cons 3 x) -> T)

    (H1 : (cofix x := cons 3 x) = (cofix x := cons 3 x)),

    feq eq_refl = feq H1.

Proof.

  intros T feq H.

  Fail progress refine (match H with eq_refl _ => _ end).

Abort.

On Wed, Aug 17, 2016 at 3:55 PM, Jason Gross <jasongross9 AT gmail.com> wrote:

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