## Stream: general

### Topic: Figure out the rest by cc

#### Johan Commelin (Aug 02 2018 at 14:00):

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,
one_smul := by cc,
mul_smul := by cc,


#### Johan Commelin (Aug 02 2018 at 14:01):

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

#### Scott Morrison (Aug 02 2018 at 14:02):

sure, something like:

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


#### Johan Commelin (Aug 02 2018 at 14:04):

Aaah, I need to understand refine.

#### Scott Morrison (Aug 02 2018 at 14:06):

Curiously that doesn't actually work...

#### Scott Morrison (Aug 02 2018 at 14:06):

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

#### Scott Morrison (Aug 02 2018 at 14:07):

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 (Aug 02 2018 at 14:07):

finish works instead of cc.

#### Kenny Lau (Aug 02 2018 at 14:08):

what is obviously? is it in mathlib?

#### Johan Commelin (Aug 02 2018 at 14:09):

No, it is Scott's Hammer.

#### Johan Commelin (Aug 02 2018 at 14:09):

Well, maybe tidy is his hammer.

#### Sean Leather (Aug 02 2018 at 14:10):

obviously

#### Johan Commelin (Aug 02 2018 at 14:11):

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


#### Johan Commelin (Aug 02 2018 at 14:11):

Let's assume we open punit.

#### Scott Morrison (Aug 02 2018 at 14:12):

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 (Aug 02 2018 at 14:12):

isn't the right command constructor

#### Kenny Lau (Aug 02 2018 at 14:13):

split is for inductive types I think

#### Johan Commelin (Aug 02 2018 at 14:13):

constructor also fails...

Last updated: May 17 2021 at 22:15 UTC