The Coq mailing list

[Jonathan Leivent <jonikelee AT gmail.com>]

On 08/28/2016 01:38 PM, Jonathan Leivent wrote:
> I have the following proof of a lemma that derives UIP_refl of a 
> simple inductive (Foo) from UIP_refl of its only field (A):
>
> Variable A : Type.
> Hypothesis A_UIP_refl : forall (a : A)(e : a=a), e=eq_refl.
>
> Inductive Foo := foo (a:A).
> Definition foo_a (f : Foo) := let '(foo a) := f in a.
>
> Lemma Foo_UIP_refl : forall (f : Foo)(e: f=f), e=eq_refl.
> Proof.
>   intros f e.
>   destruct f.
>   change eq_refl with (f_equal foo (eq_refl a)).
>   rewrite <- (A_UIP_refl a (f_equal foo_a e)).
>   change (match foo a as b return foo a = b -> Prop with
>           | foo _ => fun x => x = f_equal foo (f_equal foo_a x)
>           end e).
>   case e.
>   reflexivity.
> Qed.
>
> [The proof is based on those at the end of Coq.Logic.Eqdep_dec.]
>
> The question is - can one prove this lemma without using that "change 
> (match ...)" tactic, or any other that requires a Gallina match that 
> embeds a foo constructor pattern ("foo _" here)? Because there is no 
> way to create a Gallina match pattern in Ltac for an arbitrary 
> inductive type, hence the above proof can't be automated via Ltac for 
> other single-constructor-single-field types.  Also, there doesn't seem 
> to be any irrefutable-pattern let-in with return clause that can be 
> used in place of the match for single field constructors and that 
> doesn't use a foo constructor pattern.

Oops - sorry - I did find an irrefutable-pattern let-in that works 
without a constructor pattern (hence for any single constructor):

  change ((let (_) as b return foo a = b -> Prop := foo a in
           fun x => x = f_equal foo (f_equal foo_a x)) e).

Sometimes, those irrefutable let-ins want the := in between the as and 
return clauses, sometimes after.  Confusing.

OK - now the difficulty becomes how to automate this for constructors 
with arbitrary numbers of fields...

-- Jonathan