Agda函数定义过度展开问题咨询及bar符号含义解析

一、条件分支竖线|的含义 #

在Agda的模式匹配、with抽象和case表达式中，竖线|是划分不同分支匹配条件的分隔符：

• 在with抽象里，with后跟随需要求值的表达式（比如自然数比较n ≤? m），|后面是该表达式的可能结果模式，每个模式对应一段证明逻辑。例如：

  lemma : ∀ n m → n ≤ m → suc n ≤ suc m
  lemma n m p with n ≤? m
  ... | yes _ = ≤-step p
  ... | no _ = ⊥-elim (n≤m→¬¬n≤m p _)
  

  这里| yes _和| no _分别匹配n ≤? m返回的两种决策结果，你可以在对应分支中使用结果附带的证据（比如yes携带的n ≤ m证明）。
• 在普通模式匹配中，|也可分隔同一参数的不同模式分支，比如处理自然数的零和后继情况：

  plus-zero : ∀ n → n + 0 ≡ n
  plus-zero zero = refl
  plus-zero (suc n) | refl = cong suc (plus-zero n)
  

二、库函数意外展开的成因 #

自动展开问题本质由Agda的类型检查和化简机制导致：

1. 默认自动化简策略：Agda会自动展开可计算的递归函数定义（比如自然数比较_≤?_）。当类型检查器需要验证分支目标与上下文的一致性时，会递归展开函数定义直到完成匹配或验证，导致目标窗口出现大量底层递归细节。
2. 无抽象修饰的库函数：部分标准库函数未用abstract修饰，定义对类型检查器完全透明，Agda会随时展开这些定义进行类型推导。
3. 分支类型关联需求：当分支目标依赖于比较函数的返回值（比如Dec (n ≤ m)类型的证据），Agda需要展开函数定义确认证据与目标类型的一致性，进而触发不必要的展开。

三、自然数推理的更佳实践 #

针对自然数序关系证明，推荐以下实践：

• 优先使用标准库预制性质：直接调用Data.Nat.Properties中的引理，比如≤-trans（传递性）、≤-refl（自反性）、≤-step（后继保持序关系）等，这些引理大多经过抽象处理，不会轻易展开底层定义。
• 用rewrite简化目标：当需要用序关系或等式改写目标时，使用rewrite策略替代手动展开。例如，若有p : n ≤ m，可通过rewrite ≤-pred p将目标中的suc n ≤ suc m改写为n ≤ m，避免展开≤的递归定义。
• 拆分复杂引理：将大型证明拆分为多个小型辅助引理，每个引理聚焦单一性质，降低每个分支的复杂度，减少Agda的化简压力，降低意外展开概率。
• 封装自定义引理：自己编写的辅助引理或函数用abstract修饰，只暴露类型接口，隐藏实现细节，避免类型检查器自动展开。

四、缓解库函数意外展开的方法 #

针对自动展开问题，可通过以下方式缓解：

• 用abstract包裹关键定义：自定义的比较相关函数或引理，用abstract修饰后，Agda只会使用其类型信息检查，不会将实现细节展开到目标窗口。示例：

  abstract
    suc-≤-suc : ∀ n m → n ≤ m → suc n ≤ suc m
    suc-≤-suc n m p = ≤-step p
  

• 使用private隐藏内部实现：将不需要对外暴露的递归辅助函数标记为private，避免Agda在目标窗口展示这些函数的展开内容。
• 关闭自动化简（谨慎使用）：在文件顶部添加编译选项{-# OPTIONS --no-auto-inline #-}或{-# OPTIONS --no-normalize #-}关闭自动化简，注意这会增加类型检查耗时，仅在特定文件或代码段使用。
• 手动控制展开时机：不依赖自动化简，通过快捷键C-c C-n（normalize命令）按需查看函数展开结果，平时保持目标的抽象状态。
• 直接匹配决策类型模式：处理_≤?_的结果时，直接使用yes p和no p的模式，而非展开Dec类型的构造器（Yes P ⊎ No P），避免Agda进一步展开底层定义。

内容的提问来源于stack exchange，提问作者DoubleX