The Coq mailing list

[Erik Ernst <eernst AT cs.au.dk>]

Den 22/09/2011 kl. 13.45 skrev Adam Chlipala:

> 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.

Hello Adam,

thanks for the quick answer!  In fact, this is exactly what I meant when I 
said that the dilemma can be avoided.  However, this means that the type of P 
will be (R N1 N2) in all branches, which creates a number of problems in the 
other branches (just shown as 'magic ..' above).

Can't we have the more specific typing of P in each branch (that we do get 
with 'match N1,N2,P return..') without getting into the dilemma?

  best regards,

-- 
Erik Ernst - 
eernst AT cs.au.dk
Department of Computer Science, Aarhus University
IT-parken, Aabogade 34, DK-8200 Aarhus N, Denmark