Zulip Chat Archive

Stream: new members

Topic: please comment on my code


Amir Livne Bar-on (May 17 2020 at 20:15):

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 (May 17 2020 at 20:15):

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

Amir Livne Bar-on (May 17 2020 at 20:16):

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 (May 17 2020 at 20:18):

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 (May 17 2020 at 20:19):

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 (May 17 2020 at 20:20):

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 (May 17 2020 at 20:21):

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

Patrick Massot (May 17 2020 at 20:21):

The := looks weird.

Bhavik Mehta (May 17 2020 at 20:21):

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

Patrick Massot (May 17 2020 at 20:22):

To me := really suggests data

Bryan Gin-ge Chen (May 17 2020 at 20:23):

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 (May 17 2020 at 20:23):

Nice suggestions! Thanks :)

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

Bryan Gin-ge Chen (May 17 2020 at 20:24):

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

Yury G. Kudryashov (May 17 2020 at 20:25):

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 (May 17 2020 at 20:27):

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

Mario Carneiro (May 17 2020 at 20:27):

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

Amir Livne Bar-on (May 17 2020 at 20:30):

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 (May 17 2020 at 20:32):

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 (May 17 2020 at 20:32):

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 (May 17 2020 at 20:33):

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

Amir Livne Bar-on (May 17 2020 at 20:35):

Lovely!

Yury G. Kudryashov (May 17 2020 at 20:35):

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

Patrick Massot (May 17 2020 at 20:36):

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

Patrick Massot (May 17 2020 at 20:36):

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

Mario Carneiro (May 17 2020 at 20:37):

I'm curious where you learned the rewrite tactic

Mario Carneiro (May 17 2020 at 20:37):

mathlib almost exclusively uses rw

Amir Livne Bar-on (May 17 2020 at 20:38):

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 (May 17 2020 at 20:38):

Is your background in maths or computing?

Kevin Buzzard (May 17 2020 at 20:39):

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

Mario Carneiro (May 17 2020 at 20:39):

which tutorial

Kevin Buzzard (May 17 2020 at 20:39):

#tpil is a lot more termy

Patrick Massot (May 17 2020 at 20:39):

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

Amir Livne Bar-on (May 17 2020 at 20:39):

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

Amir Livne Bar-on (May 17 2020 at 20:39):

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

Kevin Buzzard (May 17 2020 at 20:40):

You might like tpil better

Amir Livne Bar-on (May 17 2020 at 20:40):

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 (May 17 2020 at 20:41):

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 (May 17 2020 at 20:41):

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

Patrick Massot (May 17 2020 at 20:42):

No, TPIL is not outdated

Mario Carneiro (May 17 2020 at 20:42):

Yury's version of between_mem_real_convex is a good example

Yury G. Kudryashov (May 17 2020 at 20:42):

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 (May 17 2020 at 20:42):

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

Mario Carneiro (May 17 2020 at 20:43):

why nonempty?

Amir Livne Bar-on (May 17 2020 at 20:45):

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 (May 17 2020 at 20:46):

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 (May 17 2020 at 20:46):

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

yes

Mario Carneiro (May 17 2020 at 20:47):

mathlib is a predominantly classical library

Amir Livne Bar-on (May 17 2020 at 20:47):

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

Mario Carneiro (May 17 2020 at 20:48):

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

Kevin Buzzard (May 17 2020 at 20:48):

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 (May 17 2020 at 20:48):

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 (May 17 2020 at 20:48):

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

Mario Carneiro (May 17 2020 at 20:48):

pretty much all

well, Coq and Agda mostly

Patrick Stevens (May 17 2020 at 20:49):

I stand hyperbolic

Mario Carneiro (May 17 2020 at 20:49):

isabelle, HOL, HOL light are classical

Mario Carneiro (May 17 2020 at 20:49):

but most DTT theorem provers are constructive, it is true

Amir Livne Bar-on (May 17 2020 at 20:53):

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 (May 17 2020 at 20:53):

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 (May 17 2020 at 20:53):

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

Mario Carneiro (May 17 2020 at 20:54):

(lean 4 thinks arrows are cool)

Amir Livne Bar-on (May 17 2020 at 20:54):

cool, replacing with a comma and adding an underscore works

Mario Carneiro (May 17 2020 at 20:54):

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 (May 17 2020 at 20:56):

nice :)


Last updated: Dec 20 2023 at 11:08 UTC