[Agda] Termination problems with "with" and recursion

[Jan Stolarek]

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


-------------- next part --------------
{-# OPTIONS --sized-types #-}
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

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))