如何证明加倍函数的反转等于 Isabelle 中反转函数的加倍？

Posted 2023-03-28

【中文标题】如何证明加倍函数的反转等于 Isabelle 中反转函数的加倍？

【英文标题】：How to prove the reversion of a doubling function equals the doubling of a reversion function in Isabelle?

【发布时间】：2014-10-19 20:23:42

【问题描述】：

我有一个函数可以将表单中列表的元素加倍

double [x1, x2, ...] = [x1, x1, x2, x2, ...]

即

 fun double :: " 'a list ⇒ 'a list"
 where
   "double [] = []" |
   "double (x#xs) = x # x # double xs"

以及一个在另一个函数snoc 的帮助下反转列表元素的函数，该函数将一个元素添加到列表的右侧：

 fun snoc :: "'a list ⇒ 'a ⇒ 'a list"
 where
   "snoc [] x = [x]" |
   "snoc (y # ys) x = y # (snoc ys x)"


 fun reverse :: "'a list ⇒ 'a list"
 where
   "reverse [] = []" |
   "reverse (x # xs) = snoc (reverse xs) x"

现在我要证明这一点

 lemma rev_double: "rev (double xs) = double (rev xs)"

是真的。

我尝试对xs应用归纳

lemma rev_double: "rev (double xs) = double (rev xs)"
by (induction xs)

我写了一个辅助引理double_snoc，它确保将列表加倍与将其第一个元素和列表的其余部分加倍相同（它使用函数snocleft，它在a的左端插入一个元素列表）

fun snocleft::"'a list ⇒ 'a  ⇒ 'a list "
where
  "snocleft [] x = [x]" |
  "snocleft (y # ys) x =  x # (y # ys)"


lemma double_snoc: "double (snocleft xs y) = y # y # double xs"
by (induction xs) auto

我在证明引理方面还没有取得任何进展。您对如何设置证明有一些解决方案或提示吗？

【问题讨论】：

顺便说一句：您的 snocleft 基本上只是列表缺点（即，在 Isabelle/HOL 中的 op #）与参数交换。此外，由于没有进行递归，fun 有点矫枉过正。你可以使用定义definition "snocleft ys y = y # ys"（这很明显你的引理可以是double (x # xs) = x # x # double xs，它直接来自double的定义）。

【参考方案1】：

您将函数定义为reverse，但在所有引理中，您使用rev，指的是预定义的列表反转函数rev。

你的意思大概是这样的：

lemma reverse_double: "reverse (double xs) = double (reverse xs)"

如果您尝试通过归纳来证明这一点（使用apply (induction xs)），您将陷入归纳案例，目标如下：

snoc (snoc (double (reverse xs)) a) a =
   double (snoc (reverse xs) a)

这应该很直观：如果你先snoc 然后加倍，它与第一次加倍然后snoc-ing 两次是一样的。所以让我们证明这是一个辅助引理：

lemma double_snoc: "double (snoc xs x) = snoc (snoc (double xs) x) x"
  by (induction xs) auto

现在reverse_double的证明自动通过了：

lemma reverse_double: "reverse (double xs) = double (reverse xs)"
  by (induction xs) (auto simp: double_snoc)