Skip to content

Commit

Permalink
oops, remove material that is not ready
Browse files Browse the repository at this point in the history
  • Loading branch information
kim-em committed Jul 28, 2024
1 parent 961f032 commit 8d1b1ce
Showing 1 changed file with 0 additions and 56 deletions.
56 changes: 0 additions & 56 deletions src/Init/Data/List/Lemmas.lean
Original file line number Diff line number Diff line change
Expand Up @@ -5284,60 +5284,4 @@ theorem pairwise_iff_forall_sublist : l.Pairwise R ↔ (∀ {a b}, [a,b] <+ l
intro a b hab
apply h; exact hab.cons _


/-- given a list `is` of monotonically increasing indices into `l`, getting each index
produces a sublist of `l`. -/
theorem map_get_sublist {l : List α} {is : List (Fin l.length)} (h : is.Pairwise (·.val < ·.val)) :
is.map (get l) <+ l := by
suffices ∀ n l', l' = l.drop n → (∀ i ∈ is, n ≤ i) → map (get l) is <+ l'
from this 0 l (by simp) (by simp)
intro n l' hl' his
induction is generalizing n l' with
| nil => simp
| cons hd tl IH =>
simp; cases hl'
have := IH h.of_cons (hd+1) _ rfl (pairwise_cons.mp h).1
specialize his hd (.head _)
have := (drop_eq_getElem_cons ..).symm ▸ this.cons₂ (get l hd)
have := Sublist.append (nil_sublist (take hd l |>.drop n)) this
rwa [nil_append, ← (drop_append_of_le_length ?_), take_append_drop] at this
simp [Nat.min_eq_left (Nat.le_of_lt hd.isLt), his]

/-- given a sublist `l' <+ l`, there exists a list of indices `is` such that
`l' = map (get l) is`. -/
theorem sublist_eq_map_get (h : l' <+ l) : ∃ is : List (Fin l.length),
l' = map (get l) is ∧ is.Pairwise (· < ·) := by
induction h with
| slnil => exact ⟨[], by simp⟩
| cons _ _ IH =>
let ⟨is, IH⟩ := IH
refine ⟨is.map (·.succ), ?_⟩
simp [comp, pairwise_map]
exact IH
| cons₂ _ _ IH =>
rcases IH with ⟨is,IH⟩
refine ⟨⟨0, by simp [Nat.zero_lt_succ]⟩ :: is.map (·.succ), ?_⟩
simp [comp_def, pairwise_map, IH, ← get_eq_getElem]

theorem pairwise_iff_getElem : Pairwise R l ↔
∀ (i j : Nat) (_hi : i < l.length) (_hj : j < l.length) (_hij : i < j), R l[i] l[j] := by
rw [pairwise_iff_forall_sublist]
constructor <;> intro h
· intros i j hi hj h'
apply h
simpa [h'] using map_get_sublist (is := [⟨i, hi⟩, ⟨j, hj⟩])
· intros a b h'
have ⟨is, h', hij⟩ := sublist_eq_map_get h'
rcases is with ⟨⟩ | ⟨a', ⟨⟩ | ⟨b', ⟨⟩⟩⟩ <;> simp at h'
rcases h' with ⟨rfl, rfl⟩
apply h; simpa using hij

theorem pairwise_iff_get : Pairwise R l ↔ ∀ (i j) (_hij : i < j), R (get l i) (get l j) := by
rw [pairwise_iff_getElem]
constructor <;> intro h
· intros i j h'
exact h _ _ _ _ h'
· intros i j hi hj h'
exact h ⟨i, hi⟩ ⟨j, hj⟩ h'

end List

0 comments on commit 8d1b1ce

Please sign in to comment.