<div dir="ltr"><div>Something like this, I think:</div><div><br></div>P : Bin 
→ Set <br><div></div><div>P _y = (x : Bin) → Bin <br></div><div><br></div><div>gc :  (y : Bin) → (∀ y' → y' < y → P y') → P y</div><div><br></div><div>then after applying 
<-rec
you get something 
 of type [(y : Bin) 
→ P y], which is just gcd with arguments swapped.</div><div><br></div><div>(I wrote P in a general form so that it's more similar to "dependent" examples, but of course you don't need to)<br></div></div><br><div class="gmail_quote"><div dir="ltr">On Thu, 9 Aug 2018 at 20:40, Sergei Meshveliani <<a href="mailto:mechvel@botik.ru" target="_blank">mechvel@botik.ru</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">Thank you.<br>
After this sample of  downFrom  I was able to program  divMod  for Bin.<br>
But I am stuck with  gcd  for  Bin.<br>
Consider a contrived simple version:<br>
<br>
------------------------------------------------------<br>
postulate<br>
  rem  :  Bin → (y : Bin) → y ≢ 0# → Bin    -- remainder of x by y.<br>
<br>
  rem< :  (x y : Bin) → (y≢0 : y ≢ 0#) → rem x y y≢0 < y<br>
<br>
gcd : Bin → Bin → Bin<br>
gcd x y<br>
      with y ≟ 0#<br>
...   | yes _  =  x<br>
...   | no y≢0 =  gcd y (rem x y y≢0)<br>
<br>
This lacks termination proof.<br>
The argument pair  (x , y)  is replaced in recursion with  (y , r),<br>
where  r < y.  So, it is needed well-founded recursion: <br>
<br>
gcd' : Bin → Bin → Bin<br>
gcd' =  <-rec _ _ gc<br>
  where<br>
  postulate<br>
   gc :  Bin → (b : Bin) → (∀ x y → y < b → Bin) → Bin    -- ??<br>
<br>
<br>
I do not guess what signature to set for  gc.  <br>
I set a hole "?" for  gc,  and the type checker shows<br>
<br>
      Induction.WellFounded.WfRec _<_ (λ _ → Bin → Bin)<br>
      .Relation.Unary._.⊆′ (λ _ → Bin → Bin)<br>
-- ?<br>
<br>
Can anybody help, please?<br>
<br>
Thanks,<br>
<br>
------<br>
Sergei  <br>
<br>
<br>
<br>
On Wed, 2018-08-08 at 17:49 +0200, Sandro Stucki wrote:<br>
> > Can anybody demonstrate it on the following example?<br>
> <br>
> Here you go:<br>
> <br>
> --------------------------------------------------------------<br>
> open import Function   using (_∘_; _on_)<br>
> open import Data.List  using (List; []; _∷_)<br>
> open import Data.Bin   using (Bin; toBits; pred; _<_; less; toℕ)<br>
> open import Data.Digit using (Bit)<br>
> import Data.Nat      as Nat<br>
> import Induction.Nat as NatInd<br>
> open import Induction.WellFounded<br>
> <br>
> open Bin<br>
> <br>
> predBin : Bin → Bin<br>
> predBin = pred ∘ toBits<br>
> <br>
> postulate<br>
>   predBin-< :  (bs : List Bit) -> predBin (bs 1#) < (bs 1#)<br>
> <br>
> -- The strict order on binary naturals implies the strict order on the<br>
> -- corresponding unary naturals.<br>
> <⇒<ℕ : ∀ {b₁ b₂} → b₁ < b₂ → (Nat._<_ on toℕ) b₁ b₂<br>
> <⇒<ℕ (less lt) = lt<br>
> <br>
> -- We can derive well-foundedness of _<_ on binary naturals from<br>
> -- well-foundedness of _<_ on unary naturals.<br>
> <-wellFounded : WellFounded _<_<br>
> <-wellFounded =<br>
>   Subrelation.wellFounded <⇒<ℕ (Inverse-image.wellFounded toℕ<br>
> NatInd.<-wellFounded)<br>
> <br>
> open All <-wellFounded using () renaming (wfRec to <-rec)<br>
> <br>
> downFrom : Bin → List Bin     -- x ∷ x-1 ∷ x-2 ∷ ... ∷ 0# ∷ []<br>
> downFrom = <-rec _ _ df<br>
>   where<br>
>     df : (b : Bin) → (∀ b′ → b′ < b → List Bin) → List Bin<br>
>     df 0#      dfRec = 0# ∷ []<br>
>     df (bs 1#) dfRec = (bs 1#) ∷ (dfRec (predBin (bs 1#)) (predBin-< bs))<br>
> --------------------------------------------------------------<br>
> <br>
> In order to use well-founded induction, we first have to prove that<br>
> the strict order < is indeed well-founded. Thankfully, the standard<br>
> library already contains such a proof for the strict order on (unary)<br>
> naturals as well as a collection of combinators for deriving<br>
> well-foundedness of relations from others (in this case the strict<br>
> order on unary naturals).<br>
> <br>
> The core of the implementation of `downFrom' via well-founded<br>
> recursion is the function `df', which has the same signature as<br>
> `downFrom' except for the additional argument `dfRec', which serves as<br>
> the 'induction hypothesis'. The argument `dfRec' is itself a function<br>
> with (almost) the same signature as `downFrom' allowing us to make<br>
> recursive calls (i.e. take a recursive step), provided we can prove<br>
> that the first argument of the recursive call (i.e. the argument to<br>
> the induction hypothesis) is smaller than the first argument of the<br>
> enclosing call to `df'. The proof that this is indeed the case is<br>
> passed to `dfRec' as an additional argument of type b′ < b.<br>
> <br>
> The following answer on Stackoverflow contains a nice explanation on<br>
> how all of this is implemented in Agda under the hood:<br>
> <a href="https://stackoverflow.com/a/19667260" rel="noreferrer" target="_blank">https://stackoverflow.com/a/19667260</a><br>
> <br>
> Cheers<br>
> /Sandro<br>
> <br>
> <br>
> On Wed, Aug 8, 2018 at 12:13 PM Sergei Meshveliani <<a href="mailto:mechvel@botik.ru" target="_blank">mechvel@botik.ru</a>> wrote:<br>
> ><br>
> > On Tue, 2018-08-07 at 20:51 +0300, Sergei Meshveliani wrote:<br>
> > > Dear all,<br>
> > ><br>
> > > I am trying to understand how to use WellFounded of Standard library.<br>
> > ><br>
> > > Can anybody demonstrate it on the following example?<br>
> > ><br>
> > > --------------------------------------------------------------<br>
> > > open import Function  using (_∘_)<br>
> > > open import Data.List using (List; []; _∷_)<br>
> > > open import Data.Bin  using (Bin; toBits; pred)<br>
> > ><br>
> > > open Bin<br>
> > ><br>
> > > predBin : Bin → Bin<br>
> > > predBin = pred ∘ toBits<br>
> > ><br>
> > > downFrom : Bin → List Bin     -- x ∷ x-1 ∷ x-2 ∷ ... ∷ 0# ∷ []<br>
> > > downFrom 0#      =  0# ∷ []<br>
> > > downFrom (bs 1#) =  (bs 1#) ∷ (downFrom (predBin (bs 1#)))<br>
> > > --------------------------------------------------------------<br>
> > ><br>
> > > downFrom  is not recognized as terminating.<br>
> > > How to reorganize it with using items from<br>
> > > Induction/*, WellFounded.agda ?<br>
> ><br>
> ><br>
> ><br>
> > I presumed also that it is already given the property<br>
> ><br>
> >   postulate<br>
> >     predBin-< :  (bs : List Bit) -> predBin (bs 1#) < (bs 1#)<br>
> ><br>
> > (I do not mean to deal here with its proof).<br>
> ><br>
> > --<br>
> > SM<br>
> ><br>
> ><br>
> > _______________________________________________<br>
> > Agda mailing list<br>
> > <a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br>
> > <a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
> <br>
<br>
<br>
_______________________________________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
</blockquote></div>