如何修复“非法示意图变量"在相互递归的规则归纳中? [英] How to fix "Illegal schematic variable(s)" in mutually recursive rule induction?

问题描述

在 Isabelle 中，我试图对相互递归的归纳定义进行规则归纳.这是我能够创建的最简单的示例:

In Isabelle, I'm trying to do rule induction on mutually recursive inductive definitions. Here's the simplest example I was able to create:

theory complex_exprs
imports Main
begin

datatype A = NumA int
           | AB B
and B = NumB int
      | BA A

inductive eval_a :: "A ⇒ int ⇒ bool" and eval_b :: "B ⇒ int ⇒ bool" where
eval_num_a: "eval_a (NumA i) i" |
eval_a_b:   "eval_b b i ⟹ eval_a (AB b) i" |
eval_num_b: "eval_b (NumB i) i" |
eval_b_a:   "eval_a a i ⟹ eval_b (BA a) i"

lemma foo:
  assumes "eval_a a result"
  shows   "True"
using assms
proof (induction a)
  case (NumA x)
    show ?case by auto
  case (AB x)

此时，Isabelle 以'Illegal Schematic variables(s) in case "AB"' 结束.实际上，当前的目标是 ⋀x.?P2.2 x ⟹ eval_a (AB x) 结果 ⟹ True 包含假设 ?P2.2 x.这就是伊莎贝尔所说的示意图变量"吗?它来自哪里，我该如何摆脱它?

At this point, Isabelle stops with 'Illegal schematic variable(s) in case "AB"'. Indeed the current goal is ⋀x. ?P2.2 x ⟹ eval_a (AB x) result ⟹ True which contains the assumption ?P2.2 x. Is that the 'schematic variable' Isabelle is talking about? Where does it come from, and how can I get rid of it?

如果我尝试对规则进行归纳，我会遇到同样的问题:

I get the same problem if I try to do the induction on the rules:

proof (induction)
  case (eval_num_a i)
    show ?case by auto
  case (eval_a_b b i)

同样，目标是⋀b i.eval_b b i ⟹ ?P2.0 b i ⟹ True 与未知 ?P2.0 b i，我无法继续.

Again, the goal is ⋀b i. eval_b b i ⟹ ?P2.0 b i ⟹ True with the unknown ?P2.0 b i, and I can't continue.

作为一个相关的问题:我尝试使用

As a related question: I tried to do the induction using

proof (induction rule: eval_a_eval_b.induct)

但伊莎贝尔不接受这一点，说未能应用初始证明方法".

but Isabelle doesn't accept this, saying 'Failed to apply initial proof method'.

我该如何进行这个归纳?(在我的实际应用中，我确实需要归纳，因为目标比 True 更复杂.)

How do I make this induction go through? (In my actual application, I do actually need induction because the goal is more complex than True.)

推荐答案

关于相互递归定义的证明，无论是数据类型、函数还是归纳谓词，都必须相互递归.然而，在你的引理中，你只声明了 eval_a 的归纳属性，而不是 eval_b 的归纳属性.对于 AB，您显然想对 eval_b 使用归纳假设，但由于引理没有说明 eval_b 的归纳属性，伊莎贝尔不知道是什么.所以它把它作为一个原理图变量?P2.0.

Proofs about mutually recursive definitions, be they datatypes, functions or inductive predicates, must be mutually recursive themselves. However, in your lemma, you only state the inductive property for eval_a, but not for eval_b. In the case for AB, you obviously want to use the induction hypothesis for eval_b, but as the lemma does not state the inductive property for eval_b, Isabelle does not know what it is. So it leaves it as a schematic variable ?P2.0.

所以，你必须陈述两个目标，比如说

So, you have to state two goals, say

lemma
  shows "eval_a a result ==> True"
  and "eval_b b result ==> True"

然后，induction a b 方法将计算出第一条语句对应于 A，第二条语句对应于 B.

Then, the method induction a b will figure out that the first statement corresponds to A and the second to B.

归纳谓词的归纳规则失败，因为该规则消除了归纳谓词(对数据类型的归纳只是消除"了类型信息，但这不是 HOL 公式)并且找不到第二个归纳谓词的假设.

The induction rule for the inductive predicates fails because this rule eliminates the inductive predicate (induction over datatypes only "eliminates" the type information, but this is not a HOL formula) and it cannot find the assumption for the second inductive predicate.

在src/HOL/Induct/Common_Patterns.thy中可以找到更多关于相互递归对象的归纳示例.

More examples on induction over mutually recursive objects can be found in src/HOL/Induct/Common_Patterns.thy.

这篇关于如何修复“非法示意图变量"在相互递归的规则归纳中?的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！