The Coq mailing list

[Adam Chlipala <adamc AT hcoop.net>]

Gyesik Lee wrote:
> in case of representing the semantics of a language, it is sometimes
> necessary to have the uniqueness of the term constructions. But since
> terms are usually of dependent types, it is not so simple to prove the
> uniqueness because of heterogeneous equality or dependency.
>
> Here is one simple example.
>
> Inductive P : nat -> bool -> Set :=
>  T : forall n, P n true.
>
> Goal forall (n : nat) (x : P n true), x = T n.
>
> (* one would try *)
> intros n x.
> destruct x.
>
> But the tactic destruct fails with the warning (using Coq 8.2beta3)
>
> Error: Abstracting over the terms "n", "b" and "x" leads to a term
> "fun (n : nat) (b : bool) (x : P n b) => x = T n" which is ill-typed.
>
> Maybe one has to use first the tactic of the following form
>
> pattern n at nums, true at nums , x at nums
>
> to get a well-typed application term, and then use "destruct". But I
> don't understand exactly the process.
>   

[destruct] is only going to work well when _all_ of the arguments of the 
type family you're destructing are variables.  You might also have to 
run [change] on some of the variables to get their types to match those 
in the definition of the type family.  These restrictions arise from the 
CIC typing rule for [match], which is the building block for [destruct].

I think that the general problem you're pointing out could be used to 
solve the higher-order unification problem, so we know it must be 
undecidable.  Tactics like [dependent inversion] make heuristic attempts 
at solving it in limited cases.

It's hard to give a short description of how to solve this problem in 
practice.  The best I can do is show how to solve your specific example 
using [JMeq].  (Keep in mind that this involves introducing an axiom, as 
seen in the manual page for the [JMeq] module.)

Require Import JMeq.

Inductive P : nat -> bool -> Set :=
 T : forall n, P n true.

Lemma p' : forall (n : nat) (b : bool) (x : P n b), b = true -> JMeq x 
(T n).
 destruct x; trivial.
Qed.

Theorem p : forall (n : nat) (x : P n true), x = T n.
 Hint Resolve JMeq_eq p'.
 auto.
Qed.