Figure out the rest by cc

Stream: general

[Johan Commelin]

Can I tell Lean to work out the rest by cc:

import algebra.module

variables {R : Type} [ring R]

open punit

def zero_module : module R punit :=
  { smul := λ _ _, star,
    zero := star,
    add  := λ _ _, star,
    neg  := λ _, star,
    add_zero := by cc,
    zero_add := by cc,
    add_comm := by cc,
    add_left_neg := by cc,
    one_smul := by cc,
    mul_smul := by cc,
    add_smul := by cc,
    smul_add := by cc,
    add_assoc := by cc }

[Johan Commelin]

I found that I was repeating myself, while trying to make a point to Lean.

[Scott Morrison]

sure, something like:

begin
  refine
  { smul := λ _ _, star,
    zero := star,
    add  := λ _ _, star,
    neg  := λ _, star,
    .. } ; cc
end

[Johan Commelin]

Aaah, I need to understand refine.

[Scott Morrison]

Curiously that doesn't actually work...

[Scott Morrison]

Of course, replacing cc with obviously does it. :-)

[Scott Morrison]

In fact just by obviously should work, except for some reason split doesn't work on modules, for some reason I can't see at the moment (type class inference throws an error?)

[Johan Commelin]

finish works instead of cc.

[Kenny Lau]

what is obviously? is it in mathlib?

[Johan Commelin]

No, it is Scott's Hammer.

[Johan Commelin]

Well, maybe tidy is his hammer.

[Sean Leather]

obviously

[Johan Commelin]

So, the current golf record is:

def zero_module' : module R punit :=
by refine
{ add := λ x y, punit.star,
  zero := punit.star,
  neg := λ x, punit.star,
  smul := λ c x, punit.star,
  .. }; finish

[Kenny Lau]

gadvardammt finish

[Johan Commelin]

Let's assume we open punit.

[Scott Morrison]

If someone can explain to me why you can't split when the goal is a module, maybe I can golf the entire proof to by tidy.

[Kenny Lau]

isn't the right command constructor

[Kenny Lau]

split is for inductive types I think

[Johan Commelin]

constructor also fails...