From bc2054661fca30d93915cb4a0012dcaa6757230e Mon Sep 17 00:00:00 2001 From: Vlad Tsyrklevich Date: Thu, 5 Dec 2024 18:13:55 +0100 Subject: [PATCH] Fix broken code example (#138) As noted in #138, Nat.add_succ now leads to infinite recursion with simp. Use Nat.add_assoc instead to close out the goal. --- induction_and_recursion.md | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/induction_and_recursion.md b/induction_and_recursion.md index 29abb83..d5ed636 100644 --- a/induction_and_recursion.md +++ b/induction_and_recursion.md @@ -598,7 +598,7 @@ def listAdd [Add α] : List α → List α → List α You are encouraged to experiment with similar examples in the exercises below. -Local recursive declarations +Local Recursive Declarations --------- You can define local recursive declarations using the `let rec` keyword. @@ -633,7 +633,7 @@ theorem length_replicate (n : Nat) (a : α) : (replicate n a).length = n := by : (replicate.loop a n as).length = n + as.length := by match n with | 0 => simp [replicate.loop] - | n+1 => simp [replicate.loop, aux n, Nat.add_succ, Nat.succ_add] + | n+1 => simp [replicate.loop, aux n, Nat.add_assoc, Nat.succ_add] exact aux n [] ``` @@ -655,7 +655,7 @@ where : (replicate.loop a n as).length = n + as.length := by match n with | 0 => simp [replicate.loop] - | n+1 => simp [replicate.loop, aux n, Nat.add_succ, Nat.succ_add] + | n+1 => simp [replicate.loop, aux n, Nat.add_assoc, Nat.succ_add] ``` Well-Founded Recursion and Induction