Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] A Newbie question about forward-proofs.

Email Gateway (Aug 18 2022 at 14:15):

From: Joe Fredette <jfredett@gmail.com>
Hello Isabelle Theorem Provers!

First of all, let me say, this is my first post to the list, hopefully
I'm not committing any sins-of-form-or-content, but I claim ignorance,
and thus innocence, if I do.

My question is as such:

I have a theory which has the following class definition

class Group =
fixes oper :: "'a ⇒ 'a ⇒ 'a" (infixl "[*]" 65)
and ivr :: "'a ⇒ 'a"
and e :: "'a"
assumes grp_assoc : "a [] (b [] c) = (a [] b) [] c"
and grp_id_propR [simp] : "a [*] e = a"
and grp_inv_propR [simp] : "(ivr a [] a) [] b = b";
notation oper (infixl "⨂" 65);

This (obviously) aims to represent a group. You'll of course notice
that I didn't provide the left-handed
analog of grp_id_propR, since it can be proved as a lemma, given the
following lemma, which is where I'm getting stuck, my goal is to prove
(in standard notation):

a = c => (b [] a = b [] c) /\ (a [] b = c [] b)

which is easy, simply note:

b [] a = b [] a

and

a = c

so substituting

b [] a = b [] c

And similar. My issue is that while I can get these assumptions "into"
the system (so that they're under the using this spot) I can't seem
to figure out the correct incantation to get a to be replaced with b
on one side (or any side, for that matter). My intuition is that I
need something like ssubst, but I'm not sure how to do it in the
forward-proof mode.

For reference, my current lemma:

lemma (in Group) grp_mult_id :
assumes a_eq_c: "a = c"
shows "(a [] b = c [] b) ∧ (b [] a = b [] c)";
proof
assume refl: "a [] b = a [] b";
from refl and a_eq_c obtain "a [] b = a [] c"; (* the obtain
bit (I think) is wrong,
* or at least incomplete... *)

Thanks for any help any of you could provide. I'm really enjoying
Isabelle, especially forward proof, it makes theorem proving less eye-
straining and more fun!

/Joe Fredette

Email Gateway (Aug 18 2022 at 14:15):

From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Joe,

class Group =
fixes oper :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "[*]" 65)
and ivr :: "'a \<Rightarrow> 'a"
and e :: "'a"
assumes grp_assoc: "a [] (b [] c) = (a [] b) [] c"
and grp_id_propR [simp]: "a [*] e = a"
and grp_inv_propR [simp]: "(ivr a [] a) [] b = b"
begin

What I would recommend from a pragmatic point of view is to use the simp
method:

lemma grp_mult_id:
assumes a_eq_c: "a = c"
shows "(a [] b = c [] b) \<and> (b [] a = b [] c)"
proof
have refl: "b [] a = b [] a" ..
from refl and a_eq_c have "b [] a = b [] c" by simp

"simp" invokes an automated proof tool which performs equational
rewriting using assumptions in a goal and a predefined set of rewrite
rules (see the Isabelle tutorial for more information on this).

Intermediate results in a proof are stated using "have". Assumptions
"assume" are part the resulting theorem of a proof and therefore must
fit to an outer proof obligation, which is not the case in your proof
because "b [] a = b [] a" is not part of the assumptions of the lemma.

Hope this helps,
Florian
signature.asc

Email Gateway (Aug 18 2022 at 14:15):

From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Joe,

If I can bother you with another question. I wanted to get ivr to have
a prefix unary syntax (or a postfix, the problem (I imagine) is
isomorphic), once again, I just can't seem to find a suitable
incantation. The big tutorial (the 200+ page one) talks about using
datatypes somewhere for this purpose, But I don't see how that helps me
here.

You can attach syntax to constants using "notation", e.g.

notation ivr ("INV _")

C.f. the Isabelle Reference Manual, keyword "notation".

Further, another (semi-related) question. In Haskell (which is where my
background lies), one can do associated datatypes, eg

class Foo a where
data Bar a :: * -> * bar :: Bar a b -> b -> (a,b)
--whatever

is there an analog in Isabelle?

Isabelle's type classes are, compared to Haskell, very simplistic:
operations of type classes are polymorphic in exactly one variable;
all those fancy Haskell extensions (multiple parameters, polymorphism,
constructor classes, associated types) are not present.

Hope this helps
Florian
signature.asc

Email Gateway (Aug 18 2022 at 14:15):

From: Joe Fredette <jfredett@gmail.com>
You know what it was, I just had the goal wrong. I mistyped and put "a
[] b = a [] c". You're advice worked perfectly after I saw that...

Teach me to try to prove stuff in the wee hours of the morning!

Thanks so much for your help.

If I can bother you with another question. I wanted to get ivr to
have a prefix unary syntax (or a postfix, the problem (I imagine) is
isomorphic), once again, I just can't seem to find a suitable
incantation. The big tutorial (the 200+ page one) talks about using
datatypes somewhere for this purpose, But I don't see how that helps
me here.

Further, another (semi-related) question. In Haskell (which is where
my background lies), one can do associated datatypes, eg

class Foo a where
data Bar a :: * -> * bar :: Bar a b -> b -> (a,b)
--whatever

is there an analog in Isabelle?

Last updated: Apr 19 2024 at 01:05 UTC