# Zulip Chat Archive

## Stream: general

### Topic: simp theorem iff true

#### 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 := ...

#### Gabriel Ebner (May 18 2018 at 11:34):

There is a difference if `p`

is an equation or another simp relation.

#### 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?

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

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

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

?

#### Gabriel Ebner (May 18 2018 at 11:48):

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

#### Sean Leather (May 18 2018 at 11:49):

Right, makes sense.

#### Sean Leather (May 18 2018 at 11:50):

And if `p`

is not a `simp`

relation, is there any difference between the two?

#### Gabriel Ebner (May 18 2018 at 11:50):

I don't think so.

#### 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 :=

#### Sean Leather (May 18 2018 at 11:54):

I suppose the `→`

/`Π`

is special, thus `theorem forall_true_iff : (α → true) ↔ true`

.

#### Gabriel Ebner (May 18 2018 at 11:54):

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

#### Sean Leather (May 18 2018 at 11:56):

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

.

#### Sean Leather (May 18 2018 at 11:57):

(where `t₂`

may or may not be conditional)

Last updated: Dec 20 2023 at 11:08 UTC