[Agda] Standard WellFounded

Arseniy Alekseyev arseniy.alekseyev at gmail.com
Fri Aug 10 15:05:51 CEST 2018


Two things:

1.
In your first attempt you did not re-define GCD (or you skipped that from
your e-mail, but that seems to be the important part). The original
definition can't work because [GCD x] isn't even a type so nothing can ever
return a value of this type.
You need to define something like (I'll stubbornly keep calling this P for
similarity with other examples but you're free to call it whatever):
P : Bin → Set
P a = (b : Bin) → GCD a b

2. Giving P explicitly can help improve error messages a lot. You can try
something like this:
gcd =  <-rec _ P gc

I haven't look in much detail so maybe this is not actually helpful. Sorry
if it's not.


> WellFounded recursion thing is also available directly for the signature
of
> gcd : (a b : Bin) → GCD a b,

It's only available for signatures of form [(x : X) → P a] for well-founded
X, so yes, that's the case. By unifying the two types you get exactly the P
I wrote above.

On Fri, 10 Aug 2018 at 13:35, Sergei Meshveliani <mechvel at botik.ru> wrote:

> On Fri, 2018-08-10 at 14:36 +0300, Sergei Meshveliani wrote:
> > On Thu, 2018-08-09 at 23:15 +0100, Arseniy Alekseyev wrote:
> > > 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)
> > >
> >
> >
> >
> > Thank you.
> > This works with the result of  Bin.
> > I try to extend this to
> >                      gcd : (a b : Bin) -> GCD a b,
> > and fail.
> >
>
>
> Below       r<x = rem< x y x≢0
> was a typo,
> it needs to be replaced with  r<x = rem< y x x≢0.
>
> But this  does not change the report of Agda.
>
>
> Another attempt
> ===============
>
> I change the signatures to
>
> ------------------------------------------
> BB = Bin × Bin
>
> _<p_ :  Rel BB Level.zero
> _<p_ =  _<_ on proj₁
>
> open import Induction.WellFounded using (WellFounded)
>
> postulate  <p-wellFounded : WellFounded _<p_
>
> open All <p-wellFounded using () renaming (wfRec to <-rec)
>
> record GCD (pr : BB) : Set   -- contrived
>        where
>        constructor gcd′
>        a = proj₁ pr
>        b = proj₂ pr
>
>        field  res       : Bin
>               divides-a : ∃ (\q → res * q ≡ a)
>               divides-b : ∃ (\q → res * q ≡ b)
>               -- and maximality axiom
>
> gcd : (pr : BB) → GCD pr
> ----------------------------------------------
>
> Now  gcd  is  on  Bin × Bin,  and your approach works,
> the code is type-checked:
>
> gcd =  <-rec _ _ gc
>   where
>   gc :  (pr : BB) → (∀ pr' → pr' <p pr → GCD pr') → GCD pr
>   gc (x , y) gcRec
>              with x ≟ 0#
>
>   ... | no x≢0 =  f
>                   where
>                   f : GCD (x , y)
>                   f = liftGCD (gcRec (r , x) r<x)
>                       where
>                       r   = rem y x x≢0
>                       r<x = rem< y x x≢0
>
>                       postulate  liftGCD : GCD (r , x) → GCD (x , y)
>   ... | ...
> -------------------------------------------------
>
>
> All right:  I can convert from  GCD-auxiliary (a , b)
> to                              GCD a b.
>
> But I have an impression that the WellFounded recursion thing is also
> available directly for the signature of
>
>           gcd : (a b : Bin) → GCD a b,
>
> only am missing something.
> -- ?
>
> Regards,
>
> ------
> Sergei
>
>
>
>
>
>
> > ------------------------------------------------------------------
> > 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
> >
> >
> > record GCD (a b : Bin) : Set   -- contrived
> >        where
> >        constructor gcd′
> >
> >        field  res       : Bin
> >               divides-a : ∃ (\q → res * q ≡ a)
> >               divides-b : ∃ (\q → res * q ≡ b)
> >               --
> >               -- and maximality axiom
> >
> > -- Without using termination proof:
> > --
> > {-# TERMINATING #-}
> > gcd : (a b : Bin) → GCD a b
> > gcd x y
> >       with x ≟ 0#
> > ...   | yes x≡0 =  gcd′ y (0# , y*0≡x) (1# , y*1≡y)
> >                    where
> >                    postulate  y*0≡x : y * 0# ≡ x
> >                               y*1≡y : y * 1# ≡ y
> >
> > ...   | no x≢0 =   liftGCD (gcd r x)
> >                    where
> >                    r = rem y x x≢0
> >
> >                    postulate  liftGCD : GCD r x → GCD x y
> > ---------------------------------------------------------------
> >
> > The second argument is divided by the first one in the loop -- this way
> > it is easier to use.
> >
> > This is type-checked.
> >
> > Now try WellFounded. As I understand, the approach is to reduce to a
> > function of a single argument:
> >
> > ---------------------------------------------------------------
> > gcd : (a : Bin) → GCD a
> > gcd =  <-rec _ _ gc
> >   where
> >   gc :  (x : Bin) → (∀ x' → x' < x → GCD x') → GCD x
> >   gc x gcRec
> >        with x ≟ 0#
> >   ...  | yes x≡0 =  f
> >                     where
> >                     f : GCD x
> >                     f y =  gcd′ y (0# , y*0≡x) (1# , y*1≡y)
> >                            where
> >                            postulate y*0≡x : y * 0# ≡ x
> >                                      y*1≡y : y * 1# ≡ y
> >
> >   ...  | no x≢0 =  f
> >                    where
> >                    f : GCD x
> >                          f y = liftGCD (gcRec r r<x x)
> >                                where
> >                          r   = rem y x x≢0
> >                                r<x = rem< x y x≢0
> >
> >                          postulate  liftGCD : GCD r x → GCD x y
> > ---------------------------------------------------------------
> >
> > Agda type-checks the function  gc,
> > but it reports that  (<-rec _ _ gc)  does not return a value of the type
> > GCD a.
> >
> > Then I try
> >
> >  gcd :  Bin → (Bin → Set)
> >  gcd =  <-rec _ _ gc
> >   where
> >   postulate
> >     gc :  (x : Bin) → (∀ x' → x' < x → Bin → Set) → Bin → Set
> >
> > (which goal adequacy I do not understand).
> > It is type-checked,
> > but I fail to implement this version of gc.
> >
> > Can anybody advise, please?
> >
> > ------
> > Sergei
> >
> >
> >
> >
> > > 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
> >
> >
> > _______________________________________________
> > 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/20180810/0eb038b4/attachment.html>


More information about the Agda mailing list