[Agda] `with' in standard functions

[Sergei Meshveliani]

Dear Agda developers,

Proofs by using the `inspect' construct are difficult to compose,
the thing is unclear, leads to complications.
When a function does not use `with' nor 'cade_of_', it is much easier to
write proofs for it.

Am I the only one who thinks so?

---------------------------------
In 2013 I had a talk on CICM-2013, and in the questions part someone
asked me 
"Really, do you write proofs in Agda ? Personally I cannot write proofs
in Agda !".

He had exclaimed this with a suffer. I had an impression that he really
knew of what he was talking about. 
(And some proofs in my program for algebra had the `postulate' stubs).
I answered something like this 

"There are some difficulties, I have not enough experience, I need to
see further.
Anyway, what language or system do you suggest for writing these proofs
for programming algebra? Is it Coq ?
"

He thought a bit, and had not said anything. So, I thought that all
tools bring difficulties.

I suspect now, that the problem was in proofs for the functions using
the constructs of `with' or case_of, which lead to unclear complications
caused by the `inspect' construct.

If this was today, I would answer
"A proof is not difficult to write in Agda -- when the function is free
of the constructs of `with' and case_of_, and soon as an intuitive
constructive proof is ready. And it is not difficult to program any
algorithm without using these constructs".

As I convert by hand any function to the form free of `with' and
case_of_, may be, this can be done automatically, and so that `inspect'
would not be necessary?

What people think of this?

Regards,

------
Sergei



On Sun, 2017-09-24 at 14:46 +0300, Sergei Meshveliani wrote:
> People,
> 
> There is a certain problem with user proofs for Standard library
> functions that use `with' or `case_of_'.  
> If a function is written without `with' (`with' replaced with calling an
> auxiliary function  aux, and this  aux  is exported from the module),  
> then it is much easier to compose various new proofs about it.
> 
> But the user cannot change implementation for a standard function. 
> 
> For example,  Data.Bin  implements 
> 
> -------------------------
> 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) | _
> -------------------------
> 
> I need to prove 
> 
>           fromBits-bs++1 :  fromBits ∘ (_∷ʳ 1b) ≗ _1#
> 
> And find it difficult.
> Then I get free of `with', and a proof becomes plain and easy to
> compose:
> 
> --------------------------------------------------
> fromBits-aux : Bit → List Bit → Bin → Bin    -- needs to be exported
> 
> fromBits-aux b  bs (bs' 1#) = (b ∷ bs') 1#
> fromBits-aux 0b bs 0#       = 0#
> fromBits-aux 1b bs 0#       = [] 1#
> fromBits-aux ⊥b bs _
> 
> fromBits' : List Bit → Bin
> fromBits' []       = 0#
> fromBits' (b ∷ bs) = fromBits-aux b bs (fromBits' bs)
> 
> 
> fromBits-bs++1 :  fromBits' ∘ (_∷ʳ 1b) ≗ _1#
> fromBits-bs++1 []       =  refl
> fromBits-bs++1 (b ∷ bs) =
>   begin
>     fromBits' (b ∷ (bs ∷ʳ 1b))                        ≡⟨ refl ⟩
>     fromBits-aux b (bs ∷ʳ 1b) (fromBits' (bs ∷ʳ 1b))
>        	       	       	       	    ≡⟨ cong (fromBits-aux b (bs ∷ʳ 1b))
>                                             (fromBits-bs++1 bs)
>                                      ⟩
>     fromBits-aux b (bs ∷ʳ 1b) (bs 1#)  	       	      ≡⟨ refl ⟩
>     (b ∷ bs) 1#
>   ∎
> ---------------------------------------------------
> 
> Please, what is a way out?
> 
> Thanks,
> 
> ------
> Sergei
> 
> 
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda