I'm running into what I believe could be a bug in Coq 8.4pl5. Given this proof state:
1 subgoal
st : state
a : sinstr
a0 : list sinstr
b : list sinstr
IHa : forall stack : list nat,
s_execute st stack (a0 ++ b) = s_execute st (s_execute st stack a0) b
stack : list nat
======================== ( 1 / 1 )
s_execute st stack ((a :: a0) ++ b) =
s_execute st (s_execute st stack (a :: a0)) b
Coq is allowing me to apply IHa. When I do this, it discharges the goal and proves the theorem.
Is this an incorrect unification (I'm thinking that it is) and, if so, has this issue been reported yet?
If not, how would I go about reporting it? I know that Coq is used in high assurance software and I believe that, even though this isn't the latest version, it isn't a particularly old version. So, even if it is fixed in later versions, it would be good to make sure people are aware that this issue does exist in this version of Coq.
For reference, I have narrowed the code down to this (I haven't tried to narrow it down further because I don't fully understand what might be causing this). The apply in question is in the second to last line (with all the asterisks in a comment):
(** aexp **)
Require Import Coq.Arith.Peano_dec.
Inductive id : Type :=
| Id : nat -> id.
Theorem eq_id_dec : forall a b : id,
{a = b} + {a <> b}.
Proof.
intros.
case_eq a.
case_eq b.
intros.
destruct (eq_nat_dec n0 n).
left. auto.
right. unfold not. intros. inversion H1. contradiction.
Qed.
Definition state : Type := id -> nat.
Definition empty_state : state :=
fun _ => 0.
Definition update (st : state) (i : id) (v : nat) : state :=
fun j => if eq_id_dec j i
then v
else st j.
Inductive aexp : Type :=
| AId : id -> aexp
| ANum : nat -> aexp
| APlus : aexp -> aexp -> aexp
| AMinus : aexp -> aexp -> aexp
| AMult : aexp -> aexp -> aexp.
Fixpoint aeval (a : aexp) (st : state) : nat :=
match a with
| AId i => st i
| ANum n => n
| APlus x y => aeval x st + aeval y st
| AMinus x y => aeval x st - aeval y st
| AMult x y => aeval x st * aeval y st
end.
(** Stack compiler **)
Require Import List.
Import ListNotations.
Inductive sinstr : Type :=
| SPush : nat -> sinstr
| SLoad : id -> sinstr
| SPlus : sinstr
| SMinus : sinstr
| SMult : sinstr.
Fixpoint s_execute (st : state) (stack : list nat) (prog : list sinstr)
: list nat :=
match prog with
| nil => stack
| cons x xs =>
let stack' := match x with
| SPush a => cons a stack
| SLoad v => cons (st v) stack
| SPlus => match stack with
| cons a (cons b rest) => cons (b + a) rest
| _ => [27]
end
| SMinus => match stack with
| cons a (cons b rest) => cons (b - a) rest
| _ => [27]
end
| SMult => match stack with
| cons a (cons b rest) => cons (b * a) rest
| _ => [27]
end
end
in
s_execute st stack' xs
end.
Fixpoint s_compile (e : aexp) : list sinstr :=
match e with
| AId i => [ SLoad i ]
| ANum n => [ SPush n ]
| APlus a b => (s_compile a) ++ (s_compile b) ++ [ SPlus ]
| AMinus a b => (s_compile a) ++ (s_compile b) ++ [ SMinus ]
| AMult a b => (s_compile a) ++ (s_compile b) ++ [ SMult ]
end.
Lemma s_execute_app : forall st stack a b,
s_execute st stack (a ++ b) = s_execute st (s_execute st stack a) b.
Proof.
intros.
generalize dependent stack.
induction a ; try reflexivity.
intros.
apply IHa. (***********************)
Qed.
If you do simpl after introducing, you'll see that the hypothesis and the goal can unify:
s_execute st
match a with
| SPush a1 => a1 :: stack
| SLoad v => st v :: stack
| SPlus =>
match stack with
| [] => [27]
| [a1] => [27]
| a1 :: b0 :: rest => b0 + a1 :: rest
end
| SMinus =>
match stack with
| [] => [27]
| [a1] => [27]
| a1 :: b0 :: rest => b0 - a1 :: rest
end
| SMult =>
match stack with
| [] => [27]
| [a1] => [27]
| a1 :: b0 :: rest => b0 * a1 :: rest
end
end (a0 ++ b) =
s_execute st
(s_execute st
match a with
| SPush a1 => a1 :: stack
| SLoad v => st v :: stack
| SPlus =>
match stack with
| [] => [27]
| [a1] => [27]
| a1 :: b0 :: rest => b0 + a1 :: rest
end
| SMinus =>
match stack with
| [] => [27]
| [a1] => [27]
| a1 :: b0 :: rest => b0 - a1 :: rest
end
| SMult =>
match stack with
| [] => [27]
| [a1] => [27]
| a1 :: b0 :: rest => b0 * a1 :: rest
end
end a0) b