Mathlib.Data.List

List lemmas not yet in Mathlib: indexing into an appended tail, and the surgery facts the graph and SCM developments need.

Append 1 core · 0 supporting For a nonempty list q, the list formed by appending the tail of q to a list p has length |p| + |q| − 1, agrees with p at positions below |p|, and has the entry of q at position j − |p| + 1 at each later position j. ★ get_appendTail

Length and entries of a list appended to the tail of another

For a nonempty list q, the list formed by appending the tail of q to a list p has length |p| + |q| − 1, agrees with p at positions below |p|, and has the entry of q at position j − |p| + 1 at each later position j. This describes the concatenation of two walks or paths that share an endpoint, the shared vertex being listed once.

Main results

  • get_appendTail — the length formula and both indexing rules, in one statement.
lemma get_appendTail reviewed
Causalean.Mathlib.Data.List

For lists pa and q, with pa nonempty and q nonempty, appending the tail has the stated length and indexing laws.

Formal statement
hypotheses
V :
Type*
pa q :
List V
_hpa :
pa ≠ []
hq :
q ≠ []
conclusion
conclusion 1
(pa ++ q.tail).length = pa.length + q.length - 1
conclusion 2
j :
ℕ
hj :
j < pa.length
(pa ++ q.tail).get ⟨j, by rw [List.length_append]; have := List.length_tail (l := q); omega⟩
= pa.get ⟨j, hj⟩
conclusion 3
j :
ℕ
hjL :
pa.length ≤ j
hj :
j < (pa ++ q.tail).length
(pa ++ q.tail).get ⟨j, hj⟩
= q.get ⟨j
- pa.length
+ 1, by rw [List.length_append, List.length_tail] at hj have : 1
≤ q.length := List.length_pos_iff.mpr hq omega⟩
Proof (Lean source)
lemma get_appendTail {V : Type*} (pa q : List V) (_hpa : pa ≠ []) (hq : q ≠ []) : (pa ++ q.tail).length = pa.length + q.length - 1 ∧ (∀ (j : ℕ) (hj : j < pa.length), (pa ++ q.tail).get ⟨j, by rw [List.length_append]; have := List.length_tail (l := q); omega⟩ = pa.get ⟨j, hj⟩) ∧ (∀ (j : ℕ) (hjL : pa.length ≤ j) (hj : j < (pa ++ q.tail).length), (pa ++ q.tail).get ⟨j, hj⟩ = q.get ⟨j - pa.length + 1, by rw [List.length_append, List.length_tail] at hj have : 1 ≤ q.length := List.length_pos_iff.mpr hq omega⟩) := by have htail_len : q.tail.length = q.length - 1 := List.length_tail have hqpos : 1 ≤ q.length := List.length_pos_iff.mpr hq refine ⟨?_, ?_, ?_⟩ · rw [List.length_append, htail_len]; omega · intro j hj simp only [List.get_eq_getElem, List.getElem_append_left (h := hj)] · intro j hjL hj have hjr : j - pa.length < q.tail.length := by rw [List.length_append] at hj; omega have e1 : (pa ++ q.tail).get ⟨j, hj⟩ = q.tail[j - pa.length]'hjr := by simp only [List.get_eq_getElem] rw [List.getElem_append_right (by omega)] rw [e1, List.getElem_tail] simp [List.get_eq_getElem]
Causalean.Mathlib.Data.List.get_appendTail · Causalean/Mathlib/Data/List/Append.lean:28