为什么 Agda 会针对某些参数减少我的函数应用程序，而不会针对其他参数减少我的函数应用程序？

Question

我正在使用标准库的 AVL 树实现中的joinˡ⁺。该函数由六个模式匹配子句定义。当我将函数应用到参数时，Agda 是否会减少我的函数应用程序表达式，这取决于六个子句中的哪一个与我的参数匹配。 （或者在我看来是这样。）

下面的代码将函数应用于与函数的第一个子句匹配的参数。它是目标等式的左侧。 Agda 将它减少到右侧，我可以用refl 完成证明。所以这个按预期工作。

（请注意，代码使用的是标准库的 1.3 版本。似乎最近的版本将 AVL 树代码从 Data.AVL 移到了 Data.Tree.AVL。）

module Repro2 where

open import Data.Nat using (ℕ ; suc)
open import Data.Nat.Properties using (<-strictTotalOrder)
open import Data.Product using (_,_)
open import Relation.Binary.PropositionalEquality using (_≡_ ; refl)

open import Data.AVL.Indexed <-strictTotalOrder

okay :
  ∀ {l u h} k₆ k₂ (t₁ : Tree (const ℕ) _ _ _) k₄ t₃ t₅ t₇ b →
  joinˡ⁺ {l = l} {u} {suc (suc h)} {suc h} {suc (suc h)}
    k₆ (1# , node k₂ t₁ (node {hˡ = h} {suc h} {suc h} k₄ t₃ t₅ b) ∼+) t₇ ∼-
  ≡
  (0# , node k₄ (node k₂ t₁ t₃ (max∼ b)) (node k₆ t₅ t₇ (∼max b)) ∼0)

okay k₆ k₂ t₁ k₄ t₃ t₅ t₇ b = refl

下一个示例针对函数定义的第二个子句。与上述不同的是，目标始终不会减少，即joinˡ⁺ 不会消失。

not-okay : ∀ {l u h} k₄ k₂ (t₁ : Tree (const ℕ) _ _ _)  t₃ t₅ →
  joinˡ⁺ {l = l} {u} {suc h} {h} {suc h}
    k₄ (1# , node k₂ t₁ t₃ ∼-) t₅ ∼-
    ≡
    (0# , node k₂ t₁ (node k₄ t₃ t₅ ∼0) ∼0)

not-okay k₄ k₂ t₁ t₃ t₅ = {!!}

我错过了什么？

MrO 回答后的补充

MrO 做到了。我所知道的是，如果子句模式匹配参数的子项（或整个参数），那么我显然需要为该子项传递匹配的数据构造函数，以使评估者选择该子句。然而，这还不够。正如 MrO 指出的那样，在某些情况下，我还需要为 other 子句（即，不仅仅是我要使用的子句）模式匹配的子术语传递数据构造函数，即使手头的子句不关心他们。

为了探索这个（对我来说：主要的新）见解，我尝试了joinˡ⁺ 的其余四个子句。最后一个子句，即第 6 句，引出了另一种见解。

这是第 3 条。它的工作原理与not-okay 几乎相同。

clause₃ : ∀ {l u h} k₄ k₂ (t₁ : Tree (const ℕ) _ _ _) t₃ t₅ →
  joinˡ⁺ {l = l} {u} {suc h} {h} {suc h}
    k₄ (1# , node k₂ t₁ t₃ ∼0) t₅ ∼-
  ≡
  (1# , node k₂ t₁ (node k₄ t₃ t₅ ∼-) ∼+)

-- This does not work:
--   clause₃ k₄ k₂ t₁ t₃ t₅ = {!!} 

clause₃ k₄ k₂ t₁ (node k t₃ t₄ bal) t₅ = refl

第 4 条涉及更多。

clause₄ : ∀ {l u h} k₂ (t₁ : Tree (const ℕ) _ _ _) t₃ →
  joinˡ⁺ {l = l} {u} {h} {h} {h}
    k₂ (1# , t₁) t₃ ∼0
  ≡
  (1# , node k₂ t₁ t₃ ∼-)

-- This does not work:
--   clause₄ k₂ t₁ t₃ = {!!}

-- This still doesn't, because of t' (or so I thought):
--   clause₄ k₂ (node k t t′ b) t₃ = {!!}

-- Surprise! This still doesn't, because of b:
--   clause₄ k₂ (node k t (leaf l<u) b) t₃ = {!!}
--   clause₄ k₂ (node k t (node k′ t′′ t′′′ b') b) t₃ = {!!}

clause₄ k₂ (node k t (leaf l<u) ∼0) t₃ = refl
clause₄ k₂ (node k t (leaf l<u) ∼-) t₃ = refl

clause₄ k₂ (node k t (node k′ t′′ t′′′ b') ∼+) t₃ = refl
clause₄ k₂ (node k t (node k′ t′′ t′′′ b') ∼0) t₃ = refl
clause₄ k₂ (node k t (node k′ t′′ t′′′ b') ∼-) t₃ = refl

第 5 条类似于第 4 条。

clause₅ : ∀ {l u h} k₂ (t₁ : Tree (const ℕ) _ _ _) t₃ →
  joinˡ⁺ {l = l} {u} {h} {suc h} {suc h}
    k₂ (1# , t₁) t₃ ∼+
  ≡
  (0# , node k₂ t₁ t₃ ∼0)

clause₅ k₂ (node k t (leaf l<u) ∼0) t₃ = refl
clause₅ k₂ (node k t (leaf l<u) ∼-) t₃ = refl

clause₅ k₂ (node k t (node k′ t'′ t′′′ b′) ∼+) t₃ = refl
clause₅ k₂ (node k t (node k′ t'′ t′′′ b′) ∼0) t₃ = refl
clause₅ k₂ (node k t (node k′ t'′ t′′′ b′) ∼-) t₃ = refl

第 6 条让我有点意外。我认为我需要在任何子句需要它们的地方传递数据构造函数。但这不是MrO所说的。它显示在这个子句中：

clause₆ : ∀ {l u h} k₂ (t₁ : Tree (const ℕ) _ _ _) t₃ b →
  joinˡ⁺ {l = l} {u} {h} {h} {h}
    k₂ (0# , t₁) t₃ b
  ≡
  (0# , node k₂ t₁ t₃ b)


clause₆ k₂ t₁ t₃ b = refl

比我想象的要容易：不需要额外的数据构造函数。为什么？我去阅读了Agda参考的模式匹配部分：

https://agda.readthedocs.io/en/v2.6.1/language/function-definitions.html#case-trees

我以前读过它，但完全没有应用它所说的内容。 Agda 通过决策树（case tree）找到要选择的子句。对我来说，现在看起来 Agda 需要数据构造函数，只要它还没有到达案例树的叶子，也就是说，只要它还没有弄清楚要选择哪个子句。

对于手头的功能，案例树似乎从以下问题开始：0# 还是1#？至少这可以解释第 6 条：

• 如果是0#，那么我们知道它一定是第 6 条，不需要更多的数据构造函数。第 6 条是 0# 的唯一匹配项。所以，我们在一片叶子上，我们的案例树遍历结束了。

• 如果是1#，那么我们需要做更多的匹配，即在案例树中向下移动到下一个级别。在那里，我们需要另一个数据构造函数来查看。因此，总的来说，我们需要为案例树的每个访问级别创建一个数据构造函数。

至少这是我目前的心智模型，这似乎得到了对joinˡ⁺的观察的支持。

为了进一步验证这个心智模型，我通过颠倒六个子句的顺序修改了我的标准库副本。由于 Agda 通过按顺序遍历子句并在每个子句中从左到右构建案例树，这应该会给我们一个更好的案例树。

0# 与 1# 仍然是决策树的第一层，但后面是外部平衡，然后是内部平衡。我们不需要将树拆分为节点，除了 now last（以前是 first）子句，它实际上匹配那个。

事实上，事情的发展与预期一致。这是我修改后的标准库中子句顺序颠倒后的证明。

clause₁′ : ∀ {l u h} k₂ (t₁ : Tree (const ℕ) _ _ _) t₃ b →
  joinˡ⁺ {l = l} {u} {h} {h} {h}
    k₂ (0# , t₁) t₃ b
  ≡
  (0# , node k₂ t₁ t₃ b)

clause₁′ k₂ t₁ t₃ b = refl

clause₂′ : ∀ {l u h} k₂ (t₁ : Tree (const ℕ) _ _ _) t₃ →
  joinˡ⁺ {l = l} {u} {h} {suc h} {suc h}
    k₂ (1# , t₁) t₃ ∼+
  ≡
  (0# , node k₂ t₁ t₃ ∼0)

clause₂′ k₂ t₁ t₃ = refl

clause₃′ : ∀ {l u h} k₂ (t₁ : Tree (const ℕ) _ _ _) t₃ →
  joinˡ⁺ {l = l} {u} {h} {h} {h}
    k₂ (1# , t₁) t₃ ∼0
  ≡
  (1# , node k₂ t₁ t₃ ∼-)

clause₃′ k₂ t₁ t₃ = refl

clause₄′ : ∀ {l u h} k₄ k₂ (t₁ : Tree (const ℕ) _ _ _) t₃ t₅ →
  joinˡ⁺ {l = l} {u} {suc h} {h} {suc h}
    k₄ (1# , node k₂ t₁ t₃ ∼0) t₅ ∼-
  ≡
  (1# , node k₂ t₁ (node k₄ t₃ t₅ ∼-) ∼+)

clause₄′ k₄ k₂ t₁ t₃ t₅ = refl

not-okay′ : ∀ {l u h} k₄ k₂ (t₁ : Tree (const ℕ) _ _ _) t₃ t₅ →
  joinˡ⁺ {l = l} {u} {suc h} {h} {suc h}
    k₄ (1# , node k₂ t₁ t₃ ∼-) t₅ ∼-
    ≡
    (0# , node k₂ t₁ (node k₄ t₃ t₅ ∼0) ∼0)

not-okay′ k₄ k₂ t₁ t₃ t₅ = refl

okay′ :
  ∀ {l u h} k₆ k₂ (t₁ : Tree (const ℕ) _ _ _) k₄ t₃ t₅ t₇ b →
  joinˡ⁺ {l = l} {u} {suc (suc h)} {suc h} {suc (suc h)}
    k₆ (1# , node k₂ t₁ (node {hˡ = h} {suc h} {suc h} k₄ t₃ t₅ b) ∼+) t₇ ∼-
  ≡
  (0# , node k₄ (node k₂ t₁ t₃ (max∼ b)) (node k₆ t₅ t₇ (∼max b)) ∼0)

okay′ k₆ k₂ t₁ k₄ t₃ t₅ t₇ b = refl

Answer 1

为了让 Agda 能够减少您的表达式，您需要在 t₃ 上进行模式匹配

not-okay _ _ _ (leaf _) _ = refl
not-okay _ _ _ (node _ _ _ _) _ = refl

我对为什么需要这样做的理解如下：joinˡ⁺ 是在五个参数上归纳定义的。在每种情况下，您都需要为 Agda 指定所有这些参数以减少表达式（我的意思是，Agda 需要知道，对于所有这 5 个参数，当前给出了哪些构造函数）。

在您的not-okay 函数中，您考虑joinˡ⁺ {l = l} {u} {suc h} {h} {suc h} k₄ (1# , node k₂ t₁ t₃ ∼-) t₅ ∼- 的数量，在这种情况下，五个参数中的四个指定了构造函数（1#、node k₂ t₁ t₃ ∼-、∼- 和∼-），但不是t₃ 这是缺少的想法。

相反，在您的 okay 函数中，您会考虑已指定所有五个元素的数量 joinˡ⁺ {l = l} {u} {suc (suc h)} {suc h} {suc (suc h)} k₆ (1# , node k₂ t₁ (node {hˡ = h} {suc h} {suc h} k₄ t₃ t₅ b) ∼+) t₇ ∼-。