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

Question

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

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

基本上，我希望能够编写将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用户很少使用公理化。我已经与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。