Zulip Chat Archive

Stream: new members

Topic: Feedback on code style


view this post on Zulip Chris M (Apr 13 2020 at 06:41):

I just wrote my first proof in Lean for an example not from the official tutorial. I'm hoping I can get some advice on Lean code style, because my proof looks is pretty messy to me. I think it would suffice if I just got some pointers on best practices that would make this proof more readable.

I don't want to use tactics just yet, as I want to first learn how to write good non-tactic Lean code before I start learning how to use tactics.

So it would be really great if someone is willing to give me some pointers to best practices that would make this proof more readable.

example : X,  inductiveset X  inductiveset (spec (λx, x sub X) X) :=
    λX, assume hinductivesetX: inductiveset X,
    have hQdef: (u, u ε spec (λx, x sub X) X  u ε X  (λx, x sub X) u), from (specdef (λx, x sub X) X),
    and.intro
        (show null ε (spec (λx, x sub X) X), from
            have h2: null ε X, from hinductivesetX.1,
            have h3: null sub X, from (λu, assume hu: u ε null, absurd hu (nulldef u)),
            suffices h4: null ε X  null sub X, from ((specdef (λx, x sub X) X) null).2 h4,
            and.intro h2 h3
        )
        (show u, u ε (spec (λx, x sub X) X)  u U [u] ε (spec (λx, x sub X) X), from
            λu, assume h2:u ε (spec (λx, x sub X) X),
            suffices h3: u U [u] ε X  u U [u] sub X, from (hQdef (u U [u])).2 h3,
            have h4:u U [u] ε X, from (hinductivesetX.2 u) ((hQdef u).1 h2).1,
            have h5:u U [u] sub X, from
                have h6:u ε X, from ((hQdef u).1 h2).1,
                have h7:u sub X, from ((hQdef u).1 h2).2,
                λx, assume h8:x ε (u U [u]),
                    show x ε X, from
                    have h9: x ε u  x ε [u], from (uniondef x).1 h8,
                    or.elim h9
                        (assume h10: x ε u, (h7 x) h10)
                        (assume h11: x ε [u],
                            have h12:x = u, from ( or.elim ((pairdef x).1 h11) (assume h3:x=u, h3)(assume h3:x=u, h3) ),
                            show x ε X, from
                            eq.substr h12 h6
                        ),
            and.intro h4 h5
        )

Here are the background definitions and theorems:

constant Set : Type
constant In : Set  Set  Prop
infix `ε`:50  := In

definition subsett (S X: Set) := u, u ε S  u ε X
infix `sub`:50 := subsett



axiom axextentionality : X, Y, (u, u ε X  u ε Y)  X = Y
axiom axpairing : X:Set, Y:Set, S:Set, u, u ε S  u = X  u = Y
axiom axspecification (φ : Set  Prop) : X, S, (u, u ε S  u ε X  φ u)
axiom axunion : X, Y, S, u, u ε S  u ε X  u ε Y
axiom existsset : S:Set, S=S

noncomputable definition pair (x y) := classical.some (axpairing x y)
noncomputable definition union (X Y) := classical.some (axunion X Y)
noncomputable definition null:Set := classical.some (axspecification (λu, ¬u=u)
    (classical.some existsset)  )
noncomputable definition spec (φ : Set  Prop) (X : Set) := classical.some (axspecification φ X)

theorem pairdef {x y:Set} : u, u ε (pair x y)  u = x  u = y := classical.some_spec (axpairing x y)
theorem uniondef {X Y:Set} : u, u ε (union X Y)  u ε X  u ε Y := classical.some_spec (axunion X Y)
theorem nulldef : u, ¬(u ε null) := sorry

theorem specdef (φ : Set  Prop) (X:Set) : (u, u ε spec φ X  u ε X  φ u) := classical.some_spec (axspecification φ X)

infix `U`:50 := union
notation `[` x `,` y `]` := pair x y
notation `[` x `]` := pair x x

definition inductiveset (S:Set) : Prop := null ε S  u, u ε S  u U [u] ε S

view this post on Zulip Kenny Lau (Apr 13 2020 at 06:43):

what is ε? make sure your file can compile on its own

view this post on Zulip Chris M (Apr 13 2020 at 06:44):

whoops sorry for that, for got to copy it.

view this post on Zulip Mario Carneiro (Apr 13 2020 at 07:11):

Here's my best attempt at applying lean style guide stuff to your proof

constant Set : Type
constant In : Set  Set  Prop
infix `ε`:50 := In

def subsett (S X : Set) := u, u ε S  u ε X
infix `sub`:50 := subsett

axiom ax_ext (X Y) : ( u, u ε X  u ε Y)  X = Y
axiom ax_pair (X Y : Set) :  S : Set,  u, u ε S  u = X  u = Y
axiom ax_spec (φ : Set  Prop) (X) :  S,  u, u ε S  u ε X  φ u
axiom ax_union (X Y) :  S, u, u ε S  u ε X  u ε Y
axiom ax_exists_set :  S : Set, S = S

noncomputable def pair (x y : Set) : Set :=
classical.some (ax_pair x y)
noncomputable def union (X Y : Set) : Set :=
classical.some (ax_union X Y)
noncomputable def spec (φ : Set  Prop) (X : Set) :=
classical.some (ax_spec φ X)
noncomputable def null : Set :=
spec (λu, false) (classical.some ax_exists_set)

theorem mem_pair {x y u : Set} : u ε (pair x y)  u = x  u = y :=
classical.some_spec (ax_pair x y) _
theorem mem_union {X Y u : Set} : u ε (union X Y)  u ε X  u ε Y :=
classical.some_spec (ax_union X Y) _
theorem mem_spec {φ : Set  Prop} {X u : Set} : u ε spec φ X  u ε X  φ u :=
classical.some_spec (ax_spec φ X) _
theorem mem_null (u) : ¬ u ε null :=
λ h, (mem_spec.1 h).2

infix `U`:50 := union
notation `[` x `,` y `]` := pair x y
notation `[` x `]` := pair x x

def inductive_set (S:Set) : Prop := null ε S  u, u ε S  u U [u] ε S

example {X : Set} (hX : inductive_set X) : inductive_set (spec (λx, x sub X) X) :=
have hQdef : (u, u ε spec (λx, x sub X) X  u ε X  (λx, x sub X) u),
from λ _, mem_spec,
 show null ε (spec (λx, x sub X) X), from
  have h2 : null ε X, from hX.1,
  have h3 : null sub X, from λu, assume hu: u ε null, (mem_null _ hu).elim,
  suffices h4: null ε X  null sub X, from mem_spec.2 h4,
  h2, h3,
λ u, assume h2 : u ε (spec (λx, x sub X) X),
  show u U [u] ε (spec (λx, x sub X) X), from
  suffices h3 : u U [u] ε X  u U [u] sub X, from (hQdef (u U [u])).2 h3,
   show u U [u] ε X, from (hX.2 u) ((hQdef u).1 h2).1,
    show u U [u] sub X, from
    have h6 : u ε X, from ((hQdef u).1 h2).1,
    have h7 : u sub X, from ((hQdef u).1 h2).2,
    λx, assume h8:x ε (u U [u]),
      show x ε X, from
      have h9 : x ε u  x ε [u], from mem_union.1 h8,
      or.elim h9
        (assume h10: x ε u, (h7 x) h10)
        (assume h11: x ε [u],
          have h12:x = u, from
            or.elim (mem_pair.1 h11)
              (assume h3:x=u, h3)
              (assume h3:x=u, h3),
          show x ε X, from
          eq.substr h12 h6)⟩⟩

view this post on Zulip Mario Carneiro (Apr 13 2020 at 07:12):

For the proof itself, I have difficulty using term mode for presentation purposes. I find that tactic mode is much easier to provide a overview of the proof structure

view this post on Zulip Mario Carneiro (Apr 13 2020 at 07:18):

If I am using term mode, I generally don't waste space on have and show style presentation, which is usually available via hovers anyway. As such, the proof packs way down:

example {X : Set} (hX : inductive_set X) : inductive_set (spec (λx, x sub X) X) :=
mem_spec.2 hX.1, λu hu, (mem_null _ hu).elim, λ u h2,
 mem_spec.2 (hX.2 u) (mem_spec.1 h2).1,
  λ x h8, or.elim (mem_union.1 h8) ((mem_spec.1 h2).2 x) $ λ h11,
  eq.substr ((or_self _).1 (mem_pair.1 h11)) (mem_spec.1 h2).1⟩⟩

view this post on Zulip Mario Carneiro (Apr 13 2020 at 07:32):

In tactic mode, it's a lot easier to have nice formatting and keep the have and show

example {X : Set} (hX : inductive_set X) : inductive_set (spec (λx, x sub X) X) :=
begin
  have hQdef : (u, u ε spec (λx, x sub X) X  u ε X  (λx, x sub X) u),
  { apply mem_spec },
  split,
  { show null ε (spec (λx, x sub X) X),
    have h2 : null ε X := hX.1,
    have h3 : null sub X,
    { assume u (hu : u ε null),
      exact (mem_null _ hu).elim },
    suffices h4 : null ε X  null sub X, from mem_spec.2 h4,
    exact h2, h3 },
  { assume u (h2 : u ε (spec (λx, x sub X) X)),
    show u U [u] ε (spec (λx, x sub X) X),
    suffices h3 : u U [u] ε X  u U [u] sub X,
    { exact (hQdef (u U [u])).2 h3 },
    split,
    { show u U [u] ε X,
      from (hX.2 u) ((hQdef u).1 h2).1 },
    { show u U [u] sub X,
      have h6 : u ε X := ((hQdef u).1 h2).1,
      have h7 : u sub X := ((hQdef u).1 h2).2,
      assume x (h8 : x ε (u U [u])),
      show x ε X,
      have h9 : x ε u  x ε [u] := mem_union.1 h8,
      cases h9 with h10 h11,
      { exact (h7 x) h10 },
      { have h12 : x = u,
        { cases mem_pair.1 h11 with h3 h3,
          { exact h3 },
          { exact h3 } },
        show x ε X,
        exact eq.substr h12 h6 } } }
end

view this post on Zulip Kenny Lau (Apr 13 2020 at 07:33):

how about don't use axiom

view this post on Zulip Mario Carneiro (Apr 13 2020 at 07:34):

sure, but the replacement is harder to understand for a newbie

view this post on Zulip Chris M (Jun 08 2020 at 05:55):

@Mario Carneiro Thanks for this, and apologies for the super late reply. Corona disrupted my routine and I didn't come around to reading this until now. Will be studying this.


Last updated: May 10 2021 at 00:31 UTC