Email Gateway (Aug 18 2022 at 12:36): Email Gateway (Aug 18 2022 at 12:36):From: Duraid Madina <duraid@kinoko.c.u-tokyo.ac.jp>
The following lemma:
theory bug imports Main GCD
begin
lemma test:
"gcd (Suc (Suc 0), Suc (Suc (Suc (Suc 0)))) *
((Suc (Suc 0) div gcd (Suc (Suc 0), Suc (Suc (Suc (Suc 0)))) +
2 * ((3 + Suc (Suc 0) div gcd (Suc (Suc 0), Suc (Suc (Suc (Suc 0)))) -
Suc (Suc (Suc (Suc 0))) div gcd (Suc (Suc 0), Suc (Suc (Suc (Suc
0))))) mod
3)) mod
6) ~=
4
==> gcd (Suc (Suc 0), Suc (Suc (Suc (Suc 0)))) *
((Suc (Suc 0) div gcd (Suc (Suc 0), Suc (Suc (Suc (Suc 0)))) +
2 * ((3 + Suc (Suc 0) div gcd (Suc (Suc 0), Suc (Suc (Suc (Suc
0)))) -
Suc (Suc (Suc (Suc 0))) div gcd (Suc (Suc 0), Suc (Suc (Suc
(Suc 0))))) mod
3)) mod
6) =
10"
is "True => True" in that if I try to apply 'value' to each side of the
==>, Isabelle immediately returns True in both cases, but I cannot figure
out how to prove the above lemma.
What sort of tactic should I be using in this case? Or is there some
bug here? Perhaps the fact that apply(eval) reports:
*** exception TERM raised: dest_Trueprop
will be helpful to someone, but I can't say I fully understand it. I am not
sure why, for example,
lemma doh:
"1+1=(3::nat) --> 1+1=(4::nat)"
apply(eval)
done
works, but
lemma doh:
"1+1=(3::nat) ==> 1+1=(4::nat)"
apply(eval)
done
fails. Is this exception the intended behaviour for the latter case? Note
that using 'auto' rather than 'eval' will prove both versions of lemma
"doh", but auto will _not_ prove lemma "test", above.
Puzzled,
Duraid
Email Gateway (Aug 18 2022 at 12:36):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Duraid,
the issue is that "eval" is a very special method which compiles the
goal to prove into an ML term of type and then evaluates it, proving the
goal if the result is true. This does not work with statements
involving meta-connectives like ==> (though I perfectly agree that the
error message could be more explicit).
Usually, such closed expressions would be proven using method "simp".
Alas, for gcd there are no suitable default lemmas for "simp", making a
proof involving "simp" a little bit tedious (use find_theorems to search
for suitable simplification rules).
In your particular case, what would work is to simply leave out the
hypothesis since the conclusion alone is sufficient to prove (using "eval").
Hope this helps,
Florian
P.S. Note that you can also use numeral syntax for natural numbers.
signature.asc
Email Gateway (Aug 18 2022 at 12:36):From: Tjark Weber <webertj@in.tum.de>
I don't know if the above is the intended behavior, but in any case you
can replace the meta implication ==> by a HOL implication --> using
apply (erule rev_mp)
More generally, you can replace meta connectives by HOL connectives
using
apply (atomize (full))
(See page 107 of the Isabelle/Isar Reference Manual for details.)
Best,
Tjark
Email Gateway (Aug 18 2022 at 12:36):From: Duraid Madina <duraid@kinoko.c.u-tokyo.ac.jp>
Thanks - this in conjuction with eval did the trick!
Duraid
Email Gateway (Aug 18 2022 at 12:36):From: Duraid Madina <duraid@kinoko.c.u-tokyo.ac.jp>
Hi Florian,
On Mon, Nov 10, 2008 at 02:22:38PM +0100, Florian Haftmann wrote:
Usually, such closed expressions would be proven using method "simp".
Alas, for gcd there are no suitable default lemmas for "simp", making a
proof involving "simp" a little bit tedious (use find_theorems to search
for suitable simplification rules).
I see. I hadn't really bothered to look inside GCD properly, but I will now.
In your particular case, what would work is to simply leave out the
hypothesis since the conclusion alone is sufficient to prove (using "eval").
Actually, this lemma was just cut+pasted from a goal in a larger
development...
P.S. Note that you can also use numeral syntax for natural numbers.
.. and I was about to say I had no idea where the 'Suc's came from, but now
I realise they just came through an import.
Thanks,
Duraid
Last updated: May 03 2024 at 04:19 UTC