Require Import Basics.Overture Basics.Tactics.
[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]

(** * Classes *)

(** ** Injective Functions *)

Class IsInjective {A B : Type} (f : A -> B)
  := injective : forall x y, f x = f y -> x = y.
Arguments injective {A B} f {_} _ _.

Definition neq_isinj {A B : Type} (f : A -> B) `{!IsInjective f}
  : forall x y, x <> y -> f x <> f y.
A, B: Type
f: A -> B
IsInjective0: IsInjective f
forall x y : A, x <> y -> f x <> f y
Proof.
A, B: Type
f: A -> B
IsInjective0: IsInjective f
forall x y : A, x <> y -> f x <> f y
  intros x y np q.
A, B: Type
f: A -> B
IsInjective0: IsInjective f
x, y: A
np: x <> y
q: f x = f y
Empty
  apply np, (injective f).
A, B: Type
f: A -> B
IsInjective0: IsInjective f
x, y: A
np: x <> y
q: f x = f y
f x = f y
  exact q.
Defined.

Instance isinj_idmap A : @IsInjective A A idmap
  := fun x y => idmap.

#[export] Hint Unfold IsInjective : typeclass_instances.

Definition isinj_compose {A B C f g} `{IsInjective B C g} `{IsInjective A B f}
  : IsInjective (g o f).
A, B, C: Type
f: A -> B
g: B -> C
H: IsInjective g
H0: IsInjective f
IsInjective (g o f)
Proof.
A, B, C: Type
f: A -> B
g: B -> C
H: IsInjective g
H0: IsInjective f
IsInjective (g o f)
  intros x y p.
A, B, C: Type
f: A -> B
g: B -> C
H: IsInjective g
H0: IsInjective f
x, y: A
p: g (f x) = g (f y)
x = y
  by apply (injective f), (injective g).
Defined.
#[export] Hint Immediate isinj_compose : typeclass_instances.

Definition isinj_cancelL {A B C : Type} (f : A -> B) (g : B -> C)
  `{!IsInjective (g o f)}
  : IsInjective f.
A, B, C: Type
f: A -> B
g: B -> C
IsInjective0: IsInjective (g o f)
IsInjective f
Proof.
A, B, C: Type
f: A -> B
g: B -> C
IsInjective0: IsInjective (g o f)
IsInjective f
  intros x y p.
A, B, C: Type
f: A -> B
g: B -> C
IsInjective0: IsInjective (g o f)
x, y: A
p: f x = f y
x = y
  apply (injective (g o f)).
A, B, C: Type
f: A -> B
g: B -> C
IsInjective0: IsInjective (g o f)
x, y: A
p: f x = f y
g (f x) = g (f y)
  exact (ap g p).
Defined.

(** ** Antisymmetric Relations *)

Class AntiSymmetric {A : Type} (R : A -> A -> Type) : Type
  := antisymmetry : forall x y, R x y -> R y x -> x = y.
Arguments antisymmetry {A} R {AntiSymmetric} x y _ _.