1
我在理解爲什麼我的Coq代碼沒有按照我期望的代碼執行下面的代碼時遇到問題。Coq中分號的奇怪行爲
- 我試着讓示例儘可能簡化，但是當我使它變得更簡單時，問題再也沒有出現。
- 它使用CompCert 1.8文件。
- 這發生在Coq 8.2-pl2下。
下面是代碼：
Require Import Axioms.
Require Import Coqlib.
Require Import Integers.
Require Import Values.
Require Import Asm.
Definition foo (ofs: int) (c: code) : Prop :=
c <> nil /\ ofs <> Int.zero.
Inductive some_prop: nat -> Prop :=
| some_prop_ctor :
forall n other_n ofs c lo hi ofs_ra ofs_link,
some_prop n ->
foo ofs c ->
find_instr (Int.unsigned ofs) c <> Some (Pallocframe lo hi ofs_ra ofs_link) ->
find_instr (Int.unsigned ofs) c <> Some (Pfreeframe lo hi ofs_ra ofs_link) ->
some_prop other_n
.
Lemma simplified:
forall n other_n ofs c,
some_prop n ->
foo ofs c ->
find_instr (Int.unsigned ofs) c = Some Pret ->
some_prop other_n.
Proof.
intros.
這不起作用：
eapply some_prop_ctor
with (lo:=0) (hi:=0) (ofs_ra:=Int.zero) (ofs_link:=Int.zero);
eauto; rewrite H1; discriminate.
上rewrite H1與失敗：
Error:
Found no subterm matching "find_instr (Int.unsigned ofs) c" in the current goal.
這工作雖然：
使用分號不起作用2 subgoals
n : nat
other_n : nat
ofs : int
c : code
H : some_prop n
H0 : foo ofs c
H1 : find_instr (Int.unsigned ofs) c = Some Pret
______________________________________(1/2)
find_instr (Int.unsigned ofs) c <> Some (Pallocframe 0 0 Int.zero Int.zero)
______________________________________(2/2)
find_instr (Int.unsigned ofs) c <> Some (Pfreeframe 0 0 Int.zero Int.zero)
所以，rewrite H1; discriminate兩次工作，但「管」它eauto後：
eapply some_prop_ctor
with (lo:=0) (hi:=0) (ofs_ra:=Int.zero) (ofs_link:=Int.zero);
eauto.
rewrite H1; discriminate.
rewrite H1; discriminate.
Qed.
而且，就在eauto後，我的目標是這樣的。
我希望這個問題至少有意義。謝謝！
全碼：
Require Import Axioms.
Require Import Coqlib.
Require Import Integers.
Require Import Values.
Require Import Asm.
Definition foo (ofs: int) (c: code) : Prop :=
c <> nil /\ ofs <> Int.zero.
Inductive some_prop: nat -> Prop :=
| some_prop_ctor :
forall n other_n ofs c lo hi ofs_ra ofs_link,
some_prop n ->
foo ofs c ->
find_instr (Int.unsigned ofs) c <> Some (Pallocframe lo hi ofs_ra ofs_link) ->
find_instr (Int.unsigned ofs) c <> Some (Pfreeframe lo hi ofs_ra ofs_link) ->
some_prop other_n
.
Lemma simplified:
forall n other_n ofs c,
some_prop n ->
foo ofs c ->
find_instr (Int.unsigned ofs) c = Some Pret ->
some_prop other_n.
Proof.
intros.
(*** This does not work:
eapply some_prop_ctor
with (lo:=0) (hi:=0) (ofs_ra:=Int.zero) (ofs_link:=Int.zero);
eauto; rewrite H1; discriminate.
***)
eapply some_prop_ctor
with (lo:=0) (hi:=0) (ofs_ra:=Int.zero) (ofs_link:=Int.zero);
eauto.
rewrite H1; discriminate.
rewrite H1; discriminate.
Qed.