# Zulip Chat Archive

## Stream: new members

### Topic: preferred alternatives to type ascriptions everywhere?

#### Jean Lo (Aug 27 2020 at 13:06):

as a minimal (not-)working example, consider the following (re-)definition of a monoid action by first defining a semigroup action then extending the structure to include the additional axiom:

```
import group_theory.coset
structure semigroup_act (α : Type*) (β : Type*) [semigroup α] :=
(smul : α → β → β)
(mul_smul : ∀ (x y : α) (b : β), smul (x * y) b = smul x (smul y b))
structure monoid_act (α : Type*) (β : Type*) [monoid α] extends semigroup_act α β :=
(one_smul : ∀ b : β, smul (1 : α) b = b)
```

followed by some definitions and proofs:

```
variables {α : Type*} {β : Type*}
instance [monoid α]: has_coe (monoid_act α β) (semigroup_act α β) := ⟨λ f, f.to_semigroup_act⟩
def invariant [semigroup α] (f : semigroup_act α β) (S : set β) : Prop := ∀ a (b ∈ S), f.smul a b ∈ S
variable [monoid α]
lemma invariant_univ₁ (f : monoid_act α β) : invariant (f : semigroup_act α β) set.univ := sorry
```

but the following doesn't work, (I think) because the metavariables in the expected type prevent lean from considering the coercion:

```
lemma invariant_univ₂ (f : monoid_act α β) : invariant f set.univ := sorry
-- type mismatch at application
-- invariant f
-- term
-- f
-- has type
-- monoid_act α β : Type (max u_1 u_2)
-- but is expected to have type
-- semigroup_act ?m_1 ?m_2 : Type (max ? ?)
```

I think I first encountered a version of this problem when I tried to write down things about continuous linear maps, and lean complained when I tried to invoke lemmas like `map_smul`

. mathlib does this, which makes the following seem tempting to me:

```
def invariant (f : monoid_act α β) (S : set β) : Prop := invariant (f : semigroup_act α β) S
```

(in a practical case the the definitions will probably be under different namespaces so that no collision happens.)

this feels somewhat redundant, though, if only because "a set is invariant under a monoid action f if it is invariant under f as a semigroup action" feels very obvious. is duplicating definitions/lemmas like this a good idea in general?

#### Reid Barton (Aug 27 2020 at 13:11):

This kind of error was fixed a while back for `has_coe_to_fun`

, maybe it can be fixed for coercions more generally? @Gabriel Ebner

#### Reid Barton (Aug 27 2020 at 13:14):

(Well, not "more generally", but "also".)

#### Gabriel Ebner (Aug 27 2020 at 13:15):

No, we can now coerce `monoid_act ?m_1 ?m_2`

to `semigroup_act ?m_1 ?m_2`

. But Jean's example requires finding a coercion and assigning the metavariables at the same time. I don't think this can be done using the current coercion system in Lean 3. It will also be impossible in Lean 4 as far as I can tell.

#### Reid Barton (Aug 27 2020 at 13:36):

Oh, because the target type of the coercion is also an argument to the class for `has_coe`

, while the result of a `has_coe_to_fun`

is a field of the class?

#### Reid Barton (Aug 27 2020 at 13:37):

I guess this one wouldn't work in Haskell either (or a hypothetical Haskell with coercions). Just because there is

```
has_coe (monoid_act α β) (semigroup_act α β)
```

doesn't mean there isn't/shouldn't also be, say,

```
has_coe (monoid_act α β) (semigroup_act β α)
```

#### Jean Lo (Aug 28 2020 at 00:31):

ah, that makes sense, thanks!

so maybe this is indeed a library design / convention question rather than a "how to do coercions" question. I guess an alternative would be to make `α`

and `β`

explicit arguments to `invariant`

, and do

```
lemma invariant_univ₂ (f : monoid_act α β) : invariant α β f set.univ := sorry -- this is ok
```

between this, type ascriptions, and duplicating the definitions for the extended structure, do `mathlib`

conventions have a preference? or is this something that depends on the context (supplying the types explicitly in the example here feels redundant, but e.g. — though I'm not sure how good of an example this is — when trying to apply `finite_dimensional`

to a linear space + additional structure it makes sense that I should have to tell lean which `vector_space K V`

i'm coercing into) ?

Last updated: May 13 2021 at 18:26 UTC