please comment on my code

Stream: new members

[Amir Livne Bar-on]

Hi! I'm a newcomer to Lean, started learning the system yesterday. My thoughts are to contribute some stuff about finite-dimensional convex sets to mathlib.

For starters I decided to prove a simple lemma, and spent the last 2 days chasing sorry's and shortening & simplifying the proofs and the statements...
I'm looking for feedback for my code (attached). Anything from comments on my proof technique, to granularity of the lemmas, to the use of classical logic (didn't manage the first 2 properties without it), to stylistic comments. I want my code to be idiomatic.

Also, I felt that there's a proof tactic missing: similar to "simp", but that also tries to perform "apply" and "exact" steps in addition to "rewrite". Is there such a tactic? If not, would it be hard to make one or computationally heavy to run it?

convexity.lean

[Mario Carneiro]

I suggest cut and pasting the code here in a code block in #backticks

[Amir Livne Bar-on]

Sure!

import analysis.convex.basic

attribute [instance] classical.prop_decidable

section general

universe u

variables {α : Type u} [linear_order α] [nonempty α] {s : set α}

local attribute [simp] not_forall
local attribute [simp] set.not_nonempty_iff_eq_empty
local attribute [simp] set.eq_empty_iff_forall_not_mem

lemma not_bdd_above_over_everything (hs : ¬ bdd_above s) (x : α) :
    ∃ (y : α), y ∈ s ∧ x < y :=
begin
    simp [bdd_above, upper_bounds] at hs,
    exact hs x
end

lemma not_bdd_below_under_everything (hs : ¬ bdd_below s) (x : α) :
    ∃ (y : α), y ∈ s ∧ y < x :=
begin
    simp [bdd_below, lower_bounds] at hs,
    exact hs x
end

end general

section real_line

variable {s : set ℝ}

lemma between_mem_real_convex {a b x : ℝ} (sc : convex s) (ha : a ∈ s)
    (hb : b ∈ s) (a_le_x : a ≤ x) (x_le_b : x ≤ b) : x ∈ s :=
begin
    rewrite convex_real_iff at sc,
    have ab_subset_s : set.Icc a b ⊆ s,
        from sc ha hb,
    have x_mem_ab : x ∈ set.Icc a b,
        simp [set.mem_Icc, a_le_x, x_le_b],
    exact set.mem_of_mem_of_subset x_mem_ab ab_subset_s
end

lemma unbounded_convex_is_real_line (sc : convex s)
    (sna : ¬ bdd_above s) (snb : ¬ bdd_below s) : s = set.univ :=
begin
    apply set.eq_univ_of_forall,
    intro x,
    cases not_bdd_below_under_everything snb x with a ha,
    cases not_bdd_above_over_everything sna x with b hb,
    have a_le_x : a ≤ x, from le_of_lt ha.right,
    have x_le_b : x ≤ b, from le_of_lt hb.right,
    exact between_mem_real_convex sc ha.left hb.left a_le_x x_le_b
end

end real_line

[Mario Carneiro]

I think you can prove the first theorem using

lemma not_bdd_above_over_everything (hs : ¬ bdd_above s) : \all (x : α),
    ∃ (y : α), y ∈ s ∧ x < y :=
by simpa [bdd_above, upper_bounds] using hs

[Bhavik Mehta]

The main thing which stands out to me here is the use of "non-terminal simps" - that means uses of simp which don't close the goal. For instance the first line of not_bdd_above_over_everything, but not your proof of x_mem_ab. Non-terminal simps are discouraged, mainly because they're usually less robust in mathlib: if someone adds a new simp lemma, non-terminal simp proof often break. You can avoid them by changing it to squeeze_simp, which will tell you a simp only to replace your simp with. Or in some cases you can convert to a simpa, like Mario suggests

[Bhavik Mehta]

More minor things: instead of have name : type, from proof you can do have name : type := proof. Also I think two spaces are preferred in mathlib

[Patrick Massot]

I really prefer the version using from, it reads much nicer

[Patrick Massot]

The := looks weird.

[Bhavik Mehta]

Fair enough, I prefer the := but I guess this is personal choice

[Patrick Massot]

To me := really suggests data

[Bryan Gin-ge Chen]

The best way to get a lot of feedback on a piece of Lean code is to PR it to mathlib on GitHub. People can more easily comment on specific lines of your code / make suggestions.

[Amir Livne Bar-on]

Nice suggestions! Thanks :)

Where could I have read about simpa (and presumably other tactics)?

[Bryan Gin-ge Chen]

https://leanprover-community.github.io/mathlib_docs/tactics.html

[Yury G. Kudryashov]

Most steps in the proof of between_mem_real_convex just unfold definitions, so the proof can be condensed to (fixed a typo)

lemma between_mem_real_convex {a b x : ℝ} (sc : convex s) (ha : a ∈ s)
    (hb : b ∈ s) (a_le_x : a ≤ x) (x_le_b : x ≤ b) : x ∈ s :=
convex_real_iff.1 sc ha hb ⟨a_le_x, x_le_b⟩

[Mario Carneiro]

The have : type := value version also compiles faster and has better type inference

[Mario Carneiro]

because have : type, from value is actually two tactics back to back

[Amir Livne Bar-on]

This version works:

lemma between_mem_real_convex {a b x : ℝ} (sc : convex s) (ha : a ∈ s)
  (hb : b ∈ s) (a_le_x : a ≤ x) (x_le_b : x ≤ b) : x ∈ s :=
set.mem_of_mem_of_subset
  (set.mem_Icc.2 (and.intro a_le_x x_le_b))
  (convex_real_iff.1 sc ha hb)

[Yury G. Kudryashov]

Note that both mem_of_mem_of_subset and mem_Icc just unfold definitions. In particular, you can apply h : s \sub t to hx : x \in s

[Amir Livne Bar-on]

and is more intuitive to me (I can see how the function applications correspond to logic operations).

What do the brackets do? Is it magic? (Your version works too)

[Yury G. Kudryashov]

Brackets work as "use the only constructor for the expected type"

[Amir Livne Bar-on]

Lovely!

[Yury G. Kudryashov]

So it works for and, Exists, prod, sigma, ...

[Patrick Massot]

How did you learn Lean? You seem to have an exotic combination of knownledge

[Patrick Massot]

This anonymous constructor thing is much more basic than some things you seem to understand well

[Mario Carneiro]

I'm curious where you learned the rewrite tactic

[Mario Carneiro]

mathlib almost exclusively uses rw

[Amir Livne Bar-on]

Proof assistance was in the back of my mind for a while, I read about Mizar some years ago, and started learning by doing around half of the tutorial (which is very tactic-heavy imo)

[Kevin Buzzard]

Is your background in maths or computing?

[Kevin Buzzard]

The tutorials are aimed at mathematicians, who think in a tactic-heavy way

[Mario Carneiro]

which tutorial

[Kevin Buzzard]

#tpil is a lot more termy

[Patrick Massot]

He already answered that question by complaining about tactics :wink:

[Amir Livne Bar-on]

I have a graduate degree (MA) in math, but I've been working in algorithmics for the last few years

[Amir Livne Bar-on]

https://github.com/leanprover-community/tutorials/

[Kevin Buzzard]

You might like tpil better

[Amir Livne Bar-on]

is that this book?

https://leanprover.github.io/theorem_proving_in_lean/

this really supplemented my knowledge and was a great help, but the syntax seems very out of date

[Amir Livne Bar-on]

the strange thing about the tutorial is that it focuses on goal tactics rather than on rewrite tactics, which seem to me to be closer to the usual way proofs are done (with natural language)

[Mario Carneiro]

mathlib uses term mode proofs for a lot of simple "apply, cases, exact" proofs

[Patrick Massot]

No, TPIL is not outdated

[Mario Carneiro]

Yury's version of between_mem_real_convex is a good example

[Yury G. Kudryashov]

About the first two lemmas: it would be nice to have

lemma not_bdd_above_iff' [nonempty α] [preorder α] {s : set α} :
 not (bdd_above s) <-> ∀ x, ∃ y ∈ s, not (y ≤ x) := by simp [bdd_above]

lemma not_bdd_above_iff [nonempty α] [linear_order α] {s : set α} :
 not (bdd_above s) <-> ∀ x, ∃ y ∈ s, x < y := by simp [bdd_above]

plus bdd_below versions. These lemmas should go to order/bounds.

[Yury G. Kudryashov]

(not tested, possibly I missed some "obvious" assumption)

[Mario Carneiro]

why nonempty?

[Amir Livne Bar-on]

These compile:

lemma not_bdd_above_iff' [preorder α] {s : set α} :
  ¬ (bdd_above s) ↔ ∀ x, ∃ y ∈ s, not (y ≤ x) := by simp [bdd_above, upper_bounds]

lemma not_bdd_above_iff [linear_order α] {s : set α} :
  ¬ (bdd_above s) ↔ ∀ x, ∃ y ∈ s, x < y := by simp [bdd_above, upper_bounds]

[Amir Livne Bar-on]

But they still need classical logic... Is it common practice to use it in mathlib?
(Personally I dont see why it's required here, but can be hard to tell sometimes what's constructive and what isn't)

[Mario Carneiro]

But they still need classical logic... Is it common practice to use it in mathlib?

yes

[Mario Carneiro]

mathlib is a predominantly classical library

[Amir Livne Bar-on]

It's not enough to use [decidable_linear_order α] for example

[Mario Carneiro]

right, the decidability assumption on this is complicated enough as to be useless in practice

[Kevin Buzzard]

One of the aims of mathlib is to cover a normal maths undergraduate degree course and this uses so much classical stuff that it's become the default

[Patrick Stevens]

Mathlib is trying to be "for the rest of the mathematicians", as opposed to pretty much all the other proof assistants out there which take great pains to be constructive

[Mario Carneiro]

if you are avoiding EM then you shouldn't use this lemma

[Mario Carneiro]

pretty much all

well, Coq and Agda mostly

[Patrick Stevens]

I stand hyperbolic

[Mario Carneiro]

isabelle, HOL, HOL light are classical

[Mario Carneiro]

but most DTT theorem provers are constructive, it is true

[Amir Livne Bar-on]

Another question: how can I get type hints in "direct mode"?
For example, I'm writing

lemma unbounded_convex_is_real_line' (sc : convex s)
  (sna : ¬ bdd_above s) (snb : ¬ bdd_below s) : s = set.univ :=
set.eq_univ_of_forall ( λ x : ℝ →  )

how do I get (in VS code with the plugin) the type I should create in the lambda?

[Mario Carneiro]

lemma unbounded_convex_is_real_line' (sc : convex s)
  (sna : ¬ bdd_above s) (snb : ¬ bdd_below s) : s = set.univ :=
set.eq_univ_of_forall ( λ x : ℝ, _)

[Mario Carneiro]

lean 3 uses a comma after a lambda, not an arrow

[Mario Carneiro]

(lean 4 thinks arrows are cool)

[Amir Livne Bar-on]

cool, replacing with a comma and adding an underscore works

[Mario Carneiro]

you can also use begin end in place of any underscore or place where a term is expected to go to tactic mode locally

[Amir Livne Bar-on]

nice :)