时间戳

首页 > 解决方案 > 如何在归纳中引用变量

isabelle - 如何在归纳中引用变量

问题描述

我有一个与列表匹配的函数：

fun merge where
  ‹merge [] [] = []› |
  ‹merge (v#vs) [] = (v#vs)› |
  ‹merge [] (v#vs) = (v#vs)› |
  ‹merge (x#xs) (y#ys) =
    (if x < y then x # merge xs (y#ys) else y # merge (x#xs) ys)›

当我试图证明这一点的正确性时，我在基于此的归纳方面遇到了困难：

...
lemma sorted_merge: 
  assumes s_xs: "sorted(xs)"
    and   s_ys: "sorted(ys)"
  shows ‹sorted(merge xs ys)›  
proof (induction xs ys rule: merge.induct [case_names base xs ys both])
  case base then show "?case" by auto
next
  case xs
  show "?case" 
  proof -

问题是我可以证明这种情况，sorted(merge xs [])但这并不能满足sorted(merge (v#vs) [])证明目标。

因此，我如何固定xs为v#vs，或以其他方式引用xs针对此特定案例分析的案例？

标签： isabelle

解决方案

因此，我如何将 xs 固定为v#vs，或者以其他方式引用xs针对此特定案例分析的案例？

Isabelle2020 (Isar-ref) 的参考手册第 6.5 节对此进行了解释：

...通过使用显式形式case (c y1 ... ym)...证明作者能够选择非常适合当前上下文的本地名称...

因此，在您的情况下，您可以使用类似于

fun merge where
  ‹merge [] [] = []› 
| ‹merge (v#vs) [] = (v#vs)› 
| ‹merge [] (v#vs) = (v#vs)› 
| ‹merge (x#xs) (y#ys) = 
    (if x < y then x # merge xs (y#ys) else y # merge (x#xs) ys)›

lemma sorted_merge:
  assumes s_xs: "sorted(xs)" and s_ys: "sorted(ys)"
  shows ‹sorted(merge xs ys)›  
  using assms
proof(induction xs ys rule: merge.induct[case_names base xs ys both])
  case base then show ?case by auto
next
  case (xs v vs) then show ?case by auto
next
  case (ys v vs) then show ?case by auto
next
  case (both x xs y ys)
  show ?case 
  proof(cases ‹x < y›)
    case True with both(1,3,4) show ?thesis by (induction xs) force+
  next
    case False with both(2,3,4) show ?thesis by (induction ys) force+
  qed      
qed

伊莎贝尔版本：伊莎贝尔2020

推荐阅读