Derived docstrings in `to_additive`

Stream: general

[Eric Wieser]

It would be nice if instead of writing

/-- The supremum of congruence relations `c, d` equals the smallest congruence relation containing
    the binary relation '`x` is related to `y` by `c` or `d`'. -/
@[to_additive sup_eq_add_con_gen "The supremum of additive congruence relations `c, d` equals the
smallest additive congruence relation containing the binary relation '`x` is related to `y`
by `c` or `d`'."]
lemma sup_eq_con_gen (c d : con M) := sorry

we could write

/-- The supremum of congruence relations `c, d` equals the smallest congruence relation containing
    the binary relation '`x` is related to `y` by `c` or `d`'. -/
@[to_additive sup_eq_add_con_gen (doc.replace "congruence" "additive congruence")]
lemma sup_eq_con_gen (c d : con M)  := sorry

to avoid repeating docstrings.

I'm trying to do this myself, but I've immediately run into two problems

• Is there really no string.replace built in anywhere?
• How can I set the value of doc before evaluating the expression (doc.replace "congruence" "additive congruence")?

[Rob Lewis]

This would be very nice. For your second question, I assume this is happening in the after_set method of to_additive? You can do something like

open tactic
@[user_attribute] meta def foo : user_attribute :=
{ name := `foo,
  descr := "",
  after_set := some $ λ n _ _, do d ← doc_string n, trace d }

/--hi-/
@[foo] def k := 2

[Rob Lewis]

I don't know if string.replace has been implemented but in general there's not a huge API around string.

[Eric Wieser]

Right, I know how to get the value of the docstring, and of the expression - what I can't work out is how to programatically create the expression
let doc := ${old doc string} in ${attr argument expression}

[Eric Wieser]

Part of the problem is I've forgotten the various expression quoting mechanisms, and the lean manual is blank on the pages about those.

[Rob Lewis]

I'm not quite sure what you're asking. @[to_additive] is applied to some declaration mul_thing. The after_set method of the to_additive attribute creates a declaration add_thing. You can do d <- doc_string `mul_thing, add_doc_string `add_thing (d.replace whatever)

[Eric Wieser]

My question is, if I have the string "hello world", and the expr doc.replace "hello" "goodbye", how do I obtain the expr let doc := "hello world" in doc.replace "hello" "goodbye" which I can pass to eval_expr to get string "goodbye world"?

[Rob Lewis]

Why is doc.replace "hello" "goodbye" an expr?

[Eric Wieser]

Because it's an argument to to_additive, which gets parsed as an expr and then evaluated to a string.

[Eric Wieser]

I want to add an intermediate step where doc is first substituted for the current docstring before the expression is evaluated

[Rob Lewis]

I'm still kind of confused. You have a function addify : string -> string that turns a multiplicative doc string to an additive one, right?

[Rob Lewis]

There's some line in to_additive that takes a string, not an expr, and sets the doc string for the new additive decl to that string.

[Eric Wieser]

to_additive.parser contains a step that converts the docstring argument from a pexpr to a string

[Rob Lewis]

eval_expr string?

[Eric Wieser]

That + to_expr, yes

[Eric Wieser]

I want to change that step to produce a string \to string

[Eric Wieser]

But that means I need to introduce a name binding for doc within that expression

[Rob Lewis]

I think you're really overcomplicating things

[Rob Lewis]

Maybe just take a list of substitutions?

[Eric Wieser]

Perhaps, but I'd like to understand how to do this the way I describe even if the resulting API is undesirable

[Eric Wieser]

My hunch is I want to do something like use to_expr `(λ doc, %%pe)` instead of to_expr pe within to_additive.parser, but I have no idea if that is correct use of %%, or where I can even find documentation on%%.

[Rob Lewis]

That should approximately work, I think there are complications with dot notation. Antiquotes are covered e.g. here

[Eric Wieser]

Thanks, that page was what I was looking for

[Eric Wieser]

How do I find a list of such pages? https://leanprover-community.github.io/extras is unfortunately not an index page

[Rob Lewis]

It's linked here along with many other resources, and from the mathlib docs

[Eric Wieser]

Thanks for the help