I want to prove that inverse element is unique in a monoid M
theorem inverse_unique:
assumes "u β
v' = π"
assumes "v β
u = π"
assumes "u β M"
assumes "v β M"
assumes "v' β M"
shows "v = v'"
proof -
have "v β
u β
v' = v β
π"
apply (rule arg_cong[of "u β
v'" π "Ξ» x. vβ
x"])
The idea is to show the following steps
vβ
uβ
v'=πβ
v' by congruence (multiplying both sides)
vβ
π=πβ
v' by monoid neutral element axiom
vβ
π=v' by monoid neutral element axiom
v=v' done
Unfortunately I am stuck on the very first step. I don't want to use auto
or any other automatic approach. I want to do it by hand to learn how to do it.
I've been trying with apply (subst)
and apply (rule arg_cong)
and many variations thereof. Nothing really works.
This is the definition of monoid that I am using
locale monoid =
fixes M and composition (infixl "β
" 70) and unit ("π")
assumes composition_closed [intro, simp]: "β¦ a β M; b β M β§ βΉ a β
b β M"
and unit_closed [intro, simp]: "π β M"
and associative [intro]: "β¦ a β M; b β M; c β M β§ βΉ (a β
b) β
c = a β
(b β
c)"
and left_unit [intro, simp]: "a β M βΉ π β
a = a"
and right_unit [intro, simp]: "a β M βΉ a β
π = a"
and the theorem is in context monoid begin
Other thing I've tried is this
theorem inverse_unique:
assumes uv1:"u β
v' = π"
assumes vu1:"v β
u = π"
assumes um:"u β M"
assumes vm:"v β M"
assumes v'm:"v' β M"
shows "v = v'"
proof -
from uv1 have "v β
u β
v' = v β
π"
apply(rule subst)
apply(rule associative)
which gets me quite far but the associative rule requires now
1. v β M
2. u β M
3. v' β M
However, if I add those to from
from uv1 um vm v'm have "v β
u β
v' = v β
π"
then apply(rule subst)
yields Failed to apply proof methodβ
.
Another thing I've tried is this
theorem inverse_unique:
assumes uv1:"u β
v' = π"
assumes vu1:"v β
u = π"
assumes um:"u β M"
assumes vm:"v β M"
assumes v'm:"v' β M"
shows "v = v'"
proof -
from uv1 have "v β
(u β
v') = v β
π"
apply (rule subst)
apply (rule refl)
done
from this um vm v'm have "v β
u β
v' = v β
π"
apply (subst associative)
apply (assumption)
apply (assumption)
apply (assumption)
apply (assumption)
done
from this vu1 have "π β
v' = v β
π"
which actually works, but then again I get stuck at the last from this vu1 have "π β
v' = v β
π"
because I still don't know how to substitute π
for vu1
.
If substitution rules require assumptions, it's often convenient to supply these through the [OF ...]
modifier behind the equality fact. Also, rewriting in Isar proofs usually makes more fun using the unfolding
keyword. Your proof from https://stackoverflow.com/a/75362601/5158425 would then read:
theorem inverse_unique:
assumes uv1: "u β
v' = π"
assumes vu1: "v β
u = π"
assumes um: "u β M"
assumes vm: "v β M"
assumes v'm: "v' β M"
shows "v = v'"
proof -
have "v β
(u β
v') = v β
π" unfolding uv1 by (rule refl)
from this have "v β
u β
v' = v β
π" unfolding associative[OF vm um v'm] by assumption
from this have "π β
v' = v β
π" unfolding vu1 by assumption
from this have "v' = v β
π" unfolding left_unit[OF v'm] by assumption
from this show "v = v'" unfolding right_unit[OF vm] by (rule sym)
qed
We can make this even simpler by use of the also have ...
keywords to chain equalities:
proof -
have βΉv = v β
πβΊ using right_unit[OF vm, symmetric] .
also have βΉ... = v β
(u β
v')βΊ unfolding uv1 ..
also have βΉ... = v β
u β
v'βΊ using associative[OF vm um v'm, symmetric] .
also have βΉ... = π β
v'βΊ unfolding vu1 ..
finally show ?thesis unfolding left_unit[OF v'm] .
qed
Here, the ...
on the left-hand sides abbreviate the right-hand sides of the preceding lines. Moreover, the proof is elementar to a level that we can use the proof methods for immediate proof .
and default proof ..
. They do roughly the same βby assumptionβ and βby ruleβ would.