CODEWITHSUNDEEP
mathlogicrelationcoqtheorem-proving
shouya
shouya

Reputation: 3083

How to describe the one-many relations in Coq?

I was reading the book Introduction to Mathematical Philosophy by B.Russell and trying to formalize all the theorems described in it.

One-many relations are described by the following text (contexts on book).

One-many relations may be defined as relations such that, if x has the relation in question to y, there is no other term x' which also has the relation to y.

Or, again, they may be defined as follows: Given two terms x and x', the terms to which x has the given relation and those to which x' has it have no member in common.

Or, again, they may be defined as relations such that the relative product of one of them and its converse implies identity, where the “relative product” of two relations R and S is that relation which holds between x and z when there is an intermediate term y, such that x has the relation R to y and y has the relation S to z.

It poses three ways of definition. I've been successfully described the first two and proved their equivalence. While I was stuck on the third, I tried to get rid of the concepts of 'relative product' and directly get to its connotation but also failed.

Here below are my definitions, did I make any mistakes?

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.

Below is how I interpret the definition of the third and also I failed to prove their equivalence.

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. *)

in which proof, id_eqv is Lemma id_eqv : forall {X} (x:X) (y:X), x = y <-> id x y, easily proved in advance.

Can somebody help me to figure out or give me a hint about where I went wrong? Thanks in advance.

Upvotes: 3

Views: 276

Answers (2)

Mark Dickinson
Mark Dickinson

Reputation: 30561

I think you've mistranslated the third definition. The original text says:

Or, again, they may be defined as relations such that the relative product of one of them and its converse implies identity

(emphasis mine). That would translate as:

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

That is, it should be a straight implication, rather than the equivalence you've asserted. You can't hope to prove your third statement from either of the others, since it's not equivalent: consider the empty relation on a nonempty set. That's certainly a one-to-many relation, but the relative product with its converse is also empty, so is not the full identity relation.

Upvotes: 5

Vinz
Vinz

Reputation: 6047

Wild guess, but you might need R to be reflexive or not empty. Using your script I end up having to prove

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

So you have a relation R, and one inhabitant y:X. To prove your goal, you need to have a witness z such that R y z and R z y. Without any other information, I guess your only shot is to have R to be reflexive and z be y.

Upvotes: 0

Related Questions