diff --git a/src/Init/Grind/Module/Envelope.lean b/src/Init/Grind/Module/Envelope.lean index 869e203279..df4a6fb34a 100644 --- a/src/Init/Grind/Module/Envelope.lean +++ b/src/Init/Grind/Module/Envelope.lean @@ -267,7 +267,7 @@ instance [NatModule α] [AddRightCancel α] [NoNatZeroDivisors α] : NoNatZeroDi replace h₂ := NoNatZeroDivisors.no_nat_zero_divisors k (a₁ + b₂) (a₂ + b₁) h₁ h₂ apply Quot.sound; simp [r]; exists 0; simp [h₂] -instance [Preorder α] [OrderedAdd α] : LE (OfNatModule.Q α) where +instance [LE α] [LT α] [Preorder α] [OrderedAdd α] : LE (OfNatModule.Q α) where le a b := Q.liftOn₂ a b (fun (a, b) (c, d) => a + d ≤ b + c) (by intro (a₁, b₁) (a₂, b₂) (a₃, b₃) (a₄, b₄) simp; intro k₁ h₁ k₂ h₂ @@ -283,11 +283,14 @@ instance [Preorder α] [OrderedAdd α] : LE (OfNatModule.Q α) where rw [this]; clear this rw [← OrderedAdd.add_le_left_iff]) -@[local simp] theorem mk_le_mk [Preorder α] [OrderedAdd α] {a₁ a₂ b₁ b₂ : α} : +instance [LE α] [LT α] [Preorder α] [OrderedAdd α] : LT (OfNatModule.Q α) where + lt a b := a ≤ b ∧ ¬b ≤ a + +@[local simp] theorem mk_le_mk [LE α] [LT α] [Preorder α] [OrderedAdd α] {a₁ a₂ b₁ b₂ : α} : Q.mk (a₁, a₂) ≤ Q.mk (b₁, b₂) ↔ a₁ + b₂ ≤ a₂ + b₁ := by rfl -instance [Preorder α] [OrderedAdd α] : Preorder (OfNatModule.Q α) where +instance [LE α] [LT α] [Preorder α] [OrderedAdd α] : Preorder (OfNatModule.Q α) where le_refl a := by obtain ⟨⟨a₁, a₂⟩⟩ := a change Q.mk _ ≤ Q.mk _ @@ -308,24 +311,24 @@ instance [Preorder α] [OrderedAdd α] : Preorder (OfNatModule.Q α) where attribute [-simp] Q.mk -@[local simp] private theorem mk_lt_mk [Preorder α] [OrderedAdd α] {a₁ a₂ b₁ b₂ : α} : +@[local simp] private theorem mk_lt_mk [LE α] [LT α] [Preorder α] [OrderedAdd α] {a₁ a₂ b₁ b₂ : α} : Q.mk (a₁, a₂) < Q.mk (b₁, b₂) ↔ a₁ + b₂ < a₂ + b₁ := by simp [Preorder.lt_iff_le_not_le, AddCommMonoid.add_comm] -@[local simp] private theorem mk_pos [Preorder α] [OrderedAdd α] {a₁ a₂ : α} : +@[local simp] private theorem mk_pos [LE α] [LT α] [Preorder α] [OrderedAdd α] {a₁ a₂ : α} : 0 < Q.mk (a₁, a₂) ↔ a₂ < a₁ := by change Q.mk (0,0) < _ ↔ _ simp [mk_lt_mk, AddCommMonoid.zero_add] @[local simp] -theorem toQ_le [Preorder α] [OrderedAdd α] {a b : α} : toQ a ≤ toQ b ↔ a ≤ b := by +theorem toQ_le [LE α] [LT α] [Preorder α] [OrderedAdd α] {a b : α} : toQ a ≤ toQ b ↔ a ≤ b := by simp @[local simp] -theorem toQ_lt [Preorder α] [OrderedAdd α] {a b : α} : toQ a < toQ b ↔ a < b := by +theorem toQ_lt [LE α] [LT α] [Preorder α] [OrderedAdd α] {a b : α} : toQ a < toQ b ↔ a < b := by simp [Preorder.lt_iff_le_not_le] -instance [Preorder α] [OrderedAdd α] : OrderedAdd (OfNatModule.Q α) where +instance [LE α] [LT α] [Preorder α] [OrderedAdd α] : OrderedAdd (OfNatModule.Q α) where add_le_left_iff := by intro a b c obtain ⟨⟨a₁, a₂⟩⟩ := a diff --git a/src/Init/Grind/Ordered/Field.lean b/src/Init/Grind/Ordered/Field.lean index b8157ab5c2..34cf9bdde1 100644 --- a/src/Init/Grind/Ordered/Field.lean +++ b/src/Init/Grind/Ordered/Field.lean @@ -15,7 +15,7 @@ namespace Lean.Grind namespace Field.IsOrdered -variable {R : Type u} [Field R] [LinearOrder R] [OrderedRing R] +variable {R : Type u} [Field R] [LE R] [LT R] [LinearOrder R] [OrderedRing R] open OrderedAdd open OrderedRing diff --git a/src/Init/Grind/Ordered/Linarith.lean b/src/Init/Grind/Ordered/Linarith.lean index 5dfc9cfe00..0d7e86ae81 100644 --- a/src/Init/Grind/Ordered/Linarith.lean +++ b/src/Init/Grind/Ordered/Linarith.lean @@ -254,17 +254,17 @@ open OrderedAdd Helper theorems for conflict resolution during model construction. -/ -private theorem le_add_le {α} [IntModule α] [Preorder α] [OrderedAdd α] {a b : α} +private theorem le_add_le {α} [IntModule α] [LE α] [LT α] [Preorder α] [OrderedAdd α] {a b : α} (h₁ : a ≤ 0) (h₂ : b ≤ 0) : a + b ≤ 0 := by replace h₁ := add_le_left h₁ b; simp at h₁ exact Preorder.le_trans h₁ h₂ -private theorem le_add_lt {α} [IntModule α] [Preorder α] [OrderedAdd α] {a b : α} +private theorem le_add_lt {α} [IntModule α] [LE α] [LT α] [Preorder α] [OrderedAdd α] {a b : α} (h₁ : a ≤ 0) (h₂ : b < 0) : a + b < 0 := by replace h₁ := add_le_left h₁ b; simp at h₁ exact Preorder.lt_of_le_of_lt h₁ h₂ -private theorem lt_add_lt {α} [IntModule α] [Preorder α] [OrderedAdd α] {a b : α} +private theorem lt_add_lt {α} [IntModule α] [LE α] [LT α] [Preorder α] [OrderedAdd α] {a b : α} (h₁ : a < 0) (h₂ : b < 0) : a + b < 0 := by replace h₁ := add_lt_left h₁ b; simp at h₁ exact Preorder.lt_trans h₁ h₂ @@ -277,7 +277,7 @@ def le_le_combine_cert (p₁ p₂ p₃ : Poly) : Bool := let a₂ := p₂.leadCoeff.natAbs p₃ == (p₁.mul a₂ |>.combine (p₂.mul a₁)) -theorem le_le_combine {α} [IntModule α] [Preorder α] [OrderedAdd α] (ctx : Context α) (p₁ p₂ p₃ : Poly) +theorem le_le_combine {α} [IntModule α] [LE α] [LT α] [Preorder α] [OrderedAdd α] (ctx : Context α) (p₁ p₂ p₃ : Poly) : le_le_combine_cert p₁ p₂ p₃ → p₁.denote' ctx ≤ 0 → p₂.denote' ctx ≤ 0 → p₃.denote' ctx ≤ 0 := by simp [le_le_combine_cert]; intro _ h₁ h₂; subst p₃; simp replace h₁ := zsmul_nonpos (coe_natAbs_nonneg p₂.leadCoeff) h₁ @@ -289,7 +289,7 @@ def le_lt_combine_cert (p₁ p₂ p₃ : Poly) : Bool := let a₂ := p₂.leadCoeff.natAbs a₁ > (0 : Int) && p₃ == (p₁.mul a₂ |>.combine (p₂.mul a₁)) -theorem le_lt_combine {α} [IntModule α] [Preorder α] [OrderedAdd α] (ctx : Context α) (p₁ p₂ p₃ : Poly) +theorem le_lt_combine {α} [IntModule α] [LE α] [LT α] [Preorder α] [OrderedAdd α] (ctx : Context α) (p₁ p₂ p₃ : Poly) : le_lt_combine_cert p₁ p₂ p₃ → p₁.denote' ctx ≤ 0 → p₂.denote' ctx < 0 → p₃.denote' ctx < 0 := by simp [-Int.natAbs_pos, -Int.ofNat_pos, le_lt_combine_cert]; intro hp _ h₁ h₂; subst p₃; simp replace h₁ := zsmul_nonpos (coe_natAbs_nonneg p₂.leadCoeff) h₁ @@ -301,7 +301,7 @@ def lt_lt_combine_cert (p₁ p₂ p₃ : Poly) : Bool := let a₂ := p₂.leadCoeff.natAbs a₂ > (0 : Int) && a₁ > (0 : Int) && p₃ == (p₁.mul a₂ |>.combine (p₂.mul a₁)) -theorem lt_lt_combine {α} [IntModule α] [Preorder α] [OrderedAdd α] (ctx : Context α) (p₁ p₂ p₃ : Poly) +theorem lt_lt_combine {α} [IntModule α] [LE α] [LT α] [Preorder α] [OrderedAdd α] (ctx : Context α) (p₁ p₂ p₃ : Poly) : lt_lt_combine_cert p₁ p₂ p₃ → p₁.denote' ctx < 0 → p₂.denote' ctx < 0 → p₃.denote' ctx < 0 := by simp [-Int.natAbs_pos, -Int.ofNat_pos, lt_lt_combine_cert]; intro hp₁ hp₂ _ h₁ h₂; subst p₃; simp replace h₁ := zsmul_neg_iff (↑p₂.leadCoeff.natAbs) h₁ |>.mpr hp₁ @@ -312,7 +312,7 @@ def diseq_split_cert (p₁ p₂ : Poly) : Bool := p₂ == p₁.mul (-1) -- We need `LinearOrder` to use `trichotomy` -theorem diseq_split {α} [IntModule α] [LinearOrder α] [OrderedAdd α] (ctx : Context α) (p₁ p₂ : Poly) +theorem diseq_split {α} [IntModule α] [LE α] [LT α] [LinearOrder α] [OrderedAdd α] (ctx : Context α) (p₁ p₂ : Poly) : diseq_split_cert p₁ p₂ → p₁.denote' ctx ≠ 0 → p₁.denote' ctx < 0 ∨ p₂.denote' ctx < 0 := by simp [diseq_split_cert]; intro _ h₁; subst p₂; simp cases LinearOrder.trichotomy (p₁.denote ctx) 0 @@ -322,7 +322,7 @@ theorem diseq_split {α} [IntModule α] [LinearOrder α] [OrderedAdd α] (ctx : simp [h₁] at h rw [← neg_pos_iff, neg_zsmul, neg_neg, one_zsmul]; assumption -theorem diseq_split_resolve {α} [IntModule α] [LinearOrder α] [OrderedAdd α] (ctx : Context α) (p₁ p₂ : Poly) +theorem diseq_split_resolve {α} [IntModule α] [LE α] [LT α] [LinearOrder α] [OrderedAdd α] (ctx : Context α) (p₁ p₂ : Poly) : diseq_split_cert p₁ p₂ → p₁.denote' ctx ≠ 0 → ¬p₁.denote' ctx < 0 → p₂.denote' ctx < 0 := by intro h₁ h₂ h₃ exact (diseq_split ctx p₁ p₂ h₁ h₂).resolve_left h₃ @@ -338,7 +338,7 @@ theorem eq_norm {α} [IntModule α] (ctx : Context α) (lhs rhs : Expr) (p : Pol : norm_cert lhs rhs p → lhs.denote ctx = rhs.denote ctx → p.denote' ctx = 0 := by simp [norm_cert]; intro _ h₁; subst p; simp [Expr.denote, h₁, sub_self] -theorem le_of_eq {α} [IntModule α] [Preorder α] [OrderedAdd α] (ctx : Context α) (lhs rhs : Expr) (p : Poly) +theorem le_of_eq {α} [IntModule α] [LE α] [LT α] [Preorder α] [OrderedAdd α] (ctx : Context α) (lhs rhs : Expr) (p : Poly) : norm_cert lhs rhs p → lhs.denote ctx = rhs.denote ctx → p.denote' ctx ≤ 0 := by simp [norm_cert]; intro _ h₁; subst p; simp [Expr.denote, h₁, sub_self] apply Preorder.le_refl @@ -351,21 +351,21 @@ theorem diseq_norm {α} [IntModule α] (ctx : Context α) (lhs rhs : Expr) (p : rw [add_left_comm, ← sub_eq_add_neg, sub_self, add_zero] at h contradiction -theorem le_norm {α} [IntModule α] [Preorder α] [OrderedAdd α] (ctx : Context α) (lhs rhs : Expr) (p : Poly) +theorem le_norm {α} [IntModule α] [LE α] [LT α] [Preorder α] [OrderedAdd α] (ctx : Context α) (lhs rhs : Expr) (p : Poly) : norm_cert lhs rhs p → lhs.denote ctx ≤ rhs.denote ctx → p.denote' ctx ≤ 0 := by simp [norm_cert]; intro _ h₁; subst p; simp [Expr.denote] replace h₁ := add_le_left h₁ (-rhs.denote ctx) simp [← sub_eq_add_neg, sub_self] at h₁ assumption -theorem lt_norm {α} [IntModule α] [Preorder α] [OrderedAdd α] (ctx : Context α) (lhs rhs : Expr) (p : Poly) +theorem lt_norm {α} [IntModule α] [LE α] [LT α] [Preorder α] [OrderedAdd α] (ctx : Context α) (lhs rhs : Expr) (p : Poly) : norm_cert lhs rhs p → lhs.denote ctx < rhs.denote ctx → p.denote' ctx < 0 := by simp [norm_cert]; intro _ h₁; subst p; simp [Expr.denote] replace h₁ := add_lt_left h₁ (-rhs.denote ctx) simp [← sub_eq_add_neg, sub_self] at h₁ assumption -theorem not_le_norm {α} [IntModule α] [LinearOrder α] [OrderedAdd α] (ctx : Context α) (lhs rhs : Expr) (p : Poly) +theorem not_le_norm {α} [IntModule α] [LE α] [LT α] [LinearOrder α] [OrderedAdd α] (ctx : Context α) (lhs rhs : Expr) (p : Poly) : norm_cert rhs lhs p → ¬ lhs.denote ctx ≤ rhs.denote ctx → p.denote' ctx < 0 := by simp [norm_cert]; intro _ h₁; subst p; simp [Expr.denote] replace h₁ := LinearOrder.lt_of_not_le h₁ @@ -373,7 +373,7 @@ theorem not_le_norm {α} [IntModule α] [LinearOrder α] [OrderedAdd α] (ctx : simp [← sub_eq_add_neg, sub_self] at h₁ assumption -theorem not_lt_norm {α} [IntModule α] [LinearOrder α] [OrderedAdd α] (ctx : Context α) (lhs rhs : Expr) (p : Poly) +theorem not_lt_norm {α} [IntModule α] [LE α] [LT α] [LinearOrder α] [OrderedAdd α] (ctx : Context α) (lhs rhs : Expr) (p : Poly) : norm_cert rhs lhs p → ¬ lhs.denote ctx < rhs.denote ctx → p.denote' ctx ≤ 0 := by simp [norm_cert]; intro _ h₁; subst p; simp [Expr.denote] replace h₁ := LinearOrder.le_of_not_lt h₁ @@ -383,14 +383,14 @@ theorem not_lt_norm {α} [IntModule α] [LinearOrder α] [OrderedAdd α] (ctx : -- If the module does not have a linear order, we can still put the expressions in polynomial forms -theorem not_le_norm' {α} [IntModule α] [Preorder α] [OrderedAdd α] (ctx : Context α) (lhs rhs : Expr) (p : Poly) +theorem not_le_norm' {α} [IntModule α] [LE α] [LT α] [Preorder α] [OrderedAdd α] (ctx : Context α) (lhs rhs : Expr) (p : Poly) : norm_cert lhs rhs p → ¬ lhs.denote ctx ≤ rhs.denote ctx → ¬ p.denote' ctx ≤ 0 := by simp [norm_cert]; intro _ h₁; subst p; simp [Expr.denote]; intro h replace h := add_le_right (rhs.denote ctx) h rw [sub_eq_add_neg, add_left_comm, ← sub_eq_add_neg, sub_self] at h; simp at h contradiction -theorem not_lt_norm' {α} [IntModule α] [Preorder α] [OrderedAdd α] (ctx : Context α) (lhs rhs : Expr) (p : Poly) +theorem not_lt_norm' {α} [IntModule α] [LE α] [LT α] [Preorder α] [OrderedAdd α] (ctx : Context α) (lhs rhs : Expr) (p : Poly) : norm_cert lhs rhs p → ¬ lhs.denote ctx < rhs.denote ctx → ¬ p.denote' ctx < 0 := by simp [norm_cert]; intro _ h₁; subst p; simp [Expr.denote]; intro h replace h := add_lt_right (rhs.denote ctx) h @@ -403,7 +403,7 @@ Equality detection def eq_of_le_ge_cert (p₁ p₂ : Poly) : Bool := p₂ == p₁.mul (-1) -theorem eq_of_le_ge {α} [IntModule α] [PartialOrder α] [OrderedAdd α] (ctx : Context α) (p₁ : Poly) (p₂ : Poly) +theorem eq_of_le_ge {α} [IntModule α] [LE α] [LT α] [PartialOrder α] [OrderedAdd α] (ctx : Context α) (p₁ : Poly) (p₂ : Poly) : eq_of_le_ge_cert p₁ p₂ → p₁.denote' ctx ≤ 0 → p₂.denote' ctx ≤ 0 → p₁.denote' ctx = 0 := by simp [eq_of_le_ge_cert] intro; subst p₂; simp @@ -419,7 +419,7 @@ Helper theorems for closing the goal theorem diseq_unsat {α} [IntModule α] (ctx : Context α) : (Poly.nil).denote ctx ≠ 0 → False := by simp [Poly.denote] -theorem lt_unsat {α} [IntModule α] [Preorder α] (ctx : Context α) : (Poly.nil).denote ctx < 0 → False := by +theorem lt_unsat {α} [IntModule α] [LE α] [LT α] [Preorder α] (ctx : Context α) : (Poly.nil).denote ctx < 0 → False := by simp [Poly.denote]; intro h have := Preorder.lt_iff_le_not_le.mp h simp at this @@ -427,7 +427,7 @@ theorem lt_unsat {α} [IntModule α] [Preorder α] (ctx : Context α) : (Poly.ni def zero_lt_one_cert (p : Poly) : Bool := p == .add (-1) 0 .nil -theorem zero_lt_one {α} [Ring α] [Preorder α] [OrderedRing α] (ctx : Context α) (p : Poly) +theorem zero_lt_one {α} [Ring α] [LE α] [LT α] [Preorder α] [OrderedRing α] (ctx : Context α) (p : Poly) : zero_lt_one_cert p → (0 : Var).denote ctx = One.one → p.denote' ctx < 0 := by simp [zero_lt_one_cert]; intro _ h; subst p; simp [Poly.denote, h, One.one, neg_zsmul] rw [neg_lt_iff, neg_zero]; apply OrderedRing.zero_lt_one @@ -435,7 +435,7 @@ theorem zero_lt_one {α} [Ring α] [Preorder α] [OrderedRing α] (ctx : Context def zero_ne_one_cert (p : Poly) : Bool := p == .add 1 0 .nil -theorem zero_ne_one_of_ord_ring {α} [Ring α] [Preorder α] [OrderedRing α] (ctx : Context α) (p : Poly) +theorem zero_ne_one_of_ord_ring {α} [Ring α] [LE α] [LT α] [Preorder α] [OrderedRing α] (ctx : Context α) (p : Poly) : zero_ne_one_cert p → (0 : Var).denote ctx = One.one → p.denote' ctx ≠ 0 := by simp [zero_ne_one_cert]; intro _ h; subst p; simp [Poly.denote, h, One.one] intro h; have := OrderedRing.zero_lt_one (R := α); simp [h, Preorder.lt_irrefl] at this @@ -484,7 +484,7 @@ theorem eq_coeff {α} [IntModule α] [NoNatZeroDivisors α] (ctx : Context α) ( def coeff_cert (p₁ p₂ : Poly) (k : Nat) := k > 0 && p₁ == p₂.mul k -theorem le_coeff {α} [IntModule α] [LinearOrder α] [OrderedAdd α] (ctx : Context α) (p₁ p₂ : Poly) (k : Nat) +theorem le_coeff {α} [IntModule α] [LE α] [LT α] [LinearOrder α] [OrderedAdd α] (ctx : Context α) (p₁ p₂ : Poly) (k : Nat) : coeff_cert p₁ p₂ k → p₁.denote' ctx ≤ 0 → p₂.denote' ctx ≤ 0 := by simp [coeff_cert]; intro h _; subst p₁; simp have : ↑k > (0 : Int) := Int.natCast_pos.mpr h @@ -493,7 +493,7 @@ theorem le_coeff {α} [IntModule α] [LinearOrder α] [OrderedAdd α] (ctx : Con replace h₂ := zsmul_pos_iff (↑k) h₂ |>.mpr this exact Preorder.lt_irrefl 0 (Preorder.lt_of_lt_of_le h₂ h₁) -theorem lt_coeff {α} [IntModule α] [LinearOrder α] [OrderedAdd α] (ctx : Context α) (p₁ p₂ : Poly) (k : Nat) +theorem lt_coeff {α} [IntModule α] [LE α] [LT α] [LinearOrder α] [OrderedAdd α] (ctx : Context α) (p₁ p₂ : Poly) (k : Nat) : coeff_cert p₁ p₂ k → p₁.denote' ctx < 0 → p₂.denote' ctx < 0 := by simp [coeff_cert]; intro h _; subst p₁; simp have : ↑k > (0 : Int) := Int.natCast_pos.mpr h @@ -544,7 +544,7 @@ def eq_le_subst_cert (x : Var) (p₁ p₂ p₃ : Poly) := let b := p₂.coeff x a ≥ 0 && p₃ == (p₂.mul a |>.combine (p₁.mul (-b))) -theorem eq_le_subst {α} [IntModule α] [Preorder α] [OrderedAdd α] (ctx : Context α) (x : Var) (p₁ p₂ p₃ : Poly) +theorem eq_le_subst {α} [IntModule α] [LE α] [LT α] [Preorder α] [OrderedAdd α] (ctx : Context α) (x : Var) (p₁ p₂ p₃ : Poly) : eq_le_subst_cert x p₁ p₂ p₃ → p₁.denote' ctx = 0 → p₂.denote' ctx ≤ 0 → p₃.denote' ctx ≤ 0 := by simp [eq_le_subst_cert]; intro h _ h₁ h₂; subst p₃; simp [h₁] exact zsmul_nonpos h h₂ @@ -554,7 +554,7 @@ def eq_lt_subst_cert (x : Var) (p₁ p₂ p₃ : Poly) := let b := p₂.coeff x a > 0 && p₃ == (p₂.mul a |>.combine (p₁.mul (-b))) -theorem eq_lt_subst {α} [IntModule α] [Preorder α] [OrderedAdd α] (ctx : Context α) (x : Var) (p₁ p₂ p₃ : Poly) +theorem eq_lt_subst {α} [IntModule α] [LE α] [LT α] [Preorder α] [OrderedAdd α] (ctx : Context α) (x : Var) (p₁ p₂ p₃ : Poly) : eq_lt_subst_cert x p₁ p₂ p₃ → p₁.denote' ctx = 0 → p₂.denote' ctx < 0 → p₃.denote' ctx < 0 := by simp [eq_lt_subst_cert]; intro h _ h₁ h₂; subst p₃; simp [h₁] exact zsmul_neg_iff (p₁.coeff x) h₂ |>.mpr h diff --git a/src/Init/Grind/Ordered/Module.lean b/src/Init/Grind/Ordered/Module.lean index 5a04159967..0a5104b071 100644 --- a/src/Init/Grind/Ordered/Module.lean +++ b/src/Init/Grind/Ordered/Module.lean @@ -17,7 +17,7 @@ namespace Lean.Grind /-- Addition is compatible with a preorder if `a ≤ b ↔ a + c ≤ b + c`. -/ -class OrderedAdd (M : Type u) [HAdd M M M] [Preorder M] where +class OrderedAdd (M : Type u) [HAdd M M M] [LE M] [LT M] [Preorder M] where /-- `a + c ≤ b + c` iff `a ≤ b`. -/ add_le_left_iff : ∀ {a b : M} (c : M), a ≤ b ↔ a + c ≤ b + c @@ -30,7 +30,7 @@ open AddCommMonoid NatModule section -variable {M : Type u} [Preorder M] [AddCommMonoid M] [OrderedAdd M] +variable {M : Type u} [LE M] [LT M] [Preorder M] [AddCommMonoid M] [OrderedAdd M] theorem add_le_right_iff {a b : M} (c : M) : a ≤ b ↔ c + a ≤ c + b := by rw [add_comm c a, add_comm c b, add_le_left_iff] @@ -73,7 +73,7 @@ end section -variable {M : Type u} [Preorder M] [NatModule M] [OrderedAdd M] +variable {M : Type u} [LE M] [LT M] [Preorder M] [NatModule M] [OrderedAdd M] theorem nsmul_le_nsmul {k : Nat} {a b : M} (h : a ≤ b) : k * a ≤ k * b := by induction k with @@ -117,7 +117,7 @@ end section open AddCommGroup -variable {M : Type u} [Preorder M] [AddCommGroup M] [OrderedAdd M] +variable {M : Type u} [LE M] [LT M] [Preorder M] [AddCommGroup M] [OrderedAdd M] theorem neg_le_iff {a b : M} : -a ≤ b ↔ -b ≤ a := by rw [OrderedAdd.add_le_left_iff a, neg_add_cancel] @@ -127,7 +127,7 @@ theorem neg_le_iff {a b : M} : -a ≤ b ↔ -b ≤ a := by end section -variable {M : Type u} [Preorder M] [IntModule M] [OrderedAdd M] +variable {M : Type u} [LE M] [LT M] [Preorder M] [IntModule M] [OrderedAdd M] open AddCommGroup IntModule theorem zsmul_pos_iff (k : Int) {x : M} (h : 0 < x) : 0 < k * x ↔ 0 < k := @@ -154,7 +154,7 @@ theorem zsmul_nonneg {k : Int} {x : M} (h : 0 ≤ k) (hx : 0 ≤ x) : 0 ≤ k * end section -variable {M : Type u} [Preorder M] [AddCommGroup M] [OrderedAdd M] +variable {M : Type u} [LE M] [LT M] [Preorder M] [AddCommGroup M] [OrderedAdd M] open AddCommGroup @@ -186,7 +186,7 @@ end section -variable {M : Type u} [Preorder M] [IntModule M] [OrderedAdd M] +variable {M : Type u} [LE M] [LT M] [Preorder M] [IntModule M] [OrderedAdd M] open IntModule theorem zsmul_neg_iff (k : Int) {a : M} (h : a < 0) : k * a < 0 ↔ 0 < k := by diff --git a/src/Init/Grind/Ordered/Order.lean b/src/Init/Grind/Ordered/Order.lean index e3e4c06d8c..a47d7b23b8 100644 --- a/src/Init/Grind/Ordered/Order.lean +++ b/src/Init/Grind/Ordered/Order.lean @@ -13,18 +13,18 @@ public section namespace Lean.Grind /-- A preorder is a reflexive, transitive relation `≤` with `a < b` defined in the obvious way. -/ -class Preorder (α : Type u) extends LE α, LT α where +class Preorder (α : Type u) [LE α] [LT α] where /-- The less-than-or-equal relation is reflexive. -/ le_refl : ∀ a : α, a ≤ a /-- The less-than-or-equal relation is transitive. -/ le_trans : ∀ {a b c : α}, a ≤ b → b ≤ c → a ≤ c - lt := fun a b => a ≤ b ∧ ¬b ≤ a + lt := fun a b : α => a ≤ b ∧ ¬b ≤ a /-- The less-than relation is determined by the less-than-or-equal relation. -/ lt_iff_le_not_le : ∀ {a b : α}, a < b ↔ a ≤ b ∧ ¬b ≤ a := by intros; rfl namespace Preorder -variable {α : Type u} [Preorder α] +variable {α : Type u} [LE α] [LT α] [Preorder α] theorem le_of_lt {a b : α} (h : a < b) : a ≤ b := (lt_iff_le_not_le.mp h).1 @@ -58,13 +58,13 @@ theorem not_gt_of_lt {a b : α} (h : a < b) : ¬a > b := end Preorder /-- A partial order is a preorder with the additional property that `a ≤ b` and `b ≤ a` implies `a = b`. -/ -class PartialOrder (α : Type u) extends Preorder α where +class PartialOrder (α : Type u) [LE α] [LT α] extends Preorder α where /-- The less-than-or-equal relation is antisymmetric. -/ le_antisymm : ∀ {a b : α}, a ≤ b → b ≤ a → a = b namespace PartialOrder -variable {α : Type u} [PartialOrder α] +variable {α : Type u} [LE α] [LT α] [PartialOrder α] theorem le_iff_lt_or_eq {a b : α} : a ≤ b ↔ a < b ∨ a = b := by constructor @@ -79,13 +79,13 @@ theorem le_iff_lt_or_eq {a b : α} : a ≤ b ↔ a < b ∨ a = b := by end PartialOrder /-- A linear order is a partial order with the additional property that every pair of elements is comparable. -/ -class LinearOrder (α : Type u) extends PartialOrder α where +class LinearOrder (α : Type u) [LE α] [LT α] extends PartialOrder α where /-- For every two elements `a` and `b`, either `a ≤ b` or `b ≤ a`. -/ le_total : ∀ a b : α, a ≤ b ∨ b ≤ a namespace LinearOrder -variable {α : Type u} [LinearOrder α] +variable {α : Type u} [LE α] [LT α] [LinearOrder α] theorem trichotomy (a b : α) : a < b ∨ a = b ∨ b < a := by cases LinearOrder.le_total a b with @@ -100,12 +100,12 @@ theorem trichotomy (a b : α) : a < b ∨ a = b ∨ b < a := by | inl h => right; right; exact h | inr h => right; left; exact h.symm -theorem le_of_not_lt {α} [LinearOrder α] {a b : α} (h : ¬ a < b) : b ≤ a := by +theorem le_of_not_lt {a b : α} (h : ¬ a < b) : b ≤ a := by cases LinearOrder.trichotomy a b next => contradiction next h => apply PartialOrder.le_iff_lt_or_eq.mpr; cases h <;> simp [*] -theorem lt_of_not_le {α} [LinearOrder α] {a b : α} (h : ¬ a ≤ b) : b < a := by +theorem lt_of_not_le {a b : α} (h : ¬ a ≤ b) : b < a := by cases LinearOrder.trichotomy a b next h₁ h₂ => have := Preorder.lt_iff_le_not_le.mp h₂; simp [h] at this next h => diff --git a/src/Init/Grind/Ordered/Ring.lean b/src/Init/Grind/Ordered/Ring.lean index c878637a87..5c48435a04 100644 --- a/src/Init/Grind/Ordered/Ring.lean +++ b/src/Init/Grind/Ordered/Ring.lean @@ -17,7 +17,7 @@ namespace Lean.Grind A ring which is also equipped with a preorder is considered a strict ordered ring if addition, negation, and multiplication are compatible with the preorder, and `0 < 1`. -/ -class OrderedRing (R : Type u) [Semiring R] [Preorder R] extends OrderedAdd R where +class OrderedRing (R : Type u) [Semiring R] [LE R] [LT R] [Preorder R] extends OrderedAdd R where /-- In a strict ordered semiring, we have `0 < 1`. -/ zero_lt_one : (0 : R) < 1 /-- In a strict ordered semiring, we can multiply an inequality `a < b` on the left @@ -33,7 +33,7 @@ variable {R : Type u} [Ring R] section Preorder -variable [Preorder R] [OrderedRing R] +variable [LE R] [LT R] [Preorder R] [OrderedRing R] theorem neg_one_lt_zero : (-1 : R) < 0 := by have h := zero_lt_one (R := R) @@ -52,7 +52,7 @@ theorem ofNat_nonneg (x : Nat) : (OfNat.ofNat x : R) ≥ 0 := by have := Preorder.lt_of_lt_of_le this ih exact Preorder.le_of_lt this -instance [Ring α] [Preorder α] [OrderedRing α] : IsCharP α 0 := IsCharP.mk' _ _ <| by +instance [Ring R] [LE R] [LT R] [Preorder R] [OrderedRing R] : IsCharP R 0 := IsCharP.mk' _ _ <| by intro x simp only [Nat.mod_zero]; constructor next => @@ -64,11 +64,11 @@ instance [Ring α] [Preorder α] [OrderedRing α] : IsCharP α 0 := IsCharP.mk' replace h := congrArg (· - 1) h; simp at h rw [Ring.sub_eq_add_neg, Semiring.add_assoc, AddCommGroup.add_neg_cancel, Ring.sub_eq_add_neg, AddCommMonoid.zero_add, Semiring.add_zero] at h - have h₁ : (OfNat.ofNat x : α) < 0 := by - have := OrderedRing.neg_one_lt_zero (R := α) + have h₁ : (OfNat.ofNat x : R) < 0 := by + have := OrderedRing.neg_one_lt_zero (R := R) rw [h]; assumption - have h₂ := OrderedRing.ofNat_nonneg (R := α) x - have : (0 : α) < 0 := Preorder.lt_of_le_of_lt h₂ h₁ + have h₂ := OrderedRing.ofNat_nonneg (R := R) x + have : (0 : R) < 0 := Preorder.lt_of_le_of_lt h₂ h₁ simp exact (Preorder.lt_irrefl 0) this next => intro h; rw [OfNat.ofNat, h]; rfl @@ -77,7 +77,7 @@ end Preorder section PartialOrder -variable [PartialOrder R] [OrderedRing R] +variable [LE R] [LT R] [PartialOrder R] [OrderedRing R] theorem zero_le_one : (0 : R) ≤ 1 := Preorder.le_of_lt zero_lt_one @@ -158,7 +158,7 @@ end PartialOrder section LinearOrder -variable [LinearOrder R] [OrderedRing R] +variable [LE R] [LT R] [LinearOrder R] [OrderedRing R] theorem mul_nonneg_iff {a b : R} : 0 ≤ a * b ↔ 0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0 := by rcases LinearOrder.trichotomy 0 a with (ha | rfl | ha) diff --git a/src/Init/Grind/Ring/Envelope.lean b/src/Init/Grind/Ring/Envelope.lean index 79830156df..e9a56ea70d 100644 --- a/src/Init/Grind/Ring/Envelope.lean +++ b/src/Init/Grind/Ring/Envelope.lean @@ -359,7 +359,7 @@ instance {p} [Semiring α] [AddRightCancel α] [IsCharP α p] : IsCharP (OfSemir apply Quot.sound exists 0; simp [← Semiring.ofNat_eq_natCast, this] -instance [Preorder α] [OrderedAdd α] : LE (OfSemiring.Q α) where +instance [LE α] [LT α] [Preorder α] [OrderedAdd α] : LE (OfSemiring.Q α) where le a b := Q.liftOn₂ a b (fun (a, b) (c, d) => a + d ≤ b + c) (by intro (a₁, b₁) (a₂, b₂) (a₃, b₃) (a₄, b₄) simp; intro k₁ h₁ k₂ h₂ @@ -375,11 +375,14 @@ instance [Preorder α] [OrderedAdd α] : LE (OfSemiring.Q α) where rw [this]; clear this rw [← OrderedAdd.add_le_left_iff]) -@[local simp] theorem mk_le_mk [Preorder α] [OrderedAdd α] {a₁ a₂ b₁ b₂ : α} : +instance [LE α] [LT α] [Preorder α] [OrderedAdd α] : LT (OfSemiring.Q α) where + lt a b := a ≤ b ∧ ¬b ≤ a + +@[local simp] theorem mk_le_mk [LE α] [LT α] [Preorder α] [OrderedAdd α] {a₁ a₂ b₁ b₂ : α} : Q.mk (a₁, a₂) ≤ Q.mk (b₁, b₂) ↔ a₁ + b₂ ≤ a₂ + b₁ := by rfl -instance [Preorder α] [OrderedAdd α] : Preorder (OfSemiring.Q α) where +instance [LE α] [LT α] [Preorder α] [OrderedAdd α] : Preorder (OfSemiring.Q α) where le_refl a := by obtain ⟨⟨a₁, a₂⟩⟩ := a change Q.mk _ ≤ Q.mk _ @@ -398,23 +401,23 @@ instance [Preorder α] [OrderedAdd α] : Preorder (OfSemiring.Q α) where rw [this]; clear this exact OrderedAdd.add_le_add h₁ h₂ -@[local simp] private theorem mk_lt_mk [Preorder α] [OrderedAdd α] {a₁ a₂ b₁ b₂ : α} : +@[local simp] private theorem mk_lt_mk [LE α] [LT α] [Preorder α] [OrderedAdd α] {a₁ a₂ b₁ b₂ : α} : Q.mk (a₁, a₂) < Q.mk (b₁, b₂) ↔ a₁ + b₂ < a₂ + b₁ := by simp [Preorder.lt_iff_le_not_le, Semiring.add_comm] -@[local simp] private theorem mk_pos [Preorder α] [OrderedAdd α] {a₁ a₂ : α} : +@[local simp] private theorem mk_pos [LE α] [LT α] [Preorder α] [OrderedAdd α] {a₁ a₂ : α} : 0 < Q.mk (a₁, a₂) ↔ a₂ < a₁ := by simp [← toQ_ofNat, toQ, mk_lt_mk, AddCommMonoid.zero_add] @[local simp] -theorem toQ_le [Preorder α] [OrderedAdd α] {a b : α} : toQ a ≤ toQ b ↔ a ≤ b := by +theorem toQ_le [LE α] [LT α] [Preorder α] [OrderedAdd α] {a b : α} : toQ a ≤ toQ b ↔ a ≤ b := by simp @[local simp] -theorem toQ_lt [Preorder α] [OrderedAdd α] {a b : α} : toQ a < toQ b ↔ a < b := by +theorem toQ_lt [LE α] [LT α] [Preorder α] [OrderedAdd α] {a b : α} : toQ a < toQ b ↔ a < b := by simp [Preorder.lt_iff_le_not_le] -instance [Preorder α] [OrderedAdd α] : OrderedAdd (OfSemiring.Q α) where +instance [LE α] [LT α] [Preorder α] [OrderedAdd α] : OrderedAdd (OfSemiring.Q α) where add_le_left_iff := by intro a b c obtain ⟨⟨a₁, a₂⟩⟩ := a @@ -428,7 +431,7 @@ instance [Preorder α] [OrderedAdd α] : OrderedAdd (OfSemiring.Q α) where rw [← OrderedAdd.add_le_left_iff] -- This perhaps works in more generality than `ExistsAddOfLT`? -instance [Preorder α] [OrderedRing α] [ExistsAddOfLT α] : OrderedRing (OfSemiring.Q α) where +instance [LE α] [LT α] [Preorder α] [OrderedRing α] [ExistsAddOfLT α] : OrderedRing (OfSemiring.Q α) where zero_lt_one := by rw [← toQ_ofNat, ← toQ_ofNat, toQ_lt] exact OrderedRing.zero_lt_one diff --git a/src/Init/Grind/Ring/Poly.lean b/src/Init/Grind/Ring/Poly.lean index 60dcdeab2e..e63170e678 100644 --- a/src/Init/Grind/Ring/Poly.lean +++ b/src/Init/Grind/Ring/Poly.lean @@ -1616,21 +1616,21 @@ theorem diseq_norm {α} [CommRing α] (ctx : Context α) (lhs rhs : Expr) (p : P open OrderedAdd -theorem le_norm {α} [CommRing α] [Preorder α] [OrderedRing α] (ctx : Context α) (lhs rhs : Expr) (p : Poly) +theorem le_norm {α} [CommRing α] [LE α] [LT α] [Preorder α] [OrderedRing α] (ctx : Context α) (lhs rhs : Expr) (p : Poly) : core_cert lhs rhs p → lhs.denote ctx ≤ rhs.denote ctx → p.denoteAsIntModule ctx ≤ 0 := by simp [core_cert, Poly.denoteAsIntModule_eq_denote]; intro _ h; subst p; simp [Expr.denote_toPoly, Expr.denote] replace h := add_le_left h ((-1) * rhs.denote ctx) rw [neg_mul, ← sub_eq_add_neg, one_mul, ← sub_eq_add_neg, sub_self] at h assumption -theorem lt_norm {α} [CommRing α] [Preorder α] [OrderedRing α] (ctx : Context α) (lhs rhs : Expr) (p : Poly) +theorem lt_norm {α} [CommRing α] [LE α] [LT α] [Preorder α] [OrderedRing α] (ctx : Context α) (lhs rhs : Expr) (p : Poly) : core_cert lhs rhs p → lhs.denote ctx < rhs.denote ctx → p.denoteAsIntModule ctx < 0 := by simp [core_cert, Poly.denoteAsIntModule_eq_denote]; intro _ h; subst p; simp [Expr.denote_toPoly, Expr.denote] replace h := add_lt_left h ((-1) * rhs.denote ctx) rw [neg_mul, ← sub_eq_add_neg, one_mul, ← sub_eq_add_neg, sub_self] at h assumption -theorem not_le_norm {α} [CommRing α] [LinearOrder α] [OrderedRing α] (ctx : Context α) (lhs rhs : Expr) (p : Poly) +theorem not_le_norm {α} [CommRing α] [LE α] [LT α] [LinearOrder α] [OrderedRing α] (ctx : Context α) (lhs rhs : Expr) (p : Poly) : core_cert rhs lhs p → ¬ lhs.denote ctx ≤ rhs.denote ctx → p.denoteAsIntModule ctx < 0 := by simp [core_cert, Poly.denoteAsIntModule_eq_denote]; intro _ h₁; subst p; simp [Expr.denote_toPoly, Expr.denote] replace h₁ := LinearOrder.lt_of_not_le h₁ @@ -1638,7 +1638,7 @@ theorem not_le_norm {α} [CommRing α] [LinearOrder α] [OrderedRing α] (ctx : simp [← sub_eq_add_neg, sub_self] at h₁ assumption -theorem not_lt_norm {α} [CommRing α] [LinearOrder α] [OrderedRing α] (ctx : Context α) (lhs rhs : Expr) (p : Poly) +theorem not_lt_norm {α} [CommRing α] [LE α] [LT α] [LinearOrder α] [OrderedRing α] (ctx : Context α) (lhs rhs : Expr) (p : Poly) : core_cert rhs lhs p → ¬ lhs.denote ctx < rhs.denote ctx → p.denoteAsIntModule ctx ≤ 0 := by simp [core_cert, Poly.denoteAsIntModule_eq_denote]; intro _ h₁; subst p; simp [Expr.denote_toPoly, Expr.denote] replace h₁ := LinearOrder.le_of_not_lt h₁ @@ -1646,14 +1646,14 @@ theorem not_lt_norm {α} [CommRing α] [LinearOrder α] [OrderedRing α] (ctx : simp [← sub_eq_add_neg, sub_self] at h₁ assumption -theorem not_le_norm' {α} [CommRing α] [Preorder α] [OrderedRing α] (ctx : Context α) (lhs rhs : Expr) (p : Poly) +theorem not_le_norm' {α} [CommRing α] [LE α] [LT α] [Preorder α] [OrderedRing α] (ctx : Context α) (lhs rhs : Expr) (p : Poly) : core_cert lhs rhs p → ¬ lhs.denote ctx ≤ rhs.denote ctx → ¬ p.denoteAsIntModule ctx ≤ 0 := by simp [core_cert, Poly.denoteAsIntModule_eq_denote]; intro _ h₁; subst p; simp [Expr.denote_toPoly, Expr.denote]; intro h replace h : rhs.denote ctx + (lhs.denote ctx - rhs.denote ctx) ≤ _ := add_le_right (rhs.denote ctx) h rw [sub_eq_add_neg, add_left_comm, ← sub_eq_add_neg, sub_self] at h; simp [add_zero] at h contradiction -theorem not_lt_norm' {α} [CommRing α] [Preorder α] [OrderedRing α] (ctx : Context α) (lhs rhs : Expr) (p : Poly) +theorem not_lt_norm' {α} [CommRing α] [LE α] [LT α] [Preorder α] [OrderedRing α] (ctx : Context α) (lhs rhs : Expr) (p : Poly) : core_cert lhs rhs p → ¬ lhs.denote ctx < rhs.denote ctx → ¬ p.denoteAsIntModule ctx < 0 := by simp [core_cert, Poly.denoteAsIntModule_eq_denote]; intro _ h₁; subst p; simp [Expr.denote_toPoly, Expr.denote]; intro h replace h : rhs.denote ctx + (lhs.denote ctx - rhs.denote ctx) < _ := add_lt_right (rhs.denote ctx) h diff --git a/src/Init/GrindInstances/Ring/BitVec.lean b/src/Init/GrindInstances/Ring/BitVec.lean index d7bb12bc35..599f166f77 100644 --- a/src/Init/GrindInstances/Ring/BitVec.lean +++ b/src/Init/GrindInstances/Ring/BitVec.lean @@ -7,6 +7,7 @@ module prelude public import Init.Grind.Ring.Basic +public import Init.Grind.Ordered.Order public import Init.GrindInstances.ToInt public import all Init.Data.BitVec.Basic public import all Init.Grind.ToInt @@ -53,4 +54,15 @@ example : ToInt.Sub (BitVec w) (.uint w) := inferInstance instance : ToInt.Pow (BitVec w) (.uint w) := ToInt.pow_of_semiring (by simp) +instance : Preorder (BitVec w) where + le_refl := BitVec.le_refl + le_trans := BitVec.le_trans + lt_iff_le_not_le {a b} := Std.LawfulOrderLT.lt_iff a b + +instance : PartialOrder (BitVec w) where + le_antisymm := BitVec.le_antisymm + +instance : LinearOrder (BitVec w) where + le_total := BitVec.le_total + end Lean.Grind diff --git a/src/Lean/Meta/Tactic/Grind/Arith/Linear/Proof.lean b/src/Lean/Meta/Tactic/Grind/Arith/Linear/Proof.lean index 987630ab40..1e4e198844 100644 --- a/src/Lean/Meta/Tactic/Grind/Arith/Linear/Proof.lean +++ b/src/Lean/Meta/Tactic/Grind/Arith/Linear/Proof.lean @@ -139,29 +139,29 @@ private def mkIntModNoNatDivThmPrefix (declName : Name) : ProofM Expr := do /-- Returns the prefix of a theorem with name `declName` where the first four arguments are -`{α} [IntModule α] [Preorder α] (ctx : Context α)` +`{α} [IntModule α] [LE α] [LT α] [Preorder α] (ctx : Context α)` -/ private def mkIntModPreThmPrefix (declName : Name) : ProofM Expr := do let s ← getStruct - return mkApp4 (mkConst declName [s.u]) s.type s.intModuleInst (← getPreorderInst) (← getContext) + return mkApp6 (mkConst declName [s.u]) s.type s.intModuleInst (← getLEInst) (← getLTInst) (← getPreorderInst) (← getContext) /-- Returns the prefix of a theorem with name `declName` where the first five arguments are -`{α} [IntModule α] [Preorder α] [OrderedAdd α] (ctx : Context α)` +`{α} [IntModule α] [LE α] [LT α] [Preorder α] [OrderedAdd α] (ctx : Context α)` This is the most common theorem prefix at `Linarith.lean` -/ private def mkIntModPreOrdThmPrefix (declName : Name) : ProofM Expr := do let s ← getStruct - return mkApp5 (mkConst declName [s.u]) s.type s.intModuleInst (← getPreorderInst) (← getOrderedAddInst) (← getContext) + return mkApp7 (mkConst declName [s.u]) s.type s.intModuleInst (← getLEInst) (← getLTInst) (← getPreorderInst) (← getOrderedAddInst) (← getContext) /-- Returns the prefix of a theorem with name `declName` where the first five arguments are -`{α} [IntModule α] [LinearOrder α] [OrderedAdd α] (ctx : Context α)` +`{α} [IntModule α] [LE α] [LT α] [LinearOrder α] [OrderedAdd α] (ctx : Context α)` This is the most common theorem prefix at `Linarith.lean` -/ private def mkIntModLinOrdThmPrefix (declName : Name) : ProofM Expr := do let s ← getStruct - return mkApp5 (mkConst declName [s.u]) s.type s.intModuleInst (← getLinearOrderInst) (← getOrderedAddInst) (← getContext) + return mkApp7 (mkConst declName [s.u]) s.type s.intModuleInst (← getLEInst) (← getLTInst) (← getLinearOrderInst) (← getOrderedAddInst) (← getContext) /-- Returns the prefix of a theorem with name `declName` where the first three arguments are @@ -173,19 +173,19 @@ private def mkCommRingThmPrefix (declName : Name) : ProofM Expr := do /-- Returns the prefix of a theorem with name `declName` where the first five arguments are -`{α} [CommRing α] [Preorder α] [OrderedRing α] (rctx : Context α)` +`{α} [CommRing α] [LE α] [LT α] [Preorder α] [OrderedRing α] (rctx : Context α)` -/ private def mkCommRingPreOrdThmPrefix (declName : Name) : ProofM Expr := do let s ← getStruct - return mkApp5 (mkConst declName [s.u]) s.type (← getCommRingInst) (← getPreorderInst) (← getOrderedRingInst) (← getRingContext) + return mkApp7 (mkConst declName [s.u]) s.type (← getCommRingInst) (← getLEInst) (← getLTInst) (← getPreorderInst) (← getOrderedRingInst) (← getRingContext) /-- Returns the prefix of a theorem with name `declName` where the first five arguments are -`{α} [CommRing α] [LinearOrder α] [OrderedRing α] (rctx : Context α)` +`{α} [CommRing α] [LE α] [LT α] [LinearOrder α] [OrderedRing α] (rctx : Context α)` -/ private def mkCommRingLinOrdThmPrefix (declName : Name) : ProofM Expr := do let s ← getStruct - return mkApp5 (mkConst declName [s.u]) s.type (← getCommRingInst) (← getLinearOrderInst) (← getOrderedRingInst) (← getRingContext) + return mkApp7 (mkConst declName [s.u]) s.type (← getCommRingInst) (← getLEInst) (← getLTInst) (← getLinearOrderInst) (← getOrderedRingInst) (← getRingContext) mutual partial def IneqCnstr.toExprProof (c' : IneqCnstr) : ProofM Expr := caching c' do @@ -217,7 +217,7 @@ partial def IneqCnstr.toExprProof (c' : IneqCnstr) : ProofM Expr := caching c' d (← c₁.toExprProof) (← c₂.toExprProof) | .oneGtZero => let s ← getStruct - let h := mkApp5 (mkConst ``Grind.Linarith.zero_lt_one [s.u]) s.type (← getRingInst) (← getPreorderInst) (← getOrderedRingInst) (← getContext) + let h := mkApp7 (mkConst ``Grind.Linarith.zero_lt_one [s.u]) s.type (← getRingInst) (← getLEInst) (← getLTInst) (← getPreorderInst) (← getOrderedRingInst) (← getContext) return mkApp3 h (← mkPolyDecl c'.p) eagerReflBoolTrue (← mkEqRefl (← getOne)) | .ofEq a b la lb => let h ← mkIntModPreOrdThmPrefix ``Grind.Linarith.le_of_eq diff --git a/src/Lean/Meta/Tactic/Grind/Arith/Linear/StructId.lean b/src/Lean/Meta/Tactic/Grind/Arith/Linear/StructId.lean index affe56b835..4adf8c39e0 100644 --- a/src/Lean/Meta/Tactic/Grind/Arith/Linear/StructId.lean +++ b/src/Lean/Meta/Tactic/Grind/Arith/Linear/StructId.lean @@ -97,10 +97,39 @@ private def mkOne? (u : Level) (type : Expr) : GoalM (Option Expr) := do unless (← withDefault <| isDefEq one one') do reportIssue! (← mkExpectedDefEqMsg one one') return some one -private def mkOrderedRingInst? (u : Level) (type : Expr) (semiringInst? preorderInst? : Option Expr) : GoalM (Option Expr) := do +private def mkPreorderInst? (u : Level) (type : Expr) (leInst? ltInst? : Option Expr) : GoalM (Option Expr) := do + let some leInst := leInst? | return none + let some ltInst := ltInst? | return none + let preorderType := mkApp3 (mkConst ``Grind.Preorder [u]) type leInst ltInst + let some inst ← synthInstance? preorderType + | reportIssue! "type has `LE` and `LT`, but is not a preorder, failed to synthesize{indentExpr preorderType}" + return none + return some inst + +private def mkPartialOrderInst? (u : Level) (type : Expr) (leInst? ltInst? : Option Expr) : GoalM (Option Expr) := do + let some leInst := leInst? | return none + let some ltInst := ltInst? | return none + let partialOrderType := mkApp3 (mkConst ``Grind.PartialOrder [u]) type leInst ltInst + let some inst ← synthInstance? partialOrderType + | reportIssue! "type has `LE` and `LT`, but is not a partial order, failed to synthesize{indentExpr partialOrderType}" + return none + return some inst + +private def mkLinearOrderInst? (u : Level) (type : Expr) (leInst? ltInst? : Option Expr) : GoalM (Option Expr) := do + let some leInst := leInst? | return none + let some ltInst := ltInst? | return none + let linearOrderType := mkApp3 (mkConst ``Grind.LinearOrder [u]) type leInst ltInst + let some inst ← synthInstance? linearOrderType + | reportIssue! "type has `LE` and `LT`, but is not a linear order, failed to synthesize{indentExpr linearOrderType}" + return none + return some inst + +private def mkOrderedRingInst? (u : Level) (type : Expr) (semiringInst? leInst? ltInst? preorderInst? : Option Expr) : GoalM (Option Expr) := do let some semiringInst := semiringInst? | return none + let some leInst := leInst? | return none + let some ltInst := ltInst? | return none let some preorderInst := preorderInst? | return none - let isOrdType := mkApp3 (mkConst ``Grind.OrderedRing [u]) type semiringInst preorderInst + let isOrdType := mkApp5 (mkConst ``Grind.OrderedRing [u]) type semiringInst leInst ltInst preorderInst let some inst ← synthInstance? isOrdType | reportIssue! "type has a `Preorder` and is a `Semiring`, but is not an ordered ring, failed to synthesize{indentExpr isOrdType}" return none @@ -133,14 +162,16 @@ where synthInstance <| mkApp3 (mkConst ``HMul [0, u, u]) Int.mkType type type let rec getHMulNatInst : GoalM Expr := do synthInstance <| mkApp3 (mkConst ``HMul [0, u, u]) Nat.mkType type type - let rec checkToFieldDefEq? (parentInst? : Option Expr) (instDeclName : Name) (toFieldName : Name) : GoalM (Option Expr) := do + let rec checkToFieldDefEq? (leInst? ltInst? parentInst? childInst? : Option Expr) (toFieldName : Name) : GoalM (Option Expr) := do + let some leInst := leInst? | return none + let some ltInst := ltInst? | return none let some parentInst := parentInst? | return none - let some inst ← getInst? instDeclName | return none - let toField := mkApp2 (mkConst toFieldName [u]) type inst + let some childInst := childInst? | return none + let toField := mkApp4 (mkConst toFieldName [u]) type leInst ltInst childInst unless (← withDefault <| isDefEq parentInst toField) do reportIssue! (← mkExpectedDefEqMsg parentInst toField) return none - return some inst + return some childInst let rec ensureToFieldDefEq (parentInst : Expr) (inst : Expr) (toFieldName : Name) : GoalM Unit := do let toField := mkApp2 (mkConst toFieldName [u]) type inst ensureDefEq parentInst toField @@ -149,7 +180,11 @@ where let heteroToField := mkApp2 (mkConst toHeteroName [u]) type toField ensureDefEq parentInst heteroToField let ringId? ← CommRing.getRingId? type - let preorderInst? ← getInst? ``Grind.Preorder + let leInst? ← getInst? ``LE + let ltInst? ← getInst? ``LT + let preorderInst? ← mkPreorderInst? u type leInst? ltInst? + let partialInst? ← mkPartialOrderInst? u type leInst? ltInst? + let linearInst? ← mkLinearOrderInst? u type leInst? ltInst? if (← getConfig).ring && ringId?.isSome && preorderInst?.isNone then -- If `type` is a `CommRing`, but it is not even a preorder, there is no point in use this module. -- `ring` module should handle it. @@ -159,22 +194,22 @@ where let some intModuleInst ← mkIntModuleInst? u type ringInst? | return none let addInst ← getBinHomoInst ``HAdd let addFn ← internalizeFn <| mkApp4 (mkConst ``HAdd.hAdd [u, u, u]) type type type addInst - let orderedAddInst? ← if let some preorderInst := preorderInst? then - synthInstance? <| mkApp3 (mkConst ``Grind.OrderedAdd [u]) type addInst preorderInst - else - pure none + let orderedAddInst? ← match leInst?, ltInst?, preorderInst? with + | some leInst, some ltInst, some preorderInst => + synthInstance? <| mkApp5 (mkConst ``Grind.OrderedAdd [u]) type addInst leInst ltInst preorderInst + | _, _, _ => pure none let preorderInst? := if orderedAddInst?.isNone then none else preorderInst? -- preorderInst? may have been reset, check again whether this module is needed. if (← getConfig).ring && ringId?.isSome && preorderInst?.isNone then return none - let partialInst? ← checkToFieldDefEq? preorderInst? ``Grind.PartialOrder ``Grind.PartialOrder.toPreorder - let linearInst? ← checkToFieldDefEq? partialInst? ``Grind.LinearOrder ``Grind.LinearOrder.toPartialOrder + let partialInst? ← checkToFieldDefEq? leInst? ltInst? preorderInst? partialInst? ``Grind.PartialOrder.toPreorder + let linearInst? ← checkToFieldDefEq? leInst? ltInst? partialInst? linearInst? ``Grind.LinearOrder.toPartialOrder let addCommGroupInst := mkApp2 (mkConst ``Grind.IntModule.toAddCommGroup [u]) type intModuleInst let addCommMonoidInst := mkApp2 (mkConst ``Grind.AddCommGroup.toAddCommMonoid [u]) type addCommGroupInst let semiringInst? ← mkSemiringInst? u type ringInst? let fieldInst? ← getInst? ``Grind.Field let one? ← mkOne? u type -- One must be created eagerly - let orderedRingInst? ← mkOrderedRingInst? u type semiringInst? preorderInst? + let orderedRingInst? ← mkOrderedRingInst? u type semiringInst? leInst? ltInst? preorderInst? let charInst? ← if let some semiringInst := semiringInst? then getIsCharInst? u type semiringInst else pure none let noNatDivInst? ← mkNoNatZeroDivInst? u type -- TODO: generate the remaining fields on demand @@ -199,16 +234,14 @@ where ensureToFieldDefEq negInst addCommGroupInst ``Grind.AddCommGroup.toNeg ensureToFieldDefEq zsmulInst intModuleInst ``Grind.IntModule.zsmul ensureToFieldDefEq nsmulInst intModuleInst ``Grind.IntModule.nsmul - let (leFn?, ltFn?) ← if let some preorderInst := preorderInst? then - let leInst ← getInst ``LE - let ltInst ← getInst ``LT - let leFn ← internalizeFn <| mkApp2 (mkConst ``LE.le [u]) type leInst - let ltFn ← internalizeFn <| mkApp2 (mkConst ``LT.lt [u]) type ltInst - ensureToFieldDefEq leInst preorderInst ``Grind.Preorder.toLE - ensureToFieldDefEq ltInst preorderInst ``Grind.Preorder.toLT - pure (some leFn, some ltFn) + let leFn? ← if let some leInst := leInst? then + some <$> (internalizeFn <| mkApp2 (mkConst ``LE.le [u]) type leInst) else - pure (none, none) + pure none + let ltFn? ← if let some ltInst := ltInst? then + some <$> (internalizeFn <| mkApp2 (mkConst ``LT.lt [u]) type ltInst) + else + pure none let rec getHSMulFn? : GoalM (Option Expr) := do let smulType := mkApp3 (mkConst ``HSMul [0, u, u]) Int.mkType type type let some smulInst ← synthInstance? smulType | return none @@ -226,7 +259,7 @@ where pure none let id := (← get').structs.size let struct : Struct := { - id, type, u, intModuleInst, preorderInst?, orderedAddInst?, partialInst?, linearInst?, noNatDivInst? + id, type, u, intModuleInst, leInst?, ltInst?, preorderInst?, orderedAddInst?, partialInst?, linearInst?, noNatDivInst? leFn?, ltFn?, addFn, subFn, negFn, zsmulFn, nsmulFn, zsmulFn?, nsmulFn?, zero, one? ringInst?, commRingInst?, orderedRingInst?, charInst?, ringId?, fieldInst?, ofNatZero, homomulFn? } diff --git a/src/Lean/Meta/Tactic/Grind/Arith/Linear/Types.lean b/src/Lean/Meta/Tactic/Grind/Arith/Linear/Types.lean index be0538f469..451bc6326e 100644 --- a/src/Lean/Meta/Tactic/Grind/Arith/Linear/Types.lean +++ b/src/Lean/Meta/Tactic/Grind/Arith/Linear/Types.lean @@ -97,6 +97,10 @@ structure Struct where u : Level /-- `IntModule` instance -/ intModuleInst : Expr + /-- `LE` instance if available -/ + leInst? : Option Expr + /-- `LT` instance if available -/ + ltInst? : Option Expr /-- `Preorder` instance if available -/ preorderInst? : Option Expr /-- `OrderedAdd` instance with `Preorder` if available -/ diff --git a/src/Lean/Meta/Tactic/Grind/Arith/Linear/Util.lean b/src/Lean/Meta/Tactic/Grind/Arith/Linear/Util.lean index ee445de677..7f1c84a10e 100644 --- a/src/Lean/Meta/Tactic/Grind/Arith/Linear/Util.lean +++ b/src/Lean/Meta/Tactic/Grind/Arith/Linear/Util.lean @@ -124,6 +124,16 @@ def getNoNatDivInst : LinearM Expr := do | throwError "`grind linarith` internal error, structure does not implement `NoNatZeroDivisors`" return inst +def getLEInst : LinearM Expr := do + let some inst := (← getStruct).leInst? + | throwError "`grind linarith` internal error, structure does not support LE" + return inst + +def getLTInst : LinearM Expr := do + let some inst := (← getStruct).ltInst? + | throwError "`grind linarith` internal error, structure does not support LT" + return inst + def getPreorderInst : LinearM Expr := do let some inst := (← getStruct).preorderInst? | throwError "`grind linarith` internal error, structure is not a preorder" diff --git a/tests/lean/run/grind_cutsat_commring.lean b/tests/lean/run/grind_cutsat_commring.lean index e003c7c7f5..c86a3471cb 100644 --- a/tests/lean/run/grind_cutsat_commring.lean +++ b/tests/lean/run/grind_cutsat_commring.lean @@ -1,6 +1,6 @@ open Lean.Grind -variable [CommRing R] [LinearOrder R] [OrderedRing R] +variable [CommRing R] [LE R] [LT R] [LinearOrder R] [OrderedRing R] example (a b : R) (h : 0 ≤ a * b) : 0 ≤ b * a := by grind example (a b : R) (h : 7 ≤ a * b) : 7 ≤ b * a := by grind diff --git a/tests/lean/run/grind_field_div.lean b/tests/lean/run/grind_field_div.lean index 39c8568b49..5d2ba62e1d 100644 --- a/tests/lean/run/grind_field_div.lean +++ b/tests/lean/run/grind_field_div.lean @@ -67,7 +67,7 @@ example [Field α] {sqrtTwo a b c : α} : -- characteristic zero. #guard_msgs (trace) in set_option trace.grind.split true in -example [Field α] [LinearOrder α] [OrderedRing α] (x y z : α) +example [Field α] [LE α] [LT α] [LinearOrder α] [OrderedRing α] (x y z : α) : x > 0 → y > 0 → z > 0 → x * y * z ≥ 1 → (x ^ 2 - y * z) / (x ^ 2 + y ^ 2 + z ^ 2) + (y ^ 2 - z * x) / (y ^ 2 + z ^ 2 + x ^ 2) + (z ^ 2 - x * y) / (z ^ 2 + x ^ 2 + y ^ 2) = diff --git a/tests/lean/run/grind_linarith_1.lean b/tests/lean/run/grind_linarith_1.lean index e12e1bf905..75480e9aca 100644 --- a/tests/lean/run/grind_linarith_1.lean +++ b/tests/lean/run/grind_linarith_1.lean @@ -1,152 +1,156 @@ open Lean.Grind set_option grind.debug true -example [IntModule α] [Preorder α] [OrderedAdd α] (a b : α) +example [IntModule α] [LE α] [LT α] [Preorder α] [OrderedAdd α] (a b : α) : (2:Int)*a + b < b + a + a → False := by grind -example [IntModule α] [LinearOrder α] [OrderedAdd α] (a b : α) +example [IntModule α] [LE α] [LT α] [LinearOrder α] [OrderedAdd α] (a b : α) : (2:Int)*a + b < b + a + a → False := by grind -example [IntModule α] [Preorder α] [OrderedAdd α] (a b : α) +example [IntModule α] [LE α] [LT α] [Preorder α] [OrderedAdd α] (a b : α) : (2:Int)*a + b < b + a + a → False := by fail_if_success grind -linarith grind -example [IntModule α] [LinearOrder α] [OrderedAdd α] (a b : α) +example [IntModule α] [LE α] [LT α] [LinearOrder α] [OrderedAdd α] (a b : α) : (2:Int)*a + b ≥ b + a + a := by grind #guard_msgs (drop error) in -example [IntModule α] [Preorder α] [OrderedAdd α] (a b : α) +example [IntModule α] [LE α] [LT α] [Preorder α] [OrderedAdd α] (a b : α) : (2:Int)*a + b ≥ b + a + a := by fail_if_success grind -example [CommRing α] [Preorder α] [OrderedRing α] (a b : α) +example [CommRing α] [LE α] [LT α] [Preorder α] [OrderedRing α] (a b : α) : 2*a + b < b + a + a → False := by grind -example [CommRing α] [Preorder α] [OrderedRing α] (a b : α) +example [CommRing α] [LE α] [LT α] [Preorder α] [OrderedRing α] (a b : α) : 2 + 2*a + b + 1 < b + a + a + 3 → False := by grind -example [CommRing α] [LinearOrder α] [OrderedRing α] (a b : α) +example [CommRing α] [LE α] [LT α] [LinearOrder α] [OrderedRing α] (a b : α) : 2 + 2*a + b + 1 <= b + a + a + 3 := by grind -example [IntModule α] [Preorder α] [OrderedAdd α] (a b c : α) +example [IntModule α] [LE α] [LT α] [Preorder α] [OrderedAdd α] (a b c : α) : a < b → b < c → c < a → False := by grind -example [IntModule α] [LinearOrder α] [OrderedAdd α] (a b c : α) +example [IntModule α] [LE α] [LT α] [LinearOrder α] [OrderedAdd α] (a b c : α) : a < b → b < c → a < c := by grind -example [IntModule α] [LinearOrder α] [OrderedAdd α] (a b c : α) +example [IntModule α] [LE α] [LT α] [LinearOrder α] [OrderedAdd α] (a b c : α) : a < b → b ≤ c → a < c := by grind -example [IntModule α] [LinearOrder α] [OrderedAdd α] (a b c : α) +example [IntModule α] [LE α] [LT α] [LinearOrder α] [OrderedAdd α] (a b c : α) : a ≤ b → b ≤ c → a ≤ c := by grind -example [IntModule α] [LinearOrder α] [OrderedAdd α] (a b c d : α) +example [IntModule α] [LE α] [LT α] [LinearOrder α] [OrderedAdd α] (a b c d : α) : a < b → b < c + d → a - d < c := by grind -example [CommRing α] [LinearOrder α] [OrderedRing α] (a b c d : α) +example [CommRing α] [LE α] [LT α] [LinearOrder α] [OrderedRing α] (a b c d : α) : a < b → b < c + d → a - d < c := by grind -example [CommRing α] [Preorder α] [OrderedRing α] (a b c : α) +example [CommRing α] [LE α] [LT α] [Preorder α] [OrderedRing α] (a b c : α) : a < b → 2*b < c → c < 2*a → False := by grind -- Test misconfigured instances /-- -trace: [grind.issues] type has a `Preorder` and is a `Semiring`, but is not an ordered ring, failed to synthesize +trace: [grind.issues] type has `LE` and `LT`, but is not a partial order, failed to synthesize + PartialOrder α +[grind.issues] type has `LE` and `LT`, but is not a linear order, failed to synthesize + LinearOrder α +[grind.issues] type has a `Preorder` and is a `Semiring`, but is not an ordered ring, failed to synthesize OrderedRing α -/ #guard_msgs (drop error, trace) in set_option trace.grind.issues true in -example [CommRing α] [Preorder α] [OrderedAdd α] (a b c : α) +example [CommRing α] [LE α] [LT α] [Preorder α] [OrderedAdd α] (a b c : α) : a < b → b + b < c → c < a → False := by grind -example [CommRing α] [Preorder α] [OrderedRing α] (a b : α) +example [CommRing α] [LE α] [LT α] [Preorder α] [OrderedRing α] (a b : α) : a < 2 → b < a → b > 5 → False := by grind -example [CommRing α] [Preorder α] [OrderedRing α] (a b : α) +example [CommRing α] [LE α] [LT α] [Preorder α] [OrderedRing α] (a b : α) : a < One.one + 4 → b < a → b ≥ 5 → False := by grind -example [CommRing α] [Preorder α] [OrderedRing α] (a b : α) +example [CommRing α] [LE α] [LT α] [Preorder α] [OrderedRing α] (a b : α) : a < One.one + 5 → b < a → b ≥ 5 → False := by fail_if_success grind sorry -example [IntModule α] [Preorder α] [OrderedAdd α] (a b c d : α) +example [IntModule α] [LE α] [LT α] [Preorder α] [OrderedAdd α] (a b c d : α) : a < c → b = a + d → b - d > c → False := by grind -example [IntModule α] [Preorder α] [OrderedAdd α] (a b c d : α) +example [IntModule α] [LE α] [LT α] [Preorder α] [OrderedAdd α] (a b c d : α) : a + d < c → b = a + (2:Int)*d → b - d > c → False := by grind -example [CommRing α] [Preorder α] [OrderedRing α] (a b : α) +example [CommRing α] [LE α] [LT α] [Preorder α] [OrderedRing α] (a b : α) : a < 2 → b = a → b > 5 → False := by grind -example [CommRing α] [Preorder α] [OrderedRing α] (a b : α) +example [CommRing α] [LE α] [LT α] [Preorder α] [OrderedRing α] (a b : α) : a < 2 → a = b + b → b > 5 → False := by grind -example [CommRing α] [LinearOrder α] [OrderedRing α] (a b : α) +example [CommRing α] [LE α] [LT α] [LinearOrder α] [OrderedRing α] (a b : α) : a < 2 → a = b + b → b < 1 := by grind -example [CommRing α] [LinearOrder α] [OrderedRing α] (a b : α) +example [CommRing α] [LE α] [LT α] [LinearOrder α] [OrderedRing α] (a b : α) : a ≤ 2 → a + b = 3*b → b ≤ 1 := by grind -example [CommRing α] [LinearOrder α] [OrderedRing α] (a b c d e : α) : +example [CommRing α] [LE α] [LT α] [LinearOrder α] [OrderedRing α] (a b c d e : α) : 2*a + b ≥ 1 → b ≥ 0 → c ≥ 0 → d ≥ 0 → e ≥ 0 → a ≥ 3*c → c ≥ 6*e → d - e*5 ≥ 0 → a + b + 3*c + d + 2*e ≥ 0 := by grind -example [CommRing α] [Preorder α] [OrderedRing α] (a b c d e : α) : +example [CommRing α] [LE α] [LT α] [Preorder α] [OrderedRing α] (a b c d e : α) : 2*a + b ≥ 1 → b ≥ 0 → c ≥ 0 → d ≥ 0 → e ≥ 0 → a ≥ 3*c → c ≥ 6*e → d - e*5 ≥ 0 → a + b + 3*c + d + 2*e < 0 → False := by grind -example [CommRing α] [Preorder α] [OrderedRing α] (a b : α) +example [CommRing α] [LE α] [LT α] [Preorder α] [OrderedRing α] (a b : α) : a = 0 → b = 1 → a + b > 2 → False := by grind -example [CommRing α] [LinearOrder α] [OrderedRing α] (a b c : α) +example [CommRing α] [LE α] [LT α] [LinearOrder α] [OrderedRing α] (a b c : α) : a = 0 → a + b > 2 → b = c → 1 = c → False := by grind -example [CommRing α] [LinearOrder α] [OrderedRing α] (a b : α) +example [CommRing α] [LE α] [LT α] [LinearOrder α] [OrderedRing α] (a b : α) : a = 0 → b = 1 → a + b ≤ 2 := by grind -example [CommRing α] [LinearOrder α] [OrderedRing α] (a b : α) +example [CommRing α] [LE α] [LT α] [LinearOrder α] [OrderedRing α] (a b : α) : a*b + b*a > 1 → a*b > 0 := by grind -example [CommRing α] [LinearOrder α] [OrderedRing α] (a b c : α) +example [CommRing α] [LE α] [LT α] [LinearOrder α] [OrderedRing α] (a b c : α) : a*b + c > 1 → c = b*a → a*b > 0 := by grind -- It must not internalize subterms `b + c + d` and `b + b + d` #guard_msgs (trace) in set_option trace.grind.linarith.internalize true -example [CommRing α] [LinearOrder α] [OrderedRing α] (a b c d : α) +example [CommRing α] [LE α] [LT α] [LinearOrder α] [OrderedRing α] (a b c d : α) : a < b + c + d → c = b → a < b + b + d := by grind diff --git a/tests/lean/run/grind_linarith_2.lean b/tests/lean/run/grind_linarith_2.lean index 4114f77a43..22adf58268 100644 --- a/tests/lean/run/grind_linarith_2.lean +++ b/tests/lean/run/grind_linarith_2.lean @@ -1,7 +1,7 @@ open Lean Grind set_option grind.debug true -example [IntModule α] [Preorder α] [OrderedAdd α] (a b : α) +example [IntModule α] [LE α] [LT α] [Preorder α] [OrderedAdd α] (a b : α) : a + b = b + a := by grind @@ -22,7 +22,7 @@ trace: [grind.debug.proof] Classical.byContradiction fun h => #guard_msgs in open Linarith in set_option trace.grind.debug.proof true in -example [CommRing α] [Preorder α] [OrderedRing α] (a b : α) +example [CommRing α] [LE α] [LT α] [Preorder α] [OrderedRing α] (a b : α) : a + b = b + a := by grind -ring @@ -37,33 +37,33 @@ trace: [grind.debug.linarith.search.assign] One.one := 1 -/ #guard_msgs (drop error, trace) in set_option trace.grind.debug.linarith.search.assign true in -example [CommRing α] [LinearOrder α] [OrderedRing α] (a b c d : α) +example [CommRing α] [LE α] [LT α] [LinearOrder α] [OrderedRing α] (a b c d : α) : b ≥ 0 → c > b → d > b → a ≠ b + c → a > b + c → a < b + d → False := by grind -example [CommRing α] [LinearOrder α] [OrderedRing α] (a b c d : α) +example [CommRing α] [LE α] [LT α] [LinearOrder α] [OrderedRing α] (a b c d : α) : a ≤ b → a ≥ c + d → d = 0 → b = c → a = b := by grind -example [IntModule α] [LinearOrder α] [OrderedAdd α] (a b c d : α) +example [IntModule α] [LE α] [LT α] [LinearOrder α] [OrderedAdd α] (a b c d : α) : a ≤ b → a ≥ c + d → d ≤ 0 → d ≥ 0 → b = c → a = b := by grind open Linarith RArray set_option trace.grind.debug.proof true in -example [IntModule α] [LinearOrder α] [OrderedAdd α] (a b c d : α) +example [IntModule α] [LE α] [LT α] [LinearOrder α] [OrderedAdd α] (a b c d : α) : a ≤ b → a - c ≥ 0 + d → d ≤ 0 → d ≥ 0 → b = c → a ≠ b → False := by grind -example [CommRing α] [LinearOrder α] [OrderedRing α] (a b c : α) +example [CommRing α] [LE α] [LT α] [LinearOrder α] [OrderedRing α] (a b c : α) : a + 2*b = 0 → c + b = -b → a = c := by grind -example [CommRing α] [LinearOrder α] [OrderedRing α] (a b c : α) +example [CommRing α] [LE α] [LT α] [LinearOrder α] [OrderedRing α] (a b c : α) : a + 2*b = 0 → a = c → c + b = -b := by grind -example [CommRing α] [LinearOrder α] [OrderedRing α] (a b c : α) +example [CommRing α] [LE α] [LT α] [LinearOrder α] [OrderedRing α] (a b c : α) : c = a → a + b ≤ 3 → 3 ≤ b + c → a + b = 3 := by grind @@ -75,7 +75,7 @@ trace: [grind.linarith.model] a := 7/2 -/ #guard_msgs (drop error, trace) in set_option trace.grind.linarith.model true in -example [CommRing α] [LinearOrder α] [OrderedRing α] (a b c d : α) +example [CommRing α] [LE α] [LT α] [LinearOrder α] [OrderedRing α] (a b c d : α) : b ≥ 0 → c > b → d > b → a ≠ b + c → a > b + c → a < b + d → False := by grind @@ -87,24 +87,24 @@ trace: [grind.linarith.model] a := 0 -/ #guard_msgs (drop error, trace) in set_option trace.grind.linarith.model true in -example [IntModule α] [LinearOrder α] [OrderedAdd α] (a b c d : α) +example [IntModule α] [LE α] [LT α] [LinearOrder α] [OrderedAdd α] (a b c d : α) : a ≤ b → a - c ≥ 0 + d → d ≤ 0 → b = c → a ≠ b → False := by grind /-- trace: [grind.split] x = 0, generation: 0 -/ #guard_msgs (trace) in set_option trace.grind.split true in -example [IntModule α] [LinearOrder α] [OrderedAdd α] (f : α → α) (x : α) +example [IntModule α] [LE α] [LT α] [LinearOrder α] [OrderedAdd α] (f : α → α) (x : α) : Zero.zero ≤ x → x ≤ 0 → f x = a → f 0 = a := by grind -- should not split on `x = 0` since `α` is not a linear order #guard_msgs (drop error, trace) in set_option trace.grind.split true in -example [IntModule α] [Preorder α] [OrderedAdd α] (f : α → α) (x : α) +example [IntModule α] [LE α] [LT α] [Preorder α] [OrderedAdd α] (f : α → α) (x : α) : Zero.zero ≤ x → x ≤ 0 → f x = a → f 0 = a := by grind -example [CommRing α] [LinearOrder α] [OrderedRing α] (f : α → α → α) (x y z : α) +example [CommRing α] [LE α] [LT α] [LinearOrder α] [OrderedRing α] (f : α → α → α) (x y z : α) : z ≤ x → x ≤ 1 → z = 1 → f x y = 2 → f 1 y = 2 := by grind diff --git a/tests/lean/run/grind_ord_module.lean b/tests/lean/run/grind_ord_module.lean index 6e7308916a..c790ffccc8 100644 --- a/tests/lean/run/grind_ord_module.lean +++ b/tests/lean/run/grind_ord_module.lean @@ -1,6 +1,6 @@ open Lean.Grind -variable (R : Type u) [IntModule R] [LinearOrder R] [OrderedAdd R] +variable (R : Type u) [IntModule R] [LE R] [LT R] [LinearOrder R] [OrderedAdd R] example (a b c : R) (h : a < b) : a + c < b + c := by grind example (a b c : R) (h : a < b) : c + a < c + b := by grind diff --git a/tests/lean/run/grind_preord_module.lean b/tests/lean/run/grind_preord_module.lean index d93d7e27aa..733b06ac20 100644 --- a/tests/lean/run/grind_preord_module.lean +++ b/tests/lean/run/grind_preord_module.lean @@ -1,7 +1,7 @@ open Lean.Grind -- `grind linarith` currently does not support negation of linear constraints. -variable (R : Type u) [IntModule R] [Preorder R] [OrderedAdd R] +variable (R : Type u) [IntModule R] [LE R] [LT R] [Preorder R] [OrderedAdd R] example (a b : R) (_ : a < b) (_ : b < a) : False := by grind example (a b : R) (_ : a < b ∧ b < a) : False := by grind diff --git a/tests/lean/run/grind_ring_1.lean b/tests/lean/run/grind_ring_1.lean index c11df64992..7030ae49fb 100644 --- a/tests/lean/run/grind_ring_1.lean +++ b/tests/lean/run/grind_ring_1.lean @@ -91,6 +91,6 @@ trace: [grind.ring.assert.basis] a ^ 2 * b + -1 = 0 -/ #guard_msgs (drop error, trace) in set_option trace.grind.ring.assert.basis true in -example [CommRing α] [Preorder α] [OrderedRing α] (a b c : α) +example [CommRing α] [LE α] [LT α] [Preorder α] [OrderedRing α] (a b c : α) : a^2*b = 1 → a*b^2 = b → False := by grind diff --git a/tests/lean/run/info_trees.lean b/tests/lean/run/info_trees.lean index c0476accf6..0ecb89653a 100644 --- a/tests/lean/run/info_trees.lean +++ b/tests/lean/run/info_trees.lean @@ -61,7 +61,7 @@ info: • [Command] @ ⟨83, 0⟩-⟨83, 40⟩ @ Lean.Elab.Command.elabDeclarati ⊢ 0 ≤ n after no goals • [Term] Nat.zero_le n : 0 ≤ n @ ⟨1, 1⟩†-⟨1, 1⟩† @ Lean.Elab.Term.elabApp - • [Completion-Id] Nat.zero_le : some LE.le.{0} Nat instLENat (OfNat.ofNat.{0} Nat 0 (instOfNatNat 0)) _uniq.42 @ ⟨1, 0⟩†-⟨1, 0⟩† + • [Completion-Id] Nat.zero_le : some LE.le.{0} Nat instLENat (OfNat.ofNat.{0} Nat 0 (instOfNatNat 0)) _uniq.41 @ ⟨1, 0⟩†-⟨1, 0⟩† • [Term] Nat.zero_le : ∀ (n : Nat), 0 ≤ n @ ⟨1, 0⟩†-⟨1, 0⟩† • [Term] n : Nat @ ⟨1, 5⟩†-⟨1, 5⟩† @ Lean.Elab.Term.elabIdent • [Completion-Id] n : some Nat @ ⟨1, 5⟩†-⟨1, 5⟩†