<div dir="ltr"><div>Hi Thorston,</div><div><br></div><div>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:</div><div><br></div><div><font face="monospace">f : Bool → Bool<br>f true  = true<br>f false =<br> let b : Bool<br>     b = false<br>  in b</font><br></div><div><br></div><div>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.</div><div><br></div><div><font face="monospace">_≐_ : ∀ {A : Set} (x y : A) → Set₁<br>_≐_ {A} x y = ∀ (P : A → Set) → P x → P y<br><br>refl-≐ : ∀ {A : Set} {x : A} → ∀ (P : A → Set) → P x → P x --x ≐ x<br>refl-≐ P Px  =  Px<br><br>sym-≐ : ∀ {A : Set} {x y : A} → x ≐ y → y ≐ x<br>sym-≐ {A} {x} {y} x≐y P =<br>  let<br>    Q : A → Set ; Q z = P z → P x<br>    Qx : Q x    ; Qx = refl-≐ P<br>    Qy : Q y    ; Qy = x≐y Q Qx<br>  in Qy</font><br></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">John</div><div dir="ltr" class="gmail_attr"><br></div><div dir="ltr" class="gmail_attr">On Sat, Mar 28, 2020 at 9:16 AM Thorsten Altenkirch <<a href="mailto:Thorsten.Altenkirch@nottingham.ac.uk" target="_blank">Thorsten.Altenkirch@nottingham.ac.uk</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">





<div lang="EN-GB">
<div>
<p class="MsoNormal"><span style="font-size:11pt">Hi,<u></u><u></u></span></p>
<p class="MsoNormal"><span style="font-size:11pt"><u></u> <u></u></span></p>
<p class="MsoNormal"><span style="font-size:11pt">I thought we were already able to split cases but it seems I was wrong:<u></u><u></u></span></p>
<p class="MsoNormal"><span style="font-size:11pt"><u></u> <u></u></span></p>
<p class="MsoNormal"><span style="font-size:11pt">f : Bool → Bool<u></u><u></u></span></p>
<p class="MsoNormal"><span style="font-size:11pt"><u></u> <u></u></span></p>
<p class="MsoNormal"><span style="font-size:11pt">f true = true<u></u><u></u></span></p>
<p class="MsoNormal"><span style="font-size:11pt"><u></u> <u></u></span></p>
<p class="MsoNormal"><span style="font-size:11pt">b : Bool<u></u><u></u></span></p>
<p class="MsoNormal"><span style="font-size:11pt">b = false<u></u><u></u></span></p>
<p class="MsoNormal"><span style="font-size:11pt"><u></u> <u></u></span></p>
<p class="MsoNormal"><span style="font-size:11pt">f false = b<u></u><u></u></span></p>
<p class="MsoNormal"><span style="font-size:11pt"><u></u> <u></u></span></p>
<p class="MsoNormal"><span style="font-size:11pt">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.
<u></u><u></u></span></p>
<p class="MsoNormal"><span style="font-size:11pt"><u></u> <u></u></span></p>
<p class="MsoNormal"><span style="font-size:11pt">Yes, I know I could use with but this gets to complicated. However, splitting cases is also very useful for inductive-inductive definitions.
<u></u><u></u></span></p>
<p class="MsoNormal"><span style="font-size:11pt"><u></u> <u></u></span></p>
<p class="MsoNormal"><span style="font-size:11pt">Thorsten</span></p></div></div>
</blockquote></div></div>