# Zulip Chat Archive

## 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 `Prop`

s. 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 `equiv`

alent 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