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 Std.Tactic.Omega.Context : Type

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

• cfg : Std.Tactic.Omega.OmegaConfig

  User configurable options for omega.

structure Std.Tactic.Omega.State : Type

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

• atoms : Array Lean.Expr

  The atoms up-to-defeq encountered so far.

@[inline, reducible]

abbrev Std.Tactic.Omega.OmegaM' (α : Type) : Type

An intermediate layer in the OmegaM monad.

Equations

• Std.Tactic.Omega.OmegaM' = StateRefT' IO.RealWorld Std.Tactic.Omega.State (ReaderT Std.Tactic.Omega.Context Lean.MetaM)

def Std.Tactic.Omega.Cache : Type

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

Equations

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

@[inline, reducible]

abbrev Std.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

• Std.Tactic.Omega.OmegaM = StateRefT' IO.RealWorld Std.Tactic.Omega.Cache Std.Tactic.Omega.OmegaM'

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

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

Equations

• Std.Tactic.Omega.OmegaM.run m cfg = StateRefT'.run' (StateRefT'.run' m Lean.HashMap.empty) { atoms := #[] } { cfg := cfg }

def Std.Tactic.Omega.cfg : Std.Tactic.Omega.OmegaM Std.Tactic.Omega.OmegaConfig

Retrieve the user-specified configuration options.

Equations

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

def Std.Tactic.Omega.atoms : Std.Tactic.Omega.OmegaM (List Lean.Expr)

Retrieve the list of atoms.

Equations

• Std.Tactic.Omega.atoms = do let __do_lift ← getThe Std.Tactic.Omega.State pure (Array.toList __do_lift.atoms)

def Std.Tactic.Omega.atomsList : Std.Tactic.Omega.OmegaM Lean.Expr

Return the Expr representing the list of atoms.

Equations

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

def Std.Tactic.Omega.atomsCoeffs : Std.Tactic.Omega.OmegaM Lean.Expr

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

Equations

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

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

Run an OmegaM computation, restoring the state afterwards.

Equations

• Std.Tactic.Omega.withoutModifyingState t = Std.Tactic.Omega.commitWhen do let __do_lift ← t pure (__do_lift, false)

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

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

Equations

• Std.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 Std.Tactic.Omega.intCast? (n : Lean.Expr) : Option Int

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

Equations

• Std.Tactic.Omega.intCast? n = match Lean.Expr.getAppFnArgs n with | (`Nat.cast, #[head, head_1, n]) => Lean.Internal.coeM (Lean.Expr.nat? n) | x => Lean.Expr.int? n

theorem Std.Tactic.Omega.ite_disjunction {α : Type u} {P : Prop} [Decidable P] {a : α} {b : α} : P ∧ (if P then a else b) = a ∨ ¬P ∧ (if P then a else b) = b

def Std.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

• Std.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 Std.Tactic.Omega.analyzeAtom (e : Lean.Expr) : Std.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 Std.Tactic.Omega.lookup (e : Lean.Expr) : Std.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.