Zulip Chat Archive

Stream: new members

Topic: teaching simp about my structure


view this post on Zulip Jesse Selover (Sep 25 2020 at 20:18):

Apologies for a rather vague question, but I'm wondering if there is a way to teach lean that only certain parts of my structure matter for equality?
I have a structure which is a combination of another structure and a proof, like:

structure sym_fn (σ : Type*) (α : Type*) :=
(series : mv_power_series σ α)
(series_sym :  (i j : σ) (f : σ →₀ ), series f = series (swap i j f))

And because different proofs of the same thing are equal, I've proved a helper lemma like

lemma series_part (x y : sym_fn σ α) : x.series = y.series  x = y := ...

Is that the appropriate thing to do? Is there a way to teach simp about that? I basically want to be able to infer that sym_fn addition is associative from the fact that mv_power_series addition is...

view this post on Zulip Yakov Pechersky (Sep 25 2020 at 21:36):

Try stating the iff in reverse, and supplying that to simp

view this post on Zulip Reid Barton (Sep 26 2020 at 00:14):

You can put the ext attribute on your structure, and it will prove your lemma under the name sym_fn.ext and mark it with the ext attribute so that the ext tactic will automatically use it.

view this post on Zulip Jesse Selover (Sep 26 2020 at 01:50):

thank you! I will try that

view this post on Zulip Jesse Selover (Sep 26 2020 at 02:31):

Stating the iff in reverse worked!


Last updated: May 15 2021 at 00:39 UTC