-
Notifications
You must be signed in to change notification settings - Fork 0
/
chapter8-3-plus-assoc.rkt
102 lines (77 loc) · 1.76 KB
/
chapter8-3-plus-assoc.rkt
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
#lang pie
;; Define a function called plus-assoc that states and proves that
;; + is associative.
;; (claim plus-assoc
;; (Pi ((n Nat) (m Nat) (k Nat))
;; (= Nat (+ k (+ n m)) (+ (+ k n) m))))
(claim + (-> Nat Nat Nat))
(define +
(lambda (a b)
(rec-Nat a
b
(lambda (_ b+a-1)
(add1 b+a-1)))))
;; practice by first proving that n=0+n
(claim n=0+n
(Pi ((n Nat))
(= Nat n (+ 0 n))))
(define n=0+n
(lambda (n)
(same n)))
;; practice by first proving that n=n+0
(claim n=n+0
(Pi ((n Nat))
(= Nat n (+ n 0))))
(claim mot-n=n+0
(-> Nat U))
(define mot-n=n+0
(lambda (n)
(= Nat n (+ n 0))))
(claim base-n=n+0
(= Nat 0 (+ 0 0)))
(define base-n=n+0
(same 0))
(claim step-n=n+0
(Pi ((n-1 Nat))
(-> (mot-n=n+0 n-1)
(mot-n=n+0 (add1 n-1)))))
(define step-n=n+0
(lambda (n-1)
(lambda (n-1=n-1+0)
(cong n-1=n-1+0 (+ 1)))))
(define n=n+0
(lambda (n)
(ind-Nat n
mot-n=n+0
base-n=n+0
step-n=n+0
)))
;; start actual exercise
(claim mot-plus-assoc
(-> Nat Nat Nat U))
(define mot-plus-assoc
(lambda (n m k)
(= Nat (+ k (+ n m)) (+ (+ k n) m))))
(claim base-plus-assoc
(Pi ((n Nat) (m Nat))
(= Nat (+ 0 (+ n m)) (+ (+ 0 n) m))))
(define base-plus-assoc
(lambda (n m)
(same (+ n m))))
(claim step-plus-assoc
(Pi ((n Nat) (m Nat) (k-1 Nat))
(-> (mot-plus-assoc n m k-1)
(mot-plus-assoc n m (add1 k-1)))))
(define step-plus-assoc
(lambda (n m k-1)
(lambda (mot-plus-assoc-k-1)
(cong mot-plus-assoc-k-1 (+ 1)))))
(claim plus-assoc
(Pi ((n Nat) (m Nat) (k Nat))
(= Nat (+ k (+ n m)) (+ (+ k n) m))))
(define plus-assoc
(lambda (n m k)
(ind-Nat k
(mot-plus-assoc n m)
(base-plus-assoc n m)
(step-plus-assoc n m))))