如何在Coq中推进嵌套match的案例分析与证明？

当前卡住的证明目标 #

执行到案例分析的分支后，得到如下目标：

1 goal (ID 110)
  
  addr : nat
  x : State
  l : list nat
  Heqo : write_list_index (repeat 0 (addr + 1)) addr 0 = Some l
  ============================
  match
    match write_list_index (repeat 0 (addr + 1)) addr 0 with
    | Some l' => Some (0 :: l')
    | None => None
    end
  with
  | Some stack' => Success (update_stack stack' (access_fault_handler (S addr) init_state))
  | None => Failure (access_fault_handler (S addr) init_state)
  end <> Failure x

该命题本应为真，但使用simpl无变化，改写Heqo也无法推进。

简化后的项目代码 #

Require Import Nat.
Require Import List.
Require Import Bool.
Import ListNotations.

Definition address := nat.
Definition variable := nat.

Record State: Set :=
  mkState {
    stack: list variable;
    }.

Inductive instruction: Set :=
| WriteToStack (addr: address) (value: variable).

Inductive insr_result: Set :=
| Success (state: State)
| Failure (state: State).

Definition has_access (addr: address) (state: State): bool :=
  match compare addr (length state.(stack)) with
  | Lt => true
  | _ => false
  end.

Fixpoint write_list_index {A: Type} (l: list A) (index: nat) (value: A)
  : option (list A) :=
  match l with
  | nil => None
  | h :: t => match index with
            | O => Some (value :: t)
            | S n => match (write_list_index t n value) with
                    | None => None
                    | Some l' => Some (h :: l')
                    end
            end
  end.

Definition update_stack (stack': list variable) (state: State): State :=
  {|
    stack := stack';
   |}.

Definition write_to_stack (addr: address) (value: variable) (state: State)
  (afh: address -> State -> State): insr_result :=
  if has_access addr state then
    match write_list_index state.(stack) addr value with
    | None => Failure state
    | Some stack' => Success (update_stack stack' state)
    end
  else
    let state := afh addr state in
    match write_list_index state.(stack) addr value with
    | None => Failure state
    | Some stack' => Success (update_stack stack' state)
    end.

Definition eval_insr (insr: instruction) (state: State) (afh: address -> State -> State): insr_result :=
  match insr with
  | WriteToStack addr value => write_to_stack addr value state afh
  end.


Definition access_fault_handler (addr: address) (state: State): State :=
  if addr <? length state.(stack) then
    state
  else
    let frame_size := addr - length state.(stack)+ 1 in
    {| stack := state.(stack) ++ (repeat 0 frame_size) |}.

Definition init_state: State := {| stack := nil; |}.

Theorem write_to_stack_never_fails: forall addr x, eval_insr (WriteToStack addr 0) init_state access_fault_handler <> Failure x.
Proof.
  intros.
  simpl.
  unfold write_to_stack. simpl.
  destruct addr.
  - simpl. unfold not. intros. inversion H.
  - simpl. destruct (write_list_index (repeat 0 (addr + 1)) addr 0) eqn:?.
    + (* Stuck *)

推进证明的方法 #

核心思路 #

利用假设Heqo将目标中重复的write_list_index调用替换为已知的Some l，此时目标会简化为判断Success构造的结果与Failure x不等——而Success和Failure是insr_result的互斥构造子，直接利用构造子的不相交性即可完成证明。

具体tactic序列 #

在卡住的分支中执行以下命令：

rewrite Heqo.
discriminate.

步骤解释 #

1. rewrite Heqo：将目标里的write_list_index (repeat 0 (addr + 1)) addr 0全部替换为Some l，此时目标的match结构会直接走到Some stack'分支，生成Success类型的结果。
2. discriminate：Coq内置的tactic，用于证明不同构造子构造的项不可能相等。这里Success _和Failure x是完全不同的构造子，discriminate会直接识别这种矛盾，完成证明。

如果需要更详细的步骤，也可以展开不等关系后用反证法：

rewrite Heqo.
unfold not.
intros H.
inversion H.

inversion H会拆解等式Success _ = Failure x，发现两个构造子不匹配，从而导出矛盾，完成证明。

内容的提问来源于stack exchange，提问作者kunkun