The Coq mailing list

[Matthieu Sozeau <matthieu.sozeau AT gmail.com>]

Hi all,

On 8 janv. 2014, at 10:52, Altenkirch Thorsten 
<psztxa AT exmail.nottingham.ac.uk>
 wrote:

> On 07/01/2014 23:03, "Conor McBride" 
> <conor AT strictlypositive.org>
>  wrote:
> 
>> 
>> On 7 Jan 2014, at 22:47, Altenkirch Thorsten
>> <psztxa AT exmail.nottingham.ac.uk>
>>  wrote:
>> 
>>> Hi Conor,
>>> 
>>> I am sure this must be a stupid question but why is this not covered
>>> by your result that pattern matching can be reduced to eliminators + K?
>> 
>> The recursive call isn't covered by the inductive hypothesis. The direct
>> version
>> gives no account of the inductive hypothesis *at all*, hence the whole
>> mess.
>> 
>>>>>> moo (wrap f) = noo (Zero -> WOne) myIso f
>>>>>> noo .WOne Refl x = moo x
>> 
>> The recursive call
>> 
>> moo x
>> 
>> is really a recursive call
>> 
>> moo (subst myIso ... f)
>> 
>> but the inductive hypothesis tells us just that we can call moo on
>> outputs of f.
>> 
>> Bottom line: it's not structurally recursive.
> 
> I know this - this was precisely the comment I made in my reply to Maxime.
> 
> However, it seems I am a victim of my own propaganda: I was always
> thinking that Conor's result tells us that we can replace pattern matching
> (with guarded recursion) by elimination constants.


> 
> However, this example shows that this is not true. Once we perform the
> unification required by pattern matching we obtain a a term which "looks"
> as if it is structurally smaller even though it isn??t


Pattern-matching and termination checking are still two different things, 
especially in Coq where match and fix are separate constructs. However,
one could allow recursive calls on subst??ed arguments by providing a 
different
recursion eliminator (measures, general well-foundedness etc??). You would 
just
have to find a well-founded order for which [subst (foo : Empty -> Box ?? 
Box) f <= f].

> One obvious question is how we can recognize good instances of pattern
> matching from bad ones.

Termination checking being undecidable I think that obligation to show it??s
a ??good?? pattern-matching has to be left to the user (providing as much
automation as we can without getting in her way of course). That??s what
my Equations package does (it also implements Conor??s et al elimination of 
pattern-matching down to eliminators). 

> This also increases the argument in favour of a safe version of pattern
> matching which is evidence producing. One of my new students, Gabe
> Dijkstra, is working on this - mainly triggered by the without-K issue.
> However, as we see now there are other issues which went unnoticed.

Indeed, "better be safe than sorry".

Cheers,
?? Matthieu