;; ---------------------------------------------------------------------------
;; ~/events/parsing-inv.events
;; ---------------------------------------------------------------------------

;; This is an attempt to prove the invariants of parsing correct.
;; A *massive* use of PC-NQTHM was necessary to "see" the proofs.

(enable-theory lists)
(enable-theory stacks)
(enable-theory trees)

;; ---------------------------------------------------------------------------
;;      Leaves invariant
;; ---------------------------------------------------------------------------

(prove-lemma leaves-base (rewrite)
 (equal (append (leaves (from-bottom (emptystack))) input)
        input))

(prove-lemma leaves-append (rewrite)
 (implies (listp b)
          (equal (leaves (append a b))
                 (append (leaves a) (leaves b))))
 ((enable-theory lists trees)))

(prove-lemma better-leaves (rewrite)
 (implies (listp l)
   (equal (leaves (list (mk-tree x l)))
          (leaves l)))
 ((enable-theory trees)))

(prove-lemma configuration-induction-step-shift (rewrite)
 (implies (and (token-listp input)
               (listp input)
               (is-stack trees)
               (equal next (mk-configuration
                            (cdr input)
                            (push s states)
                            (push (car input) symbols)
                            (push (mk-tree (car input) nil) trees)
                            parse
                            deriv
                            F)))
            (equal (append (leaves (from-bottom (sel-trees next))) 
                           (sel-input next))
                   (append (leaves (from-bottom trees)) input)))
 ((enable-theory stacks lists trees)))

(prove-lemma frontier-leaf-rewrite (rewrite)
 (equal (frontier 'tree (mk-tree a b))
        (if (is-leaf (mk-tree a b))
            (list a)
            (frontier 'branches b))))

(prove-lemma frontier-tree-is-leaves (rewrite)
 (implies (listp l)
          (equal (frontier 'tree (mk-tree x l))
                 (leaves l))))

(prove-lemma append-leaves (rewrite)
 (implies (listp b)
          (equal (append (leaves a) (leaves b))
                 (leaves (append a b)))))

;; The lemma needs the help of PC-NQTHM to prove, it is just a rewriting
;; proof. NQTHM alone cannot be coaxed to do the necessary rewriting.

(prove-lemma leaves-from-bottom-reduce-leaves (rewrite)
 (implies (and (is-stack trees)
               (not (zerop size))
               (not (lessp (stack-length trees) size)))
          (equal (leaves (from-bottom (reduce-trees lhs size trees)))
                 (leaves (from-bottom trees))))
           ((instructions promote
                          (dive 1 1 1)
                          x up
                          (rewrite from-bottom-push)
                          up
                          (rewrite leaves-append)
                          (dive 2)
                          (rewrite better-leaves)
                          up
                          (rewrite append-leaves)
                          (dive 1)
                          (rewrite append-from-bottom-pop-n)
                          top prove prove prove)))

;; Disable this lemma because it is an incredibly bad rewrite rule!

(disable append-leaves) 

(prove-lemma configuration-induction-step-reduce (rewrite)
 (implies (and (token-listp input)
               (listp input)
               (is-stack trees)
               (not (zerop size))
               (not (lessp (stack-length trees) size))
               (equal next (mk-configuration
                            input
                            (push s states)
                            (push (car input) symbols)
                            (reduce-trees lhs size trees)
                            parse
                            deriv
                            F)))
            (equal (append (leaves (from-bottom (sel-trees next))) 
                           (sel-input next))
                   (append (leaves (from-bottom trees)) input)))
 ((disable reduce-trees)))

(prove-lemma frontier-branches-is-leaves (rewrite)
 (equal (frontier 'branches q)
        (leaves q)))
        
(prove-lemma leaves-from-bottom-pop-n-trees (rewrite)
 (implies (and (is-stack trees)
               (not (zerop size))
               (not (lessp (stack-length trees) size)))
          (equal (append (leaves (from-bottom (pop-n size trees)))
                         (frontier 'branches
                                   (top-n size trees)))
                 (leaves (from-bottom trees))))
             ((instructions promote
                            (dive 1 2)
                            top
                            (dive 2)
                            top
                            (dive 1 2)
                            (rewrite frontier-branches-is-leaves)
                            up
                            (claim (listp (top-n size trees)))
                            (rewrite append-leaves)
                            (dive 1)
                            (rewrite append-from-bottom-pop-n)
                            top prove)))

(prove-lemma append-elimination (rewrite)
 (implies (equal (append x y) a)
          (equal (append x (append y z))
                 (append a z))))

(prove-lemma great-parsing-step-invariant (rewrite)
 (implies (equal next
                 (parsing-step (mk-configuration input states
                                                 symbols
                                                 trees parse
                                                 deriv f)
                               tables grammar))
          (equal (append (leaves (from-bottom (sel-trees next)))
                         (sel-input next))
                 (append (leaves (from-bottom trees))
                         input)))
             ((instructions promote
                            (dive 1 1 1 1 1)
                            = top bash prove promote
                            (dive 1)
                            (rewrite append-elimination
                                     (($a (leaves (from-bottom trees)))))
                            top prove
                            (dive 1)
                            (rewrite append-leaves)
                            (dive 1)
                            (rewrite append-from-bottom-pop-n)
                            top prove 
                            prove)))

;; ---------------------------------------------------------------------------
;;      Right Sentential form
;; ---------------------------------------------------------------------------

(enable-theory derivations)
(enable-theory grammar)
(disable sel-action-tag)
(disable action-lookup)

:; A problem with this invariant is that it is not valid until I have made 
;; a first reduction, as the derivation is empty at the beginning of parsing.
;; I cannot put a "dummy" derivation on, as there would be nothing to
;; put in the production component, and thus the derivation would not be
;; in lockstep.

(prove-lemma car-append-list (rewrite)
 (equal (car (append (list x) y)) x))

(prove-lemma inv-rt-sent-1-shift (rewrite)
  (implies (and (equal next
                       (mk-configuration
                        (cdr input)
                        (push s states)
                        (push (token-name (car input)) symbols)
                        (push (mk-tree (car input) nil) trees)
                        parse
                        deriv
                        f))
                (listp input)
                (token-listp input)
                (equal (append (from-bottom symbols) (pick-token-names input))
                       (step-source (car deriv))))
           (equal (append (from-bottom (sel-symbols next)) 
                           (pick-token-names (sel-input next)))
                  (step-source (car (sel-deriv next))))))

(prove-lemma append-from-bottom-push (rewrite)
      (implies (and (is-stack symbols)
                    (equal (append (from-bottom symbols)
                                   (pick-token-names input))
                           (append d (cons x w))))
               (equal (append (from-bottom (push lhs (pop-n size symbols)))
                              (pick-token-names input))
                      (append (from-bottom (pop-n size symbols))
                              (cons lhs (pick-token-names input))))))

(prove-lemma inv-rt-sent-1-reduce (rewrite)
  (implies (and (equal next
                       (mk-configuration
                        input
                        (push goto (pop-n size states))
                        (push lhs (pop-n size symbols))
                        (reduce-trees lhs size trees)
                        (append parse (list label))
                        (append (list (mk-derivation-step 
                                       (from-bottom (pop-n size symbols))
                                       (mk-prod label lhs (top-n size symbols))
                                       (pick-token-names input)))
                                deriv)
                        f))
                (is-stack symbols)
                (equal (append (from-bottom symbols) (pick-token-names input))
                       (step-source (car deriv))))
           (equal (append (from-bottom (sel-symbols next))
                           (pick-token-names (sel-input next)))
                   (step-source (car (sel-deriv next))))))

(prove-lemma inv-rt-sent-1 (rewrite)
  (implies (and (equal next
                      (parsing-step (mk-configuration input states
                                                      symbols
                                                      trees parse
                                                      deriv f)
                                    tables grammar))
                (is-stack symbols)
                (token-listp input)
                (listp input)
                (equal (append (from-bottom symbols) 
                               (pick-token-names input))
                       (step-source (car deriv))))
           (equal (append (from-bottom (sel-symbols next)) 
                          (pick-token-names (sel-input next)))
                   (step-source (car (sel-deriv next))))))

;; ---------------------------------------------------------------------------
;;      Stack size
;; ---------------------------------------------------------------------------

(prove-lemma inv-stack-size-shift (rewrite)
 (implies (and (equal next (mk-configuration
                             (cdr input)
                             (push s states)
                             (push (token-name (car input)) symbols)
                             (push (mk-tree (car input) nil) trees)
                             parse
                             deriv
                             f))
                (is-stack symbols)
                (is-stack states)
                (is-stack trees)
                (and (equal (stack-length trees)
                            (stack-length symbols))
                     (equal (add1 (stack-length symbols))
                            (stack-length states))))
           (and (equal (stack-length (sel-trees next))
                       (stack-length (sel-symbols next)))
                (equal (add1 (stack-length (sel-symbols next)))
                       (stack-length (sel-states next))))))

(prove-lemma stack-length-push (rewrite)
 (equal (stack-length (push a b))
        (add1 (stack-length b))))

(prove-lemma stack-length-pop-n (rewrite)
 (implies (not (lessp (stack-length a) size))
          (equal (stack-length (pop-n size a))
                 (difference (stack-length a) size))))

(prove-lemma inv-stack-size-reduce (rewrite)
 (implies (and (equal next 
                      (mk-configuration
                       input
                       (push goto (pop-n size states))
                       (push lhs (pop-n size symbols))
                       (reduce-trees lhs size trees)
                       (append parse (list label))
                       (append (list (mk-derivation-step 
                                      (from-bottom (pop-n size symbols))
                                      (mk-prod label lhs (top-n size symbols))
                                      (pick-token-names input)))
                               deriv)
                       f))
                (is-stack symbols)
                (is-stack states)
                (is-stack trees)
                (not (zerop size))
                (not (lessp (stack-length trees) size))
                (and (equal (stack-length trees)
                            (stack-length symbols))
                     (equal (add1 (stack-length symbols))
                            (stack-length states))))
           (and (equal (stack-length (sel-trees next))
                       (stack-length (sel-symbols next)))
                (equal (add1 (stack-length (sel-symbols next)))
                       (stack-length (sel-states next))))))

(prove-lemma inv-stack-size (rewrite)
 (implies (and (equal next
                      (parsing-step (mk-configuration input states
                                                      symbols
                                                      trees parse
                                                      deriv f)
                                    tables grammar))
                (is-stack symbols)
                (is-stack states)
                (is-stack trees)
                (and (equal (stack-length trees)
                            (stack-length symbols))
                     (equal (add1 (stack-length symbols))
                            (stack-length states))))
           (and (equal (stack-length (sel-trees next))
                       (stack-length (sel-symbols next)))
                (equal (add1 (stack-length (sel-symbols next)))
                       (stack-length (sel-states next))))))

;; ---------------------------------------------------------------------------
;;      Number of reductions
;; ---------------------------------------------------------------------------

;; I only count the inner nodes.

(defn node-count (tag tree)
  (if (equal tag 'tree)
      (if (or (not (is-tree tree))
              (equal tree (emptytree))
              (is-leaf tree))
          0
          (add1 (node-count 'branches (sel-branches tree))))
      (if (nlistp tree)
          0
          (plus (node-count 'tree (car tree))
                (node-count 'branches (cdr tree))))))
                   
(prove-lemma length-append (rewrite)
 (equal (length (append a b))
        (plus (length a)
              (length b))))

(prove-lemma node-count-append (rewrite)
 (equal (node-count 'branches (append a b))
        (plus (node-count 'branches a)
              (node-count 'branches b))))
        
(prove-lemma node-count-top-n-pop-n (rewrite)
 (equal (plus (node-count 'branches (top-n size trees))
              (node-count 'branches (from-bottom (pop-n size trees))))
        (node-count 'branches (from-bottom trees))))

(prove-lemma inv-reductions-shift (rewrite)
 (implies (and (equal next (mk-configuration
                             (cdr input)
                             (push s states)
                             (push (token-name (car input)) symbols)
                             (push (mk-tree (car input) nil) trees)
                             parse
                             deriv
                             f))
               (equal (node-count 'branches (from-bottom trees)) 
                      (length parse)))
           (equal (node-count 'branches (from-bottom (sel-trees next)))
                  (length (sel-parse next)))))

;; I need to know that trees is not empty, as the node-count
;; of an empty tree is 0, as is the node-count of a leaf.

(prove-lemma node-count-reduce-trees (rewrite)
 (implies (and (not (zerop size))
               (not (lessp (stack-length trees) size))
               (not (equal trees (emptystack))))
          (equal (node-count 'branches 
                             (from-bottom (reduce-trees lhs size trees)))
                 (add1 (node-count 'branches (from-bottom trees)))))
 ((enable-theory trees)))

(prove-lemma inv-reductions-reduce (rewrite)
 (implies (and (equal next 
                      (mk-configuration
                       input
                       (push goto (pop-n size states))
                       (push lhs (pop-n size symbols))
                       (reduce-trees lhs size trees)
                       (append parse (list label))
                       (append (list (mk-Derivation-Step 
                                      (from-bottom (pop-n size symbols))
                                      (mk-prod label lhs (top-n size symbols))
                                      (pick-token-names input)))
                               deriv)
                       f))
               (not (zerop size))
               (not (lessp (stack-length trees) size))
               (equal (node-count 'branches (from-bottom trees)) 
                      (length parse))
                      )
           (equal (node-count 'branches (from-bottom (sel-trees next)))
                  (length (sel-parse next))))
 ((disable reduce-trees)))

(prove-lemma inv-reductions (rewrite)
  (implies (and (equal next
                      (parsing-step (mk-configuration input states
                                                      symbols
                                                      trees parse
                                                      deriv f)
                                    tables grammar))
                (not  (equal trees (emptytree)))
                (equal (node-count 'branches (from-bottom trees)) 
                       (length parse)))
           (equal (node-count 'branches (from-bottom (sel-trees next)))
                  (length (sel-parse next))))
 ((disable reduce-trees )
  (induct (stack-length trees))))

;; ---------------------------------------------------------------------------
;;      Roots
;; ---------------------------------------------------------------------------

(prove-lemma roots-mk-tree (rewrite)
 (equal (roots (list (mk-tree a b))) (list a)))

(prove-lemma roots-append (rewrite)
 (implies (listp b)
          (equal (roots (append a b))
                 (append (roots a) (roots b)))))

(prove-lemma pick-token-names-append (rewrite)
 (equal (pick-token-names (append a b))
        (append (pick-token-names a) (pick-token-names b))))

(prove-lemma pick-token-names-list (rewrite)
 (implies (tokenp a)
          (equal (pick-token-names (list a))
                 (list (token-name a)))))

(prove-lemma inv-roots-shift (rewrite)
  (implies (and (equal next (mk-configuration
                             (cdr input)
                             (push s states)
                             (push (token-name (car input)) symbols)
                             (push (mk-tree (car input) nil) trees)
                             parse
                             deriv
                             f))
                (is-stack symbols)
                (token-listp input)
                (listp input)
                (is-stack trees)
                (equal (pick-token-names (roots (from-bottom trees)))
                       (from-bottom symbols)))
           (equal (pick-token-names (roots (from-bottom (sel-trees next))))
                  (from-bottom (sel-symbols next)))))

#|
;; ---------------------------------------------------------------------------
;; This is the statement of the roots reduction theorem
;; ---------------------------------------------------------------------------

;; The problem is: Sometimes the nodes are tokens (when they are leaves)
;; and sometimes they are just the names of the lhs. 
;; Even when I ensure that trees is a stack of trees - what if
;; a left hand side happens to be a token? Then it is not valid!
;; Proof abandonded at this point, as I would need to go back to the
;; definition of grammar and introduce an explicit shell for left hand
;; sides so that I can know that a left hand side can never be a token.

(prove-lemma inv-roots-reduce (rewrite)
  (implies (and (equal next 
                       (mk-configuration
                        input
                        (push goto (pop-n size states))
                        (push lhs (pop-n size symbols))
                        (reduce-trees lhs size trees)
                        (append parse (list label))
                        (append (list (mk-derivation-step 
                                       (from-bottom (pop-n size symbols))
                                       (mk-prod label lhs (top-n size symbols))
                                       (pick-token-names input)))
                                deriv)
                        f))
                (is-stack symbols)
                (token-listp input)
                (not (lessp (stack-length trees) size))
                (not (zerop size))
                (listp input)
                (is-stack trees)
                (stack-of-trees trees)
                (equal (pick-token-names (roots (from-bottom trees)))
                       (from-bottom symbols)))
           (equal (pick-token-names (roots (from-bottom (sel-trees next))))
                  (from-bottom (sel-symbols next)))))

(prove-lemma inv-roots (rewrite)
  (implies (and (equal next
                      (parsing-step (mk-configuration input states
                                                      symbols
                                                      trees parse
                                                      deriv f)
                                    tables grammar))
                (is-stack symbols)
                (token-listp input)
                (listp input)
                (is-stack trees)
                (equal (pick-token-names (roots (from-bottom trees)))
                       (from-bottom symbols)))
           (equal (pick-token-names (roots (from-bottom (sel-trees next))))
                  (from-bottom (sel-symbols next)))))
|#