Bryan Gin-ge Chen (Oct 25 2020 at 20:10):
Consider the following example code:
import tactic variables (x y : ℕ) structure foo : Prop := (plus : x + y = 4) (mul : y * x = 3) @[simp] lemma foo_iff : foo x y ↔ x + y = 4 ∧ y * x = 3 := ⟨λ h, ⟨h.1, h.2⟩, λ h, ⟨h.1, h.2⟩⟩ example : foo 1 3 := begin -- norm_num [foo], -- doesn't work norm_num [foo_iff], end def foo' : Prop := x + y = 4 ∧ y * x = 3 example : foo' 1 3 := begin norm_num [foo'], end
Is there automation to generate
foo_iff (or something similar) automatically from
foo? I was kind of hoping
foo would work, but apparently it doesn't like
Props. Failing that, is there a tactic that will prove stuff like
The use case is in the first
example, I need
foo_iff to get
norm_num to "see through"
foo. While I could switch to using
foo' is more unwieldy to use since you end up with
.2 everywhere (particularly when there are more fields in the structure).
Floris van Doorn (Oct 26 2020 at 19:12):
@[simps] is not designed for this: it creates simp-lemmas for fields of instances of a structure, not for showing that a structure is equivalent to another expression.
Writing a metaprogram that does this for you is not very hard, although the difficulty increases if you want to make it more general: you could allow dependencies between the fields, and make those equivalent to existential quantifiers, and you could allow type-valued structures, and show them
equivalent to a type built from (p)sigma's.
Mario Carneiro (Oct 26 2020 at 19:18):
Bryan Gin-ge Chen (Oct 26 2020 at 19:52):
Thanks! It did exactly what I wanted in #4599 (any other maintainers want to check this real quick?).
It might be easier to use as an attribute?
Bryan Gin-ge Chen (Nov 01 2020 at 03:56):
See #4863. I named the attribute
Last updated: May 11 2021 at 00:31 UTC