Zulip Chat Archive

Stream: general

Topic: simp theorem iff true


view this post on Zulip Sean Leather (May 18 2018 at 11:23):

What's the difference in simp behavior (if any) between these two theorems for p : Prop? Is one or the other preferable?

@[simp] theorem t₁ (...) : p  true := ...
@[simp] theorem t₂ (...) : p := ...

view this post on Zulip Gabriel Ebner (May 18 2018 at 11:34):

There is a difference if p is an equation or another simp relation.

view this post on Zulip Sean Leather (May 18 2018 at 11:37):

Can you expand on that? I'm not sure what “another simp relation” is. Is there an example?

view this post on Zulip Gabriel Ebner (May 18 2018 at 11:44):

Good question! If you have a relation R that is reflexive and transitive (as tagged with @[refl] and @[trans]), then you can use the simplifier to get proofs of R x ?m_1 where ?m_1 is the simplified version of x. For example think of equivalence relations such as equality modulo k in the integers.

view this post on Zulip Gabriel Ebner (May 18 2018 at 11:46):

In mathlib it is used for the equivalence relation on types, where types are equivalent if they are equinumerous (have a bijection between them). Then you can simplify a ⨉ unit to a for example.

view this post on Zulip Sean Leather (May 18 2018 at 11:48):

Okay. Suppose I have these:

@[simp] theorem t₁ (...) : a = b  true := ...
@[simp] theorem t₂ (...) : a = b := ...

I would intuitively write t₂ and not t₁ because I know = is a simp relation, right? What happens if you have t₁ instead of t₂?

view this post on Zulip Gabriel Ebner (May 18 2018 at 11:48):

https://github.com/leanprover/mathlib/blob/38d553694351f4c23a8a8216038c7c8abcb7cd32/data/equiv.lean#L166-L177

view this post on Zulip Gabriel Ebner (May 18 2018 at 11:49):

What happens if you have t₁ instead of t₂?

Then simp won't be able to solve b = a, for instance. It will only rewrite a = b to true.

view this post on Zulip Sean Leather (May 18 2018 at 11:49):

Right, makes sense.

view this post on Zulip Sean Leather (May 18 2018 at 11:50):

And if p is not a simp relation, is there any difference between the two?

view this post on Zulip Gabriel Ebner (May 18 2018 at 11:50):

I don't think so.

view this post on Zulip Sean Leather (May 18 2018 at 11:52):

In mathlib, I see these:

$ git grep "↔ true"
data/finset.lean:theorem forall_mem_empty_iff (p : α  Prop) : ( x, x  ( : finset α)  p x)  true :=
data/set/basic.lean:  ( x  ( : set α), p x)  true :=
logic/basic.lean:@[simp] theorem imp_self : (a  a)  true := iff_true_intro id
logic/basic.lean:@[simp] theorem imp_true_iff {α : Sort*} : (α  true)  true :=
logic/basic.lean:@[simp] theorem forall_true_iff : (α  true)  true :=
logic/basic.lean:theorem forall_true_iff' (h :  a, p a  true) : ( a, p a)  true :=
logic/basic.lean:@[simp] theorem forall_2_true_iff {β : α  Sort*} : ( a, β a  true)  true :=
logic/basic.lean:  ( a (b : β a), γ a b  true)  true :=
logic/basic.lean:@[simp] theorem forall_prop_of_false {p : Prop} {q : p  Prop} (hn : ¬ p) : ( h' : p, q h')  true :=
logic/basic.lean:theorem ball_true_iff (p : α  Prop) : ( x, p x  true)  true :=

view this post on Zulip Sean Leather (May 18 2018 at 11:54):

I suppose the /Π is special, thus theorem forall_true_iff : (α → true) ↔ true.

view this post on Zulip Gabriel Ebner (May 18 2018 at 11:54):

Yes, without the iff true, those would be conditional simp lemmas.

view this post on Zulip Sean Leather (May 18 2018 at 11:56):

Right. So, with these few exceptions, we should write @[simp] theorem t₂ (...) : p := ....

view this post on Zulip Sean Leather (May 18 2018 at 11:57):

(where t₂ may or may not be conditional)


Last updated: May 08 2021 at 19:11 UTC