The Coq mailing list

[Jonathan Leivent <jonikelee AT gmail.com>]

On 08/17/2016 01:56 PM, Jason Gross wrote:
> 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.

Perhaps - but why can't inference of the return clause do the same for 
other cases that have rather trivial decidable equality?  For instance, 
bool:

Goal forall (b:bool)(H:b=b), H=eq_refl.
intros.
refine (match H with eq_refl => _ end).

The refine doesn't help here.  Why not? (Yes I know the proof exists in 
Eqdep_dec, but that is besides the point).  I've experimenting with UIP 
recently, and find it actually quite surprising that the refine works in 
Michael's goal, considering how it fails to do so in so many other 
similar cases.

Also, why aren't there any tactics (inversion, destruct, or their 
dependent variants) that can be used to solve these goals?

-- Jonathan


> 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