1

Coqコードが以下のコードで期待することを実行しない理由を理解するのに問題があります。

  • 例をできるだけ単純化しようとしましたが、さらに単純化しても問題は発生しなくなりました。
  • CompCert1.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; discriminate2回は機能しますが、セミコロンを使用した後に「配管」すること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.
4

1 に答える 1

3

したがって、これは私自身の質問に対する答えかもしれません (#coq IRC チャンネルの誰かに感謝します):

存在変数の統一が まで起こらない場合もありえます。. したがって、セミコロンを付けることで、ofsandcが統一されないようにすることができたかもしれません。

しかし、私が見つけたのは、書く...; eauto; subst; rewrite H1; discriminate.ことがうまくいくということです。substこの場合、存在変数の統合を強制するため、書き換え機能がロック解除されます。

于 2011-05-24T04:13:17.590 に答える