From 1760675a1e5d3c3c25e57150eeff5bbe46ebd151 Mon Sep 17 00:00:00 2001
From: Nathan McCarty <nathan@mccarty.io>
Date: Fri, 30 Jun 2023 10:36:01 -0400
Subject: [PATCH] Define plus

---
 src/Naturals.idr | 27 +++++++++++++++++++++++++++
 1 file changed, 27 insertions(+)

diff --git a/src/Naturals.idr b/src/Naturals.idr
index 93e1b4e..5b86564 100644
--- a/src/Naturals.idr
+++ b/src/Naturals.idr
@@ -35,3 +35,30 @@ injection n n Reflexive = Reflexive
 
 succNotZero : (n : Natural) -> Equality (S n) Zero -> Void
 succNotZero _ Reflexive impossible
+
+plus : (n, m : Natural) -> Natural
+plus n Zero = n
+plus n (S x) = S (n `plus` x)
+
+zeroIdentityRight : (n : Natural) -> Equality n (n `plus` Zero)
+zeroIdentityRight n = Reflexive
+
+eqSucc : (n, m : Natural) -> Equality n m -> Equality (S n) (S m)
+eqSucc n n Reflexive = Reflexive
+
+zeroIdentityLeft : (n : Natural) -> Equality n (Zero `plus` n)
+zeroIdentityLeft Zero = Reflexive
+zeroIdentityLeft (S x) =
+  let rec = zeroIdentityLeft x
+  in eqSucc _ _ rec
+
+commutativeHelper : (n, m : Natural) -> Equality (S (n `plus` m)) (S (m `plus` n))
+                 -> Equality (S (n `plus` m)) ((S m) `plus` n)
+
+commutative : (n, m : Natural) -> Equality (n `plus` m) (m `plus` n)
+commutative n Zero = zeroIdentityLeft _
+commutative n (S m) =
+  let rec = eqSucc _ _ $ commutative n m
+  in commutativeHelper _ _ rec
+
+associative : (n, m, o : Natural) -> Equality (n `plus` (m `plus` o)) ((n `plus` m) `plus` o)