## Stream: Is there code for X?

### Topic: Automatic intro/cases/specialize/use dance

#### Kyle Miller (Jul 13 2020 at 20:35):

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 (Jul 13 2020 at 20:36):

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

#### Johan Commelin (Jul 13 2020 at 20:36):

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

#### Kyle Miller (Jul 13 2020 at 20:39):

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 (Jul 13 2020 at 20:41):

What does tidy? say?

#### Johan Commelin (Jul 13 2020 at 20:42):

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

#### Patrick Massot (Jul 13 2020 at 20:43):

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

#### Reid Barton (Jul 13 2020 at 20:48):

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 (Jul 13 2020 at 20:48):

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

#### Reid Barton (Jul 13 2020 at 20:48):

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

#### Kyle Miller (Jul 13 2020 at 20:49):

Johan Commelin said:

What does tidy? say?

It gives intros x, dsimp at *, fsplit

#### David Wärn (Jul 13 2020 at 20:52):

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

#### Kyle Miller (Jul 13 2020 at 20:55):

@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 (Jul 13 2020 at 20:56):

Should I add forall_imp to mathlib?

#### Reid Barton (Jul 13 2020 at 20:56):

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

#### Reid Barton (Jul 13 2020 at 21:03):

(for example, forall_congr actually exists!)

#### Kyle Miller (Jul 13 2020 at 21:18):

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

#### Kyle Miller (Jul 13 2020 at 21:23):

@Reid Barton Ok, created a pull request #3391

#### Kyle Miller (Jul 13 2020 at 21:24):

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

#### Kyle Miller (Jul 15 2020 at 18:52):

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 (Jul 15 2020 at 19:09):

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 (Jul 15 2020 at 19:12):

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

#### Yakov Pechersky (Jul 15 2020 at 19:13):

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 (Jul 15 2020 at 19:14):

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

#### Kyle Miller (Jul 15 2020 at 19:16):

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 (Jul 15 2020 at 19:16):

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 (Jul 15 2020 at 19:21):

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 (Jul 15 2020 at 19:22):

Right, I was ignoring the goal entirely.

#### Kyle Miller (Jul 15 2020 at 19:23):

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 (Jul 15 2020 at 19:25):

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

#### Yakov Pechersky (Jul 15 2020 at 19:25):

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

Last updated: May 07 2021 at 17:36 UTC