List.nonzeroMinimum, List.minNatAbs, List.maxNatAbs

List.minNatAbs computes the minimum non-zero absolute value of a List Int. This is not generally useful outside of the implementation of the omega tactic, so we keep it in the Lean/Elab/Tactic/Omega directory (although the definitions are in the List namespace).

def Lean.Elab.Tactic.Omega.List.nonzeroMinimum (xs : List Nat) : Nat

The minimum non-zero entry in a list of natural numbers, or zero if all entries are zero.

We completely characterize the function via nonzeroMinimum_eq_zero_iff and nonzeroMinimum_eq_nonzero_iff below.

Equations

• Lean.Elab.Tactic.Omega.List.nonzeroMinimum xs = (List.filter (fun (x : Nat) => decide (x ≠ 0)) xs).min?.getD 0

@[simp]

theorem Lean.Elab.Tactic.Omega.List.nonzeroMinimum_eq_zero_iff {xs : List Nat} : nonzeroMinimum xs = 0 ↔ ∀ (x : Nat), x ∈ xs → x = 0

theorem Lean.Elab.Tactic.Omega.List.nonzeroMinimum_mem {xs : List Nat} (w : nonzeroMinimum xs ≠ 0) : nonzeroMinimum xs ∈ xs

theorem Lean.Elab.Tactic.Omega.List.nonzeroMinimum_pos {a : Nat} {xs : List Nat} (m : a ∈ xs) (h : a ≠ 0) : 0 < nonzeroMinimum xs

theorem Lean.Elab.Tactic.Omega.List.nonzeroMinimum_le {a : Nat} {xs : List Nat} (m : a ∈ xs) (h : a ≠ 0) : nonzeroMinimum xs ≤ a

theorem Lean.Elab.Tactic.Omega.List.nonzeroMinimum_eq_nonzero_iff {xs : List Nat} {y : Nat} (h : y ≠ 0) : nonzeroMinimum xs = y ↔ y ∈ xs ∧ ∀ (x : Nat), x ∈ xs → y ≤ x ∨ x = 0

theorem Lean.Elab.Tactic.Omega.List.nonzeroMinimum_eq_of_nonzero {xs : List Nat} (h : nonzeroMinimum xs ≠ 0) : ∃ (x : Nat), x ∈ xs ∧ nonzeroMinimum xs = x

theorem Lean.Elab.Tactic.Omega.List.nonzeroMinimum_le_iff {xs : List Nat} {y : Nat} : nonzeroMinimum xs ≤ y ↔ nonzeroMinimum xs = 0 ∨ ∃ (x : Nat), x ∈ xs ∧ x ≤ y ∧ x ≠ 0

theorem Lean.Elab.Tactic.Omega.List.nonzeroMinimum_map_le_nonzeroMinimum {α : Type u_1} {β : Type u_2} (f : α → β) (p : α → Nat) (q : β → Nat) (xs : List α) (h : ∀ (a : α), a ∈ xs → (p a = 0 ↔ q (f a) = 0)) (w : ∀ (a : α), a ∈ xs → p a ≠ 0 → q (f a) ≤ p a) : nonzeroMinimum (List.map q (List.map f xs)) ≤ nonzeroMinimum (List.map p xs)

def Lean.Elab.Tactic.Omega.List.minNatAbs (xs : List Int) : Nat

The minimum absolute value of a nonzero entry, or zero if all entries are zero.

We completely characterize the function via minNatAbs_eq_zero_iff and minNatAbs_eq_nonzero_iff below.

Equations

• Lean.Elab.Tactic.Omega.List.minNatAbs xs = Lean.Elab.Tactic.Omega.List.nonzeroMinimum (List.map Int.natAbs xs)

@[simp]

theorem Lean.Elab.Tactic.Omega.List.minNatAbs_eq_zero_iff {xs : List Int} : minNatAbs xs = 0 ↔ ∀ (y : Int), y ∈ xs → y = 0

theorem Lean.Elab.Tactic.Omega.List.minNatAbs_eq_nonzero_iff {z : Nat} (xs : List Int) (w : z ≠ 0) : minNatAbs xs = z ↔ (∃ (y : Int), y ∈ xs ∧ y.natAbs = z) ∧ ∀ (y : Int), y ∈ xs → z ≤ y.natAbs ∨ y = 0

@[simp]

theorem Lean.Elab.Tactic.Omega.List.minNatAbs_nil : minNatAbs [] = 0

def Lean.Elab.Tactic.Omega.List.maxNatAbs (xs : List Int) : Nat

The maximum absolute value in a list of integers.

Equations

• Lean.Elab.Tactic.Omega.List.maxNatAbs xs = (List.map Int.natAbs xs).max?.getD 0