Zulip Chat Archive

Stream: general

Topic: tauto?

Sebastien Gouezel (Oct 19 2018 at 20:13):

Suppose I have an assumption

h : ∀ (ε : ℝ), ε > 0 → (∃ (N : ℕ), ∀ (n : ℕ), n ≥ N → ∀ (y : α), dist (F n y) (f y) ≤ ε)

and a goal

∀ (ε : ℝ), ε > 0 → (∃ (N : ℕ), ∀ (n : ℕ), n ≥ N → ∀ (y : α), y ∈ ball x 1 → dist (F n y) (f y) ≤ ε)

The goal is a trivial consequence of h (there are more assumptions in the goal than in h). I can prove it by hand doing the intros/rcases dance, but I did not find a tactic that would do it out of the box. Did I miss something?

Reid Barton (Oct 19 2018 at 20:19):

tidy can do these sometimes

Reid Barton (Oct 19 2018 at 20:20):

Also, there's rintros now :smile:

Sebastien Gouezel (Oct 19 2018 at 20:27):

Poor tidy is completely lost when there are real numbers: it unfolds the Cauchy sequences definition, and asks for new goals looking like

dist (F n y) (f y) ≤ quot.mk setoid.r ⟨ε_val, ε_property⟩

Kenny Lau (Oct 19 2018 at 20:27):

I don't see why one can't just prove it by hand. It isn't like it's very complicated

Kenny Lau (Oct 19 2018 at 20:27):

but yes, I agree there should be a tactic that doesn't only take iff things as argument

Patrick Massot (Oct 19 2018 at 20:28):

Because proving things by hand don't scale

Patrick Massot (Oct 19 2018 at 20:28):

We want thousands of those trivial proofs

Sebastien Gouezel (Oct 19 2018 at 20:32):

Isabelle proof: using h by blast :)

Patrick Massot (Oct 19 2018 at 20:33):

That still two words of noise, but it's getting close to acceptable

Patrick Massot (Oct 19 2018 at 20:34):

(deleted)

Chris Hughes (Oct 19 2018 at 20:36):

(deleted)

Last updated: Dec 20 2023 at 11:08 UTC