Email Gateway (Aug 19 2022 at 16:14): Email Gateway (Aug 19 2022 at 16:14):From: Scott Constable <sdconsta@syr.edu>
I am working on a proof which I was able to reduce to “of_int i = 0 ==> i = 0”. This seemed like a simple application of the rule “of_int_eq_0_iff” however I was unable to successfully apply this rule.
On further probing I found that I was unable to prove the following lemma
lemma of_int_eq_0_imp1: “of_int i = 0 ==> i = 0”
by any means whatsoever. That is, unless I declare the lemma within the context ring_char_0. Then the lemma can easily be proved as follows:
context ring_char_0 begin
lemma of_int_eq_0_imp1: “of_int i = 0 ==> i = 0”
using of_int_eq_iff [of i 0] by simp
end
But then I cannot apply this lemma outside of this context, which is what my main theorem requires (it resides within a different context).
Any help would be greatly appreciated.
Email Gateway (Aug 19 2022 at 16:24):From: Peter Lammich <lammich@in.tum.de>
Hi,
try
note [[ show_sorts]]
thm of_int_eq_0_iff
here, you will see that the of_int_eq_0_iff lemma only works
if the right hand side is in the ring_char_0 typeclass.
So make sure that your 0 on the RHS also is in this typeclass.
Email Gateway (Aug 19 2022 at 16:33):From: Scott Constable <sdconsta@syr.edu>
Thanks everyone! I think the error was actually easier to see with
declare [[show_types]]
as I was working with 32 words. Clearly it is not the case that
of_int x = (0 :: 32 word) ==> x = 0
Email Gateway (Aug 19 2022 at 16:33):From: Lars Noschinski <noschinl@in.tum.de>
The same can also be seen without show_sorts by hovering over the
variables in the lemma.
-- Lars
signature.asc
Last updated: Apr 26 2024 at 08:19 UTC