Email Gateway (Aug 23 2022 at 09:13): Email Gateway (Aug 23 2022 at 09:13):From: Tobias Nipkow <nipkow@in.tum.de>
Dear Angeliki,
I don't know if transfer can help here, but it does not surprise me that the
proofs are harder for nat than for int as soon as "-" is involved because it
does not obey the same nice algebraic properties on nat as on int. See, for
example, add_diff_assoc.
Tobias
smime.p7s
Email Gateway (Aug 23 2022 at 09:13):From: "Dr A. Koutsoukou-Argyraki" <ak2110@cam.ac.uk>
Dear Tobias,
thank you for your answer.
Update: I found a different, slightly longer proof of A in my context
with (2::nat) .
I still need B with (2::nat), but also in general, it would be
very useful to be able to convert types somewhat automatically.
Any general tips wrt type conversion anyone?
Thanks in advance,
Angeliki
Email Gateway (Aug 23 2022 at 09:13):From: Mikhail Chekhov <mikhail.chekhov.w@gmail.com>
Dear Angeliki Koutsoukou-Argyraki/All,
This is merely a side remark for the question "Change the type from int to
nat -lifting/transfer?": I do not, necessarily, anticipate that it contains
any new information for the OP.
The theory HOL-ex.Transfer_Int_Nat provides an experimental infrastructure
for the transfer between the types 'int' and 'nat'. With small amendments
to the infrastructure, it is possible to perform the transfer of the goals
associated with the theorems A and B stated for nat to int (the other
direction is more difficult). For example,
theory Scratch
imports
"HOL-ex.Transfer_Int_Nat"
begin
lemma [transfer_rule]:
includes lifting_syntax
shows "(ZN ===> ZN ===> ZN) (λx y. x ^ nat y) (^)"
by (intro rel_funI) (simp add: ZN_def)
lemma B:
includes lifting_syntax
assumes "k>l" "l≥1"
shows
"(2::nat)^k
*(((2::nat)^(k-l)f)((2^k)*f)-((2^k)*f)-((2::nat)^(k-l)*f)+((2::nat)^(2k-l))f^2)
=
(2::nat)^k *(((2::nat)^(2k-l+1)(f^2))-((2^k)*f)-((2::nat)^(k-l)*f))"
using assms
apply transfer
oops
(*
0 ≤ l ⟹
0 ≤ k ⟹
l < k ⟹
1 ≤ l ⟹
0 ≤ f ⟹
2 ^ nat k * (tsub (tsub (2 ^ nat (tsub k l) * f * (2 ^ nat k * f))
(2 ^ nat k * f)) (2 ^ nat (tsub k l) * f) + 2 ^ nat (tsub (2 * k) l) * f ^
nat 2) =
2 ^ nat k * tsub (tsub (2 ^ nat (tsub (2 * k) l + 1) * f ^ nat 2) (2
^ nat k * f)) (2 ^ nat (tsub k l) * f)
*)
However, as you can see, transfer can hardly help to overcome the problem
related to the fact that minus behaves differently on nat and the subset of
natural numbers in the type int (as already communicated in the previous
reply:
https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2020-June/msg00009.html).
Therefore, even if the theorem that involves minus holds both on int and
nat, transferring the results will not be trivial. If, for some reason, it
is easier to prove a theorem on int with minus replaced by "tsub=max 0 (k -
l)", then, of course, it is sensible to use transfer. However, I doubt that
this will be the case very often. Nonetheless, this remark does not exhaust
all possibilities of how transfer can be used to attack the problem.
Perhaps, someone else will be able to provide a more creative approach to
the solution of this problem (I guess, ideally, one would wish to build the
infrastructure around transfer in a manner such that it provides additional
goals that indicate that all applications of binary minus remain
non-negative while preserving the original minus operation on the type int
in the primary goal after the application of transfer).
Kind Regards,
Mikhail Chekhov
Email Gateway (Aug 23 2022 at 09:13):From: "Dr A. Koutsoukou-Argyraki" <ak2110@cam.ac.uk>
Dear Mikhail Chekhov/ All,
Many thanks for your comments on transfer.
Indeed, it seems that the way "-" is defined for naturals makes transfer
not work here.
I have now solved my issues in the following way:
to prove various algebraic expressions involving something of the form
x-y where x, y are naturals, I first showed that x>y so that I could
stick to naturals instead of switching to integers.
After including all these proofs which happened to work in my context,
now everything works.
(perhaps this might be of help to someone else!)
Best wishes,
Angeliki
Email Gateway (Aug 23 2022 at 09:17):From: "Dr A. Koutsoukou-Argyraki" <ak2110@cam.ac.uk>
Hi,
Could someone please help with
lifting/transfer of types- there should be some way to do this
automatically?
In particular, I need a couple of simple algebraic equalities (A, B
below)
the proofs of which here (surprisingly) only work if the constant 2 is
defined
as type integer. How do I get these with the type changed to natural
(2::nat) ?
lemma A:
assumes "k>l" "l≥1"
shows " ( 2::int)^k *( (( 2::int)^(k-l) * f )*(( 2^k ) * f) -(( 2^k ) *
f)
-(( 2::int)^(k-l)* f -(1::int))
+(( 2::int)^(2*k -l) ) *f^2 -1 ) =
( 2::int)^k *
( (( 2::int)^(k-l) * f )*(( 2^k ) * f) -(( 2^k ) * f) -(( 2::int)^(k-l)
* f) +(1::int)
+(( 2::int)^(2*k -l) ) *f^2 -1 ) "
using assms
by (simp add: )
lemma B:
assumes "k>l" "l≥1"
shows "( 2::int)^k *( (( 2::int)^(k-l) * f )*(( 2^k ) * f) -(( 2^k ) *
f)
-(( 2::int)^(k-l) * f) +(( 2::int)^(2*k -l) ) *f^2 )
= ( 2::int)^k *( (( 2::int)^(2*k-l+1) *( f^2 )) -(( 2^k ) * f) -((
2::int)^(k-l) * f))"
using assms
apply (simp add: algebra_simps power2_eq_square )
by (metis Nat.add_diff_assoc Suc_1 less_imp_le_nat mult.right_neutral
mult_Suc_right power_add)
Thank you,
Best,
Angeliki
Last updated: Apr 26 2024 at 04:17 UTC