0 | module Algebra.Solver.Prod
 1 |
 2 | import public Data.List.Elem
 3 |
 4 | %default total
 5 |
 6 | ||| A product of variables each represented by the exponent,
 7 | ||| to which it is raised.
 8 | |||
 9 | ||| When normalizing arithmetic expressions, they often
10 | ||| get converted to (sums of) products of variables
11 | ||| (listed in index `as`), each raised to a certain
12 | ||| exponent. This is the case for commutative monoids
13 | ||| (a single product) as well as commutative (semi)rings
14 | ||| (a sum of products).
15 | public export
16 | data Prod : (a : Type) -> (as : List a) -> Type where
17 |   Nil  : Prod a []
18 |   (::) : (exp : Nat) -> Prod a xs -> Prod a (x :: xs)
19 |
20 | ||| Multiplying two products means adding all
21 | ||| expontents pairwise.
22 | public export
23 | mult : Prod a as -> Prod a as -> Prod a as
24 | mult []        []        = []
25 | mult (x :: xs) (y :: ys) = (x + y) :: mult xs ys
26 |
27 | ||| We sort products by lexicographically comparing
28 | ||| the exponents.
29 | public export
30 | compProd : Prod a as -> Prod a as -> Ordering
31 | compProd []        []        = EQ
32 | compProd (x :: xs) (y :: ys) = case compare x y of
33 |   LT => LT
34 |   GT => GT
35 |   EQ => compProd xs ys
36 |
37 | ||| The neutral product where all exponents are zero.
38 | public export
39 | one : {as : List a} -> Prod a as
40 | one {as = []}      = []
41 | one {as = x :: xs} = 0 :: one
42 |
43 | ||| Convert a single variable to a product of variables.
44 | public export
45 | fromVar : {as : List a} -> Elem x as -> Prod a as
46 | fromVar {as = x :: xs} Here      = 1 :: one
47 | fromVar {as = x :: xs} (There y) = 0 :: fromVar y
48 | fromVar {as = []} Here impossible
49 | fromVar {as = []} (There y) impossible
50 |
51 | --------------------------------------------------------------------------------
52 | --          Proofs
53 | --------------------------------------------------------------------------------
54 |
55 | Uninhabited (LT = EQ) where
56 |   uninhabited _ impossible
57 |
58 | Uninhabited (GT = EQ) where
59 |   uninhabited _ impossible
60 |
61 | export
62 | 0 pcompNat : (x,y : Nat) -> (compare x y === EQ) -> x === y
63 | pcompNat 0 0         prf = Refl
64 | pcompNat (S k) (S j) prf = cong S $ pcompNat k j prf
65 | pcompNat 0 (S k) Refl impossible
66 | pcompNat (S k) 0 Refl impossible
67 |
68 | export
69 | 0 pcompProd :
70 |      (x,y : Prod a as)
71 |   -> (compProd x y === EQ)
72 |   -> x === y
73 | pcompProd []        []        prf = Refl
74 | pcompProd (x :: xs) (y :: ys) prf with (compare x y) proof eq
75 |   _ | EQ = cong2 (::) (pcompNat x y eq) (pcompProd xs ys prf)
76 |   _ | LT = absurd prf
77 |   _ | GT = absurd prf
78 | pcompProd []        (_ :: _)  Refl impossible
79 | pcompProd (_ :: _)  []        Refl impossible
80 |