坚持使用列表归纳的 Coq 证明答案

【问题标题】：Stuck on Coq proof with list induction坚持使用列表归纳的 Coq 证明
【发布时间】：2020-11-12 21:13:55
【问题描述】：

我发现自己陷入了 Coq 证明中。

初步定义：

Require Import Coq.Bool.Bool.
Require Import Coq.Arith.Arith.
Require Import Coq.Arith.EqNat.
Require Import Coq.omega.Omega.
Require Import Coq.Lists.List.
Require Export Coq.Strings.String.
Import ListNotations.


Definition total_map (A:Type) := string -> A.
Definition state := total_map nat.

Inductive sinstr : Type :=
| SPush : nat -> sinstr
| SLoad : string -> sinstr
| SPlus : sinstr
| SMinus : sinstr
| SMult : sinstr.



Definition s_execute_instr (st : state) (stack : list nat)
         (instr : sinstr)
  : option (list nat) :=
  match instr with
  | SPush n => Some (n :: stack)
  | SLoad x => Some (st x :: stack)
  | SPlus => match stack with
            | x :: y :: stack' => Some (x+y :: stack')
            | _ => None
            end
  | SMinus => match stack with
             | x :: y :: stack' => Some (y-x :: stack')
             | _ => None
             end
  | SMult => match stack with
            | x :: y :: stack' => Some (x*y::stack')
            | _ => None
            end
  end.

Fixpoint s_execute (st : state) (stack : list nat)
                   (prog : list sinstr)
  : option (list nat) :=
  match prog with
  | [] => Some (stack)
  | instr::prog' => match (s_execute_instr st stack instr) with
                  | Some stack' => s_execute st stack' prog'
                  | None => None
                  end
  end.

以及我对定理证明的尝试：

Theorem s_execute_relational : forall (l1 l2: list sinstr) (sk sk': list nat) (st : state),
  s_execute st sk l1 = Some sk' ->
  s_execute st sk (l1 ++ l2) = s_execute st sk' l2.
Proof.
  intros l1 l2 sk sk' st H.
  induction l1 as [|l1' l1].
  - inversion H. reflexivity.
  -

目前的状态是：

  l1' : sinstr
  l1, l2 : list sinstr
  sk, sk' : list nat
  st : state
  H : s_execute st sk (l1' :: l1) = Some sk'
  IHl1 : s_execute st sk l1 = Some sk' -> s_execute st sk (l1 ++ l2) = s_execute st sk' l2
  ============================
  s_execute st sk ((l1' :: l1) ++ l2) = s_execute st sk' l2

我走这条路是因为我认为我需要以某种方式使用归纳法，但在这一点上，我不确定如何继续。

我也尝试在 l2 上进行归纳，但这似乎也没有让我有所收获；

Theorem s_execute_relational : forall (l1 l2: list sinstr) (sk sk': list nat) (st : state),
  s_execute st sk l1 = Some sk' ->
  s_execute st sk (l1 ++ l2) = s_execute st sk' l2.
Proof.
  intros l1 l2 sk sk' st H.
  induction l2 as [|l2' l2].
  - simpl. rewrite <- H. replace (l1 ++ []) with l1.
    + reflexivity.
    + symmetry. apply app_nil_r.
  -

  l1 : list sinstr
  l2' : sinstr
  l2 : list sinstr
  sk, sk' : list nat
  st : state
  H : s_execute st sk l1 = Some sk'
  IHl2 : s_execute st sk (l1 ++ l2) = s_execute st sk' l2
  ============================
  s_execute st sk (l1 ++ l2' :: l2) =
  s_execute st sk' (l2' :: l2)

在 SO 上问这种类型的问题很奇怪，因为它不是……可重复使用的问题/标题确实很糟糕，但也不确定如何在这方面进行改进。

【问题讨论】：

你的代码不是独立的：state和sinstr没有定义。
@Yves 两者都添加了。

标签： coq

【解决方案1】：

您不应像在第一行中那样引入所有变量。您应该首先查看您的递归函数并有两个问题：

这里的递归函数及其“结构递归参数”是什么。您可能已经注意到，当 Coq 接受递归定义时，它会告诉您它在结构上是递归的。
函数中非结构递归的参数会发生什么情况：它们在递归调用之间是否发生变化？

问题 1 的答案：

在您的情况下，我们有两个主要的递归函数 List.app 和 s_execute。 s_execute 的递归参数是蕴含左侧的 l1。 s_execute 的递归参数是最终等式左侧的 l1 ++ l2，s_execute 的递归参数只有右侧的 l2。因为l1 ++ l2 位于递归参数的位置，所以我们现在可以通过查看其代码来查看app 的递归参数，我们可以看到在递归调用中结构减少的参数又是l1。这给人一种强烈的感觉，应该对l1进行归纳。

问题 2 的答案： s_execute 接受三个参数。状态在执行期间不会改变，但堆栈会改变。所以你可以为整个证明修复st，但不应该修复堆栈参数。 app 也出现了类似的观察结果：第二个参数在递归调用期间不会改变。

实际上，你可以从

开始你的证明

intros l1 l2.
induction l1 ....

不要在介绍中继续深入，因为堆栈应该保持灵活，在使用归纳假设时您将需要这种灵活性。

为了好玩，您可以尝试引入更多参数，但您必须使用revert 策略释放灵活的参数。就像这样：

intros l1 l2 sk sk' st; revert sk.
induction l1 as ....

这里只有sk 必须被释放（或不固定，或恢复）。

这实际上是一个非常好的问题，在正式证明中经常会出现避免修正在使用归纳假设时需要改变的论点的需要。

稍后编辑

我是这样开始证明你的：

Theorem s_execute_relational : forall (l1 l2: list sinstr) (sk sk': list nat) (st : state),
  s_execute st sk l1 = Some sk' ->
  s_execute st sk (l1 ++ l2) = s_execute st sk' l2.
Proof.
intros l1 l2 sk sk' st; revert sk.
induction l1 as [ | n l1 Ih].  
  simpl; intros sk [= skk']; rewrite skk'; easy.

现在我们处于归纳步骤案例中。堆栈仍然在目标的结论中被普遍量化。所以归纳假设和目标实际上是在谈论两个可能不同的堆栈。下一步是修复任意堆栈以推理结论。

intros sk.

然后我们计算，

simpl.

我们正在推理代码的符号执行，我们不知道(s_execute_instr st sk n) 将如何产生结果，因此我们需要涵盖这两种情况，这就是destruct 步骤所做的。

destruct (s_execute_instr st sk n) as [sk1 | ].

在第一种情况下（对于(s_execute_instr st sk n) 的执行），出现了一个新状态sk1，将在该状态下继续执行，我们知道从该状态执行l1 会导致Some sk'。让我们将名称 complete_l1 赋予该新状态。现在恰好可以通过在这个新状态上实例化归纳假设来完成证明。

  intros complete_l1.
  now rewrite (Ih sk1).

destruct 步骤产生的另一种情况仍然存在，但这种情况包含None = Some sk' 形式的自不一致假设。 easy 策略知道如何摆脱这一点（实际上easy 依赖于discriminate，它实现了我喜欢称之为数据类型的非混淆 属性）。

easy.
Qed.

请告诉我你的尝试中遗漏了什么？是destruct 步骤吗？

【讨论】：

我仍然不确定免费的sk 对我有何帮助。我应该在归纳假设部分单独介绍它们吗？在归纳假设部分我应该做什么？我仍然感到迷茫。
你的评论不清楚：你称之为“归纳假设部分”。当您通过归纳进行证明时，您有两个目标。在它们中的每一个中，您都应该执行intros sk，因为您在归纳步骤之后获得的目标是通用量化。因此，在您尝试的过程中，您的上下文中将有一个sk，但不同之处在于，在归纳步骤中，归纳假设将被普遍量化，而不是仅针对sk。
对，我指的是归纳步骤（与基本情况相反）。我的意思是问在归纳步骤中要做什么，现在我有一个普遍量化的sk。我仍然不知道去那里之后。
我宁愿给你一个更简单证明的例子，但我找不到如何在聊天中继续这个对话，因为 cmets 用起来很麻烦。
我宁愿给你一个更简单证明的例子，但我找不到如何在聊天中继续这个对话，因为 cmets 用起来很麻烦。

【解决方案2】：

最终，我想通了。

Theorem s_execute_relational : forall (l1 l2: list sinstr) (sk sk': list nat) (st : state),
  s_execute st sk l1 = Some sk' ->
  s_execute st sk (l1 ++ l2) = s_execute st sk' l2.
Proof.
  intros l1.
  induction l1 as [| l1' l1].
  - intros l2 sk sk' st H. simpl.
    inversion H. reflexivity.
  - intros l2 sk sk' st H.
    assert (forall (x:sinstr) (xs ys: list sinstr), (x::xs) ++ys = x::(xs++ys)) as app_comm_cons.
    {
      auto.
    }
    rewrite app_comm_cons.
    unfold s_execute in *. destruct (s_execute_instr st sk l1').
    + eapply IHl1. apply H.
    + inversion H.
Qed.

【讨论】：