[Agda] list equality decision procedure fails termination check with Agda 2.4.0.1?

[Maxime Dénès]

As Bruno Barras posted on this list some time ago, the fix I 
implemented* for Coq (following Bruno's ideas) is restricting the 
propagation of size information from branches of a pattern matching to 
the match itself depending on its "return predicate" (i.e. the predicate 
we would pass to an eliminator if we were using eliminators).

Problematic examples were using a predicate of the form fun X (H : T = 
X) => X, where T and X are types, to make the termination checker 
interpret the size of objects of type T in an unrelated type U, given an 
equality H : T = U. In these cases, the propagation of size is now 
forbidden. However, if the predicate returns an explicit inductive 
family, like fun X H => list X, we know that the branches and the 
pattern matching will be lists, and the size information will be 
preserved. Likewise, if the predicate is fun X H => list tree, the size 
of list elements will also be preserved.

I'm wondering what the intuition behind Agda's current criterion is, 
because even equalities between two data types can potentially be used 
to rewrite along isomorphisms which don't preserve sizes. So the fact 
that the type of the recursive argument is a data type before any 
matching doesn't seem to address the problem fully, at least from a 
"semantic" point of view. Now, maybe the syntax of pattern matching and 
flexibility of the termination checker are restricted enough to avoid 
further issues?

* The code is available on github: 
https://github.com/maximedenes/coq/tree/guard-fix

Maxime.

On 07/01/2014 12:00 AM, Jesper Cockx wrote:
> The current restriction is quite simple: for a function to be
> structurally recursive on an argument x of type T, the type T must be
> a data type *before* any matching has been done. In particular, this
> prohibits structural recursion on 'deep' arguments and universe-like
> constructions such as the one in my previous mail. I don't know what
> the current situation is on the Coq side of things, maybe someone else
> can clarify?
>
> Jesper
>
> On 6/30/14, Dan Licata <dlicata at wesleyan.edu> wrote:
>> great! is there a way to explain what the restriction is?  Has Coq fixed
>> this bug yet, and if so, how does your solution compare to theirs?
>>
>> -Dan
>>
>> On Jun 27, 2014, at 12:26 PM, Jesper Cockx <Jesper at sikanda.be> wrote:
>>
>>> Yes, this restriction is to address the incompatibility of the termination
>>> checker with univalence. As a side-effect, many functions on universes no
>>> longer pass the termination check, for example (by Andreas):
>>> T : Bool -> Set
>>> T true = Nat
>>> T false = List Nat
>>>
>>> f : (x : Bool) -> T x -> Set
>>> f true zero = Nat
>>> f true (suc x) = f true x
>>> f false nil = Nat
>>> f false (x :: xs) = f false xs
>>> For the moment, such definitions have to be unfolded manually:
>>> f : (x : Bool) -> T x -> Set
>>> f true = ftrue
>>>    where
>>>      ftrue : Nat -> Set
>>>      ftrue zero = Nat
>>>      ftrue (suc x) = ftrue x
>>> f false = ffalse
>>>    where
>>>      ffalse : List Nat -> Set
>>>      ffalse nil = Nat
>>>      ffalse (x :: xs) = ffalse xs
>>> However, due to a mistake I made in the fix, the termination checker a
>>> complains much more than necessary when --without-K is enabled. This has
>>> now been fixed in the development version:
>>> https://code.google.com/p/agda/issues/detail?id=1214&can=1. I'll check the
>>> other errors in Nils' library later. If you have any specific examples
>>> that you think should be accepted, please send them to me and I'll see
>>> what I can do.
>>>
>>> Jesper
>>>
>>>
>>> On Fri, Jun 27, 2014 at 6:52 AM, Dan Licata <dlicata at wesleyan.edu> wrote:
>>> Is this restriction addressing the "termination checker + propositional
>>> univalence inconsistency" issue, or something else?
>>>
>>> -Dan
>>>
>>> On Jun 21, 2014, at 1:44 PM, Jesper Cockx <Jesper at sikanda.be> wrote:
>>>
>>>> I suppose by 'people working on this issue', you mean Andreas and me? I'm
>>>> not currently working on this problem, but I could be convinced to if the
>>>> current hack turns out to be too inconvenient. However, I have two
>>>> problems before I can start working on a fix:
>>>>
>>>> - The current theory of pattern matching doesn't allow induction on
>>>> 'deep' arguments, i.e. ones that only get an inductive type after pattern
>>>> matching on some other arguments. So the theory would have to be
>>>> extended.
>>>>
>>>> - I don't have a lot of experience with the termination checker, so I'm
>>>> not confident to mess with it. It seems that in order to fix this
>>>> problem, the termination checker would need some type information, as
>>>> well as information about the substitutions performed by the previous
>>>> case splits.
>>>>
>>>> If anyone can help me with (one of) these problems, I'd like to work
>>>> together on it. Otherwise I'll try to get a better understanding by
>>>> myself, but then it might take a long time.
>>>>
>>>> Jesper
>>>>
>>>>
>>>> On Fri, Jun 20, 2014 at 7:13 PM, Andrés Sicard-Ramírez <asr at eafit.edu.co>
>>>> wrote:
>>>>
>>>> On 20 June 2014 09:07, Brent Yorgey <byorgey at seas.upenn.edu> wrote:
>>>> but is the code I linked now expected to
>>>> fail termination checking?
>>>>
>>>> Using the --without-K option? I don't know. This is an open issue and
>>>> people working on this issue know that the current behaviour is too
>>>> restrictive. I don't know if they are working in a better solution
>>>> right now.
>>>>
>>>> --
>>>> Andrés
>>>>
>>>> _______________________________________________
>>>> Agda mailing list
>>>> Agda at lists.chalmers.se
>>>> https://lists.chalmers.se/mailman/listinfo/agda
>>>>
>>>>
>>>> _______________________________________________
>>>> Agda mailing list
>>>> Agda at lists.chalmers.se
>>>> https://lists.chalmers.se/mailman/listinfo/agda
>>>
>>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda