[Agda] Standard WellFounded

[Sergei Meshveliani]

On Wed, 2018-08-08 at 21:33 +0300, Sergei Meshveliani wrote:
> (I have forgotten to copy my reply to the list)
> 
> Sandro, thank you very much.
> I do understand a certain part of this. And  downFrom  is type-checked.
> 
> Then I try to mimic the approach to the function  divMod  for Bin
> (without understanding the type of <-rec):
> 
> --------------------------------------------------
> record DivMod (dividend divisor : Bin) : Set where
>        constructor result
>        field
>          quotient    :  Bin
>          remainder   :  Bin
>          equality    :  dividend ≡ remainder + quotient * divisor
>          rem<divisor :  remainder < divisor
> 
> divMod :  (a b : Bin) → b ≢ 0# → DivMod a b
> divMod a b b≢0 =  
>                <-rec _ _ aux
>   where
>   postulate
>     aux :  (a : Bin) → (∀ x → x < a → DivMod x b) → DivMod a b
> ---------------------------------------------------
> 
> 
> Agda 2.5.4 reports
> 
>   (x : Bin) → DivMod x b !=< DivMod a b of type Set
>   when checking that the expression <-rec _ _ aux has type DivMod a b
> 
> Can you, please, tell: how to fix?
> 
> May be one needs to understand the type of  All.wfRec.
> But there it is written something brain-twisting, and it refers the
> Recursor. I searched by `grep', but Recursor is not visible at all
> in /Induction directory, I do not see where it is imported from.
> 


I find now that this version is type-checked:

divMod a b b≢0# =  aux a
  where
  aux :  (a : Bin) → DivMod a b
  aux =  <-rec _ _ aux0
      where
      postulate
       aux0 :  (a : Bin) → (∀ x → x < a → DivMod x b) → DivMod a b

That is I reduce it explicitly to a function of a single argument.
I shall try further.


Thanks again,

------
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