Zulip Chat Archive

Stream: new members

Topic: fin eq not unified

Patrick Thomas (Sep 22 2022 at 07:31):

Why can't ↑a = ↑b be unified with ↑a = ↑b?

import data.finset

example
    {α : Type}
    (n : ℕ)
    (f : fin n.succ → α)
    (nodup : function.injective f) :
    function.injective (fun (i : fin n), f ↑i) :=
begin
    unfold function.injective at *,
    intros a b h1,
    specialize nodup h1,
    apply fin.ext, apply nodup,
end

Ruben Van de Velde (Sep 22 2022 at 07:33):

In vs code, you can click on the ↑a in the tactic state

Ruben Van de Velde (Sep 22 2022 at 07:34):

Screenshot-from-2022-09-22-09-34-04.png Screenshot-from-2022-09-22-09-33-55.png

Patrick Thomas (Sep 22 2022 at 07:36):

Hmm. One is a nat and the other is a fin n.succ?

Ruben Van de Velde (Sep 22 2022 at 07:36):

Indeed

Patrick Thomas (Sep 22 2022 at 07:37):

Ok. Thank you.

Patrick Thomas (Sep 22 2022 at 07:41):

Do you know what the double curly braces mean in function.injective f = ∀ ⦃a₁ a₂ : α⦄, f a₁ = f a₂ → a₁ = a₂?

Patrick Thomas (Sep 22 2022 at 07:42):

Is there a way to lookup that kind of notation?

Ruben Van de Velde (Sep 22 2022 at 07:46):

It's some sort of implicit argument - I don't recall where they're documented

Patrick Thomas (Sep 22 2022 at 07:53):

Hmm. Ok.
Is using fin.ext the wrong thing here? I'm not sure I understand what is happening to make them different types.

Patrick Thomas (Sep 22 2022 at 07:56):

Oh. https://github.com/leanprover-community/mathlib/blob/88f41bb0bd5c895bca82a7900b0b6a205fd0e937/src/data/fin/basic.lean#L117

Eric Wieser (Sep 22 2022 at 07:58):

I would guess that refine nodup.comp _ almost closes this goal

Patrick Thomas (Sep 22 2022 at 08:01):

Screenshot-from-2022-09-22-01-00-35.png

Eric Wieser (Sep 22 2022 at 08:01):

I mean right at the start

Eric Wieser (Sep 22 2022 at 08:06):

The coercion you have here is a nasty one; it's the transitive one found by fin n -> nat -> fin m.succ, and it's only injective if n <= m.succ

Eric Wieser (Sep 22 2022 at 08:07):

Running dsimp (on the appropriate target) will expand the transitive coercion into two coercions, which makes it easier to make progress

Patrick Thomas (Sep 22 2022 at 08:10):

I'm sorry, I'm not sure if I follow.

Eric Wieser (Sep 22 2022 at 08:11):

Which message?

Patrick Thomas (Sep 22 2022 at 08:13):

The last one I think. Is that with the refine nodup.comp? I'm not sure how the refine nodup.comp helps.

Ruben Van de Velde (Sep 22 2022 at 08:13):

The thing you really want to prove is function.injective (λ (i : fin n), (i : fin n.succ)), and the refine changes your goal to that

Patrick Thomas (Sep 22 2022 at 08:15):

Hmm. Why is that what I really want to prove?

Patrick Thomas (Sep 22 2022 at 08:16):

Because it is the middle step of the transitivity relation?

Ruben Van de Velde (Sep 22 2022 at 08:16):

Exactly, yes

Ruben Van de Velde (Sep 22 2022 at 08:17):

I still found it quite painful to prove from there, because it seems like there's a better-supported way to write λ (i : fin n), (i : fin n.succ) in mathlib (and simp finds it)

Patrick Thomas (Sep 22 2022 at 08:21):

You mean there is a better way to state the theorem?

Patrick Thomas (Sep 22 2022 at 08:24):

Screenshot-from-2022-09-22-01-24-14.png

Eric Rodriguez (Sep 22 2022 at 08:25):

Patrick Thomas said:

Do you know what the double curly braces mean in function.injective f = ∀ ⦃a₁ a₂ : α⦄, f a₁ = f a₂ → a₁ = a₂?

{}s have this issue that if, for example, you have def test {a : Type*} (b : Type*) := a -> b, then they'll be greedy: that is have := test will have type @test ?m_1 : Type* -> Type*, while maybe instead you wanted @test : Type* -> Type* -> Type*. double curly braces do this, and don't resolve the implicitness until you write any explicit arguments that come after; that is, have := test2 would be @test2, but have := test2 nat would be @test2 ?m_1 nat

Ruben Van de Velde (Sep 22 2022 at 08:26):

Perhaps yes:

example
    {α : Type}
    (n : ℕ)
    (f : fin n.succ → α)
    (nodup : function.injective f) :
    function.injective (fun (i : fin n), f i.cast_succ) :=
nodup.comp (fin.cast_succ_injective _)

Patrick Thomas (Sep 22 2022 at 08:33):

You mean the i.cast_succ instead of ↑i? I thought the second was notation for the first?

Patrick Thomas (Sep 22 2022 at 08:38):

Eric Rodriguez said:

Patrick Thomas said:

Do you know what the double curly braces mean in function.injective f = ∀ ⦃a₁ a₂ : α⦄, f a₁ = f a₂ → a₁ = a₂?

{}s have this issue that if, for example, you have def test {a : Type*} (b : Type*) := a -> b, then they'll be greedy: that is have := test will have type @test ?m_1 : Type* -> Type*, while maybe instead you wanted @test : Type* -> Type* -> Type*. double curly braces do this, and don't resolve the implicitness until you write any explicit arguments that come after; that is, have := test2 would be @test2, but have := test2 nat would be @test2 ?m_1 nat

Thank you. I might need to call it a night and revisit this.

Eric Wieser (Sep 22 2022 at 08:52):

I thought the second was notation for the first?

Hah, you wish!

Eric Wieser (Sep 22 2022 at 08:55):

Here, ↑i is notation for ↑↑i which is notation for ↑i.val which is notation for has_nat_cast.nat_cast i.val which is _probably_ notation for fin.mk (i.val % n) _

Patrick Thomas (Sep 23 2022 at 03:44):

I see.
Is there a way in Lean to unfold notation like this?

Kyle Miller (Sep 23 2022 at 04:07):

tactic#unfold_coes is one way to unfold coercions

Patrick Thomas (Sep 23 2022 at 04:19):

Thank you. Is there any generic way to see how a notation is defined?

Eric Wieser (Sep 23 2022 at 07:03):

Hover over it the goal view?

Last updated: Dec 20 2023 at 11:08 UTC