Check if an ordering expression is well-formed.
(check-lt/le/gt/ge-expression arg1 arg2 arg1-type arg2-type arg1-obligs arg2-obligs err-keyword expr ctxt) → result
The two types must be both (subtypes of) integers, both (subtypes of) characters, or both (subtypes of) strings. We calculate the supremum type, and check whether it is (a subtype of) any of these three types. The expression returns a boolean.
Function:
(defun check-lt/le/gt/ge-expression (arg1 arg2 arg1-type arg2-type arg1-obligs arg2-obligs err-keyword expr ctxt) (declare (xargs :guard (and (expressionp arg1) (expressionp arg2) (typep arg1-type) (typep arg2-type) (proof-obligation-listp arg1-obligs) (proof-obligation-listp arg2-obligs) (keywordp err-keyword) (expressionp expr) (contextp ctxt)))) (declare (ignorable expr)) (let ((__function__ 'check-lt/le/gt/ge-expression)) (declare (ignorable __function__)) (b* ((supremum (supremum-type arg1-type arg2-type (context->tops ctxt)))) (if (and supremum (subtypep supremum (type-integer) (context->tops ctxt))) (make-type-result-ok :types (list (type-boolean)) :obligations (append arg1-obligs arg2-obligs)) (type-result-err (list err-keyword (expression-fix arg1) (expression-fix arg2) (type-fix arg1-type) (type-fix arg2-type)))))))
Theorem:
(defthm type-resultp-of-check-lt/le/gt/ge-expression (b* ((result (check-lt/le/gt/ge-expression arg1 arg2 arg1-type arg2-type arg1-obligs arg2-obligs err-keyword expr ctxt))) (type-resultp result)) :rule-classes :rewrite)
Theorem:
(defthm check-lt/le/gt/ge-expression-of-expression-fix-arg1 (equal (check-lt/le/gt/ge-expression (expression-fix arg1) arg2 arg1-type arg2-type arg1-obligs arg2-obligs err-keyword expr ctxt) (check-lt/le/gt/ge-expression arg1 arg2 arg1-type arg2-type arg1-obligs arg2-obligs err-keyword expr ctxt)))
Theorem:
(defthm check-lt/le/gt/ge-expression-expression-equiv-congruence-on-arg1 (implies (expression-equiv arg1 arg1-equiv) (equal (check-lt/le/gt/ge-expression arg1 arg2 arg1-type arg2-type arg1-obligs arg2-obligs err-keyword expr ctxt) (check-lt/le/gt/ge-expression arg1-equiv arg2 arg1-type arg2-type arg1-obligs arg2-obligs err-keyword expr ctxt))) :rule-classes :congruence)
Theorem:
(defthm check-lt/le/gt/ge-expression-of-expression-fix-arg2 (equal (check-lt/le/gt/ge-expression arg1 (expression-fix arg2) arg1-type arg2-type arg1-obligs arg2-obligs err-keyword expr ctxt) (check-lt/le/gt/ge-expression arg1 arg2 arg1-type arg2-type arg1-obligs arg2-obligs err-keyword expr ctxt)))
Theorem:
(defthm check-lt/le/gt/ge-expression-expression-equiv-congruence-on-arg2 (implies (expression-equiv arg2 arg2-equiv) (equal (check-lt/le/gt/ge-expression arg1 arg2 arg1-type arg2-type arg1-obligs arg2-obligs err-keyword expr ctxt) (check-lt/le/gt/ge-expression arg1 arg2-equiv arg1-type arg2-type arg1-obligs arg2-obligs err-keyword expr ctxt))) :rule-classes :congruence)
Theorem:
(defthm check-lt/le/gt/ge-expression-of-type-fix-arg1-type (equal (check-lt/le/gt/ge-expression arg1 arg2 (type-fix arg1-type) arg2-type arg1-obligs arg2-obligs err-keyword expr ctxt) (check-lt/le/gt/ge-expression arg1 arg2 arg1-type arg2-type arg1-obligs arg2-obligs err-keyword expr ctxt)))
Theorem:
(defthm check-lt/le/gt/ge-expression-type-equiv-congruence-on-arg1-type (implies (type-equiv arg1-type arg1-type-equiv) (equal (check-lt/le/gt/ge-expression arg1 arg2 arg1-type arg2-type arg1-obligs arg2-obligs err-keyword expr ctxt) (check-lt/le/gt/ge-expression arg1 arg2 arg1-type-equiv arg2-type arg1-obligs arg2-obligs err-keyword expr ctxt))) :rule-classes :congruence)
Theorem:
(defthm check-lt/le/gt/ge-expression-of-type-fix-arg2-type (equal (check-lt/le/gt/ge-expression arg1 arg2 arg1-type (type-fix arg2-type) arg1-obligs arg2-obligs err-keyword expr ctxt) (check-lt/le/gt/ge-expression arg1 arg2 arg1-type arg2-type arg1-obligs arg2-obligs err-keyword expr ctxt)))
Theorem:
(defthm check-lt/le/gt/ge-expression-type-equiv-congruence-on-arg2-type (implies (type-equiv arg2-type arg2-type-equiv) (equal (check-lt/le/gt/ge-expression arg1 arg2 arg1-type arg2-type arg1-obligs arg2-obligs err-keyword expr ctxt) (check-lt/le/gt/ge-expression arg1 arg2 arg1-type arg2-type-equiv arg1-obligs arg2-obligs err-keyword expr ctxt))) :rule-classes :congruence)
Theorem:
(defthm check-lt/le/gt/ge-expression-of-proof-obligation-list-fix-arg1-obligs (equal (check-lt/le/gt/ge-expression arg1 arg2 arg1-type arg2-type (proof-obligation-list-fix arg1-obligs) arg2-obligs err-keyword expr ctxt) (check-lt/le/gt/ge-expression arg1 arg2 arg1-type arg2-type arg1-obligs arg2-obligs err-keyword expr ctxt)))
Theorem:
(defthm check-lt/le/gt/ge-expression-proof-obligation-list-equiv-congruence-on-arg1-obligs (implies (proof-obligation-list-equiv arg1-obligs arg1-obligs-equiv) (equal (check-lt/le/gt/ge-expression arg1 arg2 arg1-type arg2-type arg1-obligs arg2-obligs err-keyword expr ctxt) (check-lt/le/gt/ge-expression arg1 arg2 arg1-type arg2-type arg1-obligs-equiv arg2-obligs err-keyword expr ctxt))) :rule-classes :congruence)
Theorem:
(defthm check-lt/le/gt/ge-expression-of-proof-obligation-list-fix-arg2-obligs (equal (check-lt/le/gt/ge-expression arg1 arg2 arg1-type arg2-type arg1-obligs (proof-obligation-list-fix arg2-obligs) err-keyword expr ctxt) (check-lt/le/gt/ge-expression arg1 arg2 arg1-type arg2-type arg1-obligs arg2-obligs err-keyword expr ctxt)))
Theorem:
(defthm check-lt/le/gt/ge-expression-proof-obligation-list-equiv-congruence-on-arg2-obligs (implies (proof-obligation-list-equiv arg2-obligs arg2-obligs-equiv) (equal (check-lt/le/gt/ge-expression arg1 arg2 arg1-type arg2-type arg1-obligs arg2-obligs err-keyword expr ctxt) (check-lt/le/gt/ge-expression arg1 arg2 arg1-type arg2-type arg1-obligs arg2-obligs-equiv err-keyword expr ctxt))) :rule-classes :congruence)
Theorem:
(defthm check-lt/le/gt/ge-expression-of-expression-fix-expr (equal (check-lt/le/gt/ge-expression arg1 arg2 arg1-type arg2-type arg1-obligs arg2-obligs err-keyword (expression-fix expr) ctxt) (check-lt/le/gt/ge-expression arg1 arg2 arg1-type arg2-type arg1-obligs arg2-obligs err-keyword expr ctxt)))
Theorem:
(defthm check-lt/le/gt/ge-expression-expression-equiv-congruence-on-expr (implies (expression-equiv expr expr-equiv) (equal (check-lt/le/gt/ge-expression arg1 arg2 arg1-type arg2-type arg1-obligs arg2-obligs err-keyword expr ctxt) (check-lt/le/gt/ge-expression arg1 arg2 arg1-type arg2-type arg1-obligs arg2-obligs err-keyword expr-equiv ctxt))) :rule-classes :congruence)
Theorem:
(defthm check-lt/le/gt/ge-expression-of-context-fix-ctxt (equal (check-lt/le/gt/ge-expression arg1 arg2 arg1-type arg2-type arg1-obligs arg2-obligs err-keyword expr (context-fix ctxt)) (check-lt/le/gt/ge-expression arg1 arg2 arg1-type arg2-type arg1-obligs arg2-obligs err-keyword expr ctxt)))
Theorem:
(defthm check-lt/le/gt/ge-expression-context-equiv-congruence-on-ctxt (implies (context-equiv ctxt ctxt-equiv) (equal (check-lt/le/gt/ge-expression arg1 arg2 arg1-type arg2-type arg1-obligs arg2-obligs err-keyword expr ctxt) (check-lt/le/gt/ge-expression arg1 arg2 arg1-type arg2-type arg1-obligs arg2-obligs err-keyword expr ctxt-equiv))) :rule-classes :congruence)