Algebra.Solver.Product

Reexports

Definitions

data Prod : (a : Type) -> List a -> Type

  A product of variables each represented by the exponent,
  to which it is raised.
  
  When normalizing commutative arithmetic expressions, they often
  get converted to (sums of) products of variables
  (listed in index `as`), each raised to a certain
  exponent. This is the case for commutative monoids
  (a single product) as well as commutative (semi)rings
  (a sum of products).
  
  Example: Assume the monoid in question is `(Bits8,(+),0)` (addition
           of 8-bit numbers). Assume further, that we have variables
           `[x,y,z]`. The expression `(x + x) + y + (z + z + z + z)` would
           then be represented as `[2,1,4]`

Totality: total
Visibility: public export
Constructors:

Nil : Prod a []

(::) : Nat -> Prod a xs -> Prod a (x :: xs)

mult : Prod a as -> Prod a as -> Prod a as

  Multiplying two products means adding all
  expontents pairwise.

Totality: total
Visibility: public export

compProd : Prod a as -> Prod a as -> Ordering

  We sort products by lexicographically comparing
  the exponents.

Totality: total
Visibility: public export

one : Prod a as

  The neutral product where all exponents are zero.

Totality: total
Visibility: public export

fromVar : Elem x as -> Prod a as

  Convert a single variable to a product of variables.

Totality: total
Visibility: public export

record Term : (a : Type) -> List a -> Type

  A single term in a normalized arithmetic expressions.
  
  This is a product of all variables each raised to
  a given power, multiplied with a constant factor (which is supposed
  to reduce during elaboration).
  
  Example: Assume the monoid in question is `(Bits8,(+),0)` (addition
           of 8-bit numbers). Assume further, that we have variables
           `[x,y,z]`. The expression `3 + (x + x) + y + (z + z + z + z)` would
           then be represented as `T 3 [2,1,4]`

Totality: total
Visibility: public export
Constructor: 

T : a -> Prod a as -> Term a as

Projections:

.factor : Term a as -> a

.prod : Term a as -> Prod a as

.factor : Term a as -> a

Totality: total
Visibility: public export

factor : Term a as -> a

Totality: total
Visibility: public export

.prod : Term a as -> Prod a as

Totality: total
Visibility: public export

prod : Term a as -> Prod a as

Totality: total
Visibility: public export

negTerm : (a -> a) -> Term a as -> Term a as

  Negates the constant factor in a term using the given negation function.

Totality: total
Visibility: public export

mult : (a -> a -> a) -> Term a as -> Term a as -> Term a as

  Multiplies two terms using the given function to multiply the
  constant factors.

Totality: total
Visibility: public export

times : (a -> a -> a) -> a -> Nat -> a -> a

Totality: total
Visibility: public export

eprod : (a -> a -> a) -> a -> Prod a as -> a

Totality: total
Visibility: public export

eterm : (a -> a -> a) -> a -> Term a as -> a

  Evaluate a term using the given monoid.

Totality: total
Visibility: public export

0 lemma1324 : CommutativeSemigroup a p -> (k `p` l) `p` (m `p` n) = (k `p` m) `p` (l `p` n)

  A utility proof that is used several times internally

Totality: total
Visibility: export

0 lemma213 : CommutativeSemigroup a p -> k `p` (m `p` n) = m `p` (k `p` n)

  A utility proof that is used several times internally

Totality: total
Visibility: export

0 ptimes : CommutativeMonoid a z p -> (m : Nat) -> (n : Nat) -> (x : a) -> times p z m x `p` times p z n x = times p z (m + n) x

Totality: total
Visibility: export

0 peprod : CommutativeMonoid a z p -> (e1 : Prod a as) -> (e2 : Prod a as) -> eprod p z e1 `p` eprod p z e2 = eprod p z (mult e1 e2)

Totality: total
Visibility: export

0 pappend : CommutativeMonoid a z p -> (e1 : Term a as) -> (e2 : Term a as) -> eterm p z e1 `p` eterm p z e2 = eterm p z (mult p e1 e2)

Totality: total
Visibility: export

0 pone : CommutativeMonoid a z p -> (as : List a) -> eprod p z one = z

  Proof that `Prod.one` evaluates to `neutral`

Totality: total
Visibility: export

0 pvar : CommutativeMonoid a z p -> (as : List a) -> (e : Elem x as) -> eprod p z (fromVar e) = x

  Proof that for `e : Elem x as`, `fromVar e` evaluates to `x`.

Totality: total
Visibility: export

0 pcompNat : (x : Nat) -> (y : Nat) -> compare x y = EQ -> x = y

Totality: total
Visibility: export

0 pcompProd : (x : Prod a as) -> (y : Prod a as) -> compProd x y = EQ -> x = y

Totality: total
Visibility: export

0 pmult : Rig a z o p m -> (x : Prod a as) -> (y : Prod a as) -> eprod m o (mult x y) = eprod m o x `m` eprod m o y

  Proof that evaluation of a multiplication of products
  is the same as multiplying the results of evaluating each
  of them.

Totality: total
Visibility: export