simp theorem iff true

Stream: general

[Sean Leather]

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]

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

[Sean Leather]

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

[Gabriel Ebner]

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]

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]

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]

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

[Gabriel Ebner]

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]

Right, makes sense.

[Sean Leather]

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

[Gabriel Ebner]

I don't think so.

[Sean Leather]

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]

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

[Gabriel Ebner]

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

[Sean Leather]

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

[Sean Leather]

(where t₂ may or may not be conditional)