pow : Semiring a => a -> Nat -> a Multiplies a value `n` times with itself. In case of `n`
being zero, this returns `1`.
Totality: total
Visibility: public exportdata 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.
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.
Hint: 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`.
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 Declarations:
infixl operator, level 8
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 Declarations:
infixl operator, level 8
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 Declarations:
infixl operator, level 9
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 Declarations:
infixl operator, level 9
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 Declarations:
infixl operator, level 9
infixl operator, level 9eval : Semiring a => 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 export0 ppow : {auto {conArg:1289} : Semiring a} -> (m : Nat) -> (n : Nat) -> (x : a) -> pow x (m + n) = pow x m * pow x n Proof that addition of exponents is equivalent to multiplcation
of the two terms.
Totality: total
Visibility: export