## Stream: new members

### Topic: Feedback on code style

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


#### Kenny Lau (Apr 13 2020 at 06:43):

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

#### Chris M (Apr 13 2020 at 06:44):

whoops sorry for that, for got to copy it.

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


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

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


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


#### Kenny Lau (Apr 13 2020 at 07:33):

how about don't use axiom

#### Mario Carneiro (Apr 13 2020 at 07:34):

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

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