refine_struct not working as advertised?

[semorrison]

The example in comments for refine_struct suggests using refine_struct ({ .. } : semigroup α), but I can't get this to work.

Here's my MWE:

import tactic.interactive

variable (α : Type)
def foo : semigroup α := 
begin
  refine_struct ({ .. } : semigroup α),
end

This just says failed at the refine_struct. Instead I expected it to give me two tagged goals.

[spl]

@cipher1024 says: “Yeah, refine_struct is not particularly tolerant. It only accepts a literal record. It infers semigroup from the goal.”

[cipher1024]

The goal is for refine_struct to eventually implement a superset of the features of refine.

[cipher1024]

Would refine_struct { .. } work for you?

[cipher1024]

I had a few minutes so I implemented the following:

def my_foo {α} (x : semigroup α) (y : group α) : true := trivial

example {α : Type} : true :=
begin
  refine_struct (@my_foo α { .. } { .. } ),
    -- 9 goals
    -- case semigroup, mul
    -- α : Type
    -- ⊢ α → α → α

    -- case semigroup, mul_assoc
    -- α : Type
    -- ⊢ ∀ (a b c : α), a * b * c = a * (b * c)

    -- case group, mul
    -- α : Type
    -- ⊢ α → α → α

    -- case group, mul_assoc
    -- α : Type
    -- ⊢ ∀ (a b c : α), a * b * c = a * (b * c)

    -- case group, one
    -- α : Type
    -- ⊢ α

    -- case group, one_mul
    -- α : Type
    -- ⊢ ∀ (a : α), 1 * a = a

    -- case group, mul_one
    -- α : Type
    -- ⊢ ∀ (a : α), a * 1 = a

    -- case group, inv
    -- α : Type
    -- ⊢ α → α

    -- case group, mul_left_inv
    -- α : Type
    -- ⊢ ∀ (a : α), a⁻¹ * a = 1

end

That should cover it :)

[cipher1024]

See: #162

[cipher1024]

Should we rename the tactic to refine' since it overlaps so much with the purpose of refine?

[spl]

Since #162 has been merged, can we close this issue?

[cipher1024]

I would say so. Let's see if that satisfies @semorrison.