The Coq mailing list

[Adam Chlipala <adamc AT csail.mit.edu>]

Erik Ernst wrote:
> note that the typing dilemma that I just described can be avoided by not 
> including P in the pattern match (so we would have 'match N1,N2 return..' 
> rather than 'match N1,N2,P return', with corresponding changes in each 
> branch), but this means that P will not have a type which reflects the extra 
> knowledge about N1 and N2 that we gain by being in a specific branch of the 
> match (so we always have 'P: R N1 N2' where otherwise we get 'P: R natO natO' 
> in the first branch and so on), and that is quite important in the original 
> context.
>    

In fact, the first solution I find is exactly what you say won't work. ;)

For more information on this technique, see discussion of "the convoy 
pattern" in CPDT (http://adam.chlipala.net/cpdt/).


Definition F: forall (N1 N2: Nat) (P: R N1 N2), Nat_lt N1 N2 :=
  fun (N1 N2: Nat) =>
    match N1,N2 return R N1 N2 -> Nat_lt N1 N2 with
      | natO     , natO     => fun _ => magic natO natO
      | natO     , natS N2' => fun _ => magic natO (natS N2')
      | natS N1' , natO     => fun _ => magic (natS N1') natO
      | natS N1' , natS N2' => fun P =>
        let Hyp' := Hyp (eq_magic (natS N1') N1) (eq_magic (natS N2') 
N2) in

          let P' := Hyp'
            (cast P (eq_magic N1 (natS N1')) (eq_magic N2 (natS N2')))
          in

            magic (natS N1') (natS N2')
    end.