Add axiom euclid3 (#171)

For those thinking, "isn't it somewhat arrogant to write a Hedgehog test
for Euclid's third axiom?", rest assured I accidentally mixed up `c` and
`b` and only found out thanks to the test.

bittide/src/Data/Constraint/Nat/Extra.hs

@@ -56,3 +56,8 @@ leMaxRight = unsafeCoerce (Dict :: Dict ())
 -- | if (1 <= a) and (1 <= b) then (1 <= DivRU a b)
 strictlyPositiveDivRu :: forall a b . (1 <= a, 1 <= b) => Dict (1 <= DivRU a b)
 strictlyPositiveDivRu = unsafeCoerce (Dict :: Dict ())
+
+-- | Euclid's third axiom: /If equals be subtracted from equals, the remainders
+-- are equal/.
+euclid3 :: forall a b c . (a + b <= c) => Dict (a <= c - b)
+euclid3 = unsafeCoerce (Dict :: Dict ())

bittide/tests/Tests/Haxioms.hs

@@ -24,13 +24,14 @@ haxiomsGroup = testGroup "Haxioms"
   , testPropertyNamed "leMaxLeft holds" "prop_leMaxLeft" prop_leMaxLeft
   , testPropertyNamed "leMaxRight holds" "prop_leMaxRight" prop_leMaxRight
   , testPropertyNamed "divWithRemainder holds" "prop_divWithRemainder" prop_divWithRemainder
+  , testPropertyNamed "euclid3 holds" "prop_euclid3" prop_euclid3
   ]
 
--- | Given that naturals in this module are used in proofs, we don't bother
--- generating very large ones.
---
+-- | Generate a 'Natural' greater than or equal to /n/. Can generate 'Natural's
+-- up to /n+1000/. This should be enough, given that naturals in this module are
+-- used in proofs.
 genNatural :: Natural -> Gen Natural
-genNatural min_ = Gen.integral (Range.linear min_ 1000)
+genNatural min_ = Gen.integral (Range.linear min_ (1000 + min_))
 
 -- | Like 'CLog', but at term-level. Operates on 'Double's internally, so it will
 -- probably fail on very large naturals. This is irrelevant for this module though,
@@ -152,3 +153,18 @@ prop_divWithRemainder = property $ do
   b <- forAll (genNatural 1)
   c <- forAll (Gen.integral (Range.linear 0 (b - 1)))
   ((a * b) + c) `div` b === a
+
+-- | Test whether the following equation holds:
+--
+--     a <= c - b
+--
+-- Given:
+--
+--     a + b <= c
+--
+prop_euclid3 :: Property
+prop_euclid3 = property $ do
+  a <- forAll (genNatural 0)
+  b <- forAll (genNatural 0)
+  c <- forAll (genNatural (a + b))
+  (a + b <= c) === (a <= c - b)