[Agda] The proving cycle.

[Andrea Vezzosi]

Most commands that show types can be prefixed with C-u C-u to get the
fully normalized types.

On Thu, Aug 13, 2015 at 11:52 PM, effectfully <effectfully at gmail.com> wrote:
> Hi. That's how I define a recursive function in Agda:
>
> 1) f : {A} -> B -> C -> D
>     f y z = {!!}
>
> 2) Split on `y' or `z'. At this stage Agda often changes code
> formatting and makes e.g.
>
>     f : {A} -> B -> C -> D
>     f {x} y z = {!!}
>
> from
>
>     f : {A} -> B -> C -> D
>     f {x = x} y z = {!!}
>
> I revert these changes.
>
> 3) Look at the context and the type of a term. Very often the context
> and the term are not normalized, and I need to do this manually. Terms
> usually contain implicit arguments, so C-c C-n doesn't work, and I
> have to bind these implicits, again manually.
>
> 4) Remove stuff like (λ {.x} {.y} → ...).
>
> 5) When everything become explicit, I type C-c C-n and sometimes get
> (_42 a dh dfh f sd). Agda doesn't display implicits in terms (as to
> ShowImplicit: [1]), so it's sometimes impossible to meaningfully
> normalize a term without additionally instantiating some implicits,
> which can be non-trivial.
>
> 6) C-c C-r time. Agda again ignores my formatting, so I copy an
> expression, refine the hole, delete the mess that Agda made from my
> code (it sometimes even doesn't typecheck, especially when sections
> are involved: Agda outputs something like (λ .section₀ → .section₀ +
> m)) and paste the untouched expression.
>
> When terms are large the whole process may take up to 20 minutes or
> even more. Then I prove the theorem in 2 minutes.
>
> Am I doing something wrong?
>
> Here are some proposals:
>
> 1) The ability to normalize the type of a term in a context. The
> ability to see the normalized type of a term in a hole (i.e. something
> similar to C-c C-d or C-c C-., but with full normalization). The
> ability to normalize a whole context.
>
> 2) Refine doesn't change formatting.
>
> 3) Something like C-c C-i makes an implicit explicit. I.e. C-c C-i i makes
>
> i : I
> x : A
>
> from
>
> .i : I
> x : A
>
> and inserts a lambda in the appropriate place.
>
> 4) More control on how things are evaluated. I rarely want `map' to be
> unfolded into `replicate' and `_⊛_', but I always want `const', `_∘_',
> `uncurry' and other combinators to be unfolded fully (which can
> probably be a good heuristic on its own).
>
> 5) It would be nice, if it would be possible to declare fixities for
> arguments. Maybe something like (infixl 6 _+_ : ℕ -> ℕ -> ℕ).
>
> I realize that most of these proposals are fairly complex, but I hope
> it's not just me being silly and there are other people that have
> problems with using Agda, when complicated terms are involved. I'd
> also appreciate if someone told me how to make the process of writing
> code in Agda more straightforward.
>
> Thanks for the attention.
>
> [1] http://lpaste.net/138758
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda