CODEWITHSUNDEEP
listtype-inferencecoqdependent-type
Bakuriu
Bakuriu

Reputation: 101969

Why can't coq infer the that 0+n=n in this dependently typed program?

I'm starting to use Coq and I'd like to define some dependently typed programs. Consider the following:

Inductive natlist : nat -> Type :=
  | natnil : natlist 0
  | natcons : forall k, nat -> natlist k -> natlist (S k).

Fixpoint natappend (n:nat) (l1: natlist n) (m:nat) (l2: natlist m) : natlist (n+m) :=
  match l1 with
    | natnil => l2
    | natcons _ x rest => natcons (n+m) x (natappend rest l2)
  end.

So natlist k would be a list of nats of length k. The problem with the definition of concatenation as natappend is the following error:

Error:
In environment
natappend : forall n : nat,
            natlist n ->
            forall m : nat,
            natlist m -> natlist (n + m)
n : nat
l1 : natlist n
m : nat
l2 : natlist m
The term "l2" has type "natlist m"
while it is expected to have type
 "natlist (?n@{n1:=0} + m)".

As you can see it has a problem with the clause:

| natnil => l2

because it claims that the type of l2 is natlist m while the result type must be natlist (n+m) = natlist (0+m).

I know that Coq cannot resolve arbitrary expressions at the type level to avoid non-terminating computations, but I find strange that even this simple case isn't handled.

I'm running CoqIDE on linux, the version is:

The Coq Proof Assistant, version 8.5 (February 2016)
  compiled on Feb 22 2016 18:19:5 with OCaml 4.02.2

I've seen live classes using the MacOSX version with code similar to the above that compiled in the IDE without that error, so I'm a bit puzzled.

Is there some setting that I have to set to enable more type inference and allow the kind of code as above? Alternatively: how can I write dependently typed code that doesn't rely on type inference?

Upvotes: 2

Views: 497

Answers (2)

Arthur Azevedo De Amorim
Arthur Azevedo De Amorim

Reputation: 23592

The problem is that you had a type error in your second branch. Here is a version that works:

Fixpoint natappend {n m:nat} (l1 : natlist n) (l2 : natlist m) : natlist (n + m) :=
  match l1 with
  | natnil => l2
  | natcons n' x rest => natcons (n' + m) x (natappend rest l2)
  end.

The crucial difference between this version and the original one is the parameter passed to natcons: here, it is n' + m, whereas before it was n + m.

This example illustrates very well a general issue with non-locality of error messages in Coq, in particular when writing dependently typed programs. Even though Coq complained about the first branch, the problem was actually in the second branch. Adding annotations in your match statement, as suggested by @jbapple, can be useful when trying to diagnose what is going wrong.

Upvotes: 6

jbapple
jbapple

Reputation: 3375

You need match ... as ... in ... return ... to do more sophisticated type annotations. See Adam Chlipala's chapter "Library MoreDep" in his Book "Certified Programming with Dependent Types" or "Chapter 17: Extended pattern-matching" in the Coq manual. Both have the concat example you are working on.

You could also just delay the dependent type bit until the end:

Definition natlist n := { x : list nat & n = length x }.

Then prove that non-dependently-typed concat preserves length sums.

Upvotes: 3

Related Questions