[Agda] Standard WellFounded

[Sandro Stucki]

> 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