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 Exprs to pairs consisting of a LinearCombo, and proof that the expression is equal to the evaluation of the LinearCombo at the atoms.

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

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

• cfg : Lean.Meta.Omega.OmegaConfig

  User configurable options for omega.

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

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

• atoms : Lean.HashMap Lean.Expr Nat

  The atoms up-to-defeq encountered so far.

@[inline, reducible]

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.MetaM)

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 = Lean.HashMap Lean.Expr (Lean.Omega.LinearCombo × Lean.Elab.Tactic.Omega.OmegaM' Lean.Expr)

@[inline, reducible]

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 LinearCombos (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'

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

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

Equations

• Lean.Elab.Tactic.Omega.OmegaM.run m cfg = StateRefT'.run' (StateRefT'.run' m Lean.HashMap.empty) { atoms := ∅ } { cfg := cfg }

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

Retrieve the user-specified configuration options.

Equations

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

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

Retrieve the list of atoms.

Equations

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

def Lean.Elab.Tactic.Omega.atomsList : Lean.Elab.Tactic.Omega.OmegaM Lean.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 []) (Array.toList __do_lift))

def Lean.Elab.Tactic.Omega.atomsCoeffs : Lean.Elab.Tactic.Omega.OmegaM Lean.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.app (Lean.Expr.const `Lean.Omega.Coeffs.ofList []) __do_lift)

def Lean.Elab.Tactic.Omega.commitWhen {α : Type} (t : Lean.Elab.Tactic.Omega.OmegaM (α × Bool)) : Lean.Elab.Tactic.Omega.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.

def Lean.Elab.Tactic.Omega.withoutModifyingState {α : Type} (t : Lean.Elab.Tactic.Omega.OmegaM α) : Lean.Elab.Tactic.Omega.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)

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

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

Equations

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

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

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

Equations

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

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

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

partial def Lean.Elab.Tactic.Omega.groundNat?.op (f : Nat → Nat → Nat) (x : Lean.Expr) (y : Lean.Expr) : Option Nat

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

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

def Lean.Elab.Tactic.Omega.groundInt?.op (f : Int → Int → Int) (x : Lean.Expr) (y : Lean.Expr) : Option Int

Equations

• Lean.Elab.Tactic.Omega.groundInt?.op f x y = match Lean.Elab.Tactic.Omega.groundNat? x, Lean.Elab.Tactic.Omega.groundNat? y with | some x', some y' => some (f ↑x' ↑y') | x, x_1 => none

def Lean.Elab.Tactic.Omega.mkEqReflWithExpectedType (a : Lean.Expr) (b : Lean.Expr) : Lean.MetaM Lean.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 Lean.Meta.mkExpectedTypeHint __do_lift __do_lift_1

def Lean.Elab.Tactic.Omega.analyzeAtom (e : Lean.Expr) : Lean.Elab.Tactic.Omega.OmegaM (Lean.HashSet Lean.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.

def Lean.Elab.Tactic.Omega.lookup (e : Lean.Expr) : Lean.Elab.Tactic.Omega.OmegaM (Nat × Option (Lean.HashSet Lean.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.