Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Typeclass hints #2254

Open
wants to merge 5 commits into
base: master
Choose a base branch
from
Open

Typeclass hints #2254

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
5 commits
Select commit Hold shift + click to select a range
76811bc
first round of patches after commits
Mar 12, 2025
8daae09
some more exports
Mar 14, 2025
35cd5db
Spelling and style changes
Mar 11, 2025
9cdc153
Fixed reviewer comments.
Mar 11, 2025
26b3e29
all exports
Mar 14, 2025
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
8 changes: 4 additions & 4 deletions theories/Algebra/ooGroup.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -218,25 +218,25 @@ Section Subgroups.
Definition in_coset : G -> G -> Type
:= fun g1 g2 => hfiber incl (g1 @ g2^).

Instance ishprop_in_coset : is_mere_relation G in_coset.
#[export] Instance ishprop_in_coset : is_mere_relation G in_coset.
Proof.
exact _.
Defined.

Instance reflexive_coset : Reflexive in_coset.
#[export] Instance reflexive_coset : Reflexive in_coset.
Proof.
intros g.
exact (1 ; grouphom_1 incl @ (concat_pV g)^).
Defined.

Instance symmetric_coset : Symmetric in_coset.
#[export] Instance symmetric_coset : Symmetric in_coset.
Proof.
intros g1 g2 [h p].
exists (h^).
exact (grouphom_V incl h @ inverse2 p @ inv_pp _ _ @ whiskerR (inv_V _) _).
Defined.

Instance transitive_coset : Transitive in_coset.
#[export] Instance transitive_coset : Transitive in_coset.
Proof.
intros g1 g2 g3 [h1 p1] [h2 p2].
exists (h1 @ h2).
Expand Down
12 changes: 6 additions & 6 deletions theories/Classes/orders/lattices.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -279,15 +279,15 @@ Section meet_semilattice_order.
- rewrite <-E. apply meet_lb_r.
Qed.

#[export] Instance: forall z, OrderPreserving (z ⊓).
#[export] Instance OrderPreserving_left_meet : forall z, OrderPreserving (z ⊓).
Proof.
red;intros.
apply meet_glb.
- apply meet_lb_l.
- apply meet_le_compat_l. trivial.
Qed.

#[export] Instance: forall z, OrderPreserving (⊓ z).
#[export] Instance OrderPreserving_right_meet: forall z, OrderPreserving (⊓ z).
Proof.
intros. exact maps.order_preserving_flip.
Qed.
Expand Down Expand Up @@ -346,10 +346,10 @@ End meet_semilattice_order.
Section lattice_order.
Context `{LatticeOrder L}.

Instance: IsJoinSemiLattice L := join_sl_order_join_sl.
Instance: IsMeetSemiLattice L := meet_sl_order_meet_sl.
Instance IsJoinSemilattice_LatticeOrder : IsJoinSemiLattice L := join_sl_order_join_sl.
Instance IsMeetSemilattice_LatticeOrder : IsMeetSemiLattice L := meet_sl_order_meet_sl.

Instance: Absorption (⊓) (⊔).
Instance Absorption_join_meet : Absorption (⊓) (⊔).
Proof.
intros x y. apply (antisymmetry (≤)).
- apply meet_lb_l.
Expand All @@ -358,7 +358,7 @@ Section lattice_order.
+ apply join_ub_l.
Qed.

Instance: Absorption (⊔) (⊓).
Instance Absorption_meet_join : Absorption (⊔) (⊓).
Proof.
intros x y. apply (antisymmetry (≤)).
- apply join_le.
Expand Down
4 changes: 2 additions & 2 deletions theories/Classes/orders/nat_int.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -147,15 +147,15 @@ Section another_semiring.
`{PropHolds ((1 : R2) ≶ 0)}
`{!IsSemiRingPreserving (f : R -> R2)}.

Instance: OrderPreserving f.
Instance OrderPreserving_SemiRing_Homomorphism : OrderPreserving f.
Proof.
repeat (split; try exact _).
intros x y E. apply nat_int_le_plus in E. destruct E as [z E].
rewrite E, (preserves_plus (f:=f)), (naturals.to_semiring_twice f _ _).
apply nonneg_plus_le_compat_r. apply to_semiring_nonneg.
Qed.

#[export] Instance: StrictlyOrderPreserving f | 50.
#[export] Instance StrictlyOrderPreserving_SemiRing_Homomorphism : StrictlyOrderPreserving f | 50.
Proof.
repeat (split; try exact _).
intros x y E. apply nat_int_lt_plus in E. destruct E as [z E].
Expand Down
2 changes: 1 addition & 1 deletion theories/Classes/orders/naturals.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -59,7 +59,7 @@ etransitivity.
- apply pos_ge_1.
Qed.

#[export] Instance: forall (z : N), PropHolds (z <> 0) -> OrderReflecting (z *.).
#[export] Instance OrderReflecting_left_mult : forall (z : N), PropHolds (z <> 0) -> OrderReflecting (z *.).
Proof.
intros z ?. red. apply (order_reflecting_pos (.*.) z).
apply nat_ne_0_pos. trivial.
Expand Down
2 changes: 1 addition & 1 deletion theories/Classes/orders/orders.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -558,6 +558,6 @@ Section pseudo.
- destruct (pseudo_order_antisym y z (ltyz , ltzy)).
Qed.

Existing Instance lt_transitive.
#[export] Existing Instance lt_transitive.

End pseudo.
6 changes: 3 additions & 3 deletions theories/Classes/orders/semirings.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -437,7 +437,7 @@ Section pseudo_semiring_order.
exact strictly_order_reflecting_flip.
Qed.

Global Instance apartzero_mult_strong_cancel_l
#[export] Instance apartzero_mult_strong_cancel_l
: forall z, PropHolds (z ≶ 0) -> StrongLeftCancellation (.*.) z.
Proof.
intros z Ez x y E. red in Ez.
Expand Down Expand Up @@ -602,12 +602,12 @@ Section full_pseudo_semiring_order.
destruct (neg_mult_decompose x y E) as [[? ?]|[? ?]];auto.
Qed.

#[export] Instance : forall (z : R), PropHolds (0 < z) -> OrderReflecting (z *.).
#[export] Instance OrderReflecting_left_mult : forall (z : R), PropHolds (0 < z) -> OrderReflecting (z *.).
Proof.
intros z E. exact full_pseudo_order_reflecting.
Qed.

#[export] Instance: forall (z : R), PropHolds (0 < z) -> OrderReflecting (.* z).
#[export] Instance OrderReflecting_right_mult : forall (z : R), PropHolds (0 < z) -> OrderReflecting (.* z).
Proof.
intros. exact order_reflecting_flip.
Qed.
Expand Down
2 changes: 1 addition & 1 deletion theories/Classes/theory/apartness.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -12,7 +12,7 @@ intros ap e;revert ap.
apply tight_apart. assumption.
Qed.

#[export] Instance: forall x y : A, Stable (x = y).
#[export] Instance apartness_eq_stable: forall x y : A, Stable (x = y).
Proof.
intros x y. unfold Stable.
intros dn. apply tight_apart.
Expand Down
20 changes: 10 additions & 10 deletions theories/Classes/theory/fields.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -52,7 +52,7 @@ Proof.
intros ? E. rewrite <-E. trivial.
Qed.

#[export] Instance: IsStrongInjective (-).
#[export] Instance IsStrongInjective_FieldNegation: IsStrongInjective (-).
Proof.
repeat (split; try exact _); intros x y E.
- apply (strong_extensionality (+ x + y)).
Expand All @@ -67,7 +67,7 @@ repeat (split; try exact _); intros x y E.
apply symmetry;trivial.
Qed.

#[export] Instance: IsStrongInjective (//).
#[export] Instance IsStrongInjective_FieldDivision: IsStrongInjective (//).
Proof.
repeat (split; try exact _); intros x y E.
- apply (strong_extensionality (x.1 *.)).
Expand All @@ -82,20 +82,20 @@ repeat (split; try exact _); intros x y E.
rewrite mult_1_l,mult_1_r. apply symmetry;trivial.
Qed.

#[export] Instance: forall z, StrongLeftCancellation (+) z.
#[export] Instance StrongLeftCancellation_plus_field: forall z, StrongLeftCancellation (+) z.
Proof.
intros z x y E. apply (strong_extensionality (+ -z)).
do 2 rewrite (commutativity (f:=plus) z _),
<-simple_associativity,right_inverse,plus_0_r.
trivial.
Qed.

#[export] Instance: forall z, StrongRightCancellation (+) z.
#[export] Instance StrongRightCancellation_plus_field : forall z, StrongRightCancellation (+) z.
Proof.
intros. exact (strong_right_cancel_from_left (+)).
Qed.

#[export] Instance: forall z, PropHolds (z ≶ 0) -> StrongLeftCancellation (.*.) z.
#[export] Instance StrongLeftCancellation_times_field : forall z, PropHolds (z ≶ 0) -> StrongLeftCancellation (.*.) z.
Proof.
intros z Ez x y E. red in Ez.
rewrite !(commutativity z).
Expand All @@ -104,7 +104,7 @@ rewrite <-!simple_associativity, !reciperse_alt.
rewrite !mult_1_r;trivial.
Qed.

#[export] Instance: forall z, PropHolds (z ≶ 0) -> StrongRightCancellation (.*.) z.
#[export] Instance StrongRightCancellation_times_field : forall z, PropHolds (z ≶ 0) -> StrongRightCancellation (.*.) z.
Proof.
intros. exact (strong_right_cancel_from_left (.*.)).
Qed.
Expand All @@ -130,7 +130,7 @@ rewrite <-simple_associativity, reciperse_alt, mult_1_r, mult_0_l.
trivial.
Qed.

Instance: NoZeroDivisors F.
Instance NoZeroDivisors_Field : NoZeroDivisors F.
Proof.
intros x [x_nonzero [y [y_nonzero E]]].
assert (~ ~ apart y 0) as Ey.
Expand All @@ -142,9 +142,9 @@ assert (~ ~ apart y 0) as Ey.
apply mult_0_l.
Qed.

#[export] Instance : IsIntegralDomain F := {}.
#[export] Instance IsIntegralDomain_Field : IsIntegralDomain F := {}.

#[export] Instance apart_0_sig_apart_0: forall (x : ApartZero F), PropHolds (x.1 ≶ 0).
#[export] Instance apart_0_sig_apart_0 : forall (x : ApartZero F), PropHolds (x.1 ≶ 0).
Proof.
intros [??];trivial.
Qed.
Expand Down Expand Up @@ -296,7 +296,7 @@ Section morphisms.

(* We have the following for morphisms to non-trivial strong rings as well.
However, since we do not have an interface for strong rings, we ignore it. *)
#[export] Instance: IsStrongInjective f.
#[export] Instance IsStrongInjective_FieldHomomorphism : IsStrongInjective f.
Proof.
apply strong_injective_preserves_0.
intros x Ex.
Expand Down
14 changes: 7 additions & 7 deletions theories/Classes/theory/naturals.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -76,7 +76,7 @@ Section retract_is_nat.
Section for_another_semirings.
Context `{IsSemiCRing R}.

Instance: IsSemiRingPreserving (naturals_to_semiring N R ∘ f^-1) := {}.
Instance IsSemiRingPreserving_naturals_to_semiring : IsSemiRingPreserving (naturals_to_semiring N R ∘ f^-1) := {}.

Context (h : SR -> R) `{!IsSemiRingPreserving h}.

Expand Down Expand Up @@ -144,7 +144,7 @@ Section borrowed_from_nat.
simpl. intros [|x];eauto.
Qed.

#[export] Instance: Biinduction N.
#[export] Instance biinduction_nat : Biinduction N.
Proof.
hnf. intros P E0 ES.
apply induction;trivial.
Expand All @@ -158,20 +158,20 @@ Section borrowed_from_nat.
simpl. first [exact nat_plus_cancel_l@{U i}|exact nat_plus_cancel_l@{U}].
Qed.

#[export] Instance: forall z : N, RightCancellation (+) z.
#[export] Instance RightCancellation_plus_nat : forall z : N, RightCancellation (+) z.
Proof. intro. exact (right_cancel_from_left (+)). Qed.

#[export] Instance: forall z : N, PropHolds (z <> 0) -> LeftCancellation (.*.) z.
#[export] Instance LeftCancellation_plus_nat : forall z : N, PropHolds (z <> 0) -> LeftCancellation (.*.) z.
Proof.
refine (from_nat_stmt nat (fun s =>
forall z : s, PropHolds (z <> 0) -> LeftCancellation mult z) _).
simpl. exact nat_mult_cancel_l.
Qed.

#[export] Instance: forall z : N, PropHolds (z <> 0) -> RightCancellation (.*.) z.
#[export] Instance RightCancellation_times_nat : forall z : N, PropHolds (z <> 0) -> RightCancellation (.*.) z.
Proof. intros ? ?. exact (right_cancel_from_left (.*.)). Qed.

Instance nat_nontrivial: PropHolds ((1:N) <> 0).
Instance nat_nontrivial : PropHolds ((1:N) <> 0).
Proof.
refine (from_nat_stmt nat (fun s => PropHolds ((1:s) <> 0)) _).
exact _.
Expand Down Expand Up @@ -202,7 +202,7 @@ Section borrowed_from_nat.
apply S_inj in E. destruct (S_neq_0 _ E).
Qed.

#[export] Instance: ZeroProduct N.
#[export] Instance ZeroProduct_N : ZeroProduct N.
Proof.
refine (from_nat_stmt nat (fun s => ZeroProduct s) _).
simpl. red. exact mult_eq_zero.
Expand Down
6 changes: 3 additions & 3 deletions theories/HIT/V.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -277,7 +277,7 @@ Defined.

Notation "u ~~ v" := (bisimulation u v) : set_scope.

Instance reflexive_bisimulation : Reflexive bisimulation.
#[export] Instance reflexive_bisimulation : Reflexive bisimulation.
Proof.
refine (V_ind_hprop _ _ _).
intros A f H_f. split.
Expand Down Expand Up @@ -443,7 +443,7 @@ Defined.

(** ** Two useful lemmas *)

Instance irreflexive_mem : Irreflexive mem.
#[export] Instance irreflexive_mem : Irreflexive mem.
Proof.
assert (forall v, IsHProp (complement (fun x x0 : V => x ∈ x0) v v)). (* https://coq.inria.fr/bugs/show_bug.cgi?id=3854 *)
{ intro.
Expand Down Expand Up @@ -478,7 +478,7 @@ Definition V_empty : V := set (Empty_ind (fun _ => V)).
(** The singleton {u} *)
Definition V_singleton (u : V) : V@{U' U} := set (Unit_ind u).

Instance isequiv_ap_V_singleton {u v : V}
#[export] Instance isequiv_ap_V_singleton {u v : V}
: IsEquiv (@ap _ _ V_singleton u v).
Proof.
simple refine (Build_IsEquiv _ _ _ _ _ _ _); try solve [ intro; apply path_ishprop ].
Expand Down
2 changes: 2 additions & 0 deletions theories/HoTT.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -161,9 +161,11 @@ Require Export HoTT.Homotopy.HSpace.
Require Export HoTT.Homotopy.ClassifyingSpace.
Require Export HoTT.Homotopy.CayleyDickson.
Require Export HoTT.Homotopy.EMSpace.
Require Export HoTT.Homotopy.ExactSequence.
Require Export HoTT.Homotopy.HSpaceS1.
Require Export HoTT.Homotopy.Bouquet.
Require Export HoTT.Homotopy.EncodeDecode.
Require Export HoTT.Homotopy.SuccessorStructure.
Require Export HoTT.Homotopy.Syllepsis.
Require Export HoTT.Homotopy.Hopf.
Require Export HoTT.Homotopy.IdentitySystems.
Expand Down
2 changes: 2 additions & 0 deletions theories/Spaces/Nat.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -2,4 +2,6 @@

Require Export Nat.Core.
Require Export Nat.Arithmetic.
Require Export Nat.Division.
Require Export Nat.Paths.
Require Export Nat.Factorial.
2 changes: 1 addition & 1 deletion theories/Universes/HSet.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -38,7 +38,7 @@ Proof.
eapply path_ishprop.
Defined.

Instance axiomK_isprop A : IsHProp (axiomK A) | 0.
#[export] Instance axiomK_isprop A : IsHProp (axiomK A) | 0.
Proof.
exact (istrunc_equiv_istrunc _ equiv_hset_axiomK).
Defined.
Expand Down
Loading