feat(archive/logic_puzzles): add "Knights and knaves" and "Lady or the tiger?"

[stanescuUW]

---

[robertylewis]

@stanescuUW , thanks for the contribution.

I'll admit, I find these formalizations to be very cryptic. I know most of these puzzles and still had to think hard to map the Lean code to the informal statements. Characters are free; there's no need to use random letters for names when you can make them more descriptive.

IMO, the mathlib archive is intended for "show-off" formalizations, things that won't have dependencies but make for nice demos. The content here fits, but I'm not sure about the presentation. I'd love to see this in idiomatic Lean, documented with lots of comments, so that newcomers can follow what's going on.

Content-wise: while there's certainly a correspondence to the informal puzzles, I'm not sure it's so natural. Your definition of person says "there are two people, a knight and a knave." In Q1, Jack's statement says "Jack is Bob." "Knight" and "knave" sound more naturally like predicates on a type person, with jack : person and bob : person.

[stanescuUW]

@robertylewis I totally agree with your comment, Rob. It seems, however, that this PR has gotten caught in crossfire between the terseness requirements in mathlib and the need for extensive elaboration for these puzzles to be legible. Not sure how to resolve this yet. It may be better to close this PR for now and reopen after an extensive rewrite.

[sgouezel]

The terseness requirements in mathlib are mostly for the proofs, but comments and explanations can be as long as you want. Higher comment/code ratio is almost always good!

[robertylewis]

Yeah, I wouldn't say that mathlib has terseness requirements. Personally I look for proofs that are (1) maintainable, (2) efficient, and (3) elegant, in that order. There's a correlation with "short" in all of these, but it's far from perfect.

In particular, the mathlib naming conventions can be very verbose. Descriptive names help maintainability (and even more, help users discover and use declarations) and have no effect on efficiency or elegance.

Similarly for comments, I think the only terseness requirement is that you shouldn't write so much it's hard to keep updated, and nothing in mathlib is near that point yet.

The discovery concerns about names don't really really apply in the archive, since these results aren't expected to be used. But this just gives even more freedom to pick names that relate to the source material.

It may be better to close this PR for now and reopen after an extensive rewrite.

Up to you. We have plenty of PRs that have been sitting open for a while waiting for refactoring. If you think you'll come back to it relatively soon, feel free to leave it open.

[stanescuUW]

@robertylewis @sgouezel @bryangingechen @semorrison My mention of terseness was not about the comments but about the fact that I had left in the file proofs of the style:

lemma answer_tactic : q.H → q.1 = n ∧ q.2 = y :=
begin
  rcases q with ⟨_|_,_|_⟩,
  simp [H], simp [D1], simp [D2],
  simp[H], simp [D1], simp [D2],
  simp [H], 
  simp [H], simp [D1], simp [D2], 
  done
end

alongside proofs of the style:

lemma answer_term : q.H → q.1 = n ∧ q.2 = y :=
  by rcases q with ⟨_|_,_|_⟩; simp [H, D1, D2]

I thought the first would be beneficial for beginners as they can see the state change after each comma. But mathlib style may require that I remove some of those. Please advise.

I have made quite some changes throughout, including descriptions of the puzzles, spacing etc. Again, please let me know if anything else is needed.

[jcommelin]

@stanescuUW If you have dealt with some comments and think they are resolved, please feel free to click "Resolve conversation" to indicate that you are done.

[semorrison]

Why introduce q : Q1 at all? You could just have variables (Joe Bob : islander) in each namespace, I think.

[stanescuUW]

This is somehow the same question as before. I'd say it's just a matter of choice.

[semorrison]

Okay, but I think this may be part of what @robertylewis meant when he said "I'd love to see this in idiomatic Lean,". Perhaps we can see what he thinks?

[urkud]

When I introduced structure Q and (q : Q1) in my son's file, my goal was to use q.S1 instead of S1 Joe Bob, and I wanted this in order to save him some keystrokes (he can't type fast yet).

In case of knights and knaves I think that we should have something like islander.says (i : islander) (p : Prop) := cond (i = knight) p (not p), then use Joe.says and Bob.says.

I wonder whether we can use some fintype magic to ask Lean to list all possible answers.

[stanescuUW]

@semorrison I incorporated the changes you requested. Please review.

[semorrison]

@semorrison I incorporated the changes you requested. Please review.

Great, I'll have a look! It's helpful if PR owners change the labels from "changes-requested" back to "request-review" as well --- often I decide what to look at on the list of PRs page solely based on these tags.

[bryangingechen]

@semorrison I incorporated the changes you requested. Please review.

Great, I'll have a look! It's helpful if PR owners change the labels from "changes-requested" back to "request-review" as well --- often I decide what to look at on the list of PRs page solely based on these tags.

Dan might not have permission to change the labels yet. I'll send him an invite to the repo so that he can. @stanescuUW this will also allow you to create branches in this repo; future PRs should be made from branches in this repo (as opposed to a fork) so that we can more easily see whether the commits build.

[robertylewis]

@semorrison pinged me in a line comment, but I'll address it here, since my points are more general. I still have concerns about this PR, centered around my earlier comment,

Content-wise: while there's certainly a correspondence to the informal puzzles, I'm not sure it's so natural. Your definition of person says "there are two people, a knight and a knave." In Q1, Jack's statement says "Jack is Bob." "Knight" and "knave" sound more naturally like predicates on a type person, with jack : person and bob : person.

The interesting part of a formalization like this, to me, isn't the proofs. They're all induction, simp, basic logic. The interest is in seeing how the informal puzzles translate to a formal setting. When this translation is done with cryptic names, nonstandard encodings, etc, I kind of lose track of the purpose of the project.

My point about cryptic names is indeed connected to Scott's question

Why introduce q : Q1 at all? You could just have variables (Joe Bob : islander) in each namespace, I think.

The type duplication Q1 := Q is confusing and has no semantic connection to the informal puzzle. Why the y and n notations? Why the names D1, D2, H, S1, ... for propositions?

As I wrote before, the entire islander problem setup doesn't really match the informal situation.

inductive islander
| knight
| knave

says that "there are exactly two islanders, one is a knight and one is a knave." Not "There is an island where all inhabitants are either knights or knaves." Joe's statement def S1 := q.Joe = n ∧ q.Bob = n implies q.Joe = q.Bob. Not that they're both knaves, but that they're both the same, unique, knave. The "knights lie, knaves tell the truth" fact is encoded separately in each question; in Smullyan, this is an axiom of the whole scenario, and it would be nice to see it represented like that here.

I'm not saying that this doesn't model the Smullyan puzzle in some way. But there's distance between them.

I'm also not sure that this belongs in the archive in the first place. The archive is used for "show-off" formalizations, projects that are noteworthy in some way that we don't want to bit rot but that don't fit in the main library. If this were a crystal clear tutorial about modeling logic puzzles in Lean, sure. The style standards there would be even higher than the main library.

Note that these files barely use mathlib at all, only the rcases tactic which could easily be avoided. Maybe a better home would be a separate repo of logic puzzles in Lean, maintained by whoever is interested with whatever standards they want. Since it only uses very basic features of Lean, this formalization won't bit rot.

I'm sorry to sound negative about this and I don't mean to discourage you. But IMO there's quite a bit of work done to get this into shape for the archive.