#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.
Это работает, хотя:
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
twice работает, но «конвейеризация» его после 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:
Итак, это может быть ответом на мой собственный вопрос (благодаря кому-то на IRC-канале #coq):
Могло случиться так, что объединение экзистенциальных переменных не произойдет до .
Поэтому, поставив точку с запятой, я, возможно, предотвратил бы объединение ofs
и c
.
Однако я выяснил, что запись ...; eauto; subst; rewrite H1; discriminate.
будет работать. subst
в этом случае это привело бы к принудительному объединению экзистенциальных переменных, следовательно, открыло бы возможность перезаписи.