Question: Can you have `calc` blocks in games?

[lnay]

What is the status of using a calc block in a level?
Is it possible right now (I couldn't find a way to, or see anything in docs)?

[joneugster]

You can state your proof as

Statement ... : ... = yada yada := by
  Template
    Hole
      calc .....

Which will force the user to stay in the "editor mode", i.e where they can freely type in a multi-line editor (there's one sentence about it here). There they can enter anything, even calc-blocks, but the user experience might be less guided.

It's not possible to use calc as a tactic in the "typewriter mode", i.e. where you enter one tactic at a time as you see e.g. in the NNG. In fact it does not support any multi-line tactics at all.

I can recommend using the trans tactic instead of calc, that usually works quite well. (i.e. make trans [the most complicated type in your calc block] and then got on simplifying both new equations.)

[lnay]

Thanks!

[lnay]

@AlexBrodbelt , useful note here on level design

[joneugster]

I'll reuse this issue for anything about calc blocks in games, as it does come up occationally.

Current state: It would require serious modifications to the "Typewriter interface" in order to support calc-blocks in a semi-reasonable way, and it's afaik not on anybody's TODO-list. However, if there is serious interest and somebody wants to work on it, this might be the right place to discuss further details.

[AlexBrodbelt]

I would be happy to work on this, what would I have to do?

[JadAbouHawili]

You can state your proof as

Statement ... : ... = yada yada := by
  Template
    Hole
      calc .....

Which will force the user to stay in the "editor mode", i.e where they can freely type in a multi-line editor (there's one sentence about it here). There they can enter anything, even calc-blocks, but the user experience might be less guided.

Ah, I have a weird work around to make the user experience more guided. Here's an example:

Statement {x : ℤ} (h : x + 2 = 4)
  : x = 2 := by{
  Template
    calc 
      x = x + 2 - 2 := by sorry 
      _ = 4 - 2 := by sorry
      _ = 2 := by sorry
  }

Now, when the user enters the level, there is going to be a sorry tactic not available in this game error. Placing the text cursor before sorry would show you the normal proof state making the level playable. The obvious downside is that this would give off tactic needed but not introduced warnings when building and warnings in your editor. @joneugster , is there a cleaner way or even a 'right' way to do this because this doesn't look like it.

[JadAbouHawili]

This approach would work for more than just calc blocks:

variable {P Q : Prop}
Statement (hP : P) (hQ : Q) : P ∧ Q := by 
  Template
     constructor 
        · sorry
        · sorry

Comments can also clarify each step, serving the function of Hint. Maybe allowing multiple uses of Hole would make this less weird, using Hole in place of sorry. Based on my testing, Hole can only be used once(indicate otherwise if I'm wrong). @joneugster should this go to a new issue?

[joneugster]

Hole should be usable multiple times, that sound like a bug.

[joneugster]

amd if you ever get tactic "sorry" not available thats also a bug.

For your first message, I think you are supposed to put by Hole _ where you have by sorry in your calc block and you should also be able to use Hint there, bit I havent tested that much.

Maybe you can share your wip progress with me privately, then I can use it as a MWE

[JadAbouHawili]

Doing by Hole _ instead of by sorry gives an unsolved goals error, and lake build fails. Instead of _, I can prove the goal and it would work fine.
I'll make a separate pull request regarding calc documentation later.
Here's what the code now looks like(works fine):

Statement {x : ℤ} (h : x + 2 = 4)
  : x = 2 := by{
  Template
    calc 
      x = x + 2 - 2 := by 
        Hole 
        Hint "hint here, works fine"
        ring
      _ = 4 - 2 := by Hole rw [h]
      _ = 2 := by Hole norm_num
  }

Note: Hint doesn't give a syntax error but doesn't seem to be working properly either.
Question: whats wip?

[joneugster]

Instead of _, I can prove the goal and it would work fine.
That's what I meant indeed! Probably want to indent everything inside the Hole:

        Hole 
          Hint "hint here, works fine"
          ring

Note: Hint doesn't give a syntax error but doesn't seem to be working properly either.

I'll look into that!

Question: whats wip?

(it's the abbreviation for Work in Progress)