如何证明 2 个公式在 Isabelle 中语义等价
How to show that 2 formula sare semantically equivalent in Isabelle
我想（错过）使用 Isabelle 来证明两个给定的公式在句法上是等价的。例如 A ∧ B = B ∧ A.
我不想详细介绍公式背后的逻辑。当 A 和 B 都为真时，我不想关心 A ∧ B 是否为真。我只是想在结构层面上比较这两个公式，并说它们是等价的，因为交换律 属性。
基本上我希望能够编写引理来比较 2 个公式和一些等式函数，并使用给定的公理，但要指定公理。
到目前为止，我认为这可以而且应该使用 axiomatization 来完成，但这里的每个人都告诉我 axiomatzation 不好。
这让我想到了应该如何完成这项任务的问题。 2，比如说命题，公式如何在 Isabelle 中比较它们的句法等价性。举个具体的例子：
formula ∧ formula | formula ∨ formula
作为运算符给出，如果可能的话作为数据类型给出
和 distributive and commutative property 作为规则给出。
A ∧ B = B ∧ A，如果在定理中陈述应该是可证明的。
这就是我想要做的，我希望这个想法很清楚，并且有人可以向我解释如何在 Isabelle 中正确地追求这个。提前致谢。
根据您所写的内容，我很确定您指的是 语法等价。如果两个公式对所有变量赋值的计算结果相同，则它们语义等价；两个公式 在句法上是等价的 如果你可以在给定一组特定的重写规则的情况下将一个公式重写为另一个公式（或者，更一般地说，使用一组特定的推理规则证明它们的等价性）。语义等价只看表达式的值而不看它们的结构；句法等价只看表达式的结构，而不看它们产生的值。
现在，开始回答如何在 Isabelle 中执行此操作的问题。
定义关系
标准方法是为您的公式定义数据类型（我为它添加了一些更好的中缀语法）：
type_synonym vname = nat
datatype formula =
Atom vname
| FTrue
| Neg formula
| Conj formula formula (infixl "and" 60)
| Disj formula formula (infixl "or" 50)
definition "FFalse = Neg FTrue"
那么你可以定义‘求值’这样一个公式的概念w.r.t。一个给定的变量估值：
primrec eval_formula :: "(vname ⇒ bool) ⇒ formula ⇒ bool" where
"eval_formula s (Atom x) ⟷ s x"
| "eval_formula _ FTrue ⟷ True"
| "eval_formula s (Neg a) ⟷ ¬eval_formula s a"
| "eval_formula s (a and b) ⟷ eval_formula s a ∧ eval_formula s b"
| "eval_formula s (a or b) ⟷ eval_formula s a ∨ eval_formula s b"
lemma eval_formula_False [simp]: "eval_formula s FFalse = False"
by (simp add: FFalse_def)
并且，在此基础上，您可以定义语义等价的概念：如果两个公式对所有估值的计算结果相同，则它们在语义上是等价的：
definition formula_equiv_sem :: "formula ⇒ formula ⇒ bool" (infixl "≈" 40) where
"a ≈ b ⟷ (∀s. eval_formula s a = eval_formula s b)"
根据你的问题，我了解到你想要做的是根据重写规则定义某种等价关系：如果你可以转换一个公式，那么两个公式在语法上是等价的通过应用一组给定的重写规则进入另一个。
这可以做到，例如使用 Isabelle 的归纳谓词包：
inductive formula_equiv :: "formula ⇒ formula ⇒ bool" (infixl "∼" 40) where
formula_refl [simp]: "a ∼ a"
| formula_sym: "a ∼ b ⟹ b ∼ a"
| formula_trans [trans]: "a ∼ b ⟹ b ∼ c ⟹ a ∼ c"
| neg_cong: "a ∼ b ⟹ Neg a ∼ Neg b"
| conj_cong: "a1 ∼ b1 ⟹ a2 ∼ b2 ⟹ a1 and a2 ∼ b1 and b2"
| disj_cong: "a1 ∼ b1 ⟹ a2 ∼ b2 ⟹ a1 or a2 ∼ b1 or b2"
| conj_commute: "a and b ∼ b and a"
| disj_commute: "a or b ∼ b or a"
| conj_assoc: "(a and b) and c ∼ a and (b and c)"
| disj_assoc: "(a or b) or c ∼ a or (b or c)"
| disj_conj: "a or (b and c) ∼ (a or b) and (a or c)"
| conj_disj: "a and (b or c) ∼ (a and b) or (a and c)"
| de_morgan1: "Neg (a and b) ∼ Neg a or Neg b"
| de_morgan2: "Neg (a or b) ∼ Neg a and Neg b"
| neg_neg: "Neg (Neg a) ∼ a"
| tnd: "a or Neg a ∼ FTrue"
| contr: "a and Neg a ∼ FFalse"
| disj_idem: "a or a ∼ a"
| conj_idem: "a and a ∼ a"
| conj_True: "a and FTrue ∼ a"
| disj_True: "a or FTrue ∼ FTrue"
前六条规则本质上是设置重写（你可以自己重写任何东西，你可以从左到右或从右到左重写，你可以链接重写步骤，如果你可以重写子项，你也可以重写完整期限）。其余规则是您可能希望包含在其中的一些示例规则（没有完整性声明）。
有关归纳谓词的更多信息，请参阅谓词工具手册。
证明有关它的东西
那么你能用它做什么？好吧，我希望你会想要证明这是合理的，即两个在句法上等价的公式在语义上也是等价的：
lemma formula_equiv_syntactic_imp_semantic:
"a ∼ b ⟹ a ≈ b"
by (induction a b rule: formula_equiv.induct)
(auto simp: formula_equiv_sem_def)
您可能还想证明一些派生的句法规则。为此，有一些方便的传递性规则并使用同余规则设置简化器是有用的：
lemmas formula_congs [simp] = neg_cong conj_cong disj_cong
lemma formula_trans_cong1 [trans]:
"a ∼ f b ⟹ b ∼ c ⟹ (⋀x y. x ∼ y ⟹ f x ∼ f y) ⟹ a ∼ f c"
by (rule formula_trans) simp_all
lemma formula_trans_cong2 [trans]:
"a ∼ b ⟹ f b ∼ f c ⟹ (⋀x y. x ∼ y ⟹ f x ∼ f y) ⟹ f a ∼ f c"
by (rule formula_trans) simp_all
那么我们可以这样证明：
lemma conj_False: "a and FFalse ∼ FFalse"
proof -
have "a and FFalse ∼ Neg (Neg (a and FFalse))"
by (rule formula_sym, rule neg_neg)
also have "Neg (a and FFalse) ∼ Neg a or Neg FFalse"
by (rule de_morgan1)
also have "Neg FFalse ∼ FTrue" unfolding FFalse_def by (rule neg_neg)
also have "Neg a or FTrue ∼ FTrue" by (rule disj_True)
also have "Neg FTrue = FFalse" unfolding FFalse_def ..
finally show ?thesis by - simp
qed
lemma disj_False: "a or FFalse ∼ a"
proof -
have "a or FFalse ∼ Neg (Neg (a or FFalse))" by (rule formula_sym, rule neg_neg)
also have "Neg (a or FFalse) ∼ Neg a and Neg FFalse" by (rule de_morgan2)
also have "Neg FFalse ∼ FTrue" unfolding FFalse_def by (rule neg_neg)
also have "Neg a and FTrue ∼ Neg a" by (rule conj_True)
also have "Neg (Neg a) ∼ a" by (rule neg_neg)
finally show ?thesis by - simp
qed
当然，人们也想证明完整性，即任何两个语义等价的公式在句法上也是等价的。为此，我认为您将需要更多规则，然后证明非常复杂。
为什么不公理化？
您提到了公理化，您可能会问为什么建议您不要将其用于此目的。好吧，原因之一是公理化允许您在系统中引入不一致。你可能会“定义”两个东西是等价的，并且还在另一个地方定义其他东西，这意味着它们不等价，然后你得到了 False 并破坏了一切。使用 inductive predicate 包，这不会发生，因为它会自动证明您的定义是一致的。 （通过限制它们是单调的）
一个更实际的原因是，正如您在上面看到的，您可以对归纳谓词进行归纳，即如果您有两个语法等价的公式，您可以对它们的语法等价的证明树进行归纳.特别是，您知道如果两个公式在句法上是等价的，则必须根据您指定的规则证明这一点。如果你只是做公理化，你就没有这样的保证——可能有更多语法等价的公式；使用公理化，你甚至不能反驳像 Atom 0 ≈ Atom 1 这样的东西，除非你也公理化这样的东西，这将非常丑陋并且很容易出现意外的不一致。
Isabelle 用户非常很少使用公理化。多年来，我一直在与 Isabelle 一起工作，我从未使用过公理化。这是一个非常 low-level 的功能，旨在设置基本的底层逻辑，并且在 high-level 定义工具（如 typedef、datatype、fun 方面投入了大量工作, inductive, codatatype 等为用户提供定义界面，（希望）保证用户的一致性。
附录：决定语义等价
如果您对使用代码生成在公式上做有趣的事情感兴趣：我们甚至可以决定语义等价：我们可以简单地测试两个表达式的计算结果是否相同它们包含的变量集的结果。 （句法等价也是可能的，但更难，因为你必须得到归纳谓词包来为它编译可用的代码，我没能做到）
primrec vars :: "formula ⇒ vname list" where
"vars (Atom x) = [x]"
| "vars FTrue = []"
| "vars (Neg a) = vars a"
| "vars (Conj a b) = vars a @ vars b"
| "vars (Disj a b) = vars a @ vars b"
lemma eval_formula_cong:
"(⋀x. x ∈ set (vars a) ⟹ s x = s' x) ⟹ eval_formula s a = eval_formula s' a"
by (induction a) simp_all
primrec valuations :: "vname list ⇒ (vname ⇒ bool) list" where
"valuations [] = [λ_. False]"
| "valuations (x#xs) = [f' . f ← valuations xs, f' ← [f, fun_upd f x True]]"
lemma set_valuations: "set (valuations xs) = {f. ∀x. x∉set xs ⟶ f x = False}"
proof safe
case (goal2 f)
thus ?case
proof (induction xs arbitrary: f)
case (Cons x xs)
def f' ≡ "fun_upd f x False"
from Cons.prems have f': "f' ∈ set (valuations xs)"
by (intro Cons) (auto simp: f'_def)
show ?case
proof (cases "f x")
case False
hence "f' = f" by (intro ext) (simp add: f'_def)
with f' show ?thesis by auto
next
case True
hence "fun_upd f' x True = f" by (intro ext) (simp add: f'_def)
with f' show ?thesis by auto
qed
qed auto
qed (induction xs, auto)
lemma formula_equiv_sem_code [code]:
"a ≈ b ⟷ (∀s∈set (valuations (remdups (vars a @ vars b))).
eval_formula s a = eval_formula s b)"
unfolding formula_equiv_sem_def
proof (rule iffI; rule ballI allI)
case (goal2 s)
def s' ≡ "λx. if x ∈ set (vars a @ vars b) then s x else False"
have "s' ∈ set (valuations (remdups (vars a @ vars b)))"
by (subst set_valuations) (auto simp: s'_def)
with goal2 have "eval_formula s' a = eval_formula s' b" by blast
also have "eval_formula s' a = eval_formula s a"
by (intro eval_formula_cong) (auto simp: s'_def)
also have "eval_formula s' b = eval_formula s b"
by (intro eval_formula_cong) (auto simp: s'_def)
finally show ?case .
qed auto
我们现在可以简单地让 Isabelle 计算两个公式在语义上是否等价：
value "Atom 0 and Atom 1 ≈ Atom 1 and Atom 0" (* True *)
value "Atom 0 and Atom 1 ≈ Atom 1 or Atom 0" (* False *)
您甚至可以更进一步，编写一个自动证明方法，通过用新原子替换所有自由变量，然后确定等价性，为任何公式 a 和 b 确定 a ≈ b这些公式（例如，通过决定等效的 Atom 0 and FFalse ≈ FFalse 来决定 a and FFalse ≈ FFalse）。
我想（错过）使用 Isabelle 来证明两个给定的公式在句法上是等价的。例如 A ∧ B = B ∧ A.
我不想详细介绍公式背后的逻辑。当 A 和 B 都为真时，我不想关心 A ∧ B 是否为真。我只是想在结构层面上比较这两个公式，并说它们是等价的，因为交换律 属性。
基本上我希望能够编写引理来比较 2 个公式和一些等式函数，并使用给定的公理，但要指定公理。
到目前为止，我认为这可以而且应该使用 axiomatization 来完成，但这里的每个人都告诉我 axiomatzation 不好。
这让我想到了应该如何完成这项任务的问题。 2，比如说命题，公式如何在 Isabelle 中比较它们的句法等价性。举个具体的例子：
formula ∧ formula | formula ∨ formula
作为运算符给出，如果可能的话作为数据类型给出
和 distributive and commutative property 作为规则给出。
A ∧ B = B ∧ A，如果在定理中陈述应该是可证明的。
这就是我想要做的，我希望这个想法很清楚，并且有人可以向我解释如何在 Isabelle 中正确地追求这个。提前致谢。
根据您所写的内容，我很确定您指的是 语法等价。如果两个公式对所有变量赋值的计算结果相同，则它们语义等价；两个公式 在句法上是等价的 如果你可以在给定一组特定的重写规则的情况下将一个公式重写为另一个公式（或者，更一般地说，使用一组特定的推理规则证明它们的等价性）。语义等价只看表达式的值而不看它们的结构；句法等价只看表达式的结构，而不看它们产生的值。
现在，开始回答如何在 Isabelle 中执行此操作的问题。
定义关系
标准方法是为您的公式定义数据类型（我为它添加了一些更好的中缀语法）：
type_synonym vname = nat
datatype formula =
Atom vname
| FTrue
| Neg formula
| Conj formula formula (infixl "and" 60)
| Disj formula formula (infixl "or" 50)
definition "FFalse = Neg FTrue"
那么你可以定义‘求值’这样一个公式的概念w.r.t。一个给定的变量估值：
primrec eval_formula :: "(vname ⇒ bool) ⇒ formula ⇒ bool" where
"eval_formula s (Atom x) ⟷ s x"
| "eval_formula _ FTrue ⟷ True"
| "eval_formula s (Neg a) ⟷ ¬eval_formula s a"
| "eval_formula s (a and b) ⟷ eval_formula s a ∧ eval_formula s b"
| "eval_formula s (a or b) ⟷ eval_formula s a ∨ eval_formula s b"
lemma eval_formula_False [simp]: "eval_formula s FFalse = False"
by (simp add: FFalse_def)
并且，在此基础上，您可以定义语义等价的概念：如果两个公式对所有估值的计算结果相同，则它们在语义上是等价的：
definition formula_equiv_sem :: "formula ⇒ formula ⇒ bool" (infixl "≈" 40) where
"a ≈ b ⟷ (∀s. eval_formula s a = eval_formula s b)"
根据你的问题，我了解到你想要做的是根据重写规则定义某种等价关系：如果你可以转换一个公式，那么两个公式在语法上是等价的通过应用一组给定的重写规则进入另一个。
这可以做到，例如使用 Isabelle 的归纳谓词包：
inductive formula_equiv :: "formula ⇒ formula ⇒ bool" (infixl "∼" 40) where
formula_refl [simp]: "a ∼ a"
| formula_sym: "a ∼ b ⟹ b ∼ a"
| formula_trans [trans]: "a ∼ b ⟹ b ∼ c ⟹ a ∼ c"
| neg_cong: "a ∼ b ⟹ Neg a ∼ Neg b"
| conj_cong: "a1 ∼ b1 ⟹ a2 ∼ b2 ⟹ a1 and a2 ∼ b1 and b2"
| disj_cong: "a1 ∼ b1 ⟹ a2 ∼ b2 ⟹ a1 or a2 ∼ b1 or b2"
| conj_commute: "a and b ∼ b and a"
| disj_commute: "a or b ∼ b or a"
| conj_assoc: "(a and b) and c ∼ a and (b and c)"
| disj_assoc: "(a or b) or c ∼ a or (b or c)"
| disj_conj: "a or (b and c) ∼ (a or b) and (a or c)"
| conj_disj: "a and (b or c) ∼ (a and b) or (a and c)"
| de_morgan1: "Neg (a and b) ∼ Neg a or Neg b"
| de_morgan2: "Neg (a or b) ∼ Neg a and Neg b"
| neg_neg: "Neg (Neg a) ∼ a"
| tnd: "a or Neg a ∼ FTrue"
| contr: "a and Neg a ∼ FFalse"
| disj_idem: "a or a ∼ a"
| conj_idem: "a and a ∼ a"
| conj_True: "a and FTrue ∼ a"
| disj_True: "a or FTrue ∼ FTrue"
前六条规则本质上是设置重写（你可以自己重写任何东西，你可以从左到右或从右到左重写，你可以链接重写步骤，如果你可以重写子项，你也可以重写完整期限）。其余规则是您可能希望包含在其中的一些示例规则（没有完整性声明）。
有关归纳谓词的更多信息，请参阅谓词工具手册。
证明有关它的东西
那么你能用它做什么？好吧，我希望你会想要证明这是合理的，即两个在句法上等价的公式在语义上也是等价的：
lemma formula_equiv_syntactic_imp_semantic:
"a ∼ b ⟹ a ≈ b"
by (induction a b rule: formula_equiv.induct)
(auto simp: formula_equiv_sem_def)
您可能还想证明一些派生的句法规则。为此，有一些方便的传递性规则并使用同余规则设置简化器是有用的：
lemmas formula_congs [simp] = neg_cong conj_cong disj_cong
lemma formula_trans_cong1 [trans]:
"a ∼ f b ⟹ b ∼ c ⟹ (⋀x y. x ∼ y ⟹ f x ∼ f y) ⟹ a ∼ f c"
by (rule formula_trans) simp_all
lemma formula_trans_cong2 [trans]:
"a ∼ b ⟹ f b ∼ f c ⟹ (⋀x y. x ∼ y ⟹ f x ∼ f y) ⟹ f a ∼ f c"
by (rule formula_trans) simp_all
那么我们可以这样证明：
lemma conj_False: "a and FFalse ∼ FFalse"
proof -
have "a and FFalse ∼ Neg (Neg (a and FFalse))"
by (rule formula_sym, rule neg_neg)
also have "Neg (a and FFalse) ∼ Neg a or Neg FFalse"
by (rule de_morgan1)
also have "Neg FFalse ∼ FTrue" unfolding FFalse_def by (rule neg_neg)
also have "Neg a or FTrue ∼ FTrue" by (rule disj_True)
also have "Neg FTrue = FFalse" unfolding FFalse_def ..
finally show ?thesis by - simp
qed
lemma disj_False: "a or FFalse ∼ a"
proof -
have "a or FFalse ∼ Neg (Neg (a or FFalse))" by (rule formula_sym, rule neg_neg)
also have "Neg (a or FFalse) ∼ Neg a and Neg FFalse" by (rule de_morgan2)
also have "Neg FFalse ∼ FTrue" unfolding FFalse_def by (rule neg_neg)
also have "Neg a and FTrue ∼ Neg a" by (rule conj_True)
also have "Neg (Neg a) ∼ a" by (rule neg_neg)
finally show ?thesis by - simp
qed
当然，人们也想证明完整性，即任何两个语义等价的公式在句法上也是等价的。为此，我认为您将需要更多规则，然后证明非常复杂。
为什么不公理化？
您提到了公理化，您可能会问为什么建议您不要将其用于此目的。好吧，原因之一是公理化允许您在系统中引入不一致。你可能会“定义”两个东西是等价的，并且还在另一个地方定义其他东西，这意味着它们不等价，然后你得到了 False 并破坏了一切。使用 inductive predicate 包，这不会发生，因为它会自动证明您的定义是一致的。 （通过限制它们是单调的）
一个更实际的原因是，正如您在上面看到的，您可以对归纳谓词进行归纳，即如果您有两个语法等价的公式，您可以对它们的语法等价的证明树进行归纳.特别是，您知道如果两个公式在句法上是等价的，则必须根据您指定的规则证明这一点。如果你只是做公理化，你就没有这样的保证——可能有更多语法等价的公式；使用公理化，你甚至不能反驳像 Atom 0 ≈ Atom 1 这样的东西，除非你也公理化这样的东西，这将非常丑陋并且很容易出现意外的不一致。
Isabelle 用户非常很少使用公理化。多年来，我一直在与 Isabelle 一起工作，我从未使用过公理化。这是一个非常 low-level 的功能，旨在设置基本的底层逻辑，并且在 high-level 定义工具（如 typedef、datatype、fun 方面投入了大量工作, inductive, codatatype 等为用户提供定义界面，（希望）保证用户的一致性。
附录：决定语义等价
如果您对使用代码生成在公式上做有趣的事情感兴趣：我们甚至可以决定语义等价：我们可以简单地测试两个表达式的计算结果是否相同它们包含的变量集的结果。 （句法等价也是可能的，但更难，因为你必须得到归纳谓词包来为它编译可用的代码，我没能做到）
primrec vars :: "formula ⇒ vname list" where
"vars (Atom x) = [x]"
| "vars FTrue = []"
| "vars (Neg a) = vars a"
| "vars (Conj a b) = vars a @ vars b"
| "vars (Disj a b) = vars a @ vars b"
lemma eval_formula_cong:
"(⋀x. x ∈ set (vars a) ⟹ s x = s' x) ⟹ eval_formula s a = eval_formula s' a"
by (induction a) simp_all
primrec valuations :: "vname list ⇒ (vname ⇒ bool) list" where
"valuations [] = [λ_. False]"
| "valuations (x#xs) = [f' . f ← valuations xs, f' ← [f, fun_upd f x True]]"
lemma set_valuations: "set (valuations xs) = {f. ∀x. x∉set xs ⟶ f x = False}"
proof safe
case (goal2 f)
thus ?case
proof (induction xs arbitrary: f)
case (Cons x xs)
def f' ≡ "fun_upd f x False"
from Cons.prems have f': "f' ∈ set (valuations xs)"
by (intro Cons) (auto simp: f'_def)
show ?case
proof (cases "f x")
case False
hence "f' = f" by (intro ext) (simp add: f'_def)
with f' show ?thesis by auto
next
case True
hence "fun_upd f' x True = f" by (intro ext) (simp add: f'_def)
with f' show ?thesis by auto
qed
qed auto
qed (induction xs, auto)
lemma formula_equiv_sem_code [code]:
"a ≈ b ⟷ (∀s∈set (valuations (remdups (vars a @ vars b))).
eval_formula s a = eval_formula s b)"
unfolding formula_equiv_sem_def
proof (rule iffI; rule ballI allI)
case (goal2 s)
def s' ≡ "λx. if x ∈ set (vars a @ vars b) then s x else False"
have "s' ∈ set (valuations (remdups (vars a @ vars b)))"
by (subst set_valuations) (auto simp: s'_def)
with goal2 have "eval_formula s' a = eval_formula s' b" by blast
also have "eval_formula s' a = eval_formula s a"
by (intro eval_formula_cong) (auto simp: s'_def)
also have "eval_formula s' b = eval_formula s b"
by (intro eval_formula_cong) (auto simp: s'_def)
finally show ?case .
qed auto
我们现在可以简单地让 Isabelle 计算两个公式在语义上是否等价：
value "Atom 0 and Atom 1 ≈ Atom 1 and Atom 0" (* True *)
value "Atom 0 and Atom 1 ≈ Atom 1 or Atom 0" (* False *)
您甚至可以更进一步，编写一个自动证明方法，通过用新原子替换所有自由变量，然后确定等价性，为任何公式 a 和 b 确定 a ≈ b这些公式（例如，通过决定等效的 Atom 0 and FFalse ≈ FFalse 来决定 a and FFalse ≈ FFalse）。