The Coq mailing list

[Cedric Auger <sedrikov AT gmail.com>]

2014-05-10 22:29 GMT+02:00 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!

I guess that it is due to the "extended pattern matching inference" (I don’t know how to call that).

What you intended to write was:

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 as N in _ return P N with

         0 => P0 (*Type checks*)

       | 1 => P1 (*Type checks*)

       | (S (S (S n'))) => PSSS n' (f n')  (*Type checks*)

     end.

and what Coq infered:

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 as N in _ return P O with

         0 => P0 (*Type checks*)

       | 1 => P1 (*Type error*)

       | (S (S (S n'))) => PSSS n' (f n')  (*Type error*)

     end.

This is due to the fact that inference of annotations are done by typing branches.

The "0 => P0" branch infers that the type to be inferred is "P O" but in fact, but what you want is in fact "P n" where 'n' is the value to be matched, so it fits for the other branches as well.



--
.../Sedrikov\...