From 84a0c8fd60e788180db175e44ce9d407defe3dab Mon Sep 17 00:00:00 2001 From: Samuel Giuseppe Schlesinger Date: Sun, 25 Oct 2026 12:45:29 -0400 Subject: [PATCH] feat(Foundations): List.getD_append_cons_length and getD_append_cons_of_ne Shared supplier for #1037 (Merkle signatures), as coordinator-reviewer-codex-20261023 asked under #733 practice 2. The hunk is byte-identical to #1037's. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01Dvi6MU29zU9t8zYfeU51sB --- Complexity/Foundations/Data/List/Lookup.lean | 16 ++++++++++++++++ 1 file changed, 16 insertions(+) diff --git a/Complexity/Foundations/Data/List/Lookup.lean b/Complexity/Foundations/Data/List/Lookup.lean index dcd5dc1b1..dfabf1ac4 100644 --- a/Complexity/Foundations/Data/List/Lookup.lean +++ b/Complexity/Foundations/Data/List/Lookup.lean @@ -23,6 +23,8 @@ import Mathlib.Data.List.OfFn and returns a member at its first index. * `List.getD_set_self`, `List.getD_set_ne`: reading an updated entry or an unchanged entry. * `List.Forall₂.getD`: related lists are related at every in-range defaulted lookup. +* `List.getD_append_cons_length`, `List.getD_append_cons_of_ne`: reading the entry at index + `front.length` of `front ++ x :: back`, and the reads that do not depend on it. * `List.forall_mem_set_of_forall_mem`, `List.getD_le_of_forall_le`: preserve invariants under updates and bound defaulted reads of numeric register files. * `List.getD_map_range`: read a function tabulated over a bounded range. @@ -51,6 +53,20 @@ theorem List.getD_set_ne {α : Type*} {l : List α} {i j : ℕ} {x d : α} (h : (l.set i x).getD j d = l.getD j d := by simp only [List.getD_eq_getElem?_getD, List.getElem?_set_ne h] +/-- The entry at index `front.length` of `front ++ x :: back` is `x`. -/ +theorem List.getD_append_cons_length {α : Type*} (front back : List α) (x d : α) : + (front ++ x :: back).getD front.length d = x := by + simp + +/-- Reads of `front ++ x :: back` away from index `front.length` do not depend on `x`. -/ +theorem List.getD_append_cons_of_ne {α : Type*} (front back : List α) (x y d : α) {i : ℕ} + (h : i ≠ front.length) : (front ++ x :: back).getD i d = (front ++ y :: back).getD i d := by + rcases lt_or_gt_of_ne h with hlt | hgt + · rw [List.getD_append _ _ _ _ hlt, List.getD_append _ _ _ _ hlt] + · rw [List.getD_append_right _ _ _ _ hgt.le, List.getD_append_right _ _ _ _ hgt.le] + obtain ⟨j, hj⟩ : ∃ j, i - front.length = j + 1 := ⟨i - front.length - 1, by omega⟩ + rw [hj, List.getD_cons_succ, List.getD_cons_succ] + /-- A property of all the entries of a list holds of all the entries of an update by a value having it. -/ theorem List.forall_mem_set_of_forall_mem {α : Type*} {p : α → Prop} {l : List α} {i : ℕ} {x : α}