feat: make Lean.Grind.Preorder a mixin (#9885)
This PR is initially motivated by noticing `Lean.Grind.Preorder.toLE` appearing in long Mathlib typeclass searches; this change will prevent these searches. These changes are also helpful preparation for potentially dropping the custom `Lean.Grind.*` typeclasses, and unifying with the new typeclasses introduced in #9729.
This commit is contained in:
Kim Morrison
GitHub
parent
21fa5d10f4
commit
93e0ebf25c
21 changed files with 230 additions and 161 deletions
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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 =>
|
||||
|
|
|
|||
|
|
@ -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)
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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?
|
||||
}
|
||||
|
|
|
|||
|
|
@ -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 -/
|
||||
|
|
|
|||
|
|
@ -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"
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
||||
|
|
|
|||
|
|
@ -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) =
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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⟩†
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue