卡在证明上（建模 IMP 语言）

Question

我一直在尝试“移植”一些在 Isabelle 中形式化的命令式语言（IMP2）：https://www.isa-afp.org/sessions/imp2/#Semantics.html 到阿格达。

首先，以下是我为状态建模和变量名称+谓词所做的一些初始翻译，用于测试变量是本地变量还是全局变量：

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

我目前处于 Imp2 文档的这一部分： https://www.isa-afp.org/sessions/imp2/#Semantics.html

（特别是状态组合定义——我的版本在下面的 Agda 中显示）：

-- 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 
combine-collapse s = 
    begin
        < s ! s >
    ≡⟨⟩
       λ (n : vname) -> if is-local n then (s n) else (s n)  
    ≡⟨ ? ⟩
        ?    
    ∎

使用等式重写，我想我应该从 ≡ 的左侧开始，然后慢慢推导 s，但是当在第二步中展开 <!> 的定义时，类型检查器告诉我：

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

认为由于 ite 应用程序的主体是相同的，这将导致我只得到 s，但我陷入了状态是函数的事实。

关于我应该如何继续这个证明有什么指导吗？或者国家或其他职能的建模方式是否存在疏忽（或缺陷），导致无法证明这一点？

Answer 1

你无法证明函数的命题相等。您可以在您的上下文中得到的最接近的是：

combine-collapse : ∀ {s n} -> < s ! s > n ≡ s n 
combine-collapse {s} {n} with is-local n
... | false = refl
... | true = refl

然后你必须使用外延相等（当两个函数对于所有输入都一致时，它们是外延相等的）。

您可以在本文中了解有关外延相等的更多信息。