The Coq mailing list

[Jonathan Leivent <jonikelee AT gmail.com>]

When destructing an instance of a type with indexes, destruct will often 
rewrite occurrences of terms that are index args elsewhere in the goal.  
But which occurrences and when?  The rules appear to be ad-hoc.  For 
instance:


Inductive Foo (n : nat) : nat -> Type := foo1 : Foo n 1.

Variable P : forall A (a:A), Prop.

Variable G : nat -> Type.

Goal forall n (f : Foo 42 (S n)), G (S n) -> P _ f.
intros n f g.
destruct f. (*g becomes g : G 1*)
Abort.

Goal forall n (f : Foo (S n) (S n)), G (S n) -> P _ f.
intros n f g.
destruct f. (*g stays g : G (S n)*)
Abort.


Why is the treatment of g's type by the two destructs above different?  
Is it just because the term (S n) appears as a parameter and an index to 
Foo in the second goal, but only as an index in the first?  But, what 
justifies this behavior?  Also, what justifies not changing the (S n) 
parameter of f's type in the second goal?

A possibly related question - if one replaces destruct in the above two 
goals with dependent simple inversion, this works in the first goal but 
fails in the second with a cryptic error message:

Error: In environment
n : nat
f : Foo (S n) (S n)
X : G (S n)
n0 : nat
Unable to unify "Foo n0 n0" with "Foo ?M190 n0".

Why can't it do that unification in that environment?

This is all using 8.5pl2.


-- Jonathan