如何在Prop中证明一些明显符合逻辑的 - list_get问题

Question

问题是我不能在不跳过步骤的情况下在H上应用归纳法。我应该得到一些instr0来应用标准引理：

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.

坦率地说，第一个想到的是展开Step的定义并尝试在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

这看起来很明显但我很受阻。

这里有一些关于类型的信息：

    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.

Answer 1

您可以通过destruct (list_get code (pc m)) eqn:H'获取相关信息。这将为您提供足够的信息，以便在一个案例中应用您的引理，并在另一个案例中证明exfalso的目标。