Zulip Chat Archive

Stream: maths

Topic: tactic or term mode proof?


view this post on Zulip 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 ?

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Jun 30 2020 at 14:08):

but it does make it shorter

view this post on Zulip 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

view this post on Zulip 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)

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip Mario Carneiro (Jun 30 2020 at 14:28):

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

view this post on Zulip Mario Carneiro (Jun 30 2020 at 14:28):

rintro rfl is great too

view this post on Zulip Mario Carneiro (Jun 30 2020 at 14:29):

some of the best term mode techniques are in tactic mode

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Johan Commelin (Jun 30 2020 at 14:31):

I don't have an opinion...

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Jun 30 2020 at 14:32):

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

view this post on Zulip Mario Carneiro (Jun 30 2020 at 14:33):

I just golfed your proof

view this post on Zulip 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

view this post on Zulip Kenny Lau (Jun 30 2020 at 14:33):

slow term mode proofs happen with unoptimal typeclass inference

view this post on Zulip Mario Carneiro (Jun 30 2020 at 14:33):

I guessed what maximal_of_no_maximal was

view this post on Zulip 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
  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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Jun 30 2020 at 14:34):

Why are R and P explicit?

view this post on Zulip Kevin Buzzard (Jun 30 2020 at 14:34):

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

view this post on Zulip Mario Carneiro (Jun 30 2020 at 14:34):

same in this proof

view this post on Zulip Kevin Buzzard (Jun 30 2020 at 14:34):

OK got it

view this post on Zulip Kevin Buzzard (Jun 30 2020 at 14:35):

elaboration of local_of_unique_nonzero_prime'' took 80.1ms

view this post on Zulip Mario Carneiro (Jun 30 2020 at 14:35):

that's my proof?

view this post on Zulip Kevin Buzzard (Jun 30 2020 at 14:35):

Yes

view this post on Zulip Kenny Lau (Jun 30 2020 at 14:35):

I guess rcases is the culprit

view this post on Zulip Mario Carneiro (Jun 30 2020 at 14:35):

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

view this post on Zulip Mario Carneiro (Jun 30 2020 at 14:36):

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

view this post on Zulip Mario Carneiro (Jun 30 2020 at 14:37):

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

view this post on Zulip Kenny Lau (Jun 30 2020 at 14:39):

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

view this post on Zulip Mario Carneiro (Jun 30 2020 at 14:40):

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

view this post on Zulip Kevin Buzzard (Jun 30 2020 at 14:41):

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

view this post on Zulip Kevin Buzzard (Jun 30 2020 at 14:41):

Anyway, which version goes in mathlib?

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Jun 30 2020 at 14:43):

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

view this post on Zulip Mario Carneiro (Jun 30 2020 at 14:44):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Jun 30 2020 at 14:54):

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

view this post on Zulip 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