The Coq mailing list

[Jonathan Leivent <jonikelee AT gmail.com>]

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.

-- Jonathan