The Coq mailing list

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

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

> Erik Ernst wrote:
>> 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?
>>   
> 
> I'm not sure what you mean.  The type of [P] _is_ maximally refined above, 
> as far as I understand.


In fact, I get error messages like 'The term "P" has type "R (natS N1') (natS 
N2')" in the last branch above when doing 'match N1,N2,P return..' and error 
messages like 'The term "P" has type "R N1 N2" when doing 'match N1,N2 
return..'.  

I interpreted that to mean that P was typed as indicated, which would 
presumably mean that the extra knowledge about N1 and N2 would only appear in 
the type of P when it is included in the pattern match, otherwise it always 
gets the type (R N1 N2).

I've experimented a little more with this and attached two example files 
showing the two situations.

  best regards,

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

Attachment: dilemma.v
Description: Binary data