From d2ae678fbfd4cc262b21e1b3a1b9aefa232c7989 Mon Sep 17 00:00:00 2001 From: Markus Schmaus Date: Fri, 21 Jun 2024 13:25:07 +0200 Subject: [PATCH] feat: change `List.length_cons` to use `+ 1` instead of `succ` (#4500) The simp normal form of `succ` is `+ 1`, this changes `List.length_cons` to use that normal form. --- src/Init/Data/List/Basic.lean | 3 +++ src/Init/Prelude.lean | 3 --- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/src/Init/Data/List/Basic.lean b/src/Init/Data/List/Basic.lean index 21e3819c24..3c42e6de98 100644 --- a/src/Init/Data/List/Basic.lean +++ b/src/Init/Data/List/Basic.lean @@ -67,6 +67,9 @@ namespace List @[simp 1100] theorem length_singleton (a : α) : length [a] = 1 := rfl +@[simp] theorem length_cons {α} (a : α) (as : List α) : (cons a as).length = as.length + 1 := + rfl + /-! ### set -/ @[simp] theorem length_set (as : List α) (i : Nat) (a : α) : (as.set i a).length = as.length := by diff --git a/src/Init/Prelude.lean b/src/Init/Prelude.lean index d8dfcadac9..25e8894861 100644 --- a/src/Init/Prelude.lean +++ b/src/Init/Prelude.lean @@ -2329,9 +2329,6 @@ without running out of stack space. def List.lengthTR (as : List α) : Nat := lengthTRAux as 0 -@[simp] theorem List.length_cons {α} (a : α) (as : List α) : Eq (cons a as).length as.length.succ := - rfl - /-- `as.get i` returns the `i`'th element of the list `as`. This version of the function uses `i : Fin as.length` to ensure that it will