flexible vs rigid tactics

Stream: mathlib4

[Yaël Dillies]

I think all the tactic combinators like done, skip, try, any_goals, all_goals should be allowed

[Damiano Testa]

Ok, I think that the way in which the "following tactic" is selected means that the tactic following the combinator will be flagged as well (unless it is whitelisted). This is the intended behaviour, right? I.e., the combinator should not be a stop-gag, just a see-through tactic that passes on the decision to the next one.

Do you agree?

[Yaël Dillies]

I don't really like the current logic of your linter. I think a more pertinent logic would be to mark locations (hypotheses/goals) as "non-squeezedly simped" and forbidding "rigid" tactics from using those assumptions

[Yaël Dillies]

Eg this should be allowed:

simp at h0
rw [h1] at h2

but neither of these should

simp at h0
rw [h1] at h0

simp at h0
rw [h0] at h1

[Damiano Testa]

Yaël, I do not really understand what you are proposing... what is a "non-squeezedly simped" location?

[Damiano Testa]

Maybe I should specify: currently, the "next tactic" is "the next tactic that acts on a goal that a simp produced".

[Damiano Testa]

It is not the next tactic that you type.

[Damiano Testa]

(or rather, it need not be, although often it will be.)

[Yaël Dillies]

That sounds really brittle. That means that

simp
rw [h]

is forbidden but

simp
ring
rw [h]

is not

[Yaël Dillies]

Do you understand my proposition better now?

[Damiano Testa]

Yes, I think that I understand. You would like something like a cache of "after simp locations" that are only allowed actions by "flexible" tactics, including simp, ring,..., but, for instance, not rw.

[Damiano Testa]

I wonder whether this should come after a first implementation of the linter, though...

[Damiano Testa]

This seems more like a "non-terminal flexible tactic follower" linter to me.

[Yaël Dillies]

I think it's worth exploring! If we merge your linter now, we're at risk of teachings seas of beginners the wrong style

[Damiano Testa]

This is certainly a very good suggestion, but I think that focusing on simp might already be productive.

[Yaël Dillies]

Damiano Testa said:

This seems more like a "non-terminal flexible tactic follower" linter to me.

Yes, that's exactly what it is, because simp is really no special here

[Damiano Testa]

Yaël Dillies said:

I think it's worth exploring! If we merge your linter now, we're at risk of teachings seas of beginners the wrong style

Ok, this is possible, but it is also possible that they can then learn a better style later on.

[Yaël Dillies]

Mathport experience would like to disagree...

[Yaël Dillies]

I claim that the correct implementation is so different to your current one that it's not worth trying to incrementally get to the correct one from yours

[Damiano Testa]

Ok, so maybe the tactics that I am placing in the whitelist should be all allowed and should never be followed by anything else.

This is probably not that hard to implement, although I have not really given this much thought.

[Yaël Dillies]

Also, you already ripped out most of the benefits from your linter by PRing fixes to the errors you found locally

[Yaël Dillies]

More errors will come, but only with a better logic

[Damiano Testa]

Yaël Dillies said:

I claim that the correct implementation is so different to your current one that it's not worth trying to incrementally get to the correct one from yours

The current suggestion is very far from v1 of the linter, not, I think, from v2 that I am testing right now.

[Yaël Dillies]

I think you should not allow specific tactics but instead disallow specific rigid tactics

[Damiano Testa]

Yaël Dillies said:

Also, you already ripped out most of the benefits from your linter by PRing fixes to the errors you found locally

Very few of those PRs have been merged and have conflicts now. I am planning to close them, if the newer version of the linter is definitely an improvement.

[Damiano Testa]

Yaël Dillies said:

I think you should not allow specific tactics but instead disallow them

As I am thinking of this right now, there are only two categories, right? The category of tactics that can only act on goals on which a flexible tactic has not yet acted, and the flexible tactics, right? You are saying that a tactic if automatically flexible, unless it is blacklisted?

[Yaël Dillies]

Nono, sorry I clarified

[Damiano Testa]

(the two perspective are easy to implement, it seems to be that we are simply deciding what the default category of each tactic is)

[Yaël Dillies]

The default should be rigid. This is what I'm claiming

[Damiano Testa]

Ok, I agree. By default, everything is like rw (which I consider the default rigid tactic).

[Damiano Testa]

And if a goal/location has been produced/touched by a flexible tactic, then only flexible tactics are allowed to touch it.

[Yaël Dillies]

... or use it!

[Damiano Testa]

(the "location part" I am not too sure about -- the current linter is implemented thinking about goals, but the linting framework does have access to the context.)

[Yaël Dillies]

Actually, it's not merely "touched by a flexible tactic" that's bad but "potentially touched"

[Damiano Testa]

"potentially touched" might include everything, though? Do you mean that simp_all makes everything flexible, even if it actually just modifies one hypothesis?

[Yaël Dillies]

So the correct rule is:

Only flexible tactics are allowed to target or use locations which have been previously been targeted by flexible tactics (regardless of whether said flexible tactics actually changed those locations)

[Yaël Dillies]

Yes, simp at * means that no rigid tactic can target anything in that context anymore. If you then do have := something_not_from_context, that can be touched by a rigid tactic however,

[Damiano Testa]

I understand your point, although I wonder whether this requires knowledge of what each tactic could do... E.g., when you see a simp, you should figure out whether it is at and what the at locations are. I think that this would be very hard to maintain as a linter.

[Yaël Dillies]

Yes, but luckily there aren't many flexible tactics

[Yaël Dillies]

Regardless, information on targeted locations should be part of the tactic framework long term

[Damiano Testa]

To avoid scope-creep, what do you think of focusing on goals, rather than locations, to begin with?

[Yaël Dillies]

I don't see how that could give you anything sensible

[Yaël Dillies]

There are too many ways the goal-based heuristic could go wrong

[Damiano Testa]

Yaël Dillies said:

There are too many ways the goal-based heuristic could go wrong

While this is true, I also think that for most proofs, the goal heuristic is actually good.

[Yaël Dillies]

Yes, but I really really do not want false linter positives

[Damiano Testa]

(Also, I am aware of my abilities and, while I can see myself coding the linter with locations and all, I can also see the result as being unusably slow...)

[Damiano Testa]

Yaël Dillies said:

Yes, but I really really do not want false linter positives

You can view it as "Every silencing of the linter is a todo"...

[Damiano Testa]

I am going to move all this conversation to a separate topic, is that alright?

[Damiano Testa]

(assuming that I can...)

[Notification Bot]

49 messages were moved here from #mathlib4 > simp followers by Damiano Testa.

[Damiano Testa]

Ok, to seriously implement this rigid vs flexible linter, I need to see what kind of information hides in the MetavarContext that the linter offers.

[Damiano Testa]

Just to be clear, what you are suggesting is that, after a flexible tactic that potentially changes all locations, that metavariable can (almost) only be closed by flexible tactics: e.g. assumption, tauto, linarith,..., have+something else,... and have or something similar is the only way in which rigid tactics can play again there, and then only on the new hypotheses that have been introduced.

[Damiano Testa]

I agree that this would make proofs much less brittle. It may also be somewhat of an added burden to write proofs in this "flexible-vs-rigid" style.

[Yaël Dillies]

I don't think it will be much burden since this is already how we write most proofs

[Damiano Testa]

Some iteration of the "non-terminal simp" linter produces the output below. Currently, the linter only looks at simp and simp_all, but this is easy to expand. What the linter is supposed to do is check if some tactics that are likely to break with small changes to the simp output follow simp.

The linter makes an effort to flag simp at h; rw [h] as well as simp at h; rw at h.

The lnter should not flag simp at h1; rw [h2] at h3, assuming that h1 is different from h2, h3.

Linted

-- Mathlib/Init/Data/Nat/Bitwise.lean
    cases bodd n <;> simp [cond, not]
    · rw [Nat.add_comm]

-- Mathlib/Control/Applicative.lean
  simp! [map, Seq.seq, functor_norm]
  rw [commutative_map]

-- Mathlib/Data/Nat/Defs.lean
  · by_contra h'; push_neg at h'; simp [Nat.le_zero] at h'
    obtain rfl | rfl | h' := h'

-- Mathlib/Data/List/ReduceOption.lean
  induction l <;> simp [*]
  rw [@eq_comm _ none, ← Option.not_isSome_iff_eq_none, Decidable.imp_iff_not_or]

-- Mathlib/Order/Compare.lean
  by_cases xy:x ≤ y <;> by_cases yx:y ≤ x <;> simp [cmpLE, *, Ordering.swap]
  cases not_or_of_not xy yx (total_of _ _ _)

-- Mathlib/Data/Nat/PSub.lean
  cases s : psub m n <;> simp [eq_comm]
  · show m < n

-- Mathlib/Tactic/Sat/FromLRAT.lean
    induction as₁ with simp
    | cons b as₁ ih => exact fun n bs ↦ ih (n+1) _ (Nat.succ_add ..) _

-- Mathlib/Order/Iterate.lean
  apply hf.seq_le_seq n <;> intros <;>
    simp [iterate_succ', -iterate_succ, comp_apply, id_eq, le_refl]
  case hx => exact H _

-- Mathlib/Data/Nat/Bitwise.lean
  have h4 x : (x + x + 1) / 2 = x := by rw [← two_mul, add_comm]; simp [add_mul_div_left]
  cases a <;> cases b <;> simp [h1, h2, h3, h4] <;> split_ifs

-- Mathlib/Data/Nat/Size.lean
  induction' n with n IH <;> simp [shiftLeft'] at h ⊢
  rw [size_bit h, Nat.add_succ]

-- Mathlib/Data/List/Lattice.lean
    by_cases h : b ∈ l₂ <;> simp [h]
    exact bagInter_nil_iff_inter_nil l₁ l₂

-- Mathlib/Analysis/MeanInequalities.lean
    le_of_lt hpq.symm.pos, le_of_lt hpq.symm.one_div_pos] at this
  convert this using 1 <;> [skip; congr 2] <;> [skip; skip; simp; skip; simp] <;>

-- Mathlib/RingTheory/Polynomial/Cyclotomic/Eval.lean
      and_self_iff]
  · constructor <;> intro <;> linarith

-- Mathlib/MeasureTheory/Integral/MeanInequalities.lean
    · simp [hi₀]
      have h2p : ∀ i ∈ s, p i = 0 := by

-- Mathlib/Geometry/Euclidean/Sphere/Power.lean
    simp_all only [Classical.not_not, one_smul]
  exacts [hab (vsub_left_cancel hab₁).symm, hcd (vsub_left_cancel hcd₁).symm]

-- Mathlib/MeasureTheory/Function/LpSeminorm/TriangleInequality.lean
  · simp [LpAddConst_of_one_le h'p]
    exact snorm_add_le hf hg h'p

-- Mathlib/Analysis/InnerProductSpace/PiL2.lean
  -- Porting note: `LinearIsometryEquiv.trans_assoc` doesn't trigger in the `simp` above
  rw [LinearIsometryEquiv.trans_assoc]

-- Mathlib/MeasureTheory/Function/LpSpace.lean
  · simp [q_zero]
    by_cases p_zero : p = 0

-- Mathlib/Analysis/Matrix.lean
  simp [unitOf]
  split_ifs with h

-- Mathlib/MeasureTheory/Function/SimpleFuncDenseLp.lean
  simp [edist_comm (0 : E), edist_eq_coe_nnnorm] at this
  exact mod_cast this

-- Mathlib/NumberTheory/LegendreSymbol/JacobiSymbol.lean
  interval_cases h : b % 8 <;> simp_all <;>
    exact absurd (hb2 ▸ h ▸ Nat.mod_mod_of_dvd b (by decide : 2 ∣ 8)) zero_ne_one

-- Mathlib/Probability/Process/Stopping.lean
    · set_option tactic.skipAssignedInstances false in simp [hij]
      convert @MeasurableSet.empty _ (Filtration.seq f j)

-- Mathlib/Probability/Kernel/Disintegration/Density.lean
  · simp [h]
    by_cases h' : κ a (countablePartitionSet n x ×ˢ univ) = 0

-- Mathlib/Analysis/NormedSpace/Star/ContinuousFunctionalCalculus/Instances.lean
  · simp [hr'] at hx ⊢
    exact hx.symm.le

-- Mathlib/NumberTheory/NumberField/CanonicalEmbedding.lean
    Prod.snd_neg, Complex.norm_eq_abs] at hx ⊢
  convert hx using 3

[Damiano Testa]

Let me know if something from the output above looks like something that the linter should handle differently (i.e. should allow it).

[I gave one line of context before each flag, which sometimes may not be enough to reconstruct what the issue was.]

[Yaël Dillies]

I'm not sure about the induction as with simp thing. Is simp not an identifier there?

[Yaël Dillies]

I assume that in the RingTheory.Polynomial Cyclotomic.Eval example the above tactic is a simp operating on the goal that's focused?

[Yaël Dillies]

simp [q_zero]
by_cases p_zero : p = 0

should be legal since by_cases doesn't operate on the goal.

[Yaël Dillies]

Similarly for the Probability.Kernel.Disintegration.Density one

[Ruben Van de Velde]

No, induction as with simp runs simp on each of the new subgoals

[Yaël Dillies]

That's quite confusing given the induction' syntax :thinking:

[Damiano Testa]

Yaël Dillies said:

simp [q_zero]
by_cases p_zero : p = 0

should be legal since by_cases doesn't operate on the goal.

Yes, there are still some rough edges around flagging simp when a new goal is created by the tactic.

However, what I pasted there is the first failure in each file with basically no extra filter, so this is promising!

[Damiano Testa]

The "flexible" linter is essentially ready: #11821

The PR above only defines the linter and adds a test file: the linter is not running on any file other than the test.

There is a separate PR where I added the linter to most of mathlib: you can find it here: #11822.

Here is a gist with the linter warnings from a separate run: there are approximately 230 files that the linter flags. I scanned quickly a few of them and the linter seems to be doing its job!

[Damiano Testa]

One situation that the linter does not handle correctly is the following:

example (h : 0 = 0) : True := by
  simp at h  -- h : True
  assumption

Clearly, assumption is using h, but since h is not part of the syntax of the tactic, the linter is unaware of that.

The linter does flag

example (h : 0 = 0) : True := by
  simp at h  -- h : True
  exact h

[Damiano Testa]

Btw, if anyone feels like going through the gist above and knock down a few non-terminal simps, I would be more than thrilled!

[Damiano Testa]

(Also, while the whole setup would allow tactics other than simp to be flexible, I am only linting simp at the moment: already as it, it will be quite a lot of work to make mathlib compliant.)

[Damiano Testa]

While going through some of the lints, this is the most controversial that I found so far: is the pattern

  ... <;> simp <;> split_ifs <;> simp

acceptable? What if the final simp is exact or rw?

[Damiano Testa]

I personally am not a huge fan of the <;>-combinator, because I usually value more clarity than saving space and I find that it more often obscures, rather than explain.

In some cases, my solution has been to unlint, in others to squeeze, in others still to split the <;> combinators, depending on context.

[Yaël Dillies]

Damiano Testa said:

While going through some of the lints, this is the most controversial that I found so far: is the pattern

  ... <;> simp <;> split_ifs <;> simp

acceptable? What if the final simp is exact or rw?

Surely that's fine iff the final tactic is flexible?

[Damiano Testa]

Well, if could in theory be resolved by a better simp and then split_ifs would fail.

[Damiano Testa]

I am not sure that I consider split_if flexible. Are you saying that split_ifs should simply be allowed as a simp follower?

[Yaël Dillies]

I think split_ifs is neither flexible nor rigid. It's just a combinator

[Yaël Dillies]

Damiano Testa said:

Well, if could in theory be resolved by a better simp and then split_ifs would fail.

In that case, you just remove the combinator, which should be a pretty obvious step to take

[Mario Carneiro]

Damiano Testa said:

Well, if could in theory be resolved by a better simp and then split_ifs would fail.

Most flexible tactics have this behavior

[Mario Carneiro]

simp can always produce something that the next tactic can't handle, flexible or otherwise

[Mario Carneiro]

but it's not dependent on the nitty gritty details of the goal, so it's flexible

[Damiano Testa]

Right, I agree that this is the behaviour of most flexible tactics, and the linter is trying to mitigate this by only allowing flexible tactics to follow flexible tactics. There are a lot of rigid tactics following flexible ones already as is, so I am trying to find some common ground...

[Damiano Testa]

Anyway, I'll add split_ifs to the ignored list, which means that the linter would

• not complain on simp <;> split_ifs <;> simp but
• would complain on simp <;> split_ifs <;> rw

[Damiano Testa]

Another question: should this proof be allowed, or should simp be squeezed?

  by simp [multiplicity, rootMultiplicity, Part.Dom]; congr; funext; congr

Note that there is an underlying decision that congr is allowed as a simp follower, so really the question is whether the funext jammed in there is acceptable or whether it is reason for preferring a simp only instead.

[Ruben Van de Velde]

The last congr solves the goal? Too bad simp can't handle it on its own

[Damiano Testa]

Yes, this is the full declaration:

-- Mathlib/Algebra/Polynomial/Div.lean
theorem rootMultiplicity_eq_multiplicity [DecidableEq R] [@DecidableRel R[X] (· ∣ ·)]
    (p : R[X]) (a : R) :
    rootMultiplicity a p =
      if h0 : p = 0 then 0 else (multiplicity (X - C a) p).get (multiplicity_X_sub_C_finite a h0) :=
  by simp [multiplicity, rootMultiplicity, Part.Dom]; congr; funext; congr
#align polynomial.root_multiplicity_eq_multiplicity Polynomial.rootMultiplicity_eq_multiplicity

[Damiano Testa]

and this is the goal before the last congr

Nat.find ⋯ = Nat.find ⋯

:man_facepalming:

[Damiano Testa]

Is it expected that adding

set_option pp.deepTerms true/false in -- I tried both

before the declaration, I still see the ...?

[Yaël Dillies]

Damiano Testa said:

and this is the goal before the last congr

Nat.find ⋯ = Nat.find ⋯

:man_facepalming:

I feel like the predicate argument to docs#Nat.find should be explicit

[Kevin Buzzard]

Damiano Testa said:

Is it expected that adding

set_option pp.deepTerms true/false in -- I tried both

before the declaration, I still see the ...?

I've been using set_option pp.proofs.threshold 37 to expand ....

[Damiano Testa]

Thanks Kevin! This is the goal:

⊢ Nat.find (multiplicity_X_sub_C_finite a (Eq.mpr_not (Eq.refl (p = 0)) x✝)) =
  Nat.find
    (id (Eq.refl (PartENat.find fun n ↦ ¬(X - C a) ^ (n + 1) ∣ p)) ▸
      multiplicity_X_sub_C_finite a (Eq.mpr_not (Eq.refl (p = 0)) x✝))

[Kevin Buzzard]

(I tried 0 and it didn't work so I tried 37 and it worked great)

[Yaël Dillies]

I've just noticed that something we left out of the discussion is that tactics have different flexibility regarding their inputs and outputs eg in simp [ha] at hb we have

• ha is a rigid input
• hb is a flexible input
• hb is a flexible output

[Yaël Dillies]

And, perhaps more subtly, ha is a rigid output in have ha : Foo := by simpa using hb but a flexible output in have ha := by simpa using hb

[Yaël Dillies]

I'm not quite sure how to classify ha in intermediate situations like have ha : Foo _ := by simpa using hb. I guess it should be considered rigid even if it allows have ha : _ := by simpa using hb to leave ha rigid

[Damiano Testa]

On the front of the flexible vs rigid, I was pretty happy with the linter output. However, I personally find that there is no uniformly good way of pleasing the linter: replacing simp [tacs] with

• the output of simp? [tacs] hides what tacs is and is often too verbose;
• simp? [tacs] says ... is again very verbose and also means that you still have to update the list of tactics when the simp-set changes;
• suffices ... can again be very verbose, when the goals are long.

Overall, while a non-terminal simp (or rigid tactic following a flexible one more generally) is not great for stability, I am not sure that the alternatives that are currently available are really an net improvement.

[Damiano Testa]

I have been thinking about a possible alternative. Here is an initial idea.

If a simp no longer works on a branch, but was present in master, then squeezing it in master would tell you what to use. How about we write a tactic squeeze_me_earlier that takes a tactic as input (initially just simp) and

• checks out master,
• downloads the cache,
• attempts to find the correct simp;
• runs simp? recording the output;
• checks out the branch in development;
• says Try this: [recorded output of `simp?`].

This could also be something that runs in CI, possibly applying to simps that break downstream of your changes, maybe in an untouched file, to begin with.

[Michael Rothgang]

#15101 fixes about a hundred warnings from the "flexible tactic" linter, in a way that is hopefully non-controversial. #15102 was also found by the linter, and is a small performance improvement in itself.

[Michael Rothgang]

#15130 has a few more

[Michael Rothgang]

#15318 has a few more

[Michael Rothgang]

Update: I have finished going through all warnings on mathlib. #13812 either disables the linter with a comment, or fixes its warning. The fixes have been split into #15318.
For the manual suppressions, I can see a few trends

• a category theory pattern: simp followed by coherence (I have always allowed the linter)
• a number of errors are about simp followed by erw, with a comment pointing to lean4#2644: I've left those as is, as fixing the underlying issue will also fix this linter warning
• <;> simp (say, for two goals created by by_cases or induction), followed by some further proof. The simp sets are usually different, and sometimes long enough be unreadable when spelled out
• there are surely more, for which I'd need to look at the suppressions myself

[Michael Rothgang]

I just merged master and fixed CI again: compared to master, enabling the flexible linter requires

• two minor fixes (three lines, will PR soon) and
• 187 individual linter suppressions (commented)
  To be honest, this number does not seem absurdly high --- just from the churn perspective, one could even enable the linter by default (with a clear note that this may be disabled easily).

[Michael Rothgang]

Out of these 187 exceptions,

• 14 are because of lean4#2644/related to simp and erw
• 5 are about simp followed by coherence
• 4 exceptions are about simp followed by exact, which cannot be combined into simpa
• most remaining exceptions are cases where either
  • the set of simp lemmas is long enough that squeezing it is ugly
  • simp is applied to several goals, often with different (and/or quite large) simp sets

[David Ang]

I'm not sure how flexible the flexible linter is, but do tactic patterns like field_simp; linear_combination go through with no complaints? I believe field_simp is just a juiced up version of simp and linear_combination is just a juiced up version of ring. I'm asking this because I use this pattern quite a lot in my files.

[David Ang]

I know that simp; ring is fine, but if field_simp is tagged as a simp but linear_combination is not tagged as a ring then it would complain, since linear_combination is not in the list of flexible tactics.

[Damiano Testa]

Neither field_simp, nor linear_combination are "flexible: this means that, by default, they are rigid. Hence, simp; field_simp counts as a non-terminal simp and the linter would flag it.

[Damiano Testa]

It is easy to add more tactics to the "flexible" list and maybe there is a case for field_simp to be flexible. I am not sure that linear_combination should count as flexible, though, since it is quite fixed to exact shapes, I think.

[Yaël Dillies]

I think of field_simp and linear_combination as flexible, FWIW

[Damiano Testa]

With linear_combination, also if it uses a hypothesis that has been the target of simp?

[Yaël Dillies]

Surely yes?

[Damiano Testa]

I view it as somewhat brittle, since that hypothesis could change with an increase/decrease in the simp-set and it is not clear that linear_combination would be able to cope.

[Damiano Testa]

But it is almost no work to make linear_combination and field_simp flexible, and I am happy to add them!

[David Ang]

I'd argue that they are flexible, unless you change their default normalisation (and I'm very guilty of this)

[Damiano Testa]

Ok, here is an example which is maybe not too contrived of why I am not completely convinced that linear_combination is flexible:

example (x y : ℤ) (h1 : x*y + 2*x = 1) (h2 : 2 * x = 2 * y) : x*y = -2*y + 1 := by
  --simp at h2  -- uncomment to break `linear_combination`
  linear_combination 1*h1 - h2

[Ruben Van de Velde]

Yeah, I don't think it is

[Damiano Testa]

Of course, any tactic could be broken by doing something different before it, so really everything is rigid.

[Ruben Van de Velde]

field_simp is a difficult one, though

[Damiano Testa]

But my mental model is that simp is "truly" flexible, while linear_combination is "somewhat flexible", but not so much.

[David Ang]

If this is the case, then arguably field_simp; linear_combination should be flagged, but it's not?

[Damiano Testa]

Something probably has to be done about field_simp, but I view field_simp as a "normalization" tactic: it should (in theory) produce a reliably equal result from a range of inputs, like norm_num: this, to me, makes it look like a tactic that can follow a flexible one and can be followed by whatever.

[Damiano Testa]

(Right now, though, I think that field_simp is purely rigid and cannot follow a flexible one.)

[Damiano Testa]

So, I think that field_simp; linear_combination is ok, the linter correctly does not flag it, but for the wrong reason! :smile:

[David Ang]

But doesn't field_simp do everything that simp does, except for three lemmas that surely doesn't make it a lot more flexible than simp? I'm now also confused about norm_num because isn't it just norm_num1; simp?

[Damiano Testa]

To give a little bit of extra context, the "flexible" linter started as a "non-terminal simp linter". It evolved in splitting tactics into "flexible" and "rigid": a "rigid" tactic cannot follow a "flexible" one, since the output of a flexible one is unreliable and could break the rest of the proof.

[Damiano Testa]

In development, some tactics actually take a variety of inputs and convert them to normal form, like norm_num: if you stray a little from the initial input, chances are that norm_num will return the same result.

[Damiano Testa]

Such tactics can more reliably be followed by rigid ones, since it would be a big jump to make them normalize to something different.

[Damiano Testa]

These tactics are "stoppers": they can follow a flexible one, since they can adapt to multiple outputs, but have "fewer" outputs, so can be followed by rigid ones.

[Damiano Testa]

In this context, there is always some discretion of "how big of a change you expect the typical change to be".

[Damiano Testa]

Of course, a big enough change will break whatever.

[David Ang]

Here is my concern: take your example above and replace simp with norm_num or field_simp, and they both break

[Damiano Testa]

But the kind of simp inside norm_num and field_simp is not "all simp lemmas", but "a curated list of lemmas, some that are simp, some that make sense in this context.

[Damiano Testa]

David Ang said:

Here is my concern: take your example above and replace simp with norm_num or field_simp, and they both break

Right, so I view this as evidence that linear_combination is "rigid". As for norm_num and field_simp, they of course can normalize to something different, but I view this as more rare.

[Damiano Testa]

If your point of view is "a change in the previous tactic may break the next", then nothing would be allowed.

[Yaël Dillies]

David Ang said:

If this is the case, then arguably field_simp; linear_combination should be flagged, but it's not?

Given that field_simp is meant as a preprocessor to tactics like ring and linear_combination, it would be very damageable to forbid field_simp; linear_combination!

[Damiano Testa]

Right, the example above with field_simp instead of simp breaks linear_combination, but it is unlikely that a working pair field_simp; linear_combination would break after a change in field_simp.

[Damiano Testa]

Whereas a working pair simp; linear_combination is less likely to continue working, as simp evolves.

[David Ang]

Right, but your "change" in field_simp (that is unlikely to break) refers exclusively to changes in field_simps

[Damiano Testa]

Yes, I expect field_simp to converge to some normal form that is "highly unlikely" to change: an expression of the form 2 * x / 2 should be normalized to x no matter how many times field_simp is reimplemented.

[Damiano Testa]

Whereas whether that same expression is simplified or not by a simp lemma depends more unreliably on the simp set.

[Damiano Testa]

That's why I consider field_simp; something_else "robust": the something_else is using a "field normal form". Something unusual has to have happened for the notion of "field normal form" to have changed.

[David Ang]

Maybe my concern is better phrased like this: currently we have tactics (e.g. field_simp or norm_num) that are basically (do something); simp, and you argue that we can put them before doing something rigid. On the other hand, I could may well do (do something); simp; (do something rigid), which should have identical behaviour but is flagged.

[Damiano Testa]

They are not a "free" simp, they are a "controlled simp".

[Damiano Testa]

You should view them more as simp onlys.

[David Ang]

How controlled are they? I don't know exactly how they're defined but the docs tell me e.g.: field_simp [hx, hy] is a short form for simp (disch := field_simp_discharge) [-one_div, -one_divp, -mul_eq_zero, hx, hy, field_simps], which is quite far from being a simp only?

[Damiano Testa]

From the doc-string of field_simp:

The goal of `field_simp` is to reduce an expression in a field to an expression of the form `n / d`
where neither `n` nor `d` contains any division symbol, just using the simplifier (with a carefully
crafted simpset named `field_simps`)

[Damiano Testa]

There are about 40 field_simps lemmas.

[David Ang]

Right, then shouldn't the implementation be closer to simp only [field_simps] rather than simp [field_simps]?

[Mario Carneiro]

I think David's point is that it does not use only

[Mario Carneiro]

likewise for norm_num

[Sébastien Gouëzel]

The field_simps set of lemmas is indeed added to the simpset when applying field_simp, but almost nothing is removed if I recall correctly, so adding new simp lemmas will definitely change the outcome of field_simp. In terms of rigidity, simp and field_simp should definitely be on the same line.

[Ruben Van de Velde]

Or should we change that? I'm not sure I want field_simp to go changing random things in my goal

[Ruben Van de Velde]

Or we could have both

[Damiano Testa]

Ok, so I can then make field_simp flexible and then linear_combination would not be allowed to follow it.

[Mario Carneiro]

field_simp only?

[Mario Carneiro]

you can already do this for norm_num

[Damiano Testa]

So only would mean "just field_simps (plus whatever you explicitly add)"?

[Damiano Testa]

That would probably be clearly a stopper tactic! :smile:

[David Ang]

Mario Carneiro said:

you can already do this for norm_num

You mean norm_num1? Or can we do norm_num only?

[David Ang]

I do think having field_simp only would be very nice, but I don't know how well this works in practice because if I remember correctly the 40 lemmas in field_simps doesn't actually do very much without calling all of simp

[Mario Carneiro]

David Ang said:

Mario Carneiro said:

you can already do this for norm_num

You mean norm_num1? Or can we do norm_num only?

Both. norm_num1 doesn't use the simplifier at all, and norm_num only uses the simplifier with the usual meaning of simp only