From c100140c8934165e8bedf9a143d83ba09d4f4229 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Thu, 18 Jun 2026 14:46:03 +0100
Subject: [PATCH 1/3] fix: #2231

---
 CHANGELOG.md                |  4 ++++
 src/Data/Nat/Sqrt/Base.agda | 28 ++++++++++++++++++++++++++++
 2 files changed, 32 insertions(+)
 create mode 100644 src/Data/Nat/Sqrt/Base.agda

diff --git a/CHANGELOG.md b/CHANGELOG.md
index c49aab16cc..617169cb8d 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -141,6 +141,10 @@ New modules
 * `Data.Bool.ListAction.Properties` for properties of conjunction and
   disjunction of lists.
 
+* `Data.Nat.Sqrt.Base` defines the square root of `n` as the greatest
+  natural number whose square is less than or equal to `n`, using a
+  primtive recursive definition originally due to Goodstein (1957).
+
 * A new type of lists that grow on the right.
   This is typically useful to model contexts of typing rules
   or type accumulators that need to be reversed in the base case.
diff --git a/src/Data/Nat/Sqrt/Base.agda b/src/Data/Nat/Sqrt/Base.agda
new file mode 100644
index 0000000000..152208d755
--- /dev/null
+++ b/src/Data/Nat/Sqrt/Base.agda
@@ -0,0 +1,28 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Natural number square root
+--
+-- Goodstein's (1957) primitive recursive definition, taken from
+-- Troelstra and van Dalen, Constructivity in Mathematics, Vol. I
+------------------------------------------------------------------------
+
+{-# OPTIONS --without-K --safe #-}
+
+module Data.Nat.Sqrt.Base where
+
+open import Data.Bool.Base
+open import Data.Nat.Base
+
+sqrt : ℕ → ℕ
+sqrt zero    = zero
+sqrt (suc n) = if (0 <ᵇ d) then √n else suc √n
+  module Sqrt where
+
+  √n = sqrt n
+
+  a*a+b∸c : ℕ → ℕ → ℕ → ℕ
+  a*a+b∸c zero    b c = b ∸ c
+  a*a+b∸c (suc a) b c = a*a+b∸c a (suc (b + (a + a))) c
+
+  d = a*a+b∸c √n (√n + √n) n

From 92610d91ae460834e5a1a46279ffacc518dd5d76 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Thu, 18 Jun 2026 15:35:55 +0100
Subject: [PATCH 2/3] fix: more efficient version?

---
 src/Data/Nat/Sqrt/Base.agda | 22 +++++++++++++++-------
 1 file changed, 15 insertions(+), 7 deletions(-)

diff --git a/src/Data/Nat/Sqrt/Base.agda b/src/Data/Nat/Sqrt/Base.agda
index 152208d755..0c079d8454 100644
--- a/src/Data/Nat/Sqrt/Base.agda
+++ b/src/Data/Nat/Sqrt/Base.agda
@@ -11,18 +11,26 @@
 
 module Data.Nat.Sqrt.Base where
 
-open import Data.Bool.Base
-open import Data.Nat.Base
+open import Data.Bool.Base usinf (if_then_else_)
+open import Data.Nat.Base using (ℕ; zero; suc; 2+; _+_; _∸_; _<ᵇ_)
 
 sqrt : ℕ → ℕ
 sqrt zero    = zero
 sqrt (suc n) = if (0 <ᵇ d) then √n else suc √n
   module Sqrt where
-
+  -- helper functions to compute d
+  2*_ : ℕ → ℕ
+  2* zero  = zero
+  2* suc m = 2+ (2* m)
+  _^2+2*_∸_ : ℕ → ℕ → ℕ → ℕ
+  zero    ^2+2* n ∸ o = (2* n) ∸ o
+  (suc m) ^2+2* n ∸ o = m ^2+2* (suc (m + n)) ∸ (suc o)
+  -- then recur on n
   √n = sqrt n
+  d = √n ^2+2* √n ∸ n
 
-  a*a+b∸c : ℕ → ℕ → ℕ → ℕ
-  a*a+b∸c zero    b c = b ∸ c
-  a*a+b∸c (suc a) b c = a*a+b∸c a (suc (b + (a + a))) c
+private
+  open import Agda.Builtin.Equality using (_≡_; refl)
 
-  d = a*a+b∸c √n (√n + √n) n
+  test : sqrt 16 ≡ 4
+  test = refl

From c0d24cea073119cb73ec8819431001a51315715a Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Thu, 18 Jun 2026 15:45:05 +0100
Subject: [PATCH 3/3] fix: typo

---
 src/Data/Nat/Sqrt/Base.agda | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Data/Nat/Sqrt/Base.agda b/src/Data/Nat/Sqrt/Base.agda
index 0c079d8454..d3475886bc 100644
--- a/src/Data/Nat/Sqrt/Base.agda
+++ b/src/Data/Nat/Sqrt/Base.agda
@@ -11,7 +11,7 @@
 
 module Data.Nat.Sqrt.Base where
 
-open import Data.Bool.Base usinf (if_then_else_)
+open import Data.Bool.Base using (if_then_else_)
 open import Data.Nat.Base using (ℕ; zero; suc; 2+; _+_; _∸_; _<ᵇ_)
 
 sqrt : ℕ → ℕ