[Agda] size-based termination

[Ondrej Rypacek]

> The problem here is the deep matching qtrans (qsym (...)).  For one, sized
> types would definitely work here (make Quo indexed by size).  [If you do not
> hit a bug].

Yes. It's not very complicated.
Making Quo indexed works well for trans but makes things complicated
elsewhere , I think. Or maybe I'd just have to make more changes to
the rest of the code. I guess I'd just have to replace Quo by \Sigma
(n : N) (Quo n)  // roughly speaking // and insert projections and
sizes where necessary.  But I thought there should be a local
solution.


>
> Or: Cannot you define a more general function that has a flag whether it
> stepped over a qsym.  You want two qsym to cancel out, this is like the
> structurally recursive algorithm to compute a negation normal form.

A nice idea. Yes, it should work in this case.

In the meantime I've come up with an alternative solution: see below.
Maybe a bit too long, but works.


Thank you all for pointing me in the right direction.
Cheers
Ondrej







-- Quo stays the same:

data Quo {X Y : Set}(f g : X → Y) : Y → Y → Set where
  qrefl : (b : Y) → Quo  f g b b
  qsym : {a b : Y} → Quo f g a b → Quo f g b a
  qstep : {a b c : Y} → {x : X} → f x ≡ a → g x ≡ b → Quo f g b c → Quo f g a c
  qstep' : {a b c : Y} → {x : X} → f x ≡ b → g x ≡ a → Quo f g b c → Quo f g a c


-- QuoSize is the predicate: q has size n
data QuoSize {X Y : Set}{f g : X → Y} : {a b : Y} → Quo f g a b → ℕ → Set where
  qsrefl : {b : Y} → QuoSize (qrefl b) zero
  qssym : {a b : Y}{n : ℕ}{q : Quo f g a b} → QuoSize q n → QuoSize
(qsym q) (suc n)
  qsstep : {a b c : Y}{x : X}{n : ℕ} → (h : f x ≡ a) → (i : g x ≡ b) →
(y : Quo f g b c) → (QuoSize y n) → QuoSize (qstep h i y) (suc n)
  qsstep' : {a b c : Y}{x : X}{n : ℕ} → (h : f x ≡ b) → (i : g x ≡ a)
→ (y : Quo f g b c) → (QuoSize y n) → QuoSize (qstep' h i y) (suc n)


-- qtrans' is now structurally decreasing on the size

qtrans' : {X Y : Set}{a b c : Y}{f g : X → Y} → (h : Quo f g a b) → {n
: ℕ} → QuoSize h n → (k : Quo f g b c) → {m : ℕ} → QuoSize k m → Σ
(Quo f g a c) (λ q → Σ ℕ (λ n → QuoSize q n))
qtrans' {a = .b} {b = b} .(qrefl b) {.0} (qsrefl {.b}) k {m} K = k , (m , K)
qtrans' {a = a} .(qsym (qrefl a)) {.(suc n)} (qssym {.a} {.a} {n}
{qrefl .a} y) k {m} K = k , (m , K)
qtrans' (qsym (qsym y)) (qssym  (qssym y')) k {m} K = qtrans' y y' k K
qtrans' (qsym (qstep {x = x} h i y)) (qssym (qsstep .h .i .y y')) k K
= qtrans' (qsym y) (qssym y') (qstep' h i k) (qsstep' h i k K)
qtrans' (qsym (qstep' {x = x} h i y)) (qssym (qsstep' .h .i .y y1)) k
{m} K = qtrans' (qsym y) (qssym y1) (qstep h i k) (qsstep h i k K)
qtrans' .(qstep h i y) (qsstep h i y y') k K =
  let T = qtrans' y y' k K
  in qstep h i (proj₁ T)  , (suc (proj₁ (proj₂ T))) , qsstep h i
(proj₁ T) (proj₂ (proj₂ T))
qtrans' .(qstep' h i y) (qsstep' h i y y') k K =
  let T = qtrans' y y' k K
  in (qstep' h i (proj₁ T)) , ((suc (proj₁ (proj₂ T))) , (qsstep' h i
(proj₁ T) (proj₂ (proj₂ T))))


-- Quo's can be sized structurally recursively
sizeQuo : {X Y : Set}{a b : Y}{f g : X → Y} → (h : Quo f g a b) → Σ ℕ
(λ n → QuoSize h n)
sizeQuo {X} {Y} {.b} {b} (qrefl .b) = 0 , qsrefl
sizeQuo (qsym y) = let R = sizeQuo y in suc (proj₁ R) , qssym (proj₂ R)
sizeQuo (qstep h i y) = let R = sizeQuo y in (suc (proj₁ R)) , (qsstep
h i y (proj₂ R))
sizeQuo (qstep' h i y) = let R = sizeQuo y in (suc (proj₁ R)) ,
(qsstep' h i y (proj₂ R))


-- the new qtrans forgets the sizes again
qtrans : {X Y : Set}{a b c : Y}{f g : X → Y} → Quo f g a b → Quo f g b
c → Quo f g a c
qtrans h k = let SH = sizeQuo h
             in let SK = sizeQuo k
             in proj₁ (qtrans' h {proj₁ SH} (proj₂ SH) k {proj₁ SK} (proj₂ SK) )