## Stream: maths

### Topic: tactic or term mode proof?

#### Kevin Buzzard (Jun 30 2020 at 14:07):

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 (Jun 30 2020 at 14:08):

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

#### Mario Carneiro (Jun 30 2020 at 14:08):

but it does make it shorter

#### Mario Carneiro (Jun 30 2020 at 14:14):

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 (Jun 30 2020 at 14:27):

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 (Jun 30 2020 at 14:27):

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 (Jun 30 2020 at 14:28):

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 (Jun 30 2020 at 14:28):

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

#### Mario Carneiro (Jun 30 2020 at 14:28):

rintro rfl is great too

#### Mario Carneiro (Jun 30 2020 at 14:29):

some of the best term mode techniques are in tactic mode

#### Mario Carneiro (Jun 30 2020 at 14:30):

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 (Jun 30 2020 at 14:31):

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


#### Johan Commelin (Jun 30 2020 at 14:31):

I don't have an opinion...

#### Mario Carneiro (Jun 30 2020 at 14:31):

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

#### Mario Carneiro (Jun 30 2020 at 14:32):

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

#### Kevin Buzzard (Jun 30 2020 at 14:32):

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

#### Kevin Buzzard (Jun 30 2020 at 14:33):

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

#### Kenny Lau (Jun 30 2020 at 14:33):

slow term mode proofs happen with unoptimal typeclass inference

#### Mario Carneiro (Jun 30 2020 at 14:33):

I guessed what maximal_of_no_maximal was

#### Kevin Buzzard (Jun 30 2020 at 14:33):

/-- 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
rcases exists_le_maximal J hnonmax with ⟨M, hM1, hM2⟩,
exact hmax M (lt_of_lt_of_le hPJ hM2) hM1,
end


#### Mario Carneiro (Jun 30 2020 at 14:33):

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 (Jun 30 2020 at 14:34):

Why are R and P explicit?

#### Kevin Buzzard (Jun 30 2020 at 14:34):

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

#### Mario Carneiro (Jun 30 2020 at 14:34):

same in this proof

OK got it

#### Kevin Buzzard (Jun 30 2020 at 14:35):

elaboration of local_of_unique_nonzero_prime'' took 80.1ms


that's my proof?

Yes

#### Kenny Lau (Jun 30 2020 at 14:35):

I guess rcases is the culprit

#### Mario Carneiro (Jun 30 2020 at 14:35):

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

#### Mario Carneiro (Jun 30 2020 at 14:36):

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

#### Mario Carneiro (Jun 30 2020 at 14:37):

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

#### Kenny Lau (Jun 30 2020 at 14:39):

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

#### Mario Carneiro (Jun 30 2020 at 14:40):

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

#### Kevin Buzzard (Jun 30 2020 at 14:41):

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

#### Kevin Buzzard (Jun 30 2020 at 14:41):

Anyway, which version goes in mathlib?

#### Mario Carneiro (Jun 30 2020 at 14:43):

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 (Jun 30 2020 at 14:43):

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

#### Mario Carneiro (Jun 30 2020 at 14:44):

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

#### Mario Carneiro (Jun 30 2020 at 14:49):

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

#### Mario Carneiro (Jun 30 2020 at 14:51):

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 (Jun 30 2020 at 14:52):

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 (Jun 30 2020 at 14:54):

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

#### Mario Carneiro (Jun 30 2020 at 14:55):

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

Last updated: May 10 2021 at 06:13 UTC