preferred alternatives to type ascriptions everywhere?

Stream: new members

[Jean Lo]

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]

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]

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

[Gabriel Ebner]

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]

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]

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]

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) ?