Zulip Chat Archive

Stream: new members

Topic: Structure unpacking again


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

view this post on Zulip Adam Topaz (Nov 20 2020 at 17:18):

cases b, simp

view this post on Zulip Adam Topaz (Nov 20 2020 at 17:18):

Maybe cases b, refl?

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

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

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

view this post on Zulip Eric Wieser (Nov 20 2020 at 17:29):

ext1; dsimp only does the unfolding I need in mul_assoc

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

view this post on Zulip Adam Topaz (Nov 20 2020 at 17:33):

You can always use change :-/

view this post on Zulip Adam Topaz (Nov 20 2020 at 17:33):

Or add some simp lemmas.

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

view this post on Zulip Eric Wieser (Nov 20 2020 at 17:34):

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

view this post on Zulip Eric Wieser (Nov 20 2020 at 17:35):

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

view this post on Zulip Reid Barton (Nov 20 2020 at 17:40):

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

view this post on Zulip Eric Wieser (Nov 20 2020 at 17:40):

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

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

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

view this post on Zulip Eric Wieser (Nov 20 2020 at 17:41):

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

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

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

view this post on Zulip Reid Barton (Nov 20 2020 at 17:43):

Not as long as you know step 1

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

view this post on Zulip Reid Barton (Nov 20 2020 at 17:43):

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

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