Zulip Chat Archive

Stream: general

Topic: simp lemmas for Prop-valued structures


view this post on Zulip 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).

view this post on Zulip 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.

view this post on Zulip Mario Carneiro (Oct 26 2020 at 19:18):

does mk_iff_of_inductive_prop work?

view this post on Zulip 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?

view this post on Zulip 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