如何对两个归纳谓词进行归纳？

Question

我从 Coq 开始并尝试形式化 Automated Amortized Analysis。我在引理 4.13:

Lemma preservation : forall (Sigma : prog_sig) (Gamma : context) (p : program)
  (s : stack) (h h' : heap) (e : expr) (c : type0) (v : val),
  (* 4.1 *) has_type Sigma Gamma e c ->
  (* 4.2 *) eval p s h e v h' ->
  (* 4.3 *) mem_consistant_stack h s Gamma ->
  (* 4.a *) mem_consistant h' v c /\ (* 4.b *) mem_consistant_stack h' s Gamma.
Proof.
  intros Sigma Gamma p s h h' e c v WELL_TYPED EVAL.

人工证明使用双归纳法：

证明。请注意，引理 4.8 和引理直接遵循声明 (4.b) 4.12.每个位置 l ∈ dom( H ) 要么保持不变，要么被值 Bad 覆盖，因此不会使内存无效 一致性。

但是，第一个声明（4.a）需要通过以下方式证明 对 (4.2) 和 (4.1) 有序推导的长度进行归纳 字典序与求值的推导 优先于类型推导。这是必需的，因为在 - 单独推导类型推导的长度会失败 函数应用的情况：为了允许递归 功能，应用程序的类型规则是依赖于 程序签名中为函数指定的类型。然而， 证明这种情况需要对以下陈述进行归纳： 该函数类型良好，这很可能是一种类型推导 更长的长度（即长于一步），禁止我们 使用归纳假设。请注意，在这种特殊情况下 评估陈述的推导长度确实减少了。 仅对前提 (4.2) 的推导长度进行归纳 同样失败。考虑推导前提的最后一步 (4.1) 通过应用结构规则导出，则 (4.2) 的推导长度保持完全相同，而 前提 (4.1) 的推导长度确实减少了一步。

对类型的字典顺序长度使用归纳法 和评估推导允许我们使用归纳假设 如果前提 (4.2) 的推导长度是 缩短或前提 (4.2) 的推导长度保持不变 不变，而打字推导的长度减少了。我们 首先处理类型推导的最后一步是 通过应用结构规则获得，这是所有情况 这使评估的推导长度保持不变。 然后我们继续考虑剩余的案例 604.3 上次应用的评估规则的操作语义推导前提（4.2），因为剩余的类型规则 都是语法指导的，因此明确地由 应用评估规则。

Coq 中如何进行这样的“双重归纳”？

我尝试了

induction EVAL; induction WELL_TYPED

，但得到了418个子目标，其中大部分是无法证明的。

我也试过先用

induction EVAL

然后再用

induction WELL_TYPED

，但是卡在了类似的情况下。

Answer 1

我同意@jbapple 的观点，一个最小的例子更好。也就是说，您可能只是缺少 推导长度 的概念。请注意，通过对谓词的归纳法进行证明的通常概念实际上实现了一些接近 对推导高度的归纳法，但不完全是。

我建议你展示两个新谓词

eval_n

和

has_type_n

，每个表示相同的

eval

和

has_type

，但有一个额外的参数，意思是“......并且推导的大小为n”。 size 有几种定义方式，但我怀疑高度对你来说足够了。

那么你可以证明

eval a1 .. ak <-> exists n, eval_n a1 .. ak n

和

has_type a1 .. ak <-> exists n, has_type a1 .. ak n

然后你应该能够证明

forall p : nat * nat, forall a1 ... ak, eval_n a1 .. ak (fst p) ->
   has_type_n a1 .. ak (snd p) -> YOUR GOAL

通过对自然数对的有根据的归纳，使用库

Wellfounded

的词法顺序构造（我建议库

Lexicographic_Product.v

，对于自然数对有点矫枉过正，但你只需要找到正确的实例化）。

这会很笨重，因为归纳假设只会涉及对 的词汇顺序可比较的数字，你将不得不对有关

eval_n

和

has_type_n

的假设进行反演，但这应该通过。

可能存在更简单的解决方案，但由于您缺乏更多信息，我只能提出大枪。