# Zulip Chat Archive

## Stream: new members

### Topic: Code review?

#### Andre Knispel (Aug 15 2020 at 13:08):

I'm more or less done constructing the irrelevant ideal of N graded rings, but I've come across a bunch of problems or things that I didn't like in the proof, where I didn't think I could construct a small example of the problem. So I've made a gist that should be self contained and put questions and other comments in the proof (the long one, at the end of the file). I'd be grateful for any comments! https://gist.github.com/WhatisRT/98b512bd534d70e430f9aafa350dc581

#### Johan Commelin (Aug 15 2020 at 13:30):

Hi @Andre Knispel that's a nice topic (-;

#### Andre Knispel (Aug 15 2020 at 13:33):

Thanks! My plan is to construct the `Proj`

functor and if I it doesn't take too long, state and prove the moduli problem for projective space

#### Johan Commelin (Aug 15 2020 at 13:39):

Sounds great.

#### Johan Commelin (Aug 15 2020 at 13:40):

I think the general problem with your code might be that it's an extremely long proof

#### Johan Commelin (Aug 15 2020 at 13:40):

Breaking things into sublemmas usually helps a lot.

#### Johan Commelin (Aug 15 2020 at 13:40):

But let me load your code into Lean and take a quick look

#### Johan Commelin (Aug 15 2020 at 13:42):

@Andre Knispel What is in `leanpkg.toml`

in the base of your mathlib clone?

#### Johan Commelin (Aug 15 2020 at 13:42):

Because I get a *lot* of errors when I use a recent mathlib.

#### Johan Commelin (Aug 15 2020 at 13:43):

(Like, imports that are wrong.)

#### Kevin Buzzard (Aug 15 2020 at 13:45):

Note that in some sense we don't have the Spec functor yet, because we don't have the target category. The reason schemes are not yet in mathlib is that there still seems to be no acceptable way to say "I am a sheaf of rings" in mathlib. In the schemes repo we just made an ad hoc definition of a sheaf of rings, however the definition of a presheaf in mathlib takes values in a category so is incompatible with ours (which just took values in Type). In particular if you want to develop code which will be in mathlib it is extremely difficult to proceed right now.

#### Andre Knispel (Aug 15 2020 at 14:18):

@Johan Commelin I'm using the mathlib I got from lean-scheme, it says version 0.1

#### Johan Commelin (Aug 15 2020 at 14:20):

Oof, I see. That version is ancient (-;

#### Johan Commelin (Aug 15 2020 at 14:21):

The big downside is that we don't have precompiled versions of that mathlib, I think.

#### Kevin Buzzard (Aug 15 2020 at 14:24):

This is not the right answer. Version 0.1 is the version of lean-scheme

#### Kevin Buzzard (Aug 15 2020 at 14:26):

But if you're building on lean-scheme then the answer is that it's the version of mathlib used there. In some sense there is little point building on this because it will have to be rewritten when it all moves to mathlib, but a different way of looking at it is that if you're learning how to use lean then perhaps getting stuff into mathlib is not really your main concern

#### Kevin Buzzard (Aug 15 2020 at 14:29):

There's a whole bunch of ideas in that repo, there is Gamma Spec duality, glueing sheaves and various other things, but none of it can go into mathlib because we just have to wait until they give us a definition of a ringed space

#### Kevin Buzzard (Aug 15 2020 at 14:33):

Oh hot news: https://github.com/leanprover-community/mathlib/commit/099f070f41867bb6bd0f6494307873a126e3c4ad is merged! So we have sheaves as of basically just now!

#### Kevin Buzzard (Aug 15 2020 at 14:38):

Ok this changes everything. @Andre Knispel if you want to do something which could go in mathlib we are now in a position to define ringed spaces and schemes. However without a sheafification functor we're still not able to get too far. But at least we can now start. Basically this enables us to make new definitions but we're still limited in what theorems we can prove

#### Andre Knispel (Aug 15 2020 at 14:46):

Oh, that's great! As you've guessed, getting this into mathlib isn't my main concern, but it would be nice. What I've done so far doesn't use any schemes of course, so I could just as well use master for that. Maybe getting `Proj`

as a ringed space would also be nice, if that has the advantage of being able to be merged

#### Johan Commelin (Aug 15 2020 at 14:49):

Sounds good to me

#### Johan Commelin (Aug 15 2020 at 14:49):

I hope that by the time you have Proj as ringed space, we'll have a category of schemes (-;

#### Kevin Buzzard (Aug 15 2020 at 15:01):

@Johan Commelin actually there's still a problem with defining schemes. A scheme is something locally isomorphic as a presheafed space to Spec(R) but we can't make Spec(R) a presheafed space because we only know the values of the presheaf on a basis. In the schemes repo is the proof that this presheaf is a sheaf on a basis but then we'll need to extend to the entire top space and my guess is that one is supposed to do this using formal machinery

#### Johan Commelin (Aug 15 2020 at 15:10):

Yup... I know. But Bhavik seems to have this

#### Johan Commelin (Aug 15 2020 at 15:10):

So we need to wait for his PR (-;

#### Johan Commelin (Aug 15 2020 at 15:11):

But I don't think that Andre will have Proj next week (-; so we still have a couple of days to get our act together :grinning_face_with_smiling_eyes:

#### Andre Knispel (Aug 16 2020 at 15:28):

I've taken some time to make my code compatible with the mathlib on master and updated the gist. A bunch of problems I've had went away, which made the proof much shorter, but I still have some questions that are in the comments. https://gist.github.com/WhatisRT/98b512bd534d70e430f9aafa350dc581

#### Luigi Massacci (Aug 02 2023 at 15:18):

I wonder if there's any kind soul that might suggest how to make this code look more idiomatic? I'm afraid the answer will be "learn to use `conv`

" but still... In particular I'm interested if there's a way to make lean infer the coercion I did manually with `Nat.cast`

```
import Mathlib.Tactic
import Mathlib.Data.Real.Basic
def ConvergesTo (s : ℕ → ℝ) (a : ℝ) :=
∀ ε > 0, ∃ N, ∀ n ≥ N, |s n - a| < ε
theorem harmonic : ConvergesTo (fun n : ℕ ↦ 1/n) (0) := by
intro ε εpos
rcases exists_nat_gt (ε⁻¹) with ⟨N, hN⟩
use N
intro n ngeN
dsimp
rw [sub_zero]
have ε_inv_pos : ε⁻¹ > 0 := inv_pos.mpr εpos
have Npos : (0 : ℝ) < (↑N) := lt_trans ε_inv_pos hN
have hN_rev := (inv_lt_inv Npos ε_inv_pos).mpr hN
rw [inv_inv] at hN_rev
have npos : (@Nat.cast ℝ Semiring.toNatCast n) > (0 : ℝ) := lt_of_lt_of_le Npos (Nat.cast_le.mpr ngeN)
have nge_rev : (@Nat.cast ℝ Semiring.toNatCast n)⁻¹ ≤ (@Nat.cast ℝ Semiring.toNatCast N)⁻¹ := by
apply (inv_le_inv npos Npos).mpr
exact (Nat.cast_le.mpr ngeN)
have := lt_of_le_of_lt nge_rev hN_rev
ring_nf
have inv_n_pos := (inv_pos.mpr npos)
rw [abs_of_pos inv_n_pos]
apply lt_of_le_of_lt nge_rev hN_rev
```

Thanks in advance!

#### Alex J. Best (Aug 02 2023 at 15:28):

You can write

```
have npos : (n : ℝ) > 0 := lt_of_lt_of_le Npos (Nat.cast_le.mpr ngeN)
```

for one thing, and you might find the `norm_cast`

and `exact_mod_cast`

tactics useful

```
have nge_rev : (n : ℝ)⁻¹ ≤ (N : ℝ)⁻¹ := by
rw [inv_le_inv npos Npos]
exact_mod_cast ngeN
```

I also think you should probably use `simp`

more, eg. when you use `ring_nf`

which is a bit overkill!

#### Alex J. Best (Aug 02 2023 at 15:34):

```
import Mathlib.Tactic
import Mathlib.Data.Real.Basic
def ConvergesTo (s : ℕ → ℝ) (a : ℝ) :=
∀ ε > 0, ∃ N, ∀ n ≥ N, |s n - a| < ε
theorem harmonic : ConvergesTo (fun n : ℕ ↦ 1/n) (0) := by
intro ε εpos
obtain ⟨N, hN⟩ := exists_nat_gt ε⁻¹
refine ⟨N, λ n ngeN ↦ ?_⟩
simp only [one_div, sub_zero]
have ε_inv_pos : ε⁻¹ > 0 := inv_pos_of_pos εpos
have Npos : (0 : ℝ) < N := lt_trans ε_inv_pos hN
have hN_rev := inv_lt_of_inv_lt εpos hN
have npos : 0 < (n : ℝ) := Npos.trans_le (by exact_mod_cast ngeN)
have nge_rev : (n : ℝ)⁻¹ ≤ (N : ℝ)⁻¹ := by
rw [inv_le_inv npos Npos]
exact_mod_cast ngeN
simp only [one_div, gt_iff_lt]
have inv_n_pos := inv_pos_of_pos npos
rw [abs_of_pos inv_n_pos]
apply lt_of_le_of_lt nge_rev hN_rev
```

this is a version with a few more little changes, for instance using dot notation more, using more existing lemmas

#### Kevin Buzzard (Aug 02 2023 at 15:51):

Here's what I came up with:

```
theorem harmonic : ConvergesTo (fun n : ℕ ↦ 1/n) (0) := by
intro ε εpos
rcases exists_nat_gt (ε⁻¹) with ⟨N, hN⟩
have invεpos : 0 < ε⁻¹ := inv_pos.mpr εpos -- found with `exact?` and useful to have around
refine ⟨N, fun n ngeN ↦ ?_⟩ -- use and intro at the same time
have ngeN' : (N : ℝ) ≤ n := by assumption_mod_cast -- also useful to have around; it's `ngeN` modulo casts
simp only [one_div, sub_zero] -- `simp?` gave me this
rw [abs_of_pos] -- natural next move: makes the goal simpler
· refine lt_of_le_of_lt ?_ (inv_lt_of_inv_lt εpos hN) -- found with `have : (N : ℝ)⁻¹ < ε := by exact?`
rwa [inv_le_inv] <;> linarith -- guessed the name
· simp only [inv_pos, Nat.cast_pos] -- `simp?` gave me this
suffices 0 < (n : ℝ) by assumption_mod_cast
linarith
```

I aggressively use tactics like `linarith`

and `simp?`

and `exact?`

because I don't know the names of the lemmas.

#### Kevin Buzzard (Aug 02 2023 at 15:52):

If we had `linarith_mod_cast`

then the last two lines could be one line.

#### Luigi Massacci (Aug 02 2023 at 16:07):

Thank you very much to the both of you, that was very helpful! By any chance, @Kevin Buzzard do you happen to know where I could read more about "?"-tactics? I assume it's some kind of higher order unification?

#### Eric Wieser (Aug 02 2023 at 16:15):

`?_`

isn't really a tactic, it's a term that means "I'll come back to this later". You can write `?foo`

instead of `?_`

to name that obligation `foo`

.

#### Luigi Massacci (Aug 02 2023 at 16:25):

Sorry, I meant things like `apply?`

, `simp?`

, etc. I should have put the question mark after

#### Kevin Buzzard (Aug 02 2023 at 17:45):

Just type the tactic and then hover over it for documentation

#### Kyle Miller (Aug 02 2023 at 18:01):

A number of tactics have a `?`

variant for either giving extra information ("what did this tactic do, and what can I replace it with?") or for doing a more expensive search for a proof (like `apply?`

and `exact?`

, which search the whole library).

#### Kyle Miller (Aug 02 2023 at 18:02):

A number of attributes have `?`

variants for verbose mode as well, like `@[simps?]`

tells you which simp lemmas it generated for a definition.

#### Kyle Miller (Aug 02 2023 at 18:03):

There's a `variable?`

command that figures out which additional instance arguments you need in case you're missing any.

#### Luigi Massacci (Aug 03 2023 at 01:02):

Thanks everyone, I explained myself horribly, I was curious as to how they worked under the hood, assuming that it might be some kind of complicated procedure, but I just ended up looking directly at the code and its reasonably straightforward. Cheers and thanks again!

Last updated: Dec 20 2023 at 11:08 UTC