The Coq mailing list

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

Sorry for the semi-spamming, the file I attached before contained a typo 
(which does not affect the point, but still disturbs the message).  The 
attached file fixes this.

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.

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