diff options
| -rw-r--r-- | proofs/signatures/th_lira.plf | 34 | ||||
| -rw-r--r-- | proofs/signatures/th_lira_test.plf | 49 |
2 files changed, 2 insertions, 81 deletions
diff --git a/proofs/signatures/th_lira.plf b/proofs/signatures/th_lira.plf index a5b73d6b4..70cdfc733 100644 --- 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 9b041e0c5..91d626bba 100644 --- 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))) - ))) - ))) - )) -) |