## Stream: new members

### Topic: Structure unpacking again

#### Eric Wieser (Nov 20 2020 at 17:17):

I'm sure I've run into this before, but I can never remember how to get out of it:

import linear_algebra.quadratic_form

variables {R : Type*} [comm_ring R]
variables {M : Type*} [add_comm_group M] [module R M]
variables {Q : quadratic_form R M}

variables (Q)

include Q
structure pre :=
(k : R)
(factors : list M)

lemma pre.mk_eta (b : pre Q) : b = pre.mk b.k b.factors := begin
sorry -- b = {k := b.k, factors := b.factors}
end


#### Adam Topaz (Nov 20 2020 at 17:18):

cases b, simp

#### Adam Topaz (Nov 20 2020 at 17:18):

Maybe cases b, refl?

#### Eric Wieser (Nov 20 2020 at 17:25):

A question continuing from that example...

instance : monoid (pre Q) :=
{ mul := λ a b, ⟨a.k * b.k, a.factors ++ b.factors⟩,
mul_assoc := λ a b c, begin
dunfold has_mul.mul semigroup.to_has_mul,
dsimp only,
rw distrib.mul_assoc,
end,
one := ⟨1, []⟩,
one_mul := λ a, begin
sorry
end,
mul_one := λ a, begin
sorry,
end,
}


I can't work out how to unfold the definition of mul := ... without also unfolding the * within that definition, which I don't want to touch

#### Reid Barton (Nov 20 2020 at 17:27):

Put @[ext] on structure pre and use ext as the first step, then just apply the lemmas you need

#### Adam Topaz (Nov 20 2020 at 17:28):

import linear_algebra.quadratic_form

variables {R : Type*} [comm_ring R]
variables {M : Type*} [add_comm_group M] [module R M]
variables {Q : quadratic_form R M}

variables (Q)

include Q
@[ext]
structure pre :=
(k : R)
(factors : list M)

lemma pre.mk_eta (b : pre Q) : b = pre.mk b.k b.factors := begin
cases b, refl
end

instance : monoid (pre Q) :=
{ mul := λ a b, ⟨a.k * b.k, a.factors ++ b.factors⟩,
mul_assoc := λ a b c, begin
ext,
simp [mul_assoc],
simp,
end,
one := ⟨1, []⟩,
one_mul := λ a, begin
sorry
end,
mul_one := λ a, begin
sorry,
end,
}


#### Eric Wieser (Nov 20 2020 at 17:29):

ext1; dsimp only does the unfolding I need in mul_assoc

#### Eric Wieser (Nov 20 2020 at 17:29):

But it doens't do the job for one_mul - the one is stubborn and doesn't unfold

#### Adam Topaz (Nov 20 2020 at 17:33):

You can always use change :-/

#### Eric Wieser (Nov 20 2020 at 17:34):

instance : monoid (pre Q) :=
{ mul := λ a b, ⟨a.k * b.k, a.factors ++ b.factors⟩,
one := ⟨1, []⟩,
mul_assoc := λ a b c, pre.ext _ _ (mul_assoc _ _ _) (list.append_assoc _ _ _),
one_mul := λ a, pre.ext _ _ (one_mul _) (list.nil_append _),
mul_one := λ a, pre.ext _ _ (mul_one _) (list.append_nil _) }


#### Eric Wieser (Nov 20 2020 at 17:34):

But I still have no idea how to make tactic mode useful for me here

#### Eric Wieser (Nov 20 2020 at 17:35):

@[ext] was enough to save the day, I'd assumed that it was added automatically

#### Reid Barton (Nov 20 2020 at 17:40):

Well it's going to be hard to improve much on these term-mode proofs

#### Eric Wieser (Nov 20 2020 at 17:40):

It would be nice if I had a better toolbox to discover them

#### Reid Barton (Nov 20 2020 at 17:40):

but after ext, regardless of what Lean is showing you, you know the next step should be apply one_mul etc.

#### Eric Wieser (Nov 20 2020 at 17:40):

Well, I only "know" that if I know the goal state is definitionally equal to what I was expecting

#### Eric Wieser (Nov 20 2020 at 17:41):

But I can't use rw because its not syntactically equal

#### Reid Barton (Nov 20 2020 at 17:42):

But you do know that because you know what the definition of mul is and how Lean works

#### Eric Wieser (Nov 20 2020 at 17:43):

I'd be stuck if I didn't have a one-step proof for each of the fields though

#### Reid Barton (Nov 20 2020 at 17:43):

Not as long as you know step 1

#### Eric Wieser (Nov 20 2020 at 17:43):

Right, but i need to know it in terms of apply, not just in terms of a rewrite

#### Reid Barton (Nov 20 2020 at 17:43):

In this case the first step happens to also be the last step

#### Reid Barton (Nov 20 2020 at 17:44):

Sure, it could happen but it didn't

Last updated: May 08 2021 at 04:14 UTC