Finite sequence (Fin n -> N) prefix proprety

Stream: mathlib4

[Enrico Borba]

I'm trying to show how some properties of finite sequences are preserved in their prefixes. I'm representing it using Fin n -> a because that is what I'm personally used to. I haven't tried using Vector n a, perhaps that would help here. Either way:

-- a prefix of a sequence of length n of length k < n
def Fin.init' (q : (i : Fin n) → α) (h : n' < n) (i : Fin n') : α := q ⟨i.val, i.prop.trans h⟩

-- all numbers in this sequence are either 1 or sums of two previous numbers.
def is_sum (s : Fin n → ℕ) := ∀ k, s k = 1 ∨ ∃ i < k, ∃ j < k, s i + s j = s k

-- if a sequence is `is_sum`, then so is its prefix
theorem init'_is_sum {s : Fin n → ℕ} (hs : is_sum s) (hn : n' < n) : is_sum (Fin.init' s hn) := by
  simp only [is_sum]
  intro k
  refine' Or.elim (hs ⟨k.val, k.prop.trans hn⟩) (fun h => Or.inl h) (fun ⟨i, hi, j, hj⟩ => Or.inr _)
  · sorry

this fact is intuitively correct, but I'm having a pretty annoying time casting between the different Fin n and Fin n' types, especially in the direction of Fin n to Fin n', since n' < n.

Is there a simpler way to go about something like this?

[Eric Wieser]

Using docs#Fin.castLe might be slightly nicer, since there's a small amount of API for it

[Enrico Borba]

Eric Wieser said:

Using docs#Fin.castLe might be slightly nicer, since there's a small amount of API for it

Hmm I wonder why this link 404s. I saw Fin.castLE, but I wasn't sure if it would apply in my strictly less than situation. I need it to be < for later uses of termination_by.

[Enrico Borba]

Wait this might be useful docs#OrderEmbedding.lt_iff_lt

[Enrico Borba]

From a mathematics standpoint I'm surprised this is possible (that order embedding implies lt_iff_lt)

[Matt Diamond]

I wasn't sure if it would apply in my strictly less than situation

"strictly less than" implies "less than or equals", so if you have a hypothesis a_lt_b : a < b you can use a_lt_b.le with castLE

[Enrico Borba]

Matt Diamond said:

I wasn't sure if it would apply in my strictly less than situation

"strictly less than" implies "less than or equals", so if you have a hypothesis a_lt_b : a < b you can use a_lt_b.le with castLE

I meant that it sounds like (based on the OrderEmbedding API): an embedding f : α ↪ β such that a ≤ b ↔ (f a) ≤ (f b) implies that a < b ↔ (f a) < (f b)

[Enrico Borba]

After typing that out it makes sense since ≠ maps to ≠

[Kevin Buzzard]

(deleted)

[Enrico Borba]

docs#Fin.castLT helped:

-- a prefix of a sequence of length n of length k < n
def Fin.init' (q : Fin n → α) (h : n' < n) (i : Fin n') : α := q ⟨i.val, i.prop.trans h⟩

-- all numbers in this sequence are either 1 or sums of two previous numbers.
def is_sum (s : Fin n → ℕ) := ∀ k, s k = 1 ∨ ∃ i < k, ∃ j < k, s i + s j = s k

-- if a sequence is `is_sum`, then so is its prefix
theorem init'_is_sum {s : Fin n → ℕ} (hs : is_sum s) (hn : n' < n) : is_sum (Fin.init' s hn) := by
  simp only [is_sum]
  intro k
  refine' Or.elim (hs ⟨k.val, k.prop.trans hn⟩) (fun h => Or.inl h) (fun ⟨i, hi, j, hj, hij⟩ => Or.inr _)
  · have hi₁ : i.val < n' := (Fin.lt_iff_val_lt_val.mp hi).trans k.prop
    have hi₂ : i.castLT hi₁ < k := Fin.lt_iff_val_lt_val.mp hi
    have hj₁ : j.val < n' := (Fin.lt_iff_val_lt_val.mp hj).trans k.prop
    have hj₂ : j.castLT hj₁ < k := Fin.lt_iff_val_lt_val.mp hj
    exact ⟨i.castLT hi₁, hi₂, j.castLT hj₁, hj₂, hij⟩

[Eric Wieser]

I'm surprised castLT even exists, since it's just a weaker version of castLE