Feedback on code style

Stream: new members

[Chris M]

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

[Kenny Lau]

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

[Chris M]

whoops sorry for that, for got to copy it.

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mario Carneiro]

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⟩⟩

[Mario Carneiro]

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

[Kenny Lau]

how about don't use axiom

[Mario Carneiro]

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

[Chris M]

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