[Agda] WellFounded usage

[Sergei Meshveliani]

Dear all,

I have a certain problem with termination proof.
Consider the example: division with remainder for binary natural 
numbers (the code is contrived).

-------------------------------------------------------------------
record DivMod (dividend divisor : Bin) : Set where
       constructor result
       field
         quotient    :  Bin
         remainder   :  Bin
         equality    :  dividend ≡ remainder + quotient * divisor
         rem<divisor :  remainder < divisor

-- suc, +, ∸; *, <  are of Bin,   1+, +n, ∸n; *n, <n  are of  ℕ.

∣_∣ :  Bin → ℕ 
∣ x ∣ =  number of bits
 
divMod : (a b : Bin) → b ≢ 0# → DivMod a b
divMod a b b≢0 =  
               aux a (toℕ a) ≤-refl
       where
       aux : (a : Bin) → cnt → toℕ a ≤ cnt → DivMod a b
       aux a 0 aN≤0 =
                    result 0# 0# a≡0+0*b 0<b
                    where
                    a≡0 =  derived from aN≤0

       aux 0# _ _ =  result 0# 0# 0≡0+0*b 0<b

       aux a (1+ cnt) aN≤1+cnt =   -- here a ≢ 0#
           let 
             aN  = toℕ a
             e   = ∣ a ∣ ∸n ∣ b ∣  ...
             d   = (2^ e) * b      -- 2^ e  is by prepending several 
                                   --             zero bits.
             a'  = a ∸ d
             a'N = toℕ a'

             a'N≤cnt : a'N ≤n cnt 
             a'N≤cnt = 
                     because  a, d ≢ 0#,  and toℕ∸homo.

             (result q r a'≡r+q*b r<b) = aux a' cnt a'N≤cnt
           in
           restore a b q r a' r<b
------------------------------------------------------------------

This means that  divMod a b  is reduced to  (divMod (a ∸ d) b),
where  d = 2^e * b   for a certain appropriate e : ℕ.

The counter  cnt = (toℕ a) : ℕ   is reduced to a smaller value by this
step. 
Due to the structural decrement  (suc cnt) -> cnt,  Agda decides that 
the recursion is terminating.

But this may lead to exponential performance cost, because the unary 
representation of  cnt  is large,  and the evaluation (suc cnt) -> snt  
takes place not only in the proof part but also in regular evaluation.

To fix this, I change the counter to

       cnt = ∣ a ∣ : ℕ  =  number of bits in  a.

Then one needs to prove messy lemmata in order to prove that
∣ a ∣ >n ∣ a' ∣   in the loop.

The question is

  does there exist a way for this example to join 
  * a normal code performance (as in the second method version),
  * simple termination proof
?


I see in Standard library  Induction/WellFounded.agda.

It is  difficult to understand of how to apply this
(the impression is that it will complicate the program).

Can this tool be used to solve the above problem with  divMod  for Bin ?
Somehow to prove that _>_ is well-founded on Bin
(it is useful for many other programs), 
use the tools from WellFounded.agda, and prove termination of  divMod
in a simple way and without loosing run-time performance.

Can anybody, please, demonstrate, how this will change the above code
for divMod ?


Another question
----------------

Has it sense the language semantic extension with WellFoundedOrder ?

The property  IsWellFoundedOrder  concerns any  StrictPartialOrder,
and its simple definition is
    
                          appended to this letter.

Imagine that the type checker of  Agda-extended
sees in the above loop
                       a a' : Bin  and  a>a' : a > a',

sees the instance of  StrictPartialOrder  for _≡_ and _>_ on Bin,
sees the proof for  IsWellFoundedOrder  for this instance,
and concludes that  divMod  is terminating -- by the _implicit axiom_ 
of termination by a well-founded ordering.

With this, the proofs will be much simpler, simpler than with applying
the constructs of  Induction  of Library.

Agda is able to automatically find an argument in recursion that
decreases structurally. Similarly can it be able to find the argument
decreasing by _<_ and fit for well-founded recursion?

Agda sees that  a  is replaced with  a'  in the call, and it needs to
find where in the scope it is proved  a > a'.  At least this place for
a>a' can be marked, may be, by some pragma.

Thank you in advance for explanation,

------
Sergei

-------------- next part --------------
module WellFounded-2 where

open import Function         using (flip; _∘_)
open import Relation.Nullary using (¬_)
open import Relation.Binary  using (Rel; Setoid; StrictPartialOrder)
open import Relation.Binary.PropositionalEquality as PE using (_≡_)
open import Data.Product     using (∃)
open import Data.Nat         using (ℕ; suc) 



--****************************************************************************
Sequence :  ∀ {α} → (A : Set α) → Set α     -- infinite sequences in A 
Sequence A =  ℕ → A                       

module TwoSetoids {α α= β β=} (A : Setoid α α=) (B : Setoid β β=) 
  where
  open Setoid A using (_≈_) renaming (Carrier to C)
  open Setoid B using ()    renaming (Carrier to C'; _≈_ to _≈'_)

  Injective :  (C → C') → Set _
  Injective f =  
              (x y : C) → f x ≈' f y → x ≈ y

------------------------------------------------------------------------------
module _ {α α= α<} (PO : StrictPartialOrder α α= α<)  
  where
  open StrictPartialOrder PO using (_≈_; _<_; isEquivalence) 
                                              renaming (Carrier to C) 
  setoid : Setoid α α=
  setoid = record { Carrier = C;  _≈_ = _≈_; 
                                  isEquivalence = isEquivalence }

  _>_ : Rel C α<
  _>_ = flip _<_

  _≯_ :  Rel C α<
  _≯_ x =  ¬_ ∘ _>_ x

  IsDecreasing : Sequence C → Set _  
  IsDecreasing f =
                 ∀ n → f n > f (suc n)

  natSetoid        =  PE.setoid ℕ
  module Rel-Nat-C =  TwoSetoids natSetoid setoid
  open Rel-Nat-C using (Injective)

  IsWellFoundedOrder :  Set _
  IsWellFoundedOrder =  (f : Sequence C) → Injective f → 
                                           ¬ IsDecreasing f