;; 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.