Tactic for adding projections to the lctx

Stream: Is there code for X?

[Adam Topaz]

Do we have a tactic that, given a term t of a structure S with projections p1, ..., pk, adds the projections t.pi to the local context? Context: I'm experimenting with the use of grind in category theory, and I think such a thing would be useful.

[Kenny Lau]

as in, you want let pi_t := t.pi?

[Adam Topaz]

yeah, essentially (or have instead of let when appropriate)

[Kenny Lau]

is that "basically" cases t?

[Adam Topaz]

Kenny Lau said:

is that "basically" cases t?

Yes, except that I want to keep t around as well.

[Adam Topaz]

structure Foo (a : ℕ) where
  b : ℕ
  h : a = b

example (a : ℕ) (t : Foo a) : True := by
  let t_b := t.b
  have h_b : a = t_b := t.h
  sorry

[Kenny Lau]

yep I agree that it would be useful. an "eta-deriver" would also be useful

[Adam Topaz]

Kenny Lau said:

an "eta-deriver" would also be useful

What do you mean by this?

[Kenny Lau]

import Mathlib.Data.Nat.Notation

structure Foo (a : ℕ) where
  b : ℕ
  h : a = b

theorem Foo.eta {a : ℕ} (n : Foo a) : n = ⟨n.b, n.h⟩ :=
  rfl

[Adam Topaz]

Oh I see, you want @[eta] to generate Foo.eta?

[Adam Topaz]

Yeah, I agree that would be useful as well.

[Michael Rothgang]

I would also have a use for this, in the context of positivity/finiteness/field_simp

[Bhavik Mehta]

Adam Topaz said:

Kenny Lau said:

is that "basically" cases t?

Yes, except that I want to keep t around as well.

Does cases (id t) get you close enough?

[Aaron Liu]

you get the parts of t but not the fact that t is made of those parts

[Ruben Van de Velde]

cases h : id t?