Что является хорошим примером простого доказательства в Coq, где заключение имеет экзистенциальный квантификатор? - PullRequest
Новая
       4

Что является хорошим примером простого доказательства в Coq, где заключение имеет экзистенциальный квантификатор?

0 голосов
/ 22 декабря 2018

Я хотел бы увидеть несколько раздач на примерах доказательств Кока в форме: 

\exists A(x1,...,xn)

по существу там, где у Цели был экзистенциальный квантификатор.У меня были проблемы с манипулированием целью осмысленным образом, чтобы добиться прогресса в моих доказательствах, и я хотел увидеть несколько примеров общей тактики для манипулирования.

Какие примеры хороших экзистенциальных квантификаторов в Coq могут доказать?

Мой конкретный пример, который у меня был: 

Theorem Big_Small_ForwardImpl   :
  forall (P : Program) (S' : State),
    (BigStepR (B_PgmConf P) (B_StateConf S')) -> (ConfigEquivR (S_PgmConf P) (S_BlkConf EmptyBlk S')).
Proof.
  intros.
  induction P.
  unfold ConfigEquivR.
  refine (ex_intro _ _ _) .

, мой контекст и цели были: 

1 subgoal
l : list string
s : Statement
S' : State
H : BigStepR (B_PgmConf (Pgm l s)) (B_StateConf S')
______________________________________(1/1)
exists N : nat, NSmallSteps N (S_PgmConf (Pgm l s)) (S_BlkConf EmptyBlk S')

, но затем изменился на: 

1 subgoal
l : list string
s : Statement
S' : State
H : BigStepR (B_PgmConf (Pgm l s)) (B_StateConf S')
______________________________________(1/1)
NSmallSteps ?Goal (S_PgmConf (Pgm l s)) (S_BlkConf EmptyBlk S')

после использования тактики refine (ex_intro _ _ _).Поскольку я не уверен, что происходит, я надеялся, что некоторые более простые примеры могут показать мне, как манипулировать экзистенциальными квантификаторами в моей цели Coq.

полезный комментарий:

«Цель была введена Coq в качестве заполнителя для некоторого N, который должен быть выведен позже в доказательстве.

1 Ответ

0 голосов
/ 22 декабря 2018

Следующий пример основан на коде, представленном в этом ответе .

Предположим, у нас есть тип T и двоичное отношение R для элементов типа T,Для целей этого примера мы можем определить их следующим образом. 

Variable T : Type.
Variable R : T -> T -> Prop.

Докажем следующую простую теорему. 

Theorem test : forall x y, R x y -> exists t, R x t.

Вот возможное решение. 

Proof.
  intros. exists y. apply H.
Qed.

Вместо того, чтобы явно указать, что y - это элемент, который мы ищем, мы можем положиться на мощные механизмы автоматического доказательства Coq, чтобы автоматически определить, какая переменная удовлетворяет R x t: 

Proof.
  intros.
  eexists. (* Introduce a temporary placeholder of the form ?t *)
  apply H. (* Coq can deduce from the hypothesis H that ?t must be y *)
Qed.

Существует множество тактик, которые используют одни и те же автоматические механизмы вывода, такие как eexists, eapply, eauto и т. Д.

Обратите внимание, что их имена часто соответствуют обычной тактике с префиксом e.

...