The Coq mailing list

[Kristopher Micinski <krismicinski AT gmail.com>]

You will discharge this with an 'as' inside the match. Adam has a chapter on dependent matching in the CPDT book:

http://adam.chlipala.net/cpdt/html/MoreDep.html

Kris

On Dec 29, 2012 2:38 PM, <abc.deaf.xyz AT gmail.com> wrote:

I am trying to develop a programming style that is based on preventing bad
input as soon as possible. For example, instead of the following plausible
definition for the predecessor function on the natural numbers:

    Definition pred1 n :=
      match n with
        | O   => None
        | S n => Some n
      end.

I want to write it as follows:

    Theorem nope n (p : n = O) (q : n <> O) : False.
      contradict q.
      exact p.
    Qed.

    Definition pred2 n (q : n <> O) :=
      match n with
        | S n => n
        | O   =>
          let p := _ in
          match nope n p q with end
      end.

My problem is... what do I fill in the hole in the let clause? My intuition
suggests me that every clause of a `match` block must introduce an assumption
that the matched _expression_ (in this case, `n`) is equal to the clause's data
constructor (in this case, `O`). In short, there must be some `assumption : n
= O`. Does Coq indeed introduce such an assumption? If so, what is its name?