abbreviation

Stream: general

[Reid Barton]

I don't suppose abbreviation is documented anywhere?

[Reid Barton]

It seems to do something very specific that I want (MWE incoming)

[Reid Barton]

def test1 {α : Type} [has_add α] (x : α) := x + x
@[class, reducible] def my_add := has_add
def test2 {α : Type} [my_add α] (x : α) := x + x -- failed to synthesize type class instance for has_add α
abbreviation my_add' := has_add
def test3 {α : Type} [my_add' α] (x : α) := x + x -- ok!

[Reid Barton]

Is there a catch?

[Reid Barton]

You can also do more interesting things like abbreviation my_add' (α : Type) := has_add (list α)

[Sebastien Gouezel]

I have tried to convert module to an abbreviation for semimodule, but something is not working out of the box. Here is a minimal example showing the problem.

import algebra.pi_instances

universes u v w

class SemiModule (β : Type v) [add_comm_monoid β]

abbreviation Module (β : Type v) [add_comm_group β] :=
SemiModule β

instance piSemiModule (I : Type w) (f : I → Type u)
  [∀ i, add_comm_monoid $ f i] [∀ i, SemiModule (f i)] :
  SemiModule (Π i : I, f i) := by constructor

instance piModule (I : Type w) (f : I → Type u)
  [∀ i, add_comm_group $ f i] [∀ i, Module (f i)] :
  Module (Π i : I, f i) := by apply_instance

The last by apply_instance does not find the instance piSemiModule which is right here. I don't understand why.

[Kevin Buzzard]

import algebra.pi_instances

universes u v w

class SemiModule (β : Type v) [add_comm_monoid β]

abbreviation Module (β : Type v) [add_comm_group β] :=
SemiModule β

instance piSemiModule (I : Type w) (f : I → Type u)
  [∀ i, add_comm_monoid $ f i] [∀ i, SemiModule (f i)] :
  SemiModule (Π i : I, f i) := by constructor

instance piSemiModule' (I : Type w) (f : I → Type u)
  [∀ i, add_comm_monoid $ f i] [∀ i, SemiModule (f i)] :
  SemiModule (Π i : I, f i) := by apply_instance -- works

instance piModule (I : Type w) (f : I → Type u)
  [∀ i, add_comm_group $ f i] [∀ i, SemiModule (f i)] : -- changed from Module
  Module (Π i : I, f i) := begin
  delta Module,
  -- ⊢ SemiModule (Π (i : I), f i)

  -- apply piSemiModule I f, -- works
  apply_instance -- still fails
end

Bewildering!

[Chris Hughes]

Changing abbreviation Module (β : Type v) [add_comm_group β] to abbreviation Module (β : Type v) [add_comm_monoid β] makes it work. I think the problem is unifying the different add_comm_monoid instance generated because of this.

[Chris Hughes]

I haven't worked it out exactly, but I think it's basically trying to do this unification, but with more metavariables, and it doesn't work with the metavariables

example (I : Type w) (f : I → Type u) [∀ i, add_comm_group $ f i] :
  @pi.add_comm_monoid I f _ = @add_comm_group.to_add_comm_monoid _ _ := rfl

[Chris Hughes]

I might be completely wrong.

[Chris Hughes]

It must be trying to unify

@SemiModule (Π (i : ?M_1), ?M_2 i) (@pi.add_comm_monoid ?M_1 (λ (i : ?M_1), ?M_2 i) (λ (i : ?M_1), ?M_3 i))

with

@SemiModule (Π (i : I), f i)
    (@add_comm_group.to_add_comm_monoid (Π (i : I), f i)
       (@pi.add_comm_group I (λ (i : I), f i) (λ (i : I), _inst_1 i)))

[Chris Hughes]

Which is difficult with the metavariables there.

[Chris Hughes]

?M_1 and ?M_2 look easy to infer, but ?M_3 must be the difficult one.

[Chris Hughes]

And you have to unfold ?M_3 to see that they are defeq.

[Chris Hughes]

I guess this maybe answers the question you asked me the other day about extending type classes, versus having the other class as an argument. This seems to be a downside of the argument approach.

[Paul van Wamelen]

Is there documentation for abbreviation?

[Paul van Wamelen]

Oh: "abbreviation is indeed a synonym for @[inline, reducible] def" (from Mario a while ago)