Disable all simp lemmas

Stream: lean4

[Jon Eugster]

In the MWE below, when defining MyNat, it automatically creates a simp-lemma MyNat.succ.injEq. Is there a way to disable this feature, i.e. to have a completely empty simp-set and only add things manually? This is for a learning game and I would like simp to become successively stronger after each level.

I can do attribute [-simp] MyNat.succ.injEq, but when importing the definition in a different file, it seems that the attribute is back. Maybe there is a way to remove the attribute globally for all files importing this one, too?

inductive MyNat where
| zero : MyNat
| succ : MyNat → MyNat

attribute [-simp] MyNat.succ.injEq

example (a b : MyNat) (h : (MyNat.succ a) = b) : MyNat.succ (MyNat.succ a) = MyNat.succ b := by
  simp -- should not make progress
  sorry

[Kevin Buzzard]

I know that in Lean 3 it was impossible to unsimp a lemma globally when it was simped -- core lean had sub_eq_add_neg as a simp lemma for years and it drove the mathlib community nuts but there was nothing we could do about it until the lean 3 fork.

[Jannis Limperg]

Jon Eugster said:

I can do attribute [-simp] MyNat.succ.injEq, but when importing the definition in a different file, it seems that the attribute is back. Maybe there is a way to remove the attribute globally for all files importing this one, too?

This is not possible with the current implementation of attributes. (The notation should probably reflect this: local attribute [-simp] ... would be more suggestive.) I don't see a way to keep injEqs out of the simp set short of overriding the inductive command. If you can tell simp not to use the default simp set (which I don't know), you could override simp with a variant that uses only some custom simp set.

[Jon Eugster]

That's okay, thanks! In that case I don't have to spend time trying ;)
For the game, I can just remove it for the few levels manually until it's been proven.

[Kevin Buzzard]

How about you define MyNat_aux inductively and then define MyNat to equal MyNat.aux and move over precisely the lemmas which you want?

In the natural number game I tell lies. The thing I say is tactic mode is not tactic mode, it's a modified tactic mode where tactics do different things. I found it quite difficult to do things without telling lies, because Lean is optimised for getting things done, not for education. Another possibility is that you could modify simp to be your own simp with your own simp set, or just make a new tactic simpl or whatever.

[Jon Eugster]

Redefining one of the things is indeed what I would do, I already redefined several other tactics, but if there would have been an easy way to nuke all simp lemmas, that would have been the easiest.

Btw, it's exactly about the NNG. As a second test-game I ported it to our lean4 game engine:

https://adam.math.hhu.de/#/game/nng

I was going to dm you, @Kevin Buzzard, shortly about that

[Heather Macbeth]

@Jon Eugster @Alexander Bentkamp the game engine looks great, so pretty and click-y! Congrats!

[Heather Macbeth]

You probably are aware, but there are still various bits of un-translated German. ("bisheriger beweis", "aktuelles goal")

[Jon Eugster]

Yes, that's exactly what Im doing now:+1: And I'd want an option to load new games from separate github repos.

And... the server does probably only handle about 10-14ppl at any time🫢

consider it an inofficial pre-release

[Patrick Massot]

It looks great! I'm super happy that my experiment from last summer turned into this, and I can't wait to discuss it with you and the rest of the team in Düsseldorf!

[Kevin Buzzard]

This really looks like it has a lot of potential. Mohammad and I just threw something together because we knew Imperial students enjoyed playing the game at Xena when I set it up on their computers. The material is in the course which I teach to the 1st years, and the game was just a Xena thing at first. Then Mohammad suggested we get it online somehow, told me what Lean files he wanted, and did everything else himself. It was never supposed to be more than a demo in some sense, the github repo is full of issues but I figure if it ain't broke then what the heck (the real issue is that I don't have a clue how to compile and deploy it , I just have to relearn every time from all the readmes because I'm old and stupid), and I don't remember my own code really.

[Johan Commelin]

Jon Eugster said:

https://adam.math.hhu.de/#/game/nng

This looks really great!

One tiny bit of feedback. (Maybe it isn't even NNG specific, and more directed at Lean 4 in general.) If you hover over an expression like a + 0, then you get a pop-up which starts with

@HAdd.hAdd ℕ ℕ ℕ instHAdd a 0 : ℕ

(The same happens in VSCode.)

I think this looks quite intimidating.

[Jon Eugster]

Johan Commelin said:

I think this looks quite intimidating.

Doesn't it? Right now it just shows the same pop-ups as it would in VsCode

[Kevin Buzzard]

Which is intimidating (to me, and I'm supposed to be an expert).

[Peter Nelson]

Jon Eugster said:

Btw, it's exactly about the NNG. As a second test-game I ported it to our lean4 game engine:

https://adam.math.hhu.de/#/game/nng

This is fun!

There is a typo in the latex above add_mul.

[Jon Eugster]

Thx!