Exhaustiveness matching in proof objects for induction in Coq

Question

In Software Foundations, they discuss how to build you own proof objects for induction: https://softwarefoundations.cis.upenn.edu/lf-current/IndPrinciples.html#nat_ind2

Definition nat_ind2 :
  ∀ (P : nat → Prop),
  P 0 →
  P 1 →
  (∀ n : nat, P n → P (S(S n))) →
  ∀ 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.

I experimented with this definition by commenting out "| 1 ⇒ P1". Coq then gives an error: "Non exhaustive pattern-matching: no clause found for pattern 1." I was expecting an error, of course. But I don't know how Coq figures out there is an error.

I would like to know how Coq does the exhaustiveness matching to know that 1 needs to be checked, since 1 isn't part of the constructor for nat. Roughly what algorithm is Coq following?

Answer 1

I'm not sure it answers fully your question, but you may look at the way "extended" matching are dealt with (see for instance https://coq.inria.fr/distrib/current/refman/language/extensions/match.html#mult-match ).

Let's look at a simple example.

Definition f (n: nat): nat :=
match n with 
  2 => 2
| 1 => 23
| _ => S n
end.

With the following command, I can see how f is expressed through simple pattern matchings.

Unset Printing Matching. 

Print  f. 
(*
f = 
fun n : nat =>
  match n with
  | 0 => S n
  | S n0 =>
    match n0 with
    | 0 => 23
    | S n1 => match n1 with
              | 0 => 2
              | S _ => S n
              end
    end
end
     : nat -> nat
*)

If you remove the clause for 1 from your example, it seems impossible to convert your match into nested simple 0 | S _ matchings `.