Algebra.Solver.Semiring

Reexports

Definitions

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

  Data type representing expressions in a commutative semiring.
  
  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.Semiring.Sum.normalize`.
  2. The normal forms are compared for being identical.
  3. Since in `Algebra.Solver.Semiring.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.

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.

(+) : Expr a as -> Expr a as -> Expr a as

  Addition of two expressions.

(*) : Expr a as -> Expr a as -> Expr a as

  Multiplication of two expressions.

fromInteger : Num a => Integer -> Expr a as

Totality: total
Visibility: public export

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`.

Totality: total
Visibility: public export
Fixity Declarations:
infixl operator, level 8
infixl operator, level 8

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

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

Totality: total
Visibility: public export
Fixity Declaration: infixl operator, level 8

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

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

Totality: total
Visibility: public export
Fixity Declaration: infixl operator, level 8

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

  Multiplication of variables. This is an alias for
  `var x * var y`.

Totality: total
Visibility: public export
Fixity Declaration: infixl operator, level 9

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

  Multiplication of variables. This is an alias for
  `var x * y`.

Totality: total
Visibility: public export
Fixity Declaration: infixl operator, level 9

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

  Multiplication of variables. This is an alias for
  `x * var y`.

Totality: total
Visibility: public export
Fixity Declaration: infixl operator, level 9

(+) : (0 _ : Rig a z o p m) -> ((v : a) -> Maybe (v = z)) -> a -> a -> a

Totality: total
Visibility: public export
Fixity Declaration: infixl operator, level 8

(*) : (0 _ : Rig a z o p m) -> ((v : a) -> Maybe (v = z)) -> a -> a -> a

Totality: total
Visibility: public export
Fixity Declaration: infixl operator, level 9

eval : (0 _ : Rig a z o p m) -> ((v : a) -> Maybe (v = z)) -> Expr a as -> a

  Evaluation of expressions. This keeps the exact
  structure of the expression tree. For instance
  `eval $ x .*. (y .+. z)` evaluates to `x * (y + z)`.

Totality: total
Visibility: public export

norm : (0 _ : Rig a z o p m) -> ((v : a) -> Maybe (v = z)) -> Expr a as -> Sum a as

  Normalizes an arithmetic expression to a sum of products.

Totality: total
Visibility: public export

normalize : (0 _ : Rig a z o p m) -> ((v : a) -> Maybe (v = z)) -> Expr a as -> Sum a as

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

Totality: total
Visibility: public export

0 solve : (0 r : Rig a z o p m) -> (isZ : ((v : a) -> Maybe (v = z))) -> (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

NatIsZero : (n : Nat) -> Maybe (n = 0)

Totality: total
Visibility: public export

0 solveNat : (as : List Nat) -> (e1 : Expr Nat as) -> (e2 : Expr Nat as) -> normalize e1 = normalize e2 => eval e1 = eval e2

Totality: total
Visibility: export