[Agda] Termination problems with "with" and recursion

[Andreas Abel]

[CC to Ulf]

There are two issues here.

First, your size assignment for merge does not work.  You are saying 
both argument have a common upper bound that is decreased in each 
recursive call.  This is not the case, since only one of the two heaps 
gets smaller each time.  So you need to have two sizes:

module ShouldSucceed where

   merge : {i j : Size} {p : Nat} → Heap {i} p → Heap {j} p → Heap {∞} p
   merge empty h2 = h2
   merge h1 empty = h1
   merge .{↑ i} .{↑ j} (node {i} p1 l-rank p1≥p l1 r1) (node {j} p2 
r-rank p2≥p l2 r2) with order p1 p2
   merge .{↑ i} .{↑ j} (node {i} p1 l-rank p1≥p l1 r1) (node {j} p2 
r-rank p2≥p l2 r2) | le p1≤p2 = makeT p1 p1≥p l1 (merge {i} {↑ j} r1 
(node p2 r-rank p1≤p2 l2 r2))
   merge .{↑ i} .{↑ j} (node {i} p1 l-rank p1≥p l1 r1) (node {j} p2 
r-rank p2≥p l2 r2) | ge p1≥p2 = makeT p2 p2≥p l2 (merge {↑ i} {j} (node 
p1 l-rank p1≥p2 l1 r1) r2)

This should work.  However, it does not, which seems to be a bug, and I 
filed an issue.  (See agda issues 59).

If you expand the "with" out manually (the new command C-c C-h comes in 
very handy here), you get something that is accepted by the termination 
checker:

module Succeeds where
  mutual
   merge : {i j : Size} {p : Nat} → Heap {i} p → Heap {j} p → Heap {∞} p
   merge empty h2 = h2
   merge h1 empty = h1
   merge .{↑ i} .{↑ j} (node {i} p1 l-rank p1≥p l1 r1) (node {j} p2 
r-rank p2≥p l2 r2) =
     merge' {i} {j} p1 l-rank p1≥p l1 r1 p2 r-rank p2≥p l2 r2 (order p1 p2)

   merge' : ∀ {i} {j} {p} →
            ∀ p1 → Nat → p1 ≥ p → Heap {i} p1 → Heap {i} p1 →
            ∀ p2 → Nat → p2 ≥ p → Heap {j} p2 → Heap {j} p2 → Order p1 
p2 → Heap {∞} p
   merge' {i} {j} p1 l-rank p1≥p l1 r1 p2 r-rank p2≥p l2 r2 (le p1≤p2) = 
makeT p1 p1≥p l1 (merge {i} {↑ j} r1 (node p2 r-rank p1≤p2 l2 r2))
   merge' {i} {j} p1 l-rank p1≥p l1 r1 p2 r-rank p2≥p l2 r2 (ge p1≥p2) = 
makeT p2 p2≥p l2 (merge {↑ i} {j} (node p1 l-rank p1≥p2 l1 r1) r2)

Cheers,
Andreas

On 02.12.2013 14:09, Jan Stolarek wrote:
> Ok, I think I need some more assistance :-)
>
> Now let's say I have this definition:
>
> data Heap : {i : Size} → Priority → Set where
>    empty : {i : Size} {n : Priority} → Heap {↑ i} n
>    node  : {i : Size} {n : Priority} → (p : Priority) → Rank → p ≥ n →
>            Heap {i} p → Heap {i} p → Heap {↑ i} n
>
> ≥ is evidence that p >= n. If I now extend merge with evidence like this:
>
> merge : {i : Size} {p : Nat} → Heap {i} p → Heap {i} p → Heap p
> merge empty h2 = h2
> merge h1 empty = h1
> merge .{↑ i} (node .{i} p1 l-rank p1≥p l1 r1) (node {i} p2 r-rank p2≥p l2 r2) with order p1 p2
> merge .{↑ i} (node .{i} p1 l-rank p1≥p l1 r1) (node {i} p2 r-rank p2≥p l2 r2) | le p1≤p2
>    = makeT p1 p1≥p l1 (merge r1 (node p2 r-rank p1≤p2 l2 r2))
> merge .{↑ i} (node .{i} p1 l-rank p1≥p l1 r1) (node {i} p2 r-rank p2≥p l2 r2) | ge p1≥p2
>    = makeT p2 p2≥p l2 (merge r2 (node p1 l-rank p1≥p2 l1 r1))
>
> The termination checker complains on the second call to merge, but does not complain on the first
> one. I am puzzled. Andreas, can you explain why the first case works and the second doesn't? They
> seem to be symmetric. I'm attaching source file with definitions that I'm using.
>
> Janek
>
> Dnia poniedziałek, 2 grudnia 2013, Andreas Abel napisał:
>> Here you go:
>> Note that unconstraint sizes default to \inf, so you need to give sizes
>> in type signatures where sizes are important, e.g. in merge.
>>
>> {-# OPTIONS --sized-types #-}
>>
>> open import Size
>> open import Data.Bool
>>
>> module _ (Rank Priority : Set) (_<_ : Priority → Priority → Bool) where
>>
>> data Heap : {i : Size} → Set where
>>     empty : {i : Size} → Heap {↑ i}
>>     node  : {i : Size} → Priority → Rank → Heap {i} → Heap {i} → Heap {↑ i}
>>
>> module _ (makeT : Priority → Heap → Heap → Heap) where
>>
>>     merge : {i : Size} → Heap {i} → Heap {i} → Heap
>>     merge empty h2 = h2
>>     merge h1 empty = h1
>>     merge (node p1 w1 l1 r1) (node p2 w2 l2 r2)  with p1 < p2
>>     merge (node p1 w1 l1 r1) (node p2 w2 l2 r2)  | true  =
>>       makeT p1 l1 (merge r1 (node p2 w2 l2 r2))
>>     merge (node p1 w1 l1 r1) (node p2 w2 l2 r2)  | false =
>>       makeT p2 l2 (merge (node p1 w1 l1 r1) r2)
>>
>> Depending on what makeT is, you might be able to give a more precise
>> type to merge.
>>
>> On 02.12.2013 12:38, Jan Stolarek wrote:
>>> Ok, I think I need some help with Sized types. I have a datatype
>>> representing a Heap:
>>>
>>> data Heap : {i : Size} → Set where
>>>     empty : {i : Size} → Heap {↑ i}
>>>     node  : {i : Size} → Priority → Rank → Heap {i} → Heap {i} → Heap {↑
>>> i}
>>>
>>> And I need to use sized types in merge function:
>>>
>>> merge : {i : Size} → Heap → Heap → Heap
>>> merge h1 h2 with h1 | h2
>>> merge h1 h2 | empty | _ = h2
>>> merge h1 h2 | _ | empty = h1
>>> merge h1 h2  | (node p1 w1 l1 r1)  | (node p2 w2 l2 r2)  with p1 < p2
>>> merge h1 h2  | (node p1 w1 l1 r1)  | (node p2 w2 l2 r2)  | true  = makeT
>>> p1 l1 (merge r1 h2) merge h1 h2  | (node p1 w1 l1 r1)  | (node p2 w2 l2
>>> r2)  | false = makeT p2 l2 (merge h1 r2)
>>>
>>> Can I please have a hint how to do that? I tried adding annotation
>>> according to this presentation:
>>>
>>> www2.tcs.ifi.lmu.de/~abel/talkAIM2008Sendai.pdf‎
>>>
>>> but with no success :-/ I keep getting errors like i != inf.
>>>
>>> Janek
>
>


-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Theoretical Computer Science, University of Munich
Oettingenstr. 67, D-80538 Munich, GERMANY

andreas.abel at ifi.lmu.de
http://www2.tcs.ifi.lmu.de/~abel/
-------------- next part --------------
{-# OPTIONS --sized-types #-}
{-# OPTIONS --show-implicit #-}
{-# OPTIONS -v term:20  #-}
module SizedMerge where

open import Size

data Bool : Set where
  false : Bool
  true  : Bool

data Nat : Set where
  zero : Nat
  suc  : Nat → Nat

Priority : Set
Priority = Nat

Rank : Set
Rank = Nat

data _≥_ : Nat → Nat → Set where
  ge0 : {y : Nat}                   → y     ≥ zero
  geS : {x : Nat} {y : Nat} → x ≥ y → suc x ≥ suc y

infixl 4 _≥_

_+_ : Nat → Nat → Nat
zero  + m = m
suc n + m = suc (n + m)

infixl 6 _+_

data Order : Nat → Nat → Set where
  ge : {x : Nat} {y : Nat} → x ≥ y → Order x y
  le : {x : Nat} {y : Nat} → y ≥ x → Order x y

order : (a : Nat) → (b : Nat) → Order a b
order a       zero    = ge ge0
order zero    (suc b) = le ge0
order (suc a) (suc b) with order a b
order (suc a) (suc b) | ge ageb = ge (geS ageb)
order (suc a) (suc b) | le bgea = le (geS bgea)

data Heap : {i : Size} → Priority → Set where
  empty : {i : Size} {n : Priority} → Heap {↑ i} n
  node  : {i : Size} {n : Priority} → (p : Priority) → Rank → p ≥ n →
          Heap {i} p → Heap {i} p → Heap {↑ i} n

_≥ℕ_ : Nat → Nat → Bool
m     ≥ℕ zero  = true
zero  ≥ℕ suc n = false
suc m ≥ℕ suc n = m ≥ℕ n

rank : {n : Nat} → Heap n → Nat
rank empty            = zero
rank (node _ r _ _ _) = r

makeT : {n : Nat} → (p : Priority) → p ≥ n → Heap p → Heap p → Heap n
makeT p pgen l r with rank l ≥ℕ rank r
makeT p pgen l r | true  = node p (suc (rank l + rank r)) pgen l r
makeT p pgen l r | false = node p (suc (rank l + rank r)) pgen r l


module Fails where

  merge : {i : Size} {p : Nat} → Heap {i} p → Heap {i} p → Heap p
  merge empty h2 = h2
  merge h1 empty = h1
  merge .{↑ i} (node .{i} p1 l-rank p1≥p l1 r1) (node {i} p2 r-rank p2≥p l2 r2) with order p1 p2
  merge .{↑ i} (node .{i} p1 l-rank p1≥p l1 r1) (node {i} p2 r-rank p2≥p l2 r2) | le p1≤p2
    = makeT p1 p1≥p l1 (merge {↑ i} r1 (node p2 r-rank p1≤p2 l2 r2))
  merge .{↑ i} (node .{i} p1 l-rank p1≥p l1 r1) (node {i} p2 r-rank p2≥p l2 r2) | ge p1≥p2
    = makeT p2 p2≥p l2 (merge {↑ i} r2 (node p1 l-rank p1≥p2 l1 r1))

module ShouldSucceed where

  merge : {i j : Size} {p : Nat} → Heap {i} p → Heap {j} p → Heap {∞} p
  merge empty h2 = h2
  merge h1 empty = h1
  merge .{↑ i} .{↑ j} (node {i} p1 l-rank p1≥p l1 r1) (node {j} p2 r-rank p2≥p l2 r2) with order p1 p2
  merge .{↑ i} .{↑ j} (node {i} p1 l-rank p1≥p l1 r1) (node {j} p2 r-rank p2≥p l2 r2) | le p1≤p2 = makeT p1 p1≥p l1 (merge {i} {↑ j} r1 (node p2 r-rank p1≤p2 l2 r2))
  merge .{↑ i} .{↑ j} (node {i} p1 l-rank p1≥p l1 r1) (node {j} p2 r-rank p2≥p l2 r2) | ge p1≥p2 = makeT p2 p2≥p l2 (merge {↑ i} {j} (node p1 l-rank p1≥p2 l1 r1) r2)


module Succeeds where
 mutual
  merge : {i j : Size} {p : Nat} → Heap {i} p → Heap {j} p → Heap {∞} p
  merge empty h2 = h2
  merge h1 empty = h1
  merge .{↑ i} .{↑ j} (node {i} p1 l-rank p1≥p l1 r1) (node {j} p2 r-rank p2≥p l2 r2) =
    merge' {i} {j} p1 l-rank p1≥p l1 r1 p2 r-rank p2≥p l2 r2 (order p1 p2)

  merge' : ∀ {i} {j} {p} →
           ∀ p1 → Nat → p1 ≥ p → Heap {i} p1 → Heap {i} p1 →
           ∀ p2 → Nat → p2 ≥ p → Heap {j} p2 → Heap {j} p2 → Order p1 p2 → Heap {∞} p
  merge' {i} {j} p1 l-rank p1≥p l1 r1 p2 r-rank p2≥p l2 r2 (le p1≤p2) = makeT p1 p1≥p l1 (merge {i} {↑ j} r1 (node p2 r-rank p1≤p2 l2 r2))
  merge' {i} {j} p1 l-rank p1≥p l1 r1 p2 r-rank p2≥p l2 r2 (ge p1≥p2) = makeT p2 p2≥p l2 (merge {↑ i} {j} (node p1 l-rank p1≥p2 l1 r1) r2)


module Succeeds' where
 mutual
  merge : ∀ {i j p} → Heap {i} p → Heap {j} p → Heap {∞} p
  merge empty h2 = h2
  merge h1 empty = h1
  merge  (node p1 l-rank p1≥p l1 r1) (node p2 r-rank p2≥p l2 r2) =
    merge' p1 l-rank p1≥p l1 r1 p2 r-rank p2≥p l2 r2 (order p1 p2)

  merge' : ∀ {i j p} →
           ∀ p1 → Nat → p1 ≥ p → Heap {i} p1 → Heap {i} p1 →
           ∀ p2 → Nat → p2 ≥ p → Heap {j} p2 → Heap {j} p2 → Order p1 p2 → Heap {∞} p
  merge' p1 l-rank p1≥p l1 r1 p2 r-rank p2≥p l2 r2 (le p1≤p2) = makeT p1 p1≥p l1 (merge r1 (node p2 r-rank p1≤p2 l2 r2))
  merge' p1 l-rank p1≥p l1 r1 p2 r-rank p2≥p l2 r2 (ge p1≥p2) = makeT p2 p2≥p l2 (merge (node p1 l-rank p1≥p2 l1 r1) r2)