The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

Note that [refine] is doing a lot of inference for you here.  The resulting proof term is:

match

  H1 as H2 in (_ = c)

  return

    (match c as x return (Eq = x -> Type) with

     | Eq => fun h : Eq = Eq => feq eq_refl = feq h

     | Lt => fun _ : Eq = Lt => IDProp

     | Gt => fun _ : Eq = Gt => IDProp

     end H2)

with

| eq_refl => eq_refl

end

The reason that this works is that [comparison] has decidable equality, and, as shown by UIP_dec, any type with decidable equality satisfies uniqueness of identity proofs (i.e., proof irrelevance for [eq]).  This return clause is basically an inlining and simplification of the composition of the decidable equality of [comparison] with the proof that decidable equality implies UIP.

On Wed, Aug 17, 2016 at 9:23 AM John Wiegley <johnw AT newartisans.com> wrote:

>>>>> "SM" == Soegtrop, Michael <michael.soegtrop AT intel.com> writes:

SM> I am stuck with a proof that two proofs of equality are equal:

SM> Goal forall (T : Type) (feq : Eq=Eq->T) (H1 : Eq=Eq), feq eq_refl = feq
SM> H1. intros.

SM> As far as I know "@eq_refl comparison Eq" is the only possible proof of
SM> Eq=Eq, so shouldn't all proofs of Eq=Eq be equal to "@eq_refl comparison
SM> Eq" ? Is there a way to prove this?

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

--
John Wiegley                  GPG fingerprint = 4710 CF98 AF9B 327B B80F
http://newartisans.com                          60E1 46C4 BD1A 7AC1 4BA2