isabelle - 使用 Isabelle 简化器重写非相等等价关系

Question

我想用简化词来替换不等式的子项。我将通过一个示例来说明这一点，而不是对我的问题进行通用定义:

假设我有一个简单的编程语言和一个基于它的 Hoare 逻辑。假设我们有 if、while 和序列操作。此外，我们还有 denotation 和 hoare P c Q。以下是 Isabelle/HOL 中的示例签名:

(* A simple language and Hoare logic *)
typedecl program
typedecl memory
consts
  seq :: "program ⇒ program ⇒ program" (infixl ";" 10) (* c;d: run c, then run d *)
  ifthen :: "(memory ⇒ bool) ⇒ program ⇒ program" (* ifthen e c: run c if e(current_mem)=true *)
  while :: "(memory ⇒ bool) ⇒ program ⇒ program" (* while e c: run c while e(current_mem)=true *)
  denotation :: "program ⇒ memory ⇒ memory"  (* denotation c m: memory after running c, when starting with memory m *)
  hoare :: "(memory ⇒ bool) ⇒ program ⇒ (memory ⇒ bool) ⇒ bool" 
      (* hoare P c Q: if P(current_mem), then after running c, we have Q(current_mem) *)

现在 (a;b);c = a;(b;c) 是不正确的(这些是不同的程序)，但它确实认为它们在指称上是等价的，即， 表示 ((a;b);c)) = 表示 (a;(b;c))。

这意味着，我应该能够在 Hoare 三元组中将 a;(b;c) 重写为 (a;b);c。例如，我希望能够证明

lemma "hoare P (while e (a;b;c)) Q ==> hoare P (while e (a;(b;c))) Q"

只需使用简化器(by simp)，给定合适的简化规则。

从逻辑上讲，相关规则是:

lemma "denotation (a;(b;c)) = denotation ((a;b);c)"
lemma "denotation a = denotation b ==> hoare P a Q = hoare P b Q"
lemma "denotation a = denotation b ==> denotation (while e a) = denotation (while e b)"
lemma "denotation a = denotation b ==> denotation (ifthen e a) = denotation (ifthen e b)"
lemma "denotation a = denotation a' ==> denotation b = denotation b' ==> denotation (a;b) = denotation (a';b')"

不幸的是，似乎没有直接的方法可以将这些规则告诉简化器。 (更一般地，我们想告诉同余规则中的简化器，下面的重写必须完成模块某个等价关系，在本例中为指称等价。)

我已经找到了这个问题的部分解决方案(见下面我自己的答案)，但这个解决方案似乎是一个 hack(我不知道它有多稳定)，我想知道是否有一个好的方法做吧。

我不介意在此过程中必须使用一些 ML 代码(例如，编写 simproc)，但我想避免必须重新实现整个简化器以在 Hoare 元组中重写。

Answer 1

Isabelle 的简化器不支持关于任意等价关系的重写。幸运的是，您的重写看起来相当简单，因此在 simproc 中实现重写可能是值得的。这是想法:

写一个 simproc 以 hoare P c Q 的形式触发.调用时，它会设置一个 hoare P c Q == ?rhs 形式的目标。和应用一条规则说明 %c. hoare P c Q只关心其参数的等价类，而不关心具体元素。然后，应用重写规则作为引入规则，直到解决既定目标。这应该已经实例化了 ?rhs形式为 hoare P c' Q 的东西.测试是否c和 c'是 alpha-beta-eta-...-等价的。如果是这样，则 simproc 失败并返回 NONE。 , 否则返回证明方程。

这是我将用作开始的一堆引理:

definition fun_equiv :: "('a ⇒ 'b) ⇒ 'a ⇒ 'a ⇒ bool"
where "fun_equiv f x y ⟷ f x = f y"

lemma fun_equiv_refl: "fun_equiv f x x" by(simp add: fun_equiv_def)

lemma hoare_cong_start: (* start rule *)
  "fun_equiv denotation c c' ⟹ hoare P c Q == hoare P' c' Q'"
sorry

lemma while_cong: "fun_equiv denotation c c' ⟹ fun_equiv denotation (while b c) (while b c')" sorry

lemma seq_cong: "⟦ fun_equiv denotation a a'; fun_equiv denotation b b' ⟧ ⟹ fun_equiv denotation (a ; b) (a' ; b')" sorry

lemma if_cong: "fun_equiv denotation c c' ⟹ fun_equiv denotation (ifthen b c) (ifthen b c')" sorry

lemma seq_assoc: "fun_equiv denotation (a ; (b ; c)) (a; b; c)" sorry

lemma ifthen_true: "fun_equiv denotation (ifthen (λm. True) c) c" sorry

lemmas hoare_intros =
  -- ‹rewrites come first, congruences later, reflexivity last›
  ifthen_true seq_assoc
  while_cong if_cong seq_cong
  fun_equiv_refl

由于这是简化器内部的 simproc，您可以假设调用中的命令已经是正常形式 w.r.t。简单集。在您的示例中，测试 %m. m = m已经简化为%_. True .因此，simproc 可以专注于实现 hoare 规则的重写。

simproc 调用的单个步骤应该执行类似于以下 Isar 代码段的操作:

schematic_lemma "hoare (λm. P x) (while P (c;(d;e);ifthen (λm. True) (f;g;c))) (λm. True) == ?c"
by(rule hoare_cong_start)(rule hoare_intros)+

由于化简器会迭代 simproc 直到它不再触发，所以您应该真正以正常形式结束。

如果你想支持条件重写规则 w.r.t.指称等价，rule hoare_intros应该替换为检查子目标格式的内容。如果它不是 fun_equiv denotation _ _ 的形式，那么 simproc 应该递归地调用简化器(或您选择的任何其他证明方法)，而不是尝试 hoare_intros 的另一个规则应用程序.