This repository was archived by the owner on Jul 24, 2024. It is now read-only.
-
Notifications
You must be signed in to change notification settings - Fork 289
Expand file tree
/
Copy pathbasic.lean
More file actions
175 lines (122 loc) · 6.26 KB
/
Copy pathbasic.lean
File metadata and controls
175 lines (122 loc) · 6.26 KB
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
/-
Copyright (c) 2021 Eric Wieser. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Eric Wieser
-/
import data.set.basic
import tactic.monotonicity.basic
/-!
# Typeclass for types with a set-like extensionality property
> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
> Any changes to this file require a corresponding PR to mathlib4.
The `has_mem` typeclass is used to let terms of a type have elements.
Many instances of `has_mem` have a set-like extensionality property:
things are equal iff they have the same elements. The `set_like`
typeclass provides a unified interface to define a `has_mem` that is
extensional in this way.
The main use of `set_like` 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 `set_like` with elements of type `B` if it
has an injective map to `set B`. This module provides standard
boilerplate for every `set_like`: a `coe_sort`, a `coe` to set, a
`partial_order`, and various extensionality and simp lemmas.
A typical subobject should be declared as:
```
structure my_subobject (X : Type*) [object_typeclass X] :=
(carrier : set X)
(op_mem' : ∀ {x : X}, x ∈ carrier → sorry ∈ carrier)
namespace my_subobject
variables {X : Type*} [object_typeclass X] {x : X}
instance : set_like (my_subobject X) X :=
⟨my_subobject.carrier, λ p q h, by cases p; cases q; congr'⟩
@[simp] lemma mem_carrier {p : my_subobject X} : x ∈ p.carrier ↔ x ∈ (p : set X) := iff.rfl
@[ext] theorem ext {p q : my_subobject X} (h : ∀ x, x ∈ p ↔ x ∈ q) : p = q := set_like.ext h
/-- Copy of a `my_subobject` with a new `carrier` equal to the old one. Useful to fix definitional
equalities. See Note [range copy pattern]. -/
protected def copy (p : my_subobject X) (s : set X) (hs : s = ↑p) : my_subobject X :=
{ carrier := s,
op_mem' := hs.symm ▸ p.op_mem' }
@[simp] lemma coe_copy (p : my_subobject X) (s : set X) (hs : s = ↑p) :
(p.copy s hs : set X) = s := rfl
lemma copy_eq (p : my_subobject X) (s : set X) (hs : s = ↑p) : p.copy s hs = p :=
set_like.coe_injective hs
end my_subobject
```
An alternative to `set_like` could have been an extensional `has_mem` typeclass:
```
class has_ext_mem (α : out_param $ Type u) (β : Type v) extends has_mem α β :=
(ext_iff : ∀ {s t : β}, s = t ↔ ∀ (x : α), x ∈ s ↔ x ∈ t)
```
While this is equivalent, `set_like` 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 `has_mem`
instance) and a compatible coercion to `Type*` as a subtype.
Note: if `set_like.coe` is a projection, implementers should create a simp lemma such as
```
@[simp] lemma mem_carrier {p : my_subobject X} : x ∈ p.carrier ↔ x ∈ (p : set X) := iff.rfl
```
to normalize terms.
If you declare an unbundled subclass of `set_like`, for example:
```
class mul_mem_class (S : Type*) (M : Type*) [has_mul M] [set_like S M] where
...
```
Then you should *not* repeat the `out_param` declaration, `set_like` will supply the value instead.
This ensures in Lean 4 your subclass will not have issues with synthesis of the `[has_mul M]`
parameter starting before the value of `M` is known.
-/
@[protect_proj]
class set_like (A : Type*) (B : out_param $ Type*) :=
(coe : A → set B)
(coe_injective' : function.injective coe)
namespace set_like
variables {A : Type*} {B : Type*} [i : set_like A B]
include i
instance : has_coe_t A (set B) := ⟨set_like.coe⟩
@[priority 100]
instance : has_mem B A := ⟨λ x p, x ∈ (p : set B)⟩
-- `dangerous_instance` does not know that `B` is used only as an `out_param`
@[nolint dangerous_instance, priority 100]
instance : has_coe_to_sort A Type* := ⟨λ p, {x : B // x ∈ p}⟩
variables (p q : A)
@[simp, norm_cast] theorem coe_sort_coe : ((p : set B) : Type*) = p := rfl
variables {p q}
protected theorem «exists» {q : p → Prop} :
(∃ x, q x) ↔ (∃ x ∈ p, q ⟨x, ‹_›⟩) := set_coe.exists
protected theorem «forall» {q : p → Prop} :
(∀ x, q x) ↔ (∀ x ∈ p, q ⟨x, ‹_›⟩) := set_coe.forall
theorem coe_injective : function.injective (coe : A → set B) :=
λ x y h, set_like.coe_injective' h
@[simp, norm_cast] theorem coe_set_eq : (p : set B) = q ↔ p = q := coe_injective.eq_iff
theorem ext' (h : (p : set B) = q) : p = q := coe_injective h
theorem ext'_iff : p = q ↔ (p : set B) = q := coe_set_eq.symm
/-- Note: implementers of `set_like` must copy this lemma in order to tag it with `@[ext]`. -/
theorem ext (h : ∀ x, x ∈ p ↔ x ∈ q) : p = q := coe_injective $ set.ext h
theorem ext_iff : p = q ↔ (∀ x, x ∈ p ↔ x ∈ q) := coe_injective.eq_iff.symm.trans set.ext_iff
@[simp] theorem mem_coe {x : B} : x ∈ (p : set B) ↔ x ∈ p := iff.rfl
@[simp, norm_cast] lemma coe_eq_coe {x y : p} : (x : B) = y ↔ x = y := subtype.ext_iff_val.symm
@[simp, norm_cast] lemma coe_mk (x : B) (hx : x ∈ p) : ((⟨x, hx⟩ : p) : B) = x := rfl
@[simp] lemma coe_mem (x : p) : (x : B) ∈ p := x.2
@[simp] protected lemma eta (x : p) (hx : (x : B) ∈ p) : (⟨x, hx⟩ : p) = x := subtype.eta x hx
-- `dangerous_instance` does not know that `B` is used only as an `out_param`
@[nolint dangerous_instance, priority 100]
instance : partial_order A :=
{ le := λ H K, ∀ ⦃x⦄, x ∈ H → x ∈ K,
.. partial_order.lift (coe : A → set B) coe_injective }
lemma le_def {S T : A} : S ≤ T ↔ ∀ ⦃x : B⦄, x ∈ S → x ∈ T := iff.rfl
@[simp, norm_cast]
lemma coe_subset_coe {S T : A} : (S : set B) ⊆ T ↔ S ≤ T := iff.rfl
@[mono] lemma coe_mono : monotone (coe : A → set B) := λ a b, coe_subset_coe.mpr
@[simp, norm_cast]
lemma coe_ssubset_coe {S T : A} : (S : set B) ⊂ T ↔ S < T := iff.rfl
@[mono] lemma coe_strict_mono : strict_mono (coe : A → set B) := λ a b, coe_ssubset_coe.mpr
lemma not_le_iff_exists : ¬(p ≤ q) ↔ ∃ x ∈ p, x ∉ q := set.not_subset
lemma exists_of_lt : p < q → ∃ x ∈ q, x ∉ p := set.exists_of_ssubset
lemma lt_iff_le_and_exists : p < q ↔ p ≤ q ∧ ∃ x ∈ q, x ∉ p :=
by rw [lt_iff_le_not_le, not_le_iff_exists]
end set_like