0 | module Algebra.Solver.Ring.SolvableRing
 1 |
 2 | import Algebra.Ring
 3 |
 4 | %default total
 5 |
 6 | ||| When normalizing arithmetic expressions, we must
 7 | ||| make sure that factors that evaluate to zero must
 8 | ||| be removed from the sum of products.
 9 | |||
10 | ||| For instance, the following example only works,
11 | ||| if the term `0 * x * y` gets removed before comparing
12 | ||| the normalized sums:
13 | |||
14 | ||| ```idris example
15 | ||| 0 binom3 : {x,y : Bits8} -> (x + y) * (x - y) === x * x - y * y
16 | ||| binom3 = solve [x,y] ((x .+. y) * (x .-. y)) (x .*. x - y .*. y)
17 | ||| ```
18 | |||
19 | ||| Because we cannot directly use a (primitive) pattern match
20 | ||| without having a concrete type, we need this interface.
21 | ||| (We *could* use `DecEq`, but this is not publicly exported
22 | ||| for the primitives; probably for good reasons since it is
23 | ||| implemented using `believe_me`).
24 | public export
25 | interface Ring a => SolvableRing a where
26 |
27 |   ||| Checks if a value is propositionally equal to zero.
28 |   isZero : (v : a) -> Maybe (v === 0)
29 |
30 | public export
31 | SolvableRing Bits8 where
32 |   isZero 0 = Just Refl
33 |   isZero _ = Nothing
34 |
35 | public export
36 | SolvableRing Bits16 where
37 |   isZero 0 = Just Refl
38 |   isZero _ = Nothing
39 |
40 | public export
41 | SolvableRing Bits32 where
42 |   isZero 0 = Just Refl
43 |   isZero _ = Nothing
44 |
45 | public export
46 | SolvableRing Bits64 where
47 |   isZero 0 = Just Refl
48 |   isZero _ = Nothing
49 |
50 | public export
51 | SolvableRing Int8 where
52 |   isZero 0 = Just Refl
53 |   isZero _ = Nothing
54 |
55 | public export
56 | SolvableRing Int16 where
57 |   isZero 0 = Just Refl
58 |   isZero _ = Nothing
59 |
60 | public export
61 | SolvableRing Int32 where
62 |   isZero 0 = Just Refl
63 |   isZero _ = Nothing
64 |
65 | public export
66 | SolvableRing Int64 where
67 |   isZero 0 = Just Refl
68 |   isZero _ = Nothing
69 |
70 | public export
71 | SolvableRing Int where
72 |   isZero 0 = Just Refl
73 |   isZero _ = Nothing
74 |
75 | public export
76 | SolvableRing Integer where
77 |   isZero 0 = Just Refl
78 |   isZero _ = Nothing
79 |