等式推理运算符在实践中如何使用？

Question

Agda Standard Library 导出一些运算符，允许您以类似于在纸上所做的方式或在 Haskell 社区中教授的方式编写证明。虽然您可以根据需要使用 with 抽象、rewrite 或辅助引理来改进目标，以某种系统的方式编写 "conventional" Agda 证明，但我不太清楚如何使用相等推理原语证明 "comes to be".

也就是说，虽然您可以找到有关这些证明在完成并进行类型检查后的样子的示例 here and there，但这些已经工作的示例不会向您展示它们是如何以系统步骤开发的-逐步（可能是孔驱动）方式。

实际是怎么做的？人们 "refactor" 是否已经存在证据？您是否尝试 "burn the candle from both sides" 从初始目标的左侧和右侧开始并在中间开一个洞？

此外，Agda documentation 声明如果相等推理原语在范围内，"then Auto will do equality reasoning using these constructs"。这是什么意思？

如果有人能给我指出正确的方向，或者甚至 post 一个例子，说明他们如何逐步开发这些类型的证明，他们会问自己什么问题，我将不胜感激通过它，他们把洞放在哪里等等。谢谢！

Answer 1

我认为在这里 Equational Reasoning 查看恒等式推理的定义会对您更有帮助。重点是它只是一种更好的方式来应用传递链，并允许用户看到代码中的实际表达，而不是不容易阅读的证明证据。

我使用等式推理为任何 setoid 构建证明的方法是这样的。以自然数为例

open import Relation.Binary.PropositionalEquality
open ≡-Reasoning

data ℕ : Set where
  zero : ℕ
  succ : ℕ → ℕ

_+_ : ℕ → ℕ → ℕ
m + zero   = m
m + succ n = succ (m + n)

我们以交换律为例。这就是我设定目标的方式。

comm+ : ∀ m n → m + n ≡ n + m
comm+ m zero     = {!!}
comm+ m (succ n) =
  begin
    succ (m + n)
  ≡⟨ {!!} ⟩
    succ n + m
  ∎

现在我看到了原始表达式和目标，我的目标证明在括号内。我只处理表达式，保持证明对象不变并添加我认为应该有效。

comm+ : ∀ m n → m + n ≡ n + m
comm+ m zero     = {!!}
comm+ m (succ n) =
  begin
    succ (m + n)
  ≡⟨ {!!} ⟩
    succ (n + m)
  ≡⟨ {!!}⟩
    succ n + m
  ∎

一旦我认为我有了证明，我就会处理证明我的步骤合理的证明对象。

关于自动战术，我认为你不应该为此烦恼。有一段时间没有开发了。

等式推理运算符在实践中如何使用？

How are the equational reasoning operators used in practice?

agda