New game posted on Lean Game Server (Knights And Knaves)

Stream: general

[Eric Taucher]

Was just taking a look at Lean Game Server (https://adam.math.hhu.de/) and noticed a new game - Reasoning.

Hopefully this is not a repost of old news, checked but did not find a topic.

Have not tried it but do plan to try it.

Thanks.

[Edward van de Meent]

from the looks of it, the game is incomplete

[Edward van de Meent]

particularly, world 3 level 6 asks you to use a lemma which you don't have access to

[Edward van de Meent]

there is a solution tho:

Spoiler

exact (fun | .inl h => (notleft h).elim | .inr h => h) Or

this made me stretch my lean-fu

[Jon Eugster]

the game is by @Jad Abou Hawili, and I'm sure they are happy to get this sort of feedback to eliminate any bugs and inconsisencies.:blush:

(and it's linked since yesterday, so not old news at all!)

[Kevin Buzzard]

I think I would be tempted to set up some domain-specific theorems behind the scenes such as predicates IsKnight A, IsKnave A, and proofs of IsKnight A -> \not IsKnave A, IsKnight A \or IsKnave A etc and just give them to the reader rather than say "actually these are members of something called a finset and it's all about intersections"

[Jon Eugster]

I'll copy-paste some suggestions I DMed here, too, this inclues also an explicit example for this IsKnight suggestion:

suggestions

• you have quite a lot of theorems under [anonymous]. You should probably move them all into Logic by adding more of these TheoremDoc notleft_right as "notleft_right" in "Logic"
• If you dislike editor mode for have, you could import Mathlib.Tactic.Have which allows have a : 2 = 2 to be written without the := by [proof]
• Was there a deliberate reason you've chosen to not introduce anything like apply? I found that I solved "and"s now with exact And.intro [expr1] [expr2] and I would have liked to do

apply And.intro
-- thinking/reading about what comes here...
assumption
-- thinking again...
assumption

• was there any decision process to chose Knight : Finset K and A ∈ Knight over making Knight a structure (or class)

structure Inhabitant : Type

structure Knight (A : Inhabitant) : Prop
structure Knave (A : Inhabitant) : Prop

variable (A B : Inhabitant)

/-
Knight A ∧ Knave A → Knight B : Prop
-/
#check Knight A ∧ Knave A → Knight B

[Kevin Buzzard]

(I'm assuming @Jad Abou Hawili is reading this thread): I would also be highly tempted to introduce notation for "said" e.g. -->, so A --> P would be the proposition "person A said proposition P" and then again you could have theorems (which you would just give to the player, not ask them to prove) knight_says : Knight A -> A --> P -> P and knave_says : Knave A -> A --> P -> \not P. With your current set-up levels like https://adam.math.hhu.de/#/g/jadabouhawili/knightsandknaves-lean4game/world/KnightsAndKnaves/level/2 look super-confusing. Hypotheses h, h1 and h2 should not be clogging up the assumptions because they are global throughout the game; if a user wants to do a case split on whether A is a knight or a knave they can just do cases on IsKnight A \or IsKnave A or, even better, just give them a bespoke tactic person_cases A rather than forcing them to continually jump through hoops. Also "B said that A said they're a knave" has been translated into the highly complex

stB: B ∈ Knight ↔ (A ∈ Knight ↔ A ∈ Knave)
stBn: B ∈ Knave ↔ ¬(A ∈ Knight ↔ A ∈ Knave)

whereas with my suggestion it would simply be hB : B --> (A --> IsKnave A).

[Kevin Buzzard]

In short I'm wondering whether you can just do away completely with all the earlier levels and jump straight into the game, with literally the first levels of the game being things like "A is a knight. A says that B is a knave. Prove B is a knave" and never mentioning finsets or anything like that.

[Jad Abou Hawili]

Sorry for the useless game title, ill change it.

• Regarding '-->':
  While i was working on the game, it felt like i was handling the semantics of the knights knaves puzzles 'manually'. I was bothered by this but didn't have an idea how to fix it.
  Heres an example:
  A : I am a Knight or B is a Knave.
  Here, i would have to translate the statement to lean and make sure that:

A ∈ Knight -> ...

where ... is the translated statement.
If i made a mistake while doing this, then the puzzle violates the rules.
With your suggestion, its doing it once right and not worrying about it. Also, having the fact that knights tell the truth is a theorem seems a lot more impactful than repeating it over and over.

• Regarding h ,h1 clogging the assumptions: I acknowledged this during development, but did not have a better way so this is what i went with.
• Regarding the ugly translation, I acknowledged this as well but a solution did not occur to me as well.

Most of your complaints have already occurred to my mind, just without your solutions and suggestions.
I will take your post to heart and make some improvements.

Could you elaborate more on person_cases tactic and the --> implementation wise? Would appreciate a relevant link or some pointers on that.

Thanks for the feedback.

[Jad Abou Hawili]

Kevin Buzzard said:

I think I would be tempted to set up some domain-specific theorems behind the scenes such as predicates IsKnight A, IsKnave A, and proofs of IsKnight A -> \not IsKnave A, IsKnight A \or IsKnave A etc and just give them to the reader rather than say "actually these are members of something called a finset and it's all about intersections"

Thought about this and did it , but hated it. The IsKnight, IsKnave thing is useless. In 'Knights and Knaves, Second approach', setup is

A : Prop

The semantics here are that A being true means that A is a knight, not A means A is a knave. I liked this because excluded middle would be equivalent to A being a knight or a knave.

Seemed more natural so i went with that instead.

Also, i was afraid of going too heavy into lean stuff i.e making my own datatype, structure, notation etc.. I didn't feel confident enough with them to include them in the game and explain them properly so i went with the finset approach because its familiar set theory. Also, even though its called a knights and knaves game , i was torn between going into logic and set theory and this was the result :joy:

[Kevin Buzzard]

One of the hardest parts of making a new game is having the right idea. I have had many lousy ideas about games, basically the natural number game is the only game I could get other people interested in. I think the knights and knaves is a great idea for a game. Here is a primitive way of setting things up:

import Mathlib

-- hide all this from the user

axiom Islander : Type

namespace Islander

axiom IsKnight : Islander → Prop

axiom IsKnave : Islander → Prop

axiom isKnight_or_isKnave (A : Islander) : A.IsKnight ∨ A.IsKnave

axiom not_isKnight_and_isKnave (A : Islander) : ¬ (A.IsKnight ∧ A.IsKnave)

axiom Said : Islander → Prop → Prop

-- number affects where brackets will be needed
notation A " said " P:200 => Said A P
infixr:35 " and " => And
infixr:30 " or  "  => Or

axiom knight_said {A : Islander} {P : Prop} : (A said P) → A.IsKnight → P

axiom knave_said {A : Islander} {P : Prop} : A said P → A.IsKnave → ¬ P

section tactics

-- I don't know how to get this stuff working but it looks something like this
-- and an expert will be able to fix this up in 10 seconds flat

-- Attempt to make `knight_or_knave A with hA hA` work:

syntax "knight_or_knave " term " with " term term : tactic

-- doesn't work though
-- macro_rules |
--   `(tactic| knight_or_knave A with h1 h2) => `(tactic| obtain h1 | h2 := isKnight_or_isKnave A)

end tactics

end Islander

open Islander

-- Easy example
/-
A is a knight. A says that B is a knave. Prove that B is a knave.
-/
example {A B : Islander} (hA : A.IsKnight) (hAB : A said B.IsKnave) : B.IsKnave := by
  exact knight_said hAB hA

/-
A : I am a Knave or B is a Knave.
-/
example {A B : Islander} (hAB : A said (A.IsKnave or B.IsKnave)) : A.IsKnight and B.IsKnave := by
  obtain hA | hA := A.isKnight_or_isKnave
  · obtain hA' | hB := knight_said hAB hA
    · exact (not_isKnight_and_isKnave A ⟨hA, hA'⟩).elim
    · exact ⟨hA, hB⟩
  · have := knave_said hAB hA
    tauto

As you can see, the functionality is there, there are no sets or elements, the statements of the examples are really really easy to understand, a schoolchild could understand them (and you should be targetting schoolchildren which is another reason to avoid set notation). The proofs are awful because they need more thought and I need to do other things. But once you or someone else have decided what you want the proofs to look like, you just make your own domain-specific tactics, like I wrote my own domain-specific axioms, and the game plays like that.

[Eric Taucher]

@Jad Abou Hawili

Just want to say thanks for creating the game. I'll know it will get better with time. :smile:

[Eric Taucher]

@Kevin Buzzard

Again what you thank you for starting with the first game but more importantly at this time for giving useful feedback on how to make improvements when creating a game.

I did a few of the games last week just to see if I could use it with the Equational Theories Project (Zulip Channel) (Dashboard) and your game was the most polished of them all. When I first did the Numbers game with Lean 3 I was not able to finish it, after finding the the Lean game server and seeing that it has been updated, it was actually enjoyable. :smile:

[Jad Abou Hawili]

Eric Taucher said:

Jad Abou Hawili

Just want to say thanks for creating the game. I'll know it will get better with time. :smile:

Thanks for noticing :joy: . Things got to the point where I felt like I couldn't improve the game so i decided to upload it and hope for feedback. Wasn't expecting it to be directly after the game got to the main page.

Also, it feels nice talking to people other than my brother and collaborator on the project.

[Jad Abou Hawili]

I am slowly going through all the feedback i got, and will quote and comment on each one

[Jad Abou Hawili]

@Jon Eugster says
" If you dislike editor mode for have, you could import Mathlib.Tactic.Have which allows have a : 2 = 2 to be written without the := by [proof]"

syntax of have is:

have [some-name] : [some-prop] := by [proof]

I did not want the user to write this in one go because its weird, so i forced editor mode where have was already written with a sorry that needed to be filled, concrete example:

  have  AinInter : A ∈ left ∩ right:=by sorry

Yes I disliked this but it was the best solution I knew, I like your suggestion more because it allows for the following:

have.png

have2.png

have3.png

This is much cleaner compared to:
have4.png

Using sorry in the image above is weird, doing hints is weird.

I didn't know you could 'postpone' the proof in a have statement but now I do. Thanks for the tip.

[Kevin Buzzard]

yeah we use this trick in NNG. A lot of users would ask "I don't want to prove the goal I'm supposed to be proving, I want to prove something else first" and the answer in NNG is "just write have h3 : what_you_want" and lo and behold you have a new goal, you're still in tactic mode, your goal is what you want, and once you've proved it you'll have a new hypothesis h3 : what_you_want on the old goal (as I just realised you noted above). It's very easy to explain.

[Jad Abou Hawili]

Kevin Buzzard said:

axiom Islander : Type

namespace Islander

@Kevin Buzzard
I think some of what you did here should be mentioned in the official documentation of lean4game. Maybe a heading called "Decluttering the proof state" or "Hiding clutter". All I did was the following:

axiom Inhabitant : Type
namespace Inhabitant

and this removed the pesky Inhabitant : Type u_1 from the users view, its no longer listed under objects.

inh1.png

inh2.png

[Jad Abou Hawili]

@Jon Eugster thoughts?

[Jad Abou Hawili]

i would have to do this for every file in the game, is there an easier way?

[Kevin Buzzard]

Note that if you use my IsKnight idea then you'll also get rid of DecidableEq and Finset

[Jon Eugster]

Jad Abou Hawili said:

I think some of what you did here should be mentioned in the official documentation of lean4game.

That's certainly true, although I doubt I'll be the person to write instructions on how to use Lean. If somebidy want to PR a new .md file to lean4game/doc/ I'll happily merge that.

[Jon Eugster]

Jad Abou Hawili said:

i would have to do this for every file in the game, is there an easier way?

Whatever your final setup is, you should probably do that in a preliminary file which is imported in each level. I think the sample game already has Metadata.lean as such a file, so you can define your axioms in there, don't you?:blush:

[Kevin Buzzard]

Yes in NNG we unsurprisingly import the natural numbers in each level :-) but in fact what we do is import each level in the next one, which works fine

[Jad Abou Hawili]

Kevin Buzzard said:

import Mathlib

-- hide all this from the user

axiom Islander : Type

namespace Islander

axiom IsKnight : Islander → Prop

axiom IsKnave : Islander → Prop

axiom isKnight_or_isKnave (A : Islander) : A.IsKnight ∨ A.IsKnave

axiom not_isKnight_and_isKnave (A : Islander) : ¬ (A.IsKnight ∧ A.IsKnave)

axiom Said : Islander → Prop → Prop

-- number affects where brackets will be needed
notation A " said " P:200 => Said A P
infixr:35 " and " => And
infixr:30 " or  "  => Or

axiom knight_said {A : Islander} {P : Prop} : (A said P) → A.IsKnight → P

axiom knave_said {A : Islander} {P : Prop} : A said P → A.IsKnave → ¬ P

section tactics

-- I don't know how to get this stuff working but it looks something like this
-- and an expert will be able to fix this up in 10 seconds flat

-- Attempt to make `knight_or_knave A with hA hA` work:

--syntax "knight_or_knave " term " with " term term : tactic

-- doesn't work though
-- macro_rules |
--   `(tactic| knight_or_knave A with h1 h2) => `(tactic| obtain h1 | h2 := isKnight_or_isKnave A)
macro "knight_or_knave" t1:term "with" t2:rcasesPat t3:rcasesPat : tactic => do`(tactic| obtain ($t2 | $t3) := isKnight_or_isKnave $t1)


end tactics

end Islander

open Islander

-- Easy example
/-
A is a knight. A says that B is a knave. Prove that B is a knave.
-/
example {A B : Islander} (hA : A.IsKnight) (hAB : A said B.IsKnave) : B.IsKnave := by
  exact knight_said hAB hA

/-
A : I am a Knave or B is a Knave.
-/
example {A B : Islander} (hAB : A said (A.IsKnave or B.IsKnave)) : A.IsKnight and B.IsKnave := by
  knight_or_knave A with hA hA
  --obtain hA | hA := A.isKnight_or_isKnave
  · obtain hA' | hB := knight_said hAB hA
    · exact (not_isKnight_and_isKnave A ⟨hA, hA'⟩).elim
    · exact ⟨hA, hB⟩
  · have := knave_said hAB hA
    tauto

fixed the custom tactic.

it seems like im going to lean(not a pun) into this direction, and maybe ill move the set theory stuff into a separate world that is optional.

also looking into eliminating A.isKnight A.isKnave , and just having A not A.

[Jad Abou Hawili]

also, the setup only needs 4 axioms which are :

IsKnight
IsKnave
isKnight_or_isKnave
not_isKnight_and_isKnave

mirroring the finset setup(there's a correspondence that can be made)

[Jad Abou Hawili]

Jon Eugster said:

Jad Abou Hawili said:

i would have to do this for every file in the game, is there an easier way?

Whatever your final setup is, you should probably do that in a preliminary file which is imported in each level. I think the sample game already has Metadata.lean as such a file, so you can define your axioms in there, don't you?:blush:

@Jon Eugster
Right, right.
If i define an axiom say knight_said, i can use it in all the levels. However, I can't do NewTheorem knight_said and put some documentation there, I could define it as a theorem where the proof is sorry but that's weird. Is there a way around this? Specifically, a NewTheorem thing that works for axiom not just theorem

Doing NewTheorem knight_said fails, but NewTheorem Islander.knight_said works.

[Kevin Buzzard]

Don't I do this for eg add_zero in NNG?

[Jad Abou Hawili]

ill take a look, also it seems just declaring an axiom in Metadata.lean makes it available in lean files, but not the actual game.(namespace issue)

[Jad Abou Hawili]

Kevin Buzzard said:

Don't I do this for eg add_zero in NNG?

yes, you did NewTheorem MyNat.add_zero, the namespace has to be included for some reason for it to work.

[Jad Abou Hawili]

@Kevin Buzzard
The ugly statements

stB: B ∈ Knight ↔ (A ∈ Knight ↔ A ∈ Knave)
stBn: B ∈ Knave ↔ ¬(A ∈ Knight ↔ A ∈ Knave)

are not so ugly anymore

theorem dsl_iamknave (hAKn : A said A.isKnave): False := by
  knight_or_knave A with hA hnA
  · have hnA := knight_said hAKn hA
    #check not_isKnight_and_isKnave
    apply @not_isKnight_and_isKnave A
    constructor
    assumption ; assumption
  · have hnA := knave_said hAKn hnA
    contradiction

example {A B C : Islander}
{hB : B said (A said A.isKnave)}
{hC : C said B.isKnave}
: B.isKnave and C.isKnight := by
  have BKnave : B.isKnave
  -- need to introduce apply in this game
  apply notisKnight_isKnave
  intro BKnight
  have hA := knight_said hB BKnight
  exact dsl_iamknave hA

  constructor
  assumption

  have CKnight := said_knight hC BKnave
  assumption

I'll credit you in the 'acknowledgments' section.
Thank you so much for the feedback.

[Kevin Buzzard]

This looks great! Definitely apply is very useful, although experience with NNG tells me that even though it's second-nature to many of us, beginners hugely struggle with the goal-changing tactic apply which is why I introduced the hypothesis-changing tactic apply at in NNG, which everyone finds much easier.