Level 5 / 7 : Rewriting on the final world (World: Redux: ↔ World Tactics) on "A Lean Intro to Logic" and general feedback

[joneugster]

A report by @awefhio originally posted at leanprover-community/lean4game#232.

I got stuck on Level 5 / 7 : Rewriting on the final world (World: Redux: ↔ World Tactics).

Can't think of anything to use "apply" on , and no alternative ideas due to limited tactics. I admit I might be missing something very obvious but it's out of my reach, although I'd still like to check whether it's a problem with the level.

Overall speaking, I feel like the logic game is much less polished than the natural number game and the set theory game (which I both completed). Particularly compared to the set theory game, many similar theorems have inconsistent names (e.g. And.intro vs and_intro).

The instructions also is confusing at times, I don't find the analogies particularly helpful, but I can understand if they're aimed at a less experienced audience, yet the levels themselves seem to assume a familiarity with lambda calculus. I think it'll be much more helpful if the learning curve on lambda notation can be smoothed out.

[Trequetrum]

This brings up some points that have been on my mind for a while.

1: The play testers I watched play this game never played the Natural Numbers or Set Theory Game. Early on, I saw it helped play testers when I remove the way Lean does namespace resolution so we're never in the situation where some theorems are separated by dots and some by underscores. I'm not sure if this is the best choice in the long run as people who are familiar with Mathlib/Natutal Number Game/Set Theory Game may come in with other expectations.

2: The flavor text isn't really helpful in finding a solution. It can give context around the logical operators (though even this can be tenuous), which helps a bit with players who have never done any formal logic. It's sort of how intro to logic textbooks do it, right? Even so, you have to learn to write terms as evidence and the flavor text isn't helpful there. I think the flavor text can more or less stand on its own merits, though to do so convincingly it could use some improvements. It would probably also help to have some way to signal which text is there for fun and which is meant to be instructive.

3: The level you got stuck on is way too long. It doesn't require any steps/tricks a player wouldn't have seen on earlier levels. I've seen play-testers who have had zero exposure to Lean other than Intro to Logic complete the level. So it's not broken, but it's not good either. Rather than feeling accomplished when you make it to the end, I can imagine you may well just feel tired. I've been toying with the idea of removing the redux worlds.

---

I think it'll be much more helpful if the learning curve on lambda notation can be smoothed out.

I'll think about this. My experience with play-testers has been that they get to the right expression without having any idea that they're sort of doing lambda calculus. They think about the lambda terms directly as evidence for the propositions (with no regard for the runtime behavior of functions calls or anything like that). In many ways, I guess it's a static, non-computational view of what's happening.

I don't know if that's a good or a bad thing. Certainly it can get you through the logic game, but it feels pretty limiting. Getting the right balance here is certainly something worth spending some more effort on.

[ArnoStrouwen]

I also got stuck on the same equivalence tactics level. Specifically, the apply and_left required on line 6 of the proof. I don't remember that being used anywhere else in the game. The concept of synthetic hole could use some additional explanation.

[ThijsVromen]

My experience with play-testers has been that they get to the right expression without having any idea that they're sort of doing lambda calculus. They think about the lambda terms directly as evidence for the propositions (with no regard for the runtime behavior of functions calls or anything like that). In many ways, I guess it's a static, non-computational view of what's happening.

I agree with this, however I felt that was pretty frustrating. I don't have any lambda calculus experience so I was kind of "just using it". But because of that, in more difficult levels I sometimes felt like I lacked insight to correctly apply it, or sometimes I tried something that "suddenly worked" without fully understanding why.

I also agree that this level 5/7 could really do with some extra hints or something. I see that it is intended as a tedious level (which is in my opinion fine). Instead I found it incredibly difficult in comparison to the other levels, probably because I did not realise I could use certain tactics in ways I hadn't done before? In the end I made it work, but that required writing single lines like:
apply λ h => mp_1 (λ h1 => h (λ h2 r => h1 ⟨λ p => or_elim (h2.left p) (λq => or_inl q) (λ nr => or_inr (λ s => nr (mpr s))), λsp => or_elim sp (λ s => h2.right (or_inl (mpr s))) (λ p => h2.right (or_inr p))⟩ (mp r))) at a which felt a little ridiculous.
(I still don't know how I would've been able to split that up into something simpler, so advice on that is very welcome. Or maybe there are model solutions somewhere I haven't seen?)

To end on a more positive note, overall I enjoyed the game and especially in many cases also the redux levels! I thought it was really neat to see how some of the tactics introduced there can make the process of writing these proofs so much easier than without.

[vltanh]

You can find the model solution in the source code