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 y ⇒ paths y x) (only parsing) : mc_scope.
Notation "(<>)" := (fun x y ⇒ ¬x = y) (only parsing) : mc_scope.
Notation "( x <>)" := (fun y ⇒ x ≠ y) (only parsing) : mc_scope.
Notation "(<> x )" := (fun y ⇒ y ≠ 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 y ⇒ apart 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 y ⇒ x.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 y ⇒ le 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.
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 y ⇒ paths y x) (only parsing) : mc_scope.
Notation "(<>)" := (fun x y ⇒ ¬x = y) (only parsing) : mc_scope.
Notation "( x <>)" := (fun y ⇒ x ≠ y) (only parsing) : mc_scope.
Notation "(<> x )" := (fun y ⇒ y ≠ 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 y ⇒ apart 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 y ⇒ x.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 y ⇒ le 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 y ⇒ sg_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 y ⇒ sg_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 y ⇒ y + 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 y ⇒ y × 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 Y ⇒ Y ⊓ 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 Y ⇒ Y ⊔ 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 y ⇒ y ≤ 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 y ⇒ y ≤ 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 y ⇒ y < 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.
(* 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 y ⇒ sg_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 y ⇒ sg_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 y ⇒ y + 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 y ⇒ y × 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 Y ⇒ Y ⊓ 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 Y ⇒ Y ⊔ 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 y ⇒ y ≤ 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 y ⇒ y ≤ 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 y ⇒ y < 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 g ⇒ g 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 AntiSymmetric `(R : Relation A) : Type
:= antisymmetry: ∀ x y, R x y → R y x → x = y.
Arguments antisymmetry {A} _ {AntiSymmetric} _ _ _ _.
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.
[ 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 g ⇒ g 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 AntiSymmetric `(R : Relation A) : Type
:= antisymmetry: ∀ x y, R x y → R y x → x = y.
Arguments antisymmetry {A} _ {AntiSymmetric} _ _ _ _.
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 x ⇒ x ∸ 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 x ⇒ x ?= 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 x ⇒ x =? 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 x ⇒ x <? 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 x ⇒ x <=? 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.
Infix "∸" := cut_minus : mc_scope.
Notation "(∸)" := cut_minus (only parsing) : mc_scope.
Notation "( x ∸)" := (cut_minus x) (only parsing) : mc_scope.
Notation "(∸ y )" := (fun x ⇒ x ∸ 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 x ⇒ x ?= 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 x ⇒ x =? 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 x ⇒ x <? 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 x ⇒ x <=? 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.