Zulip Chat Archive

Stream: Codewars

Topic: Kata style


view this post on Zulip Bhavik Mehta (May 11 2020 at 16:26):

Question for anyone: what sort of kata would be most interesting to see?
In my case, the task would be to prove no_double_powerset_monad below:

import category_theory.types
import category_theory.monad.basic

open category_theory monad

@[simps]
def P : Type  Type :=
{ obj := λ X, set X,
  map := λ X Y, set.image }

def no_double_powerset_monad : Prop := monad (P  P)  false

Now this isn't an easy proof: my lean version is over 500 lines (though I'm sure it can be condensed by at least a factor of 4), and the maths proof was only published in December 2018. That said, it doesn't involve any particularly advanced lean or maths, only a rough idea of the sets API and a very basic understanding of monads. As I see them, the options here are: 1) Present the kata essentially as above, with no hints. 2) Provide a link to the paper but no other information. 3) Provide an approximate lean framework for how the proof might look, so that users can fill in the gaps (but not enforce that the framework must be followed). Any suggestions?

view this post on Zulip Donald Sebastian Leung (May 12 2020 at 03:51):

I think (1) or (2) would be good, currently leaning towards (2). For (3), solvers can always ask for additional hints on the general structure of the proof if they are really stuck.

view this post on Zulip Bhavik Mehta (May 12 2020 at 05:36):

Fair enough - my concern is that solvers would struggle to come up with the proof: it was mentioned in the category theory literature before 2003 but not solved until 2018 - seems a little unfair to make solvers figure this out for the sake of a kata!


Last updated: May 08 2021 at 22:13 UTC