Zulip Chat Archive

Stream: mathlib4

Topic: Inconsistent behaviour of `Fin.castPred`,`Fin.pred`, etc.

Wrenna Robson (Dec 14 2023 at 10:17):

Fin.castPred embeds Fin (n + 2) into Fin (n + 1) by reducing last (n + 1) to last n. It's defined as Fin.predAbove (last n).

However, Fin.pred (which to be fair is more fundamental - the order in which these functions are built also confuses me) more or less acts similarly, except instead it requires a proof that its input isn't 0 before reducing it. But it would be as easy for it to reduce everything by 1, and send 0 to 0 (and this would be more similar to the behaviour of Nat.pred which also doesn't filter its input).

This came from thinking about Fin.exists_succAbove_eq, which gurantees the existing of a z for x, y non-equal such that y.succAbove z = x. But we don't have an explictly way of getting such a thing even though it is well-defined and calculable.

There are other issues around here: for instance, succAbove and predAbove are highly analogous yet have inconsistent definitions: in particular the former branches on i.1 < p.1yet the latter branches on castSucc p < i (where the roles of p and i are swapped here - the weirdness is the use of the values in the former and the Fin lt in the latter). In general I am unable to discern the design goals here - it seems to come about in part because some functions (like castSucc or pred are defined in std wheras others are extensions in mathlib. It is all a bit annoying to use!

Wrenna Robson (Dec 14 2023 at 10:32):

Regarding the latter - arguably there is a cast for redefining predAbove in these terms. It would make theorems like Fin.succAbove_predAbove more useful!

Wrenna Robson (Dec 14 2023 at 11:37):

You also have issues like e.g. Fin.predAbove_below rewrites predAbove in terms of a funtion which is itself defined in terms of predAbove, wheras Fin.predAbove_above correctly unfolds the definition!

Wrenna Robson (Dec 14 2023 at 12:47):

For an example of what I mean, here's what some alternative definitions could look like.

Whether you use pred' or pred is much of a muchness (it is somewhat useful to match definitions as much as possible, perhaps), but I think a) castPred' would be more consistent than castPred, predAbove' is a much better approach than predAbove.

In general I just think there should be a consistent approach here, where currently there is a lot of friction in my experience.

namespace Fin

def pred' (i : Fin (n + 1)) (h : 0 < i) : Fin n := i.pred h.ne.symm

def castPred' (i : Fin (n + 1)) (hi : i < last n) : Fin n := castLT i hi

def predAbove' (i : Fin (n + 1)) (j : Fin (n + 1)) (hij : j ≠ i) : Fin n :=
  if h : i < j then j.pred (lt_of_le_of_lt (zero_le _) h).ne.symm
  else j.castLT (lt_of_lt_of_le (hij.lt_or_lt.resolve_right h) (le_last i))

lemma predAbove'_below {i : Fin (n + 1)} {j : Fin (n + 1)} (hij : j < i) (hij' : j ≠ i := hij.ne) :
  predAbove' i j hij' = j.castLT (lt_of_lt_of_le hij (le_last _)) := dif_neg (not_lt_of_gt hij)

lemma predAbove'_above {i : Fin (n + 1)} {j : Fin (n + 1)} (hij : i < j)
  (hij' : j ≠ i := hij.ne.symm) :
  predAbove' i j hij' = j.pred (lt_of_le_of_lt (zero_le _) hij).ne.symm := dif_pos hij

lemma succAbove_predAbove' {i : Fin (n + 1)} {j : Fin (n + 1)} (hij : j ≠ i) :
  succAbove i (predAbove' i j hij) = j := by
  rcases hij.lt_or_lt with (h | h)
  · rw [predAbove'_below h, succAbove_castLT h]
  · rw [predAbove'_above h, succAbove_pred h]

lemma predAbove'_succAbove {i : Fin (n + 1)} {k : Fin n}
  (h : succAbove i k ≠ i := succAbove_ne _ _) : predAbove' i (succAbove i k) h = k := by
  rcases (succAbove_ne i k).lt_or_lt with (h | h)
  · rw [predAbove'_below h, castLT_succAbove ((succAbove_lt_iff _ _).mp h)]
  · rw [predAbove'_above h, pred_succAbove (((lt_succAbove_iff _ _).mp h))]

lemma predAbove'_zero_eq_pred : predAbove' (0 : Fin (n + 1)) = pred := by
  ext i h : 2
  exact predAbove'_above (pos_iff_ne_zero.mpr h)

lemma predAbove'_lt_last_eq_predAbove {i : Fin (n + 2)} {j : Fin (n + 2)} {hij : j ≠ i}
  (hi : i < last (n + 1)) : predAbove' i j hij = predAbove (i.castPred) j := by
  rcases hij.lt_or_lt with (h | h)
  · rw [predAbove'_below h, predAbove_below _ _ ((castSucc_castPred hi).symm ▸ h.le), ext_iff,
      coe_castPred _ (h.trans hi), coe_castLT]
  · rw [predAbove'_above h, predAbove_above _ _ ((castSucc_castPred hi).symm ▸ h)]

lemma predAbove'_last_eq_castLT {j : Fin (n + 2)} (hij : j ≠ last (n + 1)) :
  predAbove' (last (n + 1)) j hij = j.castLT (val_lt_last hij) := predAbove'_below (Ne.lt_top hij)

lemma predAbove'_last_eq_castPred {j : Fin (n + 2)} (hij : j ≠ last (n + 1)) :
  predAbove' (Fin.last (n + 1)) j hij = j.castPred := by
  rw [predAbove'_last_eq_castLT hij, ext_iff, coe_castPred _ (val_lt_last hij), coe_castLT]

end Fin

Wrenna Robson (Dec 14 2023 at 12:50):

Compare succAbove_predAbove' and predAbove'_succAbove to succAbove_predAbove and predAbove_succAbove and you will see why I think this is a better definition.

Wrenna Robson (Dec 14 2023 at 14:07):

(It might also be the case that we also want something that does what predAbove currently does. The point is that there are a few things you could do, but no consistent approach.)

Wrenna Robson (Dec 14 2023 at 21:21):

I also think that there's some issues with insertNth. I have some real type resolution issues here: in particular the fact that succ i is not defeq to succAbove 0 icauses some big problems.

Wrenna Robson (Dec 14 2023 at 21:24):

Kinda don't know where to document these bugs/weirdnesses but there's something quite fragile about this part of the library that could do with an expert looking at it. It's related I think to the fact that you can only say that cons = insertNth 0 for homogenous tuples - "inserting in a different order", which on some level is the primary thing I am interested in, can get real twisted round.

Wrenna Robson (Dec 14 2023 at 21:30):

Which at its core I think possibly reflects a deficiency with succAboveCases as an elaborator.

Wrenna Robson (Dec 15 2023 at 10:22):

I think I've come up with an even better definition of predAbove.

theorem exists_unique_succAbove_eq {n : ℕ} {y : Fin (n + 1)}{x : Fin (n + 1)} (h : x ≠ y) :
∃! (z : Fin n), Fin.succAbove y z = x := h.lt_or_lt.by_cases
    (fun hlt => ⟨_, succAbove_castLT hlt,
    fun _ H => (Fin.succAbove_right_injective (x := y)) ((succAbove_castLT hlt).symm ▸ H)⟩)
    (fun hlt => ⟨_, succAbove_pred hlt,
    fun _ H => (Fin.succAbove_right_injective (x := y)) ((succAbove_pred hlt).symm ▸ H)⟩)

def predAbove' {n : ℕ} (y : Fin (n + 1)) (x : Fin (n + 1)) (h : x ≠ y) : Fin n :=
    Fintype.choose _ (Fin.exists_unique_succAbove_eq h)

lemma succAbove_predAbove' {y : Fin (n + 1)} {x : Fin (n + 1)} (hij : x ≠ y) :
  y.succAbove (y.predAbove' x hij) = x := Fintype.choose_spec _ (Fin.exists_unique_succAbove_eq hij)

lemma predAbove'_below {y : Fin (n + 1)} {x : Fin (n + 1)} (hij : x < y) (hij' : x ≠ y := hij.ne) :
  y.predAbove' x hij' = x.castLT (lt_of_lt_of_le hij (le_last _)) := by
  apply Fin.succAbove_right_injective (x := y)
  simp_rw [succAbove_predAbove', succAbove_castLT hij]

lemma predAbove'_above {y : Fin (n + 1)} {x : Fin (n + 1)} (hij : y < x)
  (hij' : x ≠ y := hij.ne.symm) :
  y.predAbove' x hij' = x.pred (lt_of_le_of_lt (zero_le _) hij).ne.symm := by
  apply Fin.succAbove_right_injective (x := y)
  simp_rw [succAbove_predAbove', succAbove_pred hij]

lemma coe_predAbove'_below {y : Fin (n + 1)} {x : Fin (n + 1)} (hij : x < y)
  (hij' : x ≠ y := hij.ne) : (y.predAbove' x hij' : ℕ) = x :=
  by simp_rw [predAbove'_below hij, coe_castLT]

lemma coe_predAbove'_above {y : Fin (n + 1)} {x : Fin (n + 1)} (hij : y < x)
  (hij' : x ≠ y := hij.ne.symm) : (y.predAbove' x hij' : ℕ) = x - 1 :=
  by simp_rw [predAbove'_above hij, coe_pred]

lemma predAbove'_succAbove {i : Fin (n + 1)} {k : Fin n}
  (h : succAbove i k ≠ i := succAbove_ne _ _) : predAbove' i (succAbove i k) h = k := by
  rcases (succAbove_ne i k).lt_or_lt with (h | h)
  · rw [predAbove'_below h, castLT_succAbove ((succAbove_lt_iff _ _).mp h)]
  · rw [predAbove'_above h, pred_succAbove (((lt_succAbove_iff _ _).mp h))]

Wrenna Robson (Dec 15 2023 at 10:24):

This has the advantage of defining it in terms of its characteristic property - it's never correct to unpack the definition but you don't need to.

Wrenna Robson (Dec 15 2023 at 13:39):

@[simp]
lemma insertNth_apply_ne {p : Fin m → α} {i j : Fin (m + 1)} (hij : i ≠ j) :
  insertNth j x p i = p (predAbove! j i hij) := by
  nth_rewrite 1 [← succAbove_predAbove! hij]
  rw [insertNth_apply_succAbove]

lemma insertNth_apply {p : Fin m → α} {i j : Fin (m + 1)} :
  insertNth j x p i = if h : i = j then x else p (predAbove! j i h) := by
  rcases (eq_or_ne i j) with (rfl | h)
  · rw [insertNth_apply_same, dif_pos rfl]
  · rw [insertNth_apply_ne h, dif_neg h]

Further "this would be a real useful change/addition" evidence.

Wrenna Robson (Dec 16 2023 at 00:32):

def predPAbove {n : ℕ} (p : Fin (n + 1)) (i : Fin n) : Fin n :=
(p.succAbove i).predAbove! p (succAbove_ne _ _).symm

lemma predPAbove_def {p : Fin (n + 1)} {i : Fin n} : p.predPAbove i =
(p.succAbove i).predAbove! p (succAbove_ne _ _).symm := rfl

lemma succAbove_of_succAbove_predPAbove {p : Fin (n + 1)} {i : Fin n} :
  (p.succAbove i).succAbove (p.predPAbove i) = p := by
  rw [predPAbove_def, succAbove_predAbove!]

lemma predPAbove_of_succAbove_predPAbove {p : Fin (n + 1)} {i : Fin n} :
  (p.succAbove i).predPAbove (p.predPAbove i) = i := by
  simp_rw [predPAbove_def, succAbove_predAbove!, predAbove!_succAbove]

lemma predPAbove_predAbove! {y : Fin (n + 1)} {x : Fin (n + 1)} (hij : x ≠ y)
  (hij' : y ≠ x := hij.symm) : y.predPAbove (y.predAbove! x hij) = x.predAbove! y hij' := by
  simp_rw [predPAbove_def, succAbove_predAbove! hij]

lemma predPAbove_predPAbove_predPAbove {y : Fin (n + 1)} {x : Fin (n + 1)} (hij : x ≠ y) :
  x.predPAbove (y.predPAbove (y.predAbove! x hij)) = y.predAbove! x hij := by
  simp_rw [predPAbove_predAbove! hij, predPAbove_predAbove! hij.symm]

lemma predPAbove_below {p : Fin (n + 1)} {i : Fin n} (h : p < p.succAbove i) :
p.predPAbove i = castLT p (lt_of_lt_of_le h (le_last _)) := by
  rw [predPAbove_def, predAbove!_below h]

lemma predPAbove_above {p : Fin (n + 1)} {i : Fin n} (h : p.succAbove i < p) :
p.predPAbove i = pred p (lt_of_le_of_lt (zero_le _) h).ne.symm := by
  rw [predPAbove_def, predAbove!_above h]

def succAbove_predPAbove_equiv : Equiv.Perm (Fin (n + 1) × Fin n) where
  toFun := fun ⟨p, i⟩ => (p.succAbove i, p.predPAbove i)
  invFun := fun ⟨p, i⟩ => (p.succAbove i, p.predPAbove i)
  left_inv _ := by simp_rw [predPAbove_of_succAbove_predPAbove, succAbove_of_succAbove_predPAbove]
  right_inv _ := by simp_rw [predPAbove_of_succAbove_predPAbove, succAbove_of_succAbove_predPAbove]

lemma predPAbove_eq {p : Fin (n + 1)} {i : Fin n}:
predPAbove p i = predAbove i p := by
  rw [predAbove]
  split_ifs with H
  · exact predPAbove_above ((succAbove_below _ _ H) ▸ H)
  · exact predPAbove_below ((succAbove_above _ _ (le_of_not_lt H)).symm ▸
    (lt_of_le_of_lt (le_of_not_lt H) (castSucc_lt_succ _)))

Re-implemented our existing "predAbove" in terms of this new utlity - it behaves somewhat better I think.

Wrenna Robson (Dec 16 2023 at 00:32):

I really ought to make a PR out of all this.

Wrenna Robson (Dec 16 2023 at 00:32):

But I'm not sure what would be most useful.

Joël Riou (Dec 16 2023 at 08:31):

I do not have a strong opinion about this, but if you want to try this new design, you may test it with the proof of the simplicial relations, see https://leanprover-community.github.io/mathlib4_docs/Mathlib/AlgebraicTopology/SimplexCategory.html#SimplexCategory.%CE%B4_comp_%CE%B4 and similar lemmas, which make extensive use of succAboveand predAbove.

Wrenna Robson (Dec 16 2023 at 09:08):

Thanks, that's very useful.

Wrenna Robson (Dec 16 2023 at 09:29):

Given the amount of unfolding definitions and case bashing going on here, I definitely think there's room for improvement. It's also useful to see the interpretation of our current predAbove as the degeneracy map - it makes a lot of sense!

Wrenna Robson (Dec 16 2023 at 09:48):

Indeed I somewhat suspect that the relations I had very ugly proofs of are precisely the simplicial relations... which would be why they occurred at all.

Eric Wieser (Dec 16 2023 at 09:52):

Note that using Fintype.choose makes your definition O(n) rather than O(1)

Wrenna Robson (Dec 16 2023 at 09:53):

Yes, I suspect, having played around with it a bunch, that the thing to do is just define it using the ite and then prove the nice properties. But it should absolutely be possible to then avoid having to dig into the definitions each time and casesplit.

Wrenna Robson (Dec 16 2023 at 09:59):

So there are nice interpretations of our existing succAbove and predAbove as the face and degeneracy maps. But I wonder if this map I've defined, predAbove!, has a categorical meaning. It's defined effectively for pairs of distinct elements in [n + 1], and gives you the "equivalent of one in [n] using the other as a pivot". Obviously you can do this both ways round so it's a map [n + 1] \times [n + 1] to [n] \times [n], with the exception that the two initial coordinates must be distinct. I suppose you could extend it. This must be a thing! It's deeply related to the face and degeneracy maps.

Wrenna Robson (Dec 16 2023 at 09:59):

It preserves order as well I think?

Wrenna Robson (Dec 16 2023 at 10:04):

Actually thinking about it as a binary op, the thing you do when they're equal is clearer...

Wrenna Robson (Dec 16 2023 at 10:05):

Except on the edges...

Wrenna Robson (Dec 16 2023 at 11:43):

Yeah. Hmm! Still think the design has merit. In particular it's quite difficult to explicitly extract predAbove! (as I define it) from succAbove and predAbove, but easy to go the other way (predAbove! and predAbove contain the same data, but the use of the ne condition gives it a symmetry that makes it easier to control).