adding a definition

Stream: general

[Keeley Hoek]

I'd like implement a [user_command] which adds a definition to the environment at the place where the [user_command] is executed. Of course, there is environment.add, but I have to build a declaration and in particular pass a name. This won't act the same way as writing def blah : type = foo ... on that line because the latter will have a "full name" me.my_namespace.blah if this all goes on inside namespace me.my_namespace. Is there a way to fix this: either to get the current namespace, or to make a declaration as if it happened using a def?

[Mario Carneiro]

:four_leaf_clover:

[Mario Carneiro]

there is a command get_current_definition that tells you the name of the currently elaborating definition, from which you can derive the namespaces, but it doesn't work in a user command

[Keeley Hoek]

@Mario Carneiro Hallelujah! According to the source code (see src/library/tactic/tactic_state.cpp), it turns out that the first element returned by open_namespaces is always the namespace of the current line, as long as you're in a command! WHOOP WHOOP

[Keeley Hoek]

*as long as youre being run in some namespace, but of course there is a hack to check if this is the case...

[Scott Morrison]

This will probably all break again in :four_leaf_clover:, but I guess we'll cope. :-)

[Keeley Hoek]

Ok I was wrong again because my "easy hack" to check you're in the default namespace doesn't work and I can't fix it. But, I just discovered with_input command_like in the lean.parser monad. It's a backdoor into.... everything! So I can just emit def blah : type = blah from the command!

[Keeley Hoek]

---no silly hack required!

[Scott Morrison]

oooh... can we add rfl lemmas from commands using this??

[Keeley Hoek]

Yes, you can do anything

[Keeley Hoek]

It saves the current parser state, then literally hands a string to the parser as if it was the next line of the file, then restores it

[Keeley Hoek]

@Scott Morrison

[Keeley Hoek]

Ill cook up a demo

[Scott Morrison]

I've been wanting to do that for a while; I have lots of boilerplate rfl lemmas that just repeat a structure field.

[Scott Morrison]

I do wonder whether this is a good idea, considering :four_leaf_clover:, but I'm still tempted.

[Keeley Hoek]

when it comes time we could always turn on printing what the command outputs and go and replace them with their content
or every write a script to if there are lots

[Keeley Hoek]

what needs to go in and what needs to come out?

[Scott Morrison]

Here's a prototypical example:

def equivalence_inverse (F : C ⥤ D) [full F] [faithful F] [ess_surj F] : D ⥤ C :=
{ obj  := λ X, F.obj_preimage X,
  map' := λ X Y f, F.preimage ((F.fun_obj_preimage_iso X).hom ≫ f ≫ (F.fun_obj_preimage_iso Y).inv),
  map_id' := λ X, begin apply F.injectivity, obviously, end,
  map_comp' := λ X Y Z f g, begin apply F.injectivity, obviously, end }.

-- FIXME pure boilerplate...
@[simp] private lemma equivalence_inverse_map
  (F : C ⥤ D) [full F] [faithful F] [ess_surj F]
  {X Y : D} (f : X ⟶ Y) : (equivalence_inverse F).map f = F.preimage ((F.fun_obj_preimage_iso X).hom ≫ f ≫ (F.fun_obj_preimage_iso Y).inv) := rfl.

[Scott Morrison]

I would like to write: generate_rfl_lemma equivalence_inverse map

[Keeley Hoek]

@Scott Morrison ok I think I can do that, just sorry, who is getting rid of the primes on (e.g.) map'? I've always wondered

[Scott Morrison]

Yeah, that's a real hack. Unfortunately sometimes it's necessary to state something, and then restate it. (e.g. to clean up the mess that autoparam leaves, or to restate something using a coercion that can only be introduced later).

[Scott Morrison]

The "convention" is now to at first name the declaration with a prime at the end of the name, and then to remove it for the "real" declaration.

[Scott Morrison]

The restate_axiom user command does this.

[Scott Morrison]

If it's not given an explicit new name, it inspects the old name, removes a prime if it finds one, and otherwise adds "_lemma".

[Keeley Hoek]

And so you have to prove that what is generated is actually equal to what was there originally all the time?

[Keeley Hoek]

Also, sorry going to cook it up now, just writing library functions and testing they work
The only quirk is that when there is an attribute error, the red line appears on the first line of the file.... But I think there is a way to fix that maybe

[Keeley Hoek]

but we also have a command suggestion category_theory now

[Keeley Hoek]

I don't even think we need my thing to do this actually Scott, since we could always just put the lemma in the same namespace as wherever the parameter (e.g. equivalence_inverse) lives

[Keeley Hoek]

I think I should talk to you more about what exactly it should do, since it seems hard to decide whether for example {X Y : D} in the above example should have curly brackets instead of parentheses.