simp lemmas for Prop-valued structures

Stream: general

[Bryan Gin-ge Chen]

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 @[simps] on foo would work, but apparently it doesn't like Props. Failing that, is there a tactic that will prove stuff like foo_iff?

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 norm_num [foo'], foo' is more unwieldy to use since you end up with .1 and .2 everywhere (particularly when there are more fields in the structure).

[Floris van Doorn]

@[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]

does mk_iff_of_inductive_prop work?

[Bryan Gin-ge Chen]

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]

See #4863. I named the attribute mk_iff.