request for tactic

Stream: general

[Scott Morrison]

I'd really like a tactic that lets me add an @[elementwise] attribute to lemmas which give equations in categories.

It should check that the lemma is an equation between morphisms f g : X ⟶ Y (presumably depending on arguments) in some category C, failing otherwise.

It should produce a new copy of the lemma, appending the _apply to the name, modified as follows:

1. If we can't already infer a concrete_category C, add such an instance to the hypotheses.
2. Add a hypothesis x : (X : Type*) (using concrete_category.has_coe_to_sort).
3. Replace the conclusion with f x = g x, and the proof with concrete_category.congr_hom prf x.
4. Run dsimp only [concrete_category.comp_coe, concrete_category.id_coe] on the conclusion, to replace e.g (p ≫ q) x with q (p x).

Hopefully this is very similar to the existing @[reassoc] tag's implementation.

[Scott Morrison]

I will presumably end up trying this myself, but if anyone would like to

1. give hints
2. criticise the spec
3. help me write it sometime
4. write it!

any of these would be much appreciated. :-)

[Kevin Buzzard]

I'm in no position to help with this but I will remark that yesterday I ran into exactly this issue when thinking about your recent work on homology and trying to apply it to the category of R-modules, and I wrote an apply lemma manually which worked in this case. In other words -- you're not the only one who wants this!

[Scott Morrison]

I was just having a look at @Simon Hudon's reassoc_axiom.lean. I am hopeful that I can edit that into this tactic, using it as a crib for everything I have forgotten about metaprogramming. :-)

[Scott Morrison]

I'll start shortly if anyone wants to join!

[Scott Morrison]

I think I am there except for a really annoying unassigned universe metavariable. :-(

[Scott Morrison]

If I have an expr representing a category.{u (u+1)} C, how do I extract that universe level u?

[Scott Morrison]

Specifically, I want to build the expr representing concrete_category.{u} C. How do I insert the u into it? Currently I'm just using to_expr `(concrete_category %%C), but there are not antiquotations for universe levels.

[Gabriel Ebner]

I'd also like antiquotations for universe levels. Hopefully we can make that happen in :four_leaf_clover: .

[Gabriel Ebner]

You can always build the expression manually. expr.const ``concrete_category [u, v, w] C inst

[Gabriel Ebner]

Extracting the universe levels is easy e.get_app_fn.univ_levels.

[Scott Morrison]

Nice! I had weird error messages while I was getting the universe levels wrong, but once I sorted that out this works nicely.

[Scott Morrison]

How do I get the universe level of an expression representing something in Type u?

[Scott Morrison]

I understand that .univ_levels extracts the universes on a constant. But if I'm just looking at some term X : Type u, how do I tell which u?

[Gabriel Ebner]

I'm not sure if we have a function for that. You could pattern-match against expr.sort (level.succ u).

[Scott Morrison]

Ah, there is match_sort, which does exactly that.

[Scott Morrison]

But it seems I have to infer_type twice, so I'm actually looking at the Type v.

[Gabriel Ebner]

Once should be enough. That is, something like expr.sort (level.succ u) ← infer_type X >>= whnf,

[Scott Morrison]

Thanks.

[Scott Morrison]

Hopefully a final universe question. Say I've taken some declaration d, and prepared a new type t and proof p that I want to make a declaration for.

Usually I'd write

add_decl $ declaration.thm n' d.univ_params t (pure pr)

that is, I'd copy my universe parameter names from d.

What if t has a new universe metavariable in it? Then I get the error failed to add declaration 'tactic.foo_apply' to environment, type has metavariables. How am I meant to package this up as a declaration with one more universe parameter than before?

[Gabriel Ebner]

If you have a universe metavariable, you need to replace it by a universe parameter. (I think the easiest way to assign universe metavariables is unify (expr.sort u) (expr.sort v)). Then you append the universe parameters to d.univ_params (or prepend, it's your choice).

[Scott Morrison]

And I can just make up a fresh name for my new parameter?

[Gabriel Ebner]

:+1:

[Scott Morrison]

#6941