The Coq mailing list

[Jonathan Leivent <jonikelee AT gmail.com>]

On 08/17/2016 02:48 PM, ikdc wrote:
> On 08/17/2016 02:08 PM, Jonathan Leivent wrote:
> > ...
> >
> > 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.
> >
> > ...
>
> Your goal isn't analogous:
>
> Goal forall H : true = true, H = eq_refl.
>   intro H.
>   refine (match H with eq_refl => _ end).
>   reflexivity.
> Qed.

So it matters that the equality is between constructors instead of 
variables?  OK - thanks - but that still seems strange.  Although I have 
found other cases recently of similar strange behavior in how Coq infers 
return clauses - those related to injection proofs, which are very similar.

It would be nice to have a tactic that does "refine (match H with ctor1 
_ => _  | ctor2  _ => _ ... end)" for H with arbitrary inductive type - 
as it is extremely difficult (maybe impossible?) for Ltac to build match 
expressions for arbitrary inductive types on its own.

-- Jonathan