Как доказать что-то явно логичное - проблема list_get в Prop - PullRequest
Новая
       21

Как доказать что-то явно логичное - проблема list_get в Prop

0 голосов
/ 01 апреля 2019

Проблема в том, что я не могу применить индукцию к H без пропуска шага.Я должен был заставить Some 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.

1 Ответ

1 голос
/ 03 апреля 2019

Вы можете получить соответствующую информацию с помощью destruct (list_get code (pc m)) eqn:H'.Это даст вам достаточно информации, чтобы применить вашу лемму в одном случае и доказать цель с помощью exfalso в другом случае.

...