apply ... to

Stream: general

[Kevin Buzzard]

@Patrick Massot were you talking about a similar thing recently? I have hpq : P -> Q and I have h : P and I just want to write apply hpq to h. These are important things for maths beginners who often reason forwards. Currently I have to write replace h with hpq h which is somehow less ideal.

[Kenny Lau]

specialize hpq h

[Kevin Buzzard]

I am fixing all of this stuff in a modded version of Lean tactic mode.

[Kevin Buzzard]

apply hpq to h still looks easier to understand

[Kevin Buzzard]

can you write me an apply' tactic which does this all automatically?

[Kevin Buzzard]

Or else I might have to learn about parsers

[Kenny Lau]

import tactic.interactive

namespace tactic
namespace interactive

open interactive lean.parser interactive.types

meta def apply' (source : parse ident) (target : parse $ tk "at" *> ident) : tactic unit :=
do e1 ← get_local source,
   e2 ← get_local target,
   replace target none (some $ ``(%%e1 %%e2))

end interactive
end tactic

example (p q : Prop) (hpq : p → q) (hp : p) : true :=
begin
  apply' hpq at hp,
  guard_hyp hpq := p → q, guard_hyp hp := q,
  trivial
end

[Patrick Massot]

specialize sounds good when the assumption is a forall, but not so much when it's an implication. But in any case I think you can't completely avoid the idea that hpq h is a thing

[Kevin Buzzard]

@Kenny Lau thanks! The coolest thing would be if apply' did everything apply did too.

[Kenny Lau]

apply works backwards right

[Kenny Lau]

apply (hpq : p -> q) turns the goal from q to p

[Kenny Lau]

so I'm not sure what you mean by "everything apply did"

[Kevin Buzzard]

I mean apply' h just does the same as apply h but apply' h at h2 does the new thing. Sort of an extension to the tactic, not a new one.

[Kevin Buzzard]

In a parallel universe, apply does that already.

[Kevin Buzzard]

Like this parallel universe version of symmetry: https://github.com/leanprover-community/mathlib/blob/fa1dcb65c64c23d3d9eef1d8b0f18fc8e936db17/src/tactic/interactive.lean#L641

[Johan Commelin]

I think the point is that apply works backwards on the goal, and dually it makes perfect sense to let apply work forwards on hypotheses.

[Andrew Ashworth]

:( apply is bad style for beginners anyway, because they will want to write long chains of apply x, apply y, apply z at h instead of using have

[Kevin Buzzard]

what is wrong with that, from a purely "I'm just getting to learn Lean" point of view?

[Kevin Buzzard]

I'm interested in teaching mathematicians not to be scared of the software, I'm less worried about style.

[Johan Commelin]

I find it really quite interesting that there is such a big diffence in the way that mathematicians and CSists approach Lean when they are beginning.

[Andrew Ashworth]

it's more like all of original Isabelle was huge sequences of apply, and the they invented Isar and found out structured proofs were easier to maintain

[Johan Commelin]

But that doesn't mean that it's also easier for beginners

[Andrew Ashworth]

CS students also enjoy the straightforward way ;p

[Johan Commelin]

Right, and mathematicians seem to think that the straightforward way is: apply this_lemma, apply that_lemma, assumption

[Johan Commelin]

Especially if you can also say apply lemma_foo to hyp_bar

[Andrew Ashworth]

That is not how a paper proof goes though...

[Andrew Ashworth]

A paper proof would have a bunch of lemmas, then knock out the goal by stringing them together

[Johan Commelin]

I've had lots of mathematicians get really confused by the fact that hypotheses have names. And the fact that you have to cook up names for your have statements, or use some unnatural this.

[Andrew Ashworth]

you could use french quotes if you wanted to be verbose, but I understand it is tedious

[Johan Commelin]

Maybe \f< claim \f> is what mathematicians would find most natural.

[Johan Commelin]

Anyway, it's not the experience that we see on this chat.

[Johan Commelin]

We see CS beginners be really happy with term mode proving. (Tactics are hard and crazy and for complicated proofs.)

[Andrew Ashworth]

hypotheses don't need descriptive names, they can be called boring things like H1_1

[Johan Commelin]

OTOH math beginners are completely confused, and get stuck with the term mode tutorials.

[Johan Commelin]

We show them tactic mode and they are extremely happy

[Johan Commelin]

Because it feels to them that we just turned Lean into some FPS

[Andrew Ashworth]

I think that is obvious from how they are used, though. In CS, the definition is almost always in Type, and represents a computer algorithm. So you don't define such a thing using tactics because you want to control exactly how it is implemented

[Andrew Ashworth]

The whole idea you would want to have some unknown tactic define your definition is foreign

[Andrew Ashworth]

You don't know what it does, and you can't inspect it easily without printing it

[Johan Commelin]

Right! I'm still waiting for tidy' that can be used to fill in data that is obvious'.

[Johan Commelin]

If type class inference can figure out that my goal is unique, maybe I really don't care what tidy' spits out. (Apart from the usual concerns about speed optimizations etc...)

[Andrew Ashworth]

Anyway, if the instructor is happy with apply, I guess that's the thing that matters, hah. My thinking is, we want our proofs to look like slightly formal versions of paper proofs, so we avoid long chains of apply. If these long apply chains can be automated, we use a tactic to clear the goal, otherwise there's mathematical content and should be structured for readability.

[Kevin Buzzard]

I have no interest in readability at this point. All I want to do is to show mathematicians that proofs can be checked on a computer. I don't care what mess they generate.

[Kevin Buzzard]

It's like Euclid the game -- you don't have to do it optimally.

[Kevin Buzzard]

You should have seen my construction of the regular pentagon.

[matt rice]

@Johan Commelin

Maybe \f< claim \f> is what mathematicians would find most natural.

We see CS beginners be really happy with term mode proving. (Tactics are hard and crazy and for complicated proofs.)

fwiw, as a CS person, I tend to prefer this term-mode + \f< claim \f>/nameless binding style...
Occasionally i bind to named, when using let, or have with a very long type, when \f< style doesn't aid readability...

[Johan Commelin]

What's really sad with term-mode proofs is that you can not "replay" them in the goal state window.

[Johan Commelin]

This "replaying" is a killer feature of tactic proofs.

[Kevin Buzzard]

I know you're about to race out the door Johan but how would you envisage this working?

[Kevin Buzzard]

Clicking on a term in a term mode proof could do something -- but what do you want it to do?

[matt rice]

I don't know, but when working _on_ proofs, i tend to keep the goal state around by some silly tactic like have 0 = 0, by refl and by the time i'm done i hope to have the stack of goals readable from the proof itself ideally, agree though that workaround for replaying is kind of sad.

[Andrew Ashworth]

ideally there'd be some sort of helper vscode action that automatically wraps a term in a hole or tactic and prints out the goal state

[Floris van Doorn]

In Lean 2 you could point your mouse at an opening parenthesis, and it would show you the type of the term inside said parentheses. This was quite nice, you could see a little better what was going on. Sometimes you had to manually add extra parentheses in a term to see what was going on.
I'm not sure why this feature was removed from Lean 3.

[Jeremy Avigad]

It was a nice feature. I remember when Leo and Soonho got it to work. It required some real hacking: hovering over the parengot the server to introduce an id around the expression, re-elaborate the term, and then look at what was inferred for the metavariable that stood for the type argument to id. My guess is that at a later rewrite of the server, Leo lacked the time and energy to get it to work again.