Code review?

Stream: new members

[Andre Knispel]

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]

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

[Andre Knispel]

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]

Sounds great.

[Johan Commelin]

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

[Johan Commelin]

Breaking things into sublemmas usually helps a lot.

[Johan Commelin]

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

[Johan Commelin]

@Andre Knispel What is in leanpkg.toml in the base of your mathlib clone?

[Johan Commelin]

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

[Johan Commelin]

(Like, imports that are wrong.)

[Kevin Buzzard]

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]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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]

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]

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

[Kevin Buzzard]

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]

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]

Sounds good to me

[Johan Commelin]

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

[Kevin Buzzard]

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

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

[Johan Commelin]

So we need to wait for his PR (-;

[Johan Commelin]

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]

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]

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]

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]

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]

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]

If we had linarith_mod_cast then the last two lines could be one line.

[Luigi Massacci]

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]

?_ 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]

Sorry, I meant things like apply?, simp?, etc. I should have put the question mark after

[Kevin Buzzard]

Just type the tactic and then hover over it for documentation

[Kyle Miller]

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]

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]

There's a variable? command that figures out which additional instance arguments you need in case you're missing any.

[Luigi Massacci]

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!