如何在 HOLCF 中证明列表的双重还原不会改变它

Question

这里写一个简单的HOL理论：

theory ToyList
  imports Main
begin

no_notation Nil ("[]") and Cons (infixr "#" 65) and append (infixr "@" 65)
hide_type list
hide_const rev

datatype 'a list = Nil ("[]") | Cons 'a "'a list" (infixr "#" 65)

primrec snoc :: "'a list => 'a => 'a list" (infixr "#>" 65)
  where
    "[] #> y = y # []" |
    "(x # xs) #> y = x # (xs #> y)"

primrec rev :: "'a list => 'a list"
  where
    "rev [] = []" |
    "rev (x # xs) = (rev xs) #> x"

lemma rev_snoc [simp]: "rev(xs #> y) = y # (rev xs)"
  apply(induct_tac xs)
  apply(auto)
done

theorem rev_rev [simp]: "rev(rev xs) = xs"
  apply(induct_tac xs)
  apply(auto)
done

end

snoc与cons相反。它将一个项目添加到列表的末尾。

我想通过 HOLCF 证明一个类似的引理。在第一阶段，我只考虑严格列表。我在 HOLCF 中声明了严格列表的域。我还声明了两个递归函数：

ssnoc - 将一个项目附加到列表的末尾
srev - 反转列表

前缀s表示"strict".

theory Test
  imports HOLCF
begin

domain 'a SList = SNil | SCons "'a" "'a SList"

fixrec ssnoc :: "'a SList → 'a → 'a SList"
  where
    "ssnoc ⋅ SNil ⋅ x = SCons ⋅ x ⋅ SNil" |
    "ssnoc ⋅ ⊥ ⋅ x = ⊥" |
    "x ≠ ⊥ ∧ xs ≠ ⊥ ⟹ ssnoc ⋅ (SCons ⋅ x ⋅ xs) ⋅ y = SCons ⋅ x ⋅ (ssnoc ⋅ xs ⋅ y)"

fixrec srev :: "'a SList → 'a SList"
  where
    "srev ⋅ ⊥ = ⊥" |
    "srev ⋅ SNil = SNil" |
    "x ≠ ⊥ ∧ xs ≠ ⊥ ⟹ srev ⋅ (SCons ⋅ x ⋅ xs) = ssnoc ⋅ (srev ⋅ xs) ⋅ x"

lemma srev_singleton [simp]:
  "srev ⋅ (SCons ⋅ a ⋅ SNil) = SCons ⋅ a ⋅ SNil"
  apply(induct)
  apply(simp_all)
done

lemma srev_ssnoc [simp]:
  "srev ⋅ (ssnoc ⋅ xs ⋅ a) = SCons ⋅ a ⋅ (srev ⋅ xs)"
  apply(induct xs)
  apply(simp_all)
done

lemma srev_srev [simp]:
  "srev ⋅ (srev ⋅ xs) = xs"
  apply(induct xs)
  apply(simp_all)
done

end

我试图证明列表的双重还原等于原始列表（srev_srev 引理）。我已经声明了两个辅助引理：

srev_singleton - 单例列表的反面是原始单例列表
srev_ssnoc - 列表的还原等于从原始列表的最后一项开始的列表追加原始列表其余项目的还原

但我无法证明任何引理。能指出错误吗？

还有为什么在函数定义中需要先决条件 "x ≠ ⊥ ∧ xs ≠ ⊥"？为什么我要明确声明 "srev ⋅ ⊥ = ⊥" 和 "ssnoc ⋅ ⊥ ⋅ x = ⊥"。我想在 HOLCF 中，如果任何参数未定义，则默认情况下函数是未定义的。

Answer 1

如果您打算将列表建模为 la Haskell（又名 "lazy lists"），那么您应该使用类似的东西：

domain 'a list = Nil ("[]") | Cons (lazy 'a) (lazy "'a list") (infix ":" 65)

（注意 Cons 的 "lazy" 注释）。那么你不需要对你的第三个等式的假设。例如，

fixrec append :: "'a list → 'a list → 'a list"
  where
    "append $ [] $ ys = ys"
  | "append $ (x : xs) $ ys = x : (append $ xs $ ys)"

你所谓的ssnoc和

fixrec reverse :: "'a list → 'a list"
  where
    "reverse $ [] = []"
  | "reverse $ (x : xs) = append $ xs $ (x : [])"

反向。

但是，由于这种类型的列表允许 "infinite" 值，因此您将无法证明 reverse $ (reverse $ xs) = xs 通常成立（因为它不成立）。这仅适用于可以归纳表征的有限列表。（例如，参见 https://arxiv.org/abs/1306.1340 以获得更详细的讨论。）

但是，如果您不想为惰性列表建模（即，真的不想在您的数据类型中使用 "lazy" 注释），那么如果没有这些假设，您的方程式可能不成立。现在，如果方程式具有这些假设，则它们只能应用于满足假设的情况。所以增益，你将无法证明（没有额外的假设）reverse $ (reverse $ xs) = xs。通过归纳谓词可能再次获得适当的假设，但我没有进一步调查。

更新： 在 HOLCF 中玩了一些严格列表之后，我还有一些评论：

首先，我的猜测是由于内部构造，fixrec 规范中的先决条件是必需的，但之后我们可以摆脱它们。

我设法证明了你的引理如下。为了完整起见，我给出了我的理论文件的全部内容。首先确保符号不会与现有符号冲突：

no_notation
  List.Nil ("[]") and
  Set.member ("op :") and
  Set.member ("(_/ : _)" [51, 51] 50)

然后定义严格列表的类型

domain 'a list = Nil ("[]") | Cons 'a "'a list" (infixr ":" 65)

和函数 snoc.

fixrec snoc :: "'a list → 'a → 'a list"
  where
    "snoc $ [] $ y = y : []"
  | "x ≠ ⊥ ⟹ xs ≠ ⊥ ⟹ snoc $ (x:xs) $ y = x : snoc $ xs $ y"

现在，我们通过以下方式获得第二个方程的无条件变体：

显示 snoc 在其第一个参数中是严格的（注意 fixrec_simp 的用法）。
显示 snoc 在其第二个参数中是严格的（这里需要归纳）。
最后，通过对所有三个变量的案例分析得到方程。

lemma snoc_bot1 [simp]: "snoc $ ⊥ $ y = ⊥" by fixrec_simp
lemma snoc_bot2 [simp]: "snoc $ xs $ ⊥ = ⊥" by (induct xs) simp_all
lemma snoc_Cons [simp]: "snoc $ (x:xs) $ y = x : snoc $ xs $ y"
  by (cases "x = ⊥"; cases "xs = ⊥"; cases "y = ⊥";simp)

然后函数reverse

fixrec reverse :: "'a list → 'a list"
  where
    "reverse $ [] = []"
  | "x ≠ ⊥ ⟹ xs ≠ ⊥ ⟹ reverse $ (x : xs) = snoc $ (reverse $ xs) $ x"

又是第二个等式的无条件变体：

lemma reverse_bot [simp]: "reverse $ ⊥ = ⊥" by fixrec_simp
lemma reverse_Cons [simp]: "reverse $ (x : xs) = snoc $ (reverse $ xs) $ x"
  by (cases "x = ⊥"; cases "xs = ⊥"; simp)

关于 reverse 和 snoc 的引理你还有：

lemma reverse_snoc [simp]: "reverse $ (snoc $ xs $ y) = y : reverse $ xs"
  by (induct xs) simp_all

最后是想要的引理：

lemma reverse_reverse [simp]:
  "reverse $ (reverse $ xs) = xs"
  by (induct xs) simp_all

我获得此解决方案的方法是查看失败尝试的剩余子目标，然后进行更多失败尝试，查看剩余子目标，重复，...

如何在 HOLCF 中证明列表的双重还原不会改变它

How to prove in HOLCF that double reversion of a list doesn't change it

isabelle