max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: upstream List.get?_append (#3424)

Browse source 
This suffices to get `lean-auto` off Std. (At least, `lake build` works.
Their test suite is [not
automated](https://github.com/leanprover-community/lean-auto/issues/21)?)
This commit is contained in:
Scott Morrison 2024-02-21 10:53:41 +11:00 • committed by GitHub
parent c9aea32d3e
commit 09cfcefb25
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 12 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

12
src/Init/Data/List/Lemmas.lean
View file

@ -6,6 +6,7 @@ Authors: Parikshit Khanna, Jeremy Avigad, Leonardo de Moura, Floris van Doorn, M
prelude
import Init.Data.List.BasicAux
import Init.Data.List.Control
import Init.Data.Nat.Lemmas
import Init.PropLemmas
import Init.Control.Lawful
import Init.Hints
@ -105,6 +106,11 @@ theorem append_left_inj {s₁ s₂ : List α} (t) : s₁ ++ t = s₂ ++ t ↔ s
@[simp] theorem append_eq_nil : p ++ q = [] ↔ p = [] ∧ q = [] := by
cases p <;> simp
theorem get_append : ∀ {l₁ l₂ : List α} (n : Nat) (h : n < l₁.length),
(l₁ ++ l₂).get ⟨n, length_append .. ▸ Nat.lt_add_right _ h⟩ = l₁.get ⟨n, h⟩
| a :: l, _, 0, h => rfl
| a :: l, _, n+1, h => by simp only [get, cons_append]; apply get_append
/-! ### map -/
@[simp] theorem map_nil {f : α → β} : map f [] = [] := rfl
@ -204,6 +210,12 @@ theorem get?_eq_some : l.get? n = some a ↔ ∃ h, get l ⟨n, h⟩ = a :=
| _ :: _, 0 => rfl
| _ :: l, n+1 => get?_map f l n
theorem get?_append {l₁ l₂ : List α} {n : Nat} (hn : n < l₁.length) :
(l₁ ++ l₂).get? n = l₁.get? n := by
have hn' : n < (l₁ ++ l₂).length := Nat.lt_of_lt_of_le hn <|
length_append .. ▸ Nat.le_add_right ..
rw [get?_eq_get hn, get?_eq_get hn', get_append]
@[simp] theorem get?_concat_length : ∀ (l : List α) (a : α), (l ++ [a]).get? l.length = some a
| [], a => rfl
| b :: l, a => by rw [cons_append, length_cons]; simp only [get?, get?_concat_length]