Coq中分号的奇异行为

Question

我很难理解为什么我的Coq代码没有按照我在下面代码中所期望的那样做。

• 我试着使这个例子尽可能简化，但是当我使它变得更简单的时候，这个问题就不再出现了。
• 它在使用CompCert 1.8文件。
• 在Coq8.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.

不过，这样做是可行的：

  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之后，我的目标是：

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之后使用分号“管道”不起作用。

我希望这个问题至少有意义。谢谢!

完整代码：

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.

Answer 1

因此，这可能是我自己问题的答案(感谢#coq频道上的某个人)：

存在变量的统一可能是在.之前不会发生的，因此，通过分号，我可能阻止了ofs和c的统一。

不过，我发现，编写...; eauto; subst; rewrite H1; discriminate.是可行的。在这种情况下，subst将强制统一存在变量，从而解除重写的能力。