如何在Isabelle中显示2个公式在语义上等效

Question

我想（怀念）使用Isabelle来说明两个给定的公式在语法上是等效的。例如A ? B = B ? A。

我不想对公式背后的逻辑进行任何详细说明。我不想A ? B在A和B都为真时也是如此。我只想在结构上比较这两个公式，并说由于可交换性，它们是等效的。

基本上，我希望能够编写将2个公式与某些相等函数进行比较的引理，并使用给定的引理，但是要指定它们，公理。

到目前为止，我认为可以并且应该使用来完成此操作axiomatization，但是这里的每个人都告诉我axiomatzation不好。

这使我想到了应该如何完成此任务的问题。2，说命题公式，如何在伊莎贝尔语中就其句法等效性进行比较。举一个具体的例子：

formula ? formula | formula ? formula

以运算符的形式给出，如果可能的话，以数据类型的形式给出

并distributive and commutative property作为规则给出。 A ? B = B ? A，如果在定理中陈述，则应该是可证明的。

那就是我想要做的，我希望这个主意很明确，并且有人可以向我解释如何在Isabelle中正确地做到这一点。提前致谢。

Answer 1

从您写的内容来看，我很确定您的意思是句法对等。如果两个公式对于变量的所有赋值都得出相同的结果，则它们在语义上是等效的。如果您可以在给定一组重写规则的情况下将一个公式重写为另一个公式，那么两个公式在语法上是等价的（或更广泛地说，可以使用一组特定的推理规则证明它们的等效性）。语义等价仅关注表达式的值，而不关注它们的结构。语法等价仅关注表达式的结构，而不关注它们产生的值。

现在，继续回答在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"

然后，您可以使用给定的变量评估来定义“评估”这样的公式的概念：

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并破坏了所有内容。使用归纳谓词包，这是不可能发生的，因为它会自动证明您的定义是一致的。（通过限制它们是单调的）

一个更实际的原因是，如您在上面看到的，您可以对归纳谓词进行归纳，即，如果您有两个语法上等价的公式，则可以对它们的语法对等的证明树进行归纳。特别是，您知道如果两个公式在语法上等价，则必须从您指定的规则中证明这一点。如果仅进行公理化处理，就没有这样的保证–可能存在更多语法上等效的公式；通过公理化，您甚至无法反驳类似的东西Atom 0 ? Atom 1，除非您也对公理化这样的东西，这将是非常丑陋的，并且很容易出现意外的不一致。

这是很对的伊莎贝尔用户使用公理化罕见。我已经与Isabelle合作多年，并且从未使用公理化。它的目的是建立基本的底层逻辑和大量的工作非常低级别的功能已投资于高层次的定义工具，如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用新鲜原子替换所有自由变量，然后确定这些公式的等价性（例如a and FFalse ? FFalse，确定等效项Atom 0 and FFalse ? FFalse）。