burstall.vlisp
0 ;Mercredi 8 Mai 2002 17:34:48 file : burstall.vlisp ;
1
2 ; ----- micro verifieur de preuves par induction;
3 ; de proprietes de programmes lisp (TRES pur);
4 ; d'apres pg;
5
6 (include "evalsym.vlisp")
7
8 (df theo (l) (prove l 0))
9
10 ; ex: (theo (p m n) = (p n m));
11
12 (de prove (th n ;; thh)
13 ; th = (* = **);
14 (pstar (nconc [n 'prove] th))
15 (cond
16 ((eq (setq thh (reduce th)) t))
17 ((equal th thh) (command))
18 (t (prove thh (1+ n))))
19 (pstar [n 'proved]))
20
21 (de pstar (l) (prin1 '**) (apply 'print l))
22
23 (de command (;; com pat remp nboc)
24 (print "command ?")
25 (setq com (read))
26 (selectq (car com)
27 (induct
28 (cond
29 ((eq (cadr com) 'list) (listinduct (caddr com) th))
30 ((eq (cadr com) 'num) (numinduct (caddr com) th))
31 (t (print "wrong type") (command))))
32 (indhyp
33 (setq nboc (cadr com))
34 (if (eq (caddr com) '->) (setq pat (car ih) remp (caddr ih)) (setq pat (caddr ih) remp (car ih)))
35 (prove (useindhyp th) (1+ n)))
36 (gen
37 (prove
38 (let ((th th) (lsub (cdr com))) (if lsub (self (subst (nextl lsub) (nextl lsub) th) lsub) th))
39 (1+ n)))
40 (look (print (eval (cadr com))) (command))
41 (t (print "unknown command") (command))))
42
43 (de reduce (thh ;; x y)
44 (setq x (symeval (car thh) nil) y (symeval (caddr thh) nil))
45 (pstar ['reduit 'a x '= y])
46 (or (equal x y) [x '= y]))
47
48 (de listinduct (var ih)
49 ; ih = hypothese d'induction;
50 (pstar ['base])
51 (prove (subst nil var ih) (1+ n))
52 (pstar ['step])
53 (prove (subst ['cons (gensym) var] var ih) (1+ n)))
54
55 (de numinduct (var ih)
56 (pstar ['base])
57 (prove (subst 0 var ih) (1+ n))
58 (pstar ['step])
59 (prove (subst ['1+ var] var ih) (1+ n)))
60
61 (de useindhyp (th)
62 (cond
63 ((atom th) (if (neq th pat) th (decr nboc) (if (= nboc 0) remp th)))
64 ((equal th pat) (decr nboc) (if (= nboc 0) remp [(useindhyp (nextl th)) . (useindhyp th)]))
65 (t [(useindhyp (nextl th)) . (useindhyp th)])))
66
67
Cross Reference
command de 23
listinduct de 48
numinduct de 55
prove de 12
pstar de 21
reduce de 43
theo df 8
useindhyp de 61
1 -> 34
2 a 45
3 base 50 56
4 com 23 25 26 29 29 30 30 33 34 38 40
5 command 17 23 31 40 41
6 gen 36
7 ih 34 34 34 34 48 51 53 55 57 59
8 indhyp 32
9 induct 27
10 l 8 8 21 21
11 listinduct 29 48
12 look 40
13 lsub 38 38 38 38 38
14 n 12 14 18 19 35 39 51 53 57 59
15 nboc 23 33 63 63 64 64
16 num 30
17 numinduct 30 55
18 pat 23 34 34 63 64
19 prove 8 12 14 18 35 37 51 53 57 59
20 proved 19
21 pstar 14 19 21 45 50 52 56 58
22 reduce 16 43
23 reduit 45
24 remp 23 34 34 63 64
25 symeval 44 44
26 th 12 14 16 17 29 30 35 38 38 38 38 61 63 63 63
63 64 64 64 65 65
27 theo 8
28 thh 12 16 17 18 43 44 44
29 useindhyp 35 61 64 64 65 65
30 x 43 44 45 46 46
31 y 43 44 45 46 46
;Mercredi 8 Mai 2002 17:34:48 end of file : burstall.vlisp ;