Isabelle在等式的两边都乘以（Isar中的等式推理）

huangapple
go评论64阅读模式
英文:

Isabelle multiply both sides of an equation (equational reasoning in Isar)

问题

我想证明在一个幺半群 M 中，逆元素是唯一的。

  1. theorem inverse_unique:
  2.   assumes "u ⋅ v' = ε"
  3.   assumes "v ⋅ u = ε"
  4.   assumes "u ∈ M"
  5.   assumes "v ∈ M"
  6.   assumes "v' ∈ M"
  7.   shows "v = v'"
  8. proof -
  9.   have "v ⋅ u ⋅ v' = v ⋅ ε"  
  10.     apply (rule arg_cong[of "u ⋅ v'" ε "λ x. v⋅x"])

我想要证明的思路如下：

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

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

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

  1. locale monoid =
  2.   fixes M and composition (infixl "⋅" 70) and unit (ε)
  3.   assumes composition_closed [intro, simp]: "⟦ a ∈ M; b ∈ M ⟧ ⟹ a ⋅ b ∈ M"
  4.     and unit_closed [intro, simp]: "ε ∈ M"
  5.     and associative [intro]: "⟦ a ∈ M; b ∈ M; c ∈ M ⟧ ⟹ (a ⋅ b) ⋅ c = a ⋅ (b ⋅ c)"
  6.     and left_unit [intro, simp]: "a ∈ M ⟹ ε ⋅ a = a"
  7.     and right_unit [intro, simp]: "a ∈ M ⟹ a ⋅ ε = a"

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

我尝试过以下方法：

  1. theorem inverse_unique:
  2.   assumes uv1: "u ⋅ v' = ε"
  3.   assumes vu1: "v ⋅ u = ε"
  4.   assumes um: "u ∈ M"
  5.   assumes vm: "v ∈ M"
  6.   assumes v'm: "v' ∈ M"
  7.   shows "v = v'"
  8. proof -
  9.   from uv1 have "v ⋅ u ⋅ v' = v ⋅ ε"
  10.     apply (rule subst)
  11.     apply (rule associative)

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

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

另一种尝试是：

  1. theorem inverse_unique:
  2.   assumes uv1: "u ⋅ v' = ε"
  3.   assumes vu1: "v ⋅ u = ε"
  4.   assumes um: "u ∈ M"
  5.   assumes vm: "v ∈ M"
  6.   assumes v'm: "v' ∈ M"
  7.   shows "v = v'"
  8. proof -
  9.   from uv1 have "v ⋅ (u ⋅ v') = v ⋅ ε"
  10.     apply (rule subst) 
  11.     apply (rule refl)
  12.     done
  13.   from this um vm v'm have "v ⋅ u ⋅ v' = v ⋅ ε"
  14.     apply (subst associative)  
  15.     apply (assumption)
  16.     apply (assumption)
  17.     apply (assumption)
  18.     apply (assumption)
  19.     done
  20.   from this vu1 have "ε ⋅ v' = v ⋅ ε"

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

英文:

I want to prove that inverse element is unique in a monoid M

  2. theorem inverse_unique:
  3.   assumes "u ⋅ v' = 𝟭"
  4.   assumes "v ⋅ u = 𝟭"
  5.   assumes "u ∈ M"
  6.   assumes "v ∈ M"
  7.   assumes "v' ∈ M"
  8.   shows "v = v'"
  9. proof -
  10.   have "v ⋅ u ⋅ v' = v ⋅ 𝟭"  
  11.     apply (rule arg_cong[of "u ⋅ v'" 𝟭 "λ x. v⋅x"])

The idea is to show the following steps

  1. v⋅u⋅v'=𝟭⋅v' by congruence (multiplying both sides)
  2. v⋅𝟭=𝟭⋅v' by monoid neutral element axiom
  3. v⋅𝟭=v' by monoid neutral element axiom
  4. 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

  1. locale monoid =
  2.   fixes M and composition (infixl "⋅" 70) and unit ("𝟭")
  3.   assumes composition_closed [intro, simp]: "⟦ a ∈ M; b ∈ M ⟧ ⟹ a ⋅ b ∈ M"
  4.     and unit_closed [intro, simp]: "𝟭 ∈ M"
  5.     and associative [intro]: "⟦ a ∈ M; b ∈ M; c ∈ M ⟧ ⟹ (a ⋅ b) ⋅ c = a ⋅ (b ⋅ c)"
  6.     and left_unit [intro, simp]: "a ∈ M ⟹ 𝟭 ⋅ a = a"
  7.     and right_unit [intro, simp]: "a ∈ M ⟹ a ⋅ 𝟭 = a"

and the theorem is in context monoid begin

Other thing I've tried is this

  2. theorem inverse_unique:
  3.   assumes uv1:"u ⋅ v' = 𝟭"
  4.   assumes vu1:"v ⋅ u = 𝟭"
  5.   assumes um:"u ∈ M"
  6.   assumes vm:"v ∈ M"
  7.   assumes v'm:"v' ∈ M"
  8.   shows "v = v'"
  9. proof -
  10.   from uv1 have "v ⋅ u ⋅ v' = v ⋅ 𝟭"
  11.     apply(rule subst)
  12.     apply(rule associative)

which gets me quite far but the associative rule requires now

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

However, if I add those to from

  1. 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

  2. theorem inverse_unique:
  3.   assumes uv1:"u ⋅ v' = 𝟭"
  4.   assumes vu1:"v ⋅ u = 𝟭"
  5.   assumes um:"u ∈ M"
  6.   assumes vm:"v ∈ M"
  7.   assumes v'm:"v' ∈ M"
  8.   shows "v = v'"
  9. proof -
  10.   from uv1 have "v ⋅ (u ⋅ v') = v ⋅ 𝟭"
  11.     apply (rule subst) 
  12.     apply (rule refl)
  13.     done
  14.   from this um vm v'm have "v ⋅ u ⋅ v' = v ⋅ 𝟭"
  15.     apply (subst associative)  
  16.     apply (assumption)
  17.     apply (assumption)
  18.     apply (assumption)
  19.     apply (assumption)
  20.     done
  21.   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.

答案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:

  1. 如果替代规则需要假设，通常可以通过等式事实后面的`[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

  2. 我们可以通过使用`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

  2. 这里，左边的`...`代替了前面几行的右边部分。此外，这个证明非常基础，以至于我们可以使用立即证明(`.`)和默认证明(`..`)的证明方法。它们大致相当于“根据假设”和“根据规则”。
  5. <details>
  6. <summary>英文:</summary>
  8. 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

  2. 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

  2. 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.
  4. </details>
  8. # 答案2
  9. **得分**: 0
  11. 我找到了一个完整的证明，但它相当冗长和难看。我觉得这个证明可以更好地完成（而不是依赖于 `auto`）。
  13. ```Isabelle
  14. theorem inverse_unique:
  15.   assumes uv1: "u ⋅ v' = 𝓕"
  16.   assumes vu1: "v ⋅ u = 𝓕"
  17.   assumes um: "u ∈ M"
  18.   assumes vm: "v ∈ M"
  19.   assumes v'm: "v' ∈ M"
  20.   shows "v = v'"
  21. proof -
  22.   from uv1 have "v ⋅ (u ⋅ v') = v ⋅ 𝓕"
  23.     apply (rule subst) 
  24.     apply (rule refl)
  25.     done
  26.   from this um vm v'm have "v ⋅ u ⋅ v' = v ⋅ 𝓕"
  27.     apply (subst associative)  
  28.     apply (assumption)
  29.     apply (assumption)
  30.     apply (assumption)
  31.     apply (assumption)
  32.     done
  33.   from this vu1 have "𝓕 ⋅ v' = v ⋅ 𝓕"
  34.     apply(subst vu1[symmetric])
  35.     apply(assumption)
  36.     done
  37.   from v'm this have "v' = v ⋅ 𝓕"
  38.     apply(subst left_unit[symmetric])
  39.     apply(assumption)
  40.     apply(assumption)
  41.     done
  42.   from vm this show "v = v'"
  43.     apply(subst right_unit[symmetric])
  44.     apply(assumption)
  45.     apply(rule sym)
  46.     apply(assumption)
  47.     done
  48. qed

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

英文:

I found a full proof

  2. theorem inverse_unique:
  3.   assumes uv1:&quot;u ⋅ v&#39; = &#120813;&quot;
  4.   assumes vu1:&quot;v ⋅ u = &#120813;&quot;
  5.   assumes um:&quot;u ∈ M&quot;
  6.   assumes vm:&quot;v ∈ M&quot;
  7.   assumes v&#39;m:&quot;v&#39; ∈ M&quot;
  8.   shows &quot;v = v&#39;&quot;
  9. proof -
  10.   from uv1 have &quot;v ⋅ (u ⋅ v&#39;) = v ⋅ &#120813;&quot;
  11.     apply (rule subst) 
  12.     apply (rule refl)
  13.     done
  14.   from this um vm v&#39;m have &quot;v ⋅ u ⋅ v&#39; = v ⋅ &#120813;&quot;
  15.     apply (subst associative)  
  16.     apply (assumption)
  17.     apply (assumption)
  18.     apply (assumption)
  19.     apply (assumption)
  20.     done
  21.   from this vu1 have &quot;&#120813; ⋅ v&#39; = v ⋅ &#120813;&quot;
  22.     apply(subst vu1[symmetric])
  23.     apply(assumption)
  24.     done
  25.   from v&#39;m this have &quot;v&#39; = v ⋅ &#120813;&quot;
  26.     apply(subst left_unit[symmetric])
  27.     apply(assumption)
  28.     apply(assumption)
  29.     done
  30.   from vm this show &quot;v = v&#39;&quot;
  31.     apply(subst right_unit[symmetric])
  32.     apply(assumption)
  33.     apply(rule sym)
  34.     apply(assumption)
  35.     done
  36. qed

but it is quite long and ugly. I feel like this could have been done better (without resorting to auto).

huangapple
  • 本文由 发表于 2023年2月6日 03:59:41
  • 转载请务必保留本文链接：https://go.coder-hub.com/75355119.html
  • isabelle
匿名

发表评论

匿名网友

:?: :razz: :sad: :evil: :!: :smile: :oops: :grin: :eek: :shock: :???: :cool: :lol: :mad: :twisted: :roll: :wink: :idea: :arrow: :neutral: :cry: :mrgreen:

确定