Library HoTT.Classes.interfaces.canonical_names

Require Export
  HoTT.Basics
  HoTT.Types
  HoTT.Truncations.Core.

Declare Scope mc_scope.
Delimit Scope mc_scope with mc.
Global Open Scope mc_scope.

Generalizable Variables A B f g x y.

Monomorphic Universe Ularge Uhuge.
Monomorphic Constraint Ularge < Uhuge.

Lemma merely_destruct {A} {P : Type} {sP : IsHProp P}
  (x : merely A) : (A P) P.
Proof.
intros E;revert x.
apply Trunc_ind.
- apply _.
- exact E.
Qed.

Notation " g ∘ f " := (Compose g f)%mc.
Notation "(∘)" := Compose (only parsing) : mc_scope.

Definition id {A : Type} (a : A) := a.

Notation "(=)" := paths (only parsing) : mc_scope.
Notation "( x =)" := (paths x) (only parsing) : mc_scope.
Notation "(= x )" := (fun ypaths y x) (only parsing) : mc_scope.

Notation "(<>)" := (fun x y¬x = y) (only parsing) : mc_scope.
Notation "( x <>)" := (fun yx y) (only parsing) : mc_scope.
Notation "(<> x )" := (fun yy x) (only parsing) : mc_scope.

Class Apart A := apart : Relation A.
Infix "≶" := apart : mc_scope.
Notation "(≶)" := apart (only parsing) : mc_scope.
Notation "( x ≶)" := (apart x) (only parsing) : mc_scope.
Notation "(≶ x )" := (fun yapart y x) (only parsing) : mc_scope.

(* Even for setoids with decidable equality x <> y does not imply x ≶ y.
Therefore we introduce the following class. *)

Class TrivialApart A {Aap : Apart A} :=
  { trivial_apart_prop : is_mere_relation A apart
  ; trivial_apart : x y, x y x y }.
#[export] Existing Instance trivial_apart_prop.

Definition sig_apart `{Apart A} (P: A Type) : Apart (sig P) := fun x yx.1 y.1.
#[export]
Hint Extern 10 (Apart (sig _)) ⇒ apply @sig_apart : typeclass_instances.

Class Cast A B := cast: A B.
Arguments cast _ _ {Cast} _.
Notation "' x" := (cast _ _ x) : mc_scope.
#[global] Typeclasses Transparent Cast.

(* Other canonically named relations/operations/constants: *)
Class SgOp A := sg_op: A A A.
Class MonUnit A := mon_unit: A.
Class Plus A := plus: A A A.
Class Mult A := mult: A A A.
Class One A := one: A.
Class Zero A := zero: A.
Class Negate A := negate: A A.
Class DecRecip A := dec_recip: A A.
Definition ApartZero R `{Zero R} `{Apart R} := sig (≶ zero).
Class Recip A `{Apart A} `{Zero A} := recip: ApartZero A A.
#[global] Typeclasses Transparent SgOp MonUnit Plus Mult Zero One Negate.

Class Meet A := meet: A A A.
Class Join A := join: A A A.
Class Top A := top: A.
Class Bottom A := bottom: A.
#[global] Typeclasses Transparent Meet Join Top Bottom.

Class Le A := le: Relation A.
Class Lt A := lt: Relation A.
#[global] Typeclasses Transparent Le Lt.

Definition NonNeg R `{Zero R} `{Le R} := sig (le zero).
Definition Pos R `{Zero R} `{Lt R} := sig (lt zero).
Definition NonPos R `{Zero R} `{Le R} := sig (fun yle y zero).

Global Instance plus_is_sg_op `{f : Plus A} : SgOp A := f.
Global Instance mult_is_sg_op `{f : Mult A} : SgOp A := f.
Global Instance one_is_mon_unit `{c : One A} : MonUnit A := c.
Global Instance zero_is_mon_unit `{c : Zero A} : MonUnit A := c.
Global Instance meet_is_sg_op `{f : Meet A} : SgOp A := f.
Global Instance join_is_sg_op `{f : Join A} : SgOp A := f.
Global Instance top_is_mon_unit `{s : Top A} : MonUnit A := s.
Global Instance bottom_is_mon_unit `{s : Bottom A} : MonUnit A := s.

#[export]
Hint Extern 4 (Apart (ApartZero _)) ⇒ apply @sig_apart : typeclass_instances.
#[export]
Hint Extern 4 (Apart (NonNeg _)) ⇒ apply @sig_apart : typeclass_instances.
#[export]
Hint Extern 4 (Apart (Pos _)) ⇒ apply @sig_apart : typeclass_instances.

We group these notations into a module, so that just this subset can be exported in some cases.
Module Export BinOpNotations.
(* Notations: *)
Declare Scope mc_add_scope.
Infix "+" := sg_op : mc_add_scope.
Notation "(+)" := sg_op (only parsing) : mc_add_scope.
Notation "( x +)" := (sg_op x) (only parsing) : mc_add_scope.
Notation "(+ x )" := (fun ysg_op y x) (only parsing) : mc_add_scope.

Declare Scope mc_mult_scope.
Infix "×" := sg_op : mc_mult_scope.
Notation "( x *.)" := (sg_op x) (only parsing) : mc_mult_scope.
Notation "(.*.)" := sg_op (only parsing) : mc_mult_scope.
Notation "(.* x )" := (fun ysg_op y x) (only parsing) : mc_mult_scope.

Infix "+" := plus : mc_scope.
Notation "(+)" := plus (only parsing) : mc_scope.
Notation "( x +)" := (plus x) (only parsing) : mc_scope.
Notation "(+ x )" := (fun yy + x) (only parsing) : mc_scope.

Infix "×" := mult : mc_scope.
(* We don't add "( * )", "( * x )" and "( x * )" notations
   because they conflict with comments. *)

Notation "( x *.)" := (mult x) (only parsing) : mc_scope.
Notation "(.*.)" := mult (only parsing) : mc_scope.
Notation "(.* x )" := (fun yy × x) (only parsing) : mc_scope.

Notation "- x" := (negate x) : mc_scope.
Notation "(-)" := negate (only parsing) : mc_scope.
Notation "x - y" := (x + -y) : mc_scope.

Notation "0" := zero : mc_scope.
Notation "1" := one : mc_scope.
Notation "2" := (1 + 1) : mc_scope.
Notation "3" := (1 + (1 + 1)) : mc_scope.
Notation "4" := (1 + (1 + (1 + 1))) : mc_scope.
Notation "5" := (1 + (1 + (1 + (1 + 1)))) : mc_scope.
Notation "6" := (1 + (1 + (1 + (1 + (1 + 1))))) : mc_scope.
Notation "- 1" := (-(1)) : mc_scope.
Notation "- 2" := (-(2)) : mc_scope.
Notation "- 3" := (-(3)) : mc_scope.
Notation "- 4" := (-(4)) : mc_scope.
End BinOpNotations.

Notation "/ x" := (dec_recip x) : mc_scope.
Notation "(/)" := dec_recip (only parsing) : mc_scope.
Notation "x / y" := (x × /y) : mc_scope.

Notation "// x" := (recip x) : mc_scope.
Notation "(//)" := recip (only parsing) : mc_scope.
Notation "x // y" := (x × //y) : mc_scope.

Notation "⊤" := top : mc_scope.
Notation "⊥" := bottom : mc_scope.

Infix "⊓" := meet : mc_scope.
Notation "(⊓)" := meet (only parsing) : mc_scope.
Notation "( X ⊓)" := (meet X) (only parsing) : mc_scope.
Notation "(⊓ X )" := (fun YY X) (only parsing) : mc_scope.

Infix "⊔" := join : mc_scope.
Notation "(⊔)" := join (only parsing) : mc_scope.
Notation "( X ⊔)" := (join X) (only parsing) : mc_scope.
Notation "(⊔ X )" := (fun YY X) (only parsing) : mc_scope.

Infix "≤" := le : mc_scope.
Notation "(≤)" := le (only parsing) : mc_scope.
Notation "( x ≤)" := (le x) (only parsing) : mc_scope.
Notation "(≤ x )" := (fun yy x) (only parsing) : mc_scope.

Infix "≤" := le (only parsing) : mc_scope.
Notation "(<=)" := le (only parsing) : mc_scope.
Notation "( x <=)" := (le x) (only parsing) : mc_scope.
Notation "(<= x )" := (fun yy x) (only parsing) : mc_scope.

Infix "<" := lt : mc_scope.
Notation "(<)" := lt (only parsing) : mc_scope.
Notation "( x <)" := (lt x) (only parsing) : mc_scope.
Notation "(< x )" := (fun yy < x) (only parsing) : mc_scope.

Notation "x ≤ y ≤ z" := (x y y z) : mc_scope.
Notation "x ≤ y < z" := (x y y < z) : mc_scope.
Notation "x < y < z" := (x < y y < z) : mc_scope.
Notation "x < y ≤ z" := (x < y y z) : mc_scope.

It is likely that ≤ and < are transitive (and ≤ reflexive) so inform auto of this.
Ltac auto_trans := match goal with
                    [ H: ?R ?x ?y, I: ?R ?y ?z |- ?R ?x ?z] ⇒ apply (transitivity H I)
                  end.

#[export]
Hint Extern 2 (?x ?y) ⇒ reflexivity : core.
#[export]
Hint Extern 4 (?x ?z) ⇒ auto_trans : core.
#[export]
Hint Extern 4 (?x < ?z) ⇒ auto_trans : core.

Class Abs A `{Le A} `{Zero A} `{Negate A}
  := abs_sig: (x : A), { y : A | (0 x y = x) (x 0 y = -x)}.
Definition abs `{Abs A} := fun x : A(abs_sig x).1.

(* Common properties: *)
(* Class Inverse `(A -> B) : Type := inverse: B -> A.
Arguments inverse {A B} _ {Inverse} _.
Typeclasses Transparent Inverse.
Notation "f ⁻¹" := (inverse f) : mc_scope. *)


Class Idempotent `(f: A A A) (x : A) : Type := idempotency: f x x = x.
Arguments idempotency {A} _ _ {Idempotent}.

Class UnaryIdempotent {A} (f: A A) : Type :=
  unary_idempotent : Idempotent Compose f.
#[export] Existing Instances unary_idempotent.

Lemma unary_idempotency `{UnaryIdempotent A f} x : f (f x) = f x.
Proof.
change (f (f x)) with (Compose f f x).
apply (ap (fun gg x)).
change (Compose f f = f).
apply idempotency. apply _.
Qed.

Class BinaryIdempotent `(op: A A A) : Type
  := binary_idempotent : x, Idempotent op x.
#[export] Existing Instances binary_idempotent.

Class LeftIdentity {A B} (op : A B B) (x : A): Type
  := left_identity: y, op x y = y.
Class RightIdentity {A B} (op : A B A) (y : B): Type
  := right_identity: x, op x y = x.

Class Absorption {A B C} (op1: A C A) (op2: A B C) : Type
  := absorption: x y, op1 x (op2 x y) = x.

Class LeftAbsorb {A B} (op : A B A) (x : A): Type
  := left_absorb: y, op x y = x.
Class RightAbsorb {A B} (op : A B B) (y : B): Type
  := right_absorb: x, op x y = y.

Class LeftInverse {A} {B} {C} (op : A B C) (inv : B A) (unit : C)
  := left_inverse: x, op (inv x) x = unit.
Class RightInverse {A} {B} {C} (op : A B C) (inv : A B) (unit : C)
  := right_inverse: x, op x (inv x) = unit.

Class Commutative {B A} (f : A A B) : Type
  := commutativity: x y, f x y = f y x.

#[global] Typeclasses Transparent Commutative.

Class HeteroAssociative {A B C AB BC ABC}
  (fA_BC: A BC ABC) (fBC: B C BC)
  (fAB_C: AB C ABC) (fAB : A B AB): Type
  := associativity : x y z, fA_BC x (fBC y z) = fAB_C (fAB x y) z.
Class Associative {A} (f : A A A)
  := simple_associativity : HeteroAssociative f f f f.
#[export] Existing Instances simple_associativity.

Class Involutive {A} (f : A A) := involutive: x, f (f x) = x.

Class TotalRelation `(R : Relation A) : Type := total : x y : A, R x y |_| R y x.
Arguments total {A} _ {TotalRelation} _ _.

Class Trichotomy `(R : Relation A)
  := trichotomy : x y : A, R x y |_| x = y |_| R y x.
Arguments trichotomy {A} R {Trichotomy} _ _.

Arguments irreflexivity {A} _ {Irreflexive} _ _.

Class CoTransitive `(R : Relation A) : Type := cotransitive
  : x y, R x y z, hor (R x z) (R z y).
Arguments cotransitive {A R CoTransitive x y} _ _.

Class EquivRel `(R : Relation A) : Type := Build_EquivRel
  { EquivRel_Reflexive : Reflexive R ;
    EquivRel_Symmetric : Symmetric R ;
    EquivRel_Transitive : Transitive R }.
#[export] Existing Instances EquivRel_Reflexive EquivRel_Symmetric EquivRel_Transitive.

Definition SigEquivRel {A:Type} (R : Relation A) : Type :=
  {_ : Reflexive R | { _ : Symmetric R | Transitive R}}.

Global Instance trunc_sig_equiv_rel `{Funext} {A : Type}
  (R : Relation A) {n} `{! (x y : A), IsTrunc n (R x y)}
  : IsTrunc n (SigEquivRel R).
Proof.
  apply @istrunc_sigma.
  - apply istrunc_forall.
  - intros. apply @istrunc_sigma; intros; apply istrunc_forall.
Defined.

Lemma issig_equiv_rel {A:Type} (R : Relation A)
  : SigEquivRel R <~> EquivRel R.
Proof.
  issig.
Defined.

Global Instance istrunc_equiv_rel `{Funext} {A : Type}
  (R : Relation A) {n} `{! (x y : A), IsTrunc n (R x y)}
  : IsTrunc n (EquivRel R).
Proof.
  exact (istrunc_equiv_istrunc (SigEquivRel R) (issig_equiv_rel R)).
Qed.

Class Conjugate A := conj : A A.

Class DistrOpp {A} `(SgOp A) `(Conjugate A)
  := distropp : x y : A, conj (sg_op x y) = sg_op (conj y) (conj x).

Class SwapOp {A} `(Negate A) `(Conjugate A)
  := swapop : x, conj (-x) = - (conj x).

Class FactorNegLeft {A} `(Negate A) `(SgOp A)
  := factorneg_l : x y, sg_op (-x) y = - (sg_op x y).

Class FactorNegRight {A} `(Negate A) `(SgOp A)
  := factorneg_r : x y, sg_op x (-y) = - (sg_op x y).

Class LeftHeteroDistribute {A B C}
  (f : A B C) (g_r : B B B) (g : C C C) : Type
  := distribute_l : a b c, f a (g_r b c) = g (f a b) (f a c).
Class RightHeteroDistribute {A B C}
  (f : A B C) (g_l : A A A) (g : C C C) : Type
  := distribute_r: a b c, f (g_l a b) c = g (f a c) (f b c).
Class LeftDistribute {A} (f g: A A A)
  := simple_distribute_l : LeftHeteroDistribute f g g.
#[export] Existing Instances simple_distribute_l.
Class RightDistribute {A} (f g: A A A)
  := simple_distribute_r : RightHeteroDistribute f g g.
#[export] Existing Instances simple_distribute_r.

Class HeteroSymmetric {A} {T : A A Type}
  (R : {x y}, T x y T y x Type) : Type
  := hetero_symmetric `(a : T x y) (b : T y x) : R a b R b a.

(* Although cancellation is the same as being injective, we want a proper
  name to refer to this commonly used property. *)

Section cancellation.
  Context `(op : A A A) (z : A).

  Class LeftCancellation := left_cancellation : x y, op z x = op z y x = y.
  Class RightCancellation := right_cancellation : x y, op x z = op y z x = y.

  Context {Aap : Apart A}.

  Class StrongLeftCancellation := strong_left_cancellation
    : x y, x y op z x op z y.
  Class StrongRightCancellation := strong_right_cancellation
    : x y, x y op x z op y z.
End cancellation.

(* Common names for properties that hold in N, Z, Q, ... *)
Class ZeroProduct A `{!Mult A} `{!Zero A} : Type
  := zero_product : x y, x × y = 0 x = 0 |_| y = 0.

Class ZeroDivisor {R} `{Zero R} `{Mult R} (x : R) : Type
  := zero_divisor : x 0 y, y 0 x × y = 0.

Class NoZeroDivisors R `{Zero R} `{Mult R} : Type
  := no_zero_divisors x : ¬ZeroDivisor x.

Global Instance zero_product_no_zero_divisors `{ZeroProduct A}
  : NoZeroDivisors A.
Proof.
intros x [? [? [? E]]].
destruct (zero_product _ _ E); auto.
Qed.

(* A common induction principle for both the naturals and integers *)
Class Biinduction R `{Zero R} `{One R} `{Plus R} : Type
  := biinduction (P : R Type)
  : P 0 ( n, P n P (1 + n)) n, P n.

Additional operations
Class CutMinus A := cut_minus : A A A.
Infix "∸" := cut_minus : mc_scope.
Notation "(∸)" := cut_minus (only parsing) : mc_scope.
Notation "( x ∸)" := (cut_minus x) (only parsing) : mc_scope.
Notation "(∸ y )" := (fun xx y) (only parsing) : mc_scope.

Inductive comparison : Set := LT | EQ | GT.

Class Compare A := compare : A A comparison.
Infix "?=" := compare : mc_scope.
Notation "(?=)" := compare (only parsing) : mc_scope.
Notation "( x ?=)" := (compare x) (only parsing) : mc_scope.
Notation "(?= y )" := (fun xx ?= y) (only parsing) : mc_scope.

Class Eqb A := eqb : A A Bool.
Infix "=?" := eqb : mc_scope.
Notation "(=?)" := eqb (only parsing) : mc_scope.
Notation "( x =?)" := (eqb x) (only parsing) : mc_scope.
Notation "(=? y )" := (fun xx =? y) (only parsing) : mc_scope.

Class Ltb A := ltb : A A Bool.
Infix "<?" := ltb : mc_scope.
Notation "(<?)" := ltb (only parsing) : mc_scope.
Notation "( x <?)" := (ltb x) (only parsing) : mc_scope.
Notation "(<? y )" := (fun xx <? y) (only parsing) : mc_scope.

Class Leb A := leb : A A Bool.
Infix "<=?" := leb : mc_scope.
Notation "(<=?)" := leb (only parsing) : mc_scope.
Notation "( x <=?)" := (leb x) (only parsing) : mc_scope.
Notation "(<=? y )" := (fun xx <=? y) (only parsing) : mc_scope.

Class Return (M : Type Type) := ret : {A}, A M A.

Class Bind (M : Type Type) := bind : {A B}, M A (A M B) M B.

Class Enumerable@{i} (A : Type@{i}) :=
  { enumerator : nat A
  ; enumerator_issurj : IsSurjection enumerator }.
#[export] Existing Instance enumerator_issurj.
Arguments enumerator A {_} _.
Arguments enumerator_issurj A {_} _.

(*
  The following class is nice to parametrize instances by additional properties, for example:
   z, PropHolds (z 0) LeftCancellation op z
  This tool is very powerful as we can combine it with instances as:
   x y, PropHolds (x 0) PropHolds (y 0) PropHolds (x × y 0)
  Of course, one should be very careful not to make too many instances as that could
  easily lead to a blow-up of the search space (or worse, cycles).
*)

Class PropHolds (P : Type) := prop_holds: P.

#[export]
Hint Extern 0 (PropHolds _) ⇒ assumption : typeclass_instances.

Ltac solve_propholds :=
  match goal with
  | [ |- PropHolds (?P) ] ⇒ apply _
  | [ |- ?P ] ⇒ change (PropHolds P); apply _
  end.