Skip to content

Commit

Permalink
Paco: use o< instead of e0-ord-<
Browse files Browse the repository at this point in the history 
Use o< well-founded relation instead of e0-ord-< .
Disble unnecessary functions in measure proofs.
Remove speedup lemmas which becomes unnecessary.
  • Loading branch information
@nadezhin
nadezhin committed Jan 6, 2017
1 parent 8be1d20 commit 8b0c2e2
Show file tree
Hide file tree
Showing 5 changed files with 80 additions and 251 deletions.
13 changes: 5 additions & 8 deletions books/projects/paco/induct.lisp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -363,12 +363,10 @@
; ACL2 does not detect such loops. Paco limits them: it doesn't allow
; more than nnn rules to be invoked on any path.

(acl2::set-well-founded-relation e0-ord-<)

(mutual-recursion

(defun apply-induction-rule (rule term type-alist xterm ens wrld nnn)
(declare (xargs :measure (cons (cons (+ 1 (nfix nnn)) 3) 0)
(declare (xargs :measure (acl2::nat-list-measure (list nnn 3 0))
:hints (("Goal" :in-theory (disable type-set
one-way-unify1)))))

Expand Down Expand Up @@ -412,8 +410,8 @@
(defun suggested-induction-cands1 (induction-rules term type-alist
xterm ens wrld nnn)

(declare (xargs :measure (cons (cons (+ 1 (nfix nnn)) 1)
(acl2-count induction-rules))))
(declare (xargs :measure (acl2::nat-list-measure
(list nnn 1 (acl2-count induction-rules)))))

; We map down induction-rules and apply each enabled rule to term,
; which is known to be an application of the function symbol fn to
Expand Down Expand Up @@ -446,7 +444,7 @@
ens wrld nnn)))))

(defun suggested-induction-cands (term type-alist xterm ens wrld nnn)
(declare (xargs :measure (cons (cons (+ 1 (nfix nnn)) 2) 0)))
(declare (xargs :measure (acl2::nat-list-measure (list nnn 2 0))))

; Term is some fn applied to args. Xterm is some term occurring in the
; conjecture we are exploring and is the term upon which this induction
Expand Down Expand Up @@ -1434,8 +1432,7 @@
; Abstractly, this function closes B under fn, where B is the bag
; union of the unprocessed bag and ans.

(declare (xargs :measure (cons (+ 1 (len pairs))
(count-undel pairs del))
(declare (xargs :measure (acl2::two-nats-measure (len pairs) (count-undel pairs del))
:hints (("Goal" :in-theory (disable m&m-search)))))
(cond
((endp pairs) ans)
Expand Down
2 changes: 0 additions & 2 deletions books/projects/paco/prove.lisp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -228,8 +228,6 @@
; the first 3 components are relevant. The last is always 0; I didn't
; have lex3.

(acl2::set-well-founded-relation e0-ord-<)

(mutual-recursion

(defun waterfall (ledge id cl hist pspv wrld nnn)
Expand Down
86 changes: 22 additions & 64 deletions books/projects/paco/rewrite.lisp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -848,58 +848,18 @@
(plist-to-alist (cdr args)))))


; Theorems used to speed up the admission of the rewrite clique.

(defthm rewrite-clique-speedup-26
(implies
(not (zp nnn))
(e0-ord-<
(cons (cons (cons (+ 1 (nfix (+ -1 nnn))) 6)
(acl2-count (mv-nth 1
(let nil
(cond ((atom term) (list nil term))
((equal 'quote (car term))
(list nil term))
((equal (car term) 'not)
(list 'not (cadr term)))
((and (equal (car term) 'if)
(equal (caddr term) ''nil)
(equal (cadddr term) ''t))
(list 'if (cadr term)))
(t (list nil term)))))))
0)
(cons (cons (cons (+ 1 (nfix nnn)) 0) 0)
0))))

(defthm rewrite-clique-speedup-5
(implies
(not (zp nnn))
(e0-ord-<
(cons
(cons
(cons (+ 1 (nfix nnn)) 1)
any)
0)
(cons (cons (cons (+ 1 (nfix nnn)) 4) 0)
0)))
:rule-classes nil)

(defthm rewrite-clique-speedup-4
(implies
(not (zp nnn))
(e0-ord-<
(cons
(cons
(cons (+ 1 (nfix (+ -1 nnn))) 6)
any)
0)
(cons (cons (cons (+ 1 (nfix nnn)) 4) 0)
0)))
:rule-classes nil)

; The rewrite clique:

(ACL2::SET-WELL-FOUNDED-RELATION e0-ord-<)
(local (defthm rewrite-admission-lemma1
(implies (consp x)
(acl2::posp (acl2-count x)))))

(local (defthm rewrite-admission-lemma2
(implies (not (equal (caddr x) (cadddr x)))
(< (+ 1 (acl2-count (cadr x))
(acl2-count (caddr x))
(acl2-count (cadddr x)))
(acl2-count x)))))

(mutual-recursion

Expand All @@ -911,20 +871,18 @@
:hints (("Goal"
:in-theory
(disable assume-true-false
type-set))
("Subgoal 27" :do-not '(preprocess)
:by rewrite-clique-speedup-5)
("Subgoal 26" :do-not '(preprocess)
:by rewrite-clique-speedup-4)
; ("Subgoal 17" :do-not '(preprocess)
; :by rewrite-clique-speedup-5)
; ("Subgoal 16" :do-not '(preprocess)
; :by rewrite-clique-speedup-4)
; ("Subgoal 5" :do-not '(preprocess)
; :by rewrite-clique-speedup-5)
; ("Subgoal 4" :do-not '(preprocess)
; :by rewrite-clique-speedup-4)
)))
type-set
ancestors-check
sublis-var
enabled-numep
one-way-unify acl2-count
member-eq acl2::member-equal
refinementp
legal-variablep
apply
search-type-alist
var-fn-count
logand)))))

(cond ((zp nnn) (sublis-var alist term))
((variablep term)
Expand Down
31 changes: 11 additions & 20 deletions books/projects/paco/simplify.lisp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -390,8 +390,8 @@

(defun subsumes (cl1 cl2 alist)

(declare (xargs :measure (cons (cons (+ 1 (acl2-count cl1)) 1)
(acl2-count cl2))))
(declare (xargs :measure (acl2::nat-list-measure
(list (acl2-count cl1) 1 (acl2-count cl2)))))

; We return t iff some instance of clause cl1 is a subset of
; clause cl2 (where the instance is an extension of alist).
Expand All @@ -401,8 +401,8 @@

(defun subsumes1 (lit tl1 tl2 cl2 alist)

(declare (xargs :measure (cons (cons (+ 1 (acl2-count tl1)) 2)
(acl2-count tl2))))
(declare (xargs :measure (acl2::nat-list-measure
(list (acl2-count tl1) 2 (acl2-count tl2)))))

; If we can extend alist to an alist1 so that lit/alist1 is a member
; of tl2 and tl1/alist1 is a subset of cl2, we return t. Else we
Expand Down Expand Up @@ -560,15 +560,6 @@
(crunch-clause-segments2 cl nil)
(mv seg1 seg2)))))))

(defthm rewrite-clause-speedup-1
(implies (not (zp nnn))
(E0-ORD-<
(CONS
(CONS (+ 1 (nfix (+ -1 nnn))) 2) x)
(CONS (CONS (+ 1 (nfix nnn)) 1) y)))
:rule-classes nil)

(acl2::set-well-founded-relation e0-ord-<)

(mutual-recursion

Expand All @@ -578,15 +569,15 @@
; tail), where tail is the first argument supplied to rewrite-clause.
; See the note below about the admission of this function.

(declare (xargs :measure (cons (cons (+ 1 (nfix nnn)) 1) 0)
(declare (xargs :measure (acl2::nat-list-measure (list nnn 1 0))
:hints (("Goal" :in-theory
(disable remove-trivial-equivalences
crunch-clause-segments
DISJOIN-CLAUSE-SEGMENT-TO-CLAUSE-SET
NORMALIZE))
("Subgoal 1" :do-not '(preprocess)
:by rewrite-clause-speedup-1)
)))
NORMALIZE
type-alist-clause
strip-branches
acl2-count)))))

; We are to rewrite the literals of the clause cl formed by appending
; tail to new-clause. We assume rcnst has the correct top-clause and
Expand Down Expand Up @@ -657,7 +648,7 @@


(defun rewrite-clause-lst (segs cdr-tail new-clause wrld rcnst flg ans nnn)
(declare (xargs :measure (cons (cons (+ 1 (nfix nnn)) 2) (len segs))))
(declare (xargs :measure (acl2::nat-list-measure (list nnn 2 (len segs)))))
(cond
((endp segs) (mv flg ans))
(t
Expand Down Expand Up @@ -959,4 +950,4 @@
(declare (ignore id wrld))
(cond ((hit-it-againp hist)
(mv 'HIT (list clause) nil pspv))
(t (mv 'MISS nil nil nil))))
(t (mv 'MISS nil nil nil))))

0 comments on commit 8b0c2e2

Please sign in to comment.