apply at

Stream: general

[Kevin Buzzard]

tl;dr: how hard is to make this work:

import Mathlib.Tactic

open Nat

theorem succ_inj2 (a b : Nat) : succ a = succ b → a = b := by simp

example (a b : Nat) (h : succ a = succ b) : a = b := by
  apply succ_inj2 at h -- `h` becomes `a = b`

We have a preliminary version in NNG4:

https://github.com/hhu-adam/NNG4/blob/0eb7817cf9cb71a33b0f92d6b29a2c9f88acf165/Game/Tactic/Apply.lean#L15-L16

but it desugars to replace h := succ_inj2 h which is no good here; apply t at h works fine if t : P -> Q but succ_inj2 has got explicit inputs before P which need to be filled in by unification.

Basically, apply t changes the goal Q to P even if the type of t is \forall x, P -> Q . I'd like apply at to be as flexible. Is this difficult?

---

Here's why I would love this.

Mathematicians typically don't get taught logic formally and are expected to pick it up themselves. As a consequence they figure out that arguing forwards is normal, don't ever really see examples of arguing backwards, and so the moment they leave the main path of the natural number game (which only uses rw and induction) and run into apply, they are totally confused for two reasons: firstly because mathematicians use the word "apply" to mean lots of things (e.g. "rewrite") and secondly because when they are using it in the context of an implication, 9 times out of 10 they are applying t : P -> Qto a hypothesis h : P rather than to \|- Q.

In NNG3 I mitigated against this by making function world and proposition world, which introduce apply very slowly in an abstract context of P -> Q with P : Prop. These are the only two worlds in the Lean 3 version of the game which have variables of type Type or Prop; every other thing they see has type Nat or is a proof.

I was convinced in 2019 that this was the way to teach tactics like intro and apply, but then I learnt from Patrick that he teaches these tactics "by example", so the students never see P -> Q, they see mathematically meaningful props like $x=2\implies x^2=4$. So I'm ripping out function and proposition world and going straight into advanced addition world and teaching intro, apply and exact in this context, rewriting the entire world to have far more tutorial elements where these tactics are taught in the context of theorems about numbers. It's going really well -- I like the new version much better than I like NNG3 function and proposition world. But rewriting these levels made me realise that actually one way of teaching apply would be by teaching apply at first and then apply second, and if the students remain confused about arguing backwards they can just apply at their way through the levels. However it's really common that my lemmas have explicit inputs, it turns out, so right now I can't write them because with my current set-up apply at won't eat succ_inj2 a b and fails if I just give it succ_inj. @Alex J. Best you say you're sometimes looking for small tactic projects -- is this small, or is it a nightmare?

[Jireh Loreaux]

Kevin, I think the trickiest part of this is that the expected type is not known, so how do you determine which arguments are fillable?

For example, if have

variable {p q r s : Prop}

example (h : p → q → r → s) (hp : p) (hq : q) : r → s := by
  apply h
  · exact hp
  · exact hq

Then when I call apply, Lean can unify the goal with the end of h to see, oh, I'll do refine h ?_ ?_ and get something of the correct type. But what would you expect apply h at hp to do here?

example (h : p → q → r → s) (hp : p) (hq : q) : r → s := by
  apply h at hp
  -- hp : ???
  -- what new goals are there, if any?

[Shreyas Srinivas]

Coq does what Kevin asks.

[Jireh Loreaux]

What does it do in my example above?

[Shreyas Srinivas]

One minute. Typing it in CoqIDE.

[Adam Topaz]

Why cant you unify the type of hp with the leftmost parameter of f where it works, introduce metavariables for everything to the left of that, and return the result of applying the function?

[Jireh Loreaux]

ah, I just realized I misread Kevin's intended use case. I think what Adam says makes sense.

[Jireh Loreaux]

And then with that behavior in my example it would yield hp : q → r → s and no new goals.

[Shreyas Srinivas]

Coq did something much stranger than I expected on that example. Here's a proof of dni that works as I expected:

Require Import Coq.Unicode.Utf8.

Lemma dn_introduction : ∀ P : Prop, P → ¬¬P.
Proof.
  intros P hP.
  unfold not.
  intro hnp.
  apply hnp in hP.
  exact hP.
Qed.

[Shreyas Srinivas]

For an explanation see : forward and backward reasoning

[Shreyas Srinivas]

On your example @Jireh Loreaux it changed the hypothesis h to s

[Adam Topaz]

Changing h to s by adding goals for q and r, you mean?

[Shreyas Srinivas]

Basically yes.

[Shreyas Srinivas]

I am not sure anymore if this is what Kevin wants.

[Shreyas Srinivas]

@Adam Topaz : May I PM you to understand why Coq just did that? Don't want to hijack the thread.

Forward reasoning definitely feels more intuitive for basic logic.

[Kevin Buzzard]

I know it's very cute that apply h : p -> q -> r does something cute when the goal is r, but I think this is a pretty niche use and I'd be happy if it was not covered by apply...at. In all the examples I've seen in NNG h is of the form Nat -> Nat -> ... -> Nat -> q -> r where q and r depend on the nats, you apply it at hq : q(37,42...) and get hr : r(37,42,...).

Shreyas, thanks for pointing out that Coq already has this.

[Ioannis Konstantoulas]

Being new to tactics, I start about 75% of all my tactic proofs with apply...at. I know it doesn't work, and yet I still mechanically write it. Sometimes I write it even though I know it doesn't work, as a visual marker for "ok, now how do I make this work".

[Kevin Buzzard]

It works in NNG (but only for functions which have no explicit numerical inputs)

[Adam Topaz]

Well, I got something to kind of work:

import Mathlib.Tactic
import Lean

namespace Mathlib.Tactic
open Lean Meta Elab Tactic Term

elab "apply" t:term "at" i:ident : tactic => do
  let fn ← Term.elabTerm t none
  let fnTp ← inferType fn
  unless fnTp.isForall do throwError "oops!"
  let (ms, _, foutTp) ← forallMetaTelescopeReducing fnTp (some 1)
  let finTp ← inferType ms[0]!
  let ldecl ← (← getLCtx).findFromUserName? i.getId
  let (mvs, outTp) ← show TacticM (Array Expr × Expr) from do
    let mut mvs := #[ms[0]!]
    let mut cmpTp := finTp
    let mut outTp := foutTp
    while !(← isDefEq cmpTp ldecl.type) do
      unless outTp.isForall do throwError "oops!"
      let (ms, _, newfoutTp) ← forallMetaTelescopeReducing outTp (some 1)
      mvs := mvs ++ ms
      cmpTp ← inferType ms[0]!
      outTp := newfoutTp
    mvs := mvs.pop
    return (mvs, outTp)
  let mainGoal ← getMainGoal
  let mainGoal ← mainGoal.tryClear ldecl.fvarId
  let mainGoal ← mainGoal.assert ldecl.userName outTp (mkAppN fn (mvs.push ldecl.toExpr))
  let (_, mainGoal) ← mainGoal.intro1P
  replaceMainGoal <| [mainGoal] ++ mvs.toList.map fun e => e.mvarId!


variable (α β γ δ : Type*) (f : α → β → γ → δ)

example (g : γ) (a : α) (b : β) : δ := by
  apply f at g
  assumption
  assumption
  assumption

open Nat

theorem succ_inj2 (a b : Nat) : succ a = succ b → a = b := by simp

example (a b : Nat) (h : succ a = succ b) : a = b := by
  apply succ_inj2 at h
  assumption

[Adam Topaz]

I haven't tested it much, and it certainly needs better errors.

[Kevin Buzzard]

example (A B C : Prop) (ha : A) (f : A → B) (g : B → C) : C := by
  apply f at ha -- ha : B
  apply g at ha -- error: oops!
  exact ha

I am very impressed that you've managed to make this fail! How can the first apply work but not the second?

[Kevin Buzzard]

example (A B C : Prop) (ha : A) (f : A → B) (g : B → C) : C := by
  apply f at ha -- ha : B
  have h := ha -- h : B
  apply g at h -- error: failed
  exact ha

[Adam Topaz]

hmmm ok. I'll try to fix this when I have time later today.

[Adam Topaz]

The issue is that the local declaration is not getting updated for some reason after the first apply. So clearly there's some bug.

[Jannis Limperg]

The isForall checks look suspicious to me. forallMetaTelescopeReducing will already perform similar (but less strict) checks. They at least need a consumeMData.

[Adam Topaz]

Yeah, but i think even if I pass some 1 to forallMetaTelescopingReducing the resulting mvar array will have at most 1 element. I wanted to ensure there is exactly one.

[Jannis Limperg]

Then I would check the array size afterwards.

[Adam Topaz]

Fair enough.

[Adam Topaz]

Keep in mind that this is probably the first time I’ve tried to write an actual tactic. Im sure that there are various other issues with this code as well. Any advice would be much appreciated!

[Damiano Testa]

I think that replacing the first line of the tactic with

elab "apply" t:term "at" i:ident : tactic => do (← getMainGoal).withContext do

(i.e. work in the context of the main goal) should fix the issues.

[Adam Topaz]

Yeah that's exactly the issue. Here's my fix:

import Mathlib.Tactic
import Lean

namespace Mathlib.Tactic
open Lean Meta Elab Tactic Term

elab "apply" t:term "at" i:ident : tactic => withMainContext do
  let fn ← Term.elabTerm t none
  let fnTp ← inferType fn
  let (ms, _, foutTp) ← forallMetaTelescopeReducing fnTp (some 1)
  unless ms.size == 1 do throwError "oops!"
  let finTp ← inferType ms[0]!
  let ldecl ← (← getLCtx).findFromUserName? i.getId
  let (mvs, outTp) ← show TacticM (Array Expr × Expr) from do
    let mut mvs := #[ms[0]!]
    let mut cmpTp := finTp
    let mut outTp := foutTp
    while !(← isDefEq cmpTp ldecl.type) do
      let (ms, _, newfoutTp) ← forallMetaTelescopeReducing outTp (some 1)
      unless ms.size == 1 do throwError "oops!"
      mvs := mvs ++ ms
      cmpTp ← inferType ms[0]!
      outTp := newfoutTp
    mvs := mvs.pop
    return (mvs, outTp)
  let mainGoal ← getMainGoal
  let mainGoal ← mainGoal.tryClear ldecl.fvarId
  let mainGoal ← mainGoal.assert ldecl.userName outTp (mkAppN fn (mvs.push ldecl.toExpr))
  let (_, mainGoal) ← mainGoal.intro1P
  replaceMainGoal <| [mainGoal] ++ mvs.toList.map fun e => e.mvarId!

variable (α β γ δ : Type*) (f : α → β → γ → δ)

example (g : γ) (a : α) (b : β) : δ := by
  apply f at g
  exact g
  exact a
  exact b

open Nat

theorem succ_inj2 (a b : Nat) : succ a = succ b → a = b := by simp

example (a b : Nat) (h : succ a = succ b) : a = b := by
  apply succ_inj2 at h
  exact h

example (A B C : Prop) (ha : A) (f : A → B) (g : B → C) : C := by
  apply f at ha
  apply g at ha
  exact ha

[Adam Topaz]

I also applied Jannis's suggestion.

[Kevin Buzzard]

This is now working in all examples so far in NNG4! Thanks so much Adam!

[Adam Topaz]

If people think this is actually useful, then I can work on cleaning it up and open a mathlib pr…

[Kevin Buzzard]

It's definitely going in NNG4, and so if you don't PR we'll get people coming from NNG complaining that apply at doesn't work, on top of the usual complaints that rfl and rw close goals too quickly :-)

[Adam Topaz]

Adam Topaz said:

If people think this is actually useful, then I can work on cleaning it up and open a mathlib pr…

PR here: #7527

[Joachim Breitner]

Nice!

So parameters before the one that marches the hypothesis are turned into metavariables, and arguments afterwards are left as premises in the remaining hypothesis, correct? It makes sense from an implementation point of view, but is it the best user experience? Or would we expect something more symmetric?
For example if I have use apply Nat.lt_of_le_of_lt at h the result looks quite different if h : a < b or h : a ≤ b (I assume).
What does Coq or Isabelle do in that case?

[Shreyas Srinivas]

When applying hypothesis h :p -> q -> r -> .. -> t at HP :p , Coq modified HP to HP: t and all of q, r,... into goals

[Shreyas Srinivas]

As for UX, maybe this is fine for experts, but it was very unintuitive for me. Backward reasoning felt easier at that point.

[Kevin Buzzard]

Trust me, a gazillion highly non expert mathematicians find forward reasoning very intuitive and backwards reasoning very weird

[Joachim Breitner]

I guess for me Coq's behavior is relatively intuitive, but maybe that's because I used Coq before :-)

[Kevin Buzzard]

My users aren't going to be applying anything more complex than stuff like succ_inj at things

[Shreyas Srinivas]

Kevin Buzzard said:

Trust me, a gazillion highly non expert mathematicians find forward reasoning very intuitive and backwards reasoning very weird

Kevin I agree. I just think what Adam described is different from what Coq seems to do, and unlike Coq, it matches what you want. You wish to automate the function application that takes h : p -> q and hp : p and sets hp to hp : q. That is not what coq seems to do (EDIT: for more complicated cases like Jireh's example)

[Patrick Massot]

Kevin, the short version is: the whole discussion of what Coq does was actually completely irrelevant.

[Adam Topaz]

Joachim Breitner said:

Nice!

So parameters before the one that marches the hypothesis are turned into metavariables, and arguments afterwards are left as premises in the remaining hypothesis, correct? It makes sense from an implementation point of view, but is it the best user experience? Or would we expect something more symmetric?
For example if I have use apply Nat.lt_of_le_of_lt at h the result looks quite different if h : a < b or h : a ≤ b (I assume).
What does Coq or Isabelle do in that case?

Yes that is indeed what this tactic does. I don't know what coq actually does except for the example that was posted above in this thread, but at least in that example, the behavior is different. Yes, the result will indeed look different if one applies Nat.lt_of_le_of_lt.

[Adam Topaz]

And thanks all for the comments! I'll definitely add some tests!

[Kevin Buzzard]

Re the Coq tactic: oh sorry I misunderstood. I thought the difference was only in these funny p->q->r cases which are not relevant to me

[Shreyas Srinivas]

@Adam : one quick question. Since this Coq comparison came up again, I checked and Coq's apply also works with \iff. It automatically seems to figure out which side matches the hypothesis. Is this feasible for the tactic you are writing?

[Adam Topaz]

It's certainly possible to extend this to allow for iff as well, but maybe I'll leave that to a future PR :)

[Adam Topaz]

Ok, I added some tests to #7527 and added some code to make sure that instances are properly synthesized.

[Patrick Massot]

Do I understand from the test

example {α β : Type*} (f : α → β) (a : α) : β := by
  apply f at a
  guard_hyp a :ₛ β
  exact a

that this is meant to subsume apply_fun ... at ...?

[Adam Topaz]

No it doesn’t really subsume apply_fun which works for hypotheses of the form a = b and there f is a function whose domain is the type of a.

[Notification Bot]

A message was moved here from #general > Arbitrary Metaprograms by Adam Topaz.

[Adam Topaz]

I tried to understand what Damiano is suggesting with MVarId.apply, but I’m not sure what the intention is.

[Notification Bot]

A message was moved here from #general > Arbitrary Metaprograms by Adam Topaz.

[Adam Topaz]

(sorry, typing on mobile…)

[Adam Topaz]

I added the following test which shows how apply at can mimic at least some of the behavior of apply_fun:

example {α β : Type*} (f : α → β) (a b : α) (h : a = b) : f a = f b := by
  apply congr_arg f at h
  guard_hyp h :ₛ f a = f b
  exact h

[Patrick Massot]

Sorry, I read the test too quickly.

[Damiano Testa]

Adam Topaz said:

I tried to understand what Damiano is suggesting with MVarId.apply, but I’m not sure what the intention is.

What I was trying to achieve was to let Lean unify the argument of f with the hypothesis b, rather than doing it yourself. I have found that constructing the proof term "by hand" is more brittle than tapping into the MVarIds and using Lean.MVarId.apply to figure out the arguments. This is why I then had the extra step of trying to unify one of the leftover goals with b.

I wonder whether this would also take care of synthesizing typeclass assumptions. However, I do not think that I'll have time to try this today.

[Adam Topaz]

Ok, I think I understand @Damiano Testa -- IIUC the strategy you want to take is this:

1. After the let (mvs, bis, tp) ← forallMetaTelescopeReducingUntilDefEq (← inferType f) ldecl.type line, make a new mvar with type tp.
2. Apply the original f to this new mvar to obtain whatever goals pop up.
3. Fill in the "last" goal with the local declaration i.

Is that what you have in mind?

[Adam Topaz]

This would indeed work, I guess. But apply still has an issue with typeclass instances IIRC. I.e. this will fail if there are typeclass parameters which can't be synthesized automatically.

[Adam Topaz]

With the code in my PR, any such typeclass parameters should pop up as new goals, see the following test for example:

example {G : Type*} [Monoid G] (a b c : G) (h : a * c = b * c)
    (hh : ∀ x y z : G, x * z = y * z → x = y): a = b := by
  apply mul_right_cancel at h
  guard_hyp h :ₛ a = b
  · exact h
  · guard_target = IsRightCancelMul G
    constructor
    intros a b c
    apply hh

[Damiano Testa]

Ok, I had not tested the typeclass behaviour, and I hoped that apply would take care of this on its own. If however you have to jump through lots of hoops instead, then manually trying to synthesize the intermediate arguments is a good approach.

Thanks for the check!

[Adam Topaz]

Thanks for the suggestion! BTW, I still think changing the default behaviour of apply to introduce goals for missing type class parameters might be a good thing…

[Damiano Testa]

Yes, or at least call @pply the tactic that does it.

[Damiano Testa]

Ah, have you tried if the tactic gets tripped up by metadata?

[Adam Topaz]

no... do you have an example in mind?

[Damiano Testa]

(Sorry, I'm about to not have internet for a while!)

[Damiano Testa]

Usually, having lets around adds metadata...

[Adam Topaz]

I'll try...

[Adam Topaz]

Aha, so this works:

example {α β : Type*} (a : α) (f : α → β) : β := by
  let a' := a
  apply f at a'
  exact a'

except after apply f at a' the actual value is dropped.

[Adam Topaz]

Although this looks to be similar to the behavior of apply_fun, so maybe it's not a big issue?

[Kevin Buzzard]

Today marks the first time someone complained that apply at doesn't work in mathlib ;-) (we have it up and running locally in NNG on an Imperial server).