feat(data/list): accessing list with fallback (#15138)

Reimplement `list.inth` in terms of the new `list.nthd`. Implementation wise, it is "faster" because it doesn't have to go through `option.iget` on the way anymore.

On the way to computable list-based polynomials

src/computability/primrec.lean

@@ -941,8 +941,17 @@ this.to₂.of_eq $ λ l n, begin
   { apply IH }
 end
 
+theorem list_nthd (d : α) : primrec₂ (list.nthd d) :=
+begin
+  suffices : list.nthd d = λ l n, (list.nth l n).get_or_else d,
+  { rw this,
+    exact option_get_or_else.comp₂ list_nth (const _) },
+  funext,
+  exact list.nthd_eq_get_or_else_nth _ _ _
+end
+
 theorem list_inth [inhabited α] : primrec₂ (@list.inth α _) :=
-option_iget.comp₂ list_nth
+list_nthd _
 
 theorem list_append : primrec₂ ((++) : list α → list α → list α) :=
 (list_foldr fst snd $ to₂ $ comp (@list_cons α _) snd).to₂.of_eq $

src/computability/turing_machine.lean

@@ -238,11 +238,11 @@ theorem list_blank.exists_cons {Γ} [inhabited Γ] (l : list_blank Γ) :
 def list_blank.nth {Γ} [inhabited Γ] (l : list_blank Γ) (n : ℕ) : Γ :=
 l.lift_on (λ l, list.inth l n) begin
   rintro l _ ⟨i, rfl⟩,
-  simp only [list.inth],
-  cases lt_or_le _ _ with h h, {rw list.nth_append h},
-  rw list.nth_len_le h,
-  cases le_or_lt _ _ with h₂ h₂, {rw list.nth_len_le h₂},
-  rw [list.nth_le_nth h₂, list.nth_le_append_right h, list.nth_le_repeat]
+  simp only,
+  cases lt_or_le _ _ with h h, {rw list.inth_append _ _ _ h},
+  rw list.inth_eq_default _ h,
+  cases le_or_lt _ _ with h₂ h₂, {rw list.inth_eq_default _ h₂},
+  rw [list.inth_eq_nth_le _ h₂, list.nth_le_append_right h, list.nth_le_repeat]
 end
 
 @[simp] theorem list_blank.nth_mk {Γ} [inhabited Γ] (l : list Γ) (n : ℕ) :
@@ -270,12 +270,12 @@ begin
   refine quotient.sound' (or.inl ⟨l₂.length - l₁.length, _⟩),
   refine list.ext_le _ (λ i h h₂, eq.symm _),
   { simp only [add_tsub_cancel_of_le h, list.length_append, list.length_repeat] },
-  simp at H,
+  simp only [list_blank.nth_mk] at H,
   cases lt_or_le i l₁.length with h' h',
-  { simpa only [list.nth_le_append _ h',
-      list.nth_le_nth h, list.nth_le_nth h', option.iget] using H i },
-  { simpa only [list.nth_le_append_right h', list.nth_le_repeat,
-      list.nth_le_nth h, list.nth_len_le h', option.iget] using H i },
+  { simp only [list.nth_le_append _ h', list.nth_le_nth h, list.nth_le_nth h',
+               ←list.inth_eq_nth_le _ h, ←list.inth_eq_nth_le _ h', H] },
+  { simp only [list.nth_le_append_right h', list.nth_le_repeat, list.nth_le_nth h,
+               list.nth_len_le h', ←list.inth_eq_default _ h', H, list.inth_eq_nth_le _ h] }
 end
 
 /-- Apply a function to a value stored at the nth position of the list. -/
@@ -353,7 +353,7 @@ end
 @[simp] theorem list_blank.nth_map {Γ Γ'} [inhabited Γ] [inhabited Γ']
   (f : pointed_map Γ Γ') (l : list_blank Γ) (n : ℕ) : (l.map f).nth n = f (l.nth n) :=
 l.induction_on begin
-  intro l, simp only [list.nth_map, list_blank.map_mk, list_blank.nth_mk, list.inth],
+  intro l, simp only [list.nth_map, list_blank.map_mk, list_blank.nth_mk, list.inth_eq_iget_nth],
   cases l.nth n, {exact f.2.symm}, {refl}
 end
 
@@ -2002,7 +2002,7 @@ theorem stk_nth_val {K : Type*} {Γ : K → Type*} {L : list_blank (∀ k, optio
   (hL : list_blank.map (proj k) L = list_blank.mk (list.map some S).reverse) :
   L.nth n k = S.reverse.nth n :=
 begin
-  rw [← proj_map_nth, hL, ← list.map_reverse, list_blank.nth_mk, list.inth, list.nth_map],
+  rw [←proj_map_nth, hL, ←list.map_reverse, list_blank.nth_mk, list.inth_eq_iget_nth, list.nth_map],
   cases S.reverse.nth n; refl
 end
 
@@ -2207,15 +2207,15 @@ begin
     rw [list_blank.nth_map, list_blank.nth_modify_nth, proj, pointed_map.mk_val],
     by_cases h' : k' = k,
     { subst k', split_ifs; simp only [list.reverse_cons,
-        function.update_same, list_blank.nth_mk, list.inth, list.map],
-      { rw [list.nth_le_nth, list.nth_le_append_right];
+        function.update_same, list_blank.nth_mk, list.map],
+      { rw [list.inth_eq_nth_le, list.nth_le_append_right];
         simp only [h, list.nth_le_singleton, list.length_map, list.length_reverse, nat.succ_pos',
           list.length_append, lt_add_iff_pos_right, list.length] },
-      rw [← proj_map_nth, hL, list_blank.nth_mk, list.inth],
+      rw [← proj_map_nth, hL, list_blank.nth_mk],
       cases lt_or_gt_of_ne h with h h,
-      { rw list.nth_append, simpa only [list.length_map, list.length_reverse] using h },
+      { rw list.inth_append, simpa only [list.length_map, list.length_reverse] using h },
       { rw gt_iff_lt at h,
-        rw [list.nth_len_le, list.nth_len_le];
+        rw [list.inth_eq_default, list.inth_eq_default];
         simp only [nat.add_one_le_iff, h, list.length, le_of_lt,
           list.length_reverse, list.length_append, list.length_map] } },
     { split_ifs; rw [function.update_noteq h', ← proj_map_nth, hL],
@@ -2245,12 +2245,12 @@ begin
     rw [list_blank.nth_map, list_blank.nth_modify_nth, proj, pointed_map.mk_val],
     by_cases h' : k' = k,
     { subst k', split_ifs; simp only [
-        function.update_same, list_blank.nth_mk, list.tail, list.inth],
-      { rw [list.nth_len_le], {refl}, rw [h, list.length_reverse, list.length_map] },
-      rw [← proj_map_nth, hL, list_blank.nth_mk, list.inth, e, list.map, list.reverse_cons],
+        function.update_same, list_blank.nth_mk, list.tail],
+      { rw [list.inth_eq_default], {refl}, rw [h, list.length_reverse, list.length_map] },
+      rw [← proj_map_nth, hL, list_blank.nth_mk, e, list.map, list.reverse_cons],
       cases lt_or_gt_of_ne h with h h,
-      { rw list.nth_append, simpa only [list.length_map, list.length_reverse] using h },
-      { rw gt_iff_lt at h, rw [list.nth_len_le, list.nth_len_le];
+      { rw list.inth_append, simpa only [list.length_map, list.length_reverse] using h },
+      { rw gt_iff_lt at h, rw [list.inth_eq_default, list.inth_eq_default];
         simp only [nat.add_one_le_iff, h, list.length, le_of_lt,
           list.length_reverse, list.length_append, list.length_map] } },
     { split_ifs; rw [function.update_noteq h', ← proj_map_nth, hL],
@@ -2353,13 +2353,13 @@ begin
   rw (_ : TM1.init _ = _),
   { refine ⟨list_blank.mk (L.reverse.map $ λ a, update default k (some a)), λ k', _⟩,
     refine list_blank.ext (λ i, _),
-    rw [list_blank.map_mk, list_blank.nth_mk, list.inth, list.map_map, (∘),
+    rw [list_blank.map_mk, list_blank.nth_mk, list.inth_eq_iget_nth, list.map_map, (∘),
        list.nth_map, proj, pointed_map.mk_val],
     by_cases k' = k,
     { subst k', simp only [function.update_same],
-      rw [list_blank.nth_mk, list.inth, ← list.map_reverse, list.nth_map] },
+      rw [list_blank.nth_mk, list.inth_eq_iget_nth, ← list.map_reverse, list.nth_map] },
     { simp only [function.update_noteq h],
-      rw [list_blank.nth_mk, list.inth, list.map, list.reverse_nil, list.nth],
+      rw [list_blank.nth_mk, list.inth_eq_iget_nth, list.map, list.reverse_nil, list.nth],
       cases L.reverse.nth i; refl } },
   { rw [tr_init, TM1.init], dsimp only, congr; cases L.reverse; try {refl},
     simp only [list.map_map, list.tail_cons, list.map], refl }

src/data/list/basic.lean

@@ -3985,4 +3985,105 @@ begin
       apply lt_of_succ_lt_succ hi, } },
 end
 
+/-! ### nthd and inth -/
+
+section nthd
+
+variables (l : list α) (x : α) (xs : list α) (d : α) (n : ℕ)
+
+@[simp] lemma nthd_nil : nthd d [] n = d := rfl
+
+@[simp] lemma nthd_cons_zero : nthd d (x::xs) 0 = x := rfl
+
+@[simp] lemma nthd_cons_succ : nthd d (x::xs) (n + 1) = nthd d xs n := rfl
+
+lemma nthd_eq_nth_le {n : ℕ} (hn : n < l.length) : l.nthd d n = l.nth_le n hn :=
+begin
+  induction l with hd tl IH generalizing n,
+  { exact absurd hn (not_lt_of_ge (nat.zero_le _)) },
+  { cases n,
+    { exact nthd_cons_zero _ _ _ },
+    { exact IH _ } }
+end
+
+lemma nthd_eq_default {n : ℕ} (hn : l.length ≤ n) : l.nthd d n = d :=
+begin
+  induction l with hd tl IH generalizing n,
+  { exact nthd_nil _ _ },
+  { cases n,
+    { refine absurd (nat.zero_lt_succ _) (not_lt_of_ge hn) },
+    { exact IH (nat.le_of_succ_le_succ hn) } }
+end
+
+/-- An empty list can always be decidably checked for the presence of an element.
+Not an instance because it would clash with `decidable_eq α`. -/
+def decidable_nthd_nil_ne {α} (a : α) : decidable_pred
+  (λ (i : ℕ), nthd a ([] : list α) i ≠ a) := λ i, is_false $ λ H, H (nthd_nil _ _)
+
+@[simp] lemma nthd_singleton_default_eq (n : ℕ) : [d].nthd d n = d :=
+by { cases n; simp }
+
+@[simp] lemma nthd_repeat_default_eq (r n : ℕ) : (repeat d r).nthd d n = d :=
+begin
+  induction r with r IH generalizing n,
+  { simp },
+  { cases n;
+    simp [IH] }
+end
+
+lemma nthd_append (l l' : list α) (d : α) (n : ℕ) (h : n < l.length)
+  (h' : n < (l ++ l').length := h.trans_le ((length_append l l').symm ▸ le_self_add)) :
+  (l ++ l').nthd d n = l.nthd d n :=
+by rw [nthd_eq_nth_le _ _ h', nth_le_append h' h, nthd_eq_nth_le]
+
+lemma nthd_append_right (l l' : list α) (d : α) (n : ℕ) (h : l.length ≤ n) :
+  (l ++ l').nthd d n = l'.nthd d (n - l.length) :=
+begin
+  cases lt_or_le _ _ with h' h',
+  { rw [nthd_eq_nth_le _ _ h', nth_le_append_right h h', nthd_eq_nth_le] },
+  { rw [nthd_eq_default _ _ h', nthd_eq_default],
+    rwa [le_tsub_iff_left h, ←length_append] }
+end
+
+lemma nthd_eq_get_or_else_nth (n : ℕ) :
+  l.nthd d n = (l.nth n).get_or_else d :=
+begin
+  cases lt_or_le _ _ with h h,
+  { rw [nthd_eq_nth_le _ _ h, nth_le_nth h, option.get_or_else_some] },
+  { rw [nthd_eq_default _ _ h, nth_eq_none_iff.mpr h, option.get_or_else_none] }
+end
+
+end nthd
+
+section inth
+
+variables [inhabited α] (l : list α) (x : α) (xs : list α) (n : ℕ)
+
+@[simp] lemma inth_nil : inth ([] : list α) n = default := rfl
+
+@[simp] lemma inth_cons_zero : inth (x::xs) 0 = x := rfl
+
+@[simp] lemma inth_cons_succ : inth (x::xs) (n + 1) = inth xs n := rfl
+
+lemma inth_eq_nth_le {n : ℕ} (hn : n < l.length) : l.inth n = l.nth_le n hn := nthd_eq_nth_le _ _ _
+
+lemma inth_eq_default {n : ℕ} (hn : l.length ≤ n) : l.inth n = default := nthd_eq_default _ _ hn
+
+lemma nthd_default_eq_inth : l.nthd default = l.inth := rfl
+
+lemma inth_append (l l' : list α) (n : ℕ) (h : n < l.length)
+  (h' : n < (l ++ l').length := h.trans_le ((length_append l l').symm ▸ le_self_add)) :
+  (l ++ l').inth n = l.inth n :=
+nthd_append _ _ _ _ h h'
+
+lemma inth_append_right (l l' : list α) (n : ℕ) (h : l.length ≤ n) :
+  (l ++ l').inth n = l'.inth (n - l.length) :=
+nthd_append_right _ _ _ _ h
+
+lemma inth_eq_iget_nth (n : ℕ) :
+  l.inth n = (l.nth n).iget :=
+by rw [←nthd_default_eq_inth, nthd_eq_get_or_else_nth, option.get_or_else_default_eq_iget]
+
+end inth
+
 end list

src/data/list/defs.lean

@@ -68,9 +68,16 @@ it returns `none` otherwise -/
 def to_array (l : list α) : array l.length α :=
 {data := λ v, l.nth_le v.1 v.2}
 
+/-- "default" `nth` function: returns `d` instead of `none` in the case
+  that the index is out of bounds. -/
+def nthd (d : α) : Π (l : list α) (n : ℕ), α
+| []      _       := d
+| (x::xs) 0       := x
+| (x::xs) (n + 1) := nthd xs n
+
 /-- "inhabited" `nth` function: returns `default` instead of `none` in the case
   that the index is out of bounds. -/
-@[simp] def inth [h : inhabited α] (l : list α) (n : nat) : α := (nth l n).iget
+def inth [h : inhabited α] (l : list α) (n : nat) : α := nthd default l n
 
 /-- Apply a function to the nth tail of `l`. Returns the input without
   using `f` if the index is larger than the length of the list.

src/data/option/basic.lean

@@ -382,6 +382,9 @@ theorem iget_mem [inhabited α] : ∀ {o : option α}, is_some o → o.iget ∈
 theorem iget_of_mem [inhabited α] {a : α} : ∀ {o : option α}, a ∈ o → o.iget = a
 | _ rfl := rfl
 
+lemma get_or_else_default_eq_iget [inhabited α] (o : option α) : o.get_or_else default = o.iget :=
+by cases o; refl
+
 @[simp] theorem guard_eq_some {p : α → Prop} [decidable_pred p] {a b : α} :
   guard p a = some b ↔ a = b ∧ p a :=
 by by_cases p a; simp [option.guard, h]; intro; contradiction