tactic or term mode proof?

Stream: maths

[Kevin Buzzard]

I am writing an API for DVRs. I've just proved the following lemma about commutative rings:

lemma local_of_unique_nonzero_prime (R : Type u) [comm_ring R]
(h : ∃! P : ideal R, P ≠ ⊥ ∧ is_prime P) : local_ring R :=
local_of_unique_max_ideal
begin
  rcases h with ⟨P, ⟨hPnonzero, hPnot_top, _⟩, hPunique⟩,
  use P,
  split,
  { split, exact hPnot_top,
    apply maximal_of_no_maximal,
    intros M hPM hM,
    apply ne_of_lt hPM,
    symmetry,
    apply hPunique,
    split, apply ne_bot_of_gt hPM,
    exact is_maximal.is_prime hM},
  { intros M hM,
    apply hPunique,
    split,
    { rintro rfl,
      cases hM with hM1 hM2,
      specialize hM2 P (bot_lt_iff_ne_bot.2 hPnonzero),
      exact hPnot_top hM2},
    { exact is_maximal.is_prime hM}}
end

The proof is unremarkable: a unique non-zero prime ideal implies a unique maximal ideal by some fiddling. The proof looks to me like tidy could almost have done it. I use rcases, split, exact, apply, intros etc.

I know that if Mario had written this proof he would then start golfing it and turning it into term mode. Johan has suggested that this sort of thing makes the proofs harder to maintain. What is the argument for termgolfing this proof? It will in future be a PR to mathlib I suspect. @Mario Carneiro ?

[Mario Carneiro]

I think that golfing it into term mode doesn't really affect its maintainability in any particular direction

[Mario Carneiro]

but it does make it shorter

[Mario Carneiro]

there is a small compile time advantage for using less tactics, but it's more of a rounding error. Mostly I think it is just more tidy to get more done in less space

[Kevin Buzzard]

lemma local_of_unique_nonzero_prime' (R : Type u) [comm_ring R]
(h : ∃! P : ideal R, P ≠ ⊥ ∧ is_prime P) : local_ring R :=
let ⟨P, ⟨hPnonzero, hPnot_top, _⟩, hPunique⟩ := h in
local_of_unique_max_ideal ⟨P, ⟨hPnot_top,
  maximal_of_no_maximal _ _ $ λ M hPM hM, ne_of_lt hPM $ (hPunique _ ⟨ne_bot_of_gt hPM, is_maximal.is_prime hM⟩).symm⟩,
  λ M hM, hPunique _ ⟨λ (h : M = ⊥), hPnot_top $ hM.2 _ (h.symm ▸ (bot_lt_iff_ne_bot.2 hPnonzero : ⊥ < P) : M < P), is_maximal.is_prime hM⟩⟩

I did it (with Kenny helpnig me: rintro rfl -> stupid triangle)

[Mario Carneiro]

I got this:

lemma local_of_unique_nonzero_prime (R : Type u) [comm_ring R]
  (h : ∃! P : ideal R, P ≠ ⊥ ∧ is_prime P) : local_ring R :=
local_of_unique_max_ideal begin
  rcases h with ⟨P, ⟨hPnonzero, hPnot_top, _⟩, hPunique⟩,
  refine ⟨P, ⟨hPnot_top, _⟩, λ M hM, hPunique _ ⟨_, is_maximal.is_prime hM⟩⟩,
  { refine maximal_of_no_maximal (λ M hPM hM, ne_of_lt hPM _),
    exact (hPunique _ ⟨ne_bot_of_gt hPM, is_maximal.is_prime hM⟩).symm },
  { rintro rfl,
    exact hPnot_top (hM.2 P (bot_lt_iff_ne_bot.2 hPnonzero)) },
end

[Kevin Buzzard]

Mario Carneiro said:

I think that golfing it into term mode doesn't really affect its maintainability in any particular direction

@Johan Commelin do you agree with this?

[Mario Carneiro]

notably it's not entirely term mode because rcases is great

[Mario Carneiro]

rintro rfl is great too

[Mario Carneiro]

some of the best term mode techniques are in tactic mode

[Mario Carneiro]

I think that refine is a nice middle ground here. You can chop a term mode proof into chunks where you have as much term mode proof as fits in one refine line

[Kevin Buzzard]

elaboration of local_of_unique_nonzero_prime took 168ms
elaboration of local_of_unique_nonzero_prime' took 31.2ms

[Johan Commelin]

I don't have an opinion...

[Mario Carneiro]

Like I said: term mode is faster but they are both fast if you aren't using "real" tactics

[Mario Carneiro]

You can of course write slow term mode proofs, but all other things being equal term mode proofs are faster

[Kevin Buzzard]

This isn't Mario's proof, this is my original proof v my golfification

[Mario Carneiro]

I just golfed your proof

[Kevin Buzzard]

Mario's proof doesn't compile because he had to guess what maximal_of_no_maximal was

[Kenny Lau]

slow term mode proofs happen with unoptimal typeclass inference

[Mario Carneiro]

I guessed what maximal_of_no_maximal was

[Kevin Buzzard]

/-- If P is not properly contained in any maximal ideal then it is not properly contained
  in any proper ideal -/
lemma maximal_of_no_maximal (R : Type u) [comm_ring R] (P : ideal R)
(hmax : ∀ m : ideal R, P < m → ¬is_maximal m) (J : ideal R) (hPJ : P < J) : J = ⊤ :=
begin
  by_contradiction hnonmax,
  rcases exists_le_maximal J hnonmax with ⟨M, hM1, hM2⟩,
  exact hmax M (lt_of_lt_of_le hPJ hM2) hM1,
end

[Mario Carneiro]

theorem ideal.maximal_of_no_maximal {R} [comm_ring R] {P : ideal R}
  (H : ∀ M, P < M → ¬ is_maximal M) : ∀ (J : ideal R), P < J → J = ⊤ := sorry

[Mario Carneiro]

Why are R and P explicit?

[Kevin Buzzard]

because I wrote it 30 minutes ago and wasn't thinking

[Mario Carneiro]

same in this proof

[Kevin Buzzard]

OK got it

[Kevin Buzzard]

elaboration of local_of_unique_nonzero_prime'' took 80.1ms

[Mario Carneiro]

that's my proof?

[Kevin Buzzard]

Yes

[Kenny Lau]

I guess rcases is the culprit

[Mario Carneiro]

I think what you are seeing is that there is overhead per tactic parse and call

[Mario Carneiro]

we've seen some of this in kenny's X is slow tests

[Mario Carneiro]

I don't think that the timing here is worth sweating over

[Kenny Lau]

but isn't tactic parse part of the "parsing" time?

[Mario Carneiro]

Honestly I have no idea, profiling times are really inaccurate and hard to interpret

[Kevin Buzzard]

And there's no simple way to find out how long something actually takes, right?

[Kevin Buzzard]

Anyway, which version goes in mathlib?

[Mario Carneiro]

I'm obviously biased toward my own version. I think the full term mode version has a bit too many things going on at once; in particular the type ascriptions suggest that the proof does not really proceed in left to right textual order and needs some elaboration hints

[Mario Carneiro]

so that's where I would normally cut it up into multiple refine blocks

[Mario Carneiro]

your term mode proof doesn't compile for me, is local_ring a prop now?

[Mario Carneiro]

I guess the type ascriptions are there in this proof just to show that you can do rw using the funny arrow

[Mario Carneiro]

I think if you have to go out of your way to do something in term mode it's not worth it. It is a space saver if you are only doing apply/intro/split/exact but for most other things it's not worth it

[Mario Carneiro]

In particular I think that obtain/rcases looks better than the term mode equivalent using Exists.rec_on or what have you. If you can do it with let <...> or \lam <...> then that's fine, although rcases can do some things that destructuring let/lambda can't

[Mario Carneiro]

And rw has no real term mode equivalent (the funny arrow doesn't even come close)

[Mario Carneiro]

For the everyday fast compiling mathlib proof I recommend some combination of these tactics. If you venture into other tactics like simp, ring, linarith, or tauto then tactic compile time becomes a serious factor