How to prove something obviously logical - list_get problem in Prop

The problem is that I cannot apply induction on H without skipping a step. I was supposed to get Some instr0 to apply the standard lemma :

Lemma get_Some {A} (l:list A) n x :

 list_get l n = Some x -> n < length l.

Proof.

 revert n. induction l; destruct n; simpl; try discriminate.

 - auto with arith.
 - intros. apply IHl in H. auto with arith.

Qed.

frankly the first that come in mind is unfold the definition of Step and try induction on list_get.

Lemma getthatStep code m m' (n := List.length code): 
Step code m m' ->  pc m < length code .


1 subgoal

code : list instr

m, m' : machine

n := length code : nat

H : match list_get code (pc m) with

    | Some instr0 => Stepi instr0 m m'

    | None => False

    end

______________________________________(1/1)

pc m < length code

It seems obvious but I'm pretty blocked.

Here some Information on the types :


    Record machine :=Mach {
      (** Pointeur de code *)
      pc : nat;
      (** Pile principale *)
      stack : list nat;
      (** Pile de variables *)
      vars : list nat
    }.


    Inductive instr :=
  | Push : nat -> instr
  | Pop : instr
  | Op : op -> instr
  | NewVar : instr


 Inductive Stepi : instr -> machine -> machine -> Prop :=
| SPush pc stk vs n :  Stepi (Push n) (Mach pc stk vs) (Mach (S pc) (n::stk) vs)
| SPop pc stk vs x :   Stepi Pop (Mach pc (x::stk) vs) (Mach (S pc) stk vs)
| SOp pc stk vs o y x :     Stepi (Op o) (Mach pc (y::x::stk) vs) (Mach (S pc) (eval_op o x y :: stk) vs). ```

(* Takes two machines and a list of instructions if their code 
   is valid it returns true else it returns false   *)

Definition Step (code:list instr) (m m' : machine) : Prop :=
 match list_get code m.(pc) with
  | Some instr => Stepi instr m m'
  | None => False
 end.

Solution

You can get the relevant information with destruct (list_get code (pc m)) eqn:H'. This will give you enough information to apply your lemma in one case, and to prove the goal by exfalso in the other case.