Zulip Chat Archive

Stream: new members

Topic: Unfolding and reflection


view this post on Zulip 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!

view this post on Zulip 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

view this post on Zulip Shing Tak Lam (May 18 2020 at 03:54):

(duplicate)

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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!

view this post on Zulip Pedro Minicz (May 18 2020 at 16:26):

@Bryan Gin-ge Chen neat!

view this post on Zulip 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?

view this post on Zulip Kevin Buzzard (May 18 2020 at 16:29):

mathlib doesn't contain any lemmas

view this post on Zulip 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)

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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