[Agda] WellFounded usage

[Sergei Meshveliani]

On Mon, 2018-08-06 at 20:53 +0100, Arseniy Alekseyev wrote:
> I'll point out that I applied Induction/WellFounded.agda for exactly
> the same purpose (see DivMod.agda and Rec.agda nearby).
> Empirically this does not lead to exponential time in benchmarks (at
> least when compiled to Haskell), but I don't know why.
> 
> 
> Re: your second question, I think your definition is allowing
> non-constructive proofs of termination (because IsWellFoundedOrder is
> non-constructive), which is probably a significant extension of the
> type theory (but I don't really know what I'm talking about).
> 
> 
> You could change the definition to be constructive, of course, which
> doesn't really affect the rest of the proposal too much.
> 


Yes, it is also all right to relax 
                             ¬ IsDecreasing f 
to the property 
   breakDecrease :  (f : ℕ → C) → ∃ (\n → ¬ (f n > f (suc n)))

--
SM




> On Mon, 6 Aug 2018 at 13:20, Sergei Meshveliani <mechvel at botik.ru>
> wrote:
> 
>         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
>         
>         _______________________________________________
>         Agda mailing list
>         Agda at lists.chalmers.se
>         https://lists.chalmers.se/mailman/listinfo/agda