`positivity`

core extensions #

This file sets up the basic `positivity`

extensions tagged with the `@[positivity]`

attribute.

The `positivity`

extension which identifies expressions of the form `min a b`

,
such that `positivity`

successfully recognises both `a`

and `b`

.

## Equations

- One or more equations did not get rendered due to their size.

Extension for the `max`

operator. The `max`

of two numbers is nonnegative if at least one
is nonnegative, strictly positive if at least one is positive, and nonzero if both are nonzero.

## Equations

- One or more equations did not get rendered due to their size.

The `positivity`

extension which identifies expressions of the form `a + b`

,
such that `positivity`

successfully recognises both `a`

and `b`

.

## Equations

- One or more equations did not get rendered due to their size.

The `positivity`

extension which identifies expressions of the form `a * b`

,
such that `positivity`

successfully recognises both `a`

and `b`

.

## Equations

- One or more equations did not get rendered due to their size.

The `positivity`

extension which identifies expressions of the form `a / b`

,
where `a`

and `b`

are integers.

## Equations

- One or more equations did not get rendered due to their size.

The `positivity`

extension which identifies expressions of the form `a / b`

,
such that `positivity`

successfully recognises both `a`

and `b`

.

## Equations

- One or more equations did not get rendered due to their size.

The `positivity`

extension which identifies expressions of the form `a⁻¹⁻¹`

,
such that `positivity`

successfully recognises `a`

.

## Equations

- One or more equations did not get rendered due to their size.

The `positivity`

extension which identifies expressions of the form `a ^ (0:ℕ)`

.
This extension is run in addition to the general `a ^ b`

extension (they are overlapping).

## Equations

- One or more equations did not get rendered due to their size.

The `positivity`

extension which identifies expressions of the form `a ^ (0:ℤ)`

.

## Equations

- One or more equations did not get rendered due to their size.

The `positivity`

extension which identifies expressions of the form `a ^ (b : ℕ)`

,
such that `positivity`

successfully recognises both `a`

and `b`

.

## Equations

- One or more equations did not get rendered due to their size.

The `positivity`

extension which identifies expressions of the form `|a|`

.

## Equations

- One or more equations did not get rendered due to their size.

Extension for the `positivity`

tactic: `Int.natAbs`

is positive when its input is.
Since the output type of `Int.natAbs`

is `ℕ`

, the nonnegative case is handled by the default
`positivity`

tactic.

## Equations

- One or more equations did not get rendered due to their size.

## Equations

- One or more equations did not get rendered due to their size.

## Equations

- One or more equations did not get rendered due to their size.

Extension for Nat.succ.

## Equations

- One or more equations did not get rendered due to their size.