Algebra.Solver.Ring

Reexports

Definitions

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

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.

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

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

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

Totality: total
Visibility: public export

(-.) : 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

(.-) : (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

(.*.) : (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 _ : Ring a z o p m sub) -> ((v : a) -> Maybe (v = z)) -> a -> a -> a

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

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

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

negate : Neg ty => ty -> ty

  The underlying of unary minus. `-5` desugars to `negate (fromInteger 5)`.

Totality: total
Visibility: public export
Fixity Declaration: prefix operator, level 10

(-) : (0 _ : Ring a z o p m sub) -> ((v : a) -> Maybe (v = z)) -> a -> a -> a

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

eval : (0 _ : Ring a z o p m sub) -> ((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

negate : (0 _ : Ring a z o p m sub) -> ((v : a) -> Maybe (v = z)) -> Sum a as -> Sum a as

Totality: total
Visibility: public export
Fixity Declaration: prefix operator, level 10

norm : (0 _ : Ring a z o p m sub) -> ((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 _ : Ring a z o p m sub) -> ((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 : Ring a z o p m sub) -> (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