卡在证明上(建模 IMP 语言)

问题描述 投票:0回答:1

我一直在尝试“移植”一些在 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,但我陷入了状态是函数的事实。

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

isabelle agda proof-assistant
1个回答
0
投票

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

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

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

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

© www.soinside.com 2019 - 2024. All rights reserved.