Zulip Chat Archive

Stream: general

Topic: Figure out the rest by cc


view this post on Zulip 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,
    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 }

view this post on Zulip Johan Commelin (Aug 02 2018 at 14:01):

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

view this post on Zulip Scott Morrison (Aug 02 2018 at 14:02):

sure, something like:

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

view this post on Zulip Johan Commelin (Aug 02 2018 at 14:04):

Aaah, I need to understand refine.

view this post on Zulip Scott Morrison (Aug 02 2018 at 14:06):

Curiously that doesn't actually work...

view this post on Zulip Scott Morrison (Aug 02 2018 at 14:06):

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

view this post on Zulip 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?)

view this post on Zulip Johan Commelin (Aug 02 2018 at 14:07):

finish works instead of cc.

view this post on Zulip Kenny Lau (Aug 02 2018 at 14:08):

what is obviously? is it in mathlib?

view this post on Zulip Johan Commelin (Aug 02 2018 at 14:09):

No, it is Scott's Hammer.

view this post on Zulip Johan Commelin (Aug 02 2018 at 14:09):

Well, maybe tidy is his hammer.

view this post on Zulip Sean Leather (Aug 02 2018 at 14:10):

obviously

view this post on Zulip 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

view this post on Zulip Kenny Lau (Aug 02 2018 at 14:11):

gadvardammt finish

view this post on Zulip Johan Commelin (Aug 02 2018 at 14:11):

Let's assume we open punit.

view this post on Zulip 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.

view this post on Zulip Kenny Lau (Aug 02 2018 at 14:12):

isn't the right command constructor

view this post on Zulip Kenny Lau (Aug 02 2018 at 14:13):

split is for inductive types I think

view this post on Zulip Johan Commelin (Aug 02 2018 at 14:13):

constructor also fails...


Last updated: May 17 2021 at 22:15 UTC