The Coq mailing list

[Jonas Oberhauser <s9joober AT gmail.com>]

Hi all,

apparently I don't know how matches work. I looked at the typing rules in Chapter 4 of the manual, but didn't really understand them. Let me give you an example to describe my lack of understanding.

I want to prove the following simple Goal:

Goal forall P : _ -> _ -> Prop, (P 0 0) -> (forall k n, (forall m, P k m) -> P (S k) n) -> (forall k n, P k n -> P k (S n)) -> forall k n, P k n.
intros P base stepl stepr.

Now my first attempt was to prove it as follows:

exact (fix l k := fix r n := match k as k, n as n return P k n with
                             | 0, 0 => base
                             | _, S n => stepr k n (r n)
                             | S k, _ => stepl k n (l k)
                             end).

However, r has type forall n, P k n - and not forall n, P 0 n; even though at that point in the match we know that k is 0.

My second attempt works, by deferring the "definition" of r until in the match:

exact (fix l k := match k as k return forall n, P k n with
                             | 0 => fix r n := match n as n return P 0 n with
                                               | 0 => base
                                               | S n => stepr 0 n (r n)
                                               end
                             | S k => fun n => stepl k n (l k)
                             end).

Here, r has type forall n, P 0 n as k is 0. Why does Coq "forget" that k is 0 in my first attempt?

Kind regards, Jonas