更好地推断 agda 证明

Question

假设我有以下编译的 Agda 代码（其中 +-assoc 和 +-comm 取自 plf 课程。在每个步骤中要求显式子表达式似乎很费力为了简化代码；但是删除任何一个显式表达式都会导致代码无法编译。

如何在编写证明时获得更好的类型推断？

+-swap : ∀ (m n p : ℕ) -> m + (n + p) ≡ n + (m + p)
+-swap zero n p = refl
+-swap (suc m) n p =
  begin
    suc m + (n + p)
    ≡⟨ +-comm (suc m) (n + p) ⟩
    (n + p) + (suc m)
    ≡⟨ +-assoc n p (suc m) ⟩
    n + (p + suc m)
    ≡⟨ cong (n +_) (+-comm p (suc m)) ⟩
    n + (suc m + p)
  ∎

Answer 1

如果我对您的要求的理解是正确的，您希望能够省略中间表达式，例如 suc m + (n + p)

为用户提供 _∎、_≡⟨_⟩_ 和 begin_ 等运算符的 ≡-Reasoning 模块的全部意义在于明确这些数量，以便证明更具可读性，每个推理步骤都可以清楚地展示和理解。

这意味着如果你想省略这些量，你不应该使用这个库，而是使用下面的方法之一来证明这种等式证明。

出于自包含的目的，这里是必需的导入：

module EqProofs where

open import Data.Nat
open import Data.Nat.Properties
open import Relation.Binary.PropositionalEquality
open ≡-Reasoning

第一种可能性是像您一样使用等式推理模块：

+-swap₁ : ∀ (m n p : ℕ) → m + (n + p) ≡ n + (m + p)
+-swap₁ zero n p = refl
+-swap₁ (suc m) n p = begin
  suc m + (n + p)   ≡⟨ +-comm (suc m) (n + p) ⟩
  (n + p) + (suc m) ≡⟨ +-assoc n p (suc m) ⟩
  n + (p + suc m)   ≡⟨ cong (n +_) (+-comm p (suc m)) ⟩
  n + (suc m + p)   ∎

但您也可以使用等式的传递性显式给出项：

+-swap₂ : ∀ (m n p : ℕ) → m + (n + p) ≡ n + (m + p)
+-swap₂ zero _ _ = refl
+-swap₂ (suc m) n p =
  trans
    (+-comm (suc m) (n + p))
    (trans
      (+-assoc n p (suc m))
      (cong (n +_) (+-comm p (suc m))))

或者您可以使用 rewrite 使用等式证明来简化目标：

+-swap₃ : ∀ (m n p : ℕ) → m + (n + p) ≡ n + (m + p)
+-swap₃ zero _ _ = refl
+-swap₃ (suc m) n p
  rewrite +-comm (suc m) (n + p)
  | +-assoc n p (suc m)
  | cong (n +_) (+-comm p (suc m)) = refl

在最后两种可能性中，中间量被隐藏（并且很容易被 Agda 推断），如您所愿。

编辑：

您可以使用下划线省略一些（虽然不是全部，因为类型检查器需要信息来解决约束）所需的参数。除了使用 rewrite 之外的所有情况下都可以这样做，如下所示：

+-swap₁ : ∀ (m n p : ℕ) → m + (n + p) ≡ n + (m + p)
+-swap₁ zero n p = refl
+-swap₁ (suc m) n p = begin
  suc m + (n + p)   ≡⟨ +-comm _ (n + p) ⟩
  (n + p) + (suc m) ≡⟨ +-assoc n p _ ⟩
  n + (p + suc m)   ≡⟨ cong (n +_) (+-comm p _) ⟩
  n + (suc m + p)   ∎

+-swap₂ : ∀ (m n p : ℕ) → m + (n + p) ≡ n + (m + p)
+-swap₂ zero _ _ = refl
+-swap₂ (suc m) n p =
  trans
    (+-comm _ (n + p))
    (trans
      (+-assoc n p _)
      (cong (n +_) (+-comm p _)))

+-swap₃ : ∀ (m n p : ℕ) → m + (n + p) ≡ n + (m + p)
+-swap₃ zero _ _ = refl
+-swap₃ (suc m) n p
  rewrite +-comm (suc m) (n + p)
  | +-assoc n p (suc m)
  | cong (n +_) (+-comm p (suc m)) = refl

编辑 n°2：

作为旁注，您可以证明这个属性而不必对其任何一个参数进行模式匹配。这是这个证明，使用链式相等。你会注意到只有几个参数必须明确提供，而其他的可以用下划线代替：

+-swap₄ : ∀ (m n p : ℕ) → m + (n + p) ≡ n + (m + p)
+-swap₄ m n p = begin
  m + (n + p) ≡⟨ +-assoc m _ _ ⟩
  (m + n) + p ≡⟨ cong (_+ p) (+-comm m _) ⟩
  (n + m) + p ≡⟨ +-assoc n _ _ ⟩
  n + (m + p)  ∎

更好地推断 agda 证明

Getting better inference for agda proofs

proof

agda