当使用rewrite策略时，Coq无法找到子项

Question

我正在尝试修改Certified Programming with Dependent Types第一章中栈机器章节的compile_correct证明。在我的版本中，我试图利用progDenote是一个fold的事实，并在主引理的证明中使用更弱的归纳假设来证明compile_correct。

与书中完全相同的代码如下：

Require Import Bool Arith List.
Set Implicit Arguments.

Inductive binop : Set := Plus | Times.

Inductive exp : Set :=
  | Const : nat -> exp
  | Binop : binop -> exp -> exp -> exp.

Definition binopDenote (b : binop) : nat -> nat -> nat :=
  match b with
    | Plus => plus
    | Times => mult
  end.

Fixpoint expDenote (e : exp) : nat :=
  match e with
    | Const n => n
    | Binop b e1 e2 => (binopDenote b) (expDenote e1) (expDenote e2)
  end.

Inductive instr : Set :=
  | iConst : nat -> instr
  | iBinop : binop -> instr.

Definition prog := list instr.
Definition stack := list nat.

Definition instrDenote (i : instr) (s : stack) : option stack :=
  match i with
    | iConst n => Some (n :: s)
    | iBinop b =>
      match s with
        | arg1 :: arg2 :: s' => Some ((binopDenote b) arg1 arg2 :: s')
        | _ => None
      end
  end.

Fixpoint compile (e : exp) : prog :=
  match e with
    | Const n => iConst n :: nil
    | Binop b e1 e2 => compile e2 ++ compile e1 ++ iBinop b :: nil
  end.

然后我定义了自己版本的prog_denote，这是对程序中指令列表的折叠：

Definition bind {A B : Type} (a : option A) (f : A -> option B) : option B :=
  match a with
    | Some x => f x
    | None => None
  end.

Definition instrDenote' (s : option stack) (i : instr) : option stack :=
  bind s (instrDenote i).

Definition progDenote (p : prog) (s : stack) : option stack :=
  fold_left instrDenote' p (Some s).

我尝试证明书中compile_correct的一个较弱版本：

Lemma compile_correct' : forall e s,
  progDenote (compile e) s = Some (expDenote e :: s).
induction e.
intro s.
unfold compile.
unfold expDenote.
unfold progDenote at 1.
simpl.
reflexivity.
intro s.
unfold compile.
fold compile.
unfold expDenote.
fold expDenote.
unfold progDenote.
rewrite fold_left_app.
rewrite fold_left_app.
unfold progDenote in IHe2.
rewrite (IHe2 s).
unfold progDenote in IHe1.
rewrite (IHe1 (expDenote e2 :: s)).

我的证明在最后一行出现了问题，证明状态为：

1 subgoal
b : binop
e1 : exp
e2 : exp
IHe1 : forall s : stack,
       fold_left instrDenote' (compile e1) (Some s) =
       Some (expDenote e1 :: s)
IHe2 : forall s : stack,
       fold_left instrDenote' (compile e2) (Some s) =
       Some (expDenote e2 :: s)
s : stack
______________________________________(1/1)
fold_left instrDenote' (iBinop b :: nil)
  (fold_left instrDenote' (compile e1) (Some (expDenote e2 :: s))) =
Some (binopDenote b (expDenote e1) (expDenote e2) :: s)

错误信息为：

Error:
Found no subterm matching "fold_left instrDenote' (compile e1)
                             (Some (expDenote e2 :: s))" in the current goal.

在证明的这个阶段，我正在对被编译的表达式e进行归纳，同时处理exp的Binop构造函数。 我不明白为什么会出现这个错误，因为一旦我将IHe1 应用于 expDenote e2 :: s之后，就没有绑定变量了。这似乎是应用重写规则时通常遇到的问题。我还检查了我要创建的术语：

fold_left instrDenote' (iBinop b :: nil)
  (Some (expDenote e1 :: expDenote e2 :: s)) =
Some (binopDenote b (expDenote e1) (expDenote e2) :: s)

类型检查。

当重写规则中明显存在被抱怨的子表达式，但出现了什么问题?

编辑: 如建议所示，我在coqide中更改了显示设置，相当于设置打印所有。这揭示了问题是stack的定义已经在目标中的一个位置展开为list nat，这阻止了子项被识别。使用新设置打印的目标为:

1 subgoal
b : binop
e1 : exp
e2 : exp
IHe1 : forall s : stack,
       @eq (option stack)
         (@fold_left (option stack) instr instrDenote' (compile e1)
            (@Some stack s)) (@Some (list nat) (@cons nat (expDenote e1) s))
IHe2 : forall s : stack,
       @eq (option stack)
         (@fold_left (option stack) instr instrDenote' (compile e2)
            (@Some stack s)) (@Some (list nat) (@cons nat (expDenote e2) s))
s : stack
______________________________________(1/1)
@eq (option stack)
  (@fold_left (option stack) instr instrDenote'
     (@cons instr (iBinop b) (@nil instr))
     (@fold_left (option stack) instr instrDenote' (compile e1)
        (@Some (list nat) (@cons nat (expDenote e2) s))))
  (@Some (list nat)
     (@cons nat (binopDenote b (expDenote e1) (expDenote e2)) s))

错误信息如下

Error:
Found no subterm matching "@fold_left (option stack) instr instrDenote'
                             (compile e1)
                             (@Some stack (@cons nat (expDenote e2) s))" in the current goal.

- Kester Tong

---

你能在证明之前添加一行代码，以便在启用“Set Printing All”时打印出什么吗？ - Arthur Azevedo De Amorim

完成了，谢谢建议。现在我看到表达式不同了，因为stack在目标中显示为list nat。我对Coq的了解还不够，无法理解为什么在目标中扩展了stack的定义（以及为什么它仍然在默认打印设置下显示为stack）。 - Kester Tong

现在我看到发生了什么，fold stack解决了这个问题。从我所读的内容来看，对于初学者来说，unfold策略在展开表达式时不是完全明显的，所以加上默认显示设置似乎是问题的原因。 - Kester Tong

Answer 1

即使使用默认的显示设置，子项似乎出现在目标中，但启用了 “Set Printing All” 之后，很明显子项与目标不匹配，因为在目标中，“stack”已经展开为“list nat”。 因此，在目标中需要使用“fold stack”将“list nat”转换回“stack”。作为初学者，我被以下组合所绊倒：

- “unfold”策略展开了更多定义，比初学者预期的还要多。 - 默认的显示设置（在我的情况下是CoqIDE）可以隐藏这一点，因为它们折叠了一些术语。

感谢Arthur Azevedo De Amorim建议启用 “Set Printing All”。

- Kester Tong