blob: 3d0329fb4b6b06c07714791ed4a737e063fc878a (
plain)
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
|
(use-modules (vikalpa)
(vikalpa the-little-prover))
(define-system the-little-prover-0 (the-little-prover)
(define-theorem simple-list-induction (x)
(equal? (if (natural? (size x))
(if (atom? x) '#t (< (size (cdr x)) (size x)))
'#t)
#t))
(define-proof simple-list-induction
()
(((1 2 3) size/cdr)
((1 2) if-same)
((1) if-same)
(() equal-same)))
(define-function list-length (xs)
(if (atom? xs)
'0
(+ '1 (list-length (cdr xs)))))
(define-proof list-length
(natural? (size xs))
((() simple-list-induction)))
(define-theorem natural?/1 ()
(equal? (natural? 1) #t))
(define-proof natural?/1
()
((() if-same (set x (natural? '0)))
((2 1) natural?/succ)
((2) equal-same)
((1) natural?/0)
(() if-true)))
(define-theorem natural?/list-length (xs)
(natural? (list-length xs)))
(define-proof natural?/list-length
(list-induction xs)
(((2 1) list-length)
((2 1) if-nest-A)
((2) natural?/0)
((3 2 1) list-length)
((3 2 1) if-nest-E)
((3) if-same (set x (natural? (succ '0))))
((3 2 2) natural?/+)
((3 2) if-same)
((3 1) natural?/1)
((3) if-true)
(() if-same))))
|
