;; The syntax follows lisp closely. You can use lisp-mode in emacs, if
;; you want.
;; We are asking Simplify to show that 7 = 4 + 3.
(EQ 7 (+ 4 3)) ;; This is query 1.
;; Another query to simplify.
(FORALL (I) (> (+ I 1) I)) ;; This is query 2.
;; Now we define predicates is_mammal and is_human with one parameter each
(DEFPRED (is_mammal X))
(DEFPRED (is_human X))
;; We now add a background axiom. Background axioms in Simplify are
;; organized as a stack. BG_PUSH pushes an axiom onto the stack, and
;; BG_POP removes the most recently added axiom.
(BG_PUSH (FORALL (X) (IMPLIES (is_human X) (is_mammal X))))
;; Let's assume Bob is human
(BG_PUSH (is_human Bob))
;; Is he a mammal? Better be...
(is_mammal Bob) ;; This is query 3.
;; Let's now pop the assumption about Bob.
(BG_POP)
;; Now Bob should not be a mammal anymore...
(is_mammal Bob) ;; This is query 4.
;; Let's pop the axiom about humans and mammals
(BG_POP)
;; We define a predicate and provide it's body.
(DEFPRED (is_positive X) (>= X 0))
;; Although the above is logically equivalent to:
;;
;; (DEFPRED (is_positive X))
;; (BG_PUSH (FORALL (X) (IFF (is_positive X) (>= X 0))))
;;
;; Simplify actually treats these two versions differently. When the
;; definition of a predicate is given with its declaration, as in the
;; uncommented version of is_positive above, Simplify always rewrites
;; occurances of the predicate to its definition. When the definition
;; of a predicate is given using a forall axiom, the regular rules of
;; quantifier instantiation govern when and how the quantifier gets
;; instantiated.
;; Let's see if Simplify knows about the law of the excluded middle...
(FORALL (X) (OR (is_positive X) (NOT (is_positive X)))) ;; This is query 5.
;; Simplify has a special built-in predicate for not-equal, called
;; NEQ.
(IFF (NEQ X Y) (NOT (EQ X Y))) ;; This is query 6.
;; Ok, let's see some more complicated formulas. Here is a somewhat
;; complicated test case taken from the Simplify test cases. This was
;; generated automatically by ESC. I haven't looked in detail to see
;; what it really means.
(IMPLIES
(AND
(OR
(EQ m length)
(EQ m (- num start))
)
(<= m length)
(<= m (- num start))
(>= num -1)
(>= start 0)
(>= length 0)
)
(IMPLIES
(<= m 0)
(OR
(EQ length 0)
(>= start num)
))) ;; This is query 7.
;; Here is an even more complicated test case, again generated by ESC.
(IMPLIES
TRUE
(IMPLIES
TRUE
(IMPLIES (AND (AND TRUE (>= (NUMBER a) 0)) (>= (NUMBER b) 0))
(IMPLIES (AND TRUE TRUE)
(AND
(IMPLIES
(< (- (NUMBER a) 1) (- (NUMBER b) 1))
(AND
(IMPLIES (<= 0 (- (NUMBER a) 1))
(AND (AND (<= 0 0) (<= 0 (+ (- (NUMBER a) 1) 1)))
(AND (IMPLIES (AND (<= 0 |i.39|)
(<= |i.39| (+ (- (NUMBER a) 1) 1)))
(IMPLIES (<= |i.39| (- (NUMBER a) 1))
(AND (OR (AND (<= 0 |i.39|)
(< |i.39| (+ (NUMBER a) 0)))
(NOT |ERROR.ARRAY_BOUNDS.16.13|))
(AND
(OR (AND (<= 0 |i.39|)
(< |i.39| (+ (NUMBER b) 0)))
(NOT |ERROR.ARRAY_BOUNDS.16.20|))
(AND (<= 0 (+ |i.39| 1))
(<= (+ |i.39| 1)
(+ (- (NUMBER a) 1) 1)))))))
(IMPLIES
(AND (AND (<= 0 |i.45|)
(<= |i.45| (+ (- (NUMBER a) 1) 1)))
(OR (NOT (<= |i.45| (- (NUMBER a) 1)))
(AND (OR (AND (<= 0 |i.45|)
(< |i.45| (+ (NUMBER a) 0)))
(NOT |ERROR.ARRAY_BOUNDS.16.13|))
(AND (OR (AND (<= 0 |i.45|)
(< |i.45| (+ (NUMBER b) 0)))
(NOT |ERROR.ARRAY_BOUNDS.16.20|))
(NOT TRUE)))))
TRUE))))
(IMPLIES (OR (NOT (<= 0 (- (NUMBER a) 1))) (NOT TRUE))
TRUE)))
(IMPLIES
(OR (NOT (< (- (NUMBER a) 1) (- (NUMBER b) 1))) (NOT TRUE))
(AND
(IMPLIES (<= 0 (- (NUMBER b) 1))
(AND (AND (<= 0 0) (<= 0 (+ (- (NUMBER b) 1) 1)))
(AND (IMPLIES (AND (<= 0 |i.51|)
(<= |i.51| (+ (- (NUMBER b) 1) 1)))
(IMPLIES (<= |i.51| (- (NUMBER b) 1))
(AND (OR (AND (<= 0 |i.51|)
(< |i.51| (+ (NUMBER a) 0)))
(NOT |ERROR.ARRAY_BOUNDS.16.13|))
(AND
(OR (AND (<= 0 |i.51|)
(< |i.51| (+ (NUMBER b) 0)))
(NOT |ERROR.ARRAY_BOUNDS.16.20|))
(AND (<= 0 (+ |i.51| 1))
(<= (+ |i.51| 1)
(+ (- (NUMBER b) 1) 1)))))))
(IMPLIES
(AND (AND (<= 0 |i.57|)
(<= |i.57| (+ (- (NUMBER b) 1) 1)))
(OR (NOT (<= |i.57| (- (NUMBER b) 1)))
(AND (OR (AND (<= 0 |i.57|)
(< |i.57| (+ (NUMBER a) 0)))
(NOT |ERROR.ARRAY_BOUNDS.16.13|))
(AND (OR (AND (<= 0 |i.57|)
(< |i.57| (+ (NUMBER b) 0)))
(NOT |ERROR.ARRAY_BOUNDS.16.20|))
(NOT TRUE)))))
TRUE))))
(IMPLIES (OR (NOT (<= 0 (- (NUMBER b) 1))) (NOT TRUE))
TRUE))))))))
;; This is query 8.
;; Now let's see some of Simplify's limitations. Let's try the
;; following:
(EXISTS (X) (is_positive X)) ;; This is query 9.
;; Simplify can't prove it! Intuitively, the problem is that Simplify
;; cannot find the witness for the existential. Simplify is getting
;; confused because there is nothing in the background axioms that
;; talks about is_positive (except for its definition), so Simplify
;; doesn't know where to start. By the way, you may have noticed that
;; the counter-example is in fact empty... We will learn in class in
;; more detail what is actually going on here.
;; In the meantime, let's help Simplify out. We will prove a lemma. A
;; lemma is a formula that Simplify tries to prove. If Simplify is
;; able to prove the formula, then the formula is added as a
;; background axiom (essentially using a BG_PUSH). If Simplify cannot
;; prove the formula, then nothing is added to the background
;; axioms. So let's try the following lemma:
(LEMMA (is_positive 0)) ;; This is query 10.
;; The above lemma succeeds, and Simplify says:
;; 8: Valid. (Added to background predicate).
;; So we now have (is_positive 0) as a background predicate
;; Now let's try again. This time Simplify will be able to prove it.
(EXISTS (X) (is_positive X)) ;; This is query 11.