Isabelle中update函数的update_rec1引理验证咨询

已定义内容 #

类型定义 #

datatype mnat = mnat nat | MInfty

查找函数lookup定义 #

fun lookup :: "(nat×nat) ⇒ (nat×nat×mnat)list ⇒ mnat option"
  where "lookup (x,y) [] = None"|
        "lookup (x,y) ((a,b,c)#ps) = (if (a=x∧b=y) then Some c else lookup (x,y) ps)"

递归更新函数update及终止性证明 #

function update :: " (nat×nat×mnat)list ⇒nat⇒nat ⇒ nat ⇒ nat ⇒  (nat×nat×mnat)list "
  where "update t x y i j =(if i≤x∧length t<(x*y)∧length A+1≥(Suc i)∧x≥1∧y≥1 then 
                                    if (j≤y) then
                                      if (A!(i-1)=B!(j-1))  then update ((i,j,mnat_plus (opt_mnat(lookup (i-1,j-1) t)) (mnat 1))#t) x y i (Suc j)
                                                   else update ((i,j,mnat_max (opt_mnat(lookup (i,j-1) t)) (opt_mnat(lookup (i-1,j) t)))#t) x y i (Suc j)
                                              else update t x y (Suc i) 1
                                         else t
                                  )"
  by pat_completeness auto
termination 
  apply (relation "measure(λ(t,x,y,i,j). (x*y+length A-length t-i))")
     apply auto
  done
declare update.simps[simp del]

待验证引理 #

lemma update_rec1:
"snd(snd(hd(update [] x y 1 1))) = (if (A!(i-1)=B!(j-1)) then mnat_plus (snd(snd(hd(update [] (x-1) (y-1) 1 1)))) (mnat 1)
                                          else mnat_max (snd(snd(hd(update [] (x-1) y 1 1)))) (snd(snd(hd(update [] x (y-1) 1 1)))))"
if "1≤x∧x≤length A" "1≤y∧y≤length B"

验证思路 #

1. 拆解update执行逻辑

   • 初始调用update [] x y 1 1会从(i=1,j=1)开始遍历，按行优先顺序生成x*y个元素的列表，每次将新元素添加到列表头部，最终列表的第一个元素是最后处理的(x,y)位置元素，而非初始的(1,1)。
   • 每一步根据A!(i-1)与B!(j-1)是否相等，选择mnat_plus或mnat_max规则计算当前位置的mnat值，依赖已处理位置的结果（通过lookup从列表中获取）。

2. 修正引理的语法与逻辑错误

   • 引理中i,j是未绑定的自由变量，需替换为x,y（与左边(x,y)位置的元素对应）；
   • 若目标是(1,1)位置的元素，不能直接取hd，需用lookup (1,1) (update [] x y 1 1)获取。

3. 基础情况验证

   • 先手动模拟小实例：比如x=1,y=1、x=1,y=2、x=2,y=1，结合opt_mnat、mnat_plus、mnat_max的定义计算左右两边值，确认基础场景是否成立。

4. 归纳法证明

   • 以x+y或x*y为归纳变量，先证明基础场景（如x=1或y=1），再假设x-1,y和x,y-1的情况成立，推导x,y的情况。
   • 在Isabelle中临时恢复update.simps的化简规则（declare update.simps[simp add]），用simp、induct、rule等命令逐步展开递归，验证目标。

正确性判断建议 #

1. 检查语法与变量绑定

   • 引理中的自由变量i,j会导致陈述无意义，必须修正为与左边对应的x,y；当x=1或y=1时，右边的x-1或y-1不满足前提1≤x-1，会导致子调用update [] (x-1) ...直接返回空列表，hd []会触发异常，说明引理基础场景不成立。

2. 确认辅助函数定义

   • opt_mnat（将mnat option转为mnat）、mnat_plus、mnat_max的具体逻辑直接影响结果，比如opt_mnat None是MInfty还是mnat 0，mnat_plus对MInfty的处理规则，都会改变计算结果的正确性。

3. 验证输出结构匹配

   • 由于update将元素添加到列表头部，最终列表的顺序是逆序的（最后处理的元素在最前），若引理左边想表达(1,1)位置的元素，必须用lookup而非hd，否则逻辑完全错误。

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