Algebra.Solver.Ring.Expr

Reexports

import public Data.List.Elem
import public Algebra.Ring

Definitions

pow : Ring a => a -> Nat -> a

  Multiplies a value `n` times with itself. In case of `n`
  being zero, this returns `1`.

Totality: total
Visibility: public export

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

  Data type representing expressions in a commutative ring.
  
  This is used to at compile time compare different forms of
  the same expression and proof that they evaluate to
  the same result.
  
  An example:
  
  ```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)
  ```
  
  @ a  the type used in the arithmetic expression
  @ as list of variables which don't reduce at compile time
  
  In the example above, `x` and `y` are variables, while `2`
  is a literal known at compile time. To make working with
  variables more convenient (the have to be wrapped in data
  constructor `Var`, by using function `var` for instance),
  additional operators for addition, multiplication, and
  subtraction are provided.
  
  In order to proof that two expressions evaluate to the
  same results, the following steps are taken at compile
  time:
  
  1. Both expressions are converted to a normal form via
     `Algebra.Solver.Ring.Sum.normalize`.
  2. The normal forms are compared for being identical.
  3. Since in `Algebra.Solver.Ring.Sum` there is a proof that
     converting an expression to its normal form does not
     affect the result when evaluating it, if the normal
     forms are identical, the two expressions must evaluate
     to the same result.
  
  You can find several examples of making use of this
  in `Data.Prim.Integer.Extra`.

Totality: total
Visibility: public export
Constructors:

Lit : a -> Expr a as

  A literal. This should be a value known at compile time
  so that it reduces during normalization.

Var : (x : a) -> Elem x as -> Expr a as

  A variabl. This is is for values not known at compile
  time. In order to compare and merge variables, we need an
  `Elem x as` proof.

Neg : Expr a as -> Expr a as

  Negates and expression.

Plus : Expr a as -> Expr a as -> Expr a as

  Addition of two expressions.

Mult : Expr a as -> Expr a as -> Expr a as

  Multiplication of two expressions.

Minus : Expr a as -> Expr a as -> Expr a as

  Subtraction of two expressions.

Hints:

Neg a => Neg (Expr a as)
Num a => Num (Expr a as)

var : (x : a) -> Elem x as => Expr a as

  Like `Var` but takes the `Elem x as` as an auto implicit
  argument.

Totality: total
Visibility: public export

(.+.) : (x : a) -> (y : a) -> Elem x as => Elem y as => Expr a as

  Addition of variables. This is an alias for
  `var x + var y`.