问题

我想证明在一个幺半群 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"])

我想要证明的思路如下：

v⋅u⋅v' = ε⋅v' 通过等同性（两边同时乘）
v⋅ε = ε⋅v' 通过幺元公理
v⋅ε = v' 通过幺元公理
v = v' 完成

不幸的是，我卡在了第一步。我不想使用 auto 或其他自动方法。我想手动完成它，以学会如何做。

这是我使用的幺半群的定义：

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"

并且该定理位于 context monoid begin 中。

我尝试过以下方法：

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)

但是这需要将额外的前提条件添加到 from 中，否则 apply (rule subst) 会失败。

from uv1 um vm v'm have "v ⋅ u ⋅ v' = v ⋅ ε"

另一种尝试是：

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 ⋅ ε"

然而，我仍然不知道如何将 ε 替换为 vu1，从而卡在最后一步。

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"])

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

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"

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)

 1. v ∈ M
 2. u ∈ M
 3. v' ∈ M

from uv1 um vm v'm have "v ⋅ u ⋅ v' = v ⋅ 𝟭"

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 ⋅ 𝟭"

答案1

得分: 1

以下是代码部分的翻译：

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:

如果替代规则需要假设，通常可以通过等式事实后面的`[OF ...]`修饰词来提供这些假设。此外，在Isar证明中使用`unfolding`关键字通常更有趣。您从https://stackoverflow.com/a/75362601/5158425中的证明将如下所示：

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

我们可以通过使用`also have ...`关键字来串联相等式，使其更加简单：

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

这里，左边的`...`代替了前面几行的右边部分。此外，这个证明非常基础，以至于我们可以使用立即证明(`.`)和默认证明(`..`)的证明方法。它们大致相当于“根据假设”和“根据规则”。


<details>
<summary>英文:</summary>

If substitution rules require assumptions, it&#39;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.

</details>



# 答案2
**得分**: 0

我找到了一个完整的证明，但它相当冗长和难看。我觉得这个证明可以更好地完成（而不是依赖于 `auto`）。

```Isabelle
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 ⋅ 𝓕"
    apply(subst vu1[symmetric])
    apply(assumption)
    done
  from v'm this have "v' = v ⋅ 𝓕"
    apply(subst left_unit[symmetric])
    apply(assumption)
    apply(assumption)
    done
  from vm this show "v = v'"
    apply(subst right_unit[symmetric])
    apply(assumption)
    apply(rule sym)
    apply(assumption)
    done
qed

希望这样的格式更符合您的需求。

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 ⋅ 𝟭"
    apply(subst vu1[symmetric])
    apply(assumption)
    done
  from v'm this have "v' = v ⋅ 𝟭"
    apply(subst left_unit[symmetric])
    apply(assumption)
    apply(assumption)
    done
  from vm this show "v = v'"
    apply(subst right_unit[symmetric])
    apply(assumption)
    apply(rule sym)
    apply(assumption)
    done
qed