The Coq mailing list

[Jack Kolb <kolb0128 AT umn.edu>]

Hi,

I am working though Software Foundations and have a question on a topic included in the "MoreInd" chapter. The text discusses the idea of defining and using alternate means of induction over certain types. For example, it gives the following definition that can be used to perform induction over natural numbers:

Definition nat_ind2: forall (P : nat -> Prop),

  P 0 -> P 1 ->

  (forall n : nat, P n -> P (S (S n))) ->

  forall n : nat, P n :=

    fun P => fun P0 => fun P1 => fun PSS =>

      fix f (n:nat) := match n with

         0 => P0

       | 1 => P1

       | (S (S n')) => PSS n' (f n')

     end.

Just for fun, I experimented with this definition a bit. Coq will accept the following similar definition.

Definition nat_ind3: forall (P : nat -> Prop),

  P 0 -> P 1 -> P 2 ->

  (forall n : nat, P n -> P (S (S (S n)))) ->

  forall n : nat, P n :=

    fun P => fun P0 => fun P1 => fun P2 => fun PSSS =>

      fix f (n:nat) := match n with

         0 => P0

       | 1 => P1

       | 2 => P2

       | (S (S (S n'))) => PSSS n' (f n')

     end.

In both cases, Coq is able to determine that the function f is total, i.e. that the provided clauses cover all possible inputs. Things get interesting when I intentionally omit a clause, like so:

Definition nat_ind2: forall (P : nat -> Prop),

  P 0 -> P 1 ->

  (forall n : nat, P n -> P (S (S n))) ->

  forall n : nat, P n :=

    fun P => fun P0 => fun P1 => fun PSS =>

      fix f (n:nat) := match n with

         0 => P0

       | (S (S n')) => PSS n' (f n')

     end.

In this case, I get the helpful error message: "Non exhaustive pattern-matching: no clause found for pattern 1." However, something strange happens when I make a similar mistake in the second of the two definitions given above:

Definition nat_ind3: forall (P : nat -> Prop),

  P 0 -> P 1 -> P 2 ->

  (forall n : nat, P n -> P (S (S (S n)))) ->

  forall n : nat, P n :=

    fun P => fun P0 => fun P1 => fun P2 => fun PSSS =>

      fix f (n:nat) := match n with

         0 => P0

       | 1 => P1

       | (S (S (S n'))) => PSSS n' (f n')

     end.

In this case, I get the following error message:

In environment

P : nat -> Prop

P0 : P 0

P1 : P 1

P2 : P 2

PSSS : forall n : nat, P n -> P (S (S (S n)))

f : nat -> P 0

n : nat

n0 : nat

The term "P1" has type "P 1" while it is expected to have type "P 0".

It seems Coq has conjectured that f has the type nat -> P 0, which seems very strange. I am very curious about why this occurs. Could someone perhaps explain what is going on internally when Coq attempts to check for exhaustive pattern matching, and why this situation in particular causes this kind of problem?

Thanks!