<div dir="ltr">s/(x : X) â†’ P a/(x : X) â†’ P x/</div><br><div class="gmail_quote"><div dir="ltr">On Fri, 10 Aug 2018 at 14:05, Arseniy Alekseyev <<a href="mailto:arseniy.alekseyev@gmail.com">arseniy.alekseyev@gmail.com</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="ltr">Two things:<div><br></div><div>1.</div><div>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.</div><div>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):</div><div>P : Bin â†’ Set</div><div>P a = (b : Bin) â†’ GCD a b</div><div><br></div><div>2. Giving P explicitly can help improve error messages a lot. You can try something like this:</div><div><span class="gmail-im" style="color:rgb(80,0,80)">gcd =  <-rec _ P gc</span><br></div><div><span class="gmail-im" style="color:rgb(80,0,80)"><br></span></div><div><span class="gmail-im" style="color:rgb(80,0,80)">I haven't look in much detail so maybe this is not actually helpful. Sorry if it's not.</span></div><div><br></div><div><br></div><div><font color="#500050">> </font>WellFounded recursion thing is also available directly for the signature of </div><div>> gcd : (a b : Bin) â†’ GCD a b,</div><div><br></div><div>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.</div></div><br><div class="gmail_quote"><div dir="ltr">On Fri, 10 Aug 2018 at 13:35, Sergei Meshveliani <<a href="mailto:mechvel@botik.ru">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">On Fri, 2018-08-10 at 14:36 +0300, Sergei Meshveliani wrote:<br>
> On Thu, 2018-08-09 at 23:15 +0100, Arseniy Alekseyev wrote:<br>
> > Something like this, I think:<br>
> > <br>
> > <br>
> > P : Bin â†’ Set <br>
> > <br>
> > P _y = (x : Bin) â†’ Bin <br>
> > <br>
> > <br>
> > <br>
> > gc :  (y : Bin) â†’ (∀ y' â†’ y' < y â†’ P y') â†’ P y<br>
> > <br>
> > <br>
> > then after applying <-rec you get something of type [(y : Bin) â†’ P y],<br>
> > which is just gcd with arguments swapped.<br>
> > <br>
> > <br>
> > (I wrote P in a general form so that it's more similar to "dependent"<br>
> > examples, but of course you don't need to)<br>
> > <br>
> <br>
> <br>
> <br>
> Thank you. <br>
> This works with the result of  Bin.<br>
> I try to extend this to  Â <br>
>  Â  Â  Â  Â  Â  Â  Â  Â  Â  Â  gcd : (a b : Bin) -> GCD a b,<br>
> and fail.<br>
> <br>
<br>
<br>
Below  Â  Â  Â r<x = rem< x y x≢0<br>
was a typo,<br>
it needs to be replaced with  r<x = rem< y x x≢0.<br>
<br>
But this  does not change the report of Agda.<br>
<br>
<br>
Another attempt<br>
===============<br>
<br>
I change the signatures to  <br>
<br>
------------------------------------------<br>
BB = Bin Ã— Bin<br>
<br>
_<p_ :  Rel BB Level.zero<br>
_<p_ =  _<_ on proj₁<br>
<br>
open import Induction.WellFounded using (WellFounded)<br>
<br>
postulate  <p-wellFounded : WellFounded _<p_<br>
<br>
open All <p-wellFounded using () renaming (wfRec to <-rec)<br>
<br>
record GCD (pr : BB) : Set  Â -- contrived<br>
  Â  Â  Â where<br>
  Â  Â  Â constructor gcd′<br>
  Â  Â  Â a = proj₁ pr<br>
  Â  Â  Â b = projâ‚‚ pr<br>
<br>
  Â  Â  Â field  res  Â  Â  Â : Bin<br>
  Â  Â  Â  Â  Â  Â  divides-a : âˆƒ (\q â†’ res * q â‰¡ a)<br>
  Â  Â  Â  Â  Â  Â  divides-b : âˆƒ (\q â†’ res * q â‰¡ b)<br>
  Â  Â  Â  Â  Â  Â  -- and maximality axiom<br>
<br>
gcd : (pr : BB) â†’ GCD pr<br>
----------------------------------------------<br>
<br>
Now  gcd  is  on  Bin Ã— Bin,  and your approach works,<br>
the code is type-checked: <br>
<br>
gcd =  <-rec _ _ gc<br>
  where<br>
  gc :  (pr : BB) â†’ (∀ pr' â†’ pr' <p pr â†’ GCD pr') â†’ GCD pr<br>
  gc (x , y) gcRec<br>
  Â  Â  Â  Â  Â  Â with x â‰Ÿ 0#<br>
<br>
  ... | no x≢0 =  f<br>
  Â  Â  Â  Â  Â  Â  Â  Â  where<br>
  Â  Â  Â  Â  Â  Â  Â  Â  f : GCD (x , y)<br>
  Â  Â  Â  Â  Â  Â  Â  Â  f = liftGCD (gcRec (r , x) r<x)<br>
  Â  Â  Â  Â  Â  Â  Â  Â  Â  Â  where<br>
  Â  Â  Â  Â  Â  Â  Â  Â  Â  Â  r  Â = rem y x x≢0<br>
  Â  Â  Â  Â  Â  Â  Â  Â  Â  Â  r<x = rem< y x x≢0<br>
<br>
  Â  Â  Â  Â  Â  Â  Â  Â  Â  Â  postulate  liftGCD : GCD (r , x) â†’ GCD (x , y)<br>
  ... | ...<br>
-------------------------------------------------<br>
<br>
<br>
All right:  I can convert from  GCD-auxiliary (a , b)  <br>
to  Â  Â  Â  Â  Â  Â  Â  Â  Â  Â  Â  Â  Â  Â  GCD a b.<br>
<br>
But I have an impression that the WellFounded recursion thing is also<br>
available directly for the signature of<br>
<br>
  Â  Â  Â  Â  gcd : (a b : Bin) â†’ GCD a b,<br>
<br>
only am missing something.<br>
-- ?<br>
<br>
Regards,<br>
<br>
------<br>
Sergei<br>
<br>
<br>
<br>
<br>
<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>
> <br>
> record GCD (a b : Bin) : Set  Â -- contrived<br>
>  Â  Â  Â  where<br>
>  Â  Â  Â  constructor gcd′<br>
> <br>
>  Â  Â  Â  field  res  Â  Â  Â : Bin<br>
>  Â  Â  Â  Â  Â  Â  Â divides-a : âˆƒ (\q â†’ res * q â‰¡ a)<br>
>  Â  Â  Â  Â  Â  Â  Â divides-b : âˆƒ (\q â†’ res * q â‰¡ b)<br>
>  Â  Â  Â  Â  Â  Â  Â --<br>
>  Â  Â  Â  Â  Â  Â  Â -- and maximality axiom<br>
> <br>
> -- Without using termination proof:<br>
> --<br>
> {-# TERMINATING #-}<br>
> gcd : (a b : Bin) â†’ GCD a b<br>
> gcd x y<br>
>  Â  Â  Â with x â‰Ÿ 0#<br>
> ...  Â | yes x≡0 =  gcd′ y (0# , y*0≡x) (1# , y*1≡y)<br>
>  Â  Â  Â  Â  Â  Â  Â  Â  Â  where<br>
>  Â  Â  Â  Â  Â  Â  Â  Â  Â  postulate  y*0≡x : y * 0# â‰¡ x<br>
>  Â  Â  Â  Â  Â  Â  Â  Â  Â  Â  Â  Â  Â  Â  Â y*1≡y : y * 1# â‰¡ y<br>
> <br>
> ...  Â | no x≢0 =  Â liftGCD (gcd r x)<br>
>  Â  Â  Â  Â  Â  Â  Â  Â  Â  where<br>
>  Â  Â  Â  Â  Â  Â  Â  Â  Â  r = rem y x x≢0<br>
> <br>
>  Â  Â  Â  Â  Â  Â  Â  Â  Â  postulate  liftGCD : GCD r x â†’ GCD x y<br>
> ---------------------------------------------------------------<br>
> <br>
> The second argument is divided by the first one in the loop -- this way<br>
> it is easier to use.<br>
> <br>
> This is type-checked.<br>
> <br>
> Now try WellFounded. As I understand, the approach is to reduce to a<br>
> function of a single argument:<br>
> <br>
> --------------------------------------------------------------- <br>
> gcd : (a : Bin) â†’ GCD a<br>
> gcd =  <-rec _ _ gc<br>
>  Â where<br>
>  Â gc :  (x : Bin) â†’ (∀ x' â†’ x' < x â†’ GCD x') â†’ GCD x<br>
>  Â gc x gcRec<br>
>  Â  Â  Â  with x â‰Ÿ 0#<br>
>  Â ...  | yes x≡0 =  f<br>
>  Â  Â  Â  Â  Â  Â  Â  Â  Â  Â where<br>
>  Â  Â  Â  Â  Â  Â  Â  Â  Â  Â f : GCD x<br>
>  Â  Â  Â  Â  Â  Â  Â  Â  Â  Â f y =  gcd′ y (0# , y*0≡x) (1# , y*1≡y)<br>
>  Â  Â  Â  Â  Â  Â  Â  Â  Â  Â  Â  Â  Â  where<br>
>  Â  Â  Â  Â  Â  Â  Â  Â  Â  Â  Â  Â  Â  postulate y*0≡x : y * 0# â‰¡ x<br>
>  Â  Â  Â  Â  Â  Â  Â  Â  Â  Â  Â  Â  Â  Â  Â  Â  Â  Â  y*1≡y : y * 1# â‰¡ y<br>
> <br>
>  Â ...  | no x≢0 =  f<br>
>  Â  Â  Â  Â  Â  Â  Â  Â  Â  where<br>
>  Â  Â  Â  Â  Â  Â  Â  Â  Â  f : GCD x<br>
>  Â  Â  Â  Â  Â  Â  Â  Â  Â  Â  Â  Â  f y = liftGCD (gcRec r r<x x)<br>
>  Â  Â  Â  Â  Â  Â  Â  Â  Â  Â  Â  Â  Â  Â  Â  where<br>
>  Â  Â  Â  Â  Â  Â  Â  Â  Â  Â  Â  Â  r  Â = rem y x x≢0<br>
>  Â  Â  Â  Â  Â  Â  Â  Â  Â  Â  Â  Â  Â  Â  Â  r<x = rem< x y x≢0<br>
> <br>
>  Â  Â  Â  Â  Â  Â  Â  Â  Â  Â  Â  Â  postulate  liftGCD : GCD r x â†’ GCD x y<br>
> ---------------------------------------------------------------<br>
> <br>
> Agda type-checks the function  gc, <br>
> but it reports that  (<-rec _ _ gc)  does not return a value of the type<br>
> GCD a.<br>
> <br>
> Then I try <br>
> <br>
>  gcd :  Bin â†’ (Bin â†’ Set)<br>
>  gcd =  <-rec _ _ gc<br>
>  Â where<br>
>  Â postulate <br>
>  Â  Â gc :  (x : Bin) â†’ (∀ x' â†’ x' < x â†’ Bin â†’ Set) â†’ Bin â†’ Set<br>
>  <br>
> (which goal adequacy I do not understand). <br>
> It is type-checked,<br>
> but I fail to implement this version of gc.<br>
> <br>
> Can anybody advise, please?<br>
> <br>
> ------<br>
> Sergei <br>
> <br>
> <br>
> <br>
> <br>
> > On Thu, 9 Aug 2018 at 20:40, Sergei Meshveliani <<a href="mailto:mechvel@botik.ru" target="_blank">mechvel@botik.ru</a>><br>
> > wrote:<br>
> > <br>
> >  Â  Â  Â  Â Thank you.<br>
> >  Â  Â  Â  Â After this sample of  downFrom  I was able to program  divMod<br>
> >  Â  Â  Â  Â 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<br>
> >  Â  Â  Â  Â 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<br>
> >  Â  Â  Â  Â (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>
> >  Â  Â  Â  Â <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>
> >  Â  Â  Â  Â --------------------------------------------------------------<br>
> >  Â  Â  Â  Â > open import Function  Â using (_∘_; _on_)<br>
> >  Â  Â  Â  Â > open import Data.List  using (List; []; _∷_)<br>
> >  Â  Â  Â  Â > open import Data.Bin  Â using (Bin; toBits; pred; _<_; less;<br>
> >  Â  Â  Â  Â 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<br>
> >  Â  Â  Â  Â 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<br>
> >  Â  Â  Â  Â from<br>
> >  Â  Â  Â  Â > -- well-foundedness of _<_ on unary naturals.<br>
> >  Â  Â  Â  Â > <-wellFounded : WellFounded _<_<br>
> >  Â  Â  Â  Â > <-wellFounded =<br>
> >  Â  Â  Â  Â >  Â Subrelation.wellFounded <⇒<â„• (Inverse-image.wellFounded<br>
> >  Â  Â  Â  Â 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>
> >  Â  Â  Â  Â []<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#))<br>
> >  Â  Â  Â  Â (predBin-< bs))<br>
> >  Â  Â  Â  Â ><br>
> >  Â  Â  Â  Â --------------------------------------------------------------<br>
> >  Â  Â  Â  Â > <br>
> >  Â  Â  Â  Â > In order to use well-founded induction, we first have to<br>
> >  Â  Â  Â  Â prove that<br>
> >  Â  Â  Â  Â > the strict order < is indeed well-founded. Thankfully, the<br>
> >  Â  Â  Â  Â standard<br>
> >  Â  Â  Â  Â > library already contains such a proof for the strict order<br>
> >  Â  Â  Â  Â on (unary)<br>
> >  Â  Â  Â  Â > naturals as well as a collection of combinators for deriving<br>
> >  Â  Â  Â  Â > well-foundedness of relations from others (in this case the<br>
> >  Â  Â  Â  Â strict<br>
> >  Â  Â  Â  Â > order on unary naturals).<br>
> >  Â  Â  Â  Â > <br>
> >  Â  Â  Â  Â > The core of the implementation of `downFrom' via<br>
> >  Â  Â  Â  Â well-founded<br>
> >  Â  Â  Â  Â > recursion is the function `df', which has the same signature<br>
> >  Â  Â  Â  Â as<br>
> >  Â  Â  Â  Â > `downFrom' except for the additional argument `dfRec', which<br>
> >  Â  Â  Â  Â serves as<br>
> >  Â  Â  Â  Â > the 'induction hypothesis'. The argument `dfRec' is itself a<br>
> >  Â  Â  Â  Â function<br>
> >  Â  Â  Â  Â > with (almost) the same signature as `downFrom' allowing us<br>
> >  Â  Â  Â  Â to make<br>
> >  Â  Â  Â  Â > recursive calls (i.e. take a recursive step), provided we<br>
> >  Â  Â  Â  Â can prove<br>
> >  Â  Â  Â  Â > that the first argument of the recursive call (i.e. the<br>
> >  Â  Â  Â  Â argument to<br>
> >  Â  Â  Â  Â > the induction hypothesis) is smaller than the first argument<br>
> >  Â  Â  Â  Â of the<br>
> >  Â  Â  Â  Â > enclosing call to `df'. The proof that this is indeed the<br>
> >  Â  Â  Â  Â case is<br>
> >  Â  Â  Â  Â > passed to `dfRec' as an additional argument of type b′ < b.<br>
> >  Â  Â  Â  Â > <br>
> >  Â  Â  Â  Â > The following answer on Stackoverflow contains a nice<br>
> >  Â  Â  Â  Â 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<br>
> >  Â  Â  Â  Â <<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<br>
> >  Â  Â  Â  Â wrote:<br>
> >  Â  Â  Â  Â > > > Dear all,<br>
> >  Â  Â  Â  Â > > ><br>
> >  Â  Â  Â  Â > > > I am trying to understand how to use WellFounded of<br>
> >  Â  Â  Â  Â Standard library.<br>
> >  Â  Â  Â  Â > > ><br>
> >  Â  Â  Â  Â > > > Can anybody demonstrate it on the following example?<br>
> >  Â  Â  Â  Â > > ><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 âˆ· ... âˆ·<br>
> >  Â  Â  Â  Â 0# âˆ· []<br>
> >  Â  Â  Â  Â > > > downFrom 0#  Â  Â  =  0# âˆ· []<br>
> >  Â  Â  Â  Â > > > downFrom (bs 1#) =  (bs 1#) âˆ· (downFrom (predBin (bs<br>
> >  Â  Â  Â  Â 1#)))<br>
> >  Â  Â  Â  Â > > ><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<br>
> >  Â  Â  Â  Â 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>
> <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>
</blockquote></div></blockquote></div>