Remove IntReal tightening axioms from th_lira.plf (#3787)

diff --git a/proofs/signatures/th_lira.plf b/proofs/signatures/th_lira.plf
index a5b73d6b4fb46c9a10908dcd6365f465c1298677..70cdfc7332fef46335ac9aba7c33d75d0e56ef0c 100644 (file)
--- a/proofs/signatures/th_lira.plf
+++ b/proofs/signatures/th_lira.plf
@@ -139,40 +139,6 @@
     (default (fail (term Int)))
   ))
 
-; Statement that z is the negation of greatest integer less than q.
-(declare holds_neg_of_greatest_integer_below
-  (! z mpz
-  (! q mpq
-    type)))
-
-; For proving statements of the above form.
-(declare check_neg_of_greatest_integer_below
-  (! z mpz
-  (! q mpq
-    (! sc_check (^ (is_greatest_integer_below (mp_neg z) q) tt)
-       (holds_neg_of_greatest_integer_below z q)))))
-
-; Axiom for tightening [Int] < q into -[Int] >= -greatest_int_below(q).
-; Note that [Int] < q is actually not([Int] >= q)
-(declare tighten_not_>=_IntReal
-  (! t       (term Int)  ; Omit
-  (! neg_t   (term Int)  ; Omit
-  (! real_bound mpq    ; Omit
-  (! neg_int_bound mpz ; Omit
-    (! pf_step (holds_neg_of_greatest_integer_below neg_int_bound real_bound)
-    (! pf_real_bound (th_holds (not (>=_IntReal t (a_real real_bound))))
-      (! sc_neg (^ (negate_linear_int_term t) neg_t)
-        (th_holds (>=_IntReal neg_t (term_int_to_real (a_int neg_int_bound))))))))))))
-
-; Axiom for tightening [Int] >= q into [Int] >= ceil(q)
-(declare tighten_>=_IntReal
-  (! t       (term Int)   ; Omit
-  (! real_bound mpq     ; Omit
-    (! int_bound mpz
-    (! pf_real_bound (th_holds (>=_IntReal t (a_real real_bound)))
-      (! sc_floor (^ (is_ceil real_bound int_bound) tt)
-        (th_holds (>=_IntReal t (term_int_to_real (a_int int_bound))))))))))
-
 ; Statement that z is the greatest integer less than z'.
 (declare holds_neg_of_greatest_integer_below_int
   (! z mpz

diff --git a/proofs/signatures/th_lira_test.plf b/proofs/signatures/th_lira_test.plf
index 9b041e0c5ea79f5329dac3df71064a4d4424bb6f..91d626bba78973a710bc1fd043f1fba1d724cca8 100644 (file)
--- a/proofs/signatures/th_lira_test.plf
+++ b/proofs/signatures/th_lira_test.plf
@@ -249,7 +249,7 @@
   (@ f2 (>=_Real
           (+_Real (term_real_var x) (term_int_to_real (term_int_var y)))
           (a_real 0/1))
-  (@ f3 (not (>=_IntReal (*_Int (a_int 1) (term_int_var y)) (a_real 0/1)))
+  (@ f3 (not (>=_IntReal (*_Int (a_int 1) (term_int_var y)) (term_int_to_real (a_int 0))))
 
   ; Normalization
   ; proof of real predicates
@@ -274,7 +274,7 @@
           (is_aff_mul_c_L _ _ _ (~ 1/1) (is_aff_var_int y))
           (is_aff_const 1/1))
         (pf_reified_arith_pred _ _
-          (tighten_not_>=_IntReal _ _ _ _ (check_neg_of_greatest_integer_below 1 0/1) pf_f3)))
+          (tighten_not_>=_IntInt _ _ _ _ (check_neg_of_greatest_integer_below_int 1 0) pf_f3)))
 
   ; derivation of a contradiction using farkas coefficients
     (:
@@ -292,48 +292,3 @@
   )))
   ))
 )
-
-;; Term proof, with integer y, that needs to be strictly and non-strictly tightened.
-;; Proof (from predicates on real terms) that the following imply bottom
-;                 y >= 1/2               =>   y >= 1
-;     not[        y >=  0]    => [y < 0] => [-y >= 1]
-;
-(check
-  ; Declarations
-  ; Variables
-  (% y int_var
-  ; real predicates
-  (@ f1 (>=_IntReal (*_Int (a_int 1) (term_int_var y)) (a_real 1/2))
-  (@ f2 (not (>=_IntReal (*_Int (a_int 1) (term_int_var y)) (a_real 0/1)))
-
-  ; Normalization
-  ; proof of real predicates
-  (% pf_f1 (th_holds f1)
-  (% pf_f2 (th_holds f2)
-  ; real term -> linear polynomial normalization witnesses
-  (@ n1 (aff_>=_from_term _ _ _
-        (is_aff_- _ _ _ _ _
-          (is_aff_mul_c_L _ _ _ 1/1 (is_aff_var_int y))
-          (is_aff_const 1/1))
-        (pf_reified_arith_pred _ _
-          (tighten_>=_IntReal _ _ 1 pf_f1)))
-  (@ n2 (aff_>=_from_term _ _ _
-        (is_aff_- _ _ _ _ _
-          (is_aff_mul_c_L _ _ _ (~ 1/1) (is_aff_var_int y))
-          (is_aff_const 1/1))
-        (pf_reified_arith_pred _ _
-          (tighten_not_>=_IntReal _ _ _ _ (check_neg_of_greatest_integer_below 1 0/1) pf_f2)))
-
-  ; derivation of a contradiction using farkas coefficients
-    (:
-      (th_holds false)
-      (bounded_aff_contra _ _
-       (bounded_aff_add _ _ _ _ _
-         (bounded_aff_mul_c _ _ _ 1/1 n1)
-         (bounded_aff_add _ _ _ _ _
-           (bounded_aff_mul_c _ _ _ 1/1 n2)
-           bounded_aff_ax_0_>=_0)))
-  )))
-  )))
-  ))
-)