Zulip Chat Archive

Stream: Is there code for X?

Topic: Automatic intro/cases/specialize/use dance


view this post on Zulip 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.)

view this post on Zulip Johan Commelin (Jul 13 2020 at 20:36):

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

view this post on Zulip Johan Commelin (Jul 13 2020 at 20:36):

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

view this post on Zulip 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

view this post on Zulip Johan Commelin (Jul 13 2020 at 20:41):

What does tidy? say?

view this post on Zulip Johan Commelin (Jul 13 2020 at 20:42):

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

view this post on Zulip Patrick Massot (Jul 13 2020 at 20:43):

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

view this post on Zulip 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

view this post on Zulip Kyle Miller (Jul 13 2020 at 20:48):

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

view this post on Zulip Reid Barton (Jul 13 2020 at 20:48):

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

view this post on Zulip Kyle Miller (Jul 13 2020 at 20:49):

Johan Commelin said:

What does tidy? say?

It gives intros x, dsimp at *, fsplit

view this post on Zulip David Wärn (Jul 13 2020 at 20:52):

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

view this post on Zulip 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.)

view this post on Zulip Kyle Miller (Jul 13 2020 at 20:56):

Should I add forall_imp to mathlib?

view this post on Zulip 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

view this post on Zulip Reid Barton (Jul 13 2020 at 21:03):

(for example, forall_congr actually exists!)

view this post on Zulip Kyle Miller (Jul 13 2020 at 21:18):

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

view this post on Zulip Kyle Miller (Jul 13 2020 at 21:23):

@Reid Barton Ok, created a pull request #3391

view this post on Zulip 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).

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip Kyle Miller (Jul 15 2020 at 19:12):

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

view this post on Zulip 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".

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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]

view this post on Zulip Yakov Pechersky (Jul 15 2020 at 19:22):

Right, I was ignoring the goal entirely.

view this post on Zulip 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"

view this post on Zulip 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

view this post on Zulip 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