Странное поведение точки с запятой в Coq - PullRequest
Новая
       4

Странное поведение точки с запятой в Coq

1 голос
/ 24 мая 2011

У меня проблемы с пониманием того, почему мой код 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.

Это работает, хотя: 

  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.

1 Ответ

3 голосов
/ 24 мая 2011

Итак, это может быть ответом на мой вопрос (спасибо кому-то на IRC-канале #coq):

Может случиться так, что объединение экзистенциальных переменных не произойдет, пока . Поэтому, используя точку с запятой, я мог бы предотвратить объединение ofs и c.

Я обнаружил, что написание ...; eauto; subst; rewrite H1; discriminate. будет работать. subst в этом случае вызовет объединение экзистенциальных переменных, следовательно, разблокирует возможность перезаписи.

...