[Agda] `with' in standard functions

[Sergei Meshveliani]

On Wed, 2017-09-27 at 15:33 +0200, Nils Anders Danielsson wrote:
> On 2017-09-26 21:47, Sergei Meshveliani wrote:
> > I meant: how will it look the intended parsing result, for a simple
> > example.
> 
> Consider the following code:
> 
>    f : {A : Set} → List A → List A
>    f []       = []
>    f (x ∷ xs) with xs
>    ... | []     = xs
>    ... | y ∷ ys = x ∷ ys
> 
> This is expanded into something like the following:
> 
>    .f-aux : {A : Set} → A → List A → List A → List A
>    .f-aux x xs []       = xs
>    .f-aux x xs (y ∷ ys) = x ∷ ys
> 
>    f : {A : Set} → List A → List A
>    f []       = []
>    f (x ∷ xs) = .f-aux x xs xs
> 
> The idea is that the expression f (x ∷ xs) | ys would stand for
> .f-aux x xs ys.
> 


For example,  Data.Bin  has

fromBits : List Bit → Bin
fromBits []        = 0#
fromBits (b  ∷ bs) with fromBits bs
fromBits (b  ∷ bs) | bs′ 1# = (b ∷ bs′) 1#
fromBits (0b ∷ bs) | 0#     = 0#
fromBits (1b ∷ bs) | 0#     = [] 1#
fromBits (⊥b ∷ bs) | _

And a proof for 
      fromBits-bs++1 :  fromBits ∘ (_∷ʳ 1b) ≗ _1#

will be possible as 
-------------------------------
fromBits-bs++1 []       =  refl
fromBits-bs++1 (b ∷ bs) =
  begin
   fromBits ((b ∷ bs) ∷ʳ 1b)                          ≡⟨ refl ⟩
   fromBits (b ∷ (bs ∷ʳ 1b))                          ≡⟨ refl ⟩
   fromBits (b ∷ (bs ∷ʳ 1b)) | fromBits (bs ∷ʳ 1b)                   --
                                   ≡⟨ cong prefix0 (fromBits-bs++1 bs) 
                                    )
   fromBits (b ∷ (bs ∷ʳ 1b)) | bs 1#      ≡⟨ refl ⟩     -- 
   (b ∷ bs) 1#
  ∎
  where
  prefix0 = (fromBits (b ∷ (bs ∷ʳ 1b)) |_)    --
-------------------------------

Right?

If so, than this looks good. Because less helper functions will appear
on the top level.

Can this "_|_" be implemented?

As to 'where', any algorithm can be rewritten with eliminating `where'
by introducing top level helpers. I do not know, may be, these helpers
can be somehow rewritten to the `with' construct ... 
?

Thanks,

------
Sergei