将Isabelle的IMP2移植到Agda时的状态合并证明困境

问题背景 #

正在将Isabelle中形式化的命令式语言IMP2移植到Agda，已完成状态、变量名及全局/局部变量判断谓词的实现，代码如下：

vname : Set
vname = String

pname : Set -- procedure names 
pname = String 

is-global : vname -> Bool 
is-global name with (primStringToList name)
...    | []       = true
...    | (x ∷ xs) = primCharEquality x 'G' 

is-local : vname -> Bool 
is-local name = not (is-global name)

pval : Set 
pval = ℕ 

val : Set 
val = ℕ -> pval

-- *commands, boolean, and arith. expressions elided*

-- the state maps variable names to values 
State : Set 
State = vname -> val

状态合并操作的实现：

-- state combination
-- the state combination operator constructs a state by taking the local variables
-- from one state and the globals from another state

<_!_> : State -> State -> State
<_!_> s t = λ (n : vname) -> if (is-local n) then (s n) else (t n)

尝试证明定理combine-collapse : ∀ (s : State) -> < s ! s > ≡ s时，展开定义后类型检查器报错：

s n ≡ _z_90 !=< (ℕ → pval)
when checking that the inferred type of an application
s n ≡ _z_90
matches the expected type
ℕ → pval

原本以为if分支结果相同可直接推导出等于s，但因状态是函数类型陷入困境，需要解决证明问题或检查建模是否有误。

解决方案 #

核心原因：函数相等的证明规则 #

Agda中，函数类型（如State本质是vname → val）的相等必须通过外延性证明：两个函数相等当且仅当对所有输入，它们的输出完全一致。你直接展开后得到的是函数层面的等式，但未拆解到逐个输入的验证，导致类型不匹配。

步骤1：导入函数外延性支持 #

首先导入Agda标准库中的外延性模块，或直接假设外延性公理（构造主义下无法原生证明，需显式假设）：

open import Relation.Binary.PropositionalEquality
open import Function.Extensionality using (Extensionality)
open import Data.Bool.Base

-- 根据你的类型层级调整ℓ参数，这里用ℓ-zero适配Set层级
postulate ext : Extensionality ℓ-zero ℓ-zero

步骤2：完成定理证明 #

利用外延性将函数相等转化为“对任意变量n，< s ! s > n ≡ s n”，再分情况验证：

combine-collapse : ∀ (s : State) -> < s ! s > ≡ s
combine-collapse s = ext λ n →  -- 用外延性拆解为逐输入验证
  case is-local n of λ where
    true → refl  -- 局部变量分支：s n ≡ s n
    false → refl -- 全局变量分支：s n ≡ s n

也可以用with语句替代case，风格更贴近Agda传统写法：

combine-collapse : ∀ (s : State) -> < s ! s > ≡ s
combine-collapse s = ext λ n with is-local n
... | true = refl
... | false = refl

建模正确性验证 #

你的State建模是正确的，完全对齐IMP2中“状态映射变量到值”的定义，问题出在函数相等的证明逻辑，而非结构设计。

补充说明 #

• 函数外延性是Agda中的公理，因为构造主义逻辑无法推导函数的外延相等，必须显式引入。
• 所有函数类型的相等证明都遵循这个模式：先通过外延性拆解为逐输入的输出相等，再分别验证每个情况。

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