From 8a9bf396eaf5134a8adea747505e0c536167d659 Mon Sep 17 00:00:00 2001
From: Justus Matthiesen <mail@justusmatthiesen.com>
Date: Tue, 17 Oct 2023 18:10:51 +0100
Subject: [PATCH] [ new ] semiring instance for `SizeChange`

---
 src/Algebra/SizeChange.idr | 107 +++++++++++++++++++++++++++++++++++++
 1 file changed, 107 insertions(+)

diff --git a/src/Algebra/SizeChange.idr b/src/Algebra/SizeChange.idr
index 89f8c40ab..caba8434f 100644
--- a/src/Algebra/SizeChange.idr
+++ b/src/Algebra/SizeChange.idr
@@ -47,3 +47,110 @@ Ord SizeChange where
   max Same Unknown = Same
   max Same y = y
   max Smaller y = Smaller -- holds definitionally!
+
+export
+Semiring SizeChange where
+  (|*|) = (<+>)
+  timesNeutral = neutral
+  (|+|) = max
+  plusNeutral = Unknown
+
+-- semiring laws
+scPlusNeutralLeft : (a : SizeChange) -> Unknown |+| a = a
+scPlusNeutralLeft a = Refl
+
+scPlusNeutralRight : (a : SizeChange) -> a |+| Unknown = a
+scPlusNeutralRight Smaller = Refl
+scPlusNeutralRight Same = Refl
+scPlusNeutralRight Unknown = Refl
+
+partial
+scPlusCommutative : (a, b : SizeChange) -> a |+| b = b |+| a
+scPlusCommutative Unknown b = sym (scPlusNeutralRight b)
+scPlusCommutative b Unknown = scPlusNeutralRight b
+scPlusCommutative Smaller Smaller = Refl
+scPlusCommutative Same Smaller = Refl
+scPlusCommutative Smaller Same = Refl
+scPlusCommutative Same Same = Refl
+
+scPlusAssoc : (a, b, c : SizeChange) -> (a |+| b) |+| c = a |+| (b |+| c)
+scPlusAssoc Smaller b c = Refl
+scPlusAssoc Same Smaller c = Refl
+scPlusAssoc Same Same Smaller = Refl
+scPlusAssoc Same Same Same = Refl
+scPlusAssoc Same Same Unknown = Refl
+scPlusAssoc Same Unknown c = Refl
+scPlusAssoc Unknown b c = Refl
+
+scMultNeutralLeft : (a : SizeChange) -> Same |*| a = a
+scMultNeutralLeft a = Refl
+
+scMultNeutralRight : (a : SizeChange) -> a |*| Same = a
+scMultNeutralRight Smaller = Refl
+scMultNeutralRight Same = Refl
+scMultNeutralRight Unknown = Refl
+
+scMultZeroLeft : (a : SizeChange) -> Unknown |*| a = Unknown
+scMultZeroLeft a = Refl
+
+scMultZeroRight : (a : SizeChange) -> a |*| Unknown = Unknown
+scMultZeroRight Smaller = Refl
+scMultZeroRight Same = Refl
+scMultZeroRight Unknown = Refl
+
+scMultAssociative : (a, b, c : SizeChange) -> a |*| (b |*| c) = (a |*| b) |*| c
+scMultAssociative Smaller Smaller Smaller = Refl
+scMultAssociative Same b c = Refl
+scMultAssociative a Same c =
+  rewrite scMultNeutralRight a in
+  Refl
+scMultAssociative a b Same =
+  rewrite scMultNeutralRight b in
+  rewrite scMultNeutralRight (a |*| b) in
+  Refl
+scMultAssociative Unknown b c = Refl
+scMultAssociative a Unknown c =
+  rewrite scMultZeroRight a in
+  Refl
+scMultAssociative a b Unknown =
+  rewrite scMultZeroRight b in
+  rewrite scMultZeroRight a in
+  rewrite scMultZeroRight (a |*| b) in
+  Refl
+
+scMultCommutative : (a, b : SizeChange) -> a |*| b = b |*| a
+scMultCommutative Smaller Smaller = Refl
+scMultCommutative b Same =
+  rewrite scMultNeutralRight b in
+  Refl
+scMultCommutative Smaller Unknown = Refl
+scMultCommutative Same b =
+  rewrite scMultNeutralRight b in
+  Refl
+scMultCommutative Unknown b =
+ rewrite scMultZeroRight b in
+ Refl
+
+scPlusIdempotent : (a : SizeChange) -> a |+| a = a
+scPlusIdempotent Smaller = Refl
+scPlusIdempotent Same = Refl
+scPlusIdempotent Unknown = Refl
+
+scMultPlusDist : (a, b, c : SizeChange) -> a |*| (b |+| c) = (a |*| b) |+| (a |*| c)
+scMultPlusDist Unknown b c = Refl
+scMultPlusDist a Unknown c =
+  rewrite scMultZeroRight a in
+  Refl
+scMultPlusDist a b Unknown =
+  rewrite scPlusNeutralRight b in
+  rewrite scMultZeroRight a in
+  rewrite scPlusNeutralRight (a |*| b) in
+  Refl
+scMultPlusDist Same b c = Refl
+scMultPlusDist a Same Same =
+  rewrite scMultNeutralRight a in
+  rewrite scPlusIdempotent a in
+  Refl
+scMultPlusDist Smaller Same Smaller = Refl
+scMultPlusDist Smaller Smaller Same = Refl
+scMultPlusDist Smaller Smaller Smaller = Refl