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

(** * Classes *)

(** ** Pointwise Lemmas *)

Section Pointwise.

  Context {A : Type} {B : A -> Type} (R : forall a, Relation (B a)).

  Definition relation_pointwise : Relation (forall x, B x)
    := fun P Q => forall x, R x (P x) (Q x).

  Definition reflexive_pointwise `{!forall a, Reflexive (R a)}
    : Reflexive relation_pointwise.
A: Type
B: A -> Type
R: forall a : A, Relation (B a)
H: forall a : A, Reflexive (R a)
Reflexive relation_pointwise
  Proof.
A: Type
B: A -> Type
R: forall a : A, Relation (B a)
H: forall a : A, Reflexive (R a)
Reflexive relation_pointwise
    intros P a; reflexivity.
  Defined.

  Definition transitive_pointwise `{!forall a, Transitive (R a)}
    : Transitive relation_pointwise.
A: Type
B: A -> Type
R: forall a : A, Relation (B a)
H: forall a : A, Transitive (R a)
Transitive relation_pointwise
  Proof.
A: Type
B: A -> Type
R: forall a : A, Relation (B a)
H: forall a : A, Transitive (R a)
Transitive relation_pointwise
    intros P Q S r s a.
A: Type
B: A -> Type
R: forall a : A, Relation (B a)
H: forall a : A, Transitive (R a)
P, Q, S: forall x : A, B x
r: relation_pointwise P Q
s: relation_pointwise Q S
a: A
R a (P a) (S a)
    by transitivity (Q a).
  Defined.

  Definition symmetric_pointwise `{!forall a, Symmetric (R a)}
    : Symmetric relation_pointwise.
A: Type
B: A -> Type
R: forall a : A, Relation (B a)
H: forall a : A, Symmetric (R a)
Symmetric relation_pointwise
  Proof.
A: Type
B: A -> Type
R: forall a : A, Relation (B a)
H: forall a : A, Symmetric (R a)
Symmetric relation_pointwise
    intros P Q r a.
A: Type
B: A -> Type
R: forall a : A, Relation (B a)
H: forall a : A, Symmetric (R a)
P, Q: forall x : A, B x
r: relation_pointwise P Q
a: A
R a (Q a) (P a)
    by symmetry.
  Defined.

End Pointwise.

Hint Immediate reflexive_pointwise : typeclass_instances.
Hint Immediate transitive_pointwise : typeclass_instances.
Hint Immediate symmetric_pointwise : typeclass_instances.

Definition pointwise_precomp {A' A : Type} {B : A -> Type} (R : forall a, Relation (B a))
  (f : A' -> A) (P Q : forall x, B x)
  : relation_pointwise R P Q -> relation_pointwise (R o f) (P o f) (Q o f)
  := fun r => r o f.

(** This is easiest to state when [B] is a constant type family. *)
Definition pointwise_moveR_equiv {A A' B : Type} (R : Relation B)
  `{Reflexive _ R} `{Transitive _ R}
  (f : A' <~> A) (P : A -> B) (Q : A' -> B)
  : relation_pointwise (fun _ => R) P (Q o f^-1) -> relation_pointwise (fun _ => R) (P o f) Q.
A, A', B: Type
R: Relation B
H: Reflexive R
H0: Transitive R
f: A' <~> A
P: A -> B
Q: A' -> B
relation_pointwise (fun _ : A => R) P (Q o f^-1) ->
relation_pointwise (fun _ : A' => R) (P o f) Q
Proof.
A, A', B: Type
R: Relation B
H: Reflexive R
H0: Transitive R
f: A' <~> A
P: A -> B
Q: A' -> B
relation_pointwise (fun _ : A => R) P (Q o f^-1) ->
relation_pointwise (fun _ : A' => R) (P o f) Q
  intros r a.
A, A', B: Type
R: Relation B
H: Reflexive R
H0: Transitive R
f: A' <~> A
P: A -> B
Q: A' -> B
r: relation_pointwise (fun _ : A => R) P (Q o f^-1)
a: A'
R (P (f a)) (Q a)
  transitivity (Q (f^-1 (f a))).
A, A', B: Type
R: Relation B
H: Reflexive R
H0: Transitive R
f: A' <~> A
P: A -> B
Q: A' -> B
r: relation_pointwise (fun _ : A => R) P (Q o f^-1)
a: A'
R (P (f a)) (Q (f^-1 (f a)))
A, A', B: Type
R: Relation B
H: Reflexive R
H0: Transitive R
f: A' <~> A
P: A -> B
Q: A' -> B
r: relation_pointwise (fun _ : A => R) P (Q o f^-1)
a: A'
R (Q (f^-1 (f a))) (Q a)
  1: apply r.
A, A', B: Type
R: Relation B
H: Reflexive R
H0: Transitive R
f: A' <~> A
P: A -> B
Q: A' -> B
r: relation_pointwise (fun _ : A => R) P (Q o f^-1)
a: A'
R (Q (f^-1 (f a))) (Q a)
  rapply related_reflexive_path.
A, A', B: Type
R: Relation B
H: Reflexive R
H0: Transitive R
f: A' <~> A
P: A -> B
Q: A' -> B
r: relation_pointwise (fun _ : A => R) P (Q o f^-1)
a: A'
Q (f^-1 (f a)) = Q a
  apply (ap Q), eissect.
Defined.

Definition pointwise_moveL_equiv {A A' B : Type} (R : Relation B)
  `{Reflexive _ R} `{Transitive _ R}
  (f : A <~> A') (P : A -> B) (Q : A' -> B)
  : relation_pointwise (fun _ => R) (P o f^-1) Q -> relation_pointwise (fun _ => R) P (Q o f)
  := pointwise_moveR_equiv (flip R) f Q P.

(** ** 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 _ _.