[Agda] `with' in standard functions

Discussion:

Sergei Meshveliani

2017-09-24 11:46:32 UTC

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

Sandro Stucki

2017-09-25 12:32:07 UTC

Permalink

Hi Sergei,

Here's a solution that uses a with clause in the proof (similar to
that in the definition of `fromBits`) and the `inspect` idiom to keep
track of the result of the with clause. There's also a helper lemma to
dispatch some absurd cases. It's not very elegant, and I'm not sure it
will scale to bigger examples, but I hope it's useful to you anyway.

----
open import Data.Bin
open import Data.Digit
open import Data.Fin renaming (suc to 1+_)
open import Data.List
open import Function
open import Relation.Binary.PropositionalEquality
open ≡-Reasoning
open import Relation.Nullary.Negation

-- A helper: lists of bits ending in `1b` do not convert to `0#`.
fromBits-bs++1≠0 : ∀ bs → fromBits (bs ∷ʳ 1b) ≢ 0#
fromBits-bs++1≠0 [] ()
fromBits-bs++1≠0 (b ∷ bs) _
with fromBits (bs ∷ʳ 1b) | inspect fromBits (bs ∷ʳ 1b)
fromBits-bs++1≠0 (zero ∷ bs) _ | 0# | [ eq ] = fromBits-bs++1≠0 bs eq
fromBits-bs++1≠0 (1+ zero ∷ bs) () | 0# | [ _ ]
fromBits-bs++1≠0 (1+ (1+ ()) ∷ bs) _ | 0# | _
fromBits-bs++1≠0 (b ∷ bs) () | bs′ 1# | [ _ ]

fromBits-bs++1 : fromBits ∘ (_∷ʳ 1b) ≗ _1#
fromBits-bs++1 [] = refl
fromBits-bs++1 (b ∷ bs)
with fromBits (bs ∷ʳ 1b) | inspect fromBits (bs ∷ʳ 1b)
fromBits-bs++1 (b ∷ bs) | bs′ 1# | [ eq ] =
helper (begin
bs′ 1# ≡⟨ sym eq ⟩
fromBits (bs ++ (1+ zero) ∷ []) ≡⟨ fromBits-bs++1 bs ⟩
bs 1# ∎)
where
-- Combines injectivity of `_1#` with `cong (_#1 ∘ (b ∷_))`.
helper : ∀ {b bs₁ bs₂} → bs₁ 1# ≡ bs₂ 1# → (b ∷ bs₁) 1# ≡ (b ∷ bs₂) 1#
helper refl = refl
fromBits-bs++1 (zero ∷ bs) | 0# | [ eq ] =
contradiction eq ((fromBits-bs++1≠0 bs))
fromBits-bs++1 (1+ zero ∷ bs) | 0# | [ eq ] =
contradiction eq ((fromBits-bs++1≠0 bs))
fromBits-bs++1 (1+ (1+ ()) ∷ bs) | 0# | _
----

Cheers
/Sandro

Post by Sergei Meshveliani
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
--------------------------------------------------
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
https://lists.chalmers.se/mailman/listinfo/agda

Sergei Meshveliani

2017-09-25 14:56:38 UTC

Permalink

Post by Sandro Stucki
Hi Sergei,
Here's a solution that uses a with clause in the proof (similar to
that in the definition of `fromBits`) and the `inspect` idiom to keep
track of the result of the with clause. There's also a helper lemma to
dispatch some absurd cases. It's not very elegant, and I'm not sure it
will scale to bigger examples, but I hope it's useful to you anyway.
[..]

Thanks to Sandro!

You see, I often occur unlucky when apply `inspect'.

Post by Sandro Stucki
----
open import Data.Bin
open import Data.Digit
open import Data.Fin renaming (suc to 1+_)
open import Data.List
open import Function
open import Relation.Binary.PropositionalEquality
open ≡-Reasoning
open import Relation.Nullary.Negation
-- A helper: lists of bits ending in `1b` do not convert to `0#`.
fromBits-bs++1≠0 : ∀ bs → fromBits (bs ∷ʳ 1b) ≢ 0#
fromBits-bs++1≠0 [] ()
fromBits-bs++1≠0 (b ∷ bs) _
with fromBits (bs ∷ʳ 1b) | inspect fromBits (bs ∷ʳ 1b)
fromBits-bs++1≠0 (zero ∷ bs) _ | 0# | [ eq ] = fromBits-bs++1≠0 bs eq
fromBits-bs++1≠0 (1+ zero ∷ bs) () | 0# | [ _ ]
fromBits-bs++1≠0 (1+ (1+ ()) ∷ bs) _ | 0# | _
fromBits-bs++1≠0 (b ∷ bs) () | bs′ 1# | [ _ ]
fromBits-bs++1 : fromBits ∘ (_∷ʳ 1b) ≗ _1#
fromBits-bs++1 [] = refl
fromBits-bs++1 (b ∷ bs)
with fromBits (bs ∷ʳ 1b) | inspect fromBits (bs ∷ʳ 1b)
fromBits-bs++1 (b ∷ bs) | bs′ 1# | [ eq ] =
helper (begin
bs′ 1# ≡⟨ sym eq ⟩
fromBits (bs ++ (1+ zero) ∷ []) ≡⟨ fromBits-bs++1 bs ⟩
bs 1# ∎)
where
-- Combines injectivity of `_1#` with `cong (_#1 ∘ (b ∷_))`.
helper : ∀ {b bs₁ bs₂} → bs₁ 1# ≡ bs₂ 1# → (b ∷ bs₁) 1# ≡ (b ∷ bs₂) 1#
helper refl = refl
fromBits-bs++1 (zero ∷ bs) | 0# | [ eq ] =
contradiction eq ((fromBits-bs++1≠0 bs))
fromBits-bs++1 (1+ zero ∷ bs) | 0# | [ eq ] =
contradiction eq ((fromBits-bs++1≠0 bs))
fromBits-bs++1 (1+ (1+ ()) ∷ bs) | 0# | _
----
Cheers
/Sandro

Sergei Meshveliani

2017-09-25 16:00:40 UTC

Permalink

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

Nils Anders Danielsson

2017-09-26 08:27:29 UTC

Permalink

Post by Sergei Meshveliani
There is a certain problem with user proofs for Standard library
functions that use `with' or `case_of_'.

I guess that the main problem is when one or more parts of the first
definition cannot be referred to directly in the second definition. Some
examples:

* With. When with is used there is no way to refer directly (without
using unification) to the generated with function. We could perhaps
fix this by parsing with expressions of the form
"f ps | e_1 | ... | e_n".

* Pattern-matching lambdas. Such lambdas are compared by name, but the
name is generated and cannot be written down explicitly in source
code. This could perhaps be fixed by comparing such lambdas by
structure rather than name, but that is a rather big change.

* Local definitions in where clauses. Such definitions are presumably
supposed to be hidden, but can be named if the where clause is named.

--
/NAD

Sergei Meshveliani

2017-09-26 18:09:31 UTC

Permalink

Post by Nils Anders Danielsson

Post by Sergei Meshveliani
There is a certain problem with user proofs for Standard library
functions that use `with' or `case_of_'.

I guess that the main problem is when one or more parts of the first
definition cannot be referred to directly in the second definition. Some
* With. When with is used there is no way to refer directly (without
using unification) to the generated with function. We could perhaps
fix this by parsing with expressions of the form
"f ps | e_1 | ... | e_n".

Can you, please, demonstrate this parsing on a simple example?
Say, on Data.Bin.fromBits.
?

Post by Nils Anders Danielsson
* Pattern-matching lambdas. Such lambdas are compared by name, but the
name is generated and cannot be written down explicitly in source
code. This could perhaps be fixed by comparing such lambdas by
structure rather than name, but that is a rather big change.
* Local definitions in where clauses. Such definitions are presumably
supposed to be hidden, but can be named if the where clause is named.

For example, Data.Bin.fromBits can be written as

fromBits : List Bit → Bin
fromBits [] = 0#
fromBits (b ∷ bs) = aux b bs (fromBits' bs)
where
aux : Bit → Bin → Bin
aux b (bs' 1#) = (b ∷ bs') 1#
aux 0b 0# = 0#
aux 1b 0# = [] 1#
aux ⊥b _

How would this aux be referred from outside?
("fromBits.aux" does not look as concrete enough).

Thanks,

------
Sergei

Nils Anders Danielsson

2017-09-26 19:13:33 UTC

Permalink

Post by Sergei Meshveliani
Can you, please, demonstrate this parsing on a simple example?

Agda currently prints expressions of this form, but does not parse them.

Post by Sergei Meshveliani
How would this aux be referred from outside?

Let's take the following, self-contained example instead:

open import Agda.Builtin.List
open import Agda.Builtin.Nat

F : List Set → Set
F [] = Nat
F (A ∷ As) = B 12
module M where
B : Nat → Set
B zero = A
B (suc n) = A → B n

Here you can refer to the local function B as M.B. Note, however, that
the inferred type of M.B is (A : Set) (As : List Set) → Nat → Set. In
cases like this, where one or more arguments are not used by the local
function and you want to refer to it by name, it may be better to move
it to the top-level than to name the where module.

--
/NAD

Sergei Meshveliani

2017-09-26 19:47:01 UTC

Permalink

Post by Nils Anders Danielsson

Post by Sergei Meshveliani
Can you, please, demonstrate this parsing on a simple example?

Agda currently prints expressions of this form, but does not parse them.

I meant: how will it look the intended parsing result, for a simple
example.

Post by Nils Anders Danielsson

Post by Sergei Meshveliani
How would this aux be referred from outside?

open import Agda.Builtin.List
open import Agda.Builtin.Nat
F : List Set → Set
F [] = Nat
F (A ∷ As) = B 12
module M where
B : Nat → Set
B zero = A
B (suc n) = A → B n
Here you can refer to the local function B as M.B. Note, however, that
the inferred type of M.B is (A : Set) (As : List Set) → Nat → Set. In
cases like this, where one or more arguments are not used by the local
function and you want to refer to it by name, it may be better to move
it to the top-level than to name the where module.

Year or two ago I tried this once. And decided that it is still better
to move it to the top level, even with polluting the top level with
"-aux" functions.

Regards,

------
Sergei

Apostolis Xekoukoulotakis

2017-09-27 12:56:29 UTC

Permalink

I recently had to move a local function to top-level. Previously I used
irrelevance to to disregard the fact that I provide different (in name
only) functions. I was lucky that the function did not use many local
variables.

My main problem with 'with' is the error message. Someone on twitter said
that "Type-driven development allows him to prove things that he wouldn't
be able to do on his own".

When the complexity of the code increases, the 'with' error message does
not increase our ability to handle that complexity. We have to solve things
ourselves.

Post by Sergei Meshveliani

Post by Nils Anders Danielsson

Post by Sergei Meshveliani
Can you, please, demonstrate this parsing on a simple example?

Agda currently prints expressions of this form, but does not parse them.

I meant: how will it look the intended parsing result, for a simple
example.

Post by Nils Anders Danielsson

Post by Sergei Meshveliani
How would this aux be referred from outside?

open import Agda.Builtin.List
open import Agda.Builtin.Nat
F : List Set â Set
F [] = Nat
F (A â· As) = B 12
module M where
B : Nat â Set
B zero = A
B (suc n) = A â B n
Here you can refer to the local function B as M.B. Note, however, that
the inferred type of M.B is (A : Set) (As : List Set) â Nat â Set. In
cases like this, where one or more arguments are not used by the local
function and you want to refer to it by name, it may be better to move
it to the top-level than to name the where module.

Year or two ago I tried this once. And decided that it is still better
to move it to the top level, even with polluting the top level with
"-aux" functions.
Regards,
------
Sergei
_______________________________________________
Agda mailing list
https://lists.chalmers.se/mailman/listinfo/agda

Nils Anders Danielsson

2017-09-27 13:33:13 UTC

Permalink

Post by Sergei Meshveliani
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.

--
/NAD

Sergei Meshveliani

2017-09-28 11:16:16 UTC

Permalink

Post by Nils Anders Danielsson

Post by Sergei Meshveliani
I meant: how will it look the intended parsing result, for a simple
example.

f : {A : Set} → List A → List A
f [] = []
f (x ∷ xs) with xs
... | [] = xs
... | y ∷ ys = x ∷ ys
.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