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