Structure unpacking again

Stream: new members

[Eric Wieser]

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]

cases b, simp

[Adam Topaz]

Maybe cases b, refl?

[Eric Wieser]

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]

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

[Adam Topaz]

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]

ext1; dsimp only does the unfolding I need in mul_assoc

[Eric Wieser]

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

[Adam Topaz]

You can always use change :-/

[Adam Topaz]

Or add some simp lemmas.

[Eric Wieser]

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]

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

[Eric Wieser]

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

[Reid Barton]

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

[Eric Wieser]

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

[Reid Barton]

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

[Eric Wieser]

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

[Eric Wieser]

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

[Reid Barton]

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

[Eric Wieser]

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

[Reid Barton]

Not as long as you know step 1

[Eric Wieser]

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

[Reid Barton]

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

[Reid Barton]

Sure, it could happen but it didn't