我想使用简化器来替换不相等的子项。我将通过一个示例来说明这个问题，而不是对我的问题进行一般定义:
假设我有一个简单的编程语言和一个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)(这两个是不同的程序)，但它确实认为它们在意义上是等价的，即denotation ((a;b);c)) = denotation (a;(b;c))。
这意味着，我应该能够将a;(b;c)重写为(a;b);c在Hoare三元组中。例如，我希望能够证明
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元组内部重写而重新实现整个简化器。
Isabelle的简化器不支持对任意等价关系的重写。幸运的是，您的重写看起来相当简单，因此在simproc中实现重写可能是值得的。思路如下:
编写一个simproc，以hoare P c Q的形式触发。在调用时，它设置一个形式为hoare P c Q == ?rhs和的目标应用一条规则，声明%c. hoare P c Q只关心其实参的等价类，而不关心具体元素。然后，将重写规则作为引入规则应用，直到所述目标得到解决。这应该已经将?rhs实例化为hoare P c' Q的形式。测试c和c'是否相等。如果是，则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，因此您可以假设调用中的命令已经是普通形式，而不是简单集。在您的示例中，测试%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，直到不再触发为止，因此您最终应该得到一个正常的形式。
如果你想支持条件重写规则，而不是表意等价，rule hoare_intros应该被替换为检查子目标格式的东西。如果不是fun_equiv denotation _ _的形式，那么simproc应该递归地调用简化器(或您选择的任何其他证明方法)，而不是尝试hoare_intros的另一个规则应用程序。
关于一种似乎可行的方法，请参阅附件中的Isabelle/HOL理论。这里的想法是使用条件简单规则来模拟长规则。
。，一个同余规则
lemma l1 [cong]: "f a = f b ==> g a = g b"
也是一个有效的条件简单规则
lemma l2 [simp]: "f a = f b ==> g a = g b"
，当Isabelle应用简化规则时，b将被一个原理图变量替换，简化器将重写"f a = f ?b"，它将用b的简化实例化?b。
然而，引理l2将使简化器循环，因为它可以应用于它自己的rhs。所以我们可以写一个规则
lemma l3 [simp]: "f_simp a = f_done b ==> g_simp a = g_done b"
其中g_simp和g_done被定义为等于g，但会阻止简化器在循环中应用规则。
这个想法的一个完整的工作示例在下面的理论文件。
问题是:-这是一个黑客。我不知道在什么情况下它会崩溃或者与其他东西不相容- apply simp可能部分重写，所以你必须再次调用它来完成重写。(见理论的最后一个引理)
theory Test
imports Main
begin
section "Minimal Hoare logic"
(* 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) *)
(* seq is associative modulo denotational equivalence.
Thus we should be able to rewrite "a;(b;c)" to "a;b;c"
within a hoare triple. E.g., the following should be solved with simp: *)
lemma
assumes "hoare P (while e (a;b;c)) Q"
shows "hoare P (while e (a;(b;c))) Q"
using assms
oops (* by simp *)
section "A failed attempt"
experiment begin
(* Here a natural approach first which, however, fails. *)
(* A congruence rule for the simplifier.
To rewrite a hoare triple "hoare P c Q",
we need to rewrite "denotation c". *)
lemma enter [cong]:
assumes "P==P'" and "Q==Q'"
assumes "denotation c == denotation c'"
shows "hoare P c Q == hoare P' c' Q'"
sorry
(* To descend further into subterms, we need a congruence-rule for while. *)
lemma while [cong]:
assumes "e=e'"
and "denotation c == denotation c'"
shows "denotation (while e c) ≡ denotation (while e' c')"
sorry
(* And we give a simplification rule for the associativity of seq *)
lemma assoc [simp]:
"denotation (a;(b;c)) = denotation (a;b;c)"
sorry
(* Now we can simplify the lemma from above *)
lemma
assumes "hoare P (while e (a;b;c)) Q"
shows "hoare P (while e (a;(b;c))) Q"
using assms by simp
(* Unfortunately, this does not work any more once we add more congruence rules. *)
(* To descend further into subterms, we need a congruence-rule for while. *)
lemma ifthen [cong]:
assumes "e=e'"
and "denotation c == denotation c'"
shows "denotation (ifthen e c) ≡ denotation (ifthen e' c')"
sorry
(* Warning: Overwriting congruence rule for "Test.denotation" *)
(* Simplifier doesn't work any more because the congruence rule for while was overwritten *)
lemma
assumes "hoare P (while e (a;b;c)) Q"
shows "hoare P (while e (a;(b;c))) Q"
using assms
oops (* by simp *)
end
section {* A working attempt *}
(* Define copies of the denotation-constant, to control the simplifier *)
definition "denotation_simp == denotation"
definition "denotation_done == denotation"
(* A congruence rule for the simplifier.
To rewrite a hoare triple "hoare P c Q",
we need to rewrite "denotation c".
This means, the congruence rule should have an assumption
"denotation c == denotation c'"
However, to avoid infinite loops with the rewrite rules below,
we use the logically equivalent assumption
"denotation_simp c == denotation_done c'"
This means that we need to configure the rules below rewrite
"denotation_simp c" into "denotation_done c'" where c' is
the simplication of c (module denotational equivalence).
*)
lemma enter [cong]:
assumes "P==P'" and "Q==Q'"
assumes "denotation_simp c == denotation_done c'"
shows "hoare P c Q == hoare P' c' Q'"
sorry
(* A similar congruence rule for simplifying expressions
of the form "denotation c". *)
lemma denot [cong]:
assumes "denotation_simp c == denotation_done c'"
shows "denotation c == denotation c'"
sorry
(* Now we add a congruence-rule for while.
Since we saw above that we cannot use several congruence-rules
with "denotation" as their head,
we simulate a congruence rule using a simp-rule.
To rewrite "denotation_simp (while e c)", we need to rewrite
"denotation_simp c".
We put denotation_done on the rhs instead of denotation_simp
to avoid infinite loops.
*)
lemma while [simp]:
assumes "e=e'"
and "denotation_simp c == denotation_done c'"
shows "denotation_simp (while e c) ≡ denotation_done (while e' c')"
sorry
(* A pseudo-congruence rule for ifthen *)
lemma ifthen [simp]:
assumes "e=e'"
and "denotation_simp c == denotation_done c'"
shows "denotation_simp (ifthen e c) == denotation_done (ifthen e' c')"
sorry
(* A pseudo-congruence rule for seq *)
lemma seq [simp]:
assumes "denotation_simp c == denotation_done c'"
and "denotation_simp d == denotation_done d'"
shows "denotation_simp (c;d) == denotation_done (c';d')"
sorry
(* Finally, we can state associativity of seq. *)
lemma assoc [simp]:
"denotation_simp (a;(b;c)) = denotation_simp (a;b;c)"
sorry
(* Finally, since our congruence-rules expect the rewriting to rewrite
"denotation_simp c" into "denotation_done c'",
we need to translate any non-rewritten "denotation_simp" into
"denotation_done".
However, a rule "denotation_simp c == denotation_done c" does not work,
because it could be triggered too early, and block the pseudo-congruence rules above.
So we only trigger the rule when the current term would not match
any of the pseudo congruence rules *)
lemma finish [simp]:
assumes "NO_MATCH (while e1 c1) a"
assumes "NO_MATCH (ifthen e2 c2) a"
assumes "NO_MATCH (c3;d3) a"
shows "denotation_simp a = denotation_done a"
sorry
(* Testing the simplifier rules *)
lemma
assumes "hoare P (while e (a;b;c)) Q"
shows "hoare P (while e (a;(b;c))) Q"
using assms
by simp
(* Some more complex test *)
lemma iftrue [simp]: "denotation_simp (ifthen (λm. True) c) == denotation_simp c" sorry
lemma
assumes "⋀x. Q x"
assumes "hoare (λm. P x ∧ Q x) (while P (c;(d;e);(f;g);c)) (λm. m=m)"
shows "hoare (λm. P x) (while P (c;(d;e);ifthen (λm. m=m) (f;g;c))) (λm. True)"
using assms
apply simp (* Hmm. Only partially simplified... The assoc rule is not applied to the result of the iftrue rule *)
by simp (* Rerunning simp solves the goal *)
(* By the way: "using assms by auto" solves the goal in one go *)
end
以下是我对Andreas Lochbihler建议的实施。第一部分是一个泛型实现(适用于除表意等价之外的其他等价)，下面是我的示例Hoare逻辑的实例化。
(* Written by Dominique Unruh *)
theory Test2
imports Main
begin
section "Implementation of modulo-simplifier"
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)
ML {*
(* Call as: hoare_simproc_tac (simplifications@congruences) context/simpset *)
fun fun_equiv_simproc_tac intros ctxt =
SUBGOAL (fn (goal,i) =>
case goal of
Const(@{const_name Trueprop},_) $ (Const(@{const_name fun_equiv},_)$_$_$_) =>
(resolve0_tac intros THEN_ALL_NEW fun_equiv_simproc_tac intros ctxt) i
ORELSE (rtac @{thm fun_equiv_refl} i)
| _ =>
SOLVED' (simp_tac ctxt) i)
fun fun_equiv_simproc start intros _ ctxt (t:cterm) =
let val fresh_var = Var(("x",Term.maxidx_of_term (Thm.term_of t)+1),Thm.typ_of_cterm t)
val goal = Logic.mk_equals (Thm.term_of t,fresh_var)
val thm = Goal.prove ctxt [] [] goal
(fn {context,...} => resolve0_tac start 1 THEN ALLGOALS (fun_equiv_simproc_tac intros context))
in
if (Thm.rhs_of thm) aconvc t then NONE else SOME thm
end
handle ERROR msg => (warning ("fun_equiv_simproc failednTerm was:n"^(@{make_string} t)^"nError: "^msg); NONE)
fun fun_equiv_simproc_named start cong simp morph ctxt =
fun_equiv_simproc (Named_Theorems.get ctxt start) (Named_Theorems.get ctxt simp @ Named_Theorems.get ctxt cong) morph ctxt
*}
section "Minimal Hoare logic"
(* A simple language and Hoare logic *)
typedecl program
typedecl memory
consts
seq :: "program ⇒ program ⇒ program" (infixl ";" 100) (* 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) *)
section "Instantiating the simplifier"
named_theorems denot_simp_start
named_theorems denot_simp
named_theorems denot_cong
lemma hoare_cong_start [denot_simp_start]: "fun_equiv denotation c c' ⟹ hoare P c Q == hoare P c' Q" sorry
lemma while_cong [denot_cong]: "fun_equiv denotation c c' ⟹ fun_equiv denotation (while b c) (while b c')" sorry
lemma seq_cong [denot_cong]: "fun_equiv denotation a a' ⟹ fun_equiv denotation b b' ⟹ fun_equiv denotation (a ; b) (a' ; b')" sorry
lemma if_cong [denot_cong]: "fun_equiv denotation c c' ⟹ fun_equiv denotation (ifthen b c) (ifthen b c')" sorry
lemma seq_assoc [denot_simp]: "fun_equiv denotation (a ; (b ; c)) (a; b; c)" sorry
lemma ifthen_true [denot_simp]: "(⋀m. e m) ⟹ fun_equiv denotation (ifthen e c) c" sorry
lemma double_while [denot_simp]: "(⋀m. e m = e' m) ⟹ fun_equiv denotation c d ⟹ fun_equiv denotation (seq (while e c) (while e' d)) (while e c)" sorry
(* -- "If the set of simplification theorems is fixed, we can use the following setup"
lemmas hoare_congruences = while_cong if_cong seq_cong
lemmas hoare_simps = ifthen_true seq_assoc double_while
simproc_setup hoare_simproc ("hoare P c Q") = {* fun_equiv_simproc @{thms hoare_cong_start} @{thms hoare_simps hoare_congruences} *}
*)
(* To make use of dynamic lists of theorems, we use the following setup *)
simproc_setup hoare_simproc ("hoare P c Q") = {*
fun_equiv_simproc_named @{named_theorems denot_simp_start}
@{named_theorems denot_cong}
@{named_theorems denot_simp}
*}
section "Tests"
(* Testing the simplifier rules *)
lemma
assumes "hoare P (while e (a;b;c)) Q"
shows "hoare P (while e (a;(b;c))) Q ∧ True"
using assms
by simp
lemma
assumes "hoare P (while P (c;d;e)) Q"
assumes "⋀x. P x = R x"
shows "hoare P ((while P (c;(d;e))); (while R ((c;d);e))) Q"
using assms by simp
lemma
assumes "⋀x. Q x"
assumes "hoare (λm. P x ∧ Q x) (while P (c;(d;e);(f;g);c)) (λm. m=m)"
shows "hoare (λm. P x) (while P (c;(d;e);ifthen (λm. m=m) (f;g;c))) (λm. True)"
using assms by simp
(* Test: Disabling the simproc *)
lemma
assumes "hoare P (a;(b;c)) Q"
shows "hoare P (a;(b;c)) Q ∧ True"
using[[simproc del: hoare_simproc]] -- "Without this, proof fails"
apply simp
by (fact assms)
end