Email Gateway (Aug 18 2022 at 09:48): Email Gateway (Aug 18 2022 at 09:48):From: Gabriele Pozzani <gabriele.pozzani@gmail.com>
Hello,
I have a formula involving the "mod" operator and so on nat type, but when I
eliminate the "mod" operator using the rule Divides.mod_eqD or
Divides.mod_eq_0D I want use the int type.
In particular I have:
(k - (j - Suc 0)) mod n = (0::nat)
eliminate the mod operator obtaining:
EXISTS q. (k - (j - Suc 0)) = n * q
but in natural if q is 0 then (k - (j - Suc 0)) --> k <= (j - Suc
0) not k = (j - Suc 0).
There is a way to change automatically the type of a formula from nat to int
so using the integer theorems?
I seen the int::nat => int but I must introduce it manually and if I use it
there are many unification errors with others formula.
Thanks
Gabriele Pozzani
Email Gateway (Aug 18 2022 at 09:48):From: Amine Chaieb <chaieb@informatik.tu-muenchen.de>
This is part of the arith tactic preprocessing and is due to Grosser
Meister. You can first rewrite with The following rules
nat_number_of_def
zdvd_int
int_int_eq[symmetric]
zle_int[symmetric]
zless_int[symmetric]
zadd_int[symmetric]
zmult_int[symmetric]
and the split rule zdiff_int_split
These turn "conventional" formulae over nat in to formulae where the "int"
is in front of all terms.
After this you can rewrite with the following theorems
nat_0_le
all_nat
ex_nat
number_of1
number_of2
int_0
int_1
and cong rules : conj_le_cong imp_le_cong
These "eliminate" the "int" in favour of "int (nat ..)" which can be
eliminated easily. Note that the "nat" variables have to be quantified!!!
Please include the appropriate rules to cover the predicates and functions
you use in the same scheme.
Amine.
Email Gateway (Aug 18 2022 at 09:49):From: Tjark Weber <tjark.weber@gmx.de>
Gabriele,
On Tuesday 24 October 2006 12:13, Gabriele Pozzani wrote:
I have a formula involving the "mod" operator and so on nat type, but when
I eliminate the "mod" operator using the rule Divides.mod_eqD or
Divides.mod_eq_0D I want use the int type.In particular I have:
(k - (j - Suc 0)) mod n = (0::nat)
eliminate the mod operator obtaining:
EXISTS q. (k - (j - Suc 0)) = n * q
but in natural if q is 0 then (k - (j - Suc 0)) --> k <= (j - Suc
0) not k = (j - Suc 0).
in fact anything that would allow you to deduce "k = j - Suc 0" from your
premise would be unsound, because "k <= j - Suc 0" is a sufficient condition
for "(k - (j - Suc 0)) mod n = (0::nat)".
If subtraction on type "nat" is not accurately modelling what you want to
formalize, then maybe using type "int" in your formulas in the first place
might solve your problem.
There is a way to change automatically the type of a formula from nat to
int so using the integer theorems?
No, because a theorem that holds for type "nat" may not hold for type "int",
and vice versa. (One particular example is "m <= n ==> m - n = 0".)
Best,
Tjark
Last updated: May 03 2024 at 04:19 UTC