The Coq mailing list

[Matthieu Sozeau <matthieu.sozeau AT gmail.com>]

On 29 déc. 2012, at 20:37, 
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?

As explained by others, Coq does not provide you with such an equality 
primitively,
but there is a standard construction to get it, which is implemented by the 
Program
extension (http://coq.inria.fr/distrib/V8.4/refman/Reference-Manual028.html).
Using it you can write:

Require Import Program. 

Program Definition pred2 n (q : n <> O) :=
  match n with
    | S n => n
    | O   => !
  end.

The "!" notation is an abbreviations of False_rec. This program generates a 
single
obligation to show [n (q : n <> 0) (Heq_n : n = 0) |- False], which is 
automatically
discharged. Note that the code of [pred2] is decorated to pass this proof of 
equality
around:

<<
pred2 = fun (n : nat) (q : n = 0 -> False) =>
       match n as n0 return (n0 = n -> nat) with
       | 0 =>
           fun Heq_n : 0 = n =>
           match
             match Heq_n in (_ = y) return ((y = 0 -> False) -> False) with
             | eq_refl =>
                 fun q0 : 0 = 0 -> False =>
                 match q0 eq_refl return False with
                 end
             end q return nat
           with
           end
       | S n0 => fun _ : S n0 = n => n0
       end eq_refl
>>

Hope this helps,
-- Matthieu