Typeclass for types with a set-like extensionality property #
The Membership typeclass is used to let terms of a type have elements.
Many instances of Membership have a set-like extensionality property:
things are equal iff they have the same elements. The SetLike
typeclass provides a unified interface to define a Membership that is
extensional in this way.
The main use of SetLike is for algebraic subobjects (such as
Submonoid and Submodule), whose non-proof data consists only of a
carrier set. In such a situation, the projection to the carrier set
is injective.
In general, a type A is SetLike with elements of type B if it
has an injective map to Set B. This module provides standard
boilerplate for every SetLike: a coe_sort, a coe to set,
and various extensionality and simp lemmas. The order induced by set inclusion is
called PartialOrder.ofSetlike: this is not an instance for flexibility in choosing orders.
The class IsConcreteLE abstractly states the order is equal to that induced by set inclusion;
an instance is automatically available when defining a PartialOrder as
.ofSetLike (MySubobject X) X.
A typical subobject should be declared as:
structure MySubobject (X : Type*) [ObjectTypeclass X] where
(carrier : Set X)
(op_mem' : ∀ {x : X}, x ∈ carrier → sorry ∈ carrier)
namespace MySubobject
variable {X : Type*} [ObjectTypeclass X] {x : X}
instance : SetLike (MySubobject X) X :=
⟨MySubobject.carrier, fun p q h => by cases p; cases q; congr!⟩
instance : PartialOrder (MySubobject X) := .ofSetLike (MySubobject X) X
@[simp] lemma mem_carrier {p : MySubobject X} : x ∈ p.carrier ↔ x ∈ (p : Set X) := Iff.rfl
@[ext] theorem ext {p q : MySubobject X} (h : ∀ x, x ∈ p ↔ x ∈ q) : p = q := SetLike.ext h
/-- Copy of a `MySubobject` with a new `carrier` equal to the old one. Useful to fix definitional
equalities. See Note [range copy pattern]. -/
protected def copy (p : MySubobject X) (s : Set X) (hs : s = ↑p) : MySubobject X :=
{ carrier := s
op_mem' := hs.symm ▸ p.op_mem' }
@[simp] lemma coe_copy (p : MySubobject X) (s : Set X) (hs : s = ↑p) :
(p.copy s hs : Set X) = s := rfl
lemma copy_eq (p : MySubobject X) (s : Set X) (hs : s = ↑p) : p.copy s hs = p :=
SetLike.coe_injective hs
end MySubobject
An alternative to SetLike could have been an extensional Membership typeclass:
class ExtMembership (α : out_param <| Type u) (β : Type v) extends Membership α β where
(ext_iff : ∀ {s t : β}, s = t ↔ ∀ (x : α), x ∈ s ↔ x ∈ t)
While this is equivalent, SetLike conveniently uses a carrier set projection directly.
Tags #
subobjects
A class to indicate that there is a canonical injection between A and Set B.
This has the effect of giving terms of A elements of type B (through a Membership
instance) and a compatible coercion to Type* as a subtype.
Note: if SetLike.coe is a projection, implementers should create a simp lemma such as
@[simp] lemma mem_carrier {p : MySubobject X} : x ∈ p.carrier ↔ x ∈ (p : Set X) := Iff.rfl
to normalize terms.
If you declare an unbundled subclass of SetLike, for example:
class MulMemClass (S : Type*) (M : Type*) [Mul M] [SetLike S M] where
...
Then you should not repeat the outParam declaration so SetLike will supply the value instead.
This ensures your subclass will not have issues with synthesis of the [Mul M] parameter starting
before the value of M is known.
- coe : A → Set B
- coe_injective' : Function.Injective SetLike.coe
Instances
Equations
Equations
Equations
For terms that match the CoeSort instance's body, pretty print as ↥S
rather than as { x // x ∈ S }. The discriminating feature is that membership
uses the SetLike.instMembership instance.
Equations
Instances For
If s is a proper element of a SetLike structure (i.e., s ≠ ⊤) and the top element
coerces to the universal set, then there exists an element not in s.
A class to indicate that the canonical injection between A and Set B is order-preserving.
An instance of this class is automatically available on any partial order defined as
PartialOrder.ofSetLike.
The coercion from a
SetLiketype preserves the ordering.
Instances
The partial order induced from a SetLike instance by inclusion.
A partial order defined as .ofSetLike will automatically make available an instance
of IsConcreteLE.
Equations
Instances For
Alias of the forward direction of SetLike.le_def.
Alias of the forward direction of SetLike.le_def.
Alias of the forward direction of SetLike.le_def.