Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Pairs/tuples


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

From: Steve W <s.wong.731@gmail.com>
Greetings,

I'm currently experimenting with pairs/tuples, like the following:

axiomatization
lst :: "((natnat)nat) list"
where ax : "lst = [((1,2),3)]"

lemma "snd (lst ! 0) = (3::nat)"
using ax
sledgehammer

Does anyone know how I can prove that lemma since sledgehammer can't seem to
find a proof?

Also, if lst was of type "(nat * nat * nat) list", then how do I read the
3rd element from a tuple?

TIA

Steve

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

From: Christian Sternagel <christian.sternagel@uibk.ac.at>
Hi,

there are only pairs in Isabelle and the pair constructor * is
right-associative. Hence when you write

nat * nat * nat

it really is

nat * (nat * nat)

and a corresponding value would be (1, (2, 3)) (again you can save
parentheses by writing (1, 2, 3) instead). Thus getting the third
element is done by nested calls to snd, e.g.,

lemma "snd (snd (1, (2, 3))) = 3" by simp

You see that I do not need a sledgehammer to prove the fact ;). Mere
rewriting is enough. The same is true for your initial lemma

lemma "snd (snd ([(1, 2, 3)] ! 0)) = 3" by simp

hope this helps

chris

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

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

Thanks for that. But if I have

axiomatization
lst :: "natnatnat"
where ax : "lst = (1,2,3)"

lemma "snd (snd lst) = 3"
using ax
apply simp

doesn't seem to prove it. I guess I need some form of a substitution so
that (1,2,3) is substituted into lst?

Thanks
Steve

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

From: Steve W <s.wong.731@gmail.com>
Thanks for the replies. After some more experiments, it seems that if one of
the elements in the tuple has a variable type, then it's not so trivial. For
example:

axiomatization
lst :: "'anatnat"

axioms
ax : "lst = (1,2,3)"

lemma "snd (snd lst) = 3"
apply (simp add: ax)

doesn't find a proof. How come changing the type of an element could make
such a difference?

TIA

Steve

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

From: Tjark Weber <webertj@in.tum.de>
Steve,

In the axiom ax, 'a provides a constant 1, i.e., 'a is of sort "one".
Hence the inferred (most general) type of lst in ax is 'a::one * nat * nat. Switch on Isabelle > Settings > Display > Show Sorts and have
Isabelle print the axiom ("thm ax") to see this.

In the lemma, however, the inferred type of lst is its declared type
'a * nat * nat, which is more general than 'a::one * nat * nat.
Therefore, the axiom ax does not apply.

By the way, you should really use definition instead of axiomatization/
axioms in your formalizations.

Kind regards,
Tjark

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

From: Steve W <s.wong.731@gmail.com>
I see. But why is 'a of sort "one"? Is there a way to declare "lst =
(1,2,3)" without fixing the sort?

Thanks
Steve

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

From: Tjark Weber <webertj@in.tum.de>
On Sun, 2011-04-10 at 19:21 +0100, Steve W wrote:

I see. But why is 'a of sort "one"?

Because you used the constant 1 in ax. In Isabelle/HOL, the (most
general) type of 1 is 'a::one (rather than, e.g., nat or int).

Is there a way to declare "lst = (1,2,3)" without fixing the sort?

Well, if 1 was of type 'a (rather than 'a::one), the type of lst in your
axiom would be 'a * nat * nat (rather than 'a::one * nat * nat). For
instance, consider

consts myconst :: 'a
axiomatization lst :: "'a * nat * nat"
axioms ax : "lst = (myconst,2,3)"

lemma "snd (snd lst) = 3"
by (simp add: ax)

However, none of this is very idiomatic. It might be helpful to know
more about what you're actually trying to achieve.

Kind regards,
Tjark


Last updated: Mar 28 2024 at 20:16 UTC