Instances on terms

Stream: mathlib4

[Johan Commelin]

@Yakov Pechersky during the meeting you are arguing that typeclasses on terms should be replaced by bespoke tactics and auto_params. But what if these typeclasses are interacting? I don't have an example right now, but I'm sure they exist.

[Yakov Pechersky]

As in, some prop class requires some other prop class? Situations where the typeclass system needs access to a proof to construct some other instance. That's a good point.

My mental model was about classes like Filter.NeBot, Ideal.IsPrime, Ideal.IsTwoSided, ones where it's not clear when to have the argument as an explicit vs instance parameter. For example, IsPrime has various instances that flow in a more complex direction, like docs#Ideal.IsPrime.smul. Many lemmas about prime ideals take the argument as an instance argument rather than an explicit one. It basically is a way to not have to rely on include and omit.

Where my mental model particularly breaks down, as discussed in the call, was where we construct data from the prop class, like when Ideal.IsMaximal implies Field of the quotient by the ideal.

Like I mentioned in the call, a similar existing pattern of relying on tactics that use/resolve based on some underlying typeclass-like search occurs in nontriviality, positivity, or fun_prop.

[Damiano Testa]

Re the discussion about instances on terms, I also have a funny feeling about them. In particular, I am not sure how I feel about docs#Subgroup.Normal: I have a very ambiguous perspective where I can clearly see it being inferred by the typeclass system, but I can also see it as something where I would expect to have to prove something myself.

[Edward van de Meent]

and of course, since you need it to prove the quotient is a group, it has to have at least as much 'class'-ness as Group itself

[Notification Bot]

5 messages were moved here from #general > Mathlib community meetings by Damiano Testa.

[Jovan Gerbscheid]

I think auto_param is still not supported by some basic tactics like apply, so this would need to be improved if we are going to use auto_param more.

Should type class search be able to run auto_params?

[Yakov Pechersky]

And auto_param does not work nicely with simp either, because simp can't run those tactics

[Jovan Gerbscheid]

Do you mean there is a fundamental reason why simp can't fun those tactics? Or just that it hasn't been implemented?

[Yakov Pechersky]

I don't know all the details, but as discussed on the community call, I think the issue that when simp is trying to solve side goals for lemma usage, it doesn't run inside TacticM, so can't run auto_params.

[Kyle Miller]

A big reason simp that doesn't run auto-params is caching. Simp needs to know dischargers are "well-behaved" to be able to determine whether the simp results are cacheable. Performance suffers greatly without the simp cache. This isn't to say that there couldn't be an option to have simp run auto-params, but it can't be the default. Maybe there could be an intermediate option of "run well-behaved auto-params" one day.

There's no problem running tactics from within simp (and indeed you can run tactics using (disch := ...) argument), since SimpM is on top of MetaM, and it's easy enough to evaluate a tactic script from there.

[Eric Wieser]

I'm guessing "well-behaved" does not include things like

theorem transpose_of {m} (elems : Fin m → Fin n → α) {elemsT : Fin n → Fin m → α}
    -- this autoparam assigns the `elemsT` metavariable
    (h : (of elems)ᵀ = of elemsT := by transpose_of_tac) :
    (of elems)ᵀ = of elemsT := h

[Yakov Pechersky]

Regarding the discharger, current configurations would still require the discharger to be declared up front, not inferred on the fly based on the lemmas involved, correct?

[Yakov Pechersky]

And the discharger codepath doesn't do any goal shape matching to route to the appropriate tactic, it relies on the tactics themselves to fail fast?

[Kyle Miller]

@Yakov Pechersky I've confused things a little bringing "discharger" into it, but dischargers are a good point of comparison for what it would mean for simp to apply auto-params.

Conceptual model for an auto-param-respecting simp:

• (True currently) Simp has a discharger that it applies to Prop simp lemma hypotheses. The default one is docs#Lean.Meta.Simp.dischargeDefault?, but it can be overridden. Discharging is attempted after instance synthesis if the argument's type is a class. The discharger is like a default auto-param tactic to use for hypotheses.
• If a hypothesis has an auto-param, it could override the discharger. Simp would need to be able to determine whether the auto-param is a "well-behaved" discharger.

(By the way, here's what the default discharger does: It first has some logic about "equation theorem hypotheses" that invokes a version of assumption and cases on eq/heq, then it does a recursive simp, and finally it checks to see if the goal is solved by both trying Eq.rfl at reducible transparency and seeing if the expression is True.)

This is all to say: no, there does not need to be a single discharger up front. It's all up to docs#Lean.Meta.Simp.synthesizeArgs to decide how to try to synthesize arguments to matching simp lemmas.

[Violeta Hernández]

I used to be a member of the "instances for types" crowd, but working on game theory has completely won me to the other side. Being able to automatically find proofs for stuff like Numeric (a * y + x * b - a * b) is just way too convenient.

[Violeta Hernández]

Though if this can be done with autoparams (and if there's other benefits to this switch) I'd be willing to switch to that.

[Violeta Hernández]

(for context: Numeric is a predicate on games, and it's closed under addition, subtraction, multiplication, division, ω-exponentiation, casting from naturals, integers, rationals, real numbers, ordinals...)

[Eric Wieser]

I'd claim that typeclasses are for when the proof is always structural, not just often structural. You could of course get a long way with making even and odd type classes, but that's not going to do you any favors for Even (n * (n + 1))