File: g-direct.lisp

package info (click to toggle)
acl2 8.5dfsg-5
  • links: PTS
  • area: main
  • in suites: bookworm
  • size: 991,452 kB
  • sloc: lisp: 15,567,759; javascript: 22,820; cpp: 13,929; ansic: 12,092; perl: 7,150; java: 4,405; xml: 3,884; makefile: 3,507; sh: 3,187; ruby: 2,633; ml: 763; python: 746; yacc: 723; awk: 295; csh: 186; php: 171; lex: 154; tcl: 49; asm: 23; haskell: 17
file content (108 lines) | stat: -rw-r--r-- 2,966 bytes parent folder | download | duplicates (5)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
; (include-book "m1")
; (certify-book "g-direct" 1)

(in-package "M1")

(defun f (n)
         (if (zp n)
             1
           (* n (f (- n 1)))))

(defconst *g*
       '((PUSH 1)
         (STORE 1)
         (LOAD 0)
         (IFLE 10)
         (LOAD 0)
         (LOAD 1)
         (MUL)
         (STORE 1)
         (LOAD 0)
         (PUSH 1)
         (SUB)
         (STORE 0)
         (GOTO -10)
         (LOAD 1)
         (RETURN)))

(defun g-sched-loop (n)
  (if (zp n)
      (repeat 0 4)
    (append (repeat 0 11)
            (g-sched-loop (- n 1)))))

(defun g-sched (n)
  (append (repeat 0 2)
          (g-sched-loop n)))

(defun g (n a)
         (if (zp n)
             a
           (g (- n 1) (* n a))))

(defun run-g (n)
         (top
          (stack
           (run (g-sched n)
                (make-state 0
                            (list n 0)
                            nil
                            *g*)))))

; (run-g 5)
; (run-g 1000)

(defthm step-1-[loop]
         (implies (and (natp n)
                       (natp a))
                  (equal (run (g-sched-loop n)
                              (make-state 2
                                          (list n a)
                                          stk
                                          *g*))
                         (make-state 14
                                     (list 0 (g n a))
                                     (push (g n a) stk)
                                     *g*))))

(defthm step-1
         (implies (natp n)
                  (equal (run (g-sched n)
                              (make-state 0
                                          (list n a)
                                          stk
                                          *g*))
                         (make-state 14
                                     (list 0 (g n 1))
                                     (push (g n 1) stk)
                                     *g*))))

(in-theory (disable g-sched))

(defthm step-2
         (implies (natp a)
                  (equal (g n a)
                         (* a (f n)))))

(defthm main
         (implies (natp n)
                  (equal (run (g-sched n)
                              (make-state 0
                                          (list n a)
                                          stk
                                          *g*))
                         (make-state 14
                                     (list 0 (f n))
                                     (push (f n) stk)
                                     *g*))))

(defthm corollary
         (let ((s_fin (run (g-sched n)
                           (make-state 0
                                       (list n a)
                                       stk
                                       *g*))))
           (implies (natp n)
                    (and (equal (top (stack s_fin))
                                (f n))
                         (haltedp s_fin)))))