экзистенциальный квантификатор: как обращаться к экземпляру

У меня есть теорема, в которой я показываю, что существует объект, обладающий некоторым свойством. Я доказал эту теорему, построив объект. Затем, в другом доказательстве, я хотел бы сослаться на объект, определенный в первой теореме в формулировке второй теоремы. Я знаю, что объект должен быть доступен, если я закрою доказательство с помощью Defined, а не Qed, но я не знаю, как получить к нему доступ. Например:

Теорема T1: существует x, P x. Доказательство. ... Определенный.

Теорема T2: для того же x, построенного в T1, Q x \ / R x. Доказательство. ... Qed.

Как мне выразить это в Coq?


coq
person Mayer Goldberg    schedule 28.05.2012    source источник

Ответы (1)


arrow_upward
2
arrow_downward

В этом случае вы должны просто определить объект (x), используя определение.

Definition object : (...) := 
  ...

Theorem T1 : exists x, P x.
  Proof.
  exists object.
    ...
  Qed.

Theorem T2 : ...

где доказательство T2 использует тот же объект. Вы можете обнаружить, что определенные тактики (а именно, точные, вдвойне, если это что-то, что живет в Prop) помогут вам здесь, поскольку они позволяют вам легче манипулировать необработанными объектами доказательства.

person Kristopher Micinski    schedule 28.05.2012