[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