The Coq mailing list

[roconnor AT theorem.ca]

On Thu, 20 Mar 2008, Adam Chlipala wrote:

> Here's how I would do it, without using any of the tactics I've developed 
> over the years for simplifying this sort of thing:
>
> Require Import Eqdep.
>
> Inductive T : nat -> Set := T0 : T 0.
>
> Notation "e :? pf" := (eq_rect _ (fun X : Set => X) e _ pf)
> (no associativity, at level 90).
>
> Lemma l1' : forall n (x : T n) Heq, T0 = (x :? Heq).
> destruct x; intro Heq; rewrite (UIP_refl _ _ Heq); reflexivity.
> Qed.
>
> Lemma l1 : forall x : T 0, T0 = x.
> intros; change x with (x :? refl_equal _); apply l1'.
> Qed.

Other than relying on an axiom introduced by Eqdep, this is nice.  I'm 
sure it could be adjusted to only use Eqdep_dec.

--
Russell O'Connor                                      <http://r6.ca/>
``All talk about `theft,''' the general counsel of the American Graphophone
Company wrote, ``is the merest claptrap, for there exists no property in
ideas musical, literary or artistic, except as defined by statute.''