允许看起来不应该统一的申请
An apply that doesn't seem like it should unify is allowed
我 运行 我认为可能是 Coq 8.4pl5 中的错误。鉴于此证明状态:
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 允许我apply IHa
。当我这样做时,它完成了目标并证明了定理。
这是一个不正确的统一吗(我认为是),如果是这样,是否已报告此问题?
如果没有,我将如何报告?我知道 Coq 用于高保证软件,我相信,即使这不是最新版本,也不是特别旧的版本。所以,即使它在以后的版本中得到修复,也最好确保人们知道这个问题确实存在于这个版本的 Coq 中。
作为参考,我已将代码缩小到这个范围(我没有尝试进一步缩小范围,因为我不完全理解可能导致这种情况的原因)。有问题的 apply
在倒数第二行(注释中有所有星号):
(** 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.
引入后simpl
,你会发现假设和目标可以统一:
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
尽管您可能不想报告这个特定问题,但由于 Arthur 的分析,如果您想联系 Coq 开发人员,他们会在 Coq-club 和 Coq-dev 邮件列表上闲逛。参见
https://coq.inria.fr/community
用于存档和更多信息。
还有一个错误跟踪系统,Coq-bugs,您可以使用。
我 运行 我认为可能是 Coq 8.4pl5 中的错误。鉴于此证明状态:
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 允许我apply IHa
。当我这样做时,它完成了目标并证明了定理。
这是一个不正确的统一吗(我认为是),如果是这样,是否已报告此问题?
如果没有,我将如何报告?我知道 Coq 用于高保证软件,我相信,即使这不是最新版本,也不是特别旧的版本。所以,即使它在以后的版本中得到修复,也最好确保人们知道这个问题确实存在于这个版本的 Coq 中。
作为参考,我已将代码缩小到这个范围(我没有尝试进一步缩小范围,因为我不完全理解可能导致这种情况的原因)。有问题的 apply
在倒数第二行(注释中有所有星号):
(** 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.
引入后simpl
,你会发现假设和目标可以统一:
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
尽管您可能不想报告这个特定问题,但由于 Arthur 的分析,如果您想联系 Coq 开发人员,他们会在 Coq-club 和 Coq-dev 邮件列表上闲逛。参见
https://coq.inria.fr/community
用于存档和更多信息。 还有一个错误跟踪系统,Coq-bugs,您可以使用。