Zulip Chat Archive

Stream: general

Topic: abbreviation


view this post on Zulip Reid Barton (Dec 03 2018 at 02:46):

I don't suppose abbreviation is documented anywhere?

view this post on Zulip Reid Barton (Dec 03 2018 at 02:46):

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

view this post on Zulip Reid Barton (Dec 03 2018 at 02:48):

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!

view this post on Zulip Reid Barton (Dec 03 2018 at 02:48):

Is there a catch?

view this post on Zulip Reid Barton (Dec 03 2018 at 02:50):

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

view this post on Zulip Sebastien Gouezel (Dec 28 2019 at 18:57):

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.

view this post on Zulip Kevin Buzzard (Dec 29 2019 at 15:03):

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!

view this post on Zulip Chris Hughes (Dec 29 2019 at 17:14):

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.

view this post on Zulip Chris Hughes (Dec 29 2019 at 17:16):

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

view this post on Zulip Chris Hughes (Dec 29 2019 at 17:16):

I might be completely wrong.

view this post on Zulip Chris Hughes (Dec 29 2019 at 17:18):

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

view this post on Zulip Chris Hughes (Dec 29 2019 at 17:18):

Which is difficult with the metavariables there.

view this post on Zulip Chris Hughes (Dec 29 2019 at 17:21):

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

view this post on Zulip Chris Hughes (Dec 29 2019 at 17:22):

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

view this post on Zulip Chris Hughes (Dec 29 2019 at 17:42):

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.

view this post on Zulip Paul van Wamelen (Jan 23 2021 at 19:59):

Is there documentation for abbreviation?

view this post on Zulip Paul van Wamelen (Jan 23 2021 at 20:14):

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


Last updated: May 16 2021 at 21:11 UTC