Automatic intro/cases/specialize/use dance

Stream: Is there code for X?

[Kyle Miller]

Sometimes you have a goal and a hypothesis that share a prefix of quantifiers. As a contrived illustration,

example {α β} (p : β → Prop) (q : α → β → Prop) (h : ∀ x, ∃ y, p y ∧ q x y) : ∀ x, ∃ y, q x y :=
begin
  sorry
end

I was wondering if there was a tactic, invoked like auto_use h, that would automatically produce this sequence of tactics:

  intro x,
  specialize h x,
  cases h with y h,
  use y,

Perhaps it might even be able to apply cases on other inductive types when one of the cases can be used. For example, with a slight alteration to the above example (applying commutativity to the conjunction), it might produce the following proof:

example {α β} (p : β → Prop) (q : α → β → Prop) (h : ∀ x, ∃ y, q x y ∧ p y) : ∀ x, ∃ y, q x y :=
begin
  intro x,
  specialize h x,
  cases h with y h,
  use y,
  cases h with h' h,
  use h',
end

While it's true you can compress this proof, the point is to show the intended effect of the tactic.

That's a sort of imperative description of the wanted tactic, but put another way the idea would be to enter the "shared context" implied by a goal and a hypothesis.

(Tagging @Rahul Dalal because we discussed this at the Berkeley Lean Seminar.)

[Johan Commelin]

tidy is probably the closest to what you want...

[Johan Commelin]

But it's more general, and hence also more conservative.

[Kyle Miller]

I guess this question comes a place of wanting a tactic where you know what it will do and it's safe to use in the middle of a proof.

I was going to say that tidy certainly would deal with the second example, but I decided to check, and it actually makes a bit of a mess of the context. Maybe this is a bug in tidy?

2 goals
α : Sort ?,
β : Sort ?,
p : β → Prop,
q : α → β → Prop,
h : ∀ (x : α), ∃ (y : β), q x y ∧ p y,
x : α
⊢ β

α : Sort ?,
β : Sort ?,
p : β → Prop,
q : α → β → Prop,
h : ∀ (x : α), ∃ (y : β), q x y ∧ p y,
x : α
⊢ q x ?m_1

[Johan Commelin]

What does tidy? say?

[Johan Commelin]

I think tidy isn't really good at apply cases apart from some very specialised examples.

[Patrick Massot]

At least with the examples you gave, it will make a nice tactic writing exercise.

[Reid Barton]

I'm surprised we don't already have a lemma like

lemma forall_imp {α} (p q : α → Prop) (h : ∀ a, p a → q a) : (∀ a, p a) → (∀ a, q a) :=
by tidy

Then you can use this strategy:

example {α β} (p : β → Prop) (q : α → β → Prop) (h : ∀ x, ∃ y, p y ∧ q x y) : ∀ x, ∃ y, q x y :=
begin
  revert h,
  apply forall_imp, intro,
  apply exists_imp_exists, intro,
  -- ⊢ p a_1 ∧ q a a_1 → q a a_1
  tauto
end

[Kyle Miller]

@Patrick Massot Sounds good. I'll give it a try.

[Reid Barton]

Also I wonder whether it could be in scope for mono.

[Kyle Miller]

Johan Commelin said:

What does tidy? say?

It gives intros x, dsimp at *, fsplit

[David Wärn]

I was about to suggest forall_imp. Shocking that it does not exist...

[Kyle Miller]

@Reid Barton That's fair, but it was just a contrived example. I don't have any real examples on hand, but I've found myself doing this sort of dance in various contexts, and Rahul was saying he was doing it with even more deeply nested quantifiers. (However, in his case, it turned out to be something like simp_rw [forall_and_distrib], if I remember correctly.)

[Kyle Miller]

Should I add forall_imp to mathlib?

[Reid Barton]

If you want to prove iff rather than an implication the support is slightly better, but still not so great

[Reid Barton]

(for example, forall_congr actually exists!)

[Kyle Miller]

@Reid Barton Lean has the non-dependent version of forall_imp already: combinator.S. :grinning:

[Kyle Miller]

@Reid Barton Ok, created a pull request #3391

[Kyle Miller]

I didn't notice that the proof is laughing at the situation: λ h' a, h a (h' a).

[Kyle Miller]

Patrick Massot said:

At least with the examples you gave, it will make a nice tactic writing exercise.

That was kind of fun figuring out how to get this to work. I mostly looked carefully at the code for use, specialize, intro, and cases and combined them into a single enter tactic. An example application of the tactic is this tutorial exercise:

-- 0073
lemma seq_continuous_of_continuous (hf : continuous_at_pt f x₀)
  (hu : seq_limit u x₀) : seq_limit (f ∘ u) (f x₀) :=
begin
  enter hf with ε εpos,
  enter hf with δ δpos at hu,
  enter hu with N n nbig,
  specialize hf (u n) hu,
  exact hf,
end

What enter hf with ε εpos does is look at the quantifiers in hf and the goal and give them the names ε and εpos while doing the appropriate actions to eliminate the quantifiers. The enter hf with δ δpos at hu does something similar, but for two hypotheses hf and hu (this is a non-standard at where only a single hypothesis may be mentioned). The number of identifiers mentioned in the with clause determines how many quantifiers to eliminate.

The code follows:

import analysis.specific_limits

import tactic

namespace tactic

open tactic
open interactive
open interactive.types
open lean.parser

namespace interactive

meta def enter_aux_use (e : expr) : tactic unit :=
(focus1 $ tactic.exact e >> done) <|> (fconstructor >> enter_aux_use)

meta def enter_get_local (n : name) : tactic expr :=
get_local n <|> tactic.fail (format.join ["enter failed: no such local '", to_fmt n, "'"])

/-
The implementation of `enter` for a hypothesis and the goal.
-/
meta def enter_aux : name → parse with_ident_list → tactic unit
| nh [] := skip
| nh (i :: ids) := do
  h ← enter_get_local nh,
  let e_intro := (do
    v ← tactic.intro i,
    tactic.note nh none (h v),
    try $ tactic.clear h,
    return nh),
  let e_cases := (do
    [(name, [v, h''])] ← tactic.cases h [i, nh],
    enter_aux_use v,
    return h''.local_pp_name),
  h'' ← e_intro <|> e_cases <|> fail (format.join ["enter failed: could not use identifier '", to_fmt i, "'"]),
  enter_aux h'' ids

/-
The implementation of `enter` for two hypotheses.
-/
meta def enter_at_aux : name → name → parse with_ident_list → tactic unit
| nh nh' [] := skip
| nh nh' (i :: ids) := do
  let e_cases := λ nh nh', (do
    h ← enter_get_local nh,
    h' ← enter_get_local nh',
    [(name, [v, h''])] ← tactic.cases h [i, nh],
    tactic.note nh' none (h' v),
    try $ tactic.clear h',
    return (h''.local_pp_name, nh')),
  (nh, nh') ← e_cases nh nh' <|> e_cases nh' nh <|> fail (format.join ["enter failed: could not use identifier '", to_fmt i, "'"]),
  enter_at_aux nh nh' ids

/-
`enter h with a₁ a₂ .. aₙ` takes a prefix of n quantifiers shared
by `h` and the goal and, effectively, uses `intro`, `specialize`,
`cases`, and `use` to enter the shared context.  The supplied
identifiers determine how many quantifiers to enter.

`enter h` does `enter h with a`, choosing a fresh identifier `a` for
you.

`enter h (with a₁ a₂ .. aₙ)? at h'` performs a similar effect between
hypotheses `h` and `h'`, where h' is as if it is the `push_neg` of a
goal.  That is to say existential quantifiers of `h` or `h'` are used
to specialize a universal quantifier of the other.

A "quantifier" is any pi (Π, ∀, or →) or any single-constructor
inductive type with two arguments (∃, sigma, ∧, etc.).
-/
meta def enter (h : parse ident_) : parse with_ident_list → parse (optional $ tk "at" *> ident_) → tactic unit
| [] o := do x ← get_unused_name "a",
             enter [x] o
| ids none := propagate_tags $ enter_aux h ids
| ids (some h') := propagate_tags $ enter_at_aux h h' ids

end interactive

end tactic

example (h : ∃ y, y > 2) : ∃ y, y > 2 ∧ y > 1 :=
begin
  enter h with y,
  use h, linarith [h],
end

def lim_infinity (f : ℕ → ℕ) := ∀ m, ∃ N, ∀ n ≥ N, f n ≥ m

example (f : ℕ → ℕ) (h : lim_infinity f) : lim_infinity (λ n, f n * f n) :=
begin
  enter h with m N n h',
  dsimp only,
  have h' : m * m ≥ m := nat.le_mul_self _,
  calc f n * f n ≥ m * m : nat.mul_le_mul h h
       ... ≥ m : h',
end

section

local notation `|`x`|` := abs x

/-- Continuity of a function at a point  -/
def continuous_at_pt (f : ℝ → ℝ) (x₀ : ℝ) : Prop :=
∀ ε > 0, ∃ δ > 0, ∀ x, |x - x₀| ≤ δ → |f x - f x₀| ≤ ε

def seq_limit (u : ℕ → ℝ) (l : ℝ) : Prop :=
∀ ε > 0, ∃ N, ∀ n ≥ N, |u n - l| ≤ ε

variables {f : ℝ → ℝ} {x₀ : ℝ} {u : ℕ → ℝ}

-- 0073
lemma seq_continuous_of_continuous (hf : continuous_at_pt f x₀)
  (hu : seq_limit u x₀) : seq_limit (f ∘ u) (f x₀) :=
begin
  enter hf with ε εpos,
  enter hf with δ δpos at hu,
  enter hu with N n nbig,
  specialize hf (u n) hu,
  exact hf,
end

end

[Yakov Pechersky]

How about syntax like enter hf with δ δpos using hu?
Never mind, I see how hf is partially entered.
Then what about enter hf ... using hu?

[Kyle Miller]

Oh, so enter ID ID_LIST (using ID)?? That seems better.

[Yakov Pechersky]

enter hf with x y {with,using} hu assigns x, y gets quantifiers from hf and specializes at hu. Or you can phrase it like "using hf, specialize hu".

[Yakov Pechersky]

so either ... at ... or ... using ... could work, one would just have to be cognizant of what's used for what.

[Kyle Miller]

The way it's implemented is that it's symmetric in hf and hu, so it's a bit unfortunate that's not reflected in the tactic syntax.

[Yakov Pechersky]

Maybe that would allow for

enter hu with δ δpos N n nbig using [hf]

where it will enter as far as possible on existential, then use the available using hypotheses for the quantified, etc.

[Kyle Miller]

That's an interesting generalization. The only objection I'd have is that you might sometimes want to not consider the goal at all, but then for that you might use

enter hu with δ δpos N n nbig using only [hf]

[Yakov Pechersky]

Right, I was ignoring the goal entirely.

[Kyle Miller]

Oh, I thought you were saying "try entering the shared context with the goal, and whenever that fails try doing it with the first in the using list that would succeed"

[Yakov Pechersky]

I guess my assumption was ... using would ignore the goal by default, and goal could be included with notation for the goal

[Yakov Pechersky]

So either your option with only or explicit goal inclusion when the syntax is using [...]