如何在Agda中证明依赖函数类型相等？具体场景求助

定义与已有证明 #

首先定义依赖类型函数：

WeirdType : (n : ℕ) → Set
WeirdType n with n + zero ≟ suc n
WeirdType n    | no ¬n+zero≡sucn = ℕ
WeirdType n    | yes n+zero≡sucn = ℕ → ℕ

已证明对任意自然数n，WeirdType n命题等于ℕ：

lemma : (n : ℕ) → ℕ ≡ WeirdType n
lemma n with n + zero ≟ suc n
lemma n    | no ¬n+zero≡sucn = refl
lemma n    | yes n+zero≡sucn =
    ⊥-elim
        (case
            trans (+-comm zero n) n+zero≡sucn
        of λ())

目标定理与错误尝试 #

需要证明的目标：

theorem : (ℕ → ℕ) ≡ ((n : ℕ) → WeirdType n)

尝试通过自定义类型转换函数结合cong证明：

TypeTransform : Set → Set
TypeTransform Type = (n : ℕ) → Type

theorem : (ℕ → ℕ) ≡ ((n : ℕ) → WeirdType n)
theorem = cong TypeTransform lemma

得到错误提示：

Cannot instantiate the metavariable _182 to solution
WeirdType n₁
| Relation.Nullary.Decidable.Core.map′ (≡ᵇ⇒≡ (n₁ + zero) (suc n₁))
(≡⇒≡ᵇ (n₁ + zero) (suc n₁))
(Data.Bool.Properties.T? (n₁ + zero ≡ᵇ suc n₁))
since it contains the variable n₁
which is not in scope of the metavariable
when checking that the inferred type of an application
TypeTransform ℕ ≡ TypeTransform _y_182
matches the expected type
(ℕ → ℕ) ≡ ((n₁ : ℕ) → WeirdType n₁)

参考案例 #

当定义更简单的WeirdType'时，Agda可直接用refl证明类似定理：

WeirdType' : (n : ℕ) → Set
WeirdType' n with suc n ≟ zero
WeirdType' n    | (no ¬sucn≡zero) = ℕ
WeirdType' n    | (yes sucn≡zero) = ℕ → ℕ

theorem' : (ℕ → ℕ) ≡ ((n : ℕ) → WeirdType' n)
theorem' = refl

解决方案 #

问题核心是：lemma是逐点的命题相等，而目标是依赖函数空间的命题相等，直接用cong无法处理带依赖参数的情况，需要借助函数外延性将逐点相等提升为函数层面的相等，再推导到依赖函数空间的相等。

步骤1：导入必要模块

open import Relation.Binary.PropositionalEquality
open import Function using (funext)

步骤2：构造证明

利用funext将lemma（每个n处ℕ ≡ WeirdType n）提升为常量函数(λ _ → ℕ)与WeirdType的相等，再通过cong将这个函数等式转换为依赖函数空间的相等：

theorem : (ℕ → ℕ) ≡ ((n : ℕ) → WeirdType n)
theorem = cong (λ F → (n : ℕ) → F n) (funext lemma)

原理说明

• funext lemma：将逐点的等式(n : ℕ) → ℕ ≡ WeirdType n转换为函数等式(λ _ → ℕ) ≡ WeirdType。
• cong (λ F → (n : ℕ) → F n)：对上述函数等式应用同余规则，得到依赖函数空间的等式((n : ℕ) → ℕ) ≡ ((n : ℕ) → WeirdType n)。
• 由于(n : ℕ) → ℕ与ℕ → ℕ是定义相等的，因此最终目标等式成立。

而WeirdType'可直接用refl证明，是因为suc n ≟ zero始终返回no，WeirdType' n定义上等于ℕ，因此依赖函数空间((n : ℕ) → WeirdType' n)定义上等于ℕ → ℕ，无需命题相等推导。

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