The Coq mailing list

["Gyesik Lee" <gyesik.lee AT aist.go.jp>]

Hello,

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.

Could you explain a more general approach to such problems? Or are
there different and simpler solutions?