From 942a2c754eaf5914ef955c377168558bd8867f12 Mon Sep 17 00:00:00 2001 From: Nick Drozd Date: Tue, 5 May 2020 23:35:56 -0500 Subject: [PATCH] Add neutral product laws --- libs/contrib/Control/Algebra/Laws.idr | 14 ++++++++++++++ 1 file changed, 14 insertions(+) diff --git a/libs/contrib/Control/Algebra/Laws.idr b/libs/contrib/Control/Algebra/Laws.idr index 799f942c96..54cd23a60b 100644 --- a/libs/contrib/Control/Algebra/Laws.idr +++ b/libs/contrib/Control/Algebra/Laws.idr @@ -143,6 +143,20 @@ cancelRight x y z p = rewrite groupInverseIsInverseL x in monoidNeutralIsNeutralL z +||| ab = 0 -> a = b^-1 +neutralProductInverseR : VerifiedGroup ty => (a, b : ty) -> + a <+> b = A.neutral -> a = inverse b +neutralProductInverseR a b prf = + cancelRight b a (inverse b) $ + trans prf $ sym $ groupInverseIsInverseR b + +||| ab = 0 -> a^-1 = b +neutralProductInverseL : VerifiedGroup ty => (a, b : ty) -> + a <+> b = A.neutral -> inverse a = b +neutralProductInverseL a b prf = + cancelLeft a (inverse a) b $ + trans (groupInverseIsInverseL a) $ sym prf + ||| For any a and b, ax = b and ya = b have solutions. latinSquareProperty : VerifiedGroup t => (a, b : t) -> ((x : t ** a <+> x = b),