Abstracting over the term ... leads to a term ... which is ill-typed

Question

Here is what I am trying to prove:

  A : Type
  i : nat
  index_f : nat → nat
  n : nat
  ip : n < i
  partial_index_f : nat → option nat
  L : partial_index_f (index_f n) ≡ Some n
  V : ∀ i0 : nat, i0 < i → option A
  l : ∀ z : nat, partial_index_f (index_f n) ≡ Some z → z < i
  ============================
   V n ip
   ≡ match
       partial_index_f (index_f n) as fn
       return (partial_index_f (index_f n) ≡ fn → option A)
     with
     | Some z => λ p : partial_index_f (index_f n) ≡ Some z, V z (l z p)
     | None => λ _ : partial_index_f (index_f n) ≡ None, None
     end eq_refl

The obvious next step is either rewrite L or destruct (partial_index_f (index_f n). Trying to applying rewrite gives me an error:

Error: Abstracting over the term "partial_index_f (index_f n)"
leads to a term
"λ o : option nat,
 V n ip
 ≡ match o as fn return (o ≡ fn → option A) with
   | Some z => λ p : o ≡ Some z, V z (l z p)
   | None => λ _ : o ≡ None, None
   end eq_refl" which is ill-typed.

I do not understand what is causing this problem. I also would like to understand how I can deal with it in general.

I was able to prove it using the following steps, but I am not sure this is the best way:

  destruct (partial_index_f (index_f n)).
  inversion L.
  generalize (l n0 eq_refl).
  intros. subst n0.
  replace l0 with ip by apply proof_irrelevance.
  reflexivity.
  congruence.

Answer 1

In Coq's theory, when you perform a rewrite with an equation, you have to generalize over the side of the equation that you want to replace. In your case, you want to replace partial_index_f (index_f n), so Coq tries to generalize that, as you can tell from the error message you got.

Now, if your goal contains something whose type mentions the thing that you want to replace, you might run into trouble, because this generalization might make the goal become ill-typed. (Notice that that type does not exactly occur in the goal, hence Coq does not try to deal with it like it does when something occurs in the goal.) Going back to your case, your l function has type ∀ z : nat, partial_index_f (index_f n) ≡ Some z → z < i, which mentions partial_index_f (index_f n), the term you want to replace. In the first branch of your match, you apply this function to the o = Some z hypothesis that you abstracted over. On the original goal, o was the thing you wanted to replace, but when Coq tries to generalize, the two do not match anymore, hence the error message.

I can't try to fix the problem on my own, but you can solve issues like this usually by generalizing over the term in your context that mentions the term you are replacing, because then its type will show in the goal, associated to a universally quantified variable. This might not help if your term is defined globally and you need it to have a certain shape after the rewrite in order to be able to perform additional reasoning steps, in which case you will probably have to generalize over the lemmas that you need as well.