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
|
; $Id: root.scm 2156 2008-01-25 13:25:12Z schimans $
; We prove the existence of integer square roots.
; (load "~/minlog/init.scm")
(set! COMMENT-FLAG #f)
(libload "nat.scm")
(set! COMMENT-FLAG #t)
(set! DOT-NOTATION #f)
(add-var-name "f" "g" (py "nat=>nat"))
; "IntSqRt"
(set-goal (pf "all f,g,n(
all n(n<f 0 -> bot) -> all n n<f(g n) -> excl m((n<f m -> bot) ! n<f(m+1)))"))
(assume "f" "g" "n" 1 2 3)
(cut (pf "all m(n<f m -> bot)"))
(search)
(ind)
(search)
(search)
; Proof finished
(save "IntSqRt")
(proof-to-expr (theorem-name-to-proof "IntSqRt"))
(proof-to-expr (np (theorem-name-to-proof "IntSqRt")))
; (lambda (f)
; (lambda (g)
; (lambda (n)
; (lambda (u483)
; (lambda (u484)
; (lambda (u485)
; ((((((|Ind| n) f) (u483 n)) u485) (g n)) (u484 n))))))))
(define min-excl-proof (np (theorem-name-to-proof "IntSqRt")))
(define et (atr-min-excl-proof-to-structured-extracted-term min-excl-proof))
(define net (nt et))
(pp net)
; [f0,f1,n2](Rec nat=>nat)0([n3,n4][if (n2<f0 n3) n4 n3])(f1 n2)
(define sqr (pt "[n]n*n"))
(pp (nt (mk-term-in-app-form net sqr (pt "Succ") (pt "3")))) ;"1"
(pp (nt (mk-term-in-app-form net sqr (pt "Succ") (pt "4")))) ;"2"
(pp (nt (mk-term-in-app-form net sqr (pt "Succ") (pt "8")))) ;"2"
(pp (nt (mk-term-in-app-form net sqr (pt "Succ") (pt "9")))) ;"3"
(pp (nt (mk-term-in-app-form net sqr (pt "Succ") (pt "15")))) ;"3"
(pp (nt (mk-term-in-app-form net sqr (pt "Succ") (pt "16")))) ;"4"
; Alternative proof, using an axiomatized <=. Assume
; 1: all n (f 0)<=n
; 2: all n n<f(g n)
; Then there is an m such that f(m) <= n < f(m+1).
; For the proof one uses
(aga "Lemma1" (pf "all n,m((n<m -> F) -> m<=n)"))
(aga "Lemma2" (pf "all n,m(n<m -> m<=n -> F)"))
; (define root
; (pf "all f,g.all n f 0<=n ->
; all n n<f(g n) ->
; all n.(all m.f m<=n -> n<f(m+1) -> F) -> F"))
; (set-goal root)
; (assume "f" "g" 1 2 "n" 3)
; (use-with "Lemma2"
; (pt "n") (pt "f(g n)") DEFAULT-GOAL-NAME DEFAULT-GOAL-NAME)
; (use 2)
; (cut (pf "all m f(m)<=n"))
; (assume 4)
; (use 4)
; (ind)
; (use 1)
; (assume "m" 4)
;
; (use-with "Lemma1" (pt "n") (pt "f(m+1)") DEFAULT-GOAL-NAME)
; (use 3)
; (use 4)
; (rga "Lemma1" "Lemma2")
|
