Email Gateway (Aug 18 2022 at 09:58): Email Gateway (Aug 18 2022 at 09:58):From: Brian Huffman <brianh@csee.ogi.edu>
The following theorems may be of some use:
IntDiv.zmod_zadd_left_eq
IntDiv.zmod_zadd_right_eq
IntDiv.zmod_zmult1_eq
IntDiv.zmod_zmult1_eq'
IntDiv.zpower_zmod
In particular, you can use them to prove congruence rules for modular
arithmetic, such as:
[| x mod p = x' mod p; y mod p = y' mod p |]
==> (x + y) mod p = (x' + y') mod p
and similarly for subtraction, multiplication and exponentiation. I'm not sure
if this will give you everything you want, but at least this should allow you
to remove the inner mod operations from your subgoals.
Email Gateway (Aug 18 2022 at 10:02):From: kuecuek@rbg.informatik.tu-darmstadt.de
hallo,
i try to solve an equation but it is realy complex can anybody help me?
if i try with numbers then i can show it with "auto" but if i use variables
then i can not proof it.
the equations below are given
y1 ^2 = x1 ^3 + a*x1 + b
y2 ^2 = x2 ^ 3 + a*x2 + b
and
x3 = ((((y1 - y2) * ((x1 - x2) ^ nat (p -2 ))) mod p) ^ 2 - x1 - x2) mod p
y3 = ((((y1 - y2) * ((x1 - x2) ^ nat (p -2 ))) mod p) * (x1 - x3) - y1) mod p
and i must to show that y3^2 = x3^3 + a*x3 + b
if you put the definitionof y3 and x3 in last equation you would see how
complex it is :(
can anybody give a trick to proof something like that?
thanks a lot
Email Gateway (Aug 18 2022 at 10:02):From: Tobias Nipkow <nipkow@in.tum.de>
I am afraid there is no automation for reasoning involving "mod p" where
p is not a numeral.
Tobias
kuecuek@rbg.informatik.tu-darmstadt.de wrote:
Email Gateway (Aug 18 2022 at 12:08):From: Lawrence Paulson <lp15@cam.ac.uk>
The correct way to formalise your system is by expressing the axiom in
the form
[| B x False; S x |] ==> False
in the first place. Then it looks like you would have nothing to do.
As I mentioned earlier, we do not attempt to create complex formulas
in the assumptions. In a formal sequent calculus this is simply
impossible: the available rules only allow formulas to be broken down,
not built up. (When used to construct a backward proof of course.)
Larry Paulson
Email Gateway (Aug 18 2022 at 12:08):From: Jeremy Dawson <jeremy@rsise.anu.edu.au>
Erich Kummerfeld wrote:
You can do this (but getting an extra assumption) as follows
Level 0 (1 subgoal)
[| B x False; S x |] ==> False
[| B x False; S x |] ==> False
val it = [] : Thm.thm list
by (datac conjI 1 1) ;
Level 1 (1 subgoal)
[| B x False; S x |] ==> False
[| S x; B x False & S x |] ==> False
(or, if you like, the Isar equivalent, which I assume is
apply (drule_tac conjI) ;
apply assumption ;
Jeremy
Email Gateway (Aug 18 2022 at 12:09):From: Erich Kummerfeld <ekummerfeld@gmail.com>
Hi,
I'm fairly new to Isabelle and sequent calculus in general and am having a
couple difficulties. The first regards applying the conjI rule to a
hypothesis. When I apply (drule conjI) to [| y; x|] ==> x & y I expect to
get x & y ==> x & y, but instead get 1. y ==> ?Q 2. [| y; x & ?Q |] ==> x &
y. Being able to deduct forwards from a hypothesis of form [| x; y |] to
get a new hypothesis of form x & y is my goal here.
The second problem I'm having is with the defining and use of axioms. This
is the code I'm using:
consts
S :: "'a => bool"
B :: "'a => bool => bool"
axioms
sb: "((B x y) & (S x) ==> y"
I'm not certain how I am defining or using these wrong, but when I try to
use it in a theorem it does not do what I expect it to.
theorem "((B x z) & (S x) ==> z"
apply (simp add: sb)
yields the empty result sequence error rather than the "no subgoals!" that I
would expect.
Thanks in advance for the help, I've been hammering at these problems all
day and have been able to boil them down to these simple cases but have no
idea why they are failing.
-Erich Kummerfeld
Email Gateway (Aug 18 2022 at 12:12):From: Brian Huffman <brianh@cs.pdx.edu>
Quoting Erich Kummerfeld <ekummerfeld@gmail.com>:
Hi,
I'm fairly new to Isabelle and sequent calculus in general and am having a
couple difficulties. The first regards applying the conjI rule to a
hypothesis. When I apply (drule conjI) to [| y; x|] ==> x & y I expect to
get x & y ==> x & y, but instead get 1. y ==> ?Q 2. [| y; x & ?Q |] ==> x &
y. Being able to deduct forwards from a hypothesis of form [| x; y |] to
get a new hypothesis of form x & y is my goal here.
By default, the drule method only eliminates the first assumption of
the rule, while in your case you want to eliminate both assumptions at
once. You can do this with "apply (drule (1) conjI)", where the (1)
says how many additional assumptions to match. It is practically the
same as "apply (drule conjI, assumption)".
The second problem I'm having is with the defining and use of axioms. This
is the code I'm using:consts
S :: "'a => bool"
B :: "'a => bool => bool"axioms
sb: "((B x y) & (S x) ==> y"I'm not certain how I am defining or using these wrong, but when I try to
use it in a theorem it does not do what I expect it to.theorem "((B x z) & (S x) ==> z"
apply (simp add: sb)yields the empty result sequence error rather than the "no subgoals!" that I
would expect.
Instead of using the simplifier, try using (erule sb) or (drule sb,
simp). The lemma sb does not work well as a simp rule, because it
contains a free variable in the assumptions that does not occur in the
conclusion. Basically, the sb rule tells the simplifier to rewrite any
term "y" to "True", as long as the side-condition "(B x y) & (S x)"
holds. The problem is that the simplifier doesn't know what value of x
to use when checking the side condition.
Thanks in advance for the help, I've been hammering at these problems all
day and have been able to boil them down to these simple cases but have no
idea why they are failing.-Erich Kummerfeld
Hope this helps,
Email Gateway (Aug 18 2022 at 12:13):From: Lawrence Paulson <lp15@cam.ac.uk>
The step that you want to perform is not how the calculus is intended
to be used, so you should not expect to get a good outcome. The
correct way to prove this result is by splitting the conjunction
rather than trying to create an identical conjunction. More generally,
the usual proof technique involves breaking down the assumptions and
goals into atomic elements.
Therefore, try instead
apply (rule conjI)
Larry Paulson
Email Gateway (Aug 18 2022 at 12:15):From: Perry James <perry@dsrg.org>
Hi Erich,
For your first question, I think you want to use an introduction rule
instead of an elimination. I haven't yet worked with axioms, so I'll leave
that to others.
Hope this helps,
Perry
lemma "[| x; y |] ==> x & y"
apply (rule conjI)
apply (assumption)
apply (assumption)
done
Email Gateway (Aug 18 2022 at 12:16):From: Erich Kummerfeld <ekummerfeld@gmail.com>
Hi Perry,
The trick I'm trying to accomplish with the first problem actually ties into
the second problem I'm having. Basically I'm trying to solve [| B x False;
S x |] ==> False by transforming it into [| B x False & S x |] ==> False and
then using the axiom I mentioned earlier. Neither of these steps appears to
work though and that's my confusion.
Best,
Erich
Last updated: May 03 2024 at 04:19 UTC