如何使用 Isar 证明消除规则？

Posted 2023-03-28

【中文标题】如何使用 Isar 证明消除规则？

【英文标题】：How to prove elimination rules using Isar?

【发布时间】：2018-12-13 06:37:10

【问题描述】：

这是一个简单的理论：

datatype t1 = A | B | C
datatype t2 = D | E t1 | F | G

inductive R where
  "R A B"
| "R B C"

inductive_cases [elim]: "R x B" "R x A" "R x C"

inductive S where
  "S D (E _)"
| "R x y ⟹ S (E x) (E y)"

inductive_cases [elim]: "S x D" "S x (E y)"

我可以使用两个辅助引理证明引理elim：

lemma tranclp_S_x_E:
  "S⇧+⇧+ x (E y) ⟹ x = D ∨ (∃z. x = E z)"
  by (induct rule: converse_tranclp_induct; auto)

(* Let's assume that it's proven *)
lemma reflect_tranclp_E:
  "S⇧+⇧+ (E x) (E y) ⟹ R⇧+⇧+ x y"
  sorry

lemma elim:
  "S⇧+⇧+ x (E y) ⟹
   (x = D ⟹ P) ⟹ (⋀z. x = E z ⟹ R⇧+⇧+ z y ⟹ P) ⟹ P"
  using reflect_tranclp_E tranclp_S_x_E by blast

我需要使用 Isar 证明 elim：

lemma elim:
  assumes "S⇧+⇧+ x (E y)"
    shows "(x = D ⟹ P) ⟹ (⋀z. x = E z ⟹ R⇧+⇧+ z y ⟹ P) ⟹ P"
proof -
  assume "S⇧+⇧+ x (E y)"
  then obtain z where "x = D ∨ x = E z"
    by (induct rule: converse_tranclp_induct; auto)
  also have "S⇧+⇧+ (E z) (E y) ⟹ R⇧+⇧+ z y"
    sorry
  finally show ?thesis

但我收到以下错误：

No matching trans rules for calculation:
    x = D ∨ x = E z
    S⇧+⇧+ (E z) (E y) ⟹ R⇧+⇧+ z y

Failed to refine any pending goal 
Local statement fails to refine any pending goal
Failed attempt to solve goal by exported rule:
  (S⇧+⇧+ x (E y)) ⟹ P

如何解决？

我想这个引理可以有一个更简单的证明。但我需要分两步来证明：

显示x 的可能值 表明E 反映了传递闭包

我还认为这个引理可以通过x 上的案例来证明。但是我的真实数据类型有太多的案例。所以，这不是一个首选的解决方案。

【参考方案1】：

这个变种似乎有效：

lemma elim:
  assumes "S⇧+⇧+ x (E y)"
      and "x = D ⟹ P"
      and "⋀z. x = E z ⟹ R⇧+⇧+ z y ⟹ P"
    shows "P"
proof -
  have "S⇧+⇧+ x (E y)" by (simp add: assms(1))
  then obtain z where "x = D ∨ x = E z"
    by (induct rule: converse_tranclp_induct; auto)
  moreover
  have "S⇧+⇧+ (E z) (E y) ⟹ R⇧+⇧+ z y"
    sorry
  ultimately show ?thesis
    using assms by auto
qed

假设应该与目标分开。 作为第一条语句，我应该使用have 而不是assume。这不是一个新的假设，只是现有的假设。 我应该使用ultimately 而不是finally。貌似后者的应用逻辑更简单。

【讨论】：

also/finally 用于将传递的东西链接在一起；例如have "A = B", also have "B = C", finally have "A = C"。如果您只想收集几个事实，然后将它们全部用于显示最终结果，请使用moreover/ultimately。您收到的错误消息表明 also/finally 在您的目标语句中找不到任何可传递的链接。