Email Gateway (Aug 18 2022 at 12:47): Email Gateway (Aug 18 2022 at 12:47):From: TIMOTHY KREMANN <twksoa262@verizon.net>
I am trying to prove:
lemma nataba: "\<forall> a b. (b::nat) < a --> a * a - (2 * b * a - b * b) =
a * a - 2 * a * b + b * b"
But Isabelle returns this text when I enter the above:
proof (prove): step 0
goal (1 subgoal):
Counterexample found:
a = Suc (Suc (Suc 0))
b = Suc (Suc 0)
Can someone explain to me how 1 = 1 is a counterexample?
Thanks,
Tim
Email Gateway (Aug 18 2022 at 12:47):From: TIMOTHY KREMANN <twksoa262@verizon.net>
Sorry, the 2 had type 'a.
Tim
Email Gateway (Aug 18 2022 at 12:48):From: Brian Huffman <brianh@cs.pdx.edu>
Hi Tim,
Your confusion is probably caused by a misunderstanding about how
subtraction is defined on type nat. If you subtract a larger number
from a smaller, the result is defined to be zero. For example, at type
nat, 3 - 5 = 0.
In your example, with a = 3 and b = 2, the left hand side evaluates to
a * a - (2 * b * a - b * b) = 3 * 3 - (2 * 2 * 3 - 2 * 2) = 9 - (12 -
4) = 9 - 8 = 1
while the right hand side evaluates to
(a * a - 2 * a * b) + b * b = (3 * 3 - 2 * 3 * 2) + 2 * 2 = (9 - 12) +
4 = 0 + 4 = 4
So this is indeed a counterexample.
You might be able to prove your lemma if you add more side conditions
to ensure that a * a is always greater than or equal to 2 * a * b, so
the subtraction won't underflow to zero. I think that a <= 2 * b would
probably work.
Hope this helps,
Quoting TIMOTHY KREMANN <twksoa262@verizon.net>:
Last updated: May 03 2024 at 08:18 UTC