naming some lemmas about Prop

Stream: Is there code for X?

[Kim Morrison]

What should these be called?

@[simp] theorem or_and_left_self_left : a ∨ (a ∧ b) ↔ a := sorry
@[simp] theorem or_and_left_self_right : a ∨ (b ∧ a) ↔ a := sorry
@[simp] theorem and_or_right_self_left : (a ∧ b) ∨ a ↔ a := sorry
@[simp] theorem and_or_right_self_right : (b ∧ a) ∨ a ↔ a := sorry

[Bjørn Kjos-Hanssen]

@[simp] theorem left_absorbs_or_self_left : a ∨ (a ∧ b) ↔ a := sorry
@[simp] theorem left_absorbs_or_self_right : a ∨ (b ∧ a) ↔ a := sorry
@[simp] theorem right_absorbs_or_self_left : (a ∧ b) ∨ a ↔ a := sorry
@[simp] theorem right_absorbs_or_self_right : (b ∧ a) ∨ a ↔ a := sorry

with duals having names starting like left_absorbs_and_self_left. At any rate, maybe include something about "absorb"?

[Kim Morrison]

Hmm, I'm hesitant to introduce a new keyword in the name scheme.

[Floris van Doorn]

How about following docs#add_sub_cancel_left ?

or_and_cancel_left
or_and_cancel_right
and_or_cancel_left
and_or_cancel_right

[Yaël Dillies]

But there's no cancellation, only absorption

[Yaël Dillies]

What about

or_and_absorbs_right
or_and_absorbs_left
and_or_absorbs_right
and_or_absorbs_left

[Sébastien Gouëzel]

I don't think absorbs is already used in this sense in Mathlib (as far as I can tell, it's mostly used for topological vector spaces, in a rather precise sense), so I'd rather avoid introducing new terminology that users couldn't guess. cancel would be more standard in this respect.

[Sébastien Gouëzel]

Another possibility is or_and_iff_self_left, or_and_iff_self_right, and_or_iff_self_left and and_or_iff_self_right.

[Yaël Dillies]

And what about these lemmas?

@[simp] theorem or_and_left_self_left : a ∧ (a ∨ b) ↔ a := sorry
@[simp] theorem or_and_left_self_right : a ∧ (b ∨ a) ↔ a := sorry
@[simp] theorem and_or_right_self_left : (a ∨ b) ∧ a ↔ a := sorry
@[simp] theorem and_or_right_self_right : (b ∨ a) ∧ a ↔ a := sorry

[Yaël Dillies]

Sébastien Gouëzel said:

I don't think absorbs is already used in this sense in Mathlib (as far as I can tell, it's mostly used for topological vector spaces, in a rather precise sense), so I'd rather avoid introducing new terminology that users couldn't guess.

Indeed, I am suggesting we introduce a new naming convention for lemmas of a new kind. We successfully similarly introduced anticomm, rotate and antidistrib in the past

[Yaël Dillies]

I maintain that these are not cancel lemmas

[Bjørn Kjos-Hanssen]

https://en.wikipedia.org/wiki/Absorption_law