[Agda] Standard WellFounded
Arseniy Alekseyev
arseniy.alekseyev at gmail.com
Fri Aug 10 15:06:23 CEST 2018
s/(x : X) → P a/(x : X) → P x/
On Fri, 10 Aug 2018 at 14:05, Arseniy Alekseyev <arseniy.alekseyev at gmail.com>
wrote:
> 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/0ae41e8b/attachment.html>
More information about the Agda
mailing list