Unfolding and reflection

Stream: new members

[Pedro Minicz]

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]

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

import data.set.basic

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

[Shing Tak Lam]

(duplicate)

[Shing Tak Lam]

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

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

[Shing Tak Lam]

Since there is this lemma

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

[Bryan Gin-ge Chen]

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]

@Bryan Gin-ge Chen neat!

[Pedro Minicz]

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

[Kevin Buzzard]

mathlib doesn't contain any ≥ lemmas

[Alex J. Best]

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]

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]

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]

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]

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

[Bryan Gin-ge Chen]

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