function.injective fin

Stream: Is there code for X?

[Eric Wieser]

Is there a way of proving this earlier in the import heirarchy?

import data.fin.basic
import data.fintype.basic

lemma fin_injective : function.injective fin :=
λ m n h,
  (fintype.card_fin m).symm.trans $ (fintype.card_congr $ equiv.cast h).trans (fintype.card_fin n)

In particular, I'd like to state docs#fin.cast_eq_cast in reverse so that any docs#cast of fin can be turned into a docs#fin.cast

[Eric Rodriguez]

I have to go cook, but will something like this work?

import data.fin.basic

lemma fin_injective : function.injective fin :=
begin
  intros m n h,
  --simp only [fin] at h,
  cases m; cases n,
  { refl },
  { have hn := n.succ_pos,
    rw fin.pos_iff_nonempty at hn,
    have := hn.some,
    rw ←h at this,
    exact fin_zero_elim this },
  { have hm := m.succ_pos,
    rw fin.pos_iff_nonempty at hm,
    have := hm.some,
    rw h at this,
    exact fin_zero_elim this },
  { have := fin.last_val m,
    have := fin.last_val n,
    sorry }
end

Also, what do you mean about fin.cast_eq_cast in reverse?

[Yakov Pechersky]

Can you use the fact that fin.cast is a nonsurjective embedding? Going through lt_trichotomy n m.

[Eric Wieser]

Eric Rodriguez said:

Also, what do you mean about fin.cast_eq_cast in reverse?

I mean

theorem fin.cast_eq_cast' {n m : ℕ} (h : fin n = fin m) :
  cast h = ⇑(fin.cast $ fin_injective h) :=
(fin.cast_eq_cast _).symm

[Reid Barton]

It seems like the original proof is the correct one. Is this something you really need in practice? Using it feels like admitting that we messed up earlier, but can recover anyways.

[Eric Wieser]

I don't know for sure; the context of this is the callers ofsigma_eq_of_reindex_cast in #10255, where I actually only need the version when the index type is fin n. It probably makes more sense to state things in terms of fin.cast in that case, but if I can rewrite cast to fin.cast I don't need to add the special case there.

[Eric Wieser]

This probably also relates to your tuple stuff in #4406 vs docs#fin.append, where your tuple.append didn't take a proof argument, but docs#fin.append does.

[Reid Barton]

I don't see anywhere in either of these examples that involves thinking about fin n = fin m rather than n = m

[Eric Wieser]

(congr_arg ι h) on line 457 of pi_tensor_product is the statement fin n = fin m. I guess in theory you can recover h : n = m from that via inference though

[Reid Barton]

oh I didn't read the whole name of the function

[Reid Barton]

Well anyways, you obviously don't need this early in the import hierarchy

[Eric Wieser]

I need it early if I want to replace fin.cast_eq_cast with fin.cast_eq_cast' and make it a simp lemma, but I don't have a particularly good reason to need to do that.

[Eric Wieser]

Anyway, PR'd with the short proof as #10330

[Eric Rodriguez]

I mean, I think the list proof suffices

[Eric Rodriguez]

(as in, you can use list.range_fin and do exactly the same proof)

[Eric Wieser]

That proof is probably ugly in the middle step:

lemma fin_injective : function.injective fin :=
λ m n h,
  (list.length_fin_range m).symm.trans $ eq.trans sorry (list.length_fin_range n)

[Floris van Doorn]

This lemma talks about equality of types, which is "evil".

If we add this to the library, it should come with a warning , in my opinion.

In your application, the usage of docs#equiv.cast is also evil. The non-evil way to do this is to use

import data.equiv.basic

def equiv.cast' {ι} (P : ι → Type*) {i j : ι} (h : i = j) : P i ≃ P j :=
⟨cast (congr_arg P h), cast (congr_arg P h.symm),
  λ x, by { cases h, refl }, λ x, by { cases h, refl }⟩

[Floris van Doorn]

If you use that everywhere (where P = fin, of course), you should never have to worry about equality of types, only equality of different indices.

[Eric Rodriguez]

However, I think there is a way to get the evilness working; propext means that subtype is injective. Currently on mobile but I'll write this up when I get home

[Eric Wieser]

Floris van Doorn said:

The non-evil way to do this is to use

import data.equiv.basic

def equiv.cast' {ι} (P : ι → Type*) {i j : ι} (h : i = j) : P i ≃ P j :=
⟨cast (congr_arg P h), cast (congr_arg P h.symm),
  λ x, by { cases h, refl }, λ x, by { cases h, refl }⟩

Isn's this precisely src#equiv.cast other than congr_arg P h.symm vs (congr_arg P h).symm? docs#equiv.cast_symm fixes that part of the term anyway when actually working with equiv.cast

[Eric Rodriguez]

I am carrying on with my evil project... I really hope this is provable:

import data.fin.basic

example {α} : function.injective (@subtype α) :=
begin
  intros p q h,
  let f := equiv.cast h,
  ext,
  refine ⟨λ hp, _, sorry⟩,
  have := cast_heq h ⟨x, hp⟩,
  --rw subtype.heq_iff_coe_eq at this,
  convert (cast h ⟨x, hp⟩).prop, sorry
  -- x = ↑(cast h ⟨x, hp⟩)
  -- this: cast h ⟨x, hp⟩ == ⟨x, hp⟩
end

does anyone know?

[Reid Barton]

function.injective (@subtype α) isn't provable, but if you consider subtype p together with its associated subtype.val then it becomes injective.

[Gabriel Ebner]

I'm pretty sure this is independent of Lean. IIRC there is a model of Lean where α ≃ β → α = β is a theorem. And @subtype α (eq a) ≃ @subtype α (eq b) even if a ≠ b.

[Eric Rodriguez]

i thought univalence was incompatible with lean?

[Gabriel Ebner]

Univalence is more, it's (α ≃ β) ≃ (α = β) (roughly).

[Eric Rodriguez]

I need to just sit down and read the HoTT book some day. that's wild

[Johan Commelin]

It suffices to read the first bit. Which I found very readable.

[Floris van Doorn]

Eric Wieser said:

Isn's this precisely src#equiv.cast other than congr_arg P h.symm vs (congr_arg P h).symm? docs#equiv.cast_symm fixes that part of the term anyway when actually working with equiv.cast

It is the non-evil special case of equiv.cast

[Eric Wieser]

Although it's still evil when P = id, right?

[Floris van Doorn]

Yes, because then the argument h is evil.

[Eric Wieser]

What makes equiv.cast (congr_arg P h) more evil than equiv.cast' P h?

[Eric Wieser]

Can unification retrieve h in the latter case and not the former?