Как описать отношения "один-много" в Coq?

Я читал книгу Б. Рассела «Введение в математическую философию» и пытался формализовать все описанные в ней теоремы.

Отношения "один-много" описываются следующим текстом (контексты в книге ).

Отношения «один-много» можно определить как отношения, такие, что, если x имеет рассматриваемое отношение к y, не существует другого термина x ', который также имел бы отношение к y.

Или, опять же, они могут быть определены следующим образом: даны два термина x и x ', термины, к которым x имеет данное отношение, и те, с которыми x' имеет это отношение, не имеют общего члена.

Или, опять же, они могут быть определены как отношения, такие, что относительный продукт одного из них и его обратное подразумевает идентичность, где «относительный продукт» двух отношений R и S - это отношение, которое выполняется между x и z, когда существует промежуточный член y, такой, что x имеет отношение R к y, а y имеет отношение S к z.

Он предлагает три способа определения. Я успешно описал первые два и доказал их эквивалентность. Пока я застрял на третьем, я попытался избавиться от концепции «относительного продукта» и напрямую перейти к его коннотации, но тоже потерпел неудачу.

Вот мои определения, допустил ли я какие-нибудь ошибки?

Definition one_many {X} (R : relation X) : Prop :=
  forall x y, R x y -> forall x', x <> x' -> ~(R x' y).

Definition one_many' {X} (R : relation X) : Prop :=
  forall x x' y, R x y -> R x' y -> x = x'.

Inductive relative_product
          {X} (R: relation X) (S: relation X) : relation X :=
  | rp0 : forall x y, forall z, R x y -> S y z -> relative_product R S x z.
Inductive converse {X} (R : relation X) : relation X :=
  | cv0 : forall x y, R x y -> converse R y x.
Inductive id {X} : relation X :=
  | id0 : forall x, id x x.

Definition one_many'' {X} (R : relation X) : Prop :=
  forall x y, relative_product R (converse R) x y <-> id x y.

Ниже я интерпретирую определение третьего, и мне также не удалось доказать их эквивалентность.

Goal forall {X} (R : relation X),
    one_many'' R <-> (forall x y, R x y -> forall x', converse R y x' -> x = x').
Proof.
  intros. unfold one_many''. split.

  intros.
  assert (relative_product R (converse R) x x' <-> id x x'). apply H.
  inversion H2. apply id_eqv. apply H3.
  apply rp0 with y. assumption. assumption.

  intros.
  split. intro.
  inversion H0. subst.
  apply id_eqv. apply H with y0.
  assumption. assumption.

   (* I'm stuck here. This subgoal is obviously not provable. *)

в котором доказательство id_eqv равно Lemma id_eqv : forall {X} (x:X) (y:X), x = y <-> id x y, легко доказывается заранее.

Может ли кто-нибудь помочь мне разобраться или намекнуть, где я ошибся? Заранее спасибо.


relation logic math theorem-proving coq
person Shou Ya    schedule 25.08.2014    source источник
comment
Как вы определяете relation? Не могли бы вы поделиться остальными своими определениями?   -  person sinan    schedule 25.08.2014
comment
sinan: отношение напрямую взято из стандартной библиотеки Relations, которая равна Definition relation (X:Type) := X -> X -> Prop.   -  person Shou Ya    schedule 25.08.2014
comment
id_eqv также определен в stdlib? У меня проблемы с поиском необходимых определений.   -  person sinan    schedule 25.08.2014
comment
sinan: Извини, я пропустил это. Я доказал id_eqv себя. Lemma id_eqv : forall {X} (x:X) (y:X), x = y <-> id x y.   -  person Shou Ya    schedule 25.08.2014
comment
Вам нужно R x y <-> converse R y x в вашем определении обратного отношения, или легко доказать converse R y x -> R x y с учетом этого определения?   -  person Mark Dickinson    schedule 25.08.2014

Ответы (2)


arrow_upward
5
arrow_downward

Думаю, вы неправильно перевели третье определение. В оригинальном тексте говорится:

Или, опять же, они могут быть определены как отношения, в которых относительный продукт одного из них и его обратное подразумевают идентичность.

(курсив мой). Это можно перевести как:

forall x y, relative_product R (converse R) x y -> id x y

То есть это должно быть прямым следствием, а не эквивалентностью, которую вы утверждали. Вы не можете надеяться доказать свое третье утверждение ни одним из других, поскольку оно не эквивалентно: рассмотрите пустое отношение на непустом множестве. Это определенно отношение «один ко многим», но относительный продукт с обратным ему тоже пуст, так что это не полное отношение идентичности.

person Mark Dickinson    schedule 25.08.2014

arrow_upward
0
arrow_downward

Дикое предположение, но вам может понадобиться R быть рефлексивным или непустым. Используя ваш сценарий, мне нужно доказать

1 subgoal
X : Type
R : relation X
H : forall x y : X, R x y -> forall x' : X, converse R y x' -> x = x'
y : X
______________________________________(1/1)
relative_product R (converse R) y y

Итак, у вас есть родственник R и один житель y:X. Чтобы доказать свою цель, вам нужен свидетель z, такой, что R y z и R z y. Без какой-либо другой информации, я думаю, ваш единственный шанс - иметь R рефлексивным и z y.

person Vinz    schedule 25.08.2014