term mode haveI

Stream: new members

[Bhavik Mehta]

What's the term mode way of writing the following?

begin
  haveI := foo,
  exact bar
end

[Reid Barton]

There isn't really one, other than @

[Bhavik Mehta]

Oh, there isn't some letI ... in construction I can do?

[Bhavik Mehta]

I was sure I'd seen one in some code somewhere

[Mario Carneiro]

The term mode version is

by haveI := foo; exact
bar

[Mario Carneiro]

by exactI also works in some cases (if you are just picking up some instance from the context)

[Bhavik Mehta]

Ahh that's what I was thinking of, thanks!

[Bhavik Mehta]

Yeah in this case it's something which shouldn't be an instance but I need it in this (otherwise one-line) lemma

[Reid Barton]

In that case I'm guessing that the class it is shouldn't be a class in the first place :upside_down:

[Mario Carneiro]

You can also use local instance inside a section for the lemma, if you need it for the statement of the theorem

[Bhavik Mehta]

Reid Barton said:

In that case I'm guessing that the class it is shouldn't be a class in the first place :upside_down:

def mono_is_regular {A B : C} (m : A ⟶ B) [mono m] : regular_mono m :=

[Kevin Buzzard]

I thought that exact a $ b didn't work, or is that only true within a begin end block?

[Mario Carneiro]

it doesn't work

[Mario Carneiro]

or rather, it works and does something no one ever wants

[Kevin Buzzard]

So do you lose $ functionality in your term mode suggestion above?

[Mario Carneiro]

yes

[Bhavik Mehta]

as I'm just discovering

[Kevin Buzzard]

rofl

[Kevin Buzzard]

Is this a bug, or an issue with parsing that can't be fixed for some reason?

[Mario Carneiro]

You can still put everything in bar in parentheses and use $ therein

[Bhavik Mehta]

Yup this is what I did ^

[Bhavik Mehta]

But was very confused until I saw these messages

[Mario Carneiro]

The problem is that $ is interpreted as a tactic combinator, i.e. exact foo $ bar becomes (exact foo) bar

[Kevin Buzzard]

I've never known why this was the case. It's really annoying sometimes.

[Kevin Buzzard]

which is why { } fixes it

[Mario Carneiro]

which doesn't ever work because exact foo has type tactic unit so it expects bar to have type tactic_state and this is what the error message says

[Mario Carneiro]

The reason for this is because $ has an absurdly low precedence value of 1

[Reid Barton]

So does "interactive tactic application" have a special precedence? After all rw f x works even though you might expect it not to

[Mario Carneiro]

and the standard expr parser used in tactics, texpr, uses a precedence value of 2. See also this doc:

/-- A 'tactic expression', which uses right-binding power 2 so that it is terminated by
    '<|>' (rbp 2), ';' (rbp 1), and ',' (rbp 0). It should be used for any (potentially)
    trailing expression parameters. -/
meta def texpr := parser.pexpr tac_rbp

The comment fails to mention that $ is also one of the terminating tokens (rbp 1)

[Reid Barton]

aha

[Reid Barton]

Soooo can we just change $ to 3 (or maybe 2)?

[Mario Carneiro]

This will make <|> lower precedence than $

[Mario Carneiro]

which seems undesirable, although I can probably live with it

[Mario Carneiro]

It seems to me that a better solution, if possible, would be to treat the <|>, ; and , tokens specially inside a begin-end block, so that they aren't necessarily tied to the standard meaning of these tokens in term mode

[Reid Barton]

Ahh, I see... you want $ to have lower precedence than <|> in term mode, but higher precedence in an interactive tactic?

[Mario Carneiro]

I guess the issue is a parser ambiguity where exact tac1 <|> tac2, in a context where you are defining a tactic using tactics for some reason, could mean either (exact tac1) <|> tac2, i.e. apply tac1 and call tac2 if that doesn't work, or exact (tac1 <|> tac2), i.e. solve the goal using tac1 <|> tac2

[Reid Barton]

(<|> could also be constructing many things other than tactics.)

[Mario Carneiro]

indeed

[Mario Carneiro]

I don't even know what exact foo $ bar <|> baz should be interpreted as

[Reid Barton]

Probably (exact (foo $ bar)) <|> baz, on the basis of probability

[Reid Barton]

& backwards compatibility regarding <|>

[Mario Carneiro]

Who wants to try changing core so that $ has precedence 3 and see what breaks?

[Reid Barton]

Bhavik Mehta said:

[mono m]

Yeah, all these properties being classes makes it dreadfully tedious to prove things about them.