-
Notifications
You must be signed in to change notification settings - Fork 2
/
Assoc.agda
103 lines (86 loc) · 3.32 KB
/
Assoc.agda
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
module Ints.Add.Assoc where
open import Ints
open import Nats renaming (suc to nsuc; _+_ to _:+:_)
open import Nats.Add.Assoc
open import Nats.Add.Comm
open import Ints.Add.Comm
open import Equality
open import Function
------------------------------------------------------------------------
-- internal stuffs
private
0+a=a : ∀ a → + 0 + a ≡ a
0+a=a (+ n ) = refl
0+a=a (-[1+ n ]) = refl
a+0=a : ∀ a → a + + 0 ≡ a
a+0=a a rewrite int-add-comm a (+ 0) | 0+a=a a = refl
z+/b+c/=/z+b/+c : ∀ b c → + 0 + (b + c) ≡ (+ 0 + b) + c
z+/b+c/=/z+b/+c (+ a ) (+ b ) = refl
z+/b+c/=/z+b/+c (-[1+ a ]) (-[1+ b ]) = refl
z+/b+c/=/z+b/+c (+ a ) (-[1+ b ])
rewrite 0+a=a (a ⊖ nsuc b) = refl
z+/b+c/=/z+b/+c (-[1+ a ]) (+ b )
rewrite 0+a=a (b ⊖ nsuc a) = refl
a+b=a--b : ∀ a b → a + b ≡ a - (- b)
a+b=a--b a (+ zero ) = refl
a+b=a--b a (+ nsuc n)
rewrite a+b=a--b a (+ n) = refl
a+b=a--b a (-[1+ n ]) = refl
a-b+c=a+c-b : ∀ a b c → a ⊖ b + + c ≡ a :+: c ⊖ b
a-b+c=a+c-b zero zero _ = refl
a-b+c=a+c-b zero (nsuc _) _ = refl
a-b+c=a+c-b (nsuc _) zero _ = refl
a-b+c=a+c-b (nsuc a) (nsuc b) c = a-b+c=a+c-b a b c
a+/b-c/=a+b-c : ∀ a b c → + a + (b ⊖ c) ≡ a :+: b ⊖ c
a+/b-c/=a+b-c a b c
rewrite int-add-comm (+ a) $ b ⊖ c
| a-b+c=a+c-b b c a
| nat-add-comm a b
= refl
b-c-a=b-/c+a/ : ∀ a b c → b ⊖ c + -[1+ a ] ≡ b ⊖ (nsuc c :+: a)
b-c-a=b-/c+a/ _ zero zero = refl
b-c-a=b-/c+a/ _ zero (nsuc _) = refl
b-c-a=b-/c+a/ _ (nsuc _) zero = refl
b-c-a=b-/c+a/ a (nsuc b) (nsuc c) = b-c-a=b-/c+a/ a b c
-a+/b-c/=b-/a+c/ : ∀ a b c → -[1+ a ] + (b ⊖ c) ≡ b ⊖ (nsuc a :+: c)
-a+/b-c/=b-/a+c/ a b c
rewrite int-add-comm -[1+ a ] $ b ⊖ c
| b-c-a=b-/c+a/ a b c
| nat-add-comm a c
= refl
a+/b+c/=/a+b/+c : ∀ a b c → a + (b + c) ≡ a + b + c
a+/b+c/=/a+b/+c (+ zero) b c rewrite 0+a=a (b + c) | 0+a=a b = refl
a+/b+c/=/a+b/+c a (+ zero) c rewrite 0+a=a c | a+0=a a = refl
a+/b+c/=/a+b/+c a b (+ zero) rewrite a+0=a b | a+0=a (a + b) = refl
a+/b+c/=/a+b/+c (+ a) (+ b) (+ c)
rewrite nat-add-assoc a b c = refl
a+/b+c/=/a+b/+c -[1+ a ] -[1+ b ] (+ nsuc c)
rewrite -a+/b-c/=b-/a+c/ a c b = refl
a+/b+c/=/a+b/+c -[1+ a ] (+ nsuc b) -[1+ c ]
rewrite -a+/b-c/=b-/a+c/ a b c
| b-c-a=b-/c+a/ c b a
= refl
a+/b+c/=/a+b/+c (+ nsuc a) -[1+ b ] -[1+ c ]
rewrite b-c-a=b-/c+a/ c a b = refl
a+/b+c/=/a+b/+c (+ nsuc a) -[1+ b ] (+ nsuc c)
rewrite a-b+c=a+c-b a b $ nsuc c
| a+/b-c/=a+b-c (nsuc a) c b
| sym $ nat-add-assoc a 1 c
| nat-add-comm a 1
= refl
a+/b+c/=/a+b/+c -[1+ a ] (+ nsuc b) (+ nsuc c)
rewrite a-b+c=a+c-b b a (nsuc c) = refl
a+/b+c/=/a+b/+c -[1+ a ] -[1+ b ] -[1+ c ]
rewrite nat-add-comm a $ nsuc $ b :+: c
| nat-add-comm (b :+: c) a
| nat-add-assoc a b c
= refl
a+/b+c/=/a+b/+c (+ nsuc a) (+ nsuc b) -[1+ c ]
rewrite a+/b-c/=a+b-c (nsuc a) b c
| sym $ nat-add-assoc a 1 b
| nat-add-comm a 1
= refl
------------------------------------------------------------------------
-- public aliases
int-add-assoc : ∀ a b c → a + (b + c) ≡ a + b + c
int-add-assoc = a+/b+c/=/a+b/+c