Stream: Coq users

Topic: Can't infer type parameter

Jordan Mitchell Barrett (Mar 31 2021 at 03:48):

Coq beginner here who is hoping for some help. Suppose I have the following Coq program:

Inductive foo : nat -> Type :=
| succ{n:nat} : foo n -> foo n.

Fixpoint bar {n:nat}(A:foo n)(B:foo n) : Prop :=
  match B with
  | succ C => bar A C
  end.

Coq is complaining about the definition of bar:

In environment
bar : forall n : nat, foo n -> foo n -> Prop
n : nat
A : foo n
B : foo n
n0 : nat
C : foo n0
The term "C" has type "foo n0" while it is expected to have type "foo n".

But for B : foo n to be a succ C, C must also be a foo n. Why can't Coq infer this, and how can I fix the definition of bar?

Jasper Hugunin (Mar 31 2021 at 04:48):

What you have with foo is an inductive family indexed by a nat. When you match on such an inductive family, as you do in bar, the unsugared version has some extra annotations; it looks like

match B in foo n1 return Prop with
| succ C => bar A C
end

Jasper Hugunin (Mar 31 2021 at 04:53):

The in foo n1 clause gives a fresh name to the index. Here, we give it the name n1. Then the return clause gives the type of the match, but the trick here is that it can depend on n1. Then on the outside, the match has the type of the return clause with index of the discriminee (here n) substituted in, but on the inside, in each case, you need to provide a term of type of the return clause with the index in the conclusion of the constructor (here n0, where n0 is the implicit nat argument to succ bound invisibly in the | succ C pattern).

Jasper Hugunin (Mar 31 2021 at 04:53):

Since A still has type foo n, while C has type foo n0, you get the error you see.

Jasper Hugunin (Mar 31 2021 at 04:54):

To fix that, you need to pass A through the match, so that you can track the relationship between the indices of A and B/C.

Jasper Hugunin (Mar 31 2021 at 04:55):

You can do that by having the match return a function:

match B in foo n1 return foo n1 -> Prop with
| succ C => fun A => bar A C
end A

Jasper Hugunin (Mar 31 2021 at 04:56):

For more explanation, you should read http://adam.chlipala.net/cpdt/html/MoreDep.html, particularly the section "The One Rule of Dependent Pattern Matching in Coq".

Jasper Hugunin (Mar 31 2021 at 04:57):

Later in that chapter, the above technique is referred to as "the convoy pattern".

Jasper Hugunin (Mar 31 2021 at 04:59):

One last thing: If you are defining an indexed inductive type and all the constructors conclude with a variable in the place of that index, you can instead move the index before the colon. For foo, that looks like

Inductive foo (n : nat) : Type :=
| succ : foo n -> foo n.

Jasper Hugunin (Mar 31 2021 at 05:00):

If you do that, it becomes a parameter, and you no longer need to/are allowed to bind it in an in clause, because the type system knows that it is the same both inside and outside the match.

Jasper Hugunin (Mar 31 2021 at 05:01):

That would make your original definition of bar work without needing to change it.

Jordan Mitchell Barrett (Mar 31 2021 at 06:18):

Thanks! Very helpful, I'll try digest what you wrote and see if I have questions :)

Last updated: Oct 13 2024 at 01:02 UTC