Email Gateway (Aug 18 2022 at 20:05): Email Gateway (Aug 18 2022 at 20:05):From: John Munroe <munddr@gmail.com>
Hi,
I'm having trouble proving the following, could someone please help?
axiomatization
T :: "real set" and
S :: "real set" where
ax1: "T = {1,2}" and
ax2: "S = {1,2,3}"
lemma "ALL t:T. EX s : S. even t <-> s*t=6"
I expect it to be true since only 2 in T is even.
Any help will be appreciated. Thanks.
John
Email Gateway (Aug 18 2022 at 20:05):From: Jasmin Blanchette <jasmin.blanchette@gmail.com>
Hi John,
The problem appears to be that the above formula does not type check without coercions (since "even" is not supported for "real"s) and that the implicit coercions are not necessarily those you want. (In fact, the example is rejected by the repository version of Isabelle, which appears to be more conservative here.)
You can solve the problem by adding an explicit conversion from "real" to "int", such as "floor" below:
lemma "ALL t:T. EX s : S. even (floor t) <-> s*t=6"
Then the proof is a piece of cake:
by (simp add: ax1 ax2)
Coercions are a recent addition to Isabelle (cf. Traytel, Berghofer, Nipkow APLAS 2011), and they can be very useful for some kinds of formalization, but their potential for confusing users remains largely unexplored. ;)
Cheers,
Jasmin
Email Gateway (Aug 18 2022 at 20:06):From: Makarius <makarius@sketis.net>
Axiomatizations are bad by default; better use a local context.
In Isabelle2012 (e.g. RC2) you can do it like this:
context
fixes T :: "real set"
and S :: "real set"
assumes ax1: "T = {1,2}"
and ax2: "S = {1,2,3}"
begin
lemma "ALL t:T. EX s : S. even t <-> s*t=6"
Incidently, this then reveals a more explicit type error than in
Isabelle2011-1, as Jasmin has already pointed out.
Makarius
Email Gateway (Aug 19 2022 at 08:45):From: John Munroe <munddr@gmail.com>
Hi,
Does anyone know why the following lemma is provable?
lemma "F = G --> (EX a b. a ~= b --> F a = G a & F b ~= G b)"
by auto
If F and G are equal, then F x = G x for all x. So how come the above
is provable?
Thanks a lot for your time.
John
Email Gateway (Aug 19 2022 at 08:45):From: Brian Huffman <huffman@in.tum.de>
Your lemma is provable even without the "F = G":
lemma "EX a b. a ~= b --> F a = G a & F b ~= G b"
by auto
The proof is by instantiating "a" and "b" with the same value. Then
you get "False --> something", which simplifies to True.
I think you may have meant to say this instead:
lemma "F = G --> (EX a b. a ~= b & F a = G a & F b ~= G b)"
which is indeed unprovable.
Email Gateway (Aug 19 2022 at 08:45):From: Viorel Preoteasa <viorel.preoteasa@abo.fi>
Hello,
If you rewrite it like:
lemma "F = G --> (EX a b. a = b or (F a = G a & F b ~= G b))"
you would see why it is true.
Viorel
Last updated: Apr 25 2024 at 16:19 UTC