diff --git a/src/Init.lean b/src/Init.lean index 1b3a11862b..9d0ca6d7ad 100644 --- a/src/Init.lean +++ b/src/Init.lean @@ -32,3 +32,4 @@ import Init.Simproc import Init.SizeOfLemmas import Init.BinderPredicates import Init.Ext +import Init.Omega diff --git a/src/Init/Data/List/Basic.lean b/src/Init/Data/List/Basic.lean index 9a7f0f1e0f..14e75be125 100644 --- a/src/Init/Data/List/Basic.lean +++ b/src/Init/Data/List/Basic.lean @@ -889,6 +889,33 @@ def minimum? [Min α] : List α → Option α | [] => none | a::as => some <| as.foldl min a +/-- Inserts an element into a list without duplication. -/ +@[inline] protected def insert [BEq α] (a : α) (l : List α) : List α := + if l.elem a then l else a :: l + +instance decidableBEx (p : α → Prop) [DecidablePred p] : + ∀ l : List α, Decidable (Exists fun x => x ∈ l ∧ p x) + | [] => isFalse nofun + | x :: xs => + if h₁ : p x then isTrue ⟨x, .head .., h₁⟩ else + match decidableBEx p xs with + | isTrue h₂ => isTrue <| let ⟨y, hm, hp⟩ := h₂; ⟨y, .tail _ hm, hp⟩ + | isFalse h₂ => isFalse fun + | ⟨y, .tail _ h, hp⟩ => h₂ ⟨y, h, hp⟩ + | ⟨_, .head .., hp⟩ => h₁ hp + +instance decidableBAll (p : α → Prop) [DecidablePred p] : + ∀ l : List α, Decidable (∀ x, x ∈ l → p x) + | [] => isTrue nofun + | x :: xs => + if h₁ : p x then + match decidableBAll p xs with + | isTrue h₂ => isTrue fun + | y, .tail _ h => h₂ y h + | _, .head .. => h₁ + | isFalse h₂ => isFalse fun H => h₂ fun y hm => H y (.tail _ hm) + else isFalse fun H => h₁ <| H x (.head ..) + instance [BEq α] [LawfulBEq α] : LawfulBEq (List α) where eq_of_beq {as bs} := by induction as generalizing bs with diff --git a/src/Init/Meta.lean b/src/Init/Meta.lean index f1dea4ef0c..7198d2a950 100644 --- a/src/Init/Meta.lean +++ b/src/Init/Meta.lean @@ -1285,6 +1285,41 @@ structure Config where end Rewrite +namespace Omega + +/-- Configures the behaviour of the `omega` tactic. -/ +structure OmegaConfig where + /-- + Split disjunctions in the context. + + Note that with `splitDisjunctions := false` omega will not be able to solve `x = y` goals + as these are usually handled by introducing `¬ x = y` as a hypothesis, then replacing this with + `x < y ∨ x > y`. + + On the other hand, `omega` does not currently detect disjunctions which, when split, + introduce no new useful information, so the presence of irrelevant disjunctions in the context + can significantly increase run time. + -/ + splitDisjunctions : Bool := true + /-- + Whenever `((a - b : Nat) : Int)` is found, register the disjunction + `b ≤ a ∧ ((a - b : Nat) : Int) = a - b ∨ a < b ∧ ((a - b : Nat) : Int) = 0` + for later splitting. + -/ + splitNatSub : Bool := true + /-- + Whenever `Int.natAbs a` is found, register the disjunction + `0 ≤ a ∧ Int.natAbs a = a ∨ a < 0 ∧ Int.natAbs a = - a` for later splitting. + -/ + splitNatAbs : Bool := true + /-- + Whenever `min a b` or `max a b` is found, rewrite in terms of the definition + `if a ≤ b ...`, for later case splitting. + -/ + splitMinMax : Bool := true + +end Omega + end Meta namespace Parser.Tactic diff --git a/src/Init/Omega.lean b/src/Init/Omega.lean new file mode 100644 index 0000000000..6ecfe947d4 --- /dev/null +++ b/src/Init/Omega.lean @@ -0,0 +1,6 @@ +prelude +import Init.Omega.Int +import Init.Omega.IntList +import Init.Omega.LinearCombo +import Init.Omega.Constraint +import Init.Omega.Logic diff --git a/src/Init/Omega/Coeffs.lean b/src/Init/Omega/Coeffs.lean new file mode 100644 index 0000000000..f880ba2e3a --- /dev/null +++ b/src/Init/Omega/Coeffs.lean @@ -0,0 +1,112 @@ +/- +Copyright (c) 2023 Lean FRO, LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Scott Morrison +-/ +prelude +import Init.Omega.IntList + +/-! +# `Coeffs` as a wrapper for `IntList` + +Currently `omega` uses a dense representation for coefficients. +However, we can swap this out for a sparse representation. + +This file sets up `Coeffs` as a type synonym for `IntList`, +and abbreviations for the functions in the `IntList` namespace which we need to use in the +`omega` algorithm. + +There is an equivalent file setting up `Coeffs` as a type synonym for `AssocList Nat Int`, +currently in a private branch. +Not all the theorems about the algebraic operations on that representation have been proved yet. +When they are ready, we can replace the implementation in `omega` simply by importing +`Std.Tactic.Omega.Coeffs.IntDict` instead of `Std.Tactic.Omega.Coeffs.IntList`. + +For small problems, the sparse representation is actually slightly slower, +so it is not urgent to make this replacement. +-/ + +namespace Lean.Omega + +/-- Type synonym for `IntList := List Int`. -/ +abbrev Coeffs := IntList + +namespace Coeffs + +/-- Identity, turning `Coeffs` into `List Int`. -/ +abbrev toList (xs : Coeffs) : List Int := xs +/-- Identity, turning `List Int` into `Coeffs`. -/ +abbrev ofList (xs : List Int) : Coeffs := xs +/-- Are the coefficients all zero? -/ +abbrev isZero (xs : Coeffs) : Prop := ∀ x, x ∈ xs → x = 0 +/-- Shim for `IntList.set`. -/ +abbrev set (xs : Coeffs) (i : Nat) (y : Int) : Coeffs := IntList.set xs i y +/-- Shim for `IntList.get`. -/ +abbrev get (xs : Coeffs) (i : Nat) : Int := IntList.get xs i +/-- Shim for `IntList.gcd`. -/ +abbrev gcd (xs : Coeffs) : Nat := IntList.gcd xs +/-- Shim for `IntList.smul`. -/ +abbrev smul (xs : Coeffs) (g : Int) : Coeffs := IntList.smul xs g +/-- Shim for `IntList.sdiv`. -/ +abbrev sdiv (xs : Coeffs) (g : Int) : Coeffs := IntList.sdiv xs g +/-- Shim for `IntList.dot`. -/ +abbrev dot (xs ys : Coeffs) : Int := IntList.dot xs ys +/-- Shim for `IntList.add`. -/ +abbrev add (xs ys : Coeffs) : Coeffs := IntList.add xs ys +/-- Shim for `IntList.sub`. -/ +abbrev sub (xs ys : Coeffs) : Coeffs := IntList.sub xs ys +/-- Shim for `IntList.neg`. -/ +abbrev neg (xs : Coeffs) : Coeffs := IntList.neg xs +/-- Shim for `IntList.combo`. -/ +abbrev combo (a : Int) (xs : Coeffs) (b : Int) (ys : Coeffs) : Coeffs := IntList.combo a xs b ys +/-- Shim for `List.length`. -/ +abbrev length (xs : Coeffs) := List.length xs +/-- Shim for `IntList.leading`. -/ +abbrev leading (xs : Coeffs) : Int := IntList.leading xs +/-- Shim for `List.map`. -/ +abbrev map (f : Int → Int) (xs : Coeffs) : Coeffs := List.map f xs +/-- Shim for `.enum.find?`. -/ +abbrev findIdx? (f : Int → Bool) (xs : Coeffs) : Option Nat := + -- List.findIdx? f xs + -- We could avoid `Std.Data.List.Basic` by using the less efficient: + xs.enum.find? (f ·.2) |>.map (·.1) +/-- Shim for `IntList.bmod`. -/ +abbrev bmod (x : Coeffs) (m : Nat) : Coeffs := IntList.bmod x m +/-- Shim for `IntList.bmod_dot_sub_dot_bmod`. -/ +abbrev bmod_dot_sub_dot_bmod (m : Nat) (a b : Coeffs) : Int := + IntList.bmod_dot_sub_dot_bmod m a b +theorem bmod_length (x : Coeffs) (m : Nat) : (bmod x m).length ≤ x.length := + IntList.bmod_length x m +theorem dvd_bmod_dot_sub_dot_bmod (m : Nat) (xs ys : Coeffs) : + (m : Int) ∣ bmod_dot_sub_dot_bmod m xs ys := IntList.dvd_bmod_dot_sub_dot_bmod m xs ys + +theorem get_of_length_le {i : Nat} {xs : Coeffs} (h : length xs ≤ i) : get xs i = 0 := + IntList.get_of_length_le h +theorem dot_set_left (xs ys : Coeffs) (i : Nat) (z : Int) : + dot (set xs i z) ys = dot xs ys + (z - get xs i) * get ys i := + IntList.dot_set_left xs ys i z +theorem dot_sdiv_left (xs ys : Coeffs) {d : Int} (h : d ∣ xs.gcd) : + dot (xs.sdiv d) ys = (dot xs ys) / d := + IntList.dot_sdiv_left xs ys h +theorem dot_smul_left (xs ys : Coeffs) (i : Int) : dot (i * xs) ys = i * dot xs ys := + IntList.dot_smul_left xs ys i +theorem dot_distrib_left (xs ys zs : Coeffs) : (xs + ys).dot zs = xs.dot zs + ys.dot zs := + IntList.dot_distrib_left xs ys zs +theorem sub_eq_add_neg (xs ys : Coeffs) : xs - ys = xs + -ys := + IntList.sub_eq_add_neg xs ys +theorem combo_eq_smul_add_smul (a : Int) (xs : Coeffs) (b : Int) (ys : Coeffs) : + combo a xs b ys = (a * xs) + (b * ys) := + IntList.combo_eq_smul_add_smul a xs b ys +theorem gcd_dvd_dot_left (xs ys : Coeffs) : (gcd xs : Int) ∣ dot xs ys := + IntList.gcd_dvd_dot_left xs ys +theorem map_length {xs : Coeffs} : (xs.map f).length ≤ xs.length := + Nat.le_of_eq (List.length_map xs f) + +theorem dot_nil_right {xs : Coeffs} : dot xs .nil = 0 := IntList.dot_nil_right +theorem get_nil : get .nil i = 0 := IntList.get_nil +theorem dot_neg_left (xs ys : IntList) : dot (-xs) ys = -dot xs ys := + IntList.dot_neg_left xs ys + +end Coeffs + +end Lean.Omega diff --git a/src/Init/Omega/Constraint.lean b/src/Init/Omega/Constraint.lean new file mode 100644 index 0000000000..53359f4286 --- /dev/null +++ b/src/Init/Omega/Constraint.lean @@ -0,0 +1,395 @@ +/- +Copyright (c) 2023 Lean FRO, LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Scott Morrison +-/ +prelude +import Init.Omega.LinearCombo +import Init.Omega.Int + +/-! +A `Constraint` consists of an optional lower and upper bound (inclusive), +constraining a value to a set of the form `∅`, `{x}`, `[x, y]`, `[x, ∞)`, `(-∞, y]`, or `(-∞, ∞)`. +-/ + +namespace Lean.Omega + +/-- An optional lower bound on a integer. -/ +abbrev LowerBound : Type := Option Int +/-- An optional upper bound on a integer. -/ +abbrev UpperBound : Type := Option Int + +/-- A lower bound at `x` is satisfied at `t` if `x ≤ t`. -/ +abbrev LowerBound.sat (b : LowerBound) (t : Int) := b.all fun x => x ≤ t +/-- A upper bound at `y` is satisfied at `t` if `t ≤ y`. -/ +abbrev UpperBound.sat (b : UpperBound) (t : Int) := b.all fun y => t ≤ y + +/-- +A `Constraint` consists of an optional lower and upper bound (inclusive), +constraining a value to a set of the form `∅`, `{x}`, `[x, y]`, `[x, ∞)`, `(-∞, y]`, or `(-∞, ∞)`. +-/ +structure Constraint where + /-- A lower bound. -/ + lowerBound : LowerBound + /-- An upper bound. -/ + upperBound : UpperBound +deriving BEq, DecidableEq, Repr + +namespace Constraint + +instance : ToString Constraint where + toString := fun + | ⟨none, none⟩ => "(-∞, ∞)" + | ⟨none, some y⟩ => s!"(-∞, {y}]" + | ⟨some x, none⟩ => s!"[{x}, ∞)" + | ⟨some x, some y⟩ => + if y < x then "∅" else if x = y then s!"\{{x}}" else s!"[{x}, {y}]" + +/-- A constraint is satisfied at `t` is both the lower bound and upper bound are satisfied. -/ +def sat (c : Constraint) (t : Int) : Bool := c.lowerBound.sat t ∧ c.upperBound.sat t + +/-- Apply a function to both the lower bound and upper bound. -/ +def map (c : Constraint) (f : Int → Int) : Constraint where + lowerBound := c.lowerBound.map f + upperBound := c.upperBound.map f + +/-- Translate a constraint. -/ +def translate (c : Constraint) (t : Int) : Constraint := c.map (· + t) + +theorem translate_sat : {c : Constraint} → {v : Int} → sat c v → sat (c.translate t) (v + t) := by + rintro ⟨_ | l, _ | u⟩ v w <;> simp_all [sat, translate, map] + · exact Int.add_le_add_right w t + · exact Int.add_le_add_right w t + · rcases w with ⟨w₁, w₂⟩; constructor + · exact Int.add_le_add_right w₁ t + · exact Int.add_le_add_right w₂ t + +/-- +Flip a constraint. +This operation is not useful by itself, but is used to implement `neg` and `scale`. +-/ +def flip (c : Constraint) : Constraint where + lowerBound := c.upperBound + upperBound := c.lowerBound + +/-- +Negate a constraint. `[x, y]` becomes `[-y, -x]`. +-/ +def neg (c : Constraint) : Constraint := c.flip.map (- ·) + +theorem neg_sat : {c : Constraint} → {v : Int} → sat c v → sat (c.neg) (-v) := by + rintro ⟨_ | l, _ | u⟩ v w <;> simp_all [sat, neg, flip, map] + · exact Int.neg_le_neg w + · exact Int.neg_le_neg w + · rcases w with ⟨w₁, w₂⟩; constructor + · exact Int.neg_le_neg w₂ + · exact Int.neg_le_neg w₁ + +/-- The trivial constraint, satisfied everywhere. -/ +def trivial : Constraint := ⟨none, none⟩ +/-- The impossible constraint, unsatisfiable. -/ +def impossible : Constraint := ⟨some 1, some 0⟩ +/-- An exact constraint. -/ +def exact (r : Int) : Constraint := ⟨some r, some r⟩ + +@[simp] theorem trivial_say : trivial.sat t := by + simp [sat, trivial] + +@[simp] theorem exact_sat (r : Int) (t : Int) : (exact r).sat t = decide (r = t) := by + simp only [sat, exact, Option.all_some, decide_eq_true_eq, decide_eq_decide] + exact Int.eq_iff_le_and_ge.symm + +/-- Check if a constraint is unsatisfiable. -/ +def isImpossible : Constraint → Bool + | ⟨some x, some y⟩ => y < x + | _ => false + +/-- Check if a constraint requires an exact value. -/ +def isExact : Constraint → Bool + | ⟨some x, some y⟩ => x = y + | _ => false + +theorem not_sat_of_isImpossible (h : isImpossible c) {t} : ¬ c.sat t := by + rcases c with ⟨_ | l, _ | u⟩ <;> simp [isImpossible, sat] at h ⊢ + intro w + rw [Int.not_le] + exact Int.lt_of_lt_of_le h w + +/-- +Scale a constraint by multiplying by an integer. +* If `k = 0` this is either impossible, if the original constraint was impossible, + or the `= 0` exact constraint. +* If `k` is positive this takes `[x, y]` to `[k * x, k * y]` +* If `k` is negative this takes `[x, y]` to `[k * y, k * x]`. +-/ +def scale (k : Int) (c : Constraint) : Constraint := + if k = 0 then + if c.isImpossible then c else ⟨some 0, some 0⟩ + else if 0 < k then + c.map (k * ·) + else + c.flip.map (k * ·) + +theorem scale_sat {c : Constraint} (k) (w : c.sat t) : (scale k c).sat (k * t) := by + simp [scale] + split + · split + · simp_all [not_sat_of_isImpossible] + · simp_all [sat] + · rcases c with ⟨_ | l, _ | u⟩ <;> split <;> rename_i h <;> simp_all [sat, flip, map] + · replace h := Int.le_of_lt h + exact Int.mul_le_mul_of_nonneg_left w h + · rw [Int.not_lt] at h + exact Int.mul_le_mul_of_nonpos_left h w + · replace h := Int.le_of_lt h + exact Int.mul_le_mul_of_nonneg_left w h + · rw [Int.not_lt] at h + exact Int.mul_le_mul_of_nonpos_left h w + · constructor + · exact Int.mul_le_mul_of_nonneg_left w.1 (Int.le_of_lt h) + · exact Int.mul_le_mul_of_nonneg_left w.2 (Int.le_of_lt h) + · replace h := Int.not_lt.mp h + constructor + · exact Int.mul_le_mul_of_nonpos_left h w.2 + · exact Int.mul_le_mul_of_nonpos_left h w.1 + +/-- The sum of two constraints. `[a, b] + [c, d] = [a + c, b + d]`. -/ +def add (x y : Constraint) : Constraint where + lowerBound := x.lowerBound.bind fun a => y.lowerBound.map fun b => a + b + upperBound := x.upperBound.bind fun a => y.upperBound.map fun b => a + b + +theorem add_sat (w₁ : c₁.sat x₁) (w₂ : c₂.sat x₂) : (add c₁ c₂).sat (x₁ + x₂) := by + rcases c₁ with ⟨_ | l₁, _ | u₁⟩ <;> rcases c₂ with ⟨_ | l₂, _ | u₂⟩ + <;> simp [sat, LowerBound.sat, UpperBound.sat, add] at * + · exact Int.add_le_add w₁ w₂ + · exact Int.add_le_add w₁ w₂.2 + · exact Int.add_le_add w₁ w₂ + · exact Int.add_le_add w₁ w₂.1 + · exact Int.add_le_add w₁.2 w₂ + · exact Int.add_le_add w₁.1 w₂ + · constructor + · exact Int.add_le_add w₁.1 w₂.1 + · exact Int.add_le_add w₁.2 w₂.2 + +/-- A linear combination of two constraints. -/ +def combo (a : Int) (x : Constraint) (b : Int) (y : Constraint) : Constraint := + add (scale a x) (scale b y) + +theorem combo_sat (a) (w₁ : c₁.sat x₁) (b) (w₂ : c₂.sat x₂) : + (combo a c₁ b c₂).sat (a * x₁ + b * x₂) := + add_sat (scale_sat a w₁) (scale_sat b w₂) + +/-- The conjunction of two constraints. -/ +def combine (x y : Constraint) : Constraint where + lowerBound := max x.lowerBound y.lowerBound + upperBound := min x.upperBound y.upperBound + +theorem combine_sat : (c : Constraint) → (c' : Constraint) → (t : Int) → + (c.combine c').sat t = (c.sat t ∧ c'.sat t) := by + rintro ⟨_ | l₁, _ | u₁⟩ <;> rintro ⟨_ | l₂, _ | u₂⟩ t + <;> simp [sat, LowerBound.sat, UpperBound.sat, combine, Int.le_min, Int.max_le] at * + · rw [And.comm] + · rw [← and_assoc, And.comm (a := l₂ ≤ t), and_assoc] + · rw [and_assoc] + · rw [and_assoc] + · rw [and_assoc, and_assoc, And.comm (a := l₂ ≤ t)] + · rw [and_assoc, ← and_assoc (a := l₂ ≤ t), And.comm (a := l₂ ≤ t), and_assoc, and_assoc] + +/-- +Dividing a constraint by a natural number, and tightened to integer bounds. +Thus the lower bound is rounded up, and the upper bound is rounded down. +-/ +def div (c : Constraint) (k : Nat) : Constraint where + lowerBound := c.lowerBound.map fun x => (- ((- x) / k)) + upperBound := c.upperBound.map fun y => y / k + +theorem div_sat (c : Constraint) (t : Int) (k : Nat) (n : k ≠ 0) (h : (k : Int) ∣ t) (w : c.sat t) : + (c.div k).sat (t / k) := by + replace n : (k : Int) > 0 := Int.ofNat_lt.mpr (Nat.pos_of_ne_zero n) + rcases c with ⟨_ | l, _ | u⟩ + · simp_all [sat, div] + · simp [sat, div] at w ⊢ + apply Int.le_of_sub_nonneg + rw [← Int.sub_ediv_of_dvd _ h, ← ge_iff_le, Int.div_nonneg_iff_of_pos n] + exact Int.sub_nonneg_of_le w + · simp [sat, div] at w ⊢ + apply Int.le_of_sub_nonneg + rw [Int.sub_neg, ← Int.add_ediv_of_dvd_left h, ← ge_iff_le, + Int.div_nonneg_iff_of_pos n] + exact Int.sub_nonneg_of_le w + · simp [sat, div] at w ⊢ + constructor + · apply Int.le_of_sub_nonneg + rw [Int.sub_neg, ← Int.add_ediv_of_dvd_left h, ← ge_iff_le, + Int.div_nonneg_iff_of_pos n] + exact Int.sub_nonneg_of_le w.1 + · apply Int.le_of_sub_nonneg + rw [← Int.sub_ediv_of_dvd _ h, ← ge_iff_le, Int.div_nonneg_iff_of_pos n] + exact Int.sub_nonneg_of_le w.2 + +/-- +It is convenient below to say that a constraint is satisfied at the dot product of two vectors, +so we make an abbreviation `sat'` for this. +-/ +abbrev sat' (c : Constraint) (x y : Coeffs) := c.sat (Coeffs.dot x y) + +theorem combine_sat' {s t : Constraint} {x y} (ws : s.sat' x y) (wt : t.sat' x y) : + (s.combine t).sat' x y := (combine_sat _ _ _).mpr ⟨ws, wt⟩ + +theorem div_sat' {c : Constraint} {x y} (h : Coeffs.gcd x ≠ 0) (w : c.sat (Coeffs.dot x y)) : + (c.div (Coeffs.gcd x)).sat' (Coeffs.sdiv x (Coeffs.gcd x)) y := by + dsimp [sat'] + rw [Coeffs.dot_sdiv_left _ _ (Int.dvd_refl _)] + exact div_sat c _ (Coeffs.gcd x) h (Coeffs.gcd_dvd_dot_left x y) w + +theorem not_sat'_of_isImpossible (h : isImpossible c) {x y} : ¬ c.sat' x y := + not_sat_of_isImpossible h + +theorem addInequality_sat (w : c + Coeffs.dot x y ≥ 0) : + Constraint.sat' { lowerBound := some (-c), upperBound := none } x y := by + simp [Constraint.sat', Constraint.sat] + rw [← Int.zero_sub c] + exact Int.sub_left_le_of_le_add w + +theorem addEquality_sat (w : c + Coeffs.dot x y = 0) : + Constraint.sat' { lowerBound := some (-c), upperBound := some (-c) } x y := by + simp [Constraint.sat', Constraint.sat] + rw [Int.eq_iff_le_and_ge] at w + rwa [Int.add_le_zero_iff_le_neg', Int.add_nonnneg_iff_neg_le', and_comm] at w + +end Constraint + +/-- +Normalize a constraint, by dividing through by the GCD. + +Return `none` if there is nothing to do, to avoid adding unnecessary steps to the proof term. +-/ +def normalize? : Constraint × Coeffs → Option (Constraint × Coeffs) + | ⟨s, x⟩ => + let gcd := Coeffs.gcd x -- TODO should we be caching this? + if gcd = 0 then + if s.sat 0 then + some (.trivial, x) + else + some (.impossible, x) + else if gcd = 1 then + none + else + some (s.div gcd, Coeffs.sdiv x gcd) + +/-- Normalize a constraint, by dividing through by the GCD. -/ +def normalize (p : Constraint × Coeffs) : Constraint × Coeffs := + normalize? p |>.getD p + +/-- Shorthand for the first component of `normalize`. -/ +-- This `noncomputable` (and others below) is a safeguard that we only use this in proofs. +noncomputable abbrev normalizeConstraint (s : Constraint) (x : Coeffs) : Constraint := + (normalize (s, x)).1 +/-- Shorthand for the second component of `normalize`. -/ +noncomputable abbrev normalizeCoeffs (s : Constraint) (x : Coeffs) : Coeffs := + (normalize (s, x)).2 + +theorem normalize?_eq_some (w : normalize? (s, x) = some (s', x')) : + normalizeConstraint s x = s' ∧ normalizeCoeffs s x = x' := by + simp_all [normalizeConstraint, normalizeCoeffs, normalize] + +theorem normalize_sat {s x v} (w : s.sat' x v) : + (normalizeConstraint s x).sat' (normalizeCoeffs s x) v := by + dsimp [normalizeConstraint, normalizeCoeffs, normalize, normalize?] + split <;> rename_i h + · split + · simp + · dsimp [Constraint.sat'] at w + simp_all + · split + · exact w + · exact Constraint.div_sat' h w + +/-- Multiply by `-1` if the leading coefficient is negative, otherwise return `none`. -/ +def positivize? : Constraint × Coeffs → Option (Constraint × Coeffs) + | ⟨s, x⟩ => + if 0 ≤ x.leading then + none + else + (s.neg, Coeffs.smul x (-1)) + +/-- Multiply by `-1` if the leading coefficient is negative, otherwise do nothing. -/ +noncomputable def positivize (p : Constraint × Coeffs) : Constraint × Coeffs := + positivize? p |>.getD p + +/-- Shorthand for the first component of `positivize`. -/ +noncomputable abbrev positivizeConstraint (s : Constraint) (x : Coeffs) : Constraint := + (positivize (s, x)).1 +/-- Shorthand for the second component of `positivize`. -/ +noncomputable abbrev positivizeCoeffs (s : Constraint) (x : Coeffs) : Coeffs := + (positivize (s, x)).2 + +theorem positivize?_eq_some (w : positivize? (s, x) = some (s', x')) : + positivizeConstraint s x = s' ∧ positivizeCoeffs s x = x' := by + simp_all [positivizeConstraint, positivizeCoeffs, positivize] + +theorem positivize_sat {s x v} (w : s.sat' x v) : + (positivizeConstraint s x).sat' (positivizeCoeffs s x) v := by + dsimp [positivizeConstraint, positivizeCoeffs, positivize, positivize?] + split + · exact w + · simp [Constraint.sat'] + erw [Coeffs.dot_smul_left, ← Int.neg_eq_neg_one_mul] + exact Constraint.neg_sat w + +/-- `positivize` and `normalize`, returning `none` if neither does anything. -/ +def tidy? : Constraint × Coeffs → Option (Constraint × Coeffs) + | ⟨s, x⟩ => + match positivize? (s, x) with + | none => match normalize? (s, x) with + | none => none + | some (s', x') => some (s', x') + | some (s', x') => normalize (s', x') + +/-- `positivize` and `normalize` -/ +def tidy (p : Constraint × Coeffs) : Constraint × Coeffs := + tidy? p |>.getD p + +/-- Shorthand for the first component of `tidy`. -/ +abbrev tidyConstraint (s : Constraint) (x : Coeffs) : Constraint := (tidy (s, x)).1 +/-- Shorthand for the second component of `tidy`. -/ +abbrev tidyCoeffs (s : Constraint) (x : Coeffs) : Coeffs := (tidy (s, x)).2 + +theorem tidy_sat {s x v} (w : s.sat' x v) : (tidyConstraint s x).sat' (tidyCoeffs s x) v := by + dsimp [tidyConstraint, tidyCoeffs, tidy, tidy?] + split <;> rename_i hp + · split <;> rename_i hn + · simp_all + · rcases normalize?_eq_some hn with ⟨rfl, rfl⟩ + exact normalize_sat w + · rcases positivize?_eq_some hp with ⟨rfl, rfl⟩ + exact normalize_sat (positivize_sat w) + +theorem combo_sat' (s t : Constraint) + (a : Int) (x : Coeffs) (b : Int) (y : Coeffs) (v : Coeffs) + (wx : s.sat' x v) (wy : t.sat' y v) : + (Constraint.combo a s b t).sat' (Coeffs.combo a x b y) v := by + rw [Constraint.sat', Coeffs.combo_eq_smul_add_smul, Coeffs.dot_distrib_left, + Coeffs.dot_smul_left, Coeffs.dot_smul_left] + exact Constraint.combo_sat a wx b wy + +/-- The value of the new variable introduced when solving a hard equality. -/ +abbrev bmod_div_term (m : Nat) (a b : Coeffs) : Int := Coeffs.bmod_dot_sub_dot_bmod m a b / m + +/-- The coefficients of the new equation generated when solving a hard equality. -/ +def bmod_coeffs (m : Nat) (i : Nat) (x : Coeffs) : Coeffs := + Coeffs.set (Coeffs.bmod x m) i m + +theorem bmod_sat (m : Nat) (r : Int) (i : Nat) (x v : Coeffs) + (h : x.length ≤ i) -- during proof reconstruction this will be by `decide` + (p : Coeffs.get v i = bmod_div_term m x v) -- and this will be by `rfl` + (w : (Constraint.exact r).sat' x v) : + (Constraint.exact (Int.bmod r m)).sat' (bmod_coeffs m i x) v := by + simp at w + simp only [p, bmod_coeffs, Constraint.exact_sat, Coeffs.dot_set_left, decide_eq_true_eq] + replace h := Nat.le_trans (Coeffs.bmod_length x m) h + rw [Coeffs.get_of_length_le h, Int.sub_zero, + Int.mul_ediv_cancel' (Coeffs.dvd_bmod_dot_sub_dot_bmod _ _ _), w, + ← Int.add_sub_assoc, Int.add_comm, Int.add_sub_assoc, Int.sub_self, Int.add_zero] + +end Lean.Omega diff --git a/src/Init/Omega/Int.lean b/src/Init/Omega/Int.lean new file mode 100644 index 0000000000..e0d39c6df1 --- /dev/null +++ b/src/Init/Omega/Int.lean @@ -0,0 +1,174 @@ +/- +Copyright (c) 2023 Lean FRO, LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Scott Morrison +-/ +prelude +import Init.Data.Int.Order + +/-! +# Lemmas about `Nat` and `Int` needed internally by `omega`. + +These statements are useful for constructing proof expressions, +but unlikely to be widely useful, so are inside the `Std.Tactic.Omega` namespace. + +If you do find a use for them, please move them into the appropriate file and namespace! +-/ + +namespace Lean.Omega + +namespace Int + +theorem ofNat_pow (a b : Nat) : ((a ^ b : Nat) : Int) = (a : Int) ^ b := by + induction b with + | zero => rfl + | succ b ih => rw [Nat.pow_succ, Int.ofNat_mul, ih]; rfl + +theorem pos_pow_of_pos (a : Int) (b : Nat) (h : 0 < a) : 0 < a ^ b := by + rw [Int.eq_natAbs_of_zero_le (Int.le_of_lt h), ← Int.ofNat_zero, ← Int.ofNat_pow, Int.ofNat_lt] + exact Nat.pos_pow_of_pos _ (Int.natAbs_pos.mpr (Int.ne_of_gt h)) + +theorem ofNat_pos {a : Nat} : 0 < (a : Int) ↔ 0 < a := by + rw [← Int.ofNat_zero, Int.ofNat_lt] + +theorem ofNat_pos_of_pos {a : Nat} (h : 0 < a) : 0 < (a : Int) := + ofNat_pos.mpr h + +theorem natCast_ofNat {x : Nat} : + @Nat.cast Int instNatCastInt (no_index (OfNat.ofNat x)) = OfNat.ofNat x := rfl + +theorem ofNat_lt_of_lt {x y : Nat} (h : x < y) : (x : Int) < (y : Int) := + Int.ofNat_lt.mpr h + +theorem ofNat_le_of_le {x y : Nat} (h : x ≤ y) : (x : Int) ≤ (y : Int) := + Int.ofNat_le.mpr h + +-- FIXME these are insane: +theorem lt_of_not_ge {x y : Int} (h : ¬ (x ≤ y)) : y < x := Int.not_le.mp h +theorem lt_of_not_le {x y : Int} (h : ¬ (x ≤ y)) : y < x := Int.not_le.mp h +theorem not_le_of_lt {x y : Int} (h : y < x) : ¬ (x ≤ y) := Int.not_le.mpr h +theorem lt_le_asymm {x y : Int} (h₁ : y < x) (h₂ : x ≤ y) : False := Int.not_le.mpr h₁ h₂ +theorem le_lt_asymm {x y : Int} (h₁ : y ≤ x) (h₂ : x < y) : False := Int.not_lt.mpr h₁ h₂ + +theorem le_of_not_gt {x y : Int} (h : ¬ (y > x)) : y ≤ x := Int.not_lt.mp h +theorem not_lt_of_ge {x y : Int} (h : y ≥ x) : ¬ (y < x) := Int.not_lt.mpr h +theorem le_of_not_lt {x y : Int} (h : ¬ (x < y)) : y ≤ x := Int.not_lt.mp h +theorem not_lt_of_le {x y : Int} (h : y ≤ x) : ¬ (x < y) := Int.not_lt.mpr h + +theorem add_congr {a b c d : Int} (h₁ : a = b) (h₂ : c = d) : a + c = b + d := by + subst h₁; subst h₂; rfl + +theorem mul_congr {a b c d : Int} (h₁ : a = b) (h₂ : c = d) : a * c = b * d := by + subst h₁; subst h₂; rfl + +theorem mul_congr_left {a b : Int} (h₁ : a = b) (c : Int) : a * c = b * c := by + subst h₁; rfl + +theorem sub_congr {a b c d : Int} (h₁ : a = b) (h₂ : c = d) : a - c = b - d := by + subst h₁; subst h₂; rfl + +theorem neg_congr {a b : Int} (h₁ : a = b) : -a = -b := by + subst h₁; rfl + +theorem lt_of_gt {x y : Int} (h : x > y) : y < x := gt_iff_lt.mp h +theorem le_of_ge {x y : Int} (h : x ≥ y) : y ≤ x := ge_iff_le.mp h + +theorem ofNat_sub_eq_zero {b a : Nat} (h : ¬ b ≤ a) : ((a - b : Nat) : Int) = 0 := + Int.ofNat_eq_zero.mpr (Nat.sub_eq_zero_of_le (Nat.le_of_lt (Nat.not_le.mp h))) + +theorem ofNat_sub_dichotomy {a b : Nat} : + b ≤ a ∧ ((a - b : Nat) : Int) = a - b ∨ a < b ∧ ((a - b : Nat) : Int) = 0 := by + by_cases h : b ≤ a + · left + have t := Int.ofNat_sub h + simp at t + exact ⟨h, t⟩ + · right + have t := Nat.not_le.mp h + simp [Int.ofNat_sub_eq_zero h] + exact t + +theorem ofNat_congr {a b : Nat} (h : a = b) : (a : Int) = (b : Int) := congrArg _ h + +theorem ofNat_sub_sub {a b c : Nat} : ((a - b - c : Nat) : Int) = ((a - (b + c) : Nat) : Int) := + congrArg _ (Nat.sub_sub _ _ _) + +theorem ofNat_min (a b : Nat) : ((min a b : Nat) : Int) = min (a : Int) (b : Int) := by + simp only [Nat.min_def, Int.min_def, Int.ofNat_le] + split <;> rfl + +theorem ofNat_max (a b : Nat) : ((max a b : Nat) : Int) = max (a : Int) (b : Int) := by + simp only [Nat.max_def, Int.max_def, Int.ofNat_le] + split <;> rfl + +theorem ofNat_natAbs (a : Int) : (a.natAbs : Int) = if 0 ≤ a then a else -a := by + rw [Int.natAbs] + split <;> rename_i n + · simp only [Int.ofNat_eq_coe] + rw [if_pos (Int.ofNat_nonneg n)] + · simp; rfl + +theorem natAbs_dichotomy {a : Int} : 0 ≤ a ∧ a.natAbs = a ∨ a < 0 ∧ a.natAbs = -a := by + by_cases h : 0 ≤ a + · left + simp_all [Int.natAbs_of_nonneg] + · right + rw [Int.not_le] at h + rw [Int.ofNat_natAbs_of_nonpos (Int.le_of_lt h)] + simp_all + +theorem neg_le_natAbs {a : Int} : -a ≤ a.natAbs := by + have t := Int.le_natAbs (a := -a) + simp at t + exact t + +theorem add_le_iff_le_sub (a b c : Int) : a + b ≤ c ↔ a ≤ c - b := by + conv => + lhs + rw [← Int.add_zero c, ← Int.sub_self (-b), Int.sub_eq_add_neg, ← Int.add_assoc, Int.neg_neg, + Int.add_le_add_iff_right] + +theorem le_add_iff_sub_le (a b c : Int) : a ≤ b + c ↔ a - c ≤ b := by + conv => + lhs + rw [← Int.neg_neg c, ← Int.sub_eq_add_neg, ← add_le_iff_le_sub] + +theorem add_le_zero_iff_le_neg (a b : Int) : a + b ≤ 0 ↔ a ≤ - b := by + rw [add_le_iff_le_sub, Int.zero_sub] +theorem add_le_zero_iff_le_neg' (a b : Int) : a + b ≤ 0 ↔ b ≤ -a := by + rw [Int.add_comm, add_le_zero_iff_le_neg] +theorem add_nonnneg_iff_neg_le (a b : Int) : 0 ≤ a + b ↔ -b ≤ a := by + rw [le_add_iff_sub_le, Int.zero_sub] +theorem add_nonnneg_iff_neg_le' (a b : Int) : 0 ≤ a + b ↔ -a ≤ b := by + rw [Int.add_comm, add_nonnneg_iff_neg_le] + +theorem ofNat_fst_mk {β} {x : Nat} {y : β} : (Prod.mk x y).fst = (x : Int) := rfl +theorem ofNat_snd_mk {α} {x : α} {y : Nat} : (Prod.mk x y).snd = (y : Int) := rfl + + +end Int + +namespace Nat + +theorem lt_of_gt {x y : Nat} (h : x > y) : y < x := gt_iff_lt.mp h +theorem le_of_ge {x y : Nat} (h : x ≥ y) : y ≤ x := ge_iff_le.mp h + +end Nat + +namespace Prod + +theorem of_lex (w : Prod.Lex r s p q) : r p.fst q.fst ∨ p.fst = q.fst ∧ s p.snd q.snd := + (Prod.lex_def r s).mp w + +theorem of_not_lex {α} {r : α → α → Prop} [DecidableEq α] {β} {s : β → β → Prop} + {p q : α × β} (w : ¬ Prod.Lex r s p q) : + ¬ r p.fst q.fst ∧ (p.fst ≠ q.fst ∨ ¬ s p.snd q.snd) := by + rw [Prod.lex_def, not_or, Decidable.not_and_iff_or_not_not] at w + exact w + +theorem fst_mk : (Prod.mk x y).fst = x := rfl +theorem snd_mk : (Prod.mk x y).snd = y := rfl + +end Prod + +end Lean.Omega diff --git a/src/Init/Omega/IntList.lean b/src/Init/Omega/IntList.lean new file mode 100644 index 0000000000..f8c80147fd --- /dev/null +++ b/src/Init/Omega/IntList.lean @@ -0,0 +1,412 @@ +/- +Copyright (c) 2023 Lean FRO, LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Scott Morrison +-/ +prelude +import Init.Data.List.Lemmas + +namespace Lean.Omega + +/-- +A type synonym for `List Int`, used by `omega` for dense representation of coefficients. + +We define algebraic operations, +interpreting `List Int` as a finitely supported function `Nat → Int`. +-/ +abbrev IntList := List Int + +namespace IntList + +/-- Get the `i`-th element (interpreted as `0` if the list is not long enough). -/ +def get (xs : IntList) (i : Nat) : Int := (xs.get? i).getD 0 + +@[simp] theorem get_nil : get ([] : IntList) i = 0 := rfl +@[simp] theorem get_cons_zero : get (x :: xs) 0 = x := rfl +@[simp] theorem get_cons_succ : get (x :: xs) (i+1) = get xs i := rfl + +theorem get_map {xs : IntList} (h : f 0 = 0) : get (xs.map f) i = f (xs.get i) := by + simp only [get, List.get?_map] + cases xs.get? i <;> simp_all + +theorem get_of_length_le {xs : IntList} (h : xs.length ≤ i) : xs.get i = 0 := by + rw [get, List.get?_eq_none.mpr h] + rfl + +-- theorem lt_length_of_get_nonzero {xs : IntList} (h : xs.get i ≠ 0) : i < xs.length := by +-- revert h +-- simpa using mt get_of_length_le + +/-- Like `List.set`, but right-pad with zeroes as necessary first. -/ +def set (xs : IntList) (i : Nat) (y : Int) : IntList := + match xs, i with + | [], 0 => [y] + | [], (i+1) => 0 :: set [] i y + | _ :: xs, 0 => y :: xs + | x :: xs, (i+1) => x :: set xs i y + +@[simp] theorem set_nil_zero : set [] 0 y = [y] := rfl +@[simp] theorem set_nil_succ : set [] (i+1) y = 0 :: set [] i y := rfl +@[simp] theorem set_cons_zero : set (x :: xs) 0 y = y :: xs := rfl +@[simp] theorem set_cons_succ : set (x :: xs) (i+1) y = x :: set xs i y := rfl + +/-- Returns the leading coefficient, i.e. the first non-zero entry. -/ +def leading (xs : IntList) : Int := xs.find? (! · == 0) |>.getD 0 + +/-- Implementation of `+` on `IntList`. -/ +def add (xs ys : IntList) : IntList := + List.zipWithAll (fun x y => x.getD 0 + y.getD 0) xs ys + +instance : Add IntList := ⟨add⟩ + +theorem add_def (xs ys : IntList) : + xs + ys = List.zipWithAll (fun x y => x.getD 0 + y.getD 0) xs ys := + rfl + +@[simp] theorem add_get (xs ys : IntList) (i : Nat) : (xs + ys).get i = xs.get i + ys.get i := by + simp only [add_def, get, List.zipWithAll_get?, List.get?_eq_none] + cases xs.get? i <;> cases ys.get? i <;> simp + +@[simp] theorem add_nil (xs : IntList) : xs + [] = xs := by simp [add_def] +@[simp] theorem nil_add (xs : IntList) : [] + xs = xs := by simp [add_def] +@[simp] theorem cons_add_cons (x) (xs : IntList) (y) (ys : IntList) : + (x :: xs) + (y :: ys) = (x + y) :: (xs + ys) := by simp [add_def] + +/-- Implementation of `*` on `IntList`. -/ +def mul (xs ys : IntList) : IntList := List.zipWith (· * ·) xs ys + +instance : Mul IntList := ⟨mul⟩ + +theorem mul_def (xs ys : IntList) : xs * ys = List.zipWith (· * ·) xs ys := + rfl + +@[simp] theorem mul_get (xs ys : IntList) (i : Nat) : (xs * ys).get i = xs.get i * ys.get i := by + simp only [mul_def, get, List.zipWith_get?] + cases xs.get? i <;> cases ys.get? i <;> simp + +@[simp] theorem mul_nil_left : ([] : IntList) * ys = [] := rfl +@[simp] theorem mul_nil_right : xs * ([] : IntList) = [] := List.zipWith_nil_right +@[simp] theorem mul_cons₂ : (x::xs : IntList) * (y::ys) = (x * y) :: (xs * ys) := rfl + +/-- Implementation of negation on `IntList`. -/ +def neg (xs : IntList) : IntList := xs.map fun x => -x + +instance : Neg IntList := ⟨neg⟩ + +theorem neg_def (xs : IntList) : - xs = xs.map fun x => -x := rfl + +@[simp] theorem neg_get (xs : IntList) (i : Nat) : (- xs).get i = - xs.get i := by + simp only [neg_def, get, List.get?_map] + cases xs.get? i <;> simp + +@[simp] theorem neg_nil : (- ([] : IntList)) = [] := rfl +@[simp] theorem neg_cons : (- (x::xs : IntList)) = -x :: -xs := rfl + +/-- Implementation of subtraction on `IntList`. -/ +def sub (xs ys : IntList) : IntList := + List.zipWithAll (fun x y => x.getD 0 - y.getD 0) xs ys + +instance : Sub IntList := ⟨sub⟩ + +theorem sub_def (xs ys : IntList) : + xs - ys = List.zipWithAll (fun x y => x.getD 0 - y.getD 0) xs ys := + rfl + +/-- Implementation of scalar multiplication by an integer on `IntList`. -/ +def smul (xs : IntList) (i : Int) : IntList := + xs.map fun x => i * x + +instance : HMul Int IntList IntList where + hMul i xs := xs.smul i + +theorem smul_def (xs : IntList) (i : Int) : i * xs = xs.map fun x => i * x := rfl + +@[simp] theorem smul_get (xs : IntList) (a : Int) (i : Nat) : (a * xs).get i = a * xs.get i := by + simp only [smul_def, get, List.get?_map] + cases xs.get? i <;> simp + +@[simp] theorem smul_nil {i : Int} : i * ([] : IntList) = [] := rfl +@[simp] theorem smul_cons {i : Int} : i * (x::xs : IntList) = i * x :: i * xs := rfl + +/-- A linear combination of two `IntList`s. -/ +def combo (a : Int) (xs : IntList) (b : Int) (ys : IntList) : IntList := + List.zipWithAll (fun x y => a * x.getD 0 + b * y.getD 0) xs ys + +theorem combo_eq_smul_add_smul (a : Int) (xs : IntList) (b : Int) (ys : IntList) : + combo a xs b ys = a * xs + b * ys := by + dsimp [combo] + induction xs generalizing ys with + | nil => simp; rfl + | cons x xs ih => + cases ys with + | nil => simp; rfl + | cons y ys => simp_all + +attribute [local simp] add_def mul_def in +theorem mul_distrib_left (xs ys zs : IntList) : (xs + ys) * zs = xs * zs + ys * zs := by + induction xs generalizing ys zs with + | nil => + cases ys with + | nil => simp + | cons _ _ => + cases zs with + | nil => simp + | cons _ _ => simp_all [Int.add_mul] + | cons x xs ih₁ => + cases ys with + | nil => simp_all + | cons _ _ => + cases zs with + | nil => simp + | cons _ _ => simp_all [Int.add_mul] + +theorem mul_neg_left (xs ys : IntList) : (-xs) * ys = -(xs * ys) := by + induction xs generalizing ys with + | nil => simp + | cons x xs ih => + cases ys with + | nil => simp + | cons y ys => simp_all [Int.neg_mul] + +attribute [local simp] add_def neg_def sub_def in +theorem sub_eq_add_neg (xs ys : IntList) : xs - ys = xs + (-ys) := by + induction xs generalizing ys with + | nil => simp; rfl + | cons x xs ih => + cases ys with + | nil => simp + | cons y ys => simp_all [Int.sub_eq_add_neg] + +@[simp] theorem mul_smul_left {i : Int} {xs ys : IntList} : (i * xs) * ys = i * (xs * ys) := by + induction xs generalizing ys with + | nil => simp + | cons x xs ih => + cases ys with + | nil => simp + | cons y ys => simp_all [Int.mul_assoc] + +/-- The sum of the entries of an `IntList`. -/ +def sum (xs : IntList) : Int := xs.foldr (· + ·) 0 + +@[simp] theorem sum_nil : sum ([] : IntList) = 0 := rfl +@[simp] theorem sum_cons : sum (x::xs : IntList) = x + sum xs := rfl + +attribute [local simp] sum add_def in +theorem sum_add (xs ys : IntList) : (xs + ys).sum = xs.sum + ys.sum := by + induction xs generalizing ys with + | nil => simp + | cons x xs ih => + cases ys with + | nil => simp + | cons y ys => simp_all [Int.add_assoc, Int.add_left_comm] + +@[simp] +theorem sum_neg (xs : IntList) : (-xs).sum = -(xs.sum) := by + induction xs with + | nil => simp + | cons x xs ih => simp_all [Int.neg_add] + +@[simp] +theorem sum_smul (i : Int) (xs : IntList) : (i * xs).sum = i * (xs.sum) := by + induction xs with + | nil => simp + | cons x xs ih => simp_all [Int.mul_add] + +/-- The dot product of two `IntList`s. -/ +def dot (xs ys : IntList) : Int := (xs * ys).sum + +example : IntList.dot [a, b, c] [x, y, z] = IntList.dot [a, b, c, d] [x, y, z] := rfl +example : IntList.dot [a, b, c] [x, y, z] = IntList.dot [a, b, c] [x, y, z, w] := rfl + +@[local simp] theorem dot_nil_left : dot ([] : IntList) ys = 0 := rfl +@[simp] theorem dot_nil_right : dot xs ([] : IntList) = 0 := by simp [dot] +@[simp] theorem dot_cons₂ : dot (x::xs) (y::ys) = x * y + dot xs ys := rfl + +-- theorem dot_comm (xs ys : IntList) : dot xs ys = dot ys xs := by +-- rw [dot, dot, mul_comm] + +@[simp] theorem dot_set_left (xs ys : IntList) (i : Nat) (z : Int) : + dot (xs.set i z) ys = dot xs ys + (z - xs.get i) * ys.get i := by + induction xs generalizing i ys with + | nil => + induction i generalizing ys with + | zero => cases ys <;> simp + | succ i => cases ys <;> simp_all + | cons x xs ih => + induction i generalizing ys with + | zero => + cases ys with + | nil => simp + | cons y ys => + simp only [Nat.zero_eq, set_cons_zero, dot_cons₂, get_cons_zero, Int.sub_mul] + rw [Int.add_right_comm, Int.add_comm (x * y), Int.sub_add_cancel] + | succ i => + cases ys with + | nil => simp + | cons y ys => simp_all [Int.add_assoc] + +theorem dot_distrib_left (xs ys zs : IntList) : (xs + ys).dot zs = xs.dot zs + ys.dot zs := by + simp [dot, mul_distrib_left, sum_add] + +@[simp] theorem dot_neg_left (xs ys : IntList) : (-xs).dot ys = -(xs.dot ys) := by + simp [dot, mul_neg_left] + +@[simp] theorem dot_smul_left (xs ys : IntList) (i : Int) : (i * xs).dot ys = i * xs.dot ys := by + simp [dot] + +theorem dot_of_left_zero (w : ∀ x, x ∈ xs → x = 0) : dot xs ys = 0 := by + induction xs generalizing ys with + | nil => simp + | cons x xs ih => + cases ys with + | nil => simp + | cons y ys => + rw [dot_cons₂, w x (by simp), ih] + · simp + · intro x m + apply w + exact List.mem_cons_of_mem _ m + +/-- Division of an `IntList` by a integer. -/ +def sdiv (xs : IntList) (g : Int) : IntList := xs.map fun x => x / g + +@[simp] theorem sdiv_nil : sdiv [] g = [] := rfl +@[simp] theorem sdiv_cons : sdiv (x::xs) g = (x / g) :: sdiv xs g := rfl + +/-- The gcd of the absolute values of the entries of an `IntList`. -/ +def gcd (xs : IntList) : Nat := xs.foldr (fun x g => Nat.gcd x.natAbs g) 0 + +@[simp] theorem gcd_nil : gcd [] = 0 := rfl +@[simp] theorem gcd_cons : gcd (x :: xs) = Nat.gcd x.natAbs (gcd xs) := rfl + +theorem gcd_cons_div_left : (gcd (x::xs) : Int) ∣ x := by + simp only [gcd, List.foldr_cons, Int.ofNat_dvd_left] + apply Nat.gcd_dvd_left + +theorem gcd_cons_div_right : gcd (x::xs) ∣ gcd xs := by + simp only [gcd, List.foldr_cons] + apply Nat.gcd_dvd_right + +theorem gcd_cons_div_right' : (gcd (x::xs) : Int) ∣ (gcd xs : Int) := by + rw [Int.ofNat_dvd_left, Int.natAbs_ofNat] + exact gcd_cons_div_right + +theorem gcd_dvd (xs : IntList) {a : Int} (m : a ∈ xs) : (xs.gcd : Int) ∣ a := by + rw [Int.ofNat_dvd_left] + induction m with + | head => + simp only [gcd_cons] + apply Nat.gcd_dvd_left + | tail b m ih => -- FIXME: why is the argument of tail implicit? + simp only [gcd_cons] + exact Nat.dvd_trans (Nat.gcd_dvd_right _ _) ih + +theorem dvd_gcd (xs : IntList) (c : Nat) (w : ∀ {a : Int}, a ∈ xs → (c : Int) ∣ a) : + c ∣ xs.gcd := by + simp only [Int.ofNat_dvd_left] at w + induction xs with + | nil => have := Nat.dvd_zero c; simp at this; exact this + | cons x xs ih => + simp + apply Nat.dvd_gcd + · apply w + simp + · apply ih + intro b m + apply w + exact List.mem_cons_of_mem x m + +theorem gcd_eq_iff (xs : IntList) (g : Nat) : + xs.gcd = g ↔ + (∀ {a : Int}, a ∈ xs → (g : Int) ∣ a) ∧ + (∀ (c : Nat), (∀ {a : Int}, a ∈ xs → (c : Int) ∣ a) → c ∣ g) := by + constructor + · rintro rfl + exact ⟨gcd_dvd _, dvd_gcd _⟩ + · rintro ⟨hi, hg⟩ + apply Nat.dvd_antisymm + · apply hg + intro i m + exact gcd_dvd xs m + · exact dvd_gcd xs g hi + +attribute [simp] Int.zero_dvd + +@[simp] theorem gcd_eq_zero (xs : IntList) : xs.gcd = 0 ↔ ∀ x, x ∈ xs → x = 0 := by + simp [gcd_eq_iff, Nat.dvd_zero] + +@[simp] theorem dot_mod_gcd_left (xs ys : IntList) : dot xs ys % xs.gcd = 0 := by + induction xs generalizing ys with + | nil => simp + | cons x xs ih => + cases ys with + | nil => simp + | cons y ys => + rw [dot_cons₂, Int.add_emod, + ← Int.emod_emod_of_dvd (x * y) (gcd_cons_div_left), + ← Int.emod_emod_of_dvd (dot xs ys) (Int.ofNat_dvd.mpr gcd_cons_div_right)] + simp_all + +theorem gcd_dvd_dot_left (xs ys : IntList) : (xs.gcd : Int) ∣ dot xs ys := + Int.dvd_of_emod_eq_zero (dot_mod_gcd_left xs ys) + +@[simp] +theorem dot_eq_zero_of_left_eq_zero {xs ys : IntList} (h : ∀ x, x ∈ xs → x = 0) : dot xs ys = 0 := by + induction xs generalizing ys with + | nil => rfl + | cons x xs ih => + cases ys with + | nil => rfl + | cons y ys => + rw [dot_cons₂, h x (List.mem_cons_self _ _), ih (fun x m => h x (List.mem_cons_of_mem _ m)), + Int.zero_mul, Int.add_zero] + +theorem dot_sdiv_left (xs ys : IntList) {d : Int} (h : d ∣ xs.gcd) : + dot (xs.sdiv d) ys = (dot xs ys) / d := by + induction xs generalizing ys with + | nil => simp + | cons x xs ih => + cases ys with + | nil => simp + | cons y ys => + have wx : d ∣ x := Int.dvd_trans h (gcd_cons_div_left) + have wxy : d ∣ x * y := Int.dvd_trans wx (Int.dvd_mul_right x y) + have w : d ∣ (IntList.gcd xs : Int) := Int.dvd_trans h (gcd_cons_div_right') + simp_all [Int.add_ediv_of_dvd_left, Int.mul_ediv_assoc'] + +/-- Apply "balanced mod" to each entry in an `IntList`. -/ +abbrev bmod (x : IntList) (m : Nat) : IntList := x.map (Int.bmod · m) + +theorem bmod_length (x : IntList) (m) : (bmod x m).length ≤ x.length := + Nat.le_of_eq (List.length_map _ _) + +/-- +The difference between the balanced mod of a dot product, +and the dot product with balanced mod applied to each entry of the left factor. +-/ +abbrev bmod_dot_sub_dot_bmod (m : Nat) (a b : IntList) : Int := + (Int.bmod (dot a b) m) - dot (bmod a m) b + +theorem dvd_bmod_dot_sub_dot_bmod (m : Nat) (xs ys : IntList) : + (m : Int) ∣ bmod_dot_sub_dot_bmod m xs ys := by + dsimp [bmod_dot_sub_dot_bmod] + rw [Int.dvd_iff_emod_eq_zero] + induction xs generalizing ys with + | nil => simp + | cons x xs ih => + cases ys with + | nil => simp + | cons y ys => + simp only [IntList.dot_cons₂, List.map_cons] + specialize ih ys + rw [Int.sub_emod, Int.bmod_emod] at ih + rw [Int.sub_emod, Int.bmod_emod, Int.add_emod, Int.add_emod (Int.bmod x m * y), + ← Int.sub_emod, ← Int.sub_sub, Int.sub_eq_add_neg, Int.sub_eq_add_neg, + Int.add_assoc (x * y % m), Int.add_comm (IntList.dot _ _ % m), ← Int.add_assoc, + Int.add_assoc, ← Int.sub_eq_add_neg, ← Int.sub_eq_add_neg, Int.add_emod, ih, Int.add_zero, + Int.emod_emod, Int.mul_emod, Int.mul_emod (Int.bmod x m), Int.bmod_emod, Int.sub_self, + Int.zero_emod] + +end IntList + +end Lean.Omega diff --git a/src/Init/Omega/LinearCombo.lean b/src/Init/Omega/LinearCombo.lean new file mode 100644 index 0000000000..89bb661241 --- /dev/null +++ b/src/Init/Omega/LinearCombo.lean @@ -0,0 +1,178 @@ +/- +Copyright (c) 2023 Lean FRO, LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Scott Morrison +-/ +prelude +import Init.Omega.Coeffs + +/-! +# Linear combinations + +We use this data structure while processing hypotheses. + +-/ + +namespace Lean.Omega + +/-- Internal representation of a linear combination of atoms, and a constant term. -/ +structure LinearCombo where + /-- Constant term. -/ + const : Int := 0 + /-- Coefficients of the atoms. -/ + coeffs : Coeffs := [] +deriving DecidableEq, Repr + +namespace LinearCombo + +instance : ToString LinearCombo where + toString lc := + s!"{lc.const}{String.join <| lc.coeffs.toList.enum.map fun ⟨i, c⟩ => s!" + {c} * x{i+1}"}" + +instance : Inhabited LinearCombo := ⟨{const := 1}⟩ + +theorem ext {a b : LinearCombo} (w₁ : a.const = b.const) (w₂ : a.coeffs = b.coeffs) : + a = b := by + cases a; cases b + subst w₁; subst w₂ + congr + +/-- +Evaluate a linear combination `⟨r, [c_1, …, c_k]⟩` at values `[v_1, …, v_k]` to obtain +`r + (c_1 * x_1 + (c_2 * x_2 + ... (c_k * x_k + 0))))`. +-/ +def eval (lc : LinearCombo) (values : Coeffs) : Int := + lc.const + lc.coeffs.dot values + +@[simp] theorem eval_nil : (lc : LinearCombo).eval .nil = lc.const := by + simp [eval] + +/-- The `i`-th coordinate function. -/ +def coordinate (i : Nat) : LinearCombo where + const := 0 + coeffs := Coeffs.set .nil i 1 + +@[simp] theorem coordinate_eval (i : Nat) (v : Coeffs) : + (coordinate i).eval v = v.get i := by + simp [eval, coordinate] + +theorem coordinate_eval_0 : (coordinate 0).eval (.ofList (a0 :: t)) = a0 := by simp +theorem coordinate_eval_1 : (coordinate 1).eval (.ofList (a0 :: a1 :: t)) = a1 := by simp +theorem coordinate_eval_2 : (coordinate 2).eval (.ofList (a0 :: a1 :: a2 :: t)) = a2 := by simp +theorem coordinate_eval_3 : + (coordinate 3).eval (.ofList (a0 :: a1 :: a2 :: a3 :: t)) = a3 := by simp +theorem coordinate_eval_4 : + (coordinate 4).eval (.ofList (a0 :: a1 :: a2 :: a3 :: a4 :: t)) = a4 := by simp +theorem coordinate_eval_5 : + (coordinate 5).eval (.ofList (a0 :: a1 :: a2 :: a3 :: a4 :: a5 :: t)) = a5 := by simp +theorem coordinate_eval_6 : + (coordinate 6).eval (.ofList (a0 :: a1 :: a2 :: a3 :: a4 :: a5 :: a6 :: t)) = a6 := by simp +theorem coordinate_eval_7 : + (coordinate 7).eval + (.ofList (a0 :: a1 :: a2 :: a3 :: a4 :: a5 :: a6 :: a7 :: t)) = a7 := by simp +theorem coordinate_eval_8 : + (coordinate 8).eval + (.ofList (a0 :: a1 :: a2 :: a3 :: a4 :: a5 :: a6 :: a7 :: a8 :: t)) = a8 := by simp +theorem coordinate_eval_9 : + (coordinate 9).eval + (.ofList (a0 :: a1 :: a2 :: a3 :: a4 :: a5 :: a6 :: a7 :: a8 :: a9 :: t)) = a9 := by simp + +/-- Implementation of addition on `LinearCombo`. -/ +def add (l₁ l₂ : LinearCombo) : LinearCombo where + const := l₁.const + l₂.const + coeffs := l₁.coeffs + l₂.coeffs + +instance : Add LinearCombo := ⟨add⟩ + +@[simp] theorem add_const {l₁ l₂ : LinearCombo} : (l₁ + l₂).const = l₁.const + l₂.const := rfl +@[simp] theorem add_coeffs {l₁ l₂ : LinearCombo} : (l₁ + l₂).coeffs = l₁.coeffs + l₂.coeffs := rfl + +/-- Implementation of subtraction on `LinearCombo`. -/ +def sub (l₁ l₂ : LinearCombo) : LinearCombo where + const := l₁.const - l₂.const + coeffs := l₁.coeffs - l₂.coeffs + +instance : Sub LinearCombo := ⟨sub⟩ + +@[simp] theorem sub_const {l₁ l₂ : LinearCombo} : (l₁ - l₂).const = l₁.const - l₂.const := rfl +@[simp] theorem sub_coeffs {l₁ l₂ : LinearCombo} : (l₁ - l₂).coeffs = l₁.coeffs - l₂.coeffs := rfl + +/-- Implementation of negation on `LinearCombo`. -/ +def neg (lc : LinearCombo) : LinearCombo where + const := -lc.const + coeffs := -lc.coeffs + +instance : Neg LinearCombo := ⟨neg⟩ + +@[simp] theorem neg_const {l : LinearCombo} : (-l).const = -l.const := rfl +@[simp] theorem neg_coeffs {l : LinearCombo} : (-l).coeffs = -l.coeffs := rfl + +theorem sub_eq_add_neg (l₁ l₂ : LinearCombo) : l₁ - l₂ = l₁ + -l₂ := by + rcases l₁ with ⟨a₁, c₁⟩; rcases l₂ with ⟨a₂, c₂⟩ + apply ext + · simp [Int.sub_eq_add_neg] + · simp [Coeffs.sub_eq_add_neg] + +/-- Implementation of scalar multiplication of a `LinearCombo` by an `Int`. -/ +def smul (lc : LinearCombo) (i : Int) : LinearCombo where + const := i * lc.const + coeffs := lc.coeffs.smul i + +instance : HMul Int LinearCombo LinearCombo := ⟨fun i lc => lc.smul i⟩ + +@[simp] theorem smul_const {lc : LinearCombo} {i : Int} : (i * lc).const = i * lc.const := rfl +@[simp] theorem smul_coeffs {lc : LinearCombo} {i : Int} : (i * lc).coeffs = i * lc.coeffs := rfl + +@[simp] theorem add_eval (l₁ l₂ : LinearCombo) (v : Coeffs) : + (l₁ + l₂).eval v = l₁.eval v + l₂.eval v := by + rcases l₁ with ⟨r₁, c₁⟩; rcases l₂ with ⟨r₂, c₂⟩ + simp only [eval, add_const, add_coeffs, Int.add_assoc, Int.add_left_comm] + congr + exact Coeffs.dot_distrib_left c₁ c₂ v + +@[simp] theorem neg_eval (lc : LinearCombo) (v : Coeffs) : (-lc).eval v = - lc.eval v := by + rcases lc with ⟨a, coeffs⟩ + simp [eval, Int.neg_add] + +@[simp] theorem sub_eval (l₁ l₂ : LinearCombo) (v : Coeffs) : + (l₁ - l₂).eval v = l₁.eval v - l₂.eval v := by + simp [sub_eq_add_neg, Int.sub_eq_add_neg] + +@[simp] theorem smul_eval (lc : LinearCombo) (i : Int) (v : Coeffs) : + (i * lc).eval v = i * lc.eval v := by + rcases lc with ⟨a, coeffs⟩ + simp [eval, Int.mul_add] + +theorem smul_eval_comm (lc : LinearCombo) (i : Int) (v : Coeffs) : + (i * lc).eval v = lc.eval v * i := by + simp [Int.mul_comm] + +/-- +Multiplication of two linear combinations. +This is useful only if at least one of the linear combinations is constant, +and otherwise should be considered as a junk value. +-/ +def mul (l₁ l₂ : LinearCombo) : LinearCombo := + l₂.const * l₁ + l₁.const * l₂ - { const := l₁.const * l₂.const } + +theorem mul_eval_of_const_left (l₁ l₂ : LinearCombo) (v : Coeffs) (w : l₁.coeffs.isZero) : + (mul l₁ l₂).eval v = l₁.eval v * l₂.eval v := by + have : Coeffs.dot l₁.coeffs v = 0 := IntList.dot_of_left_zero w + simp [mul, eval, this, Coeffs.sub_eq_add_neg, Coeffs.dot_distrib_left, Int.add_mul, Int.mul_add, + Int.mul_comm] + +theorem mul_eval_of_const_right (l₁ l₂ : LinearCombo) (v : Coeffs) (w : l₂.coeffs.isZero) : + (mul l₁ l₂).eval v = l₁.eval v * l₂.eval v := by + have : Coeffs.dot l₂.coeffs v = 0 := IntList.dot_of_left_zero w + simp [mul, eval, this, Coeffs.sub_eq_add_neg, Coeffs.dot_distrib_left, Int.add_mul, Int.mul_add, + Int.mul_comm] + +theorem mul_eval (l₁ l₂ : LinearCombo) (v : Coeffs) (w : l₁.coeffs.isZero ∨ l₂.coeffs.isZero) : + (mul l₁ l₂).eval v = l₁.eval v * l₂.eval v := by + rcases w with w | w + · rw [mul_eval_of_const_left _ _ _ w] + · rw [mul_eval_of_const_right _ _ _ w] + +end LinearCombo + +end Lean.Omega diff --git a/src/Init/Omega/Logic.lean b/src/Init/Omega/Logic.lean new file mode 100644 index 0000000000..5963cf3469 --- /dev/null +++ b/src/Init/Omega/Logic.lean @@ -0,0 +1,50 @@ +/- +Copyright (c) 2023 Lean FRO, LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Scott Morrison +-/ +prelude +import Init.PropLemmas +/-! +# Specializations of basic logic lemmas + +These are useful for `omega` while constructing proofs, but not considered generally useful +so are hidden in the `Std.Tactic.Omega` namespace. + +If you find yourself needing them elsewhere, please move them first to another file. +-/ + +namespace Lean.Omega + +theorem and_not_not_of_not_or (h : ¬ (p ∨ q)) : ¬ p ∧ ¬ q := not_or.mp h + +theorem Decidable.or_not_not_of_not_and [Decidable p] [Decidable q] + (h : ¬ (p ∧ q)) : ¬ p ∨ ¬ q := + (Decidable.not_and_iff_or_not _ _).mp h + +theorem Decidable.and_or_not_and_not_of_iff {p q : Prop} [Decidable q] (h : p ↔ q) : + (p ∧ q) ∨ (¬p ∧ ¬q) := Decidable.iff_iff_and_or_not_and_not.mp h + +theorem Decidable.not_iff_iff_and_not_or_not_and [Decidable a] [Decidable b] : + (¬ (a ↔ b)) ↔ (a ∧ ¬ b) ∨ ((¬ a) ∧ b) := + ⟨fun e => if hb : b then + .inr ⟨fun ha => e ⟨fun _ => hb, fun _ => ha⟩, hb⟩ + else + .inl ⟨if ha : a then ha else False.elim (e ⟨fun ha' => absurd ha' ha, fun hb' => absurd hb' hb⟩), hb⟩, + Or.rec (And.rec fun ha nb w => nb (w.mp ha)) (And.rec fun na hb w => na (w.mpr hb))⟩ + +theorem Decidable.and_not_or_not_and_of_not_iff [Decidable a] [Decidable b] + (h : ¬ (a ↔ b)) : a ∧ ¬b ∨ ¬a ∧ b := + Decidable.not_iff_iff_and_not_or_not_and.mp h + +theorem Decidable.and_not_of_not_imp [Decidable a] (h : ¬(a → b)) : a ∧ ¬b := + Decidable.not_imp_iff_and_not.mp h + +theorem 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) := + if h : P then + .inl ⟨h, if_pos h⟩ + else + .inr ⟨h, if_neg h⟩ + +end Lean.Omega diff --git a/src/Init/Tactics.lean b/src/Init/Tactics.lean index 56841dff02..3c74e28894 100644 --- a/src/Init/Tactics.lean +++ b/src/Init/Tactics.lean @@ -972,6 +972,40 @@ macro "haveI" d:haveDecl : tactic => `(tactic| refine_lift haveI $d:haveDecl; ?_ /-- `letI` behaves like `let`, but inlines the value instead of producing a `let_fun` term. -/ macro "letI" d:haveDecl : tactic => `(tactic| refine_lift letI $d:haveDecl; ?_) + +/-- +The `omega` tactic, for resolving integer and natural linear arithmetic problems. + +It is not yet a full decision procedure (no "dark" or "grey" shadows), +but should be effective on many problems. + +We handle hypotheses of the form `x = y`, `x < y`, `x ≤ y`, and `k ∣ x` for `x y` in `Nat` or `Int` +(and `k` a literal), along with negations of these statements. + +We decompose the sides of the inequalities as linear combinations of atoms. + +If we encounter `x / k` or `x % k` for literal integers `k` we introduce new auxiliary variables +and the relevant inequalities. + +On the first pass, we do not perform case splits on natural subtraction. +If `omega` fails, we recursively perform a case split on +a natural subtraction appearing in a hypothesis, and try again. + +The options +``` +omega (config := + { splitDisjunctions := true, splitNatSub := true, splitNatAbs := true, splitMinMax := true }) +``` +can be used to: +* `splitDisjunctions`: split any disjunctions found in the context, + if the problem is not otherwise solvable. +* `splitNatSub`: for each appearance of `((a - b : Nat) : Int)`, split on `a ≤ b` if necessary. +* `splitNatAbs`: for each appearance of `Int.natAbs a`, split on `0 ≤ a` if necessary. +* `splitMinMax`: for each occurrence of `min a b`, split on `min a b = a ∨ min a b = b` +Currently, all of these are on by default. +-/ +syntax (name := omega) "omega" (config)? : tactic + end Tactic namespace Attr diff --git a/src/Lean/Elab/Tactic.lean b/src/Lean/Elab/Tactic.lean index 704e693ec0..442f478f98 100644 --- a/src/Lean/Elab/Tactic.lean +++ b/src/Lean/Elab/Tactic.lean @@ -30,3 +30,4 @@ import Lean.Elab.Tactic.Repeat import Lean.Elab.Tactic.Ext import Lean.Elab.Tactic.Change import Lean.Elab.Tactic.FalseOrByContra +import Lean.Elab.Tactic.Omega diff --git a/src/Lean/Elab/Tactic/Basic.lean b/src/Lean/Elab/Tactic/Basic.lean index 3b36205240..3933c022bb 100644 --- a/src/Lean/Elab/Tactic/Basic.lean +++ b/src/Lean/Elab/Tactic/Basic.lean @@ -382,6 +382,10 @@ then set the new goals to be the resulting goal list.-/ else replaceMainGoal [] +/-- Analogue of `liftMetaTactic` for tactics that do not return any goals. -/ +@[inline] def liftMetaFinishingTactic (tac : MVarId → MetaM Unit) : TacticM Unit := + liftMetaTactic fun g => do tac g; pure [] + def tryTactic? (tactic : TacticM α) : TacticM (Option α) := do try pure (some (← tactic)) diff --git a/src/Lean/Elab/Tactic/Omega.lean b/src/Lean/Elab/Tactic/Omega.lean new file mode 100644 index 0000000000..dbd52aea42 --- /dev/null +++ b/src/Lean/Elab/Tactic/Omega.lean @@ -0,0 +1,192 @@ +/- +Copyright (c) 2023 Lean FRO, LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Scott Morrison +-/ +import Lean.Elab.Tactic.Omega.Frontend + +/-! +# `omega` + +This is an implementation of the `omega` algorithm, currently without "dark" and "grey" shadows, +although the framework should be compatible with adding that part of the algorithm later. + +The implementation closely follows William Pugh's +"The omega test: a fast and practical integer programming algorithm for dependence analysis" +https://doi.org/10.1145/125826.125848. + +The `MetaM` level `omega` tactic takes a `List Expr` of facts, +and tries to discharge the goal by proving `False`. + +The user-facing `omega` tactic first calls `false_or_by_contra`, and then invokes the `omega` tactic +on all hypotheses. + +### Pre-processing + +In the `false_or_by_contra` step, we: +* if the goal is `False`, do nothing, +* if the goal is `¬ P`, introduce `P`, +* if the goal is `x ≠ y`, introduce `x = y`, +* otherwise, for a goal `P`, replace it with `¬ ¬ P` and introduce `¬ P`. + +The `omega` tactic pre-processes the hypotheses in the following ways: +* Replace `x > y` for `x y : Nat` or `x y : Int` with `x ≥ y + 1`. +* Given `x ≥ y` for `x : Nat`, replace it with `(x : Int) ≥ (y : Int)`. +* Push `Nat`-to-`Int` coercions inwards across `+`, `*`, `/`, `%`. +* Replace `k ∣ x` for a literal `k : Nat` with `x % k = 0`, + and replace `¬ k ∣ x` with `x % k > 0`. +* If `x / m` appears, for some `x : Int` and literal `m : Nat`, + replace `x / m` with a new variable `α` and add the constraints + `0 ≤ - m * α + x ≤ m - 1`. +* If `x % m` appears, similarly, introduce the same new contraints + but replace `x % m` with `- m * α + x`. +* Split conjunctions, existentials, and subtypes. +* Record, for each appearance of `(a - b : Int)` with `a b : Nat`, the disjunction + `b ≤ a ∧ ((a - b : Nat) : Int) = a - b ∨ a < b ∧ ((a - b : Nat) : Int) = 0`. + We don't immediately split this; see the discussion below for how disjunctions are handled. + +After this preprocessing stage, we have a collection of linear inequalities +(all using `≤` rather than `<`) and equalities in some set of atoms. + +TODO: We should identify atoms up to associativity and commutativity, +so that `omega` can handle problems such as `a * b < 0 && b * a > 0 → False`. +This should be a relatively easy modification of the `lookup` function in `OmegaM`. +After doing so, we could allow the preprocessor to distribute multiplication over addition. + +### Normalization + +Throughout the remainder of the algorithm, we apply the following normalization steps to +all linear constraints: +* Make the leading coefficient positive (thus giving us both upper and lower bounds). +* Divide through by the GCD of the coefficients, rounding the constant terms appropriately. +* Whenever we have both an upper and lower bound for the same coefficients, + check they are compatible. If they are tight, mark the pair of constraints as an equality. + If they are inconsistent, stop further processing. + +### Solving equalities + +The next step is to solve all equalities. + +We first solve any equalities that have a `±1` coefficient; +these allow us to eliminate that variable. + +After this, there may be equalities remaining with all coefficients having absolute value greater +than one. We select an equality `c₀ + ∑ cᵢ * xᵢ = 0` with smallest minimal absolute value +of the `cᵢ`, breaking ties by preferring equalities with smallest maximal absolute value. +We let `m = ∣cⱼ| + 1` where `cⱼ` is the coefficient with smallest absolute value.. +We then add the new equality `(bmod c₀ m) + ∑ (bmod cᵢ m) xᵢ = m α` with `α` being a new variable. +Here `bmod` is "balanced mod", taking values in `[- m/2, (m - 1)/2]`. +This equality holds (for some value of `α`) because the left hand side differs from the left hand +side of the original equality by a multiple of `m`. +Moreover, in this equality the coefficient of `xⱼ` is `±1`, so we can solve and eliminate `xⱼ`. + +So far this isn't progress: we've introduced a new variable and eliminated a variable. +However, this process terminates, as the pair `(c, C)` lexicographically decreases, +where `c` is the smallest minimal absolute value and `C` is the smallest maximal absolute value +amongst those equalities with minimal absolute value `c`. +(Happily because we're running this in metaprogramming code, we don't actually need to prove this +termination! If we later want to upgrade to a decision procedure, or to produce counterexamples +we would need to do this. It's certainly possible, and existed in an earlier prototype version.) + +### Solving inequalities + +After solving all equalities, we turn to the inequalities. + +We need to select a variable to eliminate; this choice is discussed below. + +#### Shadows + +The omega algorithm indicates we should consider three subproblems, +called the "real", "dark", and "grey" shadows. +(In fact the "grey" shadow is a disjunction of potentially many problems.) +Our problem is satisfiable if and only if the real shadow is satisfiable +and either the dark or grey shadow is satisfiable. + +Currently we do not implement either the dark or grey shadows, and thus if the real shadow is +satisfiable we must fail, and report that we couldn't find a contradiction, even though the +problem may be unsatisfiable. + +In practical problems, it appears to be relatively rare that we fail because of not handling the +dark and grey shadows. + +Fortunately, in many cases it is possible to choose a variable to eliminate such that +the real and dark shadows coincide, and the grey shadows are empty. In this situation +we don't lose anything by ignoring the dark and grey shadows. +We call this situation an exact elimination. +A sufficient condition for exactness is that either all upper bounds on `xᵢ` have unit coefficient, +or all lower bounds on `xᵢ` have unit coefficient. +We always prefer to select the value of `i` so that this condition holds, if possible. +We break ties by preferring to select a value of `i` that minimizes the number of new constraints +introduced in the real shadow. + +#### The real shadow: Fourier-Motzkin elimination + +The real shadow for a variable `i` is just the Fourier-Motzkin elimination. + +We begin by discarding all inequalities involving the variable `i`. + +Then, for each pair of constraints `f ≤ c * xᵢ` and `c' * xᵢ ≤ f'` +with both `c` and `c'` positive (i.e. for each pair of an lower and upper bound on `xᵢ`) +we introduce the new constraint `c * f' - c' * f ≥ 0`. + +(Note that if there are only upper bounds on `xᵢ`, or only lower bounds on `xᵢ` this step +simply discards inequalities.) + +#### The dark and grey shadows + +For each such new constraint `c' * f - c * f' ≤ 0`, we either have the strengthening +`c * f' - c' * f ≥ c * c' - c - c' + 1` +or we do not, i.e. +`c * f' - c' * f ≤ c * c' - c - c'`. +In the latter case, combining this inequality with `f' ≥ c' * xᵢ` we obtain +`c' * (c * xᵢ - f) ≤ c * c' - c - c'` +and as we already have `c * xᵢ - f ≥ 0`, +we conclude that `c * xᵢ - f = j` for some `j = 0, 1, ..., (c * c' - c - c')/c'` +(with, as usual the division rounded down). + +Note that the largest possible value of `j` occurs with `c'` is as large as possible. + +Thus the "dark" shadow is the variant of the real shadow where we replace each new inequality +with its strengthening. +The "grey" shadows are the union of the problems obtained by taking +a lower bound `f ≤ c * xᵢ` for `xᵢ` and some `j = 0, 1, ..., (c * m - c - m)/m`, where `m` +is the largest coefficient `c'` appearing in an upper bound `c' * xᵢ ≤ f'` for `xᵢ`, +and adding to the original problem (i.e. without doing any Fourier-Motzkin elimination) the single +new equation `c * xᵢ - f = j`, and the inequalities +`c * xᵢ - f > (c * m - c - m)/m` for each previously considered lower bound. + +As stated above, the satisfiability of the original problem is in fact equivalent to +the satisfiability of the real shadow, *and* the satisfiability of *either* the dark shadow, +or at least one of the grey shadows. + +TODO: implement the dark and grey shadows! + +### Disjunctions + +The omega algorithm as described above accumulates various disjunctions, +either coming from natural subtraction, or from the dark and grey shadows. + +When we encounter such a disjunction, we store it in a list of disjunctions, +but do not immediately split it. + +Instead we first try to find a contradiction (i.e. by eliminating equalities and inequalities) +without the disjunctive hypothesis. +If this fails, we then retrieve the first disjunction from the list, split it, +and try to find a contradiction in both branches. + +(Note that we make no attempt to optimize the order in which we split disjunctions: +it's currently on a first in first out basis.) + +The work done eliminating equalities can be reused when splitting disjunctions, +but we need to redo all the work eliminating inequalities in each branch. + +## Future work +* Implementation of dark and grey shadows. +* Identification of atoms up to associativity and commutativity of monomials. +* Further optimization. + * Some data is recomputed unnecessarily, e.g. the GCDs of coefficients. +* Sparse representation of coefficients. + * I have a branch in which this is implemented, modulo some proofs about algebraic operations + on sparse arrays. +* Case splitting on `Int.abs`? +-/ diff --git a/src/Lean/Elab/Tactic/Omega/Core.lean b/src/Lean/Elab/Tactic/Omega/Core.lean new file mode 100644 index 0000000000..6db76f4c17 --- /dev/null +++ b/src/Lean/Elab/Tactic/Omega/Core.lean @@ -0,0 +1,565 @@ +/- +Copyright (c) 2023 Lean FRO, LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Scott Morrison +-/ +import Lean.Elab.Tactic.Omega.OmegaM +import Lean.Elab.Tactic.Omega.MinNatAbs + +open Lean (HashMap HashSet) + +namespace Lean.Elab.Tactic.Omega + +initialize Lean.registerTraceClass `omega + +open Lean (Expr) +open Lean Meta Omega + +open Lean in +instance : ToExpr LinearCombo where + toExpr lc := + (Expr.const ``LinearCombo.mk []).app (toExpr lc.const) |>.app (toExpr lc.coeffs) + toTypeExpr := .const ``LinearCombo [] + +open Lean in +instance : ToExpr Constraint where + toExpr s := + (Expr.const ``Constraint.mk []).app (toExpr s.lowerBound) |>.app (toExpr s.upperBound) + toTypeExpr := .const ``Constraint [] + +/-- +A delayed proof that a constraint is satisfied at the atoms. +-/ +abbrev Proof : Type := OmegaM Expr + +/-- +Our internal representation of an argument "justifying" that a constraint holds on some coefficients. +We'll use this to construct the proof term once a contradiction is found. +-/ +inductive Justification : Constraint → Coeffs → Type + /-- + `Problem.assumptions[i]` generates a proof that `s.sat' coeffs atoms` + -/ + | assumption (s : Constraint) (x : Coeffs) (i : Nat) : Justification s x + /-- The result of `tidy` on another `Justification`. -/ + | tidy (j : Justification s c) : Justification (tidyConstraint s c) (tidyCoeffs s c) + /-- The result of `combine` on two `Justifications`. -/ + | combine {s t c} (j : Justification s c) (k : Justification t c) : Justification (s.combine t) c + /-- A linear `combo` of two `Justifications`. -/ + | combo {s t x y} (a : Int) (j : Justification s x) (b : Int) (k : Justification t y) : + Justification (Constraint.combo a s b t) (Coeffs.combo a x b y) + /-- + The justification for the constraing constructed using "balanced mod" while + eliminating an equality. + -/ + | bmod (m : Nat) (r : Int) (i : Nat) {x} (j : Justification (.exact r) x) : + Justification (.exact (Int.bmod r m)) (bmod_coeffs m i x) + +/-- Wrapping for `Justification.tidy` when `tidy?` is nonempty. -/ +nonrec def Justification.tidy? (j : Justification s c) : Option (Σ s' c', Justification s' c') := + match tidy? (s, c) with + | some _ => some ⟨_, _, tidy j⟩ + | none => none + +namespace Justification + +private def bullet (s : String) := "• " ++ s.replace "\n" "\n " + +/-- Print a `Justification` as an indented tree structure. -/ +def toString : Justification s x → String + | assumption _ _ i => s!"{x} ∈ {s}: assumption {i}" + | @tidy s' x' j => + if s == s' && x == x' then j.toString else s!"{x} ∈ {s}: tidying up:\n" ++ bullet j.toString + | combine j k => + s!"{x} ∈ {s}: combination of:\n" ++ bullet j.toString ++ "\n" ++ bullet k.toString + | combo a j b k => + s!"{x} ∈ {s}: {a} * x + {b} * y combo of:\n" ++ bullet j.toString ++ "\n" ++ bullet k.toString + | bmod m _ i j => + s!"{x} ∈ {s}: bmod with m={m} and i={i} of:\n" ++ bullet j.toString + +instance : ToString (Justification s x) where toString := toString + +open Lean + +/-- Construct the proof term associated to a `tidy` step. -/ +def tidyProof (s : Constraint) (x : Coeffs) (v : Expr) (prf : Expr) : Expr := + mkApp4 (.const ``tidy_sat []) (toExpr s) (toExpr x) v prf + +/-- Construct the proof term associated to a `combine` step. -/ +def combineProof (s t : Constraint) (x : Coeffs) (v : Expr) (ps pt : Expr) : Expr := + mkApp6 (.const ``Constraint.combine_sat' []) (toExpr s) (toExpr t) (toExpr x) v ps pt + +/-- Construct the proof term associated to a `combo` step. -/ +def comboProof (s t : Constraint) (a : Int) (x : Coeffs) (b : Int) (y : Coeffs) + (v : Expr) (px py : Expr) : Expr := + mkApp9 (.const ``combo_sat' []) (toExpr s) (toExpr t) (toExpr a) (toExpr x) (toExpr b) (toExpr y) + v px py + +/-- Construct the proof term associated to a `bmod` step. -/ +def bmodProof (m : Nat) (r : Int) (i : Nat) (x : Coeffs) (v : Expr) (w : Expr) : MetaM Expr := do + let m := toExpr m + let r := toExpr r + let i := toExpr i + let x := toExpr x + let h ← mkDecideProof (mkApp4 (.const ``LE.le [.zero]) (.const ``Nat []) (.const ``instLENat []) + (.app (.const ``Coeffs.length []) x) i) + let lhs := mkApp2 (.const ``Coeffs.get []) v i + let rhs := mkApp3 (.const ``bmod_div_term []) m x v + let p ← mkEqReflWithExpectedType lhs rhs + return mkApp8 (.const ``bmod_sat []) m r i x v h p w + +-- TODO could we increase sharing in the proof term here? + +/-- Constructs a proof that `s.sat' c v = true` -/ +def proof (v : Expr) (assumptions : Array Proof) : Justification s c → Proof + | assumption s c i => assumptions[i]! + | @tidy s c j => return tidyProof s c v (← proof v assumptions j) + | @combine s t c j k => + return combineProof s t c v (← proof v assumptions j) (← proof v assumptions k) + | @combo s t x y a j b k => + return comboProof s t a x b y v (← proof v assumptions j) (← proof v assumptions k) + | @bmod m r i x j => do bmodProof m r i x v (← proof v assumptions j) + +end Justification + +/-- A `Justification` bundled together with its parameters. -/ +structure Fact where + /-- The coefficients of a constraint. -/ + coeffs : Coeffs + /-- The constraint. -/ + constraint : Constraint + /-- The justification of a derived fact. -/ + justification : Justification constraint coeffs + +namespace Fact + +instance : ToString Fact where + toString f := toString f.justification + +/-- `tidy`, implemented on `Fact`. -/ +def tidy (f : Fact) : Fact := + match f.justification.tidy? with + | some ⟨_, _, justification⟩ => { justification } + | none => f + +/-- `combo`, implemented on `Fact`. -/ +def combo (a : Int) (f : Fact) (b : Int) (g : Fact) : Fact := + { justification := .combo a f.justification b g.justification } + +end Fact + +/-- +A `omega` problem. + +This is a hybrid structure: +it contains both `Expr` objects giving proofs of the "ground" assumptions +(or rather continuations which will produce the proofs when needed) +and internal representations of the linear constraints that we manipulate in the algorithm. + +While the algorithm is running we do not synthesize any new `Expr` proofs: proof extraction happens +only once we've found a contradiction. +-/ +structure Problem where + /-- The ground assumptions that the algorithm starts from. -/ + assumptions : Array Proof := ∅ + /-- The number of variables in the problem. -/ + numVars : Nat := 0 + /-- The current constraints, indexed by their coefficients. -/ + constraints : HashMap Coeffs Fact := ∅ + /-- + The coefficients for which `constraints` contains an exact constraint (i.e. an equality). + -/ + equalities : HashSet Coeffs := ∅ + /-- + Equations that have already been used to eliminate variables, + along with the variable which was removed, and its coefficient (either `1` or `-1`). + The earlier elements are more recent, + so if these are being reapplied it is essential to use `List.foldr`. + -/ + eliminations : List (Fact × Nat × Int) := [] + /-- Whether the problem is possible. -/ + possible : Bool := true + /-- If the problem is impossible, then `proveFalse?` will contain a proof of `False`. -/ + proveFalse? : Option Proof := none + /-- Invariant between `possible` and `proveFalse?`. -/ + proveFalse?_spec : possible || proveFalse?.isSome := by rfl + /-- + If we have found a contradiction, + `explanation?` will contain a human readable account of the deriviation. + -/ + explanation? : Thunk String := "" + +namespace Problem + +/-- Check if a problem has no constraints. -/ +def isEmpty (p : Problem) : Bool := p.constraints.isEmpty + +instance : ToString Problem where + toString p := + if p.possible then + if p.isEmpty then + "trivial" + else + "\n".intercalate <| + (p.constraints.toList.map fun ⟨coeffs, ⟨_, cst, _⟩⟩ => s!"{coeffs} ∈ {cst}") + else + "impossible" + +open Lean in +/-- +Takes a proof that `s.sat' x v` for some `s` such that `s.isImpossible`, +and constructs a proof of `False`. +-/ +def proveFalse {s x} (j : Justification s x) (assumptions : Array Proof) : Proof := do + let v := ← atomsCoeffs + let prf ← j.proof v assumptions + let x := toExpr x + let s := toExpr s + let impossible ← + mkDecideProof (← mkEq (mkApp (.const ``Constraint.isImpossible []) s) (.const ``true [])) + return mkApp5 (.const ``Constraint.not_sat'_of_isImpossible []) s impossible x v prf + +/-- +Insert a constraint into the problem, +without checking if there is already a constraint for these coefficients. +-/ +def insertConstraint (p : Problem) : Fact → Problem + | f@⟨x, s, j⟩ => + if s.isImpossible then + { p with + possible := false + proveFalse? := some (proveFalse j p.assumptions) + explanation? := Thunk.mk fun _ => j.toString + proveFalse?_spec := rfl } + else + { p with + numVars := max p.numVars x.length + constraints := p.constraints.insert x f + proveFalse?_spec := p.proveFalse?_spec + equalities := + if f.constraint.isExact then + p.equalities.insert x + else + p.equalities } + +/-- +Add a constraint into the problem, +combining it with any existing constraints for the same coefficients. +-/ +def addConstraint (p : Problem) : Fact → Problem + | f@⟨x, s, j⟩ => + if p.possible then + match p.constraints.find? x with + | none => + match s with + | .trivial => p + | _ => p.insertConstraint f + | some ⟨x', t, k⟩ => + if h : x = x' then + let r := s.combine t + if r = t then + -- No need to overwrite the existing fact + -- with the same fact with a more complicated justification + p + else + if r = s then + -- The new constraint is strictly stronger, no need to combine with the old one: + p.insertConstraint ⟨x, s, j⟩ + else + p.insertConstraint ⟨x, s.combine t, j.combine (h ▸ k)⟩ + else + p -- unreachable + else + p + +/-- +Walk through the equalities, finding either the first equality with minimal coefficient `±1`, +or otherwise the equality with minimal `(r.minNatAbs, r.maxNatAbs)` (ordered lexicographically). + +Returns the coefficients of the equality, along with the value of `minNatAbs`. + +Although we don't need to run a termination proof here, it's nevertheless important that we use this +ordering so the algorithm terminates in practice! +-/ +def selectEquality (p : Problem) : Option (Coeffs × Nat) := + p.equalities.fold (init := none) fun + | none, c => (c, c.minNatAbs) + | some (r, m), c => + if 2 ≤ m then + let m' := c.minNatAbs + if (m' < m || m' = m && c.maxNatAbs < r.maxNatAbs) then + (c, m') + else + (r, m) + else + (r, m) + +/-- +If we have already solved some equalities, apply those to some new `Fact`. +-/ +def replayEliminations (p : Problem) (f : Fact) : Fact := + p.eliminations.foldr (init := f) fun (f, i, s) g => + match Coeffs.get g.coeffs i with + | 0 => g + | y => Fact.combo (-1 * s * y) f 1 g + +/-- +Solve an "easy" equality, i.e. one with a coefficient that is `±1`. + +After solving, the variable will have been eliminated from all constraints. +-/ +def solveEasyEquality (p : Problem) (c : Coeffs) : Problem := + let i := c.findIdx? (·.natAbs = 1) |>.getD 0 -- findIdx? is always some + let sign := c.get i |> Int.sign + match p.constraints.find? c with + | some f => + let init := + { assumptions := p.assumptions + eliminations := (f, i, sign) :: p.eliminations } + p.constraints.fold (init := init) fun p' coeffs g => + match Coeffs.get coeffs i with + | 0 => + p'.addConstraint g + | ci => + let k := -1 * sign * ci + p'.addConstraint (Fact.combo k f 1 g).tidy + | _ => p -- unreachable + +open Lean in +/-- +We deal with a hard equality by introducing a new easy equality. + +After solving the easy equality, +the minimum lexicographic value of `(c.minNatAbs, c.maxNatAbs)` will have been reduced. +-/ +def dealWithHardEquality (p : Problem) (c : Coeffs) : OmegaM Problem := + match p.constraints.find? c with + | some ⟨_, ⟨some r, some r'⟩, j⟩ => do + let m := c.minNatAbs + 1 + -- We have to store the valid value of the newly introduced variable in the atoms. + let x := mkApp3 (.const ``bmod_div_term []) (toExpr m) (toExpr c) (← atomsCoeffs) + let (i, facts?) ← lookup x + if hr : r' = r then + match facts? with + | none => throwError "When solving hard equality, new atom had been seen before!" + | some facts => if ! facts.isEmpty then + throwError "When solving hard equality, there were unexpected new facts!" + return p.addConstraint { coeffs := _, constraint := _, justification := (hr ▸ j).bmod m r i } + else + throwError "Invalid constraint, expected an equation." -- unreachable + | _ => + return p -- unreachable + +/-- +Solve an equality, by deciding whether it is easy (has a `±1` coefficient) or hard, +and delegating to the appropriate function. +-/ +def solveEquality (p : Problem) (c : Coeffs) (m : Nat) : OmegaM Problem := + if m = 1 then + return p.solveEasyEquality c + else + p.dealWithHardEquality c + +/-- Recursively solve all equalities. -/ +partial def solveEqualities (p : Problem) : OmegaM Problem := + if p.possible then + match p.selectEquality with + | some (c, m) => do (← p.solveEquality c m).solveEqualities + | none => return p + else return p + +open Constraint + +open Lean in +/-- Constructing the proof term for `addInequality`. -/ +def addInequality_proof (c : Int) (x : Coeffs) (p : Proof) : Proof := do + return mkApp4 (.const ``addInequality_sat []) (toExpr c) (toExpr x) (← atomsCoeffs) (← p) + +open Lean in +/-- Constructing the proof term for `addEquality`. -/ +def addEquality_proof (c : Int) (x : Coeffs) (p : Proof) : Proof := do + return mkApp4 (.const ``addEquality_sat []) (toExpr c) (toExpr x) (← atomsCoeffs) (← p) + +/-- +Helper function for adding an inequality of the form `const + Coeffs.dot coeffs atoms ≥ 0` +to a `Problem`. + +(This is only used while initializing a `Problem`. During elimination we use `addConstraint`.) +-/ +-- We are given `prf? : const + Coeffs.dot coeffs atoms ≥ 0`, +-- and need to transform this to `Coeffs.dot coeffs atoms ≥ -const`. +def addInequality (p : Problem) (const : Int) (coeffs : Coeffs) (prf? : Option Proof) : Problem := + let prf := prf?.getD (do mkSorry (← mkFreshExprMVar none) false) + let i := p.assumptions.size + let p' := { p with assumptions := p.assumptions.push (addInequality_proof const coeffs prf) } + let f : Fact := + { coeffs + constraint := { lowerBound := some (-const), upperBound := none } + justification := .assumption _ _ i } + let f := p.replayEliminations f + let f := f.tidy + p'.addConstraint f + +/-- +Helper function for adding an equality of the form `const + Coeffs.dot coeffs atoms = 0` +to a `Problem`. + +(This is only used while initializing a `Problem`. During elimination we use `addConstraint`.) +-/ +def addEquality (p : Problem) (const : Int) (coeffs : Coeffs) (prf? : Option Proof) : Problem := + let prf := prf?.getD (do mkSorry (← mkFreshExprMVar none) false) + let i := p.assumptions.size + let p' := { p with assumptions := p.assumptions.push (addEquality_proof const coeffs prf) } + let f : Fact := + { coeffs + constraint := { lowerBound := some (-const), upperBound := some (-const) } + justification := .assumption _ _ i } + let f := p.replayEliminations f + let f := f.tidy + p'.addConstraint f + +/-- Folding `addInequality` over a list. -/ +def addInequalities (p : Problem) (ineqs : List (Int × Coeffs × Option Proof)) : Problem := + ineqs.foldl (init := p) fun p ⟨const, coeffs, prf?⟩ => p.addInequality const coeffs prf? + +/-- Folding `addEquality` over a list. -/ +def addEqualities (p : Problem) (eqs : List (Int × Coeffs × Option Proof)) : Problem := + eqs.foldl (init := p) fun p ⟨const, coeffs, prf?⟩ => p.addEquality const coeffs prf? + +/-- Representation of the data required to run Fourier-Motzkin elimination on a variable. -/ +structure FourierMotzkinData where + /-- Which variable is being eliminated. -/ + var : Nat + /-- The "irrelevant" facts which do not involve the target variable. -/ + irrelevant : List Fact := [] + /-- + The facts which give a lower bound on the target variable, + and the coefficient of the target variable in each. + -/ + lowerBounds : List (Fact × Int) := [] + /-- + The facts which give an upper bound on the target variable, + and the coefficient of the target variable in each. + -/ + upperBounds : List (Fact × Int) := [] + /-- + Whether the elimination would be exact, because all of the lower bound coefficients are `±1`. + -/ + lowerExact : Bool := true + /-- + Whether the elimination would be exact, because all of the upper bound coefficients are `±1`. + -/ + upperExact : Bool := true +deriving Inhabited + +instance : ToString FourierMotzkinData where + toString d := + let irrelevant := d.irrelevant.map fun ⟨x, s, _⟩ => s!"{x} ∈ {s}" + let lowerBounds := d.lowerBounds.map fun ⟨⟨x, s, _⟩, _⟩ => s!"{x} ∈ {s}" + let upperBounds := d.upperBounds.map fun ⟨⟨x, s, _⟩, _⟩ => s!"{x} ∈ {s}" + s!"Fourier-Motzkin elimination data for variable {d.var}\n" + ++ s!"• irrelevant: {irrelevant}\n" + ++ s!"• lowerBounds: {lowerBounds}\n" + ++ s!"• upperBounds: {upperBounds}" + +/-- Is a Fourier-Motzkin elimination empty (i.e. there are no relevant constraints). -/ +def FourierMotzkinData.isEmpty (d : FourierMotzkinData) : Bool := + d.lowerBounds.isEmpty && d.upperBounds.isEmpty +/-- The number of new constraints that would be introduced by Fourier-Motzkin elimination. -/ +def FourierMotzkinData.size (d : FourierMotzkinData) : Nat := + d.lowerBounds.length * d.upperBounds.length +/-- Is the Fourier-Motzkin elimination known to be exact? -/ +def FourierMotzkinData.exact (d : FourierMotzkinData) : Bool := d.lowerExact || d.upperExact + +/-- Prepare the Fourier-Motzkin elimination data for each variable. -/ +-- TODO we could short-circuit here, if we find one with `size = 0`. +def fourierMotzkinData (p : Problem) : Array FourierMotzkinData := Id.run do + let n := p.numVars + let mut data : Array FourierMotzkinData := + (List.range p.numVars).foldl (fun a i => a.push { var := i}) #[] + for (_, f@⟨xs, s, _⟩) in p.constraints.toList do -- We could make a forIn instance for HashMap + for i in [0:n] do + let x := Coeffs.get xs i + data := data.modify i fun d => + if x = 0 then + { d with irrelevant := f :: d.irrelevant } + else Id.run do + let s' := s.scale x + let mut d' := d + if s'.lowerBound.isSome then + d' := { d' with + lowerBounds := (f, x) :: d'.lowerBounds + lowerExact := d'.lowerExact && x.natAbs = 1 } + if s'.upperBound.isSome then + d' := { d' with + upperBounds := (f, x) :: d'.upperBounds + upperExact := d'.upperExact && x.natAbs = 1 } + return d' + return data + +/-- +Decides which variable to run Fourier-Motzkin elimination on, and returns the associated data. + +We prefer eliminations which introduce no new inequalities, or otherwise exact eliminations, +and break ties by the number of new inequalities introduced. +-/ +def fourierMotzkinSelect (data : Array FourierMotzkinData) : FourierMotzkinData := Id.run do + let data := data.filter fun d => ¬ d.isEmpty + let mut bestIdx := 0 + let mut bestSize := data[0]!.size + let mut bestExact := data[0]!.exact + if bestSize = 0 then return data[0]! + for i in [1:data.size] do + let exact := data[i]!.exact + let size := data[i]!.size + if size = 0 || !bestExact && exact || size < bestSize then + if size = 0 then return data[i]! + bestIdx := i + bestExact := exact + bestSize := size + return data[bestIdx]! + +/-- +Run Fourier-Motzkin elimination on one variable. +-/ +def fourierMotzkin (p : Problem) : Problem := Id.run do + let data := p.fourierMotzkinData + -- Now perform the elimination. + let ⟨_, irrelevant, lower, upper, _, _⟩ := fourierMotzkinSelect data + let mut r : Problem := { assumptions := p.assumptions, eliminations := p.eliminations } + for f in irrelevant do + r := r.insertConstraint f + for ⟨f, b⟩ in lower do + for ⟨g, a⟩ in upper do + r := r.addConstraint (Fact.combo a f (-b) g).tidy + return r + +mutual + +/-- +Run the `omega` algorithm (for now without dark and grey shadows!) on a problem. +-/ +partial def runOmega (p : Problem) : OmegaM Problem := do + trace[omega] "Running omega on:\n{p}" + if p.possible then + let p' ← p.solveEqualities + elimination p' + else + return p + +/-- As for `runOmega`, but assuming the first round of solving equalities has already happened. -/ +partial def elimination (p : Problem) : OmegaM Problem := + if p.possible then + if p.isEmpty then + return p + else do + trace[omega] "Running Fourier-Motzkin elimination on:\n{p}" + runOmega p.fourierMotzkin + else + return p + +end + +end Problem + +end Lean.Elab.Tactic.Omega diff --git a/src/Lean/Elab/Tactic/Omega/Frontend.lean b/src/Lean/Elab/Tactic/Omega/Frontend.lean new file mode 100644 index 0000000000..04d70e82ae --- /dev/null +++ b/src/Lean/Elab/Tactic/Omega/Frontend.lean @@ -0,0 +1,542 @@ +/- +Copyright (c) 2023 Lean FRO, LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Scott Morrison +-/ +import Lean.Elab.Tactic.Omega.Core +import Lean.Elab.Tactic.FalseOrByContra +import Lean.Meta.Tactic.Cases +import Lean.Elab.Tactic.Config + +/-! +# Frontend to the `omega` tactic. + +See `Lean.Elab.Tactic.Omega` for an overview of the tactic. +-/ + +open Lean Meta Omega + +namespace Lean.Elab.Tactic.Omega + +/-- +Allow elaboration of `OmegaConfig` arguments to tactics. +-/ +declare_config_elab elabOmegaConfig Lean.Meta.Omega.OmegaConfig + + +/-- +A partially processed `omega` context. + +We have: +* a `Problem` representing the integer linear constraints extracted so far, and their proofs +* the unprocessed `facts : List Expr` taken from the local context, +* the unprocessed `disjunctions : List Expr`, + which will only be split one at a time if we can't otherwise find a contradiction. + +We begin with `facts := ← getLocalHyps` and `problem := .trivial`, +and progressively process the facts. + +As we process the facts, we may generate additional facts +(e.g. about coercions and integer divisions). +To avoid duplicates, we maintain a `HashSet` of previously processed facts. +-/ +structure MetaProblem where + /-- An integer linear arithmetic problem. -/ + problem : Problem := {} + /-- Pending facts which have not been processed yet. -/ + facts : List Expr := [] + /-- + Pending disjunctions, which we will case split one at a time if we can't get a contradiction. + -/ + disjunctions : List Expr := [] + /-- Facts which have already been processed; we keep these to avoid duplicates. -/ + processedFacts : HashSet Expr := ∅ + +/-- Construct the `rfl` proof that `lc.eval atoms = e`. -/ +def mkEvalRflProof (e : Expr) (lc : LinearCombo) : OmegaM Expr := do + mkEqReflWithExpectedType e (mkApp2 (.const ``LinearCombo.eval []) (toExpr lc) (← atomsCoeffs)) + +/-- If `e : Expr` is the `n`-th atom, construct the proof that +`e = (coordinate n).eval atoms`. -/ +def mkCoordinateEvalAtomsEq (e : Expr) (n : Nat) : OmegaM Expr := do + if n < 10 then + let atoms := (← getThe State).atoms + let tail ← mkListLit (.const ``Int []) atoms[n+1:].toArray.toList + let lem := .str ``LinearCombo s!"coordinate_eval_{n}" + mkEqSymm (mkAppN (.const lem []) (atoms[:n+1].toArray.push tail)) + else + let atoms ← atomsCoeffs + let n := toExpr n + -- Construct the `rfl` proof that `e = (atoms.get? n).getD 0` + let eq ← mkEqReflWithExpectedType e (mkApp2 (.const ``Coeffs.get []) atoms n) + mkEqTrans eq (← mkEqSymm (mkApp2 (.const ``LinearCombo.coordinate_eval []) n atoms)) + +/-- Construct the linear combination (and its associated proof and new facts) for an atom. -/ +def mkAtomLinearCombo (e : Expr) : OmegaM (LinearCombo × OmegaM Expr × HashSet Expr) := do + let (n, facts) ← lookup e + return ⟨LinearCombo.coordinate n, mkCoordinateEvalAtomsEq e n, facts.getD ∅⟩ + +-- This has been PR'd as +-- https://github.com/leanprover/lean4/pull/2900 +-- and can be removed when that is merged. +@[inherit_doc mkAppN] +local macro_rules + | `(mkAppN $f #[$xs,*]) => (xs.getElems.foldlM (fun x e => `(Expr.app $x $e)) f : MacroM Term) + +mutual + +/-- +Wrapper for `asLinearComboImpl`, +using a cache for previously visited expressions. + +Gives a small (10%) speedup in testing. +I tried using a pointer based cache, +but there was never enough subexpression sharing to make it effective. +-/ +partial def asLinearCombo (e : Expr) : OmegaM (LinearCombo × OmegaM Expr × HashSet Expr) := do + let cache ← get + match cache.find? e with + | some (lc, prf) => + trace[omega] "Found in cache: {e}" + return (lc, prf, ∅) + | none => + let r ← asLinearComboImpl e + modifyThe Cache fun cache => (cache.insert e (r.1, r.2.1.run' cache)) + pure r + +/-- +Translates an expression into a `LinearCombo`. +Also returns: +* a proof that this linear combo evaluated at the atoms is equal to the original expression +* a list of new facts which should be recorded: + * 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 + 1) * a` + * 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` + +We also transform the expression as we descend into it: +* pushing coercions: `↑(x + y)`, `↑(x * y)`, `↑(x / k)`, `↑(x % k)`, `↑k` +* unfolding `emod`: `x % k` → `x - x / k` +-/ +partial def asLinearComboImpl (e : Expr) : OmegaM (LinearCombo × OmegaM Expr × HashSet Expr) := do + trace[omega] "processing {e}" + match e.int? with + | some i => + let lc := {const := i} + return ⟨lc, mkEvalRflProof e lc, ∅⟩ + | none => + if e.isFVar then + if let some v ← e.fvarId!.getValue? then + rewrite e (← mkEqReflWithExpectedType e v) + else + mkAtomLinearCombo e + else match e.getAppFnArgs with + | (``HAdd.hAdd, #[_, _, _, _, e₁, e₂]) => do + let (l₁, prf₁, facts₁) ← asLinearCombo e₁ + let (l₂, prf₂, facts₂) ← asLinearCombo e₂ + let prf : OmegaM Expr := do + let add_eval := + mkApp3 (.const ``LinearCombo.add_eval []) (toExpr l₁) (toExpr l₂) (← atomsCoeffs) + mkEqTrans + (← mkAppM ``Int.add_congr #[← prf₁, ← prf₂]) + (← mkEqSymm add_eval) + pure (l₁ + l₂, prf, facts₁.merge facts₂) + | (``HSub.hSub, #[_, _, _, _, e₁, e₂]) => do + let (l₁, prf₁, facts₁) ← asLinearCombo e₁ + let (l₂, prf₂, facts₂) ← asLinearCombo e₂ + let prf : OmegaM Expr := do + let sub_eval := + mkApp3 (.const ``LinearCombo.sub_eval []) (toExpr l₁) (toExpr l₂) (← atomsCoeffs) + mkEqTrans + (← mkAppM ``Int.sub_congr #[← prf₁, ← prf₂]) + (← mkEqSymm sub_eval) + pure (l₁ - l₂, prf, facts₁.merge facts₂) + | (``Neg.neg, #[_, _, e']) => do + let (l, prf, facts) ← asLinearCombo e' + let prf' : OmegaM Expr := do + let neg_eval := mkApp2 (.const ``LinearCombo.neg_eval []) (toExpr l) (← atomsCoeffs) + mkEqTrans + (← mkAppM ``Int.neg_congr #[← prf]) + (← mkEqSymm neg_eval) + pure (-l, prf', facts) + | (``HMul.hMul, #[_, _, _, _, x, y]) => + -- If we decide not to expand out the multiplication, + -- we have to revert the `OmegaM` state so that any new facts about the factors + -- can still be reported when they are visited elsewhere. + let r? ← commitWhen do + let (xl, xprf, xfacts) ← asLinearCombo x + let (yl, yprf, yfacts) ← asLinearCombo y + if xl.coeffs.isZero ∨ yl.coeffs.isZero then + let prf : OmegaM Expr := do + let h ← mkDecideProof (mkApp2 (.const ``Or []) + (.app (.const ``Coeffs.isZero []) (toExpr xl.coeffs)) + (.app (.const ``Coeffs.isZero []) (toExpr yl.coeffs))) + let mul_eval := + mkApp4 (.const ``LinearCombo.mul_eval []) (toExpr xl) (toExpr yl) (← atomsCoeffs) h + mkEqTrans + (← mkAppM ``Int.mul_congr #[← xprf, ← yprf]) + (← mkEqSymm mul_eval) + pure (some (LinearCombo.mul xl yl, prf, xfacts.merge yfacts), true) + else + pure (none, false) + match r? with + | some r => pure r + | none => mkAtomLinearCombo e + | (``HMod.hMod, #[_, _, _, _, n, k]) => + match natCast? k with + | some _ => rewrite e (mkApp2 (.const ``Int.emod_def []) n k) + | none => mkAtomLinearCombo e + | (``HDiv.hDiv, #[_, _, _, _, x, z]) => + match intCast? z with + | some 0 => rewrite e (mkApp (.const ``Int.ediv_zero []) x) + | some i => + if i < 0 then + rewrite e (mkApp2 (.const ``Int.ediv_neg []) x (toExpr (-i))) + else + mkAtomLinearCombo e + | _ => mkAtomLinearCombo e + | (``Min.min, #[_, _, a, b]) => + if (← cfg).splitMinMax then + rewrite e (mkApp2 (.const ``Int.min_def []) a b) + else + mkAtomLinearCombo e + | (``Max.max, #[_, _, a, b]) => + if (← cfg).splitMinMax then + rewrite e (mkApp2 (.const ``Int.max_def []) a b) + else + mkAtomLinearCombo e + | (``Nat.cast, #[.const ``Int [], i, n]) => + match n with + | .fvar h => + if let some v ← h.getValue? then + rewrite e (← mkEqReflWithExpectedType e + (mkApp3 (.const ``Nat.cast [0]) (.const ``Int []) i v)) + else + mkAtomLinearCombo e + | _ => match n.getAppFnArgs with + | (``Nat.succ, #[n]) => rewrite e (.app (.const ``Int.ofNat_succ []) n) + | (``HAdd.hAdd, #[_, _, _, _, a, b]) => rewrite e (mkApp2 (.const ``Int.ofNat_add []) a b) + | (``HMul.hMul, #[_, _, _, _, a, b]) => rewrite e (mkApp2 (.const ``Int.ofNat_mul []) a b) + | (``HDiv.hDiv, #[_, _, _, _, a, b]) => rewrite e (mkApp2 (.const ``Int.ofNat_ediv []) a b) + | (``OfNat.ofNat, #[_, n, _]) => rewrite e (.app (.const ``Int.natCast_ofNat []) n) + | (``HMod.hMod, #[_, _, _, _, a, b]) => rewrite e (mkApp2 (.const ``Int.ofNat_emod []) a b) + | (``HSub.hSub, #[_, _, _, _, mkAppN (.const ``HSub.hSub _) #[_, _, _, _, a, b], c]) => + rewrite e (mkApp3 (.const ``Int.ofNat_sub_sub []) a b c) + | (``Prod.fst, #[_, β, p]) => match p with + | .app (.app (.app (.app (.const ``Prod.mk [0, v]) _) _) x) y => + rewrite e (mkApp3 (.const ``Int.ofNat_fst_mk [v]) β x y) + | _ => mkAtomLinearCombo e + | (``Prod.snd, #[α, _, p]) => match p with + | .app (.app (.app (.app (.const ``Prod.mk [u, 0]) _) _) x) y => + rewrite e (mkApp3 (.const ``Int.ofNat_snd_mk [u]) α x y) + | _ => mkAtomLinearCombo e + | (``Min.min, #[_, _, a, b]) => rewrite e (mkApp2 (.const ``Int.ofNat_min []) a b) + | (``Max.max, #[_, _, a, b]) => rewrite e (mkApp2 (.const ``Int.ofNat_max []) a b) + | (``Int.natAbs, #[n]) => + if (← cfg).splitNatAbs then + rewrite e (mkApp (.const ``Int.ofNat_natAbs []) n) + else + mkAtomLinearCombo e + | _ => mkAtomLinearCombo e + | (``Prod.fst, #[α, β, p]) => match p with + | .app (.app (.app (.app (.const ``Prod.mk [u, v]) _) _) x) y => + rewrite e (mkApp4 (.const ``Prod.fst_mk [u, v]) α x β y) + | _ => mkAtomLinearCombo e + | (``Prod.snd, #[α, β, p]) => match p with + | .app (.app (.app (.app (.const ``Prod.mk [u, v]) _) _) x) y => + rewrite e (mkApp4 (.const ``Prod.snd_mk [u, v]) α x β y) + | _ => mkAtomLinearCombo e + | _ => mkAtomLinearCombo e +where + /-- + Apply a rewrite rule to an expression, and interpret the result as a `LinearCombo`. + (We're not rewriting any subexpressions here, just the top level, for efficiency.) + -/ + rewrite (lhs rw : Expr) : OmegaM (LinearCombo × OmegaM Expr × HashSet Expr) := do + trace[omega] "rewriting {lhs} via {rw} : {← inferType rw}" + match (← inferType rw).eq? with + | some (_, _lhs', rhs) => + let (lc, prf, facts) ← asLinearCombo rhs + let prf' : OmegaM Expr := do mkEqTrans rw (← prf) + pure (lc, prf', facts) + | none => panic! "Invalid rewrite rule in 'asLinearCombo'" + +end +namespace MetaProblem + +/-- The trivial `MetaProblem`, with no facts to processs and a trivial `Problem`. -/ +def trivial : MetaProblem where + problem := {} + +instance : Inhabited MetaProblem := ⟨trivial⟩ + +/-- +Add an integer equality to the `Problem`. + +We solve equalities as they are discovered, as this often results in an earlier contradiction. +-/ +def addIntEquality (p : MetaProblem) (h x : Expr) : OmegaM MetaProblem := do + let (lc, prf, facts) ← asLinearCombo x + let newFacts : HashSet Expr := facts.fold (init := ∅) fun s e => + if p.processedFacts.contains e then s else s.insert e + trace[omega] "Adding proof of {lc} = 0" + pure <| + { p with + facts := newFacts.toList ++ p.facts + problem := ← (p.problem.addEquality lc.const lc.coeffs + (some do mkEqTrans (← mkEqSymm (← prf)) h)) |>.solveEqualities } + +/-- +Add an integer inequality to the `Problem`. + +We solve equalities as they are discovered, as this often results in an earlier contradiction. +-/ +def addIntInequality (p : MetaProblem) (h y : Expr) : OmegaM MetaProblem := do + let (lc, prf, facts) ← asLinearCombo y + let newFacts : HashSet Expr := facts.fold (init := ∅) fun s e => + if p.processedFacts.contains e then s else s.insert e + trace[omega] "Adding proof of {lc} ≥ 0" + pure <| + { p with + facts := newFacts.toList ++ p.facts + problem := ← (p.problem.addInequality lc.const lc.coeffs + (some do mkAppM ``le_of_le_of_eq #[h, (← prf)])) |>.solveEqualities } + +/-- Given a fact `h` with type `¬ P`, return a more useful fact obtained by pushing the negation. -/ +def pushNot (h P : Expr) : MetaM (Option Expr) := do + let P ← whnfR P + match P with + | .forallE _ t b _ => + if (← isProp t) && (← isProp b) then + return some (mkApp4 (.const ``Decidable.and_not_of_not_imp []) t b + (.app (.const ``Classical.propDecidable []) t) h) + else + return none + | .app _ _ => + match P.getAppFnArgs with + | (``LT.lt, #[.const ``Int [], _, x, y]) => + return some (mkApp3 (.const ``Int.le_of_not_lt []) x y h) + | (``LE.le, #[.const ``Int [], _, x, y]) => + return some (mkApp3 (.const ``Int.lt_of_not_le []) x y h) + | (``LT.lt, #[.const ``Nat [], _, x, y]) => + return some (mkApp3 (.const ``Nat.le_of_not_lt []) x y h) + | (``LE.le, #[.const ``Nat [], _, x, y]) => + return some (mkApp3 (.const ``Nat.lt_of_not_le []) x y h) + | (``Eq, #[.const ``Nat [], x, y]) => + return some (mkApp3 (.const ``Nat.lt_or_gt_of_ne []) x y h) + | (``Eq, #[.const ``Int [], x, y]) => + return some (mkApp3 (.const ``Int.lt_or_gt_of_ne []) x y h) + | (``Prod.Lex, _) => return some (← mkAppM ``Prod.of_not_lex #[h]) + | (``Dvd.dvd, #[.const ``Nat [], _, k, x]) => + return some (mkApp3 (.const ``Nat.emod_pos_of_not_dvd []) k x h) + | (``Dvd.dvd, #[.const ``Int [], _, k, x]) => + -- This introduces a disjunction that could be avoided by checking `k ≠ 0`. + return some (mkApp3 (.const ``Int.emod_pos_of_not_dvd []) k x h) + | (``Or, #[P₁, P₂]) => return some (mkApp3 (.const ``and_not_not_of_not_or []) P₁ P₂ h) + | (``And, #[P₁, P₂]) => + return some (mkApp5 (.const ``Decidable.or_not_not_of_not_and []) P₁ P₂ + (.app (.const ``Classical.propDecidable []) P₁) + (.app (.const ``Classical.propDecidable []) P₂) h) + | (``Not, #[P']) => + return some (mkApp3 (.const ``Decidable.of_not_not []) P' + (.app (.const ``Classical.propDecidable []) P') h) + | (``Iff, #[P₁, P₂]) => + return some (mkApp5 (.const ``Decidable.and_not_or_not_and_of_not_iff []) P₁ P₂ + (.app (.const ``Classical.propDecidable []) P₁) + (.app (.const ``Classical.propDecidable []) P₂) h) + | _ => return none + | _ => return none + +/-- +Parse an `Expr` and extract facts, also returning the number of new facts found. +-/ +partial def addFact (p : MetaProblem) (h : Expr) : OmegaM (MetaProblem × Nat) := do + if ! p.problem.possible then + return (p, 0) + else + let t ← instantiateMVars (← whnfR (← inferType h)) + trace[omega] "adding fact: {t}" + match t with + | .forallE _ x y _ => + if (← isProp x) && (← isProp y) then + p.addFact (mkApp4 (.const ``Decidable.not_or_of_imp []) x y + (.app (.const ``Classical.propDecidable []) x) h) + else + return (p, 0) + | .app _ _ => + match t.getAppFnArgs with + | (``Eq, #[.const ``Int [], x, y]) => + match y.int? with + | some 0 => pure (← p.addIntEquality h x, 1) + | _ => p.addFact (mkApp3 (.const ``Int.sub_eq_zero_of_eq []) x y h) + | (``LE.le, #[.const ``Int [], _, x, y]) => + match x.int? with + | some 0 => pure (← p.addIntInequality h y, 1) + | _ => p.addFact (mkApp3 (.const ``Int.sub_nonneg_of_le []) y x h) + | (``LT.lt, #[.const ``Int [], _, x, y]) => + p.addFact (mkApp3 (.const ``Int.add_one_le_of_lt []) x y h) + | (``GT.gt, #[.const ``Int [], _, x, y]) => + p.addFact (mkApp3 (.const ``Int.lt_of_gt []) x y h) + | (``GE.ge, #[.const ``Int [], _, x, y]) => + p.addFact (mkApp3 (.const ``Int.le_of_ge []) x y h) + | (``GT.gt, #[.const ``Nat [], _, x, y]) => + p.addFact (mkApp3 (.const ``Nat.lt_of_gt []) x y h) + | (``GE.ge, #[.const ``Nat [], _, x, y]) => + p.addFact (mkApp3 (.const ``Nat.le_of_ge []) x y h) + | (``Ne, #[.const ``Nat [], x, y]) => + p.addFact (mkApp3 (.const ``Nat.lt_or_gt_of_ne []) x y h) + | (``Not, #[P]) => match ← pushNot h P with + | none => return (p, 0) + | some h' => p.addFact h' + | (``Eq, #[.const ``Nat [], x, y]) => + p.addFact (mkApp3 (.const ``Int.ofNat_congr []) x y h) + | (``LT.lt, #[.const ``Nat [], _, x, y]) => + p.addFact (mkApp3 (.const ``Int.ofNat_lt_of_lt []) x y h) + | (``LE.le, #[.const ``Nat [], _, x, y]) => + p.addFact (mkApp3 (.const ``Int.ofNat_le_of_le []) x y h) + | (``Ne, #[.const ``Int [], x, y]) => + p.addFact (mkApp3 (.const ``Int.lt_or_gt_of_ne []) x y h) + | (``Prod.Lex, _) => p.addFact (← mkAppM ``Prod.of_lex #[h]) + | (``Dvd.dvd, #[.const ``Nat [], _, k, x]) => + p.addFact (mkApp3 (.const ``Nat.mod_eq_zero_of_dvd []) k x h) + | (``Dvd.dvd, #[.const ``Int [], _, k, x]) => + p.addFact (mkApp3 (.const ``Int.emod_eq_zero_of_dvd []) k x h) + | (``And, #[t₁, t₂]) => do + let (p₁, n₁) ← p.addFact (mkApp3 (.const ``And.left []) t₁ t₂ h) + let (p₂, n₂) ← p₁.addFact (mkApp3 (.const ``And.right []) t₁ t₂ h) + return (p₂, n₁ + n₂) + | (``Exists, #[α, P]) => + p.addFact (mkApp3 (.const ``Exists.choose_spec [← getLevel α]) α P h) + | (``Subtype, #[α, P]) => + p.addFact (mkApp3 (.const ``Subtype.property [← getLevel α]) α P h) + | (``Iff, #[P₁, P₂]) => + p.addFact (mkApp4 (.const ``Decidable.and_or_not_and_not_of_iff []) + P₁ P₂ (.app (.const ``Classical.propDecidable []) P₂) h) + | (``Or, #[_, _]) => + if (← cfg).splitDisjunctions then + return ({ p with disjunctions := p.disjunctions.insert h }, 1) + else + return (p, 0) + | _ => pure (p, 0) + | _ => pure (p, 0) + +/-- +Process all the facts in a `MetaProblem`, returning the new problem, and the number of new facts. + +This is partial because new facts may be generated along the way. +-/ +partial def processFacts (p : MetaProblem) : OmegaM (MetaProblem × Nat) := do + match p.facts with + | [] => pure (p, 0) + | h :: t => + if p.processedFacts.contains h then + processFacts { p with facts := t } + else + let (p₁, n₁) ← MetaProblem.addFact { p with + facts := t + processedFacts := p.processedFacts.insert h } h + let (p₂, n₂) ← p₁.processFacts + return (p₂, n₁ + n₂) + +end MetaProblem + +/-- +Given `p : P ∨ Q` (or any inductive type with two one-argument constructors), +split the goal into two subgoals: +one containing the hypothesis `h : P` and another containing `h : Q`. +-/ +def cases₂ (mvarId : MVarId) (p : Expr) (hName : Name := `h) : + MetaM ((MVarId × FVarId) × (MVarId × FVarId)) := do + let mvarId ← mvarId.assert `hByCases (← inferType p) p + let (fvarId, mvarId) ← mvarId.intro1 + let #[s₁, s₂] ← mvarId.cases fvarId #[{ varNames := [hName] }, { varNames := [hName] }] | + throwError "'cases' tactic failed, unexpected number of subgoals" + let #[Expr.fvar f₁ ..] ← pure s₁.fields + | throwError "'cases' tactic failed, unexpected new hypothesis" + let #[Expr.fvar f₂ ..] ← pure s₂.fields + | throwError "'cases' tactic failed, unexpected new hypothesis" + return ((s₁.mvarId, f₁), (s₂.mvarId, f₂)) + + +mutual + +/-- +Split a disjunction in a `MetaProblem`, and if we find a new usable fact +call `omegaImpl` in both branches. +-/ +partial def splitDisjunction (m : MetaProblem) (g : MVarId) : OmegaM Unit := g.withContext do + match m.disjunctions with + | [] => throwError "omega did not find a contradiction:\n{m.problem}" + | h :: t => + trace[omega] "Case splitting on {← inferType h}" + let ctx ← getMCtx + let (⟨g₁, h₁⟩, ⟨g₂, h₂⟩) ← cases₂ g h + trace[omega] "Adding facts:\n{← g₁.withContext <| inferType (.fvar h₁)}" + let m₁ := { m with facts := [.fvar h₁], disjunctions := t } + let r ← withoutModifyingState do + let (m₁, n) ← g₁.withContext m₁.processFacts + if 0 < n then + omegaImpl m₁ g₁ + pure true + else + pure false + if r then + trace[omega] "Adding facts:\n{← g₂.withContext <| inferType (.fvar h₂)}" + let m₂ := { m with facts := [.fvar h₂], disjunctions := t } + omegaImpl m₂ g₂ + else + trace[omega] "No new facts found." + setMCtx ctx + splitDisjunction { m with disjunctions := t } g + +/-- Implementation of the `omega` algorithm, and handling disjunctions. -/ +partial def omegaImpl (m : MetaProblem) (g : MVarId) : OmegaM Unit := g.withContext do + let (m, _) ← m.processFacts + guard m.facts.isEmpty + let p := m.problem + trace[omega] "Extracted linear arithmetic problem:\nAtoms: {← atomsList}\n{p}" + let p' ← if p.possible then p.elimination else pure p + trace[omega] "After elimination:\nAtoms: {← atomsList}\n{p'}" + match p'.possible, p'.proveFalse?, p'.proveFalse?_spec with + | true, _, _ => + splitDisjunction m g + | false, .some prf, _ => + trace[omega] "Justification:\n{p'.explanation?.get}" + let prf ← instantiateMVars (← prf) + trace[omega] "omega found a contradiction, proving {← inferType prf}" + trace[omega] "{prf}" + g.assign prf + +end + +/-- +Given a collection of facts, try prove `False` using the omega algorithm, +and close the goal using that. +-/ +def omega (facts : List Expr) (g : MVarId) (cfg : OmegaConfig := {}) : MetaM Unit := + OmegaM.run (omegaImpl { facts } g) cfg + +open Lean Elab Tactic Parser.Tactic + +/-- The `omega` tactic, for resolving integer and natural linear arithmetic problems. -/ +def omegaTactic (cfg : OmegaConfig) : TacticM Unit := do + liftMetaFinishingTactic fun g => do + let g ← g.falseOrByContra + (useClassical := false) -- because all the hypotheses we can make use of are decidable + g.withContext do + let hyps := (← getLocalHyps).toList + trace[omega] "analyzing {hyps.length} hypotheses:\n{← hyps.mapM inferType}" + omega hyps g cfg + +/-- The `omega` tactic, for resolving integer and natural linear arithmetic problems. This +`TacticM Unit` frontend with default configuration can be used as an Aesop rule, for example via +the tactic call `aesop (add 50% tactic Std.Tactic.Omega.omegaDefault)`. -/ +def omegaDefault : TacticM Unit := omegaTactic {} + +@[builtin_tactic Lean.Parser.Tactic.omega] +def evalOmega : Tactic := fun + | `(tactic| omega $[$cfg]?) => do + let cfg ← elabOmegaConfig (mkOptionalNode cfg) + omegaTactic cfg + | _ => throwUnsupportedSyntax diff --git a/src/Lean/Elab/Tactic/Omega/MinNatAbs.lean b/src/Lean/Elab/Tactic/Omega/MinNatAbs.lean new file mode 100644 index 0000000000..c569d7b564 --- /dev/null +++ b/src/Lean/Elab/Tactic/Omega/MinNatAbs.lean @@ -0,0 +1,139 @@ +/- +Copyright (c) 2023 Lean FRO, LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Scott Morrison +-/ + +/-! +# `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). + +-/ + + +namespace List + +/-- +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. +-/ +def nonzeroMinimum (xs : List Nat) : Nat := xs.filter (· ≠ 0) |>.minimum? |>.getD 0 + +-- A specialization of `minimum?_eq_some_iff` to Nat. +theorem minimum?_eq_some_iff' {xs : List Nat} : + xs.minimum? = some a ↔ (a ∈ xs ∧ ∀ b ∈ xs, a ≤ b) := + minimum?_eq_some_iff + (le_refl := Nat.le_refl) + (min_eq_or := fun _ _ => Nat.min_def .. ▸ by split <;> simp) + (le_min_iff := fun _ _ _ => Nat.le_min) + +open Classical in +@[simp] theorem nonzeroMinimum_eq_zero_iff {xs : List Nat} : + xs.nonzeroMinimum = 0 ↔ ∀ x ∈ xs, x = 0 := by + simp [nonzeroMinimum, Option.getD_eq_iff, minimum?_eq_none_iff, minimum?_eq_some_iff', + filter_eq_nil, mem_filter] + +theorem nonzeroMinimum_mem {xs : List Nat} (w : xs.nonzeroMinimum ≠ 0) : + xs.nonzeroMinimum ∈ xs := by + dsimp [nonzeroMinimum] at * + generalize h : (xs.filter (· ≠ 0) |>.minimum?) = m at * + match m, w with + | some (m+1), _ => simp_all [minimum?_eq_some_iff', mem_filter] + +theorem nonzeroMinimum_pos {xs : List Nat} (m : a ∈ xs) (h : a ≠ 0) : 0 < xs.nonzeroMinimum := + Nat.pos_iff_ne_zero.mpr fun w => h (nonzeroMinimum_eq_zero_iff.mp w _ m) + +theorem nonzeroMinimum_le {xs : List Nat} (m : a ∈ xs) (h : a ≠ 0) : xs.nonzeroMinimum ≤ a := by + have : (xs.filter (· ≠ 0) |>.minimum?) = some xs.nonzeroMinimum := by + have w := nonzeroMinimum_pos m h + dsimp [nonzeroMinimum] at * + generalize h : (xs.filter (· ≠ 0) |>.minimum?) = m? at * + match m?, w with + | some m?, _ => rfl + rw [minimum?_eq_some_iff'] at this + apply this.2 + simp [List.mem_filter] + exact ⟨m, h⟩ + +theorem nonzeroMinimum_eq_nonzero_iff {xs : List Nat} {y : Nat} (h : y ≠ 0) : + xs.nonzeroMinimum = y ↔ y ∈ xs ∧ (∀ x ∈ xs, y ≤ x ∨ x = 0) := by + constructor + · rintro rfl + constructor + exact nonzeroMinimum_mem h + intro y m + by_cases w : y = 0 + · right; exact w + · left; apply nonzeroMinimum_le m w + · rintro ⟨m, w⟩ + apply Nat.le_antisymm + · exact nonzeroMinimum_le m h + · have nz : xs.nonzeroMinimum ≠ 0 := by + apply Nat.pos_iff_ne_zero.mp + apply nonzeroMinimum_pos m h + specialize w (nonzeroMinimum xs) (nonzeroMinimum_mem nz) + cases w with + | inl h => exact h + | inr h => exact False.elim (nz h) + +theorem nonzeroMinimum_eq_of_nonzero {xs : List Nat} (h : xs.nonzeroMinimum ≠ 0) : + ∃ x ∈ xs, xs.nonzeroMinimum = x := + ⟨xs.nonzeroMinimum, ((nonzeroMinimum_eq_nonzero_iff h).mp rfl).1, rfl⟩ + +theorem nonzeroMinimum_le_iff {xs : List Nat} {y : Nat} : + xs.nonzeroMinimum ≤ y ↔ xs.nonzeroMinimum = 0 ∨ ∃ x ∈ xs, x ≤ y ∧ x ≠ 0 := by + refine ⟨fun h => ?_, fun h => ?_⟩ + · rw [Classical.or_iff_not_imp_right] + simp only [ne_eq, not_exists, not_and, Classical.not_not, nonzeroMinimum_eq_zero_iff] + intro w + apply nonzeroMinimum_eq_zero_iff.mp + if p : xs.nonzeroMinimum = 0 then + exact p + else + exact w _ (nonzeroMinimum_mem p) h + · match h with + | .inl h => simp [h] + | .inr ⟨x, m, le, ne⟩ => exact Nat.le_trans (nonzeroMinimum_le m ne) le + +theorem nonzeroMininum_map_le_nonzeroMinimum (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) : + ((xs.map f).map q).nonzeroMinimum ≤ (xs.map p).nonzeroMinimum := by + rw [nonzeroMinimum_le_iff] + if z : (xs.map p).nonzeroMinimum = 0 then + rw [nonzeroMinimum_eq_zero_iff] + simp_all + else + have := nonzeroMinimum_eq_of_nonzero z + simp only [mem_map] at this + obtain ⟨x, ⟨a, m, rfl⟩, eq⟩ := this + refine .inr ⟨q (f a), List.mem_map_of_mem _ (List.mem_map_of_mem _ m), ?_, ?_⟩ + · rw [eq] at z ⊢ + apply w _ m z + · rwa [Ne, ← h _ m, ← eq] + +/-- +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. +-/ +def minNatAbs (xs : List Int) : Nat := xs.map Int.natAbs |>.nonzeroMinimum + +@[simp] theorem minNatAbs_eq_zero_iff {xs : List Int} : xs.minNatAbs = 0 ↔ ∀ y ∈ xs, y = 0 := by + simp [minNatAbs] + +theorem minNatAbs_eq_nonzero_iff (xs : List Int) (w : z ≠ 0) : + xs.minNatAbs = z ↔ (∃ y ∈ xs, y.natAbs = z) ∧ (∀ y ∈ xs, z ≤ y.natAbs ∨ y = 0) := by + simp [minNatAbs, nonzeroMinimum_eq_nonzero_iff w] + +@[simp] theorem minNatAbs_nil : ([] : List Int).minNatAbs = 0 := rfl + +/-- The maximum absolute value in a list of integers. -/ +def maxNatAbs (xs : List Int) : Nat := xs.map Int.natAbs |>.maximum? |>.getD 0 diff --git a/src/Lean/Elab/Tactic/Omega/OmegaM.lean b/src/Lean/Elab/Tactic/Omega/OmegaM.lean new file mode 100644 index 0000000000..dbc296b234 --- /dev/null +++ b/src/Lean/Elab/Tactic/Omega/OmegaM.lean @@ -0,0 +1,211 @@ +/- +Copyright (c) 2023 Lean FRO, LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Scott Morrison +-/ +import Lean.Meta.AppBuilder + +/-! +# 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. +-/ + +open Lean Meta Omega + +namespace Lean.Elab.Tactic.Omega + +/-- Context for the `OmegaM` monad, containing the user configurable options. -/ +structure Context where + /-- User configurable options for `omega`. -/ + cfg : OmegaConfig + +/-- The internal state for the `OmegaM` monad, recording previously encountered atoms. -/ +structure State where + /-- The atoms up-to-defeq encountered so far. -/ + atoms : Array Expr := #[] + +/-- An intermediate layer in the `OmegaM` monad. -/ +abbrev OmegaM' := StateRefT State (ReaderT Context MetaM) + +/-- +Cache of expressions that have been visited, and their reflection as a linear combination. +-/ +def Cache : Type := HashMap Expr (LinearCombo × OmegaM' Expr) + +/-- +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). -/ +abbrev OmegaM := StateRefT Cache OmegaM' + +/-- Run a computation in the `OmegaM` monad, starting with no recorded atoms. -/ +def OmegaM.run (m : OmegaM α) (cfg : OmegaConfig) : MetaM α := + m.run' HashMap.empty |>.run' {} { cfg } + +/-- Retrieve the user-specified configuration options. -/ +def cfg : OmegaM OmegaConfig := do pure (← read).cfg + +/-- Retrieve the list of atoms. -/ +def atoms : OmegaM (List Expr) := return (← getThe State).atoms.toList + +/-- Return the `Expr` representing the list of atoms. -/ +def atomsList : OmegaM Expr := do mkListLit (.const ``Int []) (← atoms) + +/-- Return the `Expr` representing the list of atoms as a `Coeffs`. -/ +def atomsCoeffs : OmegaM Expr := do + return .app (.const ``Coeffs.ofList []) (← atomsList) + +/-- Run an `OmegaM` computation, restoring the state afterwards depending on the result. -/ +def commitWhen (t : OmegaM (α × Bool)) : OmegaM α := do + let state ← getThe State + let cache ← getThe Cache + let (a, r) ← t + if !r then do + modifyThe State fun _ => state + modifyThe Cache fun _ => cache + pure a + +/-- +Run an `OmegaM` computation, restoring the state afterwards. +-/ +def withoutModifyingState (t : OmegaM α) : OmegaM α := + commitWhen (do pure (← t, false)) + +/-- Wrapper around `Expr.nat?` that also allows `Nat.cast`. -/ +def natCast? (n : Expr) : Option Nat := + match n.getAppFnArgs with + | (``Nat.cast, #[_, _, n]) => n.nat? + | _ => n.nat? + +/-- Wrapper around `Expr.int?` that also allows `Nat.cast`. -/ +def intCast? (n : Expr) : Option Int := + match n.getAppFnArgs with + | (``Nat.cast, #[_, _, n]) => n.nat? + | _ => n.int? + +/-- Construct the term with type hint `(Eq.refl a : a = b)`-/ +def mkEqReflWithExpectedType (a b : Expr) : MetaM Expr := do + mkExpectedTypeHint (← mkEqRefl a) (← mkEq a b) + +/-- +Analyzes a newly recorded atom, +returning a collection of interesting facts about it that should be added to the context. +-/ +def analyzeAtom (e : Expr) : OmegaM (HashSet Expr) := do + match e.getAppFnArgs with + | (``Nat.cast, #[.const ``Int [], _, e']) => + -- Casts of natural numbers are non-negative. + let mut r := HashSet.empty.insert (Expr.app (.const ``Int.ofNat_nonneg []) e') + match (← cfg).splitNatSub, e'.getAppFnArgs with + | true, (``HSub.hSub, #[_, _, _, _, a, b]) => + -- `((a - b : Nat) : Int)` gives a dichotomy + r := r.insert (mkApp2 (.const ``Int.ofNat_sub_dichotomy []) a b) + | _, (``Int.natAbs, #[x]) => + r := r.insert (mkApp (.const ``Int.le_natAbs []) x) + r := r.insert (mkApp (.const ``Int.neg_le_natAbs []) x) + | _, (``Fin.val, #[n, i]) => + r := r.insert (mkApp2 (.const ``Fin.isLt []) n i) + | _, _ => pure () + return r + | (``HDiv.hDiv, #[_, _, _, _, x, k]) => match natCast? k with + | none + | some 0 => pure ∅ + | some _ => + -- `k * x/k ≤ x < k * x/k + k` + let ne_zero := mkApp3 (.const ``Ne [1]) (.const ``Int []) k (toExpr (0 : Int)) + let pos := mkApp4 (.const ``LT.lt [0]) (.const ``Int []) (.const ``Int.instLTInt []) + (toExpr (0 : Int)) k + pure <| HashSet.empty.insert + (mkApp3 (.const ``Int.mul_ediv_self_le []) x k (← mkDecideProof ne_zero)) |>.insert + (mkApp3 (.const ``Int.lt_mul_ediv_self_add []) x k (← mkDecideProof pos)) + | (``HMod.hMod, #[_, _, _, _, x, k]) => + match k.getAppFnArgs with + | (``HPow.hPow, #[_, _, _, _, b, exp]) => match natCast? b with + | none + | some 0 => pure ∅ + | some _ => + let b_pos := mkApp4 (.const ``LT.lt [0]) (.const ``Int []) (.const ``Int.instLTInt []) + (toExpr (0 : Int)) b + let pow_pos := mkApp3 (.const ``Int.pos_pow_of_pos []) b exp (← mkDecideProof b_pos) + pure <| HashSet.empty.insert + (mkApp3 (.const ``Int.emod_nonneg []) x k + (mkApp3 (.const ``Int.ne_of_gt []) k (toExpr (0 : Int)) pow_pos)) |>.insert + (mkApp3 (.const ``Int.emod_lt_of_pos []) x k pow_pos) + | (``Nat.cast, #[.const ``Int [], _, k']) => + match k'.getAppFnArgs with + | (``HPow.hPow, #[_, _, _, _, b, exp]) => match natCast? b with + | none + | some 0 => pure ∅ + | some _ => + let b_pos := mkApp4 (.const ``LT.lt [0]) (.const ``Nat []) (.const ``instLTNat []) + (toExpr (0 : Nat)) b + let pow_pos := mkApp3 (.const ``Nat.pos_pow_of_pos []) b exp (← mkDecideProof b_pos) + let cast_pos := mkApp2 (.const ``Int.ofNat_pos_of_pos []) k' pow_pos + pure <| HashSet.empty.insert + (mkApp3 (.const ``Int.emod_nonneg []) x k + (mkApp3 (.const ``Int.ne_of_gt []) k (toExpr (0 : Int)) cast_pos)) |>.insert + (mkApp3 (.const ``Int.emod_lt_of_pos []) x k cast_pos) + | _ => pure ∅ + | _ => pure ∅ + | (``Min.min, #[_, _, x, y]) => + pure <| HashSet.empty.insert (mkApp2 (.const ``Int.min_le_left []) x y) |>.insert + (mkApp2 (.const ``Int.min_le_right []) x y) + | (``Max.max, #[_, _, x, y]) => + pure <| HashSet.empty.insert (mkApp2 (.const ``Int.le_max_left []) x y) |>.insert + (mkApp2 (.const ``Int.le_max_right []) x y) + | (``ite, #[α, i, dec, t, e]) => + if α == (.const ``Int []) then + pure <| HashSet.empty.insert <| mkApp5 (.const ``ite_disjunction [0]) α i dec t e + else + pure {} + | _ => pure ∅ + +/-- +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` +-/ +def lookup (e : Expr) : OmegaM (Nat × Option (HashSet Expr)) := do + let c ← getThe State + for h : i in [:c.atoms.size] do + if ← isDefEq e c.atoms[i] then + return (i, none) + trace[omega] "New atom: {e}" + let facts ← analyzeAtom e + if ← isTracingEnabledFor `omega then + unless facts.isEmpty do + trace[omega] "New facts: {← facts.toList.mapM fun e => inferType e}" + let i ← modifyGetThe State fun c => (c.atoms.size, { c with atoms := c.atoms.push e }) + return (i, some facts) + +end Omega diff --git a/src/Lean/LocalContext.lean b/src/Lean/LocalContext.lean index 10dd1d3d6f..ffdc746c2a 100644 --- a/src/Lean/LocalContext.lean +++ b/src/Lean/LocalContext.lean @@ -501,6 +501,13 @@ export MonadLCtx (getLCtx) instance [MonadLift m n] [MonadLCtx m] : MonadLCtx n where getLCtx := liftM (getLCtx : m _) +/-- Return local hypotheses which are not "implementation detail", as `Expr`s. -/ +def getLocalHyps [Monad m] [MonadLCtx m] : m (Array Expr) := do + let mut hs := #[] + for d in ← getLCtx do + if !d.isImplementationDetail then hs := hs.push d.toExpr + return hs + def LocalDecl.replaceFVarId (fvarId : FVarId) (e : Expr) (d : LocalDecl) : LocalDecl := if d.fvarId == fvarId then d else match d with diff --git a/tests/bench/reduceMatch.lean b/tests/bench/reduceMatch.lean index 8fc0af9ee6..3f997c6a04 100644 --- a/tests/bench/reduceMatch.lean +++ b/tests/bench/reduceMatch.lean @@ -27,9 +27,6 @@ instance decidableBall (l : List α) : Decidable (∀ x, x ∈ l → p x) := end decidability_instances -@[inline] protected def List.insert {α : Type} [DecidableEq α] (a : α) (l : List α) : List α := - if a ∈ l then l else a :: l - def parts : List (List Nat) := List.insert ([1, 1, 0, 0]) <| List.insert ([0, 0, 1, 1]) <| List.insert ([1, 0, 0, 1]) <| List.insert ([1, 1, 1, 0]) <| List.insert ([1, 0, 0, 0]) <| List.insert [1, 2, 3, 4] <| List.insert [5, 6, 7, 8] [] diff --git a/tests/lean/run/mergeSortCPDT.lean b/tests/lean/run/mergeSortCPDT.lean index 680f44d95a..67ba339127 100644 --- a/tests/lean/run/mergeSortCPDT.lean +++ b/tests/lean/run/mergeSortCPDT.lean @@ -1,12 +1,12 @@ -def List.insert (p : α → α → Bool) (a : α) (bs : List α) : List α := +def List.insert' (p : α → α → Bool) (a : α) (bs : List α) : List α := match bs with | [] => [a] - | b :: bs' => if p a b then a :: bs else b :: bs'.insert p a + | b :: bs' => if p a b then a :: bs else b :: bs'.insert' p a def List.merge (p : α → α → Bool) (as bs : List α) : List α := match as with | [] => bs - | a :: as' => insert p a (merge p as' bs) + | a :: as' => insert' p a (merge p as' bs) def List.split (as : List α) : List α × List α := match as with diff --git a/tests/lean/run/omega.lean b/tests/lean/run/omega.lean new file mode 100644 index 0000000000..3e136fb1fa --- /dev/null +++ b/tests/lean/run/omega.lean @@ -0,0 +1,382 @@ + +example : True := by + fail_if_success omega + trivial + +-- set_option trace.omega true +example (_ : (1 : Int) < (0 : Int)) : False := by omega + +example (_ : (0 : Int) < (0 : Int)) : False := by omega +example (_ : (0 : Int) < (1 : Int)) : True := by (fail_if_success omega); trivial + +example {x : Int} (_ : 0 ≤ x) (_ : x ≤ 1) : True := by (fail_if_success omega); trivial +example {x : Int} (_ : 0 ≤ x) (_ : x ≤ -1) : False := by omega + +example {x : Int} (_ : x % 2 < x - 2 * (x / 2)) : False := by omega +example {x : Int} (_ : x % 2 > 5) : False := by omega + +example {x : Int} (_ : 2 * (x / 2) > x) : False := by omega +example {x : Int} (_ : 2 * (x / 2) ≤ x - 2) : False := by omega + +example {x : Nat} : x / 0 = 0 := by omega +example {x : Int} : x / 0 = 0 := by omega + +example {x : Int} : x / 2 + x / (-2) = 0 := by omega + +example {x : Nat} (_ : x ≠ 0) : 0 < x := by omega + +example {x y z : Nat} (_ : a ≤ c) (_ : b ≤ c) : a < Nat.succ c := by omega + +example (_ : 7 < 3) : False := by omega +example (_ : 0 < 0) : False := by omega + +example {x : Nat} (_ : x > 7) (_ : x < 3) : False := by omega +example {x : Nat} (_ : x ≥ 7) (_ : x ≤ 3) : False := by omega + +example {x y : Nat} (_ : x + y > 10) (_ : x < 5) (_ : y < 5) : False := by omega + +example {x y : Int} (_ : x + y > 10) (_ : 2 * x < 11) (_ : y < 5) : False := by omega +example {x y : Nat} (_ : x + y > 10) (_ : 2 * x < 11) (_ : y < 5) : False := by omega + +example {x y : Int} (_ : 2 * x + 4 * y = 5) : False := by omega +example {x y : Nat} (_ : 2 * x + 4 * y = 5) : False := by omega + +example {x y : Int} (_ : 6 * x + 7 * y = 5) : True := by (fail_if_success omega); trivial + +example {x y : Nat} (_ : 6 * x + 7 * y = 5) : False := by omega + +example {x y : Nat} (_ : x * 6 + y * 7 = 5) : False := by omega +example {x y : Nat} (_ : 2 * (3 * x) + y * 7 = 5) : False := by omega +example {x y : Nat} (_ : 2 * x * 3 + y * 7 = 5) : False := by omega +example {x y : Nat} (_ : 2 * 3 * x + y * 7 = 5) : False := by omega + +example {x : Nat} (_ : x < 0) : False := by omega + +example {x y z : Int} (_ : x + y > z) (_ : x < 0) (_ : y < 0) (_ : z > 0) : False := by omega + +example {x y : Nat} (_ : x - y = 0) (_ : x > y) : False := by + fail_if_success omega (config := { splitNatSub := false }) + omega + +example {x y z : Int} (_ : x - y - z = 0) (_ : x > y + z) : False := by omega + +example {x y z : Nat} (_ : x - y - z = 0) (_ : x > y + z) : False := by omega + +example {a b c d e f : Nat} (_ : a - b - c - d - e - f = 0) (_ : a > b + c + d + e + f) : + False := by + omega + +example {x y : Nat} (h₁ : x - y ≤ 0) (h₂ : y < x) : False := by omega + +example {x y : Int} (_ : x / 2 - y / 3 < 1) (_ : 3 * x ≥ 2 * y + 6) : False := by omega + +example {x y : Nat} (_ : x / 2 - y / 3 < 1) (_ : 3 * x ≥ 2 * y + 6) : False := by omega + +example {x y : Nat} (_ : x / 2 - y / 3 < 1) (_ : 3 * x ≥ 2 * y + 4) : False := by omega + +example {x y : Nat} (_ : x / 2 - y / 3 < x % 2) (_ : 3 * x ≥ 2 * y + 4) : False := by omega + +example {x : Int} (h₁ : 5 ≤ x) (h₂ : x ≤ 4) : False := by omega + +example {x : Nat} (h₁ : 5 ≤ x) (h₂ : x ≤ 4) : False := by omega + +example {x : Nat} (h₁ : x / 3 ≥ 2) (h₂ : x < 6) : False := by omega + +example {x : Int} {y : Nat} (_ : 0 < x) (_ : x + y ≤ 0) : False := by omega + +example {a b c : Nat} (_ : a - (b - c) ≤ 5) (_ : b ≥ c + 3) (_ : a + c ≥ b + 6) : False := by omega + +example {x : Nat} : 1 < (1 + ((x + 1 : Nat) : Int) + 2) / 2 := by omega + +example {x : Nat} : (x + 4) / 2 ≤ x + 2 := by omega + +example {x : Int} {m : Nat} (_ : 0 < m) (_ : ¬x % ↑m < (↑m + 1) / 2) : -↑m / 2 ≤ x % ↑m - ↑m := by + omega + +example (h : (7 : Int) = 0) : False := by omega + +example (h : (7 : Int) ≤ 0) : False := by omega + +example (h : (-7 : Int) + 14 = 0) : False := by omega + +example (h : (-7 : Int) + 14 ≤ 0) : False := by omega + +example (h : (1 : Int) + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 = 0) : False := by + omega + +example (h : (7 : Int) - 14 = 0) : False := by omega + +example (h : (14 : Int) - 7 ≤ 0) : False := by omega + +example (h : (1 : Int) - 1 + 1 - 1 + 1 - 1 + 1 - 1 + 1 - 1 + 1 - 1 + 1 - 1 + 1 = 0) : False := by + omega + +example (h : -(7 : Int) = 0) : False := by omega + +example (h : -(-7 : Int) ≤ 0) : False := by omega + +example (h : 2 * (7 : Int) = 0) : False := by omega + +example (h : (7 : Int) < 0) : False := by omega + +example {x : Int} (h : x + x + 1 = 0) : False := by omega + +example {x : Int} (h : 2 * x + 1 = 0) : False := by omega + +example {x y : Int} (h : x + x + y + y + 1 = 0) : False := by omega + +example {x y : Int} (h : 2 * x + 2 * y + 1 = 0) : False := by omega + +example {x : Int} (h₁ : 0 ≤ -7 + x) (h₂ : 0 ≤ 3 - x) : False := by omega + +example {x : Int} (h₁ : 0 ≤ -7 + x) (h₂ : 0 < 4 - x) : False := by omega + +example {x : Int} (h₁ : 0 ≤ 2 * x + 1) (h₂ : 2 * x + 1 ≤ 0) : False := by omega + +example {x : Int} (h₁ : 0 < 2 * x + 2) (h₂ : 2 * x + 1 ≤ 0) : False := by omega + +example {x y : Int} (h₁ : 0 ≤ 2 * x + 1) (h₂ : x = y) (h₃ : 2 * y + 1 ≤ 0) : False := by omega + +example {x y z : Int} (h₁ : 0 ≤ 2 * x + 1) (h₂ : x = y) (h₃ : y = z) (h₄ : 2 * z + 1 ≤ 0) : + False := by omega + +example {x1 x2 x3 x4 x5 x6 : Int} (h : 0 ≤ 2 * x1 + 1) (h : x1 = x2) (h : x2 = x3) (h : x3 = x4) + (h : x4 = x5) (h : x5 = x6) (h : 2 * x6 + 1 ≤ 0) : False := by omega + +example {x : Int} (_ : 1 ≤ -3 * x) (_ : 1 ≤ 2 * x) : False := by omega + +example {x y : Int} (_ : 2 * x + 3 * y = 0) (_ : 1 ≤ x) (_ : 1 ≤ y) : False := by omega + +example {x y z : Int} (_ : 2 * x + 3 * y = 0) (_ : 3 * y + 4 * z = 0) (_ : 1 ≤ x) (_ : 1 ≤ -z) : + False := by omega + +example {x y z : Int} (_ : 2 * x + 3 * y + 4 * z = 0) (_ : 1 ≤ x + y) (_ : 1 ≤ y + z) + (_ : 1 ≤ x + z) : False := by omega + +example {x y : Int} (_ : 1 ≤ 3 * x) (_ : y ≤ 2) (_ : 6 * x - 2 ≤ y) : False := by omega + +example {x y : Int} (_ : y = x) (_ : 0 ≤ x - 2 * y) (_ : x - 2 * y ≤ 1) (_ : 1 ≤ x) : False := by + omega +example {x y : Int} (_ : y = x) (_ : 0 ≤ x - 2 * y) (_ : x - 2 * y ≤ 1) (_ : x ≥ 1) : False := by + omega +example {x y : Int} (_ : y = x) (_ : 0 ≤ x - 2 * y) (_ : x - 2 * y ≤ 1) (_ : 0 < x) : False := by + omega +example {x y : Int} (_ : y = x) (_ : 0 ≤ x - 2 * y) (_ : x - 2 * y ≤ 1) (_ : x > 0) : False := by + omega + +example {x : Nat} (_ : 10 ∣ x) (_ : ¬ 5 ∣ x) : False := by omega +example {x y : Nat} (_ : 5 ∣ x) (_ : ¬ 10 ∣ x) (_ : y = 7) (_ : x - y ≤ 2) (_ : x ≥ 6) : False := by + omega + +example (x : Nat) : x % 4 - x % 8 = 0 := by omega + +example {n : Nat} (_ : n > 0) : (2*n - 1) % 2 = 1 := by omega + +example (x : Int) (_ : x > 0 ∧ x < -1) : False := by omega +example (x : Int) (_ : x > 7) : x < 0 ∨ x > 3 := by omega + +example (_ : ∃ n : Nat, n < 0) : False := by omega +example (_ : { x : Int // x < 0 ∧ x > 0 }) : False := by omega +example {x y : Int} (_ : x < y) (z : { z : Int // y ≤ z ∧ z ≤ x }) : False := by omega + +example (a b c d e : Int) + (ha : 2 * a + b + c + d + e = 4) + (hb : a + 2 * b + c + d + e = 5) + (hc : a + b + 2 * c + d + e = 6) + (hd : a + b + c + 2 * d + e = 7) + (he : a + b + c + d + 2 * e = 8) : e = 3 := by omega + +example (a b c d e : Int) + (ha : 2 * a + b + c + d + e = 4) + (hb : a + 2 * b + c + d + e = 5) + (hc : a + b + 2 * c + d + e = 6) + (hd : a + b + c + 2 * d + e = 7) + (he : a + b + c + d + 2 * e = 8 ∨ e = 3) : e = 3 := by + fail_if_success omega (config := { splitDisjunctions := false }) + omega + +example {x : Int} (h : x = 7) : x.natAbs = 7 := by + fail_if_success omega (config := { splitNatAbs := false }) + fail_if_success omega (config := { splitDisjunctions := false }) + omega + +example {x y : Int} (_ : (x - y).natAbs < 3) (_ : x < 5) (_ : y > 15) : False := by + omega + +example {a b : Int} (h : a < b) (w : b < a) : False := by omega + +example (_e b c a v0 v1 : Int) (_h1 : v0 = 5 * a) (_h2 : v1 = 3 * b) (h3 : v0 + v1 + c = 10) : + v0 + 5 + (v1 - 3) + (c - 2) = 10 := by omega + +example (h : (1 : Int) < 0) (_ : ¬ (37 : Int) < 42) (_ : True) (_ : (-7 : Int) < 5) : + (3 : Int) < 7 := by omega + +example (A B : Int) (h : 0 < A * B) : 0 < 8 * (A * B) := by omega + +example (A B : Nat) (h : 7 < A * B) : 0 < A*B/8 := by omega +example (A B : Int) (h : 7 < A * B) : 0 < A*B/8 := by omega + +example (ε : Int) (h1 : ε > 0) : ε / 2 + ε / 3 + ε / 7 < ε := by omega + +example (x y z : Int) (h1 : 2*x < 3*y) (h2 : -4*x + z/2 < 0) (h3 : 12*y - z < 0) : False := by omega + +example (ε : Int) (h1 : ε > 0) : ε / 2 < ε := by omega + +example (ε : Int) (_ : ε > 0) : ε - 2 ≤ ε / 3 + ε / 3 + ε / 3 := by omega +example (ε : Int) (_ : ε > 0) : ε / 3 + ε / 3 + ε / 3 ≤ ε := by omega +example (ε : Int) (_ : ε > 0) : ε - 2 ≤ ε / 3 + ε / 3 + ε / 3 ∧ ε / 3 + ε / 3 + ε / 3 ≤ ε := by + omega + +example (x : Int) (h : 0 < x) : 0 < x / 1 := by omega + +example (x : Int) (h : 5 < x) : 0 < x/2/3 := by omega + +example (_a b _c : Nat) (h2 : b + 2 > 3 + b) : False := by omega +example (_a b _c : Int) (h2 : b + 2 > 3 + b) : False := by omega + +example (g v V c h : Int) (_ : h = 0) (_ : v = V) (_ : V > 0) (_ : g > 0) + (_ : 0 ≤ c) (_ : c < 1) : v ≤ V := by omega + +example (x y z : Int) (h1 : 2 * x < 3 * y) (h2 : -4 * x + 2 * z < 0) (h3 : 12 * y - 4 * z < 0) : + False := by + omega + +example (x y z : Int) (h1 : 2 * x < 3 * y) (h2 : -4 * x + 2 * z < 0) (_h3 : x * y < 5) + (h3 : 12 * y - 4 * z < 0) : False := by omega + +example (a b c : Int) (h1 : a > 0) (h2 : b > 5) (h3 : c < -10) (h4 : a + b - c < 3) : False := by + omega + +example (_ b _ : Int) (h2 : b > 0) (h3 : ¬ b ≥ 0) : False := by + omega + +example (x y z : Int) (hx : x ≤ 3 * y) (h2 : y ≤ 2 * z) (h3 : x ≥ 6 * z) : x = 3 * y := by + omega + +example (x y z : Int) (h1 : 2 * x < 3 * y) (h2 : -4 * x + 2 * z < 0) (_h3 : x * y < 5) : + ¬ 12 * y - 4 * z < 0 := by + omega + +example (x y z : Int) (hx : ¬ x > 3 * y) (h2 : ¬ y > 2 * z) (h3 : x ≥ 6 * z) : x = 3 * y := by + omega + +example (x y : Int) (h : 6 + ((x + 4) * x + (6 + 3 * y) * y) = 3) (h' : (x + 4) * x ≥ 0) + (h'' : (6 + 3 * y) * y ≥ 0) : False := by omega + +example (a : Int) (ha : 0 ≤ a) : 0 * 0 ≤ 2 * a := by omega + +example (x y : Int) (h : x < y) : x ≠ y := by omega + +example (x y : Int) (h : x < y) : ¬ x = y := by omega + +example (x : Int) : id x ≥ x := by omega + +example (prime : Nat → Prop) (x y z : Int) (h1 : 2 * x + ((-3) * y) < 0) (h2 : (-4) * x + 2* z < 0) + (h3 : 12 * y + (-4) * z < 0) (_ : prime 7) : False := by omega + +example (i n : Nat) (h : (2 : Int) ^ i ≤ 2 ^ n) : (0 : Int) ≤ 2 ^ n - 2 ^ i := by omega + +-- Check we use `exfalso` on non-comparison goals. +example (prime : Nat → Prop) (_ b _ : Nat) (h2 : b > 0) (h3 : b < 0) : prime 10 := by + omega + +example (a b c : Nat) (h2 : (2 : Nat) > 3) : a + b - c ≥ 3 := by omega + +-- Verify that we split conjunctions in hypotheses. +example (x y : Int) + (h : 6 + ((x + 4) * x + (6 + 3 * y) * y) = 3 ∧ (x + 4) * x ≥ 0 ∧ (6 + 3 * y) * y ≥ 0) : + False := by omega + +example (mess : Nat → Nat) (S n : Nat) : + mess S + (n * mess S + n * 2 + 1) < n * mess S + mess S + (n * 2 + 2) := by omega + +example (p n p' n' : Nat) (h : p + n' = p' + n) : n + p' = n' + p := by + omega + +example (a b c : Int) (h1 : 32 / a < b) (h2 : b < c) : 32 / a < c := by omega + +-- Check that `autoParam` wrappers do not get in the way of using hypotheses. +example (i n : Nat) (hi : i ≤ n := by omega) : i < n + 1 := by + omega + +-- Test that we consume expression metadata when necessary. +example : 0 = 0 := by + have : 0 = 0 := by omega + omega -- This used to fail. + +/-! ### `Prod.Lex` -/ + +-- This example comes from the termination proof +-- for `permutationsAux.rec` in `Mathlib.Data.List.Defs`. +example {x y : Nat} : Prod.Lex (· < ·) (· < ·) (x, x) (Nat.succ y + x, Nat.succ y) := by omega + +-- We test the termination proof in-situ: +def List.permutationsAux.rec' {C : List α → List α → Sort v} (H0 : ∀ is, C [] is) + (H1 : ∀ t ts is, C ts (t :: is) → C is [] → C (t :: ts) is) : ∀ l₁ l₂, C l₁ l₂ + | [], is => H0 is + | t :: ts, is => + H1 t ts is (permutationsAux.rec' H0 H1 ts (t :: is)) (permutationsAux.rec' H0 H1 is []) + termination_by ts is => (length ts + length is, length ts) + decreasing_by all_goals simp_wf; omega + +example {x y w z : Nat} (h : Prod.Lex (· < ·) (· < ·) (x + 1, y + 1) (w, z)) : + Prod.Lex (· < ·) (· < ·) (x, y) (w, z) := by omega + +-- Verify that we can handle `iff` statements in hypotheses: +example (a b : Int) (h : a < 0 ↔ b < 0) (w : b > 3) : a ≥ 0 := by omega + +-- Verify that we can prove `iff` goals: +example (a b : Int) (h : a > 7) (w : b > 2) : a > 0 ↔ b > 0 := by omega + +-- Verify that we can prove implications: +example (a : Int) : a > 0 → a > -1 := by omega + +-- Verify that we can introduce multiple arguments: +example (x y : Int) : x + 1 ≤ y → ¬ y + 1 ≤ x := by omega + +-- Verify that we can handle double negation: +example (x y : Int) (_ : x < y) (_ : ¬ ¬ y < x) : False := by omega + +-- Verify that we don't treat function goals as implications. +example (a : Nat) (h : a < 0) : Nat → Nat := by omega + +-- Example from Cedar: +example {a₁ a₂ p₁ p₂ : Nat} + (h₁ : a₁ = a₂ → ¬p₁ = p₂) : + (a₁ < a₂ ∨ a₁ = a₂ ∧ p₁ < p₂) ∨ a₂ < a₁ ∨ a₂ = a₁ ∧ p₂ < p₁ := by omega + +-- From https://github.com/leanprover/std4/issues/562 +example {i : Nat} (h1 : i < 330) (_h2 : 7 ∣ (660 + i) * (1319 - i)) : 1319 - i < 1979 := by + omega + +example {a : Int} (_ : a < min a b) : False := by omega (config := { splitMinMax := false }) +example {a : Int} (_ : max a b < b) : False := by omega (config := { splitMinMax := false }) +example {a : Nat} (_ : a < min a b) : False := by omega (config := { splitMinMax := false }) +example {a : Nat} (_ : max a b < b) : False := by omega (config := { splitMinMax := false }) + +example {a b : Nat} (_ : a = 7) (_ : b = 3) : min a b = 3 := by + fail_if_success omega (config := { splitMinMax := false }) + omega + +example {a b : Nat} (_ : a + b = 9) : (min a b) % 2 + (max a b) % 2 = 1 := by + fail_if_success omega (config := { splitMinMax := false }) + omega + +example {a : Int} (_ : a < if a ≤ b then a else b) : False := by omega +example {a b : Int} : (if a < b then a else b - 1) ≤ b := by omega + +-- Check that we use local values. +example (i j : Nat) (p : i ≥ j) : True := by + let l := j - 1 + have _ : i ≥ l := by omega + trivial + +example (i j : Nat) (p : i ≥ j) : True := by + let l := j - 1 + let k := l + have _ : i ≥ k := by omega + trivial + +example (i : Fin 7) : (i : Nat) < 8 := by omega + +example (x y z i : Nat) (hz : z ≤ 1) : x % 2 ^ i + y % 2 ^ i + z < 2 * 2^ i := by omega