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):

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

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: May 08 2021 at 19:11 UTC