如何在coq中继续进行嵌套匹配的案例分析？

Question

我最近从coq得到了一个目标（其实我是通过案例分析得到这个目标的）：

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 *)

Answer 1

1. 在

   Printing All

   模式下查看目标，您会发现将隐式参数

   variable

   替换为

   nat

   就足够了。

Set Printing All. 
unfold variable in *; rewrite Heqo. discriminate. 
Unset Printing All. 

2. 不幸的是，相同的序列导致了一个显然无法解决的子目标（因为

   x

   是任何

   nat

   （正如上下文似乎推断的）-。 也许这是你的形式化错误？

 + unfold variable in *. rewrite Heqo. 
      simpl. 
      (*
  addr : nat
  x : State
  Heqo : write_list_index (repeat 0 (addr + 1)) addr 0 = None
  ============================
  Failure (access_fault_handler (S addr) init_state) <> Failure x
       *)