Stream: new members
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...
Yakov Pechersky (Sep 25 2020 at 21:36):
Try stating the iff in reverse, and supplying that to simp
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.
Jesse Selover (Sep 26 2020 at 01:50):
thank you! I will try that
Jesse Selover (Sep 26 2020 at 02:31):
Stating the iff in reverse worked!
Last updated: May 15 2021 at 00:39 UTC