Isabelle 中的脆弱规则应用

如何解决Isabelle 中的脆弱规则应用

我正在玩 Isabelle/HOL 教程中的一个示例，以更好地理解 Isar 和 Tactics 证明之间的对应关系。

这是一个有效的版本：

lemma rtrancl_converseD: "(x,y) ∈ (r ^-1 )^* ⟹ (y,x) ∈ r^* "
proof (induct y rule: rtrancl_induct)
  case base
  then show ?case ..
next case (step y z)
  then have "(z,y) ∈ r" using rtrancl_converseD by simp 
  with `(y,x)∈ r^*` show "(z,x) ∈ r^*" using [[unify_trace_failure]]
    apply (subgoal_tac "1=(1::nat)")
    apply (rule converse_rtrancl_into_rtrancl)
      apply simp_all
    done
qed

我想实例化 converse_rtrancl_into_rtrancl 证明 (?a,?b) ∈ ?r ⟹ (?b,?c) ∈ ?r^* ⟹ (?a,?c) ∈ ?r^* .
但是如果没有看似荒谬的 apply (subgoal_tac "1=(1::nat)") 行，这个错误与

Clash: r =/= Transitive_Closure.rtrancl 
Failed to apply proof method⌂:
using this:
    (y,x) ∈ r^*
    (z,y) ∈ r
goal (1 subgoal):
 1. (z,x) ∈ r^*

如果我完全实例化规则 apply (rule converse_rtrancl_into_rtrancl[of z y r x])，这将变成 Clash: z__ =/= ya__。

这给我留下了三个问题：为什么这个特定案例会破裂？我该如何解决？由于我无法真正理解 unify_trace_failure 消息想要告诉我什么，我该如何找出这些情况下出了什么问题。

解决方法

rule - 策略通常对前提的顺序很敏感。 converse_rtrancl_into_rtrancl 和您的证明状态中的前提顺序不匹配。使用 rotate_tac 切换证明状态中的前提顺序将使它们匹配规则，因此您可以像这样直接应用 fact：

... show "(z,x) ∈ r^*" 
  apply (rotate_tac)
  apply (fact converse_rtrancl_into_rtrancl)
done

或者，如果您想包含某种 rule 策略，则如下所示：

  apply (rotate_tac)
  apply (erule converse_rtrancl_into_rtrancl)
  apply (assumption)

（我个人从不在日常工作中使用应用脚本。因此应用风格的大师可能知道处理这种情况的更优雅的方法。;））

---

关于您的 1=(1::nat) / simp_all 修复：

整个目标可以通过simp_all直接解决。因此，尝试添加诸如 1=1 之类的内容可能并没有真正告诉您其他方法对解决证明有多大贡献。

然而，附加假设似乎实际上有助于 Isabelle 正确匹配 converse_rtrancl_into_rtrancl。 （不要问我为什么！）所以，确实可以通过添加这个虚假假设然后再次用 refl 消除它来规避这个问题，例如：

apply (subgoal_tac "1=(1::nat)")
  apply (erule converse_rtrancl_into_rtrancl)
  apply (assumption)
apply (rule refl)

当然，这看起来不是特别优雅。

---

只有熟悉 Nipkow 高阶统一算法的内部工作原理，[[unify_trace_failure]] 才可能真正有用。 （我不是。）我认为这里对未来的暗示真的是人们必须仔细查看某些策略的前提顺序（而不是统一调试输出）。

,

我在 Isar 参考文献 6.4.3 中找到了解释。

with b1..bn 命令等效于 from b1..bn and this，即它进入证明链接模式，将它们作为（结构化）假设添加到证明方法中。

基本证明方法（如规则）期望给出多个事实 以正确的顺序，对应于前提的前缀 所涉及的规则。请注意，位置可以很容易地使用 例如，来自 _ 和 a 和 b 之类的东西。这涉及到 平凡规则 PROP ψ =⇒ PROP ψ，在 Isabelle/Pure 中绑定为“_” （下划线）。

自动化方法（例如 simp 或 auto）只是插入任何给定的事实 在他们通常的操作之前。取决于程序的类型 涉及，事实的顺序在这里不太重要。

给定有关“with”翻译的信息，并且该规则期望链接的事实按顺序排列，我们可以尝试翻转链接的事实。这确实有效：

  from this and `(y,x)∈ r^*` show "(z,x) ∈ r^*"
    by (rule converse_rtrancl_into_rtrancl)

我认为“6.4.3 基本方法和属性”也很重要，因为它描述了基本方法如何与传入的事实交互。值得注意的是，有时在开始证明时使用的“-”noop 会将前向链接转化为对目标的假设。

  with `(y,x) ∈ r^*"
    apply -
    apply (rule converse_rtrancl_into_rtrancl; assumption)
    done

这是有效的，因为第一个 apply 消耗所有链接的事实，所以第二个应用是纯粹的反向链接。这也是 subgoal_tac 或 rotate_tac 起作用的原因，但前提是它们在单独的应用命令中。