Zulip Chat Archive

Stream: general

Topic: outparams

Kevin Buzzard (Nov 11 2021 at 16:07):

Johan was telling me about outparams recently and I am now in the dangerous situation of having a very weak understanding of them and trying to use them to solve everything. Ashvni is rewriting docs#zmod.cast_nat_cast and getting goals of the form char_p (zmod (d * p ^ m)) ?m_1. Note that char_p is a class. Lean has an instance zmod.char_p : ∀ (n : ℕ), char_p (zmod n) n but what the type class inference system does _not_ know is that if char_p (zmod n) a then we'd better have a = n! Is there a way of telling the type class inference system to solve all goals of the form char_p (zmod n) ?m_1 by setting ?m_1 = n and then using zmod.char_p? Is this what outparams do or am I way off?

Johan Commelin (Nov 11 2021 at 16:15):

I personally wouldn't mind making p an out_param of char_p. But some instances would need to be removed. For example char_p R (ring_char R) would be very dangerous.

Eric Wieser (Nov 11 2021 at 18:06):

Do we have any instances of the form char_p R (ring_char R) today?

Eric Wieser (Nov 11 2021 at 18:07):

As I understand it, out_param modifies char_p not zmod.char_p, so it says roughly "whenever you search for a char_p instance, infer the canonical p value from the instance you find"

Johan Commelin (Nov 11 2021 at 18:09):

$ rg "char_p.*ring_char"
25:@@subsingleton.elim (@@char_p.subsingleton _ $ ring_char.of_eq h1) _ _

92:unfold ring_char; exact char_p.cast_eq_zero_iff R (ring_char R)
94:theorem eq {p : } (C : char_p R p) : p = ring_char R :=
97:instance char_p : char_p R (ring_char R) :=
103:char_p.congr (ring_char R) h

Eric Wieser (Nov 11 2021 at 18:24):

I assume that's docs#ring_char.char_p

Kevin Buzzard (Nov 12 2021 at 16:19):

and docs#ring_char.eq_iff

Last updated: Dec 20 2023 at 11:08 UTC