Invertible and data

Stream: maths

[Yury G. Kudryashov]

Motivated by @Michael Stoll 's #14986. Why do we carry data in docs#Invertible ? Should we turn docs#IsUnit into a typeclass instead?

[Yury G. Kudryashov]

Alternatively, we can turn IsUnit into a typeclass and treat [Invertible _] the same way we treat Decidable: only use it if we need a computable invOf.

[Johan Commelin]

I think it was done because there are examples where you can compute, and it is nice if it works in those examples. For example some localizations like $\Z[1/2]$, where 2 is invertible, but you don't have all rational numbers. Or $\Z/8\Z$ where 3, 5, 7 are their own multiplicative inverses.

[Johan Commelin]

So I think it is worth looking into your 2nd suggestion. Where we have a data-carrying class that is used sparingly, and prop-class that is used for almost all the theory.

[Adam Topaz]

I think there is no obvious overlap here: docs#Units is essentially a bundled docs#Invertible and docs#IsUnit is the associated prop.

[Edward van de Meent]

• docs#Units

[Adam Topaz]

yeah, sorry!

[Yury G. Kudryashov]

Adam Topaz said:

I think there is no obvious overlap here: docs#Units is essentially a bundled docs#Invertible and docs#IsUnit is the associated prop.

IsUnit x is the same as Nonempty (Invertible x). What I'm trying to say is that we use a typeclass with subsingleton data (Invertible) as an assumption in theorems that don't need the data, and this can lead to non-defeq diamonds.

[Yury G. Kudryashov]

Opened #17458

[Yury G. Kudryashov]

On Github, @Eric Wieser argues that we should migrate to (h : IsUnit _) instead.

[Eric Wieser]

At least in places where we don't actually want the data

[Yury G. Kudryashov]

My main argument pro [IsUnit _] is that people who don't care about fields of positive characteristic may want to apply theorems that require IsUnit (2 : K) without making another stop to prove it.

[Eric Wieser]

Is it 2 specifically that we care about?

[Yury G. Kudryashov]

I definitely have some examples for IsUnit (2 : K), incl. midpoint and #14986

[Yury G. Kudryashov]

I don't have other examples in mind right now.

[Yury G. Kudryashov]

Unless we want to generalize docs#mul_inv_cancel etc to [DivisionMonoid G] [IsUnit a]

[Yury G. Kudryashov]

Note: we already have it as @[simp] for Invertible a.

[Eric Wieser]

I think we might be missing the bigger picture on 14986; the result is also true (and I believe straightforward to prove with docs#QuadraticMap.toBilin) in free modules where 2 is not invertible

[Yury G. Kudryashov]

See https://github.com/leanprover-community/mathlib4/actions/runs/11195116893/job/31122394124 for a list of lemmas that assume [Invertible _] but never use invOf in the statement.

[Yury G. Kudryashov]

(there are other pending linters in the same PR, so you need to search for Invertible)

[Eric Wieser]

Yury G. Kudryashov said:

See https://github.com/leanprover-community/mathlib4/actions/runs/11195116893/job/31122394124 for a list of lemmas that assume [Invertible _] but never use invOf in the statement.

I think I would be in favor of changing all these to (h : IsUnit x) and using [Fact (IsUnit x)] on the one or two instances.

[Yury G. Kudryashov]

Why [IsUnit _] is worse?

[Eric Wieser]

I don't understand how this argument doesn't lead to us converting everything of type Prop into a typeclass

[Eric Wieser]

Maybe that really is a fine outcome, but I've definitely heard arguments that doing that for, say, Odd and Even would amount to an abuse of typeclass search.

[Violeta Hernández]

This smells like typeclass abuse to me too. It feels much more likely that we'll want to prove IsUnit from other available hypotheses, than being able to infer it from the structure of the argument.

[Yury G. Kudryashov]

What do you think about docs#MonoidAlgebra.Submodule.complementedLattice ?

[Yury G. Kudryashov]

UPD: it should assume NeZero.

[Yury G. Kudryashov]

Ignore my last 2 messages.

[Yury G. Kudryashov]

#17754 makes Maschke use IsUnit.

[Yury G. Kudryashov]

What should I do about IsUnit 2? Use Fact? Introduce a typeclass specifically for this?

[Yury G. Kudryashov]

I also see an assumption Invertible 3 in docs#WeierstrassCurve.exists_variableChange_isShortNF

[Yury G. Kudryashov]

See also docs#CategoryTheory.Linear.instEpiHSMulHomOfInvertible

[Yury G. Kudryashov]

It's an instance that assumes [Invertible r] but doesn't use data.

[Violeta Hernández]

I think it makes sense to use Fact for these "a specific number is invertible" predicates

[Eric Wieser]

I think that depends whether the instance you're using Fact on is data or a proof

[Eric Wieser]

If it's a proof, then Fact (IsUnit x) does indeed make the most sense. If it's data, then Invertible x is often better.

[Eric Wieser]

If your proof uses some auxiliary data along the way, use def aux [Invertible x] to define that data, then use IsUnit.nonempty_invertible to construct that instance mid-proof

[Yury G. Kudryashov]

Why Fact (IsUnit _) is better than [IsUnit _]?

[Yury G. Kudryashov]

(e.g., docs#IsClosed is a typeclass but we mostly use it as a predicate)

[Violeta Hernández]

Yury G. Kudryashov said:

Why Fact (IsUnit _) is better than [IsUnit _]?

I'll admit, I'm not sure. Why is Fact (IsPrime _) better than [IsPrime _]? Seems to be similar reasoning.

[Eric Wieser]

Does docs#Fact have anything to say?

[Violeta Hernández]

Yes, but I don't really get its reasoning. Is the issue just that Nat.prime would become a one-field structure instead of being def-eq to its definition?

[Violeta Hernández]

By that reasoning, IsUnit should probably not be a class either

[Eric Wieser]

Ah, I hadn't considered that (historic?) limitations around non-structure classes could have factored in here.

[Eric Wieser]

My rule of thumb would be "only use typeclasses for types"

[Violeta Hernández]

I don't think it's quite as simple as that, e.g. having docs#CharZero as a typeclass is definitely a good thing.

[Violeta Hernández]

I'd argue the same for docs#WellFoundedLT and docs#WellFoundedGT but maybe I'm biased since I'm the one who pushed for those :stuck_out_tongue:

[Violeta Hernández]

Oh wait, I misunderstood you as implying typeclasses should be type-valued rather than having type arguments

[Violeta Hernández]

I mostly agree with that rule of thumb.

[Violeta Hernández]

I'd like to point to the counterexample of the unbundled order classes like docs#IsRefl, docs#IsTrans, etc. I'd argue these are still good to have, but if anyone ever wants to refactor them out I don't think I'll be strongly opposed.

[Yury G. Kudryashov]

We have docs#NeZero docs#IsClosed

[Eric Wieser]

IsClosed I'd argue should be de-classified, NeZero I haven't thought about before.

[Michael Stoll]

NeZero seems to be helpful e.g. to avoid using PNat.

[Yury G. Kudryashov]

Do you suggest migrating to Fact (IsClosed _) whenever we need to assume IsClosed in an instance?

[Eric Wieser]

Yes, that's my claim

[Sébastien Gouëzel]

The reason we used IsClosed as a typeclass is to be able to obtain that quotients of normed spaces by closed subspaces are normed spaces. For instance, if you're in finite dimension, subspaces are automatically closed, so quotients are automatically normed spaces. If you want to get this fact for free using the Fact mechanism, then you need to register this as a global Fact instance, but if I remember correctly global Fact instances should be avoided if possible. So I see what we lose when going from [IsClosed ...] to [Fact (IsClosed ...)]. What do we gain?

[Eric Wieser]

Agreed that the alternative would be a few global instances of docs#Fact, but we have a number of those already

[Eric Wieser]

Flipping the question around; what do we lose if we make _every_ structure ... : Prop a class?

[Yaël Dillies]

In Lean 3, that would have caused a lot of frozen instance cache issues

[Floris van Doorn]

Yury G. Kudryashov said:

We have docs#NeZero docs#IsClosed

IsClosed is a class? :shock:

[Violeta Hernández]

RE NeZero, I've only ever come across NeZero 1 in my own applications, which arguably could be made into a OneNeZeroClass if we really wanted to.

[Yury G. Kudryashov]

NeZero is used, e.g., in our instances about Fin.

[Yury G. Kudryashov]

In many cases, NeZero (1 : R) can be replaced with Nontrivial R.

[Yury G. Kudryashov]

See docs#NeZero.one

[Yaël Dillies]

It's also used for measures, where a bunch of lemmas break for the zero measure

[Oliver Nash]

Also in low characteristic [NeZero (2 : R)]and [NeZero (3 : R)] are already useful (and one day we'll certainly get to [NeZero (5 : R)] and maybe higher). E.g., docs#EllipticCurve.ofJ_0_of_three_ne_zero

[Eric Wieser]

That looks like it could just take (h : 3 \ne 0) as an argument

[Matthew Ballard]

In these scenarios, I just want to avoid manually supplying a proof that something is not 0. Typeclass synthesis is one mechanism. If set up appropriately, autoparams could be another. Though NeZero didn’t get upstreamed for no reason.

[Eric Wieser]

My understanding is that NeZero got upstreamed because of Fin, and the decision was based on "this is what mathlib does" not "this is clearly the perfect solution"

[Eric Wieser]

NeZero is also somehow different because we have both the class and the non-class

[Matthew Ballard]

Sure, but if they had a better idea, they wouldn’t have.

I think the cost of flipping everything to classes is just performance.

[Matthew Ballard]

I would like

import Mathlib.Data.ZMod.Defs

instance (p : Nat) (hp : p.Prime := by norm_num) : Field (ZMod p) := sorry

#synth Field (ZMod 5)

to succeed

[Eric Wieser]

Enough to create an RFC for it?

[Sébastien Gouëzel]

If I recall correctly, having the possibility to run tactics for default arguments in typeclass inference was considered at the beginning of Lean 4, but it was discarded later because of added complexity and performance issues. Given how critical this is, I'm not sure the FRO is willing to revisit this.

[Matthew Ballard]

I think an RFC is fine but I would guess that as @Sébastien Gouëzel says: significant changes to typeclass synthesis are currently off the table

[Matthew Ballard]

I would also guess that the FRO considered something like this before upstreaming NeZero but I have no first-hand knowledge

[Jz Pan]

Now my PR #18531 of to elliptic curves is related to #17458... If IsUnit is a typeclass then this PR could be simplified a little bit (also with API changes).

[Kim Morrison]

Pinging that #17458 is marked awaiting-zulip based on this thread. It would be good to come to a decision here, and either close that PR or proceed with reviewing it.

[Yury G. Kudryashov]

+1 for ping

[Michael Stoll]

I've been using (and got to like) docs#NeZero quite consistently in the recent factor of rootsOfUnity. So I think a Prop- valued version of docs#Invertible makes sense. But I haven't followed this discussion very closely.

[Yury G. Kudryashov]

@Eric Wieser WDYT?

[Eric Wieser]

My stance is:

• IsUnit shouldn't be a class
• Invertible is mostly ok as is
• A new HasInverse x x_inv : Prop (which is to IsUnit as HasSum is to Summable) would ease some of the pain around Invertible.

[Yury G. Kudryashov]

In the examples where I suggest we assume [IsUnit a], we don't want to know a_inv.

[Eric Wieser]

Right, in those examples I am suggesting Fact (IsUnit a)

[Eric Wieser]

(and I am not proposing HasInverse should be a class)

[Yury G. Kudryashov]

Why Fact (IsUnit a) is better than class IsUnit (rarely used as a class)?

[Eric Wieser]

Should Summable be a class too? Should Prime?

[Yury G. Kudryashov]

Summable: AFAICT, we never need it to construct an instance. Prime: possibly (we use Fact (Nat.Prime p) very often).

[Eric Wieser]

Yury G. Kudryashov said:

Why Fact (IsUnit a) is better than class IsUnit (rarely used as a class)?

Here's one argument; if you make it a class, every caller has to think about whether to write (h : IsUnit a) or [IsUnit a]. If you use Fact, this choice is obvious

[Yury G. Kudryashov]

Makes sense, but didn't work for Nat.Prime... I don't see any system in (h : p.Prime) vs [Fact p.Prime]...

[Yury G. Kudryashov]

So, we should add instances for, e.g., [GroupWithZero G] {a : G} [NeZero a] : Fact (IsUnit a)?

[Eric Wieser]

Yury G. Kudryashov said:

AFAICT, we never need it to construct an instance.

I think "needed to construct an instance" is exactly the design problem that Fact is intended to solve.

So I think your argument might extend to "we should remove Fact", which is worthy of its own thread.

[Yury G. Kudryashov]

BTW, are discrimination trees good enough with Facts?

[Eric Wieser]

They should be fine, key (Fact X) = [Fact] ++ key X

[Yury G. Kudryashov]

Does it mean that we can use Fact (Predicate ...) instead of turning Predicate into a class without slowdown?

[Eric Wieser]

I think yes

[Eric Wieser]

(ignoring the negligable cost of the key having one more element)

[Yury G. Kudryashov]

Then I'll start migrating some [Invertible] assumptions to [Fact (IsUnit _)].

[Kim Morrison]

Yury G. Kudryashov said:

Does it mean that we can use Fact (Predicate ...) instead of turning Predicate into a class without slowdown?

While this is true, it also goes against our original plans to not use Fact as a general "let's have typeclass search do our proving" mechanism.

(Perhaps it is a feature, not a bug, that there is overhead to turning something into a class?)

[Kevin Buzzard]

With Nat.prime p there is never any proving; it literally is just a convenient way of saying "let p be a prime forever". So this is a great use of Fact as far as I can see.

[Eric Wieser]

My mental model was that Fact was only really intended to allow non-typeclasses into the assumptions of instances as instance [Fact (Predicate ..)] : _; which is compatible with Kim's comment which I think is objecting to it appearing in the conclusion as instance : Fact (Predicate ..).

[Eric Wieser]

(docs#Fact indicates a few such instances exist, but I think they're mostly for convenience rather than doing heavy lifting)

[Yury G. Kudryashov]

But we want to have at least the following instances for IsUnit _ (or `Fact (IsUnit _)1):

• [Group G] (a : G) : IsUnit a
• [Invertible a] : IsUnit a
• IsUnit 1
• [GroupWithZero G₀] (a : G₀) [NeZero a]
• [CommMonoid M] {a b : M} [IsUnit a] [IsUnit b] : IsUnit (a * b)
• [IsUnit a] (n : Nat) : IsUnit (a ^ n)
• [IsUnit (OfNat.ofNat n : R)] : IsUnit (OfNat.ofNat : Module.End R M) (this instance from #14986 and motivated this thread).

[Johan Commelin]

@Eric Wieser Maybe we should just try to make IsUnit a class. Your argument is that this puts us on a slippery slope. Maybe it does. But we're still deciding on a case-by-case basis. And Yury has some good arguments for wanting automation to kick in. TC is the best we have for this right now.

[Eric Wieser]

The examples above feel rather like

Kim Morrison said:

"let's have typeclass search do our proving"

I'm not sure that the fact some proposition can be deduced structurally is a sufficient argument for us to use typeclasses search to prove it; otherwise Differentiable and IsSquare would surely deserve the same treatment.

[Patrick Massot]

I find it sad that we can’t have “let’s have typeclass search do our proving”.

[Kevin Buzzard]

IIRC we tried this a bit in LTE with simple inequalities. We were working with L^p spaces with p<1 remembered as a Fact, and would occasionally get typeclass inference to prove things like q<p and p<1 implies q<1.

[Johan Commelin]

Yeah, we used it a lot. It did all sorts of multiplications of inequalities

[Johan Commelin]

Of course we didn't have gcongr back then

[Yakov Pechersky]

The situation is somewhat similar to docs#Ideal.IsPrime where that is a class. Sometimes IsPrime is passed as an explicit argument, and sometimes as a TC argument. And it has to be in TC access so that one can get an integral domain instance on the quotient ring.

[Yury G. Kudryashov]

Note that I explained that we may have reasonable IsUnit instances but I didn't find any instances that need to assume [IsUnit _], at least in this thread.

[Yury G. Kudryashov]

I guess, we can try to migrate some of those [Invertible _] to (h : IsUnit _) until we meet an instance, then come back to this discussion.

[Eric Wieser]

I think we should do that (and migrate to Fact (IsUnit _) where appropriate), then come back to this discussion once we know how many such Fact (IsUnit _)s there are which we want to de-Fact

[Jz Pan]

Yury G. Kudryashov said:

Note that I explained that we may have reasonable IsUnit instances but I didn't find any instances that need to assume [IsUnit _], at least in this thread.

https://github.com/leanprover-community/mathlib4/blob/3f45494422faa4e895db8a57b7a486dd9e0c2a5d/Mathlib/AlgebraicGeometry/EllipticCurve/Weierstrass.lean#L556-L563 in PR #18531. It is [Invertible ...] in current mathlib, but we plan to refactor it without requiring knowing what the exact inverse is.

[Eric Wieser]

My impression from that PR is that IsElliptic should perhaps also not be a class

[Yury G. Kudryashov]

I don't think that we'll have any instance implying IsUnit (_ - 1728).

[Violeta Hernández]

Just to be clear, what's the argument against having typeclass search take over every single structural predicate?

[Johan Commelin]

TC is already the most expensive part of building mathlib. I guess we should keep it in check a bit.
And probably going down that path would cause a net slowdown.

I would still love to have more invisible automation for these structural proofs though...

[Violeta Hernández]

Can we maybe make custom simp / aesop sets? And have an autoparam calling the relevant tactic

[Jz Pan]

Eric Wieser said:

My impression from that PR is that IsElliptic should perhaps also not be a class

Then each time you write j you need to provide a proof that the discriminant is invertible. Or fall back to current design: WeierstrassCurve vs EllipticCurve which I want to refactor. Or assign j a junk value when the discriminant is not invertible.

[Jz Pan]

I have already list the reason in that PR why current design is suboptimal: it requires copies of APIs between WeierstrassCurve and EllipticCurve.

[Jz Pan]

Yury G. Kudryashov said:

I don't think that we'll have any instance implying IsUnit (_ - 1728).

It is provided by haveI later in that file. That instance is used in another instance which does not require any other auxiliary inputs, and which is designed to be the public instance to use.

[Artie Khovanov]

Question: Should I be using Invertible or IsUnit in the following statement, and should it be a typeclass?

theorem {R : Type*} [CommRing R] {P : RingPreordering R} hasIdealSupport_of_invertible_2 [Invertible (2 : R)] : P.HasIdealSupport

Context: A preordering on a ring $R$ is a subset $P\subseteq R$ closed under $+$ and $\cdot$ and containing all squares, but not containing $-1$. The support of a preordering is $\text{supp}(P)=P\cap-P$. Now, $\text{supp}(P)$ is an additive subgroup, but not necessarily an ideal. However, in nearly all relevant cases it is an ideal: in particular, if 2 has an inverse in $R$. This matters in Lean because, if I know $\text{supp}(P)$ is an ideal, then I can use the ideal structure P.support rather than having to use P.supportAddSubgroup.

[Eric Wieser]

Theorems should arguably always assume the data-less version of things unless they use the data in the statement.

[Yaël Dillies]

I think here it's worth having the instance version assuming Fact [(IsUnit (2 : R))]

[Eric Wieser]

I think the rule is usually "only use Fact if you are writing an instance"?

[Yaël Dillies]

So... my suggestion agrees with the rule?

[Bhavik Mehta]

Eric Wieser said:

I think the rule is usually "only use Fact if you are writing an instance"?

Or if the statement relies on an instance which uses Fact

[Artie Khovanov]

Yaël Dillies said:

I think here it's worth having the instance version assuming Fact [(IsUnit (2 : R))]

hm, why is having it as an instance better here? just so I know what principles to apply in future
I'm very aware of not wanting Fact-creep

[Kevin Buzzard]

Eric Wieser said:

I think the rule is usually "only use Fact if you are writing an instance"?

Isn't [Fact p.Prime] all over the number theory parts of mathlib? Searching for the phrase gives 179 hits and randomly clicking on them it seems that most of the usages are in theorems rather than instances. Or have I misunderstood what you're saying?

[Eric Wieser]

What I wrote needs Bhavik's clarification

[Kevin Buzzard]

Concrete examples: docs#isUnit_iff_not_dvd_char_of_ringChar_ne_zero , docs#isUnit_iff_not_dvd_char , docs#Choose.choose_modEq_choose_mod_mul_choose_div , docs#IsUnit.natCast_factorial_of_isNilpotent , docs#Nat.Prime.mod_two_eq_one_iff_ne_two ,...

[Eric Wieser]

If you can remove the Fact from an assumption to a non-instance and the statement still compiles, then I claim it should be a regular hypothesis instead

[Kevin Buzzard]

Well I posted the 5 theorems at the top of the search results above, and I've just commented out [Fact p.Prime] from all of them and all the statements still compiled (and all the proofs broke) so whatever world you're living in it doesn't seem to be related to what's actually happening on the ground

[Eric Wieser]

Well, the ground is always chaotic, the question is what fraction of it agrees with my claim, and what breaks if we fix the rest?

[Kevin Buzzard]

Here's some code from Data/Nat/Prime/Basic.lean:

theorem Prime.odd_of_ne_two {p : ℕ} (hp : p.Prime) (h_two : p ≠ 2) : Odd p :=
  hp.eq_two_or_odd'.resolve_left h_two

theorem Prime.even_sub_one {p : ℕ} (hp : p.Prime) (h2 : p ≠ 2) : Even (p - 1) :=
  let ⟨n, hn⟩ := hp.odd_of_ne_two h2; ⟨n, by rw [hn, Nat.add_sub_cancel, two_mul]⟩

/-- A prime `p` satisfies `p % 2 = 1` if and only if `p ≠ 2`. -/
theorem Prime.mod_two_eq_one_iff_ne_two {p : ℕ} [Fact p.Prime] : p % 2 = 1 ↔ p ≠ 2 := by
  refine ⟨fun h hf => ?_, (Nat.Prime.eq_two_or_odd <| @Fact.out p.Prime _).resolve_left⟩
  rw [hf] at h
  simp at h

so quite what logic is being used to determine whether to use facts is beyond me.

[Bhavik Mehta]

I agree with Eric here; it's true that some parts of the library, particularly around padic valuations don't follow the rules as above, but I'm confident that these are things we should correct. Indeed in the third example you give, avoiding Fact means the theorem is easier to use with dot notation, so it should be easier to apply in virtually all situations.
The rule I gave above is essentially derived from the docstring for docs#Fact, so I also claim this is also not a new idea.

[Kevin Buzzard]

So I'm not pushing back against the idea of removing those Facts but let me put this into some context. The completion of the rationals that the analysts use is the real numbers and there's only one of those. But arithmeticians like to also use the p-adic completions which are an infinite family parametrised by prime numbers, and in general you typically fix p once and for all and then prove 100 theorems about it all of which assume p is prime. In the literature this is typically done by announcing that p is a fixed prime on page 1 of the paper and then never saying it again. Here you're saying that the thing to do is to constantly carry around (hp : p.Prime) and supply it everywhere. I can quite see how this gets old quickly, because the hypothesis will be used in all the theorems and proofs and if it's not being carried around by typeclass inference then it will have to be carried around manually. Imagine telling the analysts that every time they write the real numbers they have to also add some random extra variable -- there would be a lot of pushback. But that's what you're saying should be the way to develop, say, p-adic analysis.

[Kevin Buzzard]

docs#Padic

[Kevin Buzzard]

Ah, no you're not because there it is a Fact.

[Ruben Van de Velde]

#29090

[Bhavik Mehta]

Kevin Buzzard said:

Ah, no you're not because there it is a Fact.

Yes, exactly this! I think Padic and its API is as it should be, but docs#padicValNat_self (and the things around it) should be changed to avoid Fact.

[Alex Meiburg]

Suppose that we changed that lemma appropriately. If simp wanted to apply padicValNat_self {p : ℕ} (hp : Nat.Prime p) : padicValNat p p = 1 and there's no Nat.Prime p in the argument list to simp, but there is a Fact (Nat.Prime p) in the context where the tactic executes, would simp be able to use that?

In general I think "any Facts in context be passed to simp by default" would probably often be a good rule of thumb, but afaik there's no such behavior

[Kevin Buzzard]

Can you just feed Fact.out or whatever to simp, or make it a local simp lemma or something?

[Yaël Dillies]

docs#Fact.out very annoyingly doesn't take the predicate explicitly

[Aaron Liu]

Yaël Dillies said:

docs#Fact.out very annoyingly doesn't take the predicate explicitly

do you think we should have a version which does take the predicate explicitly

[Yaël Dillies]

I think Fact.out itself should change. It's very rarely used without specifying its argument, as one would then fully rely on unification to figure out what the Prop is

[Eric Wieser]

I think docs#Fact.out is the way it is because the language feature was missing

[Alex Meiburg]

Even assuming there's an ergonomic syntax for Fact.out, my point is that -- often during a proof I'll try to just call simp and see if it does a lot for me (and I might not immediately know how much it will accomplish). It could be that simp _would_ do a lot more, if I passed it the appropriate Fact.out, but I don't always know to do that.

But Facts are _usually_ relatively common and clean hypotheses, and would pretty much always be a useful thing to discharge away without having to think about it. If the simp lemmas all took Facts too, it would be fine because it's done by typeclass inference, but in a world where they're mixed a lot it's harder

[Alex Meiburg]

It's especially a bit silly because simp_all and simp [*] won't pick it up

[Alex Meiburg]

So I think it would be good to have the default discharger do something like try Fact.out

[Eric Wieser]

Can Fact.out itself be tagged simp?

[Aaron Liu]

Eric Wieser said:

Can Fact.out itself be tagged simp?

Would that be tried everywhere?

[Robin Arnez]

Yes :-(

import Mathlib

set_option trace.Meta.synthInstance true
example (a b : Nat) : a = b ∨ 3 = 5 ∨ Nat.Prime 3 := by
  simp [Fact.out]

Screenshot 2025-08-29 210522.png
(some lines containing Fact (Fact (Fact True)) or Fact (a = b ∨ True) are below)

[Yakov Pechersky]

:chili_pepper: write all (h : p.Prime := by first | assumption | exact Fact.out) hypotheses with autoParams

[Robin Arnez]

won't help with simp though

[Kevin Buzzard]

Instead of making Fact.out a simp lemma, is it possible to teach simp about specific facts? For example in some big work about primes can simp be taught p.Prime somehow? i.e. "teach simp the relevant fact" rather than "teach simp to extract stuff from Fact in general"?

[Aaron Liu]

Kevin Buzzard said:

Instead of making Fact.out a simp lemma, is it possible to teach simp about specific facts? For example in some big work about primes can simp be taught p.Prime somehow? i.e. "teach simp the relevant fact" rather than "teach simp to extract stuff from Fact in general"?

Maybe

import Mathlib

@[simp]
theorem Nat.Prime.of_fact (p : Nat) [Fact p.Prime] : p.Prime := Fact.out

[Eric Wieser]

(deleted)

[Johan Commelin]

Kevin Buzzard said:

Instead of making Fact.out a simp lemma, is it possible to teach simp about specific facts? For example in some big work about primes can simp be taught p.Prime somehow? i.e. "teach simp the relevant fact" rather than "teach simp to extract stuff from Fact in general"?

Sounds like a simproc to me.