# The `OmegaM` state monad. #

We keep track of the linear atoms (up to defeq) that have been encountered so far, and also generate new facts as new atoms are recorded.

The main functions are:

- `atoms : OmegaM (List Expr)` which returns the atoms recorded so far
- `lookup (e : Expr) : OmegaM (Nat × Option (HashSet Expr))` which checks if an `Expr` has already been recorded as an atom, and records it. `lookup` return the index in `atoms` for this `Expr`. The `Option (HashSet Expr)` return value is `none` is the expression has been previously recorded, and otherwise contains new facts that should be added to the `omega` problem.
  - for each new atom `a` of the form `((x : Nat) : Int)`, the fact that `0 ≤ a`
  - for each new atom `a` of the form `x / k`, for `k` a positive numeral, the facts that `k * a ≤ x < k * a + k`
  - for each new atom of the form `((a - b : Nat) : Int)`, the fact: `b ≤ a ∧ ((a - b : Nat) : Int) = a - b ∨ a < b ∧ ((a - b : Nat) : Int) = 0`
  - for each new atom of the form `min a b`, the facts `min a b ≤ a` and `min a b ≤ b` (and similarly for `max`)
  - for each new atom of the form `if P then a else b`, the disjunction: `(P ∧ (if P then a else b) = a) ∨ (¬ P ∧ (if P then a else b) = b)` The `OmegaM` monad also keeps an internal cache of visited expressions (not necessarily atoms, but arbitrary subexpressions of one side of a linear relation) to reduce duplication. The cache maps `Expr`s to pairs consisting of a `LinearCombo`, and proof that the expression is equal to the evaluation of the `LinearCombo` at the atoms.

source
structure Lean.Elab.Tactic.Omega.Context :
Type

Context for the `OmegaM` monad, containing the user configurable options.

- cfg : Meta.Omega.OmegaConfig

  User configurable options for `omega`.

Instances For

source
structure Lean.Elab.Tactic.Omega.State :
Type

The internal state for the `OmegaM` monad, recording previously encountered atoms.

- atoms : Std.HashMap Expr Nat

  The atoms up-to-defeq encountered so far.

Instances For

source
@[reducible, inline]
abbrev Lean.Elab.Tactic.Omega.OmegaM' (α : Type) :
Type

An intermediate layer in the `OmegaM` monad.

Equations

- Lean.Elab.Tactic.Omega.OmegaM' = StateRefT' IO.RealWorld Lean.Elab.Tactic.Omega.State (ReaderT Lean.Elab.Tactic.Omega.Context Lean.Meta.CanonM)

Instances For

source
def Lean.Elab.Tactic.Omega.Cache :
Type

Cache of expressions that have been visited, and their reflection as a linear combination.

Equations

- Lean.Elab.Tactic.Omega.Cache = Std.HashMap Lean.Expr (Lean.Omega.LinearCombo × Lean.Elab.Tactic.Omega.OmegaM' Lean.Expr)

Instances For

source
@[reducible, inline]
abbrev Lean.Elab.Tactic.Omega.OmegaM (α : Type) :
Type

The `OmegaM` monad maintains two pieces of state:

- the linear atoms discovered while processing hypotheses
- a cache mapping subexpressions of one side of a linear inequality to `LinearCombo`s (and a proof that the `LinearCombo` evaluates at the atoms to the original expression).

Equations

- Lean.Elab.Tactic.Omega.OmegaM = StateRefT' IO.RealWorld Lean.Elab.Tactic.Omega.Cache Lean.Elab.Tactic.Omega.OmegaM'

Instances For

source
def Lean.Elab.Tactic.Omega.OmegaM.run {α : Type} (m : OmegaM α) (cfg : Meta.Omega.OmegaConfig) :
MetaM α

Run a computation in the `OmegaM` monad, starting with no recorded atoms.

Equations

- m.run cfg = (StateRefT'.run' (StateRefT'.run' m ∅) { } { cfg := cfg }).run'

Instances For

source
def Lean.Elab.Tactic.Omega.cfg :
OmegaM Meta.Omega.OmegaConfig

Retrieve the user-specified configuration options.

Equations

- Lean.Elab.Tactic.Omega.cfg = do let __do_lift ← read pure __do_lift.cfg

Instances For

source
def Lean.Elab.Tactic.Omega.atoms :
OmegaM (Array Expr)

Retrieve the list of atoms.

Equations

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

Instances For

source
def Lean.Elab.Tactic.Omega.atomsList :
OmegaM Expr

Return the `Expr` representing the list of atoms.

Equations

- Lean.Elab.Tactic.Omega.atomsList = do let __do_lift ← Lean.Elab.Tactic.Omega.atoms liftM (Lean.Meta.mkListLit (Lean.Expr.const `Int []) __do_lift.toList)

Instances For

source
def Lean.Elab.Tactic.Omega.atomsCoeffs :
OmegaM Expr

Return the `Expr` representing the list of atoms as a `Coeffs`.

Equations

- Lean.Elab.Tactic.Omega.atomsCoeffs = do let __do_lift ← Lean.Elab.Tactic.Omega.atomsList pure ((Lean.Expr.const `Lean.Omega.Coeffs.ofList []).app __do_lift)

Instances For

source
def Lean.Elab.Tactic.Omega.commitWhen {α : Type} (t : OmegaM (α × Bool)) :
OmegaM α

Run an `OmegaM` computation, restoring the state afterwards depending on the result.

Equations

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

Instances For

source
def Lean.Elab.Tactic.Omega.withoutModifyingState {α : Type} (t : OmegaM α) :
OmegaM α

Run an `OmegaM` computation, restoring the state afterwards.

Equations

- Lean.Elab.Tactic.Omega.withoutModifyingState t = Lean.Elab.Tactic.Omega.commitWhen do let __do_lift ← t pure (__do_lift, false)

Instances For

source
def Lean.Elab.Tactic.Omega.natCast? (n : Expr) :
Option Nat

Wrapper around `Expr.nat?` that also allows `Nat.cast`.

Equations

- Lean.Elab.Tactic.Omega.natCast? n = match n.getAppFnArgs with | (`Nat.cast, #[head, head_1, n]) => n.nat? | x => n.nat?

Instances For

source
def Lean.Elab.Tactic.Omega.intCast? (n : Expr) :
Option Int

Wrapper around `Expr.int?` that also allows `Nat.cast`.

Equations

- Lean.Elab.Tactic.Omega.intCast? n = match n.getAppFnArgs with | (`Nat.cast, #[head, head_1, n]) => do let a ← n.nat? pure ↑a | x => n.int?

Instances For

source
partial def Lean.Elab.Tactic.Omega.groundNat? (e : Expr) :
Option Nat

If `groundNat? e = some n`, then `e` is definitionally equal to `OfNat.ofNat n`.

source
partial def Lean.Elab.Tactic.Omega.groundInt? (e : Expr) :
Option Int

If `groundInt? e = some i`, then `e` is definitionally equal to the standard expression for `i`.

source
def Lean.Elab.Tactic.Omega.mkEqReflWithExpectedType (a b : Expr) :
MetaM Expr

Construct the term with type hint `(Eq.refl a : a = b)`

Equations

- Lean.Elab.Tactic.Omega.mkEqReflWithExpectedType a b = do let __do_lift ← Lean.Meta.mkEqRefl a let __do_lift_1 ← Lean.Meta.mkEq a b pure (Lean.Meta.mkExpectedPropHint __do_lift __do_lift_1)

Instances For

source
def Lean.Elab.Tactic.Omega.analyzeAtom (e : Expr) :
OmegaM (List Expr)

Analyzes a newly recorded atom, returning a collection of interesting facts about it that should be added to the context.

Equations

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

Instances For

source
def Lean.Elab.Tactic.Omega.lookup (e : Expr) :
OmegaM (Nat × Option (List Expr))

Look up an expression in the atoms, recording it if it has not previously appeared.

Return its index, and, if it is new, a collection of interesting facts about the atom.

- for each new atom `a` of the form `((x : Nat) : Int)`, the fact that `0 ≤ a`
- for each new atom `a` of the form `x / k`, for `k` a positive numeral, the facts that `k * a ≤ x < k * a + k`
- for each new atom of the form `((a - b : Nat) : Int)`, the fact: `b ≤ a ∧ ((a - b : Nat) : Int) = a - b ∨ a < b ∧ ((a - b : Nat) : Int) = 0`

Equations

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

Instances For