An `exists_intro` tactic?

Stream: Is there code for X?

[Igor Khavkine]

Are there (could there be) tactics analogous to intro and revert but for ∃ quantifiers?

I'm a new Lean user and I've been trying my hand at writing some non trivial formalizations. I like how there are Lean tactics that correspond to steps in informal mathematical reasoning (initially Terry Tao's dictionary was a good guide for me). But I've found that there's currently an asymmetry between the tactics for dealing with ∀ and ∃ quantifiers.

The problem of course has to do with manipulating the goal or a hypothesis under quantifiers. For transformations that involve equality or iff, this to some degree can be done by simp, rw and simp_rw. But for modifications that change the strength of the goal or hypothesis, one has to use intro, obtain, ...

I have seen the peel tactic, that can match sequences of quantifiers between the goal and a hypothesis, which then allows for interactive simplification. But that requires a hypothesis with the appropriate quantifier structure to exist. In practice, with a complicated goal, it might be tedious to build such a hypothesis by hand.

[Igor Khavkine]

Here's a toy example that illustrates the difference for a ∀ goal.

import Mathlib.Tactic

lemma intro_or_peel (α β γ δ : Prop) (h : γ → δ)
    (H : ∀ a : α, β → γ) : ∀ a : α, β → δ := by
  apply and_self_iff.mp _; constructor
  · intro a   -- ⊢ β → δ
    intro b   -- ⊢ δ
    apply h   -- ⊢ γ
    revert b  -- ⊢ β → γ
    revert a  -- ⊢ α → β → γ
    exact H   -- done
  . peel H with H a b -- ⊢ δ
    apply h           -- ⊢ γ
    exact H           -- done

lemma just_intro (α β γ δ : Prop) (h : γ → δ)
    (H : β → γ) : ∀ a : α, β → δ := by
  apply and_self_iff.mp _; constructor
  · intro a   -- ⊢ β → δ
    intro b   -- ⊢ δ
    apply h   -- ⊢ γ
    revert b  -- ⊢ β → γ
    exact H   -- done
  . peel H with H a b
    /- Tactic 'peel' could not match quantifiers in
      β → γ
    and
      α → β → δ -/

[Igor Khavkine]

Finally, I did manage to cobble together an intro tactic for an ∃ goal using Exists.imp. Here's an analogous example.

import Mathlib.Tactic

lemma exists_intro_or_peel (α β γ δ : Prop) (h : γ → δ)
    (H : ∃ a : α, β → γ) : ∃ a : α, β → δ := by
  apply and_self_iff.mp _; constructor
  · apply Exists.imp; intro a new_goal -- simulate `exists_intro a`
    -- a : α, new_goal : ?p a ⊢ β → δ
    intro b                -- ⊢ δ
    apply h                -- ⊢ γ
    revert b               -- ⊢ β → γ
    exact new_goal  -- simulate `exists_revert a`
    --                        ⊢ ∃ a : α, β → γ
    exact H                -- done
  · peel H with H a b
    --    a : α, b : β, H : γ ⊢ δ
    apply h                -- ⊢ γ
    exact H                -- done

lemma just_exists_intro (α β γ δ : Prop) (h : γ → δ)
    (x : α) (H : β → γ) : ∃ a : α, β → δ := by
  apply and_self_iff.mp _; constructor
  · apply Exists.imp; intro a new_goal -- simulate `exists_intro a`
    -- a : α, new_goal : ?p a ⊢ β → δ
    intro b                -- ⊢ δ
    apply h                -- ⊢ γ
    revert b               -- ⊢ β → γ
    exact new_goal  -- simulate `exists_revert a`
    --                        ⊢ ∃ a : α, β → γ
    refine' ⟨x, _⟩         -- ⊢ β → γ
    exact H                -- done (`exists x` is faster, but I wanted to show this step)
  · peel H with H a b
    /- Tactic 'peel' could not match quantifiers in
      β → γ
    and
      ∃ (_ : α), β → δ -/

More generally, one could invoke BEx.imp_right, Exists₂.imp, ...

[Igor Khavkine]

While the above solution is workable, it would be nice if it were encapsulated in a tactic. Maybe this can already be done in a standard way that I've missed? For example, one disadvantage of the above solution is that any modification to the proof context (have or let statements) inside the Exists.imp subgoal are thrown away when it is closed with exact new_goal. I suspect that a tactic could keep the modifications to the context that were independent of the intro-ed variables, like revert does.

[Kyle Miller]

Could you come up with a non-toy example?

Something I find worrisome is that exists_intro a is giving you a ?p a goal, which can be difficult to work with. At the moment, Lean's unification algorithm doesn't handle unifying against ?p a as well as it can.

[Igor Khavkine]

@Kyle Miller I've used this pattern successfully a few times in a long proof that I've been working on. It'd be rather involved extracting those specific cases into a MWE.

To describe it in words, the goal is something like ∃ x, P U x where P is some property relating x to a U that belongs to some filter (say of open neighborhoods in a topology, or of entourages in a uniformity), and you want to replace U by an element of a filter basis. Since the elements of a filter basis are typically much more structured, under the quantifier the goal can be simplified to some much more concrete formula say Q x. But since this changes the strength of the goal, ∃ x, P U x can't be turned into ∃ x, Q x using simp_rw, for instance. Also, you might not know exactly what Q xis until you apply some interactive simplifications, so building the ∀ x, Q x -> P U x hypothesis for Exists.imp by hand could be quite tedious.

I know you could also feed a metavariable into the goal (something like use ?y), but then I've had problems forcing an assignment of ?y later on.

[Patrick Massot]

It sounds like this is again a task for a port of the Coq procrastination tactic.

[Igor Khavkine]

What would that tactic do exactly? And is this something that's just on a wishlist, or there's a concrete plan to port it?

[Patrick Massot]

A very quick zulip search answers those questions, but let me answer anyway. The Coq tactic description is at https://armael.github.io/coq-procrastination/manual/manual.pdf. The concrete plan is that someone will end up being tired of seeing this tactic mentioned pretty often, or will simply really need it, and port it.

[Dan Velleman]

Your examples are a little strange. In particular, your quantifiers are vacuous. You write ∀ a : α or ∃ a : α followed by a proposition that doesn't mention a. I wonder if you have misunderstood quantifier notation in Lean.

I suspect that the tactics you are looking for are obtain and use, which are tactics you can use if you have either a hypothesis or a goal that starts with ∃. Here are much shorter proofs of your lemmas, where the last two use obtain and use:

import Mathlib.Tactic

lemma intro_or_peel (α β γ δ : Prop) (h : γ → δ)
    (H : ∀ a : α, β → γ) : ∀ a : α, β → δ := by
  intro a
  intro b
  exact h (H a b)

lemma just_intro (α β γ δ : Prop) (h : γ → δ)
    (H : β → γ) : ∀ a : α, β → δ := by
  intro a
  intro b
  exact h (H b)

lemma exists_intro_or_peel (α β γ δ : Prop) (h : γ → δ)
    (H : ∃ a : α, β → γ) : ∃ a : α, β → δ := by
  obtain ⟨a, H2⟩ := H
  use a
  intro b
  exact h (H2 b)

lemma just_exists_intro (α β γ δ : Prop) (h : γ → δ)
    (x : α) (H : β → γ) : ∃ a : α, β → δ := by
  use x
  intro b
  exact h (H b)

[Mario Carneiro]

By the way @Patrick Massot Coq-procrastination would need to be implemented in core, so if you actually want this to happen you should open an RFC.

[Patrick Massot]

Really? What is the missing piece?

[Patrick Massot]

The coq version certainly does not look like it required coq core changes.

[Mario Carneiro]

The concept of "shelved" goals does not exist in lean

[Mario Carneiro]

and you would need some code to check for those at the end of the block or something, when your tactic is not running

[Mario Carneiro]

basically this is a request to extend the definition of TacticM with additional state

[Patrick Massot]

Do you know what else uses this feature in Coq? Surely it hasn't been added for this tactic?

[Mario Carneiro]

You can already do a limited amount of procrastination using named metavariables, for example src#UnionFind.link uses this technique

[Mario Carneiro]

It has a whole tab for it in vscoq

[Mario Carneiro]

I don't know if it was added for this tactic, I would expect there are other tactics that interact with it too

[Mario Carneiro]

but coq and lean have slightly different tactic framework designs so this shouldn't be too surprising

[Igor Khavkine]

Patrick Massot said:

A very quick zulip search answers those questions, but let me answer anyway. The Coq tactic description is at https://armael.github.io/coq-procrastination/manual/manual.pdf. The concrete plan is that someone will end up being tired of seeing this tactic mentioned pretty often, or will simply really need it, and port it.

Thanks for kindly explaining. :-) As a newcomer, I had no context to go with your first remark.

[Igor Khavkine]

Dan Velleman said:

Your examples are a little strange. In particular, your quantifiers are vacuous. You write ∀ a : α or ∃ a : α followed by a proposition that doesn't mention a. I wonder if you have misunderstood quantifier notation in Lean.

I suspect that the tactics you are looking for are obtain and use, which are tactics you can use if you have either a hypothesis or a goal that starts with ∃. [...]

Thanks for the well-meaning effort. The emphasis in my toy examples is on "toy", where I just wanted to illustrate the interactive workflow that I had in mind. I guess you'll just have to trust me if I say that I'm not under some elementary misunderstanding. :-) The informal example in my reply to Kyle Miller is closer to "real world". Anyway, I think I'm describing standard practice in informal proofs of applying non reversible simplifications at every level of a goal with multiply nested quantifiers. For instance, if working through an analysis proof interactively, you might not know how to choose all the \epsilon's and \delta's until the end of the proof, but use doesn't easily allow you to delay that choice.

[Dan Velleman]

Yes, I see now that I misunderstood your question. Thanks for recognizing my effort as well-meaning:)