The type checker's behavior while pattern matching in Coq

Question

I'm trying to examine how the type checker works on the following function, but can't understand how the type checker works in the second (the nested) match clause:

Definition plus_O_2 := 
(fix F (m : mynat) : m == plus m O :=
    match m as m0 with
      | O as m2 => myeq_refl O : m2 == plus m2 O
      | S x as m2 => ((match F x in (m0 == m1) return (S m0 == S m1) with
                        | myeq_refl x0 => myeq_refl (S x0)
                      end) : m2 == plus m2 O)
    end) : forall n : mynat, n == plus n O.

This is a function that provides proof that forall n : mynat, n == plus n O, where mynat, ==, plus are self-defined natural numbers, equality, and addition:

Inductive mynat :=
| O
| S (x:mynat).

Fixpoint plus (a b:mynat) :=
match a with
| O => b
| S n => S (plus n b)
end.

Inductive myeq {X:Type} : X -> X -> Prop :=
| myeq_refl : forall x, myeq x x.

Notation "x == y" := (myeq x y)
                       (at level 70, no associativity)
                     : type_scope.

(The definition for myeq and the corresponding Notation statement was referenced from Software Foundations Vol.1, https://softwarefoundations.cis.upenn.edu/lf-current/ProofObjects.html).

What I'm trying to understand is how Coq manages to type check this function. Here's what I understand of now:

F first receives m. It is expected to return a value of type m == plus m O (The proposition we want to show).
m passes through pattern matching.
- If m is O (meant to represent zero), it returns myeq_refl O.
  - myeq_refl O has type O == O. Meanwhile, from F's definition, it is expected to have type O == plus O O. (My guess is that,) Coq compares these types while type checking, and notices that plus O O is equivalent to O by its definition, so it passes the type check.
- If m is of form S x, a second pattern matching starts running.
  - F x will have the form x == plus x O. This structure is captured in the in clause, and the return clause specifies that the returning type will be S x == S (plus x O).
  - (I don't understand what happens here)
Since both patterns end up with the type m == plus m O, the function has the type forall n : mynat, n == plus n O.

Now, my questions are, what exactly happens with the type checker in where I wrote "I don't understand what happens here?" Particularly,

In my understanding, as the in clause specifies, F x is expected to have the type m0 == m1. Meanwhile, the matching clause myeq_refl x0 seems to have the type x0 == x0, where both sides are equal. Why does Coq's type checker match these two seemingly different types?
After the match (after =>), the match clause outputs myeq_refl (S x0), which should have type S x0 == S x0. Meanwhile, the return clause stipulates that the returning type should be S m0 == S m1, which in my understanding should be equivalent to S x == S (plus x O). These types, at first glance, seem different. How does Coq find out that these types are in fact equivalent?
- Particularly, the second type seems to have a more complicated structure than the original proposition we want to show, n == plus n O, which should mean that Coq should not immediately be able to find that this is in fact equivalent to n == n.

kyo dralliam kyo dralliam · Accepted Answer · 2021-05-21T11:16:37

The occurences of m0 and m1 inside the clause in m0 == m1 are actually binding occurences of the variables for the pattern matching construct (in particular for the return clause). Your code is actually the same as

Definition plus_O_2 := 
(fix F (m : mynat) : m == plus m O :=
    match m as m0 with
      | O as m2 => myeq_refl O : m2 == plus m2 O
      | S x as m2 => ((match F x in (p == q) return (S p == S q) with
                        | myeq_refl x0 => myeq_refl (S x0)
                      end) : m2 == plus m2 O)
    end) : forall n : mynat, n == plus n O.

where I renamed the name of the variables in the inner match.

Now the constructor myeq_refl x is by construction of type x == x which should also be p == q so in that branch, it is enough to build a term of type (S p == S q)[x/p, x/q] (where brackets denote substitution), that is of type S x == S x. Since myeq_refl is the only constructor of this inductive type, you are done with this match once you have provided such a witness.

The type checker's behavior while pattern matching in Coq

1 Answers