Zulip Chat Archive

Stream: general

Topic: Modifying a structure

Patrick Johnson (Mar 18 2022 at 10:19):

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 :=
  split; intro h,
  { rw h },
  { ext; simp [h] },

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 (Mar 18 2022 at 10:20):

ext is slow? Never heard of that

Patrick Johnson (Mar 18 2022 at 10:21):

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

Reid Barton (Mar 18 2022 at 10:21):

cases x, simp works here

Eric Wieser (Mar 18 2022 at 10:22):

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

Reid Barton (Mar 18 2022 at 10:22):

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

Last updated: Aug 03 2023 at 10:10 UTC