search

UlfNorell / agda-test

Agda test
0 stars 0 forks source link

how to reduce code repetition in `with' branches #913

Closed UlfNorell closed 10 years ago

UlfNorell commented 10 years ago

From mech...@botik.ru on September 27, 2013 21:29:45

This is for Agda-2.3.2 MAlonzo, with lib-0.7.

The code is small, it is attached.

Its function power

returns the power x^e in a Semigroup by applying the binary method.

The function comm-with-power

proves x ∙ x^e ≈ x^e ∙ x for x : Carrier.

comm-with-power has two branches of with' in the last clause. Thesewith' branches have a relatively large repeated code segment (for pp∙x=x∙pp and some other).

How to re-implement comm-with-power so that to reduce this code repetition ?

Instead of this last with' I tried 1)case', 2) introducing a new function.

Both variants are not type-checked.

The example is simple and small. Can you, please, demonstrate how to reduce the code repetition?

Original issue: http://code.google.com/p/agda/issues/detail?id=913

UlfNorell commented 10 years ago

From mech...@botik.ru on September 28, 2013 02:46:12

The improved Power.agda in the second attached archive has the with' branches with fully identic large repeating code. The questions are the same: 1) how to plainly rewrite thiswith' into a) `case', b) new introduced function ? 2) if (1) is possible, then how to reduce the code segment repetition?

Attachment: power.zip

UlfNorell commented 10 years ago

From andreas....@gmail.com on September 28, 2013 06:44:44

Analogous to the filter example I gave on the mailing list, while you can define power with case, reasoning about power needs with, because even? e needs to be abstracted in the goal.

The where-definitions can be shared if you define them before you do the 'with'-split. In your case, it is sufficient to define a helper, comm, which is then with-split. See attached file.

So, there is no Agda bug. The Agda list is a better forum for such questions.

Status: Invalid
Owner: andreas....@gmail.com

Attachment: Power.agda

UlfNorell commented 10 years ago

From mech...@botik.ru on September 28, 2013 10:00:01

Thank you. It works. Earlier, I also tried a helper function, but I tried it in a bit different way:

             = comm (even? e)
     where
     ...
     comm (yes _) = ...
     ...

And this was not type-checked.