## Stream: general

### Topic: simp lemmas for Prop-valued structures

#### 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 @[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 (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):

does mk_iff_of_inductive_prop work?

#### 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 mk_iff.

Last updated: May 11 2021 at 00:31 UTC