Skip to content

Commit

Permalink
chore(Data/Funlike): update examples and replace Lean 3 syntax (#11409)
Browse files Browse the repository at this point in the history 
Fully update the module docstrings (in particular, the examples given therein) after #8386.

This includes switching to where syntax, but also replacing Lean 3 syntax, replacing => by "\mapsto" while at it and indenting code per the style guide. As such, it's also a follow-up to #11301.

Co-authored-by: @Vierkantor



Co-authored-by: Vierkantor <[email protected]>
  • Loading branch information
@grunweg @Vierkantor @uniwuni
2 people authored and uniwuni committed Apr 19, 2024
1 parent 424b957 commit afb1082
Show file tree
Hide file tree
Showing 4 changed files with 138 additions and 141 deletions.
82 changes: 39 additions & 43 deletions Mathlib/Data/FunLike/Basic.lean
View file
Original file line number Diff line number Diff line change
Expand Up @@ -21,27 +21,23 @@ A typical type of morphisms should be declared as:
```
structure MyHom (A B : Type*) [MyClass A] [MyClass B] :=
(toFun : A → B)
(map_op' : ∀ {x y : A}, toFun (MyClass.op x y) = MyClass.op (toFun x) (toFun y))
(map_op' : ∀ (x y : A), toFun (MyClass.op x y) = MyClass.op (toFun x) (toFun y))
namespace MyHom
variable (A B : Type*) [MyClass A] [MyClass B]
-- This instance is optional if you follow the "morphism class" design below:
instance : FunLike (MyHom A B) A B :=
{ coe := MyHom.toFun, coe_injective' := fun f g h => by cases f; cases g; congr' }
/-- Helper instance for when there's too many metavariables to apply
`DFunLike.coe` directly. -/
instance : CoeFun (MyHom A B) (fun _ => A → B) := ⟨MyHom.toFun⟩
instance : FunLike (MyHom A B) A B where
coe := MyHom.toFun
coe_injective' := fun f g h => by cases f; cases g; congr
@[ext] theorem ext {f g : MyHom A B} (h : ∀ x, f x = g x) : f = g := DFunLike.ext f g h
/-- Copy of a `MyHom` with a new `toFun` equal to the old one. Useful to fix definitional
equalities. -/
protected def copy (f : MyHom A B) (f' : A → B) (h : f' = ⇑f) : MyHom A B :=
{ toFun := f',
map_op' := h.symm ▸ f.map_op' }
protected def copy (f : MyHom A B) (f' : A → B) (h : f' = ⇑f) : MyHom A B where
toFun := f'
map_op' := h.symm ▸ f.map_op'
end MyHom
```
Expand All @@ -51,29 +47,29 @@ extensionality and simp lemmas.
## Morphism classes extending `DFunLike` and `FunLike`
The `DFunLike` design provides further benefits if you put in a bit more work.
The first step is to extend `DFunLike` to create a class of those types satisfying
The `FunLike` design provides further benefits if you put in a bit more work.
The first step is to extend `FunLike` to create a class of those types satisfying
the axioms of your new type of morphisms.
Continuing the example above:
```
/-- `MyHomClass F A B` states that `F` is a type of `MyClass.op`-preserving morphisms.
You should extend this class when you extend `MyHom`. -/
class MyHomClass (F : Type*) (A B : outParam Type*) [MyClass A] [MyClass B]
[FunLike F A B] : Prop :=
(map_op : ∀ (f : F) (x y : A), f (MyClass.op x y) = MyClass.op (f x) (f y))
[FunLike F A B] : Prop :=
(map_op : ∀ (f : F) (x y : A), f (MyClass.op x y) = MyClass.op (f x) (f y))
@[simp] lemma map_op {F A B : Type*} [MyClass A] [MyClass B] [MyHomClass F A B]
(f : F) (x y : A) : f (MyClass.op x y) = MyClass.op (f x) (f y) :=
MyHomClass.map_op
@[simp]
lemma map_op {F A B : Type*} [MyClass A] [MyClass B] [FunLike F A B] [MyHomClass F A B]
(f : F) (x y : A) :
f (MyClass.op x y) = MyClass.op (f x) (f y) :=
MyHomClass.map_op _ _ _
-- You can add the below instance next to `MyHomClass.instFunLike`:
instance : MyHomClass (MyHom A B) A B :=
{ coe := MyHom.toFun,
coe_injective' := λ f g h, by cases f; cases g; congr',
map_op := MyHom.map_op' }
instance : MyHomClass (MyHom A B) A B where
map_op := MyHom.map_op'
-- [Insert `CoeFun`, `ext` and `copy` here]
-- [Insert `ext` and `copy` here]
```
Note that `A B` are marked as `outParam` even though they are not purely required to be so
Expand All @@ -85,28 +81,28 @@ The second step is to add instances of your new `MyHomClass` for all types exten
Typically, you can just declare a new class analogous to `MyHomClass`:
```
structure CoolerHom (A B : Type*) [CoolClass A] [CoolClass B]
extends MyHom A B :=
(map_cool' : toFun CoolClass.cool = CoolClass.cool)
structure CoolerHom (A B : Type*) [CoolClass A] [CoolClass B] extends MyHom A B :=
(map_cool' : toFun CoolClass.cool = CoolClass.cool)
class CoolerHomClass (F : Type*) (A B : outParam Type*) [CoolClass A] [CoolClass B]
[FunLike F A B]
extends MyHomClass F A B :=
(map_cool : ∀ (f : F), f CoolClass.cool = CoolClass.cool)
@[simp] lemma map_cool {F A B : Type*} [CoolClass A] [CoolClass B] [FunLike F A (fun _ => B)]
[CoolerHomClass F A B] (f : F) :
f CoolClass.cool = CoolClass.cool :=
MyHomClass.map_op
-- You can add the below instance next to `MyHom.instFunLike`:
instance : CoolerHomClass (CoolHom A B) A B :=
{ coe := CoolHom.toFun,
coe_injective' := λ f g h, by cases f; cases g; congr',
map_op := CoolHom.map_op',
map_cool := CoolHom.map_cool' }
-- [Insert `CoeFun`, `ext` and `copy` here]
[FunLike F A B] extends MyHomClass F A B :=
(map_cool : ∀ (f : F), f CoolClass.cool = CoolClass.cool)
@[simp] lemma map_cool {F A B : Type*} [CoolClass A] [CoolClass B] [FunLike F A B]
[CoolerHomClass F A B] (f : F) : f CoolClass.cool = CoolClass.cool :=
CoolerHomClass.map_cool _
variable {A B : Type*} [CoolClass A] [CoolClass B]
instance : FunLike (CoolerHom A B) A B where
coe f := f.toFun
coe_injective' := fun f g h ↦ by cases f; cases g; congr; apply DFunLike.coe_injective; congr
instance : CoolerHomClass (CoolerHom A B) A B where
map_op f := f.map_op'
map_cool f := f.map_cool'
-- [Insert `ext` and `copy` here]
```
Then any declaration taking a specific type of morphisms as parameter can instead take the
Expand Down
91 changes: 45 additions & 46 deletions Mathlib/Data/FunLike/Embedding.lean
View file
Original file line number Diff line number Diff line change
Expand Up @@ -19,28 +19,27 @@ A typical type of embeddings should be declared as:
structure MyEmbedding (A B : Type*) [MyClass A] [MyClass B] :=
(toFun : A → B)
(injective' : Function.Injective toFun)
(map_op' : ∀ {x y : A}, toFun (MyClass.op x y) = MyClass.op (toFun x) (toFun y))
(map_op' : ∀ (x y : A), toFun (MyClass.op x y) = MyClass.op (toFun x) (toFun y))
namespace MyEmbedding
variable (A B : Type*) [MyClass A] [MyClass B]
-- This instance is optional if you follow the "Embedding class" design below:
instance : EmbeddingLike (MyEmbedding A B) A B :=
{ coe := MyEmbedding.toFun,
coe_injective' := λ f g h, by cases f; cases g; congr',
injective' := MyEmbedding.injective' }
instance : FunLike (MyEmbedding A B) A B where
coe := MyEmbedding.toFun
coe_injective' := fun f g h ↦ by cases f; cases g; congr
/-- Helper instance for when there's too many metavariables to `EmbeddingLike.coe` directly. -/
instance : CoeFun (MyEmbedding A B) (λ _, A → B) := ⟨MyEmbedding.toFun⟩
-- This instance is optional if you follow the "Embedding class" design below:
instance : EmbeddingLike (MyEmbedding A B) A B where
injective' := MyEmbedding.injective'
@[ext] theorem ext {f g : MyEmbedding A B} (h : ∀ x, f x = g x) : f = g := DFunLike.ext f g h
/-- Copy of a `MyEmbedding` with a new `toFun` equal to the old one. Useful to fix definitional
equalities. -/
protected def copy (f : MyEmbedding A B) (f' : A → B) (h : f' = ⇑f) : MyEmbedding A B :=
{ toFun := f',
injective' := h.symm ▸ f.injective',
{ toFun := f'
injective' := h.symm ▸ f.injective'
map_op' := h.symm ▸ f.map_op' }
end MyEmbedding
Expand All @@ -57,74 +56,74 @@ the axioms of your new type of morphisms.
Continuing the example above:
```
section
/-- `MyEmbeddingClass F A B` states that `F` is a type of `MyClass.op`-preserving embeddings.
You should extend this class when you extend `MyEmbedding`. -/
class MyEmbeddingClass (F : Type*) (A B : outParam <| Type*) [MyClass A] [MyClass B]
extends EmbeddingLike F A B :=
(map_op : ∀ (f : F) (x y : A), f (MyClass.op x y) = MyClass.op (f x) (f y))
[FunLike F A B]
extends EmbeddingLike F A B :=
(map_op : ∀ (f : F) (x y : A), f (MyClass.op x y) = MyClass.op (f x) (f y))
end
@[simp]
lemma map_op {F A B : Type*} [MyClass A] [MyClass B] [FunLike F A B] [MyEmbeddingClass F A B]
(f : F) (x y : A) :
f (MyClass.op x y) = MyClass.op (f x) (f y) :=
MyEmbeddingClass.map_op _ _ _
namespace MyEmbedding
@[simp] lemma map_op {F A B : Type*} [MyClass A] [MyClass B] [MyEmbeddingClass F A B]
(f : F) (x y : A) : f (MyClass.op x y) = MyClass.op (f x) (f y) :=
MyEmbeddingClass.map_op
variable {A B : Type*} [MyClass A] [MyClass B]
-- You can replace `MyEmbedding.EmbeddingLike` with the below instance:
instance : MyEmbeddingClass (MyEmbedding A B) A B :=
{ coe := MyEmbedding.toFun,
coe_injective' := λ f g h, by cases f; cases g; congr',
injective' := MyEmbedding.injective',
map_op := MyEmbedding.map_op' }
instance : MyEmbeddingClass (MyEmbedding A B) A B where
injective' := MyEmbedding.injective'
map_op := MyEmbedding.map_op'
-- [Insert `CoeFun`, `ext` and `copy` here]
end MyEmbedding
```
The second step is to add instances of your new `MyEmbeddingClass` for all types extending
`MyEmbedding`.
Typically, you can just declare a new class analogous to `MyEmbeddingClass`:
```
structure CoolerEmbedding (A B : Type*) [CoolClass A] [CoolClass B]
extends MyEmbedding A B :=
(map_cool' : toFun CoolClass.cool = CoolClass.cool)
section
set_option old_structure_cmd true
structure CoolerEmbedding (A B : Type*) [CoolClass A] [CoolClass B] extends MyEmbedding A B :=
(map_cool' : toFun CoolClass.cool = CoolClass.cool)
class CoolerEmbeddingClass (F : Type*) (A B : outParam <| Type*) [CoolClass A] [CoolClass B]
extends MyEmbeddingClass F A B :=
(map_cool : ∀ (f : F), f CoolClass.cool = CoolClass.cool)
[FunLike F A B]
extends MyEmbeddingClass F A B :=
(map_cool : ∀ (f : F), f CoolClass.cool = CoolClass.cool)
end
@[simp]
lemma map_cool {F A B : Type*} [CoolClass A] [CoolClass B]
[FunLike F A B] [CoolerEmbeddingClass F A B] (f : F) :
f CoolClass.cool = CoolClass.cool :=
CoolerEmbeddingClass.map_cool _
@[simp] lemma map_cool {F A B : Type*} [CoolClass A] [CoolClass B] [CoolerEmbeddingClass F A B]
(f : F) : f CoolClass.cool = CoolClass.cool :=
MyEmbeddingClass.map_op
variable {A B : Type*} [CoolClass A] [CoolClass B]
-- You can also replace `MyEmbedding.EmbeddingLike` with the below instance:
instance : CoolerEmbeddingClass (CoolerEmbedding A B) A B :=
{ coe := CoolerEmbedding.toFun,
coe_injective' := λ f g h, by cases f; cases g; congr',
injective' := MyEmbedding.injective',
map_op := CoolerEmbedding.map_op',
map_cool := CoolerEmbedding.map_cool' }
instance : FunLike (CoolerEmbedding A B) A B where
coe f := f.toFun
coe_injective' f g h := by cases f; cases g; congr; apply DFunLike.coe_injective; congr
-- [Insert `CoeFun`, `ext` and `copy` here]
instance : CoolerEmbeddingClass (CoolerEmbedding A B) A B where
injective' f := f.injective'
map_op f := f.map_op'
map_cool f := f.map_cool'
-- [Insert `ext` and `copy` here]
```
Then any declaration taking a specific type of morphisms as parameter can instead take the
class you just defined:
```
-- Compare with: lemma do_something (f : MyEmbedding A B) : sorry := sorry
lemma do_something {F : Type*} [MyEmbeddingClass F A B] (f : F) : sorry := sorry
lemma do_something {F : Type*} [FunLike F A B] [MyEmbeddingClass F A B] (f : F) : sorry := sorry
```
This means anything set up for `MyEmbedding`s will automatically work for `CoolerEmbeddingClass`es,
and defining `CoolerEmbeddingClass` only takes a constant amount of effort,
instead of linearly increasing the work per `MyEmbedding`-related declaration.
-/


Expand Down
Loading

0 comments on commit afb1082

Please sign in to comment.