contrapose! this

Stream: mathlib4

[Johan Commelin]

It seems that contrapose! doesn't like this as argument. So I'm renaming assumptions to H and then contrapose! H is happy.
Probably some small bug lurking somewhere.

[Mario Carneiro]

yep, it's a recurring issue, see https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/.60guard_hyp.60.3A.20can't.20guard.20this

[Sebastian Ullrich]

An alternative solution would be to, instead of restricting this back to ident, extend hypothesis-taking tactics to term:max so that contrapose! ‹foo› would also be accepted

[Mario Carneiro]

I think it is unlikely to be possible to do this everywhere a local constant can be mentioned

[Mario Carneiro]

if ‹_› : p then e else f?

[Mario Carneiro]

That's a significantly more ambitious change than lean4#2105 . You should look at all of those examples and see whether ‹_› makes sense in them

[Sebastian Ullrich]

That's a binding, not a reference. I know Lean 3 accepted this as a binding as well, is it desirable to restore this behavior, for the port or in general?

[Mario Carneiro]

Of course this can be a binding

[Mario Carneiro]

it's normally being used as a binding in these examples

[Mario Carneiro]

when you want a ident_ it's usually a binding

[Mario Carneiro]

for references we usually use term (and don't even restrict to fvars, any proof will do)

[Mario Carneiro]

I think there is strong evidence to suggest that people don't treat this specially as a binding / identifier in the majority of cases

[Sebastian Ullrich]

Mario Carneiro said:

for references we usually use term (and don't even restrict to fvars, any proof will do)

Well this thread is about such a tactic that takes a hypothesis reference, so that's what I focused on. Any tactic with at falls under this case.

[Sebastian Ullrich]

So my proposal really is complementary to your PR: accept binderIdent for bindings, accept term:max for hypothesis references. In combination they could be used to solve the this problem (by further extending binderIdent if desired), but they can also be desirable independently.

[Eric Wieser]

Doesn't accepting term:max for hypothesis references mean that nonsense like revert (x + 1) becomes syntactically legal?

[Mario Carneiro]

Adding this to binderIdent would be a possibility, but currently it's really painful to deal with those special cases and that's why it's so bug-prone

[Mario Carneiro]

Sebastian Ullrich said:

Mario Carneiro said:

for references we usually use term (and don't even restrict to fvars, any proof will do)

Well this thread is about such a tactic that takes a hypothesis reference, so that's what I focused on. Any tactic with at falls under this case.

No, contrapose is like by_cases, it introduces a binding

[Mario Carneiro]

actually it's a bit of a combo, it reverts a hypothesis named h and then introduces a binding named h

[Sebastian Ullrich]

Right, but syntactically I'd say it's a reference primarily. contrapose _ doesn't make sense.

[Mario Carneiro]

it is both a binding and a term, so it needs to be in the intersection of their grammars

[Mario Carneiro]

technically that includes _ but you would never be able to infer the _ so that's not so useful

[Mario Carneiro]

Eric Wieser said:

Doesn't accepting term:max for hypothesis references mean that nonsense like revert (x + 1) becomes syntactically legal?

Syntactically legal yes, but usually the pattern here is to elaborate the expression and assert that the result is an fvar

[Mario Carneiro]

you can even throw a "syntax exception" if it's not if you want to make it look like a syntax error

[Mario Carneiro]

the main justification for using terms that elaborate to fvars is using ‹_›

[Sebastian Ullrich]

Mario Carneiro said:

it is both a binding and a term, so it needs to be in the intersection of their grammars

That's not really true because you would use the syntax to resolve the reference and then use the resolved identifier as the binding. contrapose ‹foo› could definitely be made to work.

[Mario Carneiro]

okay, but that's definitely not a general fact about binderIdents

[Sebastian Ullrich]

Yes, but there is a general kind of tactics that "manipulate" a given hypothesis where users might not think of it being referenced and then rebound but changed "in place"

[Mario Carneiro]

I agree that at h can have this kind of treatment

[Mario Carneiro]

idents are just so common throughout the grammar that it seems we need to make common things easy (rather than easy to get slightly wrong)

[Sebastian Ullrich]

In the end, there is the question of whether we want to allow use of macros for either of these currently closed categories, binders and hypothesis references. Because that's what this really is, a macro for an internal identifier. But I understand that it is also common enough that we might want to solve its issues without touching macro support at large in that place.

[Mario Carneiro]

why can't it just be a regular word? There are only a small handful of things that need to be patched to make that work, but if you grep for uses of ident in lean4 and mathlib4 it's just depressing how many things have to be reviewed

[Mario Carneiro]

macros for idents is definitely a can of worms. I have no idea how feasible that really is

[Mario Carneiro]

if this 7 year old rust RFC on the topic is any indication

[Sebastian Ullrich]

Yeah, I'm definitely not suggesting to touch more than the two limited categories I mentioned. Some discussion on how this could be preserved as an ident and issues with that happened in the original issue https://github.com/leanprover/lean4/issues/821

[Mario Carneiro]

Because that's what this really is, a macro for an internal identifier.

I'm not sure how this definition doesn't also say that identifiers are macros for internal identifiers though

[Mario Carneiro]

Here's a fun example:

variable (this : Nat)
include this

Hard to see how to do that with macro-this

[Mario Carneiro]

oof...

/--
...
The form `#help option id` will show only options that begin with `id`.
-/
elab "#help" &"option" id:(ident)? : command => do

[Mario Carneiro]

actually this one is spoiled by any keywords at all. Isn't there a rawIdent for this?

[Sebastian Ullrich]

Mario Carneiro said:

Here's a fun example:

variable (this : Nat)
include this

Hard to see how to do that with macro-this

I've asked about this above without an answer, but now I'm getting more convinced that in any solution (that requires customizing how this behaves as a reference), this should not be available as a binder name. Allowing users to introduce a magical identifier name whose hygiene behavior is different from any other identifier is a catastrophe. It should only be introduced by custom anaphoric elaborators like have, and by "hypothesis manipulating" tactics like discussed above.

[Mario Carneiro]

Allowing users to introduce a magical identifier name whose hygiene behavior is different from any other identifier is a catastrophe.

I think this is the root of the issue. I disagree that this should be magical at all. It's just a variable name with no magical hygiene behavior

[Mario Carneiro]

The magic is entirely contained to macros that want to create a hygiene-less this identifier, e.g. have :=, which macros can already easily do using $(mkIdent `this)

[Sebastian Ullrich]

That was exactly the state when https://github.com/leanprover/lean4/issues/821 was opened

[Mario Carneiro]

We already have many tactics in mathlib4 that do this kind of thing with names other than this, for example by_cases which introduces h instead

[Mario Carneiro]

yes, I'm suggesting that the fix be reverted because the cure is worse

[Sebastian Ullrich]

I see, then at least I understand your PoV now

[Mario Carneiro]

while looking at examples I even found an example which is using this kind of trick for this itself:

macro_rules
  | `(tactic| by_contra'%$tk $[_%$under]? $[: $ty]?) =>
    `(tactic| by_contra' $(mkIdentFrom (under.getD tk) `this (canonical := true)):ident $[: $ty]?)
  | `(tactic| by_contra' $e:ident) => `(tactic| (by_contra $e:ident; push_neg at $e:ident))
  | `(tactic| by_contra' $e:ident : $y) => `(tactic|
       (by_contra' h;
        -- if the below `exact` call fails then this tactic should fail with the message
        -- tactic failed: <goal type> and <type of h> are not definitionally equal
        have $e:ident : $y := by { push_neg; exact h };
        clear h ) )

[Sebastian Ullrich]

For the sake of completeness, a solution for keeping this as a regular identifier but make it work inside quotations as well would be for the have elaborator to attach the caller's macro scopes (if any) to the introduced identifier. But that's not a concept that really exists in the current macro system.

[Mario Carneiro]

Can that be done by using %$tk stuff like in the above example?

[Sebastian Ullrich]

That is, if the have keyword had macro scopes, we could transplant them onto this. But currently only identifiers carry macro scopes.

[Mario Carneiro]

another possibility is to have a macroScope parser that parses nothing but captures the scope into an identifier

[Mario Carneiro]

kind of like ident except it parses the empty string

[Mario Carneiro]

so then you could introduce that in a parser like have :=

[Sebastian Ullrich]

Yes, some kind of special node the quotation elaborator attaches macro scopes to, instead of to all keywords which sounds wasteful (though Racket essentially does it, as it doesn't have a concept of keywords anyway)

[Mario Carneiro]

it still probably would not be enough to write tactics like by_contra' without using $(...), since you would in most cases want to combine the macro scopes from this special node, the span from another node, and a name like "this" to form the resulting identifier

[Sebastian Ullrich]

It's not really possible to combine macro scopes from different sources - in the end, they represent a single lexical scope from the input. But it should be possible to forward the captured scopes so that macros like by_contra' can put this in their caller's scope.

[Mario Carneiro]

sorry, I didn't mean to combine multiple macro scopes. I meant that you might want to assemble an identifier from a string, a span, and a macro scope, all coming from different places

[Mario Carneiro]

in the by_contra' example we want the span to come from either the by_contra' token or the _, the macro scope to come from the proposed macroScope node (that would be added as an additional parser in by_contra'), and the string is "this", written explicitly in the macro source somehow

[Mario Carneiro]

the present implementation has 2 out of those 3 things; the macro scope is currently empty (unhygienic) due to use of mkIdentFrom

[Mario Carneiro]

the point being that if you want some fancy sigil expression it will have to take at least 3 things, which will be a bit of a mess: this%$tk%!scope?

[Mario Carneiro]

at that point it seems preferable to just use $(...) and call a proper function

[Sebastian Ullrich]

Oh yes, this is such a special case (on the definition side) that it should just be a mkIdent variant

[Sebastian Ullrich]

Or rather something like

 | `(tactic| by_contra'%$tk $ms:macroScopes $[_%$under]? $[: $ty]?) =>
   `(tactic| by_contra' $(mkIdentFrom (under.getD tk) (ms.applyMacroScopes `this) (canonical := true)):ident $[: $ty]?)