Translating linear orders to ℤ

In this file we implement the translation of a problem in any linearly ordered type to a problem in ℤ. This allows us to use the omega tactic to solve it.

While the core algorithm of the order tactic is complete for the theory of linear orders in the signature (<, ≤), it becomes incomplete in the signature with lattice operations ⊓ and ⊔. With these operations, the problem becomes NP-hard, and the idea is to reuse a smart and efficient procedure, such as omega.

TODO

Migrate to grind when it is ready.

theorem Mathlib.Tactic.Order.ToInt.exists_translation {α : Type u_1} [LinearOrder α] {n : ℕ} (val : Fin n → α) : ∃ (tr : Fin n → ℤ), ∀ (i j : Fin n), val i ≤ val j ↔ tr i ≤ tr j

The main theorem asserting the existence of a translation. We use Classical.chooose to turn this into a value for use in the order tactic, see toInt.

noncomputable def Mathlib.Tactic.Order.ToInt.toInt {α : Type u_1} [LinearOrder α] {n : ℕ} (val : Fin n → α) (k : Fin n) : ℤ

Auxiliary definition used by the order tactic to transfer facts in a linear order to ℤ.

Equations

• Mathlib.Tactic.Order.ToInt.toInt val k = ⋯.choose k

theorem Mathlib.Tactic.Order.ToInt.toInt_le_toInt {α : Type u_1} [LinearOrder α] {n : ℕ} (val : Fin n → α) (i j : Fin n) : toInt val i ≤ toInt val j ↔ val i ≤ val j

theorem Mathlib.Tactic.Order.ToInt.toInt_lt_toInt {α : Type u_1} [LinearOrder α] {n : ℕ} (val : Fin n → α) (i j : Fin n) : toInt val i < toInt val j ↔ val i < val j

theorem Mathlib.Tactic.Order.ToInt.toInt_eq_toInt {α : Type u_1} [LinearOrder α] {n : ℕ} (val : Fin n → α) (i j : Fin n) : toInt val i = toInt val j ↔ val i = val j

theorem Mathlib.Tactic.Order.ToInt.toInt_ne_toInt {α : Type u_1} [LinearOrder α] {n : ℕ} (val : Fin n → α) (i j : Fin n) : toInt val i ≠ toInt val j ↔ val i ≠ val j

theorem Mathlib.Tactic.Order.ToInt.toInt_nle_toInt {α : Type u_1} [LinearOrder α] {n : ℕ} (val : Fin n → α) (i j : Fin n) : ¬toInt val i ≤ toInt val j ↔ ¬val i ≤ val j

theorem Mathlib.Tactic.Order.ToInt.toInt_nlt_toInt {α : Type u_1} [LinearOrder α] {n : ℕ} (val : Fin n → α) (i j : Fin n) : ¬toInt val i < toInt val j ↔ ¬val i < val j

theorem Mathlib.Tactic.Order.ToInt.toInt_sup_toInt_eq_toInt {α : Type u_1} [LinearOrder α] {n : ℕ} (val : Fin n → α) (i j k : Fin n) : max (toInt val i) (toInt val j) = toInt val k ↔ max (val i) (val j) = val k

theorem Mathlib.Tactic.Order.ToInt.toInt_inf_toInt_eq_toInt {α : Type u_1} [LinearOrder α] {n : ℕ} (val : Fin n → α) (i j k : Fin n) : min (toInt val i) (toInt val j) = toInt val k ↔ min (val i) (val j) = val k

def Mathlib.Tactic.Order.ToInt.mkFinFun {u : Lean.Level} {α : have u := u; Q(Type u)} (atoms : Array Q(«$α»)) : Lean.MetaM Lean.Expr

Given an array atoms : Array α, create an expression representing a function f : Fin atoms.size → α such that f n is defeq to atoms[n] for n : Fin atoms.size.

def Mathlib.Tactic.Order.ToInt.translateToInt {u : Lean.Level} (type : Q(Type u)) (inst : Q(LinearOrder «$type»)) (idxToAtom : Std.HashMap ℕ Q(«$type»)) (facts : Array AtomicFact) : Lean.MetaM (Std.HashMap ℕ Q(ℤ) × Array AtomicFact)

Translates a set of values in a linear ordered type to ℤ, preserving all the facts except for .isTop and .isBot. These facts are filtered at the preprocessing step.