The Coq mailing list

[Beta Ziliani <beta AT mpi-sws.org>]

I attempt to give an explanation, without actually testing the code.
A pattern matching of the form

match n with
| 0 => f 0
| 1 => g 1
| S (S n') => h (S (S n'))
end

can be thought of as (and I think is translated to)

match n with
| 0 => f 0
| S n' => match n' with
             | 1 => g 1
             | S n''  => h (S (S n''))
             end
end


What I guess is happening in your second case is that there is not
enough typing information to guess what the type of the third match
should be. You can try see what happens if you do the decomposition by
hand.

Hope it helps.
B


On Sat, May 10, 2014 at 10:29 PM, Jack Kolb 
<kolb0128 AT umn.edu>
 wrote:
> 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!