Modifying a structure

Stream: general

[Patrick Johnson]

What is the recommended way to work with structures that differ at some fields? I often want to prove that if x is a structure of some type, if some fields are modified with some other values, then some properties hold. The structures usually differ by only one field. A dumb example:

@[ext] structure T := (a b c d e f g h : ℕ)

example {x : T} : x = {x with a := 0} ↔ x.a = 0 :=
begin
  split; intro h,
  { rw h },
  { ext; simp [h] },
end

The problem is that it often requires ext, which is slow and creates a lot of trivial goals. Also, the notation is very ugly: x = {a := 0, b := x.b, c := x.c, d := x.d, e := x.e, f := x.f, g := x.g, h := x.h} ↔ x.a = 0 (is there a pp option I can set to make it show with with notation instead?). Another pattern would be to pass all fields as lemma arguments and then construct two different structures explicitly. It makes lemma statement much verboser and harder to work with.

[Reid Barton]

ext is slow? Never heard of that

[Patrick Johnson]

I didn't mean ext itself is slow, but ext creates a lot of goals and then ; simp is slow.

[Reid Barton]

cases x, simp works here

[Eric Wieser]

Presumably ext; try {refl} would also clean up all the unwanted goals

[Reid Barton]

One could imagine ext trying to do a reducible-transparency refl afterwards to get rid of any trivial goals automatically