beefing up `convert`

Stream: general

[Kevin Buzzard]

I might have asked this before but I can't find the thread; perhaps someone already told me why this can't happen. I can imagine a beefed-up convert which makes much more progress on the goals below.

import tactic
import data.real.basic

-- proof that aₙ → t implies -aₙ → -t
example {a : ℕ → ℝ} {t : ℝ}
  (ha : ∀ (ε : ℝ), 0 < ε → (∃ (B : ℕ), ∀ (n : ℕ), B ≤ n → |a n - t| < ε)) :
        ∀ (ε : ℝ), 0 < ε → (∃ (B : ℕ), ∀ (n : ℕ), B ≤ n → | -a n - -t| < ε) :=
begin
  convert ha, -- using 4 or whatever
  -- want: ∀ n, |a n - t| = | -a n - -t|
  -- but get
  -- ⊢ ∀ ε, ... = ∀ ε, ...
  sorry,
  --
end

-- workaround
example {a : ℕ → ℝ} {t : ℝ}
  (ha : ∀ (ε : ℝ), 0 < ε → (∃ (B : ℕ), ∀ (n : ℕ), B ≤ n → |a n - t| < ε)) :
        ∀ (ε : ℝ), 0 < ε → (∃ (B : ℕ), ∀ (n : ℕ), B ≤ n → | -a n - -t| < ε) :=
begin
  -- I want this to be the goal so I don't have to type it
  have : ∀ n : ℕ, |a n - t| = | -a n - -t|,
  { intro n,
    rw abs_sub_comm,
    congr' 1,
    ring },
  simpa [this] using ha,
end

-- minimised convert "failure"
example (P Q R : Prop) (h : P → Q) : P → R :=
begin
  convert h,
  -- ⊢ (P → R) = (P → Q)
  -- Why not `R = Q` or `R ↔ Q`?
  sorry,
end

example (f : ℕ → ℝ) (a b : ℝ) (h : ∀ n, f n = a) : ∀ n, f n = b :=
begin
  convert h, -- expecting `b = a`
  -- ⊢ (∀ (n : ℕ), f n = b) = ∀ (n : ℕ), f n = a
  sorry
end

[Reid Barton]

So the first-order explanation is that congr checks for a function application, and a Pi/forall/function type (P → R) is not a function application

[Reid Barton]

But, I don't see why congr couldn't also try applying a suitable version of docs#forall_congr (followed by intro) and then continuing

[Kyle Miller]

This reminds me of a tactic I wrote as an exercise that does sort of what you want here. https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there.20code.20for.20X.3F/topic/Automatic.20intro.2Fcases.2Fspecialize.2Fuse.20dance/near/203997071

[Kyle Miller]

example {a : ℕ → ℝ} {t : ℝ}
  (ha : ∀ (ε : ℝ), 0 < ε → (∃ (B : ℕ), ∀ (n : ℕ), B ≤ n → |a n - t| < ε)) :
        ∀ (ε : ℝ), 0 < ε → (∃ (B : ℕ), ∀ (n : ℕ), B ≤ n → | -a n - -t| < ε) :=
begin
  enter ha with ε εpos B n hB,
  /-
a : ℕ → ℝ,
t ε : ℝ,
εpos : 0 < ε,
B n : ℕ,
hB : B ≤ n,
ha : |a n - t| < ε
⊢ | -a n - -t| < ε
  -/
  sorry
end

example (P Q R : Prop) (h : P → Q) : P → R :=
begin
  enter h with hP,
  /-
P Q R : Prop,
hP : P,
h : Q
⊢ R
  -/
  sorry,
end

example (f : ℕ → ℝ) (a b : ℝ) (h : ∀ n, f n = a) : ∀ n, f n = b :=
begin
  enter h with n,
  /-
f : ℕ → ℝ,
a b : ℝ,
n : ℕ,
h : f n = a
⊢ f n = b
  -/
  sorry
end

[Kyle Miller]

Code

import analysis.specific_limits
import data.real.basic

import tactic

namespace tactic

setup_tactic_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

-- proof that aₙ → t implies -aₙ → -t
example {a : ℕ → ℝ} {t : ℝ}
  (ha : ∀ (ε : ℝ), 0 < ε → (∃ (B : ℕ), ∀ (n : ℕ), B ≤ n → |a n - t| < ε)) :
        ∀ (ε : ℝ), 0 < ε → (∃ (B : ℕ), ∀ (n : ℕ), B ≤ n → | -a n - -t| < ε) :=
begin
  enter ha with ε εpos B n hB,
  /-
a : ℕ → ℝ,
t ε : ℝ,
εpos : 0 < ε,
B n : ℕ,
hB : B ≤ n,
ha : |a n - t| < ε
⊢ | -a n - -t| < ε
  -/
  sorry
end

-- minimised convert "failure"
example (P Q R : Prop) (h : P → Q) : P → R :=
begin
  enter h with hP,
  /-
P Q R : Prop,
hP : P,
h : Q
⊢ R
  -/
  sorry,
end

example (f : ℕ → ℝ) (a b : ℝ) (h : ∀ n, f n = a) : ∀ n, f n = b :=
begin
  enter h with n,
  /-
f : ℕ → ℝ,
a b : ℝ,
n : ℕ,
h : f n = a
⊢ f n = b
  -/
  sorry
end

[Kyle Miller]

Reid Barton said:

But, I don't see why congr couldn't also try applying a suitable version of docs#forall_congr (followed by intro) and then continuing

Maybe convert/congr could get a with clause so you can name those variables being introduced?

[Eric Wieser]

congr' already has such a clause