[Agda] splitting cases

[John Leo]

Hi Thorston,

Personally I think this style would be more confusing than helpful. If I
need a local lemma, I just prove it in place using a let statement ("where"
would also be fine). If it's a more general lemma, I just prove it before
the function that uses it. I do this when I teach Agda as well and students
are fine with it. So for your example:

f : Bool → Bool
f true  = true
f false =
 let b : Bool
     b = false
  in b

In general I will have a whole series of variables in the let clause that
represent local lemmas, culminating with the final "in". In fact if I
include the types of each local variable I typically put them on the same
line as the terms and separated by a semicolon which I then line up. This
resembles then the two column proof style ("statements and reasons") from
Euclidean geometry that I learned in high school (sadly not taught anymore)
which I find it the most easy to follow. It's also easy to work with
interactively, filling in the holes as one continues. Here's an example
from the class I'm teaching at Google using Wadler's wonderful text.

_≐_ : ∀ {A : Set} (x y : A) → Set₁
_≐_ {A} x y = ∀ (P : A → Set) → P x → P y

refl-≐ : ∀ {A : Set} {x : A} → ∀ (P : A → Set) → P x → P x --x ≐ x
refl-≐ P Px  =  Px

sym-≐ : ∀ {A : Set} {x y : A} → x ≐ y → y ≐ x
sym-≐ {A} {x} {y} x≐y P =
  let
    Q : A → Set ; Q z = P z → P x
    Qx : Q x    ; Qx = refl-≐ P
    Qy : Q y    ; Qy = x≐y Q Qx
  in Qy

John

On Sat, Mar 28, 2020 at 9:16 AM Thorsten Altenkirch <
Thorsten.Altenkirch at nottingham.ac.uk> wrote:

> Hi,
>
>
>
> I thought we were already able to split cases but it seems I was wrong:
>
>
>
> f : Bool → Bool
>
>
>
> f true = true
>
>
>
> b : Bool
>
> b = false
>
>
>
> f false = b
>
>
>
> doesn’t work. Was this already a feature request? I actually need it
> mostly for pedagogical reasons. I want to prove a theorem, ah I need a
> lemma, let’s prove it and then continue.
>
>
>
> Yes, I know I could use with but this gets to complicated. However,
> splitting cases is also very useful for inductive-inductive definitions.
>
>
>
> Thorsten
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20200328/818ccc8c/attachment.html>