[Agda] Standard WellFounded
Sergei Meshveliani
mechvel at botik.ru
Fri Aug 10 13:36:43 CEST 2018
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.
------------------------------------------------------------------
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
More information about the Agda
mailing list