在 Isabelle 中调试 ML 证明答案

【问题标题】：Debugging ML proofs in Isabelle在 Isabelle 中调试 ML 证明
【发布时间】：2020-03-23 03:33:12
【问题描述】：

我编写了以下 ML 代码：

lemma fstI: "x = (y, z) ⟹ y = fst x"
  by simp

ML ‹
val ctxt0 = @{context};
val ctxt = ctxt0;
val (_,ctxt) = Variable.add_fixes ["z1'","x1'","y1'","x1", "y1", "x2", "y2"] ctxt;
val (assms,ctxt) = Assumption.add_assumes 
                       [@{cprop "z1' = (x1',y1')"},@{cprop "z1' = ext_add (x1,y1) (x2,y2)"}] ctxt;
val th1 = @{thm fstI}  OF  [(nth assms 0)]
val th2 = Thm.instantiate' [SOME @{ctyp "'a"}] [SOME @{cterm "fst::'a×'a ⇒ 'a"}] (@{thm arg_cong} OF [(nth assms 1)])
val x1'_expr = Goal.prove ctxt [] []
                               @{prop "x1' = fst (ext_add (x1,y1) (x2,y2))"}
                          (fn _ => EqSubst.eqsubst_tac ctxt [1] [th1] 1
                                  THEN EqSubst.eqsubst_tac ctxt [1] [th2] 1
                                  THEN simp_tac ctxt 1)
›

对应以下Isar证明：

lemma taylored_assoc: 
  assumes "z1' = (x1',y1')"
          "z1' = ext_add (x1,y1) (x2,y2)" "z3' = add (x2,y2) (x3,y3)" 
  shows "x1' = fst (ext_add (x1,y1) (x2,y2))"   
  by(tactic ‹EqSubst.eqsubst_tac @{context} [1] [@{thm fstI[OF assms(1)]}] 1
                THEN EqSubst.eqsubst_tac @{context} [1] [@{thm arg_cong[OF assms(2), of fst]}] 1
                THEN simp_tac @{context} 1›)

它的 ML 版本由于某种原因无法正常工作？我怎么能调试这个？有 print_tac 策略，但它只接受字符串，而我想在应用每个策略后打印实际的子目标。

【问题讨论】：

"有print_tac 策略，但它只接受字符串。"为什么这是个问题？ print_tac 过去对我来说效果很好。时不时还用Subgoal.FOCUS作为调试策略。
@xanonec，我想在第一次替换后打印目标，以便了解为什么在 ML 级别失败...我感觉上下文可能有问题，但我有没有办法检查
这似乎不是print_tac 做不到的。为什么不能在合适的位置插入THEN print_tac @{context} ""？如果这不是一个选项，那么您应该能够在“内部”SUBPROOF 或 Subgoal.FOCUS 打印任何相关信息：有关更多信息和示例，请参阅实施手册或 Isabelle/ML 食谱。
@xanonec 这对我不起作用...我正在尝试 ml 的调试工具（以防这样做没有意义）
@xanonec 在上述之上，我觉得问题可能出在上下文中：Isabelle 的通用 Simplifier [14] 已经是将自动证明工具集成到我们的架构中的一个重要示例上下文数据和声明（参见§3）。通用证明方法 simp 依赖于作为上下文数据维护的 simpset 容器。（来自www21.in.tum.de/~wenzelm/papers/context-methods.pdf），所以基本上我认为简化器可能是从理论而不是从实际证明中获取上下文......只是一个想法

标签： isabelle ml

【解决方案1】：

我认为问题与类型推断有关：在反引用@{cprop "z1' = (x1',y1')"} 中，没有简单的方法可以自动推断变量x1' 和y1' 的所需类型y1'，因为每个反引用在假设列表在传递给add_assumes之前独立于其他反引号进行预处理。因此，推断出最一般的类型。您只需要明确提供每个变量的类型，例如@{cprop "z1' = (x1'::'a,y1'::'a)"} 这个策略应该奏效。但是，在我看来，更好的解决方案是直接在 ML 中使用显式类型分配定义变量，例如 x1' 和 y1'，例如val x1t = Free("x1", T)，其中 T 是所需的类型 'a。

【讨论】：