The Coq mailing list

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

Hello again Adam & [Coq-Club]'ers,

the convoy pattern indeed solves the problem! - Here's the version of the 
match that refines the type of P as required:

  Definition F (N1 N2: Nat) (P: R N1 N2): True :=
    match N1,N2 return (R N1 N2) -> True with
      | natO     , natO     => (fun (P': R natO       natO)       => I)
      | natO     , natS N2' => (fun (P': R natO       (natS N2')) => I)
      | natS N1' , natO     => (fun (P': R (natS N1') natO)       => I)
      | natS N1' , natS N2' => (fun (P': R (natS N1') (natS N2')) => I)
    end P.

This idea also works in the original context.  Cool, and thanks!

On another note, I still think that my earlier experiments demonstrate a 
problem in coqc type checking, as explained below.

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

> Erik Ernst wrote:
>> Den 22/09/2011 kl. 14.14 skrev Adam Chlipala:
>> 
>>  
>>> Erik Ernst wrote:
>>>    
>>>> 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.
> 
> The code I suggested has none of the problems you mention.  I'm a bit 
> confused because your new example program demonstrates issues with two ways 
> of writing the pattern match, neither of which is the way that I suggested.

I probably wasn't sufficiently explicit about the purpose of those examples.  
So let me clarify a bit:  The point was _not_

  "here are two type incorrect definitions, please help me making them 
acceptable to the type checker"

On the contrary, the point was

  "here are two definitions that contain type incorrect expressions 
demonstrating the following:

      - in 'match N1,N2 return ..', the Coq type checker tells me that P has 
type (R N1 N2)

      - in 'match N1,N2,P return ..' the Coq type checker tells me that P has 
type (R (natS N1') (natS N2'))

  and in both cases the error message shows that Coq considers (R N1 N2) and 
(R (natS N1') (natS N2'))
  as different types even though the given branch of the match implies that 
N1 = natS N1' and N2 = natS N2'.

My conclusion was that using 'match N1,N2,P return ..' is the way to get the 
most specific type for P in each branch.  However, it seems to cause Coq to 
produce inconsistent error messages, and that was the first issue I raised:

In the first version of the definition I mailed to this list, I used 'match 
N1,N2,P return ..' and provided two different expressions containing P, let 
us call them e1[P] and e2[P]:

  match N1,N2,P return .. with
    ... (* other branches *) ...
    | natS N1', natS N2', P => e[ei[P]]
  end

where e[_] is a larger expression with a hole where either e1[P] or e2[P] 
goes (shown above as ei[P]).  Note that e1 and e2 do not contain any binders 
for the name P, so P has the same meaning when used in e1 and in e2.  Still,

  - if we use e1[P], Coq claims that P has type (R (natS N1') (natS N2')) but 
it must have type (R N1 N2)
  - if we use e2[P], Coq claims that P has type (R N1 N2) but it must have 
type (R (natS N1') (natS N2'))

Isn't that a bug?  Shouldn't P have one specific type T in both cases, and 
type checking should then verify that T is an appropriate type for the 
expression that occurs in the "hole" of e1 resp. e2.  But then we should have 
had the following type of response from Coq for some types T, T1, and T2:

  - if we use e1[P], Coq would then claim that P has type T but it must have 
type T1
  - if we use e2[P], Coq would then claim that P has type T but it must have 
type T2

(or, of course, the check might succeed such that one or both of the error 
messages would not be printed).  But Coq does in fact claim two different 
types for P in the two situations.

> The rules in question here, for dependent pattern matching, are extremely 
> simple, and basically 10 minutes of studying the typing rule can save you 
> from ever being surprised again about the types of variables.

I would have considered Coq's behavior to be more simple if it had given P 
the same type in both cases described above.  ;-)

> The CPDT book explains all this, along with some useful design patterns for 
> fitting the dependency structures of particular programs into the framework 
> that Coq understands.


Thanks a lot for all your input to this community!

  best regards,

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