[Agda] Nat for termination counter

[Sergei Meshveliani]

Dear all,

I have a certain doubt about using the counter of Nat for termination
proofs.
Consider the function for listing binary numbers:

----------------------------------------
pred : Bin → Bin
pred = fromBits ∘ minusCarry 1b ∘ toBits

downFrom : Bin → List Bin
downFrom 0# = [ 0# ]
downFrom (bs 1#) = (bs 1#) ∷ (downFrom (pred (bs 1#)))
----------------------------------------

Bin is intended to be used in order to avoid certain expensive
operations with Nat.

downFrom is fast, but it has termination problem.
It needs a terminating version which is also fast. I try:

---------------------------------------------------------------------
downFrom x = aux x (toℕ x) refl
where
aux : (x : Bin) → (cnt : ℕ) → toℕ x ≡ cnt → List Bin
aux 0# _ _ = [ 0# ]
aux (bs 1#) 0 bs1N≡0 = ⊥-elim (toℕ-bs1≢0 bs bs1N≡0)
aux (bs 1#) (suc cnt) bs1N≡cnt' = bs1 ∷ (aux (pred bs1) cnt eq)
where
bs1 = bs 1#

eq : toℕ (pred bs1) ≡ cnt
eq = begin toℕ (pred bs1) ≡⟨ toℕ-pred-homo bs1 ⟩
predN (toℕ bs1) ≡⟨ cong predN bs1N≡cnt' ⟩
predN (suc cnt) ≡⟨ refl ⟩
cnt
∎
---------------------------------------------------------------------

It applies a certain theorem of toℕ-pred-homo.
It also uses the toℕ conversion for the counter cnt, and the counter
serves termination proof.

I do not know how to avoid potentially large data for the counter
(never looked into sized types).

But I have an impression that here the usage of toℕ does not explode
the evaluation cost. Because
* the (suc cnt) data always appears fast from toℕ bs1 (?),
and the next counter is cnt,
* the cnt value is evaluated lazily, it never becomes large in memory
(?).

What people think of this?

As an experiment, I try

-------------------------
test : Bin → List String
test x =
"x = " ∷ showB x ∷
"\nxL = " ∷ showB xL ∷
[]
where
xs = downFrom x; xL = last 0# xs
-------------------------

- build x ∷ (pred x) ∷ pred (pred x) ∷ ... ∷ 0# ∷ []

and print the last elment (x is input from file).

Running this shows a linear cost order:
the time for (x *2) is 2 * (time for x).

How people think, is this a reliable approach?

Thanks,

------
Sergei