The Coq mailing list

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

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.