[Agda] On termination checkers

[david.janin at labri.fr]

Dear Andrew,

To your question, what shall be the best sizing for (inductive) lists,  
experiment seems to show that the answer is none !!!

I describe below the arguments with examples piled one on top of the other,  the 
correct code being enclosed. 

The experiment consists in trying all discussed definitions of sized (inductive)
list, dropping the pack/unpack aspects that is now irrelevant, and trying to prove
some expected (easy) list’s properties.

The possibilities discussed so far  (given in incorrect « piled » Agda code) are:

data SList (A : Set) : Size -> Set where
  — option (1) 
  nil : ∀ {i} -> SList A (↑ i) 
  — option (2)
  nil : ∀ {i} -> SList A i
  — option (3) 
  cons : ∀ {i} ->  A -> SList A i -> SList A (↑ i)
  — option (4) 
  cons : ∀ {i}{j : Size< i} ->  A -> SList A j -> SList A i

But, with the associated functions :

append : ∀ {A} -> SList A -> SList A  -> SList A
append nil l2 = l2
append (cons x l) l2 = cons x (append l l2) 

select : ∀ {A i} -> (A -> Bool) -> SList A i -> SList A _
select p nil = nil
select p (cons x l) with (p x)
... | false = select p l
... | true = cons x (select p l)

the following (expected) properties do not seem to hold:

append-nil : ∀ {A i} -> (l : SList A i) -> append l nil ≡ l
append-nil nil = refl                         
append-nil (cons x l) rewrite (append-nil l)
   = refl                                             — fail with option (4)

select-all : ∀ {A i} -> (l : SList A i) -> select (const true) l ≡ l
select-all nil = refl                            — fail with option (1) 
select-all (cons x l)  rewrite (select-all l)
  = refl                                              — fail with option (3)


with the error message «  ∞ != j of type Size » in all case. 
Option (2) is not an issue since  it must be combined with either (3) or (4).

The second counter example eventually came from the (wrong) intuition that
sized list with option (3) would force all functions on sized list to be size
preserving. But the outcome was rather unexpected. This sounds like a bug
doesn’t it ? 

Or this suggests that sized type are bound to be used with co-induction so that
escape towards infinity is possible.

In all case, my initial question on how to use helper functions in nested inductive types remains open.

Best,
David


P.S. The unpiled correct Agda code is enclosed below.

-------------- next part --------------
A non-text attachment was scrubbed...
Name: SizedList.agda
Type: application/octet-stream
Size: 2395 bytes
Desc: not available
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20190612/2b68664f/attachment.obj>
-------------- next part --------------