1

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

4

2 回答 2

2

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可能并没有真正告诉您其他方法对解决证明的贡献有多大。

然而，额外的假设似乎实际上有助于 Isabelleconverse_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 的高阶统一算法的内部工作原理，这可能真的很有帮助。（我不是。）我认为这里对未来的暗示实际上是必须仔细查看某些策略的前提顺序（而不是统一调试输出）。

于 2021-05-27T07:58:33.890 回答
0

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

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

基本证明方法（例如规则）期望以正确的顺序给出多个事实，对应于所涉及规则前提的前缀。请注意，使用 from _ 和 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_tacorrotate_tac起作用的原因，但前提是它们位于单独的应用命令中。

于 2021-05-29T14:24:38.220 回答