Isabelle 中的脆弱规则应用

Question

我正在玩 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 消息想要告诉我什么，我该如何弄清楚这些情况下出了什么问题。

Answer 1

rule-tactics 通常对前提的顺序很敏感。 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)

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

---

[[unify_trace_failure]] 可能只有在熟悉 Nipkow 的高阶统一算法的内部工作原理的情况下才真正有帮助。 （我不是。）我认为这里对未来的暗示实际上是必须仔细研究某些策略的前提顺序（而不是统一调试输出）。

Answer 2

我在 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^*` show "(z,x) ∈ r^*"
    apply -
    apply (rule converse_rtrancl_into_rtrancl; assumption)
    done

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