outparams

Stream: general

[Kevin Buzzard]

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]

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]

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

[Eric Wieser]

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]

$ rg "char_p.*ring_char"
src/algebra/char_p/quotient.lean
25:@@subsingleton.elim (@@char_p.subsingleton _ $ ring_char.of_eq h1) _ _

src/algebra/char_p/basic.lean
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]

I assume that's docs#ring_char.char_p

[Kevin Buzzard]

and docs#ring_char.eq_iff