fin hell

Stream: general

[Patrick Massot]

I have a fun little puzzle for people who like that kind of "fun little puzzle":

import data.fin.basic

example {n : ℕ} (k : fin n) (j : fin (n + 1)) :
  j < k + 1 ↔ j < k ∨ j = k  :=
sorry

[Johan Commelin]

This ought to be cases k, cases j, linarith.

[Patrick Massot]

namespace profinitely_filtered_pseudo_normed_group_with_Tinv will save you this time

[Yaël Dillies]

docs#succ_order.lt_succ_iff_lt_or_eq

[Johan Commelin]

s/linarith/omega/?

[Yaël Dillies]

docs#succ_order.lt_succ_iff along with docs#le_iff_lt_or_eq?

[Yaël Dillies]

or rather the more general version of lt_succ_iff which takes in a proof that k is not maximal rather than inferring it from no_max_order.

[Eric Wieser]

I did not know that we had a coercion from fin n to fin (n + 1)

[Eric Wieser]

example {n : ℕ} (k : fin n) (j : fin (n + 1)) :
  j < k + 1 ↔ j < k ∨ j = k  :=
by simpa [fin.lt_def, fin.ext_iff] using nat.lt_succ_iff_lt_or_eq

[Yaël Dillies]

My way using succ_order would be much easier if fin addition was absorbent...

[Reid Barton]

k + 1 really shouldn't appear in the statement at all

[Yaël Dillies]

The succ I'm getting is λ a, if a = fin.last n then fin.last n else a + 1, not λ a, a + 1 as you would expect.

[Reid Barton]

There is already a function for this, namely docs#fin.succ. But then the right hand side is awkward, maybe it should be about fin.cast_succ j.

[Eric Wieser]

simp changes the statement to j < k.succ ↔ j < ⇑fin.cast_succ k ∨ j = ⇑fin.cast_succ k

[Patrick Massot]

There may be a #xy issue here. The full context is:

import linear_algebra.basis

noncomputable theory

universe u

open function set submodule
open_locale classical big_operators

variables {R : Type*} [semiring R]
          {M : Type*} [add_comm_monoid M] [module R M]

def basis.flag {n : ℕ} (b : basis (fin $ n + 1) R M) : fin (n + 1) → submodule R M :=
λ k, span R (b '' {j | j < k})

@[simp] lemma basis.flag_zero {n : ℕ} (b : basis (fin $ n + 1) R M) : b.flag 0 = ⊥ :=
sorry

@[simp] lemma basis.flag_last {n : ℕ} (b : basis (fin $ n + 1) R M) : b.flag (fin.last n) = ⊤  :=
sorry

@[simp] lemma basis.flag_mono {n : ℕ} (b : basis (fin $ n + 1) R M) : monotone b.flag :=
sorry

lemma pain {n : ℕ} (k : fin n) (j : fin (n + 1)) :
  j < k + 1 ↔ j < k ∨ j = k  :=
sorry

@[simp] lemma basis.flag_span_succ {n : ℕ} (b : basis (fin $ n + 1) R M) (k : fin n) :
  b.flag k ⊔ span R {b k} = b.flag k.succ :=
begin
  rw [basis.flag, ← span_union, ← image_singleton, ← image_union],
  congr,
  ext j,
  suffices : j = k ∨ j < k ↔ j < k + 1, by simpa,
  rw pain,
  tauto
end

[Patrick Massot]

You can see the weird goal is generated by simp in the suffices.

[Patrick Massot]

Maybe the correct path is to forget about fin and define a function on nat.

[Reid Barton]

In basis.flag shouldn't b be a basis of size n?

[Patrick Massot]

I don't really care. Maybe I was too cautious there.

[Reid Barton]

I mean, if M is dimension 3 then a flag has 4 subspaces (of dimensions 0, 1, 2, 3)

[Patrick Massot]

Oh I see. I got my counting wrong.

[Patrick Massot]

Now I need to fight casts and inclusion even in the definition of basis.flag :sob:

[Reid Barton]

Patrick Massot said:

Maybe the correct path is to forget about fin and define a function on nat.

This seems very reasonable. You could even use int if there was some use for it.

[Bolton Bailey]

Just as we have tactics#zify to transition from N to Z, we should have nify to transition from fin to N.

[Yakov Pechersky]

You can always "cases i" to destruct your fin into the underlying nat value. And then rely on simp lemmas