map_rel_example.v

Definition gen_rel (X Y : Type) := X -> Y -> Prop.

Definition map_rel {X Y : Type} (R : gen_rel X Y) :=
  forall x x', x = x' -> forall y y', R x y -> R x' y' -> y = y'.
Arguments map_rel {X Y} R/.

Definition map_rel' {X Y : Type} (R : gen_rel X Y) :=
  forall x, exists! y, R x y.
Arguments map_rel' {X Y} R/.

Inductive hoge : nat -> nat -> Prop :=
| hoge_1_2 : hoge 1 2
| hoge_1_3 : hoge 1 3.

Theorem hoge_is_not_map_rel : ~ map_rel hoge.
Proof.
  simpl.
  intro.
  specialize H with (x:=1) (x':=1).
  assert (1 = 1) by reflexivity.
  assert (H1 := H H0 2 3).
  assert (H2 := H1 hoge_1_2 hoge_1_3).
  discriminate.
Qed.

Theorem hoge_is_not_map_rel' : ~ map_rel' hoge.
Proof.
  simpl.
  intro.
  specialize H with (x:=1).
  inversion H.
  inversion H0.
  inversion H1.
  -
    assert (H3 := H2 3 hoge_1_3).
    rewrite H3 in H4.
    discriminate.
  -
    assert (H3 := H2 2 hoge_1_2).
    rewrite H3 in H4.
    discriminate.
Qed.