Email Gateway (Aug 19 2022 at 15:39): Email Gateway (Aug 19 2022 at 15:39):From: "W. Douglas Maurer" <maurer@gwu.edu>
I would appreciate some kind of strategy to determine what to write
after simp add: when proving a simple fact. This first came up for me
when I was trying to prove "floor (9.5::real) = (9::int)" and
"ceiling (9.5::real) = (10::int)". Here try0 was no help; it tried
simp, auto, fast, fastforce, force, blast, metis, linarith, and
presburger, and then reported no proof found. Quite by accident, I
found out how to do these; you type simp add: floor_unique or simp
add: ceiling_unique . I'd like to know how to find rules like
floor_unique and ceiling_unique in other cases. The one I'm concerned
about now is "(2::nat)*x ~= 3", which arose for me as an unproved
subgoal. Yes, I know I can prove this one by presburger, because try0
told me so, but that seems like using an elephant to crush a flea;
presburger took forever to find a proof. I've also tried
find_theorems, but that said it found over 18,000 theorems and none
of the first few looked promising. I'm sure there's a much simpler
way of proving that "(2::nat)*x ~= 3", and I'm sure that many people
on the mailing list know what it is, but what I'd really appreciate
is some hints on how to find something like this. -Douglas
Email Gateway (Aug 19 2022 at 15:39):From: Tobias Nipkow <nipkow@in.tum.de>
On 29/08/2014 05:22, W. Douglas Maurer wrote:
I would appreciate some kind of strategy to determine what to write after simp
add: when proving a simple fact. This first came up for me when I was trying to
prove "floor (9.5::real) = (9::int)" and "ceiling (9.5::real) = (10::int)".
For a start, simp should prove this, but unfortunately it does not. We will have
to add the right lemmas to automate this, thanks.
Here
try0 was no help; it tried simp, auto, fast, fastforce, force, blast, metis,
linarith, and presburger, and then reported no proof found. Quite by accident, I
found out how to do these; you type simp add: floor_unique or simp add:
ceiling_unique . I'd like to know how to find rules like floor_unique and
ceiling_unique in other cases.
The search button (Find' or Query'). In this case it is not so clear what to
search for. Certainly "floor", but that still gives you 75 lemmas, which you
would have to go through and see if they might be helpful.
The one I'm concerned about now is "(2::nat)*x ~=
3", which arose for me as an unproved subgoal. Yes, I know I can prove this one
by presburger, because try0 told me so, but that seems like using an elephant to
crush a flea; presburger took forever to find a proof.
Not for me: presburger is instantaneous, as is arith (which tries linear
arithmetic first and only then presburger).
I've also tried
find_theorems, but that said it found over 18,000 theorems and none of the first
few looked promising. I'm sure there's a much simpler way of proving that
"(2::nat)*x ~= 3", and I'm sure that many people on the mailing list know what
it is, but what I'd really appreciate is some hints on how to find something
like this. -Douglas
The 18,000 suggests you just typed find_theorems. Use the search facility
(Find' or Query') with appropriate selection criteria.
Tobias
Email Gateway (Aug 19 2022 at 15:39):From: Lars Noschinski <noschinl@in.tum.de>
On 29.08.2014 05:22, W. Douglas Maurer wrote:
I would appreciate some kind of strategy to determine what to write
after simp add: when proving a simple fact. This first came up for me
when I was trying to prove "floor (9.5::real) = (9::int)" and "ceiling
(9.5::real) = (10::int)". Here try0 was no help; it tried simp, auto,
fast, fastforce, force, blast, metis, linarith, and presburger, and
then reported no proof found. Quite by accident, I found out how to do
these; you type simp add: floor_unique or simp add: ceiling_unique .
I'd like to know how to find rules like floor_unique and
ceiling_unique in other cases.
In this case, my approach would have been to use find_theorems to look
for "floor _ = _". If the property could also be computed (there are no
variables in this goal), you can also try code_simp/normalization/eval
-- these methods use a different setup of rewrite rules aimed at
generation of executable code instead of proving.
The one I'm concerned about now is "(2::nat)*x ~= 3", which arose for
me as an unproved subgoal. Yes, I know I can prove this one by
presburger, because try0 told me so, but that seems like using an
elephant to crush a flea; presburger took forever to find a proof.
It shouldn't take long -- on my machine, presburger is almost
instantaneous on this goal (additional premises may slow it down, though).
I've also tried find_theorems, but that said it found over 18,000
theorems and none of the first few looked promising. I'm sure there's
a much simpler way of proving that "(2::nat)*x ~= 3", and I'm sure
that many people on the mailing list know what it is, but what I'd
really appreciate is some hints on how to find something like this.
find_theorems is often the right approach. However, if you need to give
it a query, otherwise it lists all theorems (which is not going to be
useful). The simples queries consist of a number of term patterns (like
"_ * _"); another very useful query is "intro" which lists all
applicable introduction rules. The reference manual has a full list of
options.
Another way to discover lemmas is using sledgehammer and inspecting the
proofs (especially if you give it the isar_proofs option). For me, it
gives the proof
by (metis Suc_numeral even_mult_two_ex monoid_mult_class.mult.right_neutral
odd_Suc_mult_two_ex semiring_norm(5))
The interesting lemmas here are even_mult_two_ex and
odd_Suc_mult_two_ex. However, due to the existential, they are not
well-suited for simp and auto.
The goal "2*x ~= 3" is a bit tricky for automated tools: The reasoning
is that 2*x is even and 3 is odd. However, neither "even" nor "odd" is
mentioned in the goal. A rule like "even x ==> odd y ==> x ~= y" could
introduce these constants. However, looking at the theorems for "even"
and "odd" [1], none of the existing theorems suggests itself.
We can easily prove it ourselves, though:
lemma even_odd_neq_nat: "⋀x y :: nat. even x ⟹ odd y ⟹ x ≠ y" by auto
Giving this lemma to simp easily solves the goal.
-- Lars
[1] There is some oddity in find_theorems. Searching for "odd" will not
yield any lemmas, you will need to write "odd _". This is somehow
related to odd being an abbreviation for "~ even" and possibly warrants
some closer investigation from the developers.
Email Gateway (Aug 19 2022 at 15:40):From: Johannes Hölzl <hoelzl@in.tum.de>
These rules are now in the Isabelle repository:
http://isabelle.in.tum.de/repos/isabelle/rev/cfd3cff9387b
Email Gateway (Aug 19 2022 at 16:00):From: "W. Douglas Maurer" <maurer@gwu.edu>
In response to my submission, Lars Noschinski wrote: 'The goal "2*x
~= 3" is a bit tricky for automated tools: The reasoning is that 2*x
is even and 3 is odd. However, neither "even" nor "odd" is mentioned
in the goal.' But a proof that "2*x ~= 3" by reference to even and
odd doesn't generalize in even simple ways, such as "3*x ~= 5".
The real solution, it would appear to me, is that ax=b (for the free
variable x, and constant natural numbers a and b) should simplify to
b mod a = 0. Since a and b are constants, this should be easy to
check. Similarly, ax ~= b should simplify to b mod a ~= 0. For "2*x
~= 3", this would simplify to 3 mod 2 ~= 0, or 1 ~= 0. -Douglas
Last updated: Apr 23 2024 at 20:15 UTC