barber paradox

Stream: general

[Cameron Crossman]

Can someone please help me with the barber paradox proof in lean?

[Cameron Crossman]

theorem barber_paradox : ¬ (∀ x : men, shaves barber x ↔ ¬ shaves x x)

[Andrew Ashworth]

Do you have a specific question?

[Chris Hughes]

https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Logic.20.26.20Proof

[Abhimanyu Pallavi Sudhir]

theorem barber_paradox : ¬ (∀ x : men, shaves barber x ↔ ¬ shaves x x)

See barber_is_dead (and a tactic mode proof above it) here: https://github.com/abhimanyupallavisudhir/lean/blob/master/logic_theorems.lean

[Kevin Buzzard]

Ha ha are you revising Cantor's theorem :-)

[Kevin Buzzard]

I don't think you need to be classical for pants on fire. I had to prove this in cantor at the end

[Kevin Buzzard]

example (P : Prop) (Q : Prop) : ¬ P → (P → Q) := by intros;contradiction etc. Your instinct as a mathematician is to case split, but it's often not necessary. Not that this matters (at least not that it matters to us mathematicians...)

[Norbert Bátfai]

I am enthusiastic because I have recently read Kevin Buzzard’s article: When will computers prove theorems? I really liked the comparison of LaTeX and Lean from the point of view of the progress of mathematics. Now I have already started to get acquainted with the language of Lean. I am working on an informatically-philosophically inspired manuscript in which I would like to put a Lean proof. I chose the Barber Paradox. Partly based on the conversations here, I have made a proof and would like to ask that is it correct?

variables (Man : Type) (shaves : Man → Man → Prop)
theorem NoSuchBarber ( h : ∃ x : Man,  ∀ y : Man, shaves x y ↔ ¬ shaves y y )
: false :=
    exists.elim h
  ( assume barber,
    begin
        intro h,
        have hbarbermpr : ¬shaves barber barber → shaves barber barber,
            from iff.mpr (h barber),
        have hbarbermp  : shaves barber barber → ¬shaves barber barber,
            from iff.mp (h barber),
        have nsbb : ¬shaves barber barber, from
            assume sbb : shaves barber barber,
            show false, from hbarbermp sbb sbb,
        show false, from nsbb (hbarbermpr nsbb)
    end
)
#print NoSuchBarber

[Kenny Lau]

Norbert Bátfai said:

is it correct?

The whole point of Lean is that you can ask Lean if it's correct. If there are no errors, then it's correct.

[Kyle Miller]

(assuming you formalized the statement correctly)

[Eric Wieser]

Could save two lines in your manuscript with:

have hbarber : ¬shaves barber barber ↔ shaves barber barber,
    from h barber,

and then use hbarber.mpr instead of hbarbermpr below

[Scott Morrison]

well, you could save more than that :-)

[Eric Wieser]

Oh, for sure :)

[Chris Wong]

I guess it comes down to context. If the purpose of the code snippet is to demonstrate Lean to a lay audience, then having all the intermediate steps spelled out can be helpful. But someone writing for mathlib – whose audience is experienced Lean programmers – would use a much terser style.

[Kevin Buzzard]

import tactic

variables (Man : Type) (shaves : Man → Man → Prop)
theorem NoSuchBarber ( h : ∃ x : Man,  ∀ y : Man, shaves x y ↔ ¬ shaves y y )
: false :=
    exists.elim h
  ( assume barber,
    begin
        intro h2, -- I don't want two hypotheses called h
        have hbarber := h2 barber, -- human-generated good idea
        tauto!, -- computer can finish it off
    end
)

[Kevin Buzzard]

but of course this teaches you far less :-)

[Norbert Bátfai]

Thanks, so the proof is really nicer:

variables (Man : Type) (shaves : Man → Man → Prop)
theorem NoSuchBarber ( h : ∃ x : Man,  ∀ y : Man, shaves x y ↔ ¬ shaves y y )
: false :=
    exists.elim h
  ( assume barber,
    begin
        intro h,
        have hbarber : shaves barber barber ↔ ¬shaves barber barber,
            from h barber,
        have nsbb : ¬shaves barber barber, from
            assume sbb : shaves barber barber,
            show false, from hbarber.mp sbb sbb,
        show false, from nsbb (hbarber.mpr nsbb)
    end
)
#print NoSuchBarber

[Kevin Buzzard]

variables (Man : Type) (shaves : Man → Man → Prop)
theorem NoSuchBarber : ¬ (∃ x : Man,  ∀ y : Man, shaves x y ↔ ¬ shaves y y ) :=
λ ⟨x, hx⟩, (not_iff_self _).1 (hx x).symm

[Kevin Buzzard]

That's the mathlib proof

[Norbert Bátfai]

Kevin Buzzard said:

import tactic

variables (Man : Type) (shaves : Man → Man → Prop)
theorem NoSuchBarber ( h : ∃ x : Man,  ∀ y : Man, shaves x y ↔ ¬ shaves y y )
: false :=
    exists.elim h
  ( assume barber,
    begin
        intro h2, -- I don't want two hypotheses called h
        have hbarber := h2 barber, -- human-generated good idea
        tauto!, -- computer can finish it off
    end
)

Thanks, your tactical proof is amazing. I am a newbie, but for me, it shows very well the power of the interactive nature of Lean.

[Kevin Buzzard]

import tactic

variables (Man : Type) (shaves : Man → Man → Prop)
theorem NoSuchBarber : ¬ (∃ x : Man,  ∀ y : Man, shaves x y ↔ ¬ shaves y y ) :=
begin
  rintros ⟨barber, h2⟩,
  have hbarber := h2 barber,
  library_search,
end

Here's a proof discovered by a computer after the good idea is input.

[Kevin Buzzard]

I cannot get the computer to have the good idea itself :-(

[Ruben Van de Velde]

Going the manual way:

variables (Man : Type) (shaves : Man → Man → Prop)
theorem NoSuchBarber ( h : ∃ x : Man,  ∀ y : Man, shaves x y ↔ ¬ shaves y y )
: false :=
exists.elim h
  ( λ barber h,
    have hbarber : shaves barber barber ↔ ¬shaves barber barber := h barber,
    have nsbb : ¬shaves barber barber := λ sbb, hbarber.mp sbb sbb,
    nsbb (hbarber.mpr nsbb))
#print NoSuchBarber

[Chris Wong]

@Kevin Buzzard a bit unfortunate that tauto (without the !) doesn't work, since the manual proof seems to be constructive :pensive:

[Kenny Lau]

@Norbert Bátfai here's your code minimally modified to follow the spacing conventions (indent with 2 spaces, no space after opening bracket and before closing bracket, don't start a line with a punctuation except brackets), and also to remove the use of tactic mode (your proof does not actually need tactic mode):

theorem NoSuchBarber (Man : Type) (shaves : Man → Man → Prop)
  (h : ∃ x : Man, ∀ y : Man, shaves x y ↔ ¬shaves y y) :
  false :=
exists.elim h $
  assume barber : Man,
  assume h : ∀ y : Man, shaves barber y ↔ ¬shaves y y,
    have hbarbermpr : ¬shaves barber barber → shaves barber barber,
      from iff.mpr (h barber),
    have hbarbermp  : shaves barber barber → ¬shaves barber barber,
      from iff.mp (h barber),
    have nsbb : ¬shaves barber barber, from
      assume sbb : shaves barber barber,
      show false, from hbarbermp sbb sbb,
    show false, from nsbb (hbarbermpr nsbb)

[Norbert Bátfai]

Chris Wong said:

I guess it comes down to context. If the purpose of the code snippet is to demonstrate Lean to a lay audience, then having all the intermediate steps spelled out can be helpful. But someone writing for mathlib – whose audience is experienced Lean programmers – would use a much terser style.

I am interested in the case of "lay audience". Because I am looking for the opportunity to desing a First Ordel Logic-based game. My idea is for players to formalize their relationships and everyday activities. Until recently I have been thinking about a combination of FOL and Prolog, but now I really liked the Lean.

[Chris Wong]

Sounds great! I assume you've heard of the Natural Number Game? Perhaps you can reuse the infrastructure for that.

[Norbert Bátfai]

Thanks, and yes, I have played with it. From the point of view of education, it is a great gamification app for mathematical logic and especially the Lean. But I think, from the point of view of gaming, it seems like learning math rather than gaming. Unfortunately, I don’t have such a good idea of how to make a new League of legends or CS:GO on a logical basis either :) I am thinking of a simple secret diary written in a visual or math language where additional knowledge can be generated from the knowledge entered. Now that I have met the Lean, I am thinking about organizing a game around this ITP. I don’t have a specific idea for a rapid prototype for experimenting game-experience, but I am looking at pages that You mentioned, for example https://github.com/mpedramfar/Lean-game-maker or https://github.com/ImperialCollegeLondon/natural_number_game

[Norbert Bátfai]

Thanks for your pieces of advice. They are merged with Eric Wieser's modification:

theorem NoSuchBarber (Man : Type) (shaves : Man → Man → Prop)
  (h : ∃ x : Man, ∀ y : Man, shaves x y ↔ ¬shaves y y) :
  false :=
exists.elim h $
  assume barber : Man,
  assume h : ∀ y : Man, shaves barber y ↔ ¬shaves y y,
    have hbarber : shaves barber barber ↔ ¬shaves barber barber,
      from h barber,
    have nsbb : ¬shaves barber barber, from
      assume sbb : shaves barber barber,
      show false, from hbarber.mp sbb sbb,
    show false, from nsbb (hbarber.mpr nsbb)

I was using tactical mode mainly because in this mode I was able to trace the operation of Lean well.

[Eric Wieser]

I remember hearing that the proof state was now traceable in term mode, but I didn't find that to be the case on the online lean compiler. Did I imagine it? Is that feature restricted to vs-code?

[Kenny Lau]

you just need to know the undocumented underscore trick

[Kenny Lau]

the only reason tactic mode is more popular is because NNG popularized tactic-mode Lean

[Kenny Lau]

but term mode is as easy to use as tactic mode

[Kenny Lau]

at least for me

[Johan Commelin]

Kenny Lau said:

the only reason tactic mode is more popular is because NNG popularized tactic-mode Lean

Mwahh, tactic mode was popular before NNG existed

[Johan Commelin]

I think Eric is talking about inspecting the proof state of a term-mode proof after it has been written. This feature was added 2 months ago (or somewhere around then).

[Johan Commelin]

I have no idea if it is supposed to work in the web editor.

[Johan Commelin]

I think it greatly improved the readability of term-mode proofs.

[Bryan Gin-ge Chen]

The community web editor should be on the same version of Lean as mathlib master. Can you show an example?

[Eric Wieser]

My example is the proofs above. I can't seem to stick my cursor anywhere to get something useful

[Eric Wieser]

Relatedly, I'm finding that import data.subtype works locally but fails on the web editor - is the web editor mathlib-less?

[Bryan Gin-ge Chen]

Are you using the community web editor? Here's the link to the barber paradox.

I do see the types as I move my cursor around: Screen-Shot-2020-08-14-at-10.32.03-AM.png

[Eric Wieser]

Nope, I was using the other one...

[Utensil Song]

I strongly believe that the proof should be as readable as the same proof in natural language:

import tactic

variables (Man : Type) (shaves : Man → Man → Prop)

theorem NoSuchBarber ( h : ∃ barber : Man,  ∀ m : Man, shaves barber m ↔ ¬ shaves m m )
: false :=
begin
  -- from the existence of such a barber,
  -- we obtain a barber and the associated hypothesis
  obtain ⟨barber, barber_shaves_only_who_doesnt_self_shave⟩ := h,
  -- apply the associated hypothesis to the barber (as a customer)
  have self_shaving_dilemma := barber_shaves_only_who_doesnt_self_shave barber,
  -- apply `(a ↔ ¬a) → false` to `shaves barber barber` as `a`
  have dilemma_implies_false := (iff_not_self (shaves barber barber)).mp,
  -- apply the theorem "dilemma implies false" to the fact that
  -- we have proven the self-shaving dilemma
  exact dilemma_implies_false self_shaving_dilemma
end

[Alex J. Best]

There have been several interesting advances recently on making simple games with graphical interfaces in lean (using the Widgets setup), like rubiks cube https://github.com/kendfrey/rubiks-cube-group and sudoku https://github.com/TwoFX/sudoku

[Gabriel Ebner]

Do you have a screenshot/example file for the Rubik's cube?

[Kevin Buzzard]

Some screenshots here https://twitter.com/XenaProject/status/1289450598530654208?s=20 . I don't think the code is public yet.

Ooh https://twitter.com/XenaProject/status/1289450598530654208/photo/1

- The Xena Project (@XenaProject)

[Kevin Buzzard]

Oh -- https://github.com/kendfrey/rubiks-cube-group

[Kevin Buzzard]

@Kendall Frey how does it work?

[Kevin Buzzard]

he tells me that you can put stuff like #html (R2 L2 U2 D2 F2 B2).to_html at the bottom of src/rubiks_cube.lean to get stuff like cube.png

[Kendall Frey]

Yes, it's not an interactive game though. It renders a cube state as a human-readable picture, as a fancier form of has_repr

[Kevin Buzzard]

one person's repo which renders a cube state as a human-readable picture is another person's game

[Eric Wieser]

Can to_html emit JavaScript with a webgl 3d canvas?

[Kendall Frey]

HTML widgets don't support JS as far as I know.

[Chris Wong]

Surely that's an artificial restriction, as the VS Code extension itself is written in JavaScript.

[Mario Carneiro]

there are security concerns, of course...

[Chris Wong]

Of course! A less (?) dangerous solution would be to define custom elements on the VS Code side, and have the Lean use those.

[Mario Carneiro]

however from what I can tell vscode-lean has disabled all the security restrictions, so it's probably just a lack of implementation in the widget impl

[Chris Wong]

I think also since tactics can run arbitrary code already, the only situation where that makes a difference is when using a remote editor, as in that case the compiler and editor are running in separate contexts

[Norbert Bátfai]

I tried to describe my thoughts: https://arxiv.org/abs/2009.09068

[Edward Ayers]

wrt the 3D stuff; right now with widgets you can only output an html DOM object for the infoview to render, so you can do svg and CSS transformations and even CSS animations, but no arbitrary javascript yet.