Enter lambda in `conv`

Stream: general

[Yury G. Kudryashov]

I should read docs before asking questions.

[Yury G. Kudryashov]

Though I still have a question: how hard is it to make conv aware of ext? Now I can call funext to enter a function but it would be nice to be able to call ext to enter anything.

[Mario Carneiro]

Actually, I think congr or to_args or whatever it is called should do this

[Mario Carneiro]

ext doesn't make as much sense inside conv since most extensionality lemmas don't have the right form

[Yury G. Kudryashov]

congr doesn't.

[Yury G. Kudryashov]

funext worked but it doesn't allow me to name the new variable.

[Mario Carneiro]

that's odd

[Mario Carneiro]

intro is also a reasonable synonym here

[Mario Carneiro]

I think the story for navigating terms in conv needs improvement on the whole. to_lhs and to_rhs aren't nearly enough

[Mario Carneiro]

Here are the basic conv tactics I can see a use for. I've tried to borrow names when the tactics have a similar effect, but the underlying theorems are often quite different. It's hard to say which drives the mental model more.

• arg i: enter the i-th nondependent argument of an application, intro on binders
• args: enter all nondependent arguments of an application
• left, to_lhs: synonym for arg n-2
• right, to_rhs: synonym for arg n-1
• intro x, ext x, funext x: enter the body of a pi or lambda.
• intros: same repetition behavior as intros tactic
• apply h: rewrite the entire goal with h by transitivity
• rw h: rewrite with h somewhere in the goal
• enter [1,3,x,y]: iterate arg and intro with the given arguments
• pattern (_+_): find the first matching subterm (in top down left right order)

Many of these already have equivalent functions, but I think we should try to organize the whole set and bikeshed on names until this is as usable as regular tactic mode

[Johan Commelin]

One reason why I don't use conv mode that much is that it seems to me it is often quite slow and not so responsive... do others recognise this?

[Mario Carneiro]

It shouldn't be any slower than any other tactic; what conv does in its most basic mode is extremely simple, essentially just apply eq.mp

[Mario Carneiro]

More conv tactics:

• convert y: produce a subgoal |- goal = y in regular tactic mode
• trans y: produce a tactic subgoal |- goal = y and a conv subgoal | y
• tactic { tac }: use a regular tactic as a conv tactic (the tactic sees the goal |- goal = ?m1). (This is the identity function under the hood)
• done, refl: close the goal by reflexivity (should be optional most of the time)

[Patrick Massot]

Please don't make intro different from intros.