diff options
author | Alex Ozdemir <aozdemir@hmc.edu> | 2020-02-21 07:25:25 -0800 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-02-21 09:25:25 -0600 |
commit | ba91b6a2dabe7d153b78e6a04e0ef594f033e945 (patch) | |
tree | d6d9267a516a2983872a8524215c2734e2f3a0b0 /proofs/signatures/th_lira_test.plf | |
parent | 5489ef01beb91e256e343e2fd2d734b48b42ad6e (diff) |
Remove IntReal tightening axioms from th_lira.plf (#3787)
Diffstat (limited to 'proofs/signatures/th_lira_test.plf')
-rw-r--r-- | proofs/signatures/th_lira_test.plf | 49 |
1 files changed, 2 insertions, 47 deletions
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))) - ))) - ))) - )) -) |