## Stream: new members

### Topic: Unfolding and reflection

#### Pedro Minicz (May 18 2020 at 03:50):

refl can't manage n ≥ n, yet unfolding solves reflection automatically, which is nice, don't get me wrong. I feel like refl and simp should unfold trivial definitions. Where can I read about Lean's unfolding mechanics? Definitions annotated with @[simp] will unfold on simplification if I am not mistaken, is there an equivalent for relf? Also, why doesn't core/mathlib use automatic unfolding more aggressively?

example {n : ℝ} : n ≥ n := by unfold ge
example {n : ℝ} : n ≥ n := by refl -- Fails!


#### Shing Tak Lam (May 18 2020 at 03:54):

There is a @[refl] attribute, which means that this works:

import data.set.basic

example {α : Type} (A : set α) : A ⊆ A :=
begin
refl,
end


(duplicate)

#### Shing Tak Lam (May 18 2020 at 03:58):

In fact, your example works if you switch ge for le.

example {n : ℕ} : n ≤ n := by refl


#### Shing Tak Lam (May 18 2020 at 04:04):

Since there is this lemma

@[refl] lemma le_refl [preorder α] : ∀ a : α, a ≤ a :=
preorder.le_refl


#### Bryan Gin-ge Chen (May 18 2020 at 04:19):

Thus:

import data.real.basic

@[refl] lemma ge_refl (α : Type*) [preorder α] :
∀ a : α, a ≥ a :=
preorder.le_refl

example {n : ℝ} : n ≥ n := by unfold ge
example {n : ℝ} : n ≥ n := by refl -- works!


#### Pedro Minicz (May 18 2020 at 16:26):

@Bryan Gin-ge Chen neat!

#### Pedro Minicz (May 18 2020 at 16:27):

Any reason why core/mathlib doesn't include that definition? Is it by design or something that was just not added?

#### Kevin Buzzard (May 18 2020 at 16:29):

mathlib doesn't contain any ≥ lemmas

#### Alex J. Best (May 18 2020 at 16:29):

A conscious decision was made to reduce duplication and only work with less than as much as possible (with a few exceptions), so almost all results in mathlib are stated with less than as assumption (hence you should use the less than version of everything too where possible)

#### Pedro Minicz (May 18 2020 at 16:46):

Talking about design decisions, why not merge intros/rintros, cases/rcases, etc. The recursive counterparts work like the vanilla ones if the user doesn't pattern match the arguments.

#### Johan Commelin (May 18 2020 at 16:58):

Pedro Minicz said:

Talking about design decisions, why not merge intros/rintros, cases/rcases, etc. The recursive counterparts work like the vanilla ones if the user doesn't pattern match the arguments.

We've been talking about that before. For cases/rcases it's a bit delicate. But intros/rintros could certainly be done. However intros is in core lib, and rintros in mathlib. So it would require a bit of work.

#### Pedro Minicz (May 18 2020 at 17:21):

I see, thank you. Could you point me to the discussion about cases/rcases, I'd be interested in understanding what makes it more difficult.

#### Bryan Gin-ge Chen (May 18 2020 at 17:23):

There's some discussion here. There might be some older ones as well if you search for rcases.

#### Bryan Gin-ge Chen (May 18 2020 at 17:24):

I guess the upshot is that rcases h with ... and cases h with ... are not compatible.

Last updated: May 08 2021 at 10:12 UTC