Coq中分号的奇怪行为

我在理解为什么我的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.

来源

2011-05-23 Ptival

所以，这可能是一个答案，以我自己的问题（感谢有人#coq IRC频道）：

这可能是这样的情况的直到. 才会发生存在变量的统一因此，通过分号，我可能会阻止统一和c。

但我发现虽然写...; eauto; subst; rewrite H1; discriminate.将工作。 subst会在这种情况下强制存在变量的统一，从而解锁重写的能力。

来源

2011-05-24 04:13:17 Ptival

Coq中分号的奇怪行为

回答

相关问题