Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] simplifier failure in Isabelle2014

Email Gateway (Aug 19 2022 at 17:21):

From: Tobias Nipkow <nipkow@in.tum.de>
It looks like a proof in some simplification procedure failed unexpectedly,
probably "ring_eq_cancel_numeral_factor".

Here is a simpler goal with the same problem:

lemma "(pi * (real u * 2) = pi * (real (xa v) * - 2))"
apply simp

Proof failed.

1. (pi * (real u * 2) = pi * (real (xa v) * - 2)) = (pi * (real u * 2) = pi *
(2 * - real (xa v)))
The error(s) above occurred for the goal statement⌂:
(pi * (real u * 2) = - (pi * (real (xa v) * 2))) =
(2 * (Numeral1 * (pi * real u)) = 2 * (- 1 * (pi * real (xa v))))

Note that subterm "xa v". If I replace that with just a single variable, it
works and it turns out it is indeed "ring_eq_cancel_numeral_factor".

Summary: there is a problem in "ring_eq_cancel_numeral_factor". Possibly some
rewrite rules are missing somewhere.

Tobias
smime.p7s

Email Gateway (Aug 22 2022 at 09:02):

From: Larry Paulson <lp15@cam.ac.uk>
Consider the following theory snippet:

theory T imports
Complex_Main
begin

lemma cos_one_2pi:
"cos(x) = 1 ⟷ (∃n::nat. x = n * 2 * pi) | (∃n::nat. x = -(n * 2 * pi))"
sorry

lemma cos_one_2pi_int: "cos(x) = 1 ⟷ (∃n::int. x = n * 2 * pi)"
apply (auto simp add: cos_one_2pi)

Here “auto” fails with the attached output. Simplifier tracing reveals no obvious clues. The current development version exhibits the same behaviour.

Larry Paulson

Proof failed.

1. (pi * (real :000 * 2) = pi * (real (xa__ :000) * - 2)) =
   (pi * (real :000 * 2) = pi * (2 * - real (xa__ :000)))
   The error(s) above occurred for the goal statement⌂:
   (real xb * 2 * pi = - (real (xa__ xb) * 2 * pi)) =
   (2 * (Numeral1 * (pi * real xb)) = 2 * (- 1 * (pi * real (xa__ xb))))

Last updated: Apr 23 2024 at 20:15 UTC