[Agda] Standard WellFounded

[Arseniy Alekseyev]

Something like this, I think:

P : Bin → Set
P _y = (x : Bin) → Bin

gc :  (y : Bin) → (∀ y' → y' < y → P y') → P y

then after applying <-rec you get something of type [(y : Bin) → P y],
which is just gcd with arguments swapped.

(I wrote P in a general form so that it's more similar to "dependent"
examples, but of course you don't need to)

On Thu, 9 Aug 2018 at 20:40, Sergei Meshveliani <mechvel at botik.ru> wrote:

> 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
> >
>
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20180809/a93ff425/attachment.html>