refactor: add denote' functions to Int/Linear.lean (#7094)
This PR adds the functions `Poly.denote'`, `RelCnstr.denote'`, and `DvdCnstr.denote'`. These functions are useful for representing the denotation of normalized results in `simp +arith` and the `grind` preprocessor. This PR also adjusts all auxiliary normalization theorems to use them to represent the normalized constraints. Previously, we were converting `RelCnstr` and `DvdCnstr` back into raw constraints. While this overhead was reasonable for `simp +arith`, it is not for the cutsat procedure, which has no need for raw constraints. All constraints have already been normalized by the time they reach cutsat.
This commit is contained in:
Leonardo de Moura
GitHub
parent
ecdc2d57f2
commit
747ea91c3a
5 changed files with 210 additions and 73 deletions
|
|
@ -11,6 +11,7 @@ import Init.Data.Int.LemmasAux
|
|||
import Init.Data.Int.DivModLemmas
|
||||
import Init.Data.Int.Gcd
|
||||
import Init.Data.RArray
|
||||
import Init.Data.AC
|
||||
|
||||
namespace Int.Linear
|
||||
|
||||
|
|
@ -51,6 +52,32 @@ def Poly.denote (ctx : Context) (p : Poly) : Int :=
|
|||
| .num k => k
|
||||
| .add k v p => Int.add (Int.mul k (v.denote ctx)) (denote ctx p)
|
||||
|
||||
/--
|
||||
Similar to `Poly.denote`, but produces a denotation better for `simp +arith`.
|
||||
Remark: we used to convert `Poly` back into `Expr` to achieve that.
|
||||
-/
|
||||
def Poly.denote' (ctx : Context) (p : Poly) : Int :=
|
||||
match p with
|
||||
| .num k => k
|
||||
| .add 1 v p => go (v.denote ctx) p
|
||||
| .add k v p => go (Int.mul k (v.denote ctx)) p
|
||||
where
|
||||
go (r : Int) (p : Poly) : Int :=
|
||||
match p with
|
||||
| .num 0 => r
|
||||
| .num k => Int.add r k
|
||||
| .add 1 v p => go (Int.add r (v.denote ctx)) p
|
||||
| .add k v p => go (Int.add r (Int.mul k (v.denote ctx))) p
|
||||
|
||||
theorem Poly.denote'_go_eq_denote (ctx : Context) (p : Poly) (r : Int) : denote'.go ctx r p = p.denote ctx + r := by
|
||||
induction r, p using denote'.go.induct ctx <;> simp [denote'.go, denote]
|
||||
next => rw [Int.add_comm]
|
||||
next ih => simp [denote'.go] at ih; rw [ih]; ac_rfl
|
||||
next ih => simp [denote'.go] at ih; rw [ih]; ac_rfl
|
||||
|
||||
theorem Poly.denote'_eq_denote (ctx : Context) (p : Poly) : p.denote' ctx = p.denote ctx := by
|
||||
unfold denote' <;> split <;> simp [denote, denote'_go_eq_denote] <;> ac_rfl
|
||||
|
||||
def Poly.addConst (p : Poly) (k : Int) : Poly :=
|
||||
match p with
|
||||
| .num k' => .num (k+k')
|
||||
|
|
@ -105,6 +132,13 @@ def RelCnstr.denote (ctx : Context) : RelCnstr → Prop
|
|||
| .eq p => p.denote ctx = 0
|
||||
| .le p => p.denote ctx ≤ 0
|
||||
|
||||
def RelCnstr.denote' (ctx : Context) : RelCnstr → Prop
|
||||
| .eq p => p.denote' ctx = 0
|
||||
| .le p => p.denote' ctx ≤ 0
|
||||
|
||||
theorem RelCnstr.denote'_eq_denote (ctx : Context) (c : RelCnstr) : c.denote' ctx = c.denote ctx := by
|
||||
cases c <;> simp [denote, denote', Poly.denote'_eq_denote]
|
||||
|
||||
/--
|
||||
Returns the ceiling of the division `a / b`. That is, the result is equivalent to `⌈a / b⌉`.
|
||||
Examples:
|
||||
|
|
@ -202,6 +236,18 @@ def Poly.divCoeffs (k : Int) : Poly → Bool
|
|||
| .num _ => true
|
||||
| .add k' _ p => k' % k == 0 && divCoeffs k p
|
||||
|
||||
/--
|
||||
`p.mul k` multiplies all coefficients and constant of the polynomial `p` by `k`.
|
||||
-/
|
||||
def Poly.mul (p : Poly) (k : Int) : Poly :=
|
||||
match p with
|
||||
| .num k' => .num (k*k')
|
||||
| .add k' v p => .add (k*k') v (mul p k)
|
||||
|
||||
@[simp] theorem Poly.denote_mul (ctx : Context) (p : Poly) (k : Int) : (p.mul k).denote ctx = k * p.denote ctx := by
|
||||
induction p <;> simp [mul, denote, *]
|
||||
rw [Int.mul_assoc, Int.mul_add]
|
||||
|
||||
/-- Normalizes the polynomial of the given relational constraint. -/
|
||||
def RelCnstr.norm : RelCnstr → RelCnstr
|
||||
| .eq p => .eq p.norm
|
||||
|
|
@ -228,6 +274,30 @@ def RelCnstr.div (k : Int) : RelCnstr → RelCnstr
|
|||
| .eq p => .eq <| p.div k
|
||||
| .le p => .le <| p.div k
|
||||
|
||||
/--
|
||||
Multiplies all coefficients and constants in the linear polynomial of the given constraint by `k`.
|
||||
-/
|
||||
def RelCnstr.mul (k : Int) : RelCnstr → RelCnstr
|
||||
| .eq p => .eq <| p.mul k
|
||||
| .le p => .le <| p.mul k
|
||||
|
||||
@[simp] theorem RelCnstr.denote_mul (ctx : Context) (c : RelCnstr) (k : Int) (h : k > 0) : (c.mul k).denote ctx = c.denote ctx := by
|
||||
cases c <;> simp [mul, denote]
|
||||
next =>
|
||||
constructor
|
||||
· intro h₁; cases (Int.mul_eq_zero.mp h₁)
|
||||
next hz => simp [hz] at h
|
||||
next => assumption
|
||||
· intro h'; simp [*]
|
||||
next =>
|
||||
constructor
|
||||
· intro h₁
|
||||
conv at h₁ => rhs; rw [← Int.mul_zero k]
|
||||
exact Int.le_of_mul_le_mul_left h₁ h
|
||||
· intro h₂
|
||||
have := Int.mul_le_mul_of_nonneg_left h₂ (Int.le_of_lt h)
|
||||
simp at this; assumption
|
||||
|
||||
/-- Raw relational constraint. They are later converted into `RelCnstr`. -/
|
||||
inductive RawRelCnstr where
|
||||
| eq (p₁ p₂ : Expr)
|
||||
|
|
@ -248,8 +318,8 @@ def RawRelCnstr.norm : RawRelCnstr → RelCnstr
|
|||
| .le e₁ e₂ => .le (e₁.sub e₂).toPoly.norm
|
||||
|
||||
/-- A certificate for normalizing the coefficients of a raw relational constraint. -/
|
||||
def divBy (e e' : RawRelCnstr) (k : Int) : Bool :=
|
||||
k > 0 && e.norm.divAll k && e'.norm == e.norm.div k
|
||||
def divBy (c : RawRelCnstr) (c' : RelCnstr) (k : Int) : Bool :=
|
||||
k > 0 && c.norm == c'.mul k
|
||||
|
||||
attribute [local simp] Int.add_comm Int.add_assoc Int.add_left_comm Int.add_mul Int.mul_add
|
||||
attribute [local simp] Poly.insert Poly.denote Poly.norm Poly.addConst
|
||||
|
|
@ -371,10 +441,10 @@ theorem Expr.eq_of_toPoly_eq (ctx : Context) (e e' : Expr) (h : e.toPoly == e'.t
|
|||
simp [Poly.norm] at h
|
||||
assumption
|
||||
|
||||
theorem RawRelCnstr.eq_of_norm_eq (ctx : Context) (c c' : RawRelCnstr) (h : c.norm == c'.norm) : c.denote ctx = c'.denote ctx := by
|
||||
theorem RawRelCnstr.eq_of_norm_eq (ctx : Context) (c : RawRelCnstr) (c' : RelCnstr) (h : c.norm == c') : c.denote ctx = c'.denote' ctx := by
|
||||
have h := congrArg (RelCnstr.denote ctx) (eq_of_beq h)
|
||||
rw [denote_norm, denote_norm] at h
|
||||
assumption
|
||||
rw [denote_norm] at h
|
||||
rw [RelCnstr.denote'_eq_denote, h]
|
||||
|
||||
theorem RawRelCnstr.eq_of_norm_eq_var (ctx : Context) (x y : Var) (c : RawRelCnstr) (h : c.norm == .eq (.add 1 x (.add (-1) y (.num 0))))
|
||||
: c.denote ctx = (x.denote ctx = y.denote ctx) := by
|
||||
|
|
@ -411,39 +481,19 @@ private theorem eq_mul_le_zero {a b : Int} : 0 < b → (a ≤ 0 ↔ a * b ≤ 0)
|
|||
rw [this] at h'
|
||||
exact Int.le_of_mul_le_mul_right h' h
|
||||
|
||||
attribute [local simp] RelCnstr.divAll RelCnstr.div
|
||||
attribute [local simp] RelCnstr.divAll RelCnstr.div RelCnstr.mul
|
||||
|
||||
theorem RawRelCnstr.eq_of_norm_eq_of_divBy' (ctx : Context) (c c' : RawRelCnstr) (p : RelCnstr) (k : Int)
|
||||
: k > 0 → p.divAll k → c.norm = p → c'.norm = p.div k → c.denote ctx = c'.denote ctx := by
|
||||
intro h₀ h₁ h₂ h₃
|
||||
have hz : k ≠ 0 := Int.ne_of_gt h₀
|
||||
cases p <;> simp at h₁
|
||||
next p =>
|
||||
replace h₁ := Poly.denote_div_eq_of_divAll ctx p k h₁
|
||||
replace h₂ := congrArg (RelCnstr.denote ctx) h₂
|
||||
simp only [RelCnstr.denote.eq_1, ← h₁] at h₂
|
||||
replace h₃ := congrArg (RelCnstr.denote ctx) h₃
|
||||
simp only [RelCnstr.denote.eq_1, RelCnstr.div] at h₃
|
||||
rw [mul_eq_zero_iff_eq_zero _ _ hz] at h₂
|
||||
have := Eq.trans h₂ h₃.symm
|
||||
rw [denote_norm, denote_norm] at this
|
||||
exact this
|
||||
next p =>
|
||||
replace h₁ := Poly.denote_div_eq_of_divAll ctx p k h₁
|
||||
replace h₂ := congrArg (RelCnstr.denote ctx) h₂
|
||||
simp only [RelCnstr.denote.eq_2, ← h₁] at h₂
|
||||
replace h₃ := congrArg (RelCnstr.denote ctx) h₃
|
||||
simp only [RelCnstr.denote.eq_2, RelCnstr.div] at h₃
|
||||
rw [eq_mul_le_zero h₀] at h₃
|
||||
have := Eq.trans h₂ h₃.symm
|
||||
rw [denote_norm, denote_norm] at this
|
||||
exact this
|
||||
theorem RawRelCnstr.eq_of_norm_eq_mul (ctx : Context) (c : RawRelCnstr) (c' : RelCnstr) (k : Int) (hz : k > 0) (h : c.norm = c'.mul k) : c.denote ctx = c'.denote ctx := by
|
||||
replace h := congrArg (RelCnstr.denote ctx) h
|
||||
simp only [RawRelCnstr.denote_norm, RelCnstr.denote_mul, *] at h
|
||||
assumption
|
||||
|
||||
theorem RawRelCnstr.eq_of_divBy (ctx : Context) (e e' : RawRelCnstr) (k : Int) : divBy e e' k → e.denote ctx = e'.denote ctx := by
|
||||
theorem RawRelCnstr.eq_of_divBy (ctx : Context) (c : RawRelCnstr) (c' : RelCnstr) (k : Int) : divBy c c' k → c.denote ctx = c'.denote' ctx := by
|
||||
intro h
|
||||
simp only [RelCnstr.denote'_eq_denote]
|
||||
simp only [divBy, Bool.and_eq_true, bne_iff_ne, ne_eq, beq_iff_eq, decide_eq_true_eq] at h
|
||||
have ⟨⟨h₁, h₂⟩, h₃⟩ := h
|
||||
exact eq_of_norm_eq_of_divBy' ctx e e' e.norm k h₁ h₂ rfl h₃
|
||||
have ⟨h₁, h₂⟩ := h
|
||||
exact eq_of_norm_eq_mul ctx c c' k h₁ h₂
|
||||
|
||||
private theorem mul_add_cmod_le_iff {a k b : Int} (h : k > 0) : a*k + cmod b k ≤ 0 ↔ a ≤ 0 := by
|
||||
constructor
|
||||
|
|
@ -469,11 +519,11 @@ private theorem mul_add_cmod_le_iff {a k b : Int} (h : k > 0) : a*k + cmod b k
|
|||
simp at this
|
||||
assumption
|
||||
|
||||
theorem RawRelCnstr.eq_of_norm_eq_of_divCoeffs (ctx : Context) (c c' : RawRelCnstr) (p : RelCnstr) (k : Int)
|
||||
: k > 0 → p.divCoeffs k → p.isLe → c.norm = p → c'.norm = p.div k → c.denote ctx = c'.denote ctx := by
|
||||
theorem RawRelCnstr.eq_of_norm_eq_of_divCoeffs (ctx : Context) (c₁ : RawRelCnstr) (c₂ : RelCnstr) (c₃ : RelCnstr) (k : Int)
|
||||
: k > 0 → c₂.divCoeffs k → c₂.isLe → c₁.norm = c₂ → c₃ = c₂.div k → c₁.denote ctx = c₃.denote ctx := by
|
||||
intro h₀ h₁ h₂ h₃ h₄
|
||||
have hz : k ≠ 0 := Int.ne_of_gt h₀
|
||||
cases p <;> simp [RelCnstr.isLe] at h₂
|
||||
cases c₂ <;> simp [RelCnstr.isLe] at h₂
|
||||
clear h₂
|
||||
next p =>
|
||||
simp [RelCnstr.divCoeffs] at h₁
|
||||
|
|
@ -482,24 +532,25 @@ theorem RawRelCnstr.eq_of_norm_eq_of_divCoeffs (ctx : Context) (c c' : RawRelCns
|
|||
simp only [RelCnstr.denote.eq_2, ← h₁] at h₃
|
||||
replace h₄ := congrArg (RelCnstr.denote ctx) h₄
|
||||
simp only [RelCnstr.denote.eq_2, RelCnstr.div] at h₄
|
||||
rw [denote_norm] at h₃ h₄
|
||||
rw [denote_norm] at h₃
|
||||
rw [h₃, h₄]
|
||||
apply propext
|
||||
apply mul_add_cmod_le_iff
|
||||
exact h₀
|
||||
|
||||
/-- Certificate for normalizing the coefficients of inequality constraint with bound tightening. -/
|
||||
def divByLe (c c' : RawRelCnstr) (k : Int) : Bool :=
|
||||
k > 0 && c.isLe && c.norm.divCoeffs k && c'.norm == c.norm.div k
|
||||
def divByLe (c : RawRelCnstr) (c' : RelCnstr) (k : Int) : Bool :=
|
||||
k > 0 && c.isLe && c.norm.divCoeffs k && c' == c.norm.div k
|
||||
|
||||
theorem RawRelCnstr.eq_of_divByLe (ctx : Context) (c c' : RawRelCnstr) (k : Int) : divByLe c c' k → c.denote ctx = c'.denote ctx := by
|
||||
theorem RawRelCnstr.eq_of_divByLe (ctx : Context) (c : RawRelCnstr) (c' : RelCnstr) (k : Int) : divByLe c c' k → c.denote ctx = c'.denote' ctx := by
|
||||
intro h
|
||||
simp only [RelCnstr.denote'_eq_denote]
|
||||
simp only [divByLe, Bool.and_eq_true, bne_iff_ne, ne_eq, beq_iff_eq, decide_eq_true_eq] at h
|
||||
have ⟨⟨⟨h₀, h₁⟩, h₂⟩, h₃⟩ := h
|
||||
have hle : c.norm.isLe := by
|
||||
cases c <;> simp [RawRelCnstr.isLe] at h₁
|
||||
simp [RelCnstr.isLe]
|
||||
apply eq_of_norm_eq_of_divCoeffs ctx c c' c.norm k h₀ h₂ hle rfl h₃
|
||||
apply eq_of_norm_eq_of_divCoeffs ctx c c.norm c' k h₀ h₂ hle rfl h₃
|
||||
|
||||
def RelCnstr.isUnsat : RelCnstr → Bool
|
||||
| .eq (.num k) => k != 0
|
||||
|
|
@ -606,15 +657,6 @@ theorem Poly.gcd_dvd_const {ctx : Context} {p : Poly} {k : Int} (h : k ∣ p.den
|
|||
rw [Int.add_comm] at h
|
||||
exact ih (gcd_dvd_step h)
|
||||
|
||||
def Poly.mul (p : Poly) (k : Int) : Poly :=
|
||||
match p with
|
||||
| .num k' => .num (k*k')
|
||||
| .add k' v p => .add (k*k') v (mul p k)
|
||||
|
||||
@[simp] theorem Poly.denote_mul (ctx : Context) (p : Poly) (k : Int) : (p.mul k).denote ctx = k * p.denote ctx := by
|
||||
induction p <;> simp [mul, *]
|
||||
rw [Int.mul_assoc]
|
||||
|
||||
/-- Divibility constraint of the form `k ∣ p`. -/
|
||||
structure DvdCnstr where
|
||||
k : Int
|
||||
|
|
@ -623,6 +665,12 @@ structure DvdCnstr where
|
|||
def DvdCnstr.denote (ctx : Context) (c : DvdCnstr) : Prop :=
|
||||
c.k ∣ c.p.denote ctx
|
||||
|
||||
def DvdCnstr.denote' (ctx : Context) (c : DvdCnstr) : Prop :=
|
||||
c.k ∣ c.p.denote' ctx
|
||||
|
||||
theorem DvdCnstr.denote'_eq_denote (ctx : Context) (c : DvdCnstr) : c.denote' ctx = c.denote ctx := by
|
||||
simp [denote', denote, Poly.denote'_eq_denote]
|
||||
|
||||
def DvdCnstr.isUnsat (c : DvdCnstr) : Bool :=
|
||||
c.p.getConst % c.p.gcdCoeffs c.k != 0
|
||||
|
||||
|
|
@ -679,14 +727,14 @@ def RawDvdCnstr.norm (c : RawDvdCnstr) : DvdCnstr :=
|
|||
@[simp] theorem RawDvdCnstr.denote_norm_eq (ctx : Context) (c : RawDvdCnstr) : c.denote ctx = c.norm.denote ctx := by
|
||||
simp [norm, denote, DvdCnstr.denote]
|
||||
|
||||
def RawDvdCnstr.isEqv (c₁ c₂ : RawDvdCnstr) (k : Int) : Bool :=
|
||||
c₁.norm.isEqv c₂.norm k
|
||||
def RawDvdCnstr.isEqv (c : RawDvdCnstr) (c' : DvdCnstr) (k : Int) : Bool :=
|
||||
c.norm.isEqv c' k
|
||||
|
||||
def RawDvdCnstr.isUnsat (c : RawDvdCnstr) : Bool :=
|
||||
c.norm.isUnsat
|
||||
|
||||
theorem RawDvdCnstr.eq_of_isEqv (ctx : Context) (c₁ c₂ : RawDvdCnstr) (k : Int) (h : isEqv c₁ c₂ k) : c₁.denote ctx = c₂.denote ctx := by
|
||||
simp [DvdCnstr.eq_of_isEqv ctx c₁.norm c₂.norm k h]
|
||||
theorem RawDvdCnstr.eq_of_isEqv (ctx : Context) (c : RawDvdCnstr) (c' : DvdCnstr) (k : Int) (h : isEqv c c' k) : c.denote ctx = c'.denote' ctx := by
|
||||
simp [DvdCnstr.eq_of_isEqv ctx c.norm c' k h, DvdCnstr.denote'_eq_denote]
|
||||
|
||||
theorem RawDvdCnstr.eq_false_of_isUnsat (ctx : Context) (c : RawDvdCnstr) (h : c.isUnsat) : c.denote ctx = False := by
|
||||
simp [DvdCnstr.eq_false_of_isUnsat ctx c.norm h]
|
||||
|
|
|
|||
|
|
@ -68,10 +68,36 @@ end Int.Linear
|
|||
|
||||
namespace Lean.Meta.Linear.Int
|
||||
|
||||
def ofPoly (p : Int.Linear.Poly) : Expr :=
|
||||
open Int.Linear.Poly in
|
||||
match p with
|
||||
| .num v => mkApp (mkConst ``num) (toExpr v)
|
||||
| .add k v p => mkApp3 (mkConst ``add) (toExpr k) (toExpr v) (ofPoly p)
|
||||
|
||||
instance : ToExpr Int.Linear.Poly where
|
||||
toExpr a := ofPoly a
|
||||
toTypeExpr := mkConst ``Int.Linear.Poly
|
||||
|
||||
def ofRelCnstr (c : Int.Linear.RelCnstr) : Expr :=
|
||||
match c with
|
||||
| .eq p => mkApp (mkConst ``Int.Linear.RelCnstr.eq) (toExpr p)
|
||||
| .le p => mkApp (mkConst ``Int.Linear.RelCnstr.le) (toExpr p)
|
||||
|
||||
instance : ToExpr Int.Linear.RelCnstr where
|
||||
toExpr a := ofRelCnstr a
|
||||
toTypeExpr := mkConst ``Int.Linear.RelCnstr
|
||||
|
||||
def ofDvdCnstr (c : Int.Linear.DvdCnstr) : Expr :=
|
||||
mkApp2 (mkConst ``Int.Linear.DvdCnstr.mk) (toExpr c.k) (toExpr c.p)
|
||||
|
||||
instance : ToExpr Int.Linear.DvdCnstr where
|
||||
toExpr a := ofDvdCnstr a
|
||||
toTypeExpr := mkConst ``Int.Linear.DvdCnstr
|
||||
|
||||
def ofLinearExpr (e : Int.Linear.Expr) : Expr :=
|
||||
open Int.Linear.Expr in
|
||||
match e with
|
||||
| .num v => mkApp (mkConst ``num) (Lean.toExpr v)
|
||||
| .num v => mkApp (mkConst ``num) (toExpr v)
|
||||
| .var i => mkApp (mkConst ``var) (mkNatLit i)
|
||||
| .neg a => mkApp (mkConst ``neg) (ofLinearExpr a)
|
||||
| .add a b => mkApp2 (mkConst ``add) (ofLinearExpr a) (ofLinearExpr b)
|
||||
|
|
@ -117,6 +143,27 @@ def _root_.Int.Linear.RawRelCnstr.denoteExpr (ctx : Array Expr) (c : Int.Linear.
|
|||
def _root_.Int.Linear.RawDvdCnstr.denoteExpr (ctx : Array Expr) (c : Int.Linear.RawDvdCnstr) : MetaM Expr := do
|
||||
return mkIntDvd (mkIntLit c.k) (← c.e.denoteExpr ctx)
|
||||
|
||||
def _root_.Int.Linear.Poly.denoteExpr (ctx : Array Expr) (p : Int.Linear.Poly) : MetaM Expr := do
|
||||
match p with
|
||||
| .num k => return toExpr k
|
||||
| .add 1 x p => go ctx[x]! p
|
||||
| .add k x p => go (mkIntMul (toExpr k) ctx[x]!) p
|
||||
where
|
||||
go (r : Expr) (p : Int.Linear.Poly) : MetaM Expr :=
|
||||
match p with
|
||||
| .num 0 => return r
|
||||
| .num k => return mkIntAdd r (toExpr k)
|
||||
| .add 1 x p => go (mkIntAdd r ctx[x]!) p
|
||||
| .add k x p => go (mkIntAdd r (mkIntMul (toExpr k) ctx[x]!)) p
|
||||
|
||||
def _root_.Int.Linear.RelCnstr.denoteExpr (ctx : Array Expr) (c : Int.Linear.RelCnstr) : MetaM Expr := do
|
||||
match c with
|
||||
| .eq p => return mkIntEq (← p.denoteExpr ctx) (mkIntLit 0)
|
||||
| .le p => return mkIntLE (← p.denoteExpr ctx) (mkIntLit 0)
|
||||
|
||||
def _root_.Int.Linear.DvdCnstr.denoteExpr (ctx : Array Expr) (c : Int.Linear.DvdCnstr) : MetaM Expr := do
|
||||
return mkIntDvd (mkIntLit c.k) (← c.p.denoteExpr ctx)
|
||||
|
||||
namespace ToLinear
|
||||
|
||||
structure State where
|
||||
|
|
|
|||
|
|
@ -47,19 +47,18 @@ def simpRelCnstrPos? (e : Expr) : MetaM (Option (Expr × Expr)) := do
|
|||
let some (c, atoms) ← toRawRelCnstr? e | return none
|
||||
withAbstractAtoms atoms ``Int fun atoms => do
|
||||
let lhs ← c.denoteExpr atoms
|
||||
let p := c.norm
|
||||
if p.isUnsat then
|
||||
let c' := c.norm
|
||||
if c'.isUnsat then
|
||||
let r := mkConst ``False
|
||||
let h := mkApp3 (mkConst ``Int.Linear.RawRelCnstr.eq_false_of_isUnsat) (toContextExpr atoms) (toExpr c) reflBoolTrue
|
||||
return some (r, ← mkExpectedTypeHint h (← mkEq lhs r))
|
||||
else if p.isValid then
|
||||
else if c'.isValid then
|
||||
let r := mkConst ``True
|
||||
let h := mkApp3 (mkConst ``Int.Linear.RawRelCnstr.eq_true_of_isValid) (toContextExpr atoms) (toExpr c) reflBoolTrue
|
||||
return some (r, ← mkExpectedTypeHint h (← mkEq lhs r))
|
||||
else
|
||||
let c' := p.toRaw
|
||||
if c != c' then
|
||||
match p with
|
||||
if c != c'.toRaw then
|
||||
match c' with
|
||||
| .eq (.add 1 x (.add (-1) y (.num 0))) =>
|
||||
let r := mkIntEq atoms[x]! atoms[y]!
|
||||
let h := mkApp5 (mkConst ``Int.Linear.RawRelCnstr.eq_of_norm_eq_var) (toContextExpr atoms) (toExpr x) (toExpr y) (toExpr c) reflBoolTrue
|
||||
|
|
@ -69,23 +68,23 @@ def simpRelCnstrPos? (e : Expr) : MetaM (Option (Expr × Expr)) := do
|
|||
let h := mkApp5 (mkConst ``Int.Linear.RawRelCnstr.eq_of_norm_eq_const) (toContextExpr atoms) (toExpr x) (toExpr (-k)) (toExpr c) reflBoolTrue
|
||||
return some (r, ← mkExpectedTypeHint h (← mkEq lhs r))
|
||||
| _ =>
|
||||
let k := p.gcdCoeffs
|
||||
let k := c'.gcdCoeffs
|
||||
if k == 1 then
|
||||
let r ← c'.denoteExpr atoms
|
||||
let h := mkApp4 (mkConst ``Int.Linear.RawRelCnstr.eq_of_norm_eq) (toContextExpr atoms) (toExpr c) (toExpr c') reflBoolTrue
|
||||
return some (r, ← mkExpectedTypeHint h (← mkEq lhs r))
|
||||
else if p.getConst % k == 0 then
|
||||
let c' := (p.div k).toRaw
|
||||
else if c'.getConst % k == 0 then
|
||||
let c' := c'.div k
|
||||
let r ← c'.denoteExpr atoms
|
||||
let h := mkApp5 (mkConst ``Int.Linear.RawRelCnstr.eq_of_divBy) (toContextExpr atoms) (toExpr c) (toExpr c') (toExpr (Int.ofNat k)) reflBoolTrue
|
||||
return some (r, ← mkExpectedTypeHint h (← mkEq lhs r))
|
||||
else if p.isEq then
|
||||
else if c'.isEq then
|
||||
let r := mkConst ``False
|
||||
let h := mkApp4 (mkConst ``Int.Linear.RawRelCnstr.eq_false_of_isUnsat_coeff) (toContextExpr atoms) (toExpr c) (toExpr (Int.ofNat k)) reflBoolTrue
|
||||
return some (r, ← mkExpectedTypeHint h (← mkEq lhs r))
|
||||
else
|
||||
-- `p.isLe`: tighten the bound
|
||||
let c' := (p.div k).toRaw
|
||||
let c' := c'.div k
|
||||
let r ← c'.denoteExpr atoms
|
||||
let h := mkApp5 (mkConst ``Int.Linear.RawRelCnstr.eq_of_divByLe) (toContextExpr atoms) (toExpr c) (toExpr c') (toExpr (Int.ofNat k)) reflBoolTrue
|
||||
return some (r, ← mkExpectedTypeHint h (← mkEq lhs r))
|
||||
|
|
@ -135,8 +134,7 @@ def simpDvdCnstr? (e : Expr) : MetaM (Option (Expr × Expr)) := do
|
|||
let k := c'.p.gcdCoeffs c'.k
|
||||
if c'.p.getConst % k == 0 then
|
||||
let c' := c'.div k
|
||||
let c' := c'.toRaw
|
||||
if c == c' then
|
||||
if c == c'.toRaw then
|
||||
return none
|
||||
let r ← c'.denoteExpr atoms
|
||||
let h := mkApp5 (mkConst ``Int.Linear.RawDvdCnstr.eq_of_isEqv) (toContextExpr atoms) (toExpr c) (toExpr c') (toExpr k) reflBoolTrue
|
||||
|
|
|
|||
|
|
@ -74,14 +74,12 @@ example (x₁ x₂ x₃ : Int) : ((x₁ + x₂) + (x₂ + x₃) = x₃ + x₂) =
|
|||
RawRelCnstr.eq_of_norm_eq #R[x₁, x₂, x₃]
|
||||
(.eq (Expr.add (Expr.add (Expr.var 0) (Expr.var 1)) (Expr.add (Expr.var 1) (Expr.var 2)))
|
||||
(Expr.add (Expr.var 2) (Expr.var 1)))
|
||||
(.eq (Expr.add (Expr.var 0) (Expr.var 1))
|
||||
(Expr.num 0))
|
||||
(.eq (.add 1 0 (.add 1 1 (.num 0))))
|
||||
rfl
|
||||
|
||||
example (x₁ x₂ x₃ : Int) : ((x₁ + x₂) + (x₂ + x₃) ≤ x₃ + x₂) = (x₁ + x₂ ≤ 0) :=
|
||||
RawRelCnstr.eq_of_norm_eq #R[x₁, x₂, x₃]
|
||||
(.le (Expr.add (Expr.add (Expr.var 0) (Expr.var 1)) (Expr.add (Expr.var 1) (Expr.var 2)))
|
||||
(Expr.add (Expr.var 2) (Expr.var 1)))
|
||||
(.le (Expr.add (Expr.var 0) (Expr.var 1))
|
||||
(Expr.num 0))
|
||||
(.le (Poly.add 1 0 (.add 1 1 (.num 0))))
|
||||
rfl
|
||||
|
|
|
|||
|
|
@ -292,3 +292,49 @@ example (a : Int) : 2+1 ∣ a + a + 1 - a + 1 + a ↔ 3 ∣ 2*a + 2 := by
|
|||
|
||||
example (a b : Int) : 6 ∣ a + 21 - a + 3*a + 6*b + 12 ↔ 2 ∣ a + 2*b + 11 := by
|
||||
simp +arith
|
||||
|
||||
theorem ex3 (a b : Int) : 6 ∣ a + (21 - a) + 3*(a + 2*b) + 12 ↔ 2 ∣ a + 2*b + 11 := by
|
||||
simp +arith
|
||||
|
||||
/--
|
||||
info: theorem ex3 : ∀ (a b : Int), 6 ∣ a + (21 - a) + 3 * (a + 2 * b) + 12 ↔ 2 ∣ a + 2 * b + 11 :=
|
||||
fun a b =>
|
||||
of_eq_true
|
||||
(Eq.trans
|
||||
(congrArg (fun x => x ↔ 2 ∣ a + 2 * b + 11)
|
||||
(id
|
||||
(RawDvdCnstr.eq_of_isEqv (RArray.branch 1 (RArray.leaf a) (RArray.leaf b))
|
||||
{ k := 6,
|
||||
e :=
|
||||
(((Expr.var 0).add ((Expr.num 21).sub (Expr.var 0))).add
|
||||
(Expr.mulL 3 ((Expr.var 0).add (Expr.mulL 2 (Expr.var 1))))).add
|
||||
(Expr.num 12) }
|
||||
{ k := 2, p := Poly.add 1 0 (Poly.add 2 1 (Poly.num 11)) } 3 (Eq.refl true))))
|
||||
(iff_self (2 ∣ a + 2 * b + 11)))
|
||||
-/
|
||||
#guard_msgs (info) in
|
||||
open Lean in open Int.Linear in
|
||||
#print ex3
|
||||
|
||||
theorem ex4 (a b : Int) : 6 ∣ a + (11 - a) + 3*(a + 2*b) - 11 ↔ 2 ∣ a + 2*b := by
|
||||
simp +arith
|
||||
|
||||
/--
|
||||
info: theorem ex4 : ∀ (a b : Int), 6 ∣ a + (11 - a) + 3 * (a + 2 * b) - 11 ↔ 2 ∣ a + 2 * b :=
|
||||
fun a b =>
|
||||
of_eq_true
|
||||
(Eq.trans
|
||||
(congrArg (fun x => x ↔ 2 ∣ a + 2 * b)
|
||||
(id
|
||||
(RawDvdCnstr.eq_of_isEqv (RArray.branch 1 (RArray.leaf a) (RArray.leaf b))
|
||||
{ k := 6,
|
||||
e :=
|
||||
(((Expr.var 0).add ((Expr.num 11).sub (Expr.var 0))).add
|
||||
(Expr.mulL 3 ((Expr.var 0).add (Expr.mulL 2 (Expr.var 1))))).sub
|
||||
(Expr.num 11) }
|
||||
{ k := 2, p := Poly.add 1 0 (Poly.add 2 1 (Poly.num 0)) } 3 (Eq.refl true))))
|
||||
(iff_self (2 ∣ a + 2 * b)))
|
||||
-/
|
||||
#guard_msgs (info) in
|
||||
open Lean in open Int.Linear in
|
||||
#print ex4
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue