Zulip Chat Archive

Stream: general

Topic: tauto?


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

view this post on Zulip Reid Barton (Oct 19 2018 at 20:19):

tidy can do these sometimes

view this post on Zulip Reid Barton (Oct 19 2018 at 20:20):

Also, there's rintros now :smile:

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

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

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

view this post on Zulip Patrick Massot (Oct 19 2018 at 20:28):

Because proving things by hand don't scale

view this post on Zulip Patrick Massot (Oct 19 2018 at 20:28):

We want thousands of those trivial proofs

view this post on Zulip Sebastien Gouezel (Oct 19 2018 at 20:32):

Isabelle proof: using h by blast :)

view this post on Zulip Patrick Massot (Oct 19 2018 at 20:33):

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

view this post on Zulip Patrick Massot (Oct 19 2018 at 20:34):

(deleted)

view this post on Zulip Chris Hughes (Oct 19 2018 at 20:36):

(deleted)


Last updated: May 14 2021 at 14:20 UTC