Fix some bugs with ARITH_TIGHT_* rules. (#145)

ufmg-smite · Nov 19, 2024 · 9a3ac3f · 9a3ac3f
1 parent 71ac743
commit 9a3ac3f
Show file tree

Hide file tree

Showing 6 changed files with 16 additions and 38 deletions.
diff --git a/Smt/Reconstruct/Int.lean b/Smt/Reconstruct/Int.lean
@@ -338,13 +338,13 @@ where
     if !pf.getResult[0]!.getSort.isInteger then return none
     reconstructSumUB pf
   | .INT_TIGHT_UB =>
-    if !pf.getResult[0]!.getSort.isInteger then return none
+    if !pf.getChildren[0]!.getResult[1]!.getSort.isInteger then return none
     let i : Q(Int) ← reconstructTerm pf.getChildren[0]!.getResult[0]!
     let c : Q(Int) ← reconstructTerm pf.getChildren[0]!.getResult[1]!
     let h : Q($i < $c) ← reconstructProof pf.getChildren[0]!
     addThm q($i ≤ $c - 1) q(@Int.int_tight_ub $c $i $h)
   | .INT_TIGHT_LB =>
-    if !pf.getResult[0]!.getSort.isInteger then return none
+    if !pf.getChildren[0]!.getResult[1]!.getSort.isInteger then return none
     let i : Q(Int) ← reconstructTerm pf.getChildren[0]!.getResult[0]!
     let c : Q(Int) ← reconstructTerm pf.getChildren[0]!.getResult[1]!
     let h : Q($i > $c) ← reconstructProof pf.getChildren[0]!

diff --git a/Smt/Reconstruct/Rat.lean b/Smt/Reconstruct/Rat.lean
@@ -323,17 +323,17 @@ where
     if pf.getResult[0]!.getSort.isInteger then return none
     reconstructSumUB pf
   | .INT_TIGHT_UB =>
-    logInfo
-      m!"rule : {pf.getRule}\npremises : {pf.getChildren.map (·.getResult)}\nargs : {pf.getArguments}\nconclusion : {pf.getResult}"
+    if pf.getChildren[0]!.getResult[1]!.getSort.isInteger then return none
     let i : Q(Int) ← reconstructTerm pf.getChildren[0]!.getResult[0]!
     let c : Q(Rat) ← reconstructTerm pf.getChildren[0]!.getResult[1]!
     let h : Q($i < $c) ← reconstructProof pf.getChildren[0]!
-    addThm q($i ≤ «$c».floor) q(@Rat.int_tight_ub $c $i $h)
+    addThm q($i ≤ «$c».ceil - 1) q(@Rat.int_tight_ub $c $i $h)
   | .INT_TIGHT_LB =>
+    if pf.getChildren[0]!.getResult[1]!.getSort.isInteger then return none
     let i : Q(Int) ← reconstructTerm pf.getChildren[0]!.getResult[0]!
     let c : Q(Rat) ← reconstructTerm pf.getChildren[0]!.getResult[1]!
     let h : Q($i > $c) ← reconstructProof pf.getChildren[0]!
-    addThm q($i ≥ «$c».ceil) q(@Rat.int_tight_lb $c $i $h)
+    addThm q($i ≥ «$c».floor + 1) q(@Rat.int_tight_lb $c $i $h)
   | .ARITH_TRICHOTOMY =>
     if pf.getResult[0]!.getSort.isInteger then return none
     let x : Q(Rat) ← reconstructTerm pf.getResult[0]!

diff --git a/Smt/Reconstruct/Rat/Lemmas.lean b/Smt/Reconstruct/Rat/Lemmas.lean
@@ -58,10 +58,10 @@ theorem neg_lt_neg (h : a < b) : -a > -b := by
 theorem neg_le_neg (h : a ≤ b) : -a ≥ -b := by
   sorry
 
-theorem int_tight_ub (h : i < c) : i ≤ c.floor := by
+theorem int_tight_ub {i : Int} (h : i < c) : i ≤ c.ceil - 1 := by
   sorry
 
-theorem int_tight_lb (h : i > c) : i ≥ c.ceil := by
+theorem int_tight_lb {i : Int} (h : i > c) : i ≥ c.floor + 1 := by
   sorry
 
 theorem trichotomy₁ (h₁ : a ≤ b) (h₂ : a ≠ b) : a < b := by

diff --git a/Smt/Reconstruct/Real.lean b/Smt/Reconstruct/Real.lean
@@ -356,15 +356,17 @@ where
     if pf.getResult[0]!.getSort.isInteger then return none
     reconstructSumUB pf
   | .INT_TIGHT_UB =>
+    if pf.getChildren[0]!.getResult[1]!.getSort.isInteger then return none
     let i : Q(Int) ← reconstructTerm pf.getChildren[0]!.getResult[0]!
     let c : Q(Real) ← reconstructTerm pf.getChildren[0]!.getResult[1]!
     let h : Q($i < $c) ← reconstructProof pf.getChildren[0]!
-    addThm q($i ≤ ⌊$c⌋) q(@Real.int_tight_ub $c $i $h)
+    addThm q($i ≤ ⌈$c⌉ - 1) q(@Real.int_tight_ub $c $i $h)
   | .INT_TIGHT_LB =>
+    if pf.getChildren[0]!.getResult[1]!.getSort.isInteger then return none
     let i : Q(Int) ← reconstructTerm pf.getChildren[0]!.getResult[0]!
     let c : Q(Real) ← reconstructTerm pf.getChildren[0]!.getResult[1]!
     let h : Q($i > $c) ← reconstructProof pf.getChildren[0]!
-    addThm q($i ≥ ⌈$c⌉) q(@Real.int_tight_lb $c $i $h)
+    addThm q($i ≥ ⌊$c⌋ + 1) q(@Real.int_tight_lb $c $i $h)
   | .ARITH_TRICHOTOMY =>
     if pf.getResult[0]!.getSort.isInteger then return none
     let x : Q(Real) ← reconstructTerm pf.getResult[0]!

diff --git a/Smt/Reconstruct/Real/Lemmas.lean b/Smt/Reconstruct/Real/Lemmas.lean
@@ -56,11 +56,11 @@ theorem sum_ub₉ (h₁ : a = b) (h₂ : c = d) : a + c ≤ b + d := by
   rewrite [h₁, h₂]
   exact le_refl (b + d)
 
-theorem int_tight_ub {i : Int} (h : i < c) : i ≤ ⌊c⌋ :=
-  Int.le_floor.mpr (le_of_lt h)
+theorem int_tight_ub {i : Int} (h : i < c) : i ≤ ⌈c⌉ - 1 :=
+  Int.le_of_lt_add_one (Int.sub_add_cancel _ _ ▸ Int.lt_ceil.mpr h)
 
-theorem int_tight_lb {i : Int} (h : i > c) : i ≥ ⌈c⌉ :=
-  Int.ceil_le.mpr (le_of_lt h)
+theorem int_tight_lb {i : Int} (h : i > c) : i ≥ ⌊c⌋ + 1 :=
+  Int.add_one_le_of_lt (Int.floor_lt.mpr h)
 
 theorem trichotomy₁ (h₁ : a ≤ b) (h₂ : a ≠ b) : a < b := by
   have tr := lt_trichotomy a b

diff --git a/Test/linarith.expected b/Test/linarith.expected
@@ -1,21 +1,3 @@
-Test/linarith.lean:10:0: error: application type mismatch
-  @Smt.Reconstruct.Real.int_tight_ub 1
-argument has type
-  ℤ
-but function has type
-  ∀ {c : ℝ} {i : ℤ}, ↑i < c → i ≤ ⌊c⌋
-Test/linarith.lean:19:0: error: application type mismatch
-  @Smt.Reconstruct.Real.int_tight_ub 0
-argument has type
-  ℤ
-but function has type
-  ∀ {c : ℝ} {i : ℤ}, ↑i < c → i ≤ ⌊c⌋
-Test/linarith.lean:22:0: error: application type mismatch
-  @Smt.Reconstruct.Real.int_tight_ub 0
-argument has type
-  ℤ
-but function has type
-  ∀ {c : ℝ} {i : ℤ}, ↑i < c → i ≤ ⌊c⌋
 Test/linarith.lean:34:9: warning: unused variable `e`
 note: this linter can be disabled with `set_option linter.unusedVariables false`
 Test/linarith.lean:53:0: warning: declaration uses 'sorry'
@@ -45,9 +27,3 @@ Test/linarith.lean:168:34: warning: unused variable `z`
 note: this linter can be disabled with `set_option linter.unusedVariables false`
 Test/linarith.lean:169:5: warning: unused variable `h5`
 note: this linter can be disabled with `set_option linter.unusedVariables false`
-Test/linarith.lean:173:0: error: application type mismatch
-  @Smt.Reconstruct.Real.int_tight_ub 0
-argument has type
-  ℤ
-but function has type
-  ∀ {c : ℝ} {i : ℤ}, ↑i < c → i ≤ ⌊c⌋