[Agda] Standard WellFounded

[Sergei Meshveliani]

Thank you.
After this sample of  downFrom  I was able to program  divMod  for Bin.
But I am stuck with  gcd  for  Bin.
Consider a contrived simple version:

------------------------------------------------------
postulate
  rem  :  Bin → (y : Bin) → y ≢ 0# → Bin    -- remainder of x by y.

  rem< :  (x y : Bin) → (y≢0 : y ≢ 0#) → rem x y y≢0 < y

gcd : Bin → Bin → Bin
gcd x y
      with y ≟ 0#
...   | yes _  =  x
...   | no y≢0 =  gcd y (rem x y y≢0)

This lacks termination proof.
The argument pair  (x , y)  is replaced in recursion with  (y , r),
where  r < y.  So, it is needed well-founded recursion: 

gcd' : Bin → Bin → Bin
gcd' =  <-rec _ _ gc
  where
  postulate
   gc :  Bin → (b : Bin) → (∀ x y → y < b → Bin) → Bin    -- ??


I do not guess what signature to set for  gc.  
I set a hole "?" for  gc,  and the type checker shows

      Induction.WellFounded.WfRec _<_ (λ _ → Bin → Bin)
      .Relation.Unary._.⊆′ (λ _ → Bin → Bin)
-- ?

Can anybody help, please?

Thanks,

------
Sergei  



On Wed, 2018-08-08 at 17:49 +0200, Sandro Stucki wrote:
> > Can anybody demonstrate it on the following example?
> 
> Here you go:
> 
> --------------------------------------------------------------
> open import Function   using (_∘_; _on_)
> open import Data.List  using (List; []; _∷_)
> open import Data.Bin   using (Bin; toBits; pred; _<_; less; toℕ)
> open import Data.Digit using (Bit)
> import Data.Nat      as Nat
> import Induction.Nat as NatInd
> open import Induction.WellFounded
> 
> open Bin
> 
> predBin : Bin → Bin
> predBin = pred ∘ toBits
> 
> postulate
>   predBin-< :  (bs : List Bit) -> predBin (bs 1#) < (bs 1#)
> 
> -- The strict order on binary naturals implies the strict order on the
> -- corresponding unary naturals.
> <⇒<ℕ : ∀ {b₁ b₂} → b₁ < b₂ → (Nat._<_ on toℕ) b₁ b₂
> <⇒<ℕ (less lt) = lt
> 
> -- We can derive well-foundedness of _<_ on binary naturals from
> -- well-foundedness of _<_ on unary naturals.
> <-wellFounded : WellFounded _<_
> <-wellFounded =
>   Subrelation.wellFounded <⇒<ℕ (Inverse-image.wellFounded toℕ
> NatInd.<-wellFounded)
> 
> open All <-wellFounded using () renaming (wfRec to <-rec)
> 
> downFrom : Bin → List Bin     -- x ∷ x-1 ∷ x-2 ∷ ... ∷ 0# ∷ []
> downFrom = <-rec _ _ df
>   where
>     df : (b : Bin) → (∀ b′ → b′ < b → List Bin) → List Bin
>     df 0#      dfRec = 0# ∷ []
>     df (bs 1#) dfRec = (bs 1#) ∷ (dfRec (predBin (bs 1#)) (predBin-< bs))
> --------------------------------------------------------------
> 
> In order to use well-founded induction, we first have to prove that
> the strict order < is indeed well-founded. Thankfully, the standard
> library already contains such a proof for the strict order on (unary)
> naturals as well as a collection of combinators for deriving
> well-foundedness of relations from others (in this case the strict
> order on unary naturals).
> 
> The core of the implementation of `downFrom' via well-founded
> recursion is the function `df', which has the same signature as
> `downFrom' except for the additional argument `dfRec', which serves as
> the 'induction hypothesis'. The argument `dfRec' is itself a function
> with (almost) the same signature as `downFrom' allowing us to make
> recursive calls (i.e. take a recursive step), provided we can prove
> that the first argument of the recursive call (i.e. the argument to
> the induction hypothesis) is smaller than the first argument of the
> enclosing call to `df'. The proof that this is indeed the case is
> passed to `dfRec' as an additional argument of type b′ < b.
> 
> The following answer on Stackoverflow contains a nice explanation on
> how all of this is implemented in Agda under the hood:
> https://stackoverflow.com/a/19667260
> 
> Cheers
> /Sandro
> 
> 
> On Wed, Aug 8, 2018 at 12:13 PM Sergei Meshveliani <mechvel at botik.ru> wrote:
> >
> > On Tue, 2018-08-07 at 20:51 +0300, Sergei Meshveliani wrote:
> > > Dear all,
> > >
> > > I am trying to understand how to use WellFounded of Standard library.
> > >
> > > Can anybody demonstrate it on the following example?
> > >
> > > --------------------------------------------------------------
> > > open import Function  using (_∘_)
> > > open import Data.List using (List; []; _∷_)
> > > open import Data.Bin  using (Bin; toBits; pred)
> > >
> > > open Bin
> > >
> > > predBin : Bin → Bin
> > > predBin = pred ∘ toBits
> > >
> > > downFrom : Bin → List Bin     -- x ∷ x-1 ∷ x-2 ∷ ... ∷ 0# ∷ []
> > > downFrom 0#      =  0# ∷ []
> > > downFrom (bs 1#) =  (bs 1#) ∷ (downFrom (predBin (bs 1#)))
> > > --------------------------------------------------------------
> > >
> > > downFrom  is not recognized as terminating.
> > > How to reorganize it with using items from
> > > Induction/*, WellFounded.agda ?
> >
> >
> >
> > I presumed also that it is already given the property
> >
> >   postulate
> >     predBin-< :  (bs : List Bit) -> predBin (bs 1#) < (bs 1#)
> >
> > (I do not mean to deal here with its proof).
> >
> > --
> > SM
> >
> >
> > _______________________________________________
> > Agda mailing list
> > Agda at lists.chalmers.se
> > https://lists.chalmers.se/mailman/listinfo/agda
>