How to continue case analysis of a nested match in coq?

Question

I recently got a goal from coq (Actually I get this goal from case analysis):

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

This should be true, however, I cannot continue this proof since I use simpl tactic it doesn't change, moreover, I also cannot rewrite Heqo, because it doesn't change, too.

How can I continue this proof? Thanks!

Update: I have simplify my project and get the following code:

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. Looking at your goal in Printing All mode, you may notice that it's enough to replace in the implicit argument variable with nat.

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

2. In order to solve the remaining subgoal, you may first prove some lemma about write_list_index which may imply that Heqo leads to a contradiction.

Lemma L addr : 
  exists i, write_list_index (repeat 0 (addr + 1)) addr 0 = Some i.