Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Proving two real^3 spaces are the same

view this post on Zulip Email Gateway (Aug 18 2022 at 17:27):

From: s.wong.731@gmail.com
Hi,

If I have two real^3 spaces S1 and S2 as:

axiomatization
S1 :: "real ^ 2" and
S2 :: "real ^ 2" where
r1: "S1 $ 0 = S2 $ 0" and
r2: "S1 $ 1 = S2 $ 1" and
r3: "S1 $ 2 = S2 $ 2"

lemma "S1 = S2"

How would one go about proving the lemma? I suppose I'd need Cart_eq, which
reads:

lemma Cart_eq: "(x = y) <--> (ALL i. x$i = y$i)"

but it quantifies over all i's. Since S1 and S2 have only 3 dimensions,
then should i be only in the range [1..3]?

Thanks
Steve

view this post on Zulip Email Gateway (Aug 18 2022 at 17:27):

From: Timothy McKenzie <tjm1983@gmail.com>
On Wed, 30 Mar 2011 07:33:25 s.wong.731@gmail.com wrote:

Hi,

If I have two real^3 spaces S1 and S2 as:

axiomatization
S1 :: "real ^ 2" and
S2 :: "real ^ 2" where
r1: "S1 $ 0 = S2 $ 0" and
r2: "S1 $ 1 = S2 $ 1" and
r3: "S1 $ 2 = S2 $ 2"

You've written "real ^ 2" where I think you mean "real ^ 3", but
I'll leave it as it is for illustrative purposes.

lemma "S1 = S2"

How would one go about proving the lemma? I suppose I'd need
Cart_eq, which reads:

lemma Cart_eq: "(x = y) <--> (ALL i. x$i = y$i)"

but it quantifies over all i's. Since S1 and S2 have only 3
dimensions, then should i be only in the range [1..3]?

The "2" in your type "real^2" is a type, not a member of the
natural numbers type (or any other type). You can write any
integer, and if Isabelle believes it's of the type "2", it will be
interpreted as a member of that type by taking its remainder
modulo 2. For example:

lemma "-6 = (2 :: 2)" by simp

So your r1 and r3 say exactly the same thing, but Isabelle didn't
complain, because it can interpret them meaningfully.

So the quantified i in Cart_eq (when applied in your situation) is
an element of the type "2", which has only two elements: "0" and
"1" (or "1" and "2", if you prefer). The trick is to turn this
"ALL i." into a conjunction "x$1 = y$1 & x$2 = y$2", which can be
quickly proven from your r2 and r3. Fortunately, forall_2 can do
just this, so:

lemma "S1 = S2"
using r2 r3
by (simp add: Cart_eq forall_2)

Multivariate_Analysis also has similar lemmas forall_1 and
forall_3 for the types "1" and "3", but not forall_4 or greater.

I tested all this in Isabelle2009-2. I haven't moved to
Isabelle2011 yet, because my work relies heavily on what I've just
described, and the following in the NEWS file for Isabelle2011
worried me:

Also note that the indices are now natural numbers and not from
some finite type. Finite cartesian products of euclidean spaces,
products of euclidean spaces the real and complex numbers are
instantiated to be euclidean_spaces. INCOMPATIBILITY.

Thanks
Steve

Tim
<><
signature.asc

view this post on Zulip Email Gateway (Aug 18 2022 at 17:27):

From: Brian Huffman <brianh@cs.pdx.edu>
On Tue, Mar 29, 2011 at 3:05 PM, Timothy McKenzie <tjm1983@gmail.com> wrote:

On Wed, 30 Mar 2011 07:33:25 s.wong.731@gmail.com wrote:

Hi,

If I have two real^3 spaces S1 and S2 as:

axiomatization
S1 :: "real ^ 2" and
S2 :: "real ^ 2" where
r1: "S1 $ 0 = S2 $ 0" and
r2: "S1 $ 1 = S2 $ 1" and
r3: "S1 $ 2 = S2 $ 2"

You've written "real ^ 2" where I think you mean "real ^ 3", but
I'll leave it as it is for illustrative purposes.

lemma "S1 = S2"

How would one go about proving the lemma? I suppose I'd need
Cart_eq, which reads:

lemma Cart_eq: "(x = y) <--> (ALL i. x$i = y$i)"

but it quantifies over all i's. Since S1 and S2 have only 3
dimensions, then should i be only in the range [1..3]?

The "2" in your type "real^2" is a type, not a member of the
natural numbers type (or any other type). You can write any
integer, and if Isabelle believes it's of the type "2", it will be
interpreted as a member of that type by taking its remainder
modulo 2. For example:

lemma "-6 = (2 :: 2)" by simp

So your r1 and r3 say exactly the same thing, but Isabelle didn't
complain, because it can interpret them meaningfully.

So the quantified i in Cart_eq (when applied in your situation) is
an element of the type "2", which has only two elements: "0" and
"1" (or "1" and "2", if you prefer). The trick is to turn this
"ALL i." into a conjunction "x$1 = y$1 & x$2 = y$2", which can be
quickly proven from your r2 and r3. Fortunately, forall_2 can do
just this, so:

lemma "S1 = S2"
using r2 r3
by (simp add: Cart_eq forall_2)

Multivariate_Analysis also has similar lemmas forall_1 and
forall_3 for the types "1" and "3", but not forall_4 or greater.

Tim,

Thanks for the great explanation of numeral types!

I tested all this in Isabelle2009-2. I haven't moved to
Isabelle2011 yet, because my work relies heavily on what I've just
described, and the following in the NEWS file for Isabelle2011
worried me:

types
real ^ 'n ~> 'a::real_vector
~> 'a::euclidean_space
~> 'a::ordered_euclidean_space
(depends on your needs)

I'm sure Johannes could say more about these changes, but I wanted to
point out one benefit:

Many lemmas that used to be specific to types "real ^ 'n" are now
proved in general for any type in class euclidean_space. This means
that users of the Multivariate_Analysis libraries are no longer
restricted to using cartesian product types like "real ^ 2" and "real
^ 3". Types like "real * real" and "real * real * real" are also
instances of class euclidean_space, and so most of the theorems in the
Multivariate_Analysis library will work with them too.

I happen to think that ordinary tuples are much easier to work with:
For example, "(x, y, z)" is rather nicer than any notation available
for type "real ^ 3". Also, it isn't too much trouble to convert back
and forth between tuples and the generic "_$$_" notations:

lemma
fixes x y z :: "real"
shows "(x,y,z) $$ 0 = x \<and> (x,y,z) $$ 1 = y \<and> (x,y,z) $$ 2 = z"
by (simp add: euclidean_component_def basis_prod_def)

view this post on Zulip Email Gateway (Aug 18 2022 at 17:27):

From: Johannes Hölzl <hoelzl@in.tum.de>
Hi Timothy,

Am Mittwoch, den 30.03.2011, 11:05 +1300 schrieb Timothy McKenzie:
[..]

I tested all this in Isabelle2009-2. I haven't moved to
Isabelle2011 yet, because my work relies heavily on what I've just
described, and the following in the NEWS file for Isabelle2011
worried me:

Also note that the indices are now natural numbers and not from
some finite type. Finite cartesian products of euclidean spaces,
products of euclidean spaces the real and complex numbers are
instantiated to be euclidean_spaces. INCOMPATIBILITY.

Did you try Isabelle2011? Of course the type real ^ 'n was not removed,
but for most lemmas the constant names changed.

Either you rewrite your terms (which is mostly Search & Replace) or you
try to stay with the "real ^ 'n" constants and use the simplifier to
rewrite them at each proof (but I'm not sure how well this approach
works).

Alternatively we could try to add the real^'n version of all changed
lemmas back (by specialising the lemmas about euclidean spaces).

When we introduced this changes I were not aware of any existing work
using Multivariate_Analysis. Hence we did not care about backwards
compatibility. But we can try to add compatibility lemmas so you can
port your work to the next Isabelle release. Is your work available
anywhere? Is it possible to take a look at it?

Tim
<><

Greetings,
Johannes

Last updated: Nov 21 2024 at 12:39 UTC