Algebra.Solver.Semiring.Sum

Definitions

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 factors (which is supposed
  to reduce during elaboration).

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

eterm : Semiring a => Term a as -> a

  Evaluate a term.

Totality: total
Visibility: public export

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

  Normalized arithmetic expression in a commutative
  ring (represented as an (ordered) sum of terms).

Totality: total
Visibility: public export
Constructors:

Nil : Sum a as

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

esum : Semiring a => Sum a as -> a

  Evaluate a sum of terms.

Totality: total
Visibility: public export

add : SolvableSemiring a => Sum a as -> Sum a as -> Sum a as

  Add two sums of terms.
  
  The order of terms will be kept. If two terms have identical
  products of variables, they will be unified by adding their
  factors.

Totality: total
Visibility: public export

normSum : SolvableSemiring a => Sum a as -> Sum a as

  Normalize a sum of terms by removing all terms with a
  `zero` factor.

Totality: total
Visibility: public export

mult1 : SolvableSemiring a => Term a as -> Sum a as -> Sum a as

  Multiplies a single term with a sum of terms.

Totality: total
Visibility: public export

mult : SolvableSemiring a => Sum a as -> Sum a as -> Sum a as

  Multiplies two sums of terms.

Totality: total
Visibility: public export

norm : SolvableSemiring a => Expr a as -> Sum a as

  Normalizes an arithmetic expression to a sum of products.

Totality: total
Visibility: public export

normalize : SolvableSemiring a => Expr a as -> Sum a as

  Like `norm` but removes all `zero` terms.

Totality: total
Visibility: public export

0 solve : {auto {conArg:4370} : SolvableSemiring a} -> (as : List a) -> (e1 : Expr a as) -> (e2 : Expr a as) -> normalize e1 = normalize e2 => eval e1 = eval e2

  Given a list `as` of variables and two arithmetic expressions
  over these variables, if the expressions are converted
  to the same normal form, evaluating them gives the same
  result.
  
  This simple fact allows us to conveniently and quickly
  proof arithmetic equalities required in other parts of
  our code. For instance:
  
  ```idris example
  0 binom1 : {x,y : Bits8}
           -> (x + y) * (x + y) === x * x + 2 * x * y + y * y
  binom1 = solve [x,y]
                 ((x .+. y) * (x .+. y))
                 (x .*. x + 2 *. x *. y + y .*. y)
  ```

Totality: total
Visibility: export