The Coq mailing list

[Adam Chlipala <adam AT chlipala.net>]

Petter Urkedal wrote:
> I want to write a function on a constrained pair type, i.e.
> embedding two data components with a fact about the two.  The actual
> problem is a bit involved, but I think the essence is captured by an
> ordered nat-pair type,
>
>      Inductive ordnatpair : Set :=
>         ordnatpair_intro : forall n m : nat, n<= m ->  ordnatpair.
>
> The function will utilize the hypothesis to prove facts which will
> be embedded in the result.  Since it's easiest to do the logic part
> in Ltac, I use refine:
>
>      Definition test : ordnatpair ->  nat.
>      Proof.
>        intro p.
>        refine match p with
>         | ordnatpair_intro 0 m H =>  _
>         | ordnatpair_intro (S n') m H =>  _
>        end.
>
> But, the equations from the match-cases are not made present when
> proving the goals corresponding to the two holes
>    

This is easy to solve using what I call the convoy pattern in CPDT 
(http://adam.chlipala.net/cpdt/):

Definition test : ordnatpair -> nat.
  refine (fun p => match p with
                 | ordnatpair_intro n m H =>
                       match n return n <= m -> nat with
                         | O => fun H => _
                         | S n' => fun H => _
                       end H
                   end).

If you're getting into the Coq dependent types business, it's probably 
worth reading more of the book.