Zulip Chat Archive

Stream: general

Topic: barber paradox


view this post on Zulip Cameron Crossman (Dec 11 2018 at 20:34):

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

view this post on Zulip Cameron Crossman (Dec 11 2018 at 20:34):

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

view this post on Zulip Andrew Ashworth (Dec 11 2018 at 20:37):

Do you have a specific question?

view this post on Zulip Chris Hughes (Dec 11 2018 at 20:44):

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

view this post on Zulip Abhimanyu Pallavi Sudhir (Dec 16 2018 at 14:51):

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

view this post on Zulip Kevin Buzzard (Dec 16 2018 at 15:07):

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

view this post on Zulip Kevin Buzzard (Dec 16 2018 at 15:10):

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

view this post on Zulip Kevin Buzzard (Dec 16 2018 at 16:48):

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...)

view this post on Zulip Norbert Bátfai (Aug 14 2020 at 10:54):

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

view this post on Zulip Kenny Lau (Aug 14 2020 at 10:57):

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.

view this post on Zulip Kyle Miller (Aug 14 2020 at 10:57):

(assuming you formalized the statement correctly)

view this post on Zulip Eric Wieser (Aug 14 2020 at 11:27):

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

view this post on Zulip Scott Morrison (Aug 14 2020 at 11:28):

well, you could save more than that :-)

view this post on Zulip Eric Wieser (Aug 14 2020 at 11:28):

Oh, for sure :)

view this post on Zulip Chris Wong (Aug 14 2020 at 12:21):

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.

view this post on Zulip Kevin Buzzard (Aug 14 2020 at 12:22):

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
)

view this post on Zulip Kevin Buzzard (Aug 14 2020 at 12:23):

but of course this teaches you far less :-)

view this post on Zulip Norbert Bátfai (Aug 14 2020 at 12:23):

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

view this post on Zulip Kevin Buzzard (Aug 14 2020 at 12:29):

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

view this post on Zulip Kevin Buzzard (Aug 14 2020 at 12:29):

That's the mathlib proof

view this post on Zulip Norbert Bátfai (Aug 14 2020 at 12:31):

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.

view this post on Zulip Kevin Buzzard (Aug 14 2020 at 12:31):

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.

view this post on Zulip Kevin Buzzard (Aug 14 2020 at 12:32):

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

view this post on Zulip Ruben Van de Velde (Aug 14 2020 at 12:33):

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

view this post on Zulip Chris Wong (Aug 14 2020 at 12:34):

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

view this post on Zulip Kenny Lau (Aug 14 2020 at 12:48):

@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)

view this post on Zulip Norbert Bátfai (Aug 14 2020 at 12:54):

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.

view this post on Zulip Chris Wong (Aug 14 2020 at 13:03):

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

view this post on Zulip Norbert Bátfai (Aug 14 2020 at 13:52):

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

view this post on Zulip Norbert Bátfai (Aug 14 2020 at 14:07):

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.

view this post on Zulip Eric Wieser (Aug 14 2020 at 14:18):

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?

view this post on Zulip Kenny Lau (Aug 14 2020 at 14:19):

you just need to know the undocumented underscore trick

view this post on Zulip Kenny Lau (Aug 14 2020 at 14:20):

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

view this post on Zulip Kenny Lau (Aug 14 2020 at 14:20):

but term mode is as easy to use as tactic mode

view this post on Zulip Kenny Lau (Aug 14 2020 at 14:20):

at least for me

view this post on Zulip Johan Commelin (Aug 14 2020 at 14:21):

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

view this post on Zulip Johan Commelin (Aug 14 2020 at 14:22):

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).

view this post on Zulip Johan Commelin (Aug 14 2020 at 14:22):

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

view this post on Zulip Johan Commelin (Aug 14 2020 at 14:22):

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

view this post on Zulip Bryan Gin-ge Chen (Aug 14 2020 at 14:23):

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

view this post on Zulip Eric Wieser (Aug 14 2020 at 14:31):

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

view this post on Zulip Eric Wieser (Aug 14 2020 at 14:31):

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

view this post on Zulip Bryan Gin-ge Chen (Aug 14 2020 at 14:33):

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

view this post on Zulip Eric Wieser (Aug 14 2020 at 14:40):

Nope, I was using the other one...

view this post on Zulip Utensil Song (Aug 14 2020 at 14:52):

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

view this post on Zulip Alex J. Best (Aug 14 2020 at 16:01):

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

view this post on Zulip Gabriel Ebner (Aug 14 2020 at 16:50):

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

view this post on Zulip Kevin Buzzard (Aug 14 2020 at 16:52):

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

view this post on Zulip Kevin Buzzard (Aug 14 2020 at 16:53):

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

view this post on Zulip Kevin Buzzard (Aug 14 2020 at 16:57):

@Kendall Frey how does it work?

view this post on Zulip Kevin Buzzard (Aug 14 2020 at 17:03):

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

view this post on Zulip Kendall Frey (Aug 14 2020 at 17:06):

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

view this post on Zulip Kevin Buzzard (Aug 14 2020 at 17:13):

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

view this post on Zulip Eric Wieser (Aug 14 2020 at 19:30):

Can to_html emit JavaScript with a webgl 3d canvas?

view this post on Zulip Kendall Frey (Aug 15 2020 at 00:59):

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

view this post on Zulip Chris Wong (Aug 15 2020 at 02:09):

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

view this post on Zulip Mario Carneiro (Aug 15 2020 at 02:16):

there are security concerns, of course...

view this post on Zulip Chris Wong (Aug 15 2020 at 02:21):

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

view this post on Zulip Mario Carneiro (Aug 15 2020 at 02:21):

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

view this post on Zulip Chris Wong (Aug 15 2020 at 03:55):

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

view this post on Zulip Norbert Bátfai (Sep 22 2020 at 06:46):

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

view this post on Zulip Edward Ayers (Nov 12 2020 at 18:04):

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.


Last updated: May 13 2021 at 20:13 UTC