Mercurial > hg > Members > atton > agda-proofs

annotate systemT/int.agda @ 57:75f9f71f364a

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Trying define maybe-subtype
author atton <atton@cr.ie.u-ryukyu.ac.jp>
date Thu, 12 Jan 2017 01:04:59 +0000
parents fe247f476ecb
children
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
rev   line source
1
fe247f476ecb Migrate systemT from atton/agda/systemT (13:5a81867278af)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
1 open import systemT
fe247f476ecb Migrate systemT from atton/agda/systemT (13:5a81867278af)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
2 open import Relation.Binary.PropositionalEquality
fe247f476ecb Migrate systemT from atton/agda/systemT (13:5a81867278af)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
3 open ≡-Reasoning
fe247f476ecb Migrate systemT from atton/agda/systemT (13:5a81867278af)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
4
fe247f476ecb Migrate systemT from atton/agda/systemT (13:5a81867278af)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
5 module int where
fe247f476ecb Migrate systemT from atton/agda/systemT (13:5a81867278af)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
6
fe247f476ecb Migrate systemT from atton/agda/systemT (13:5a81867278af)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
7 double : Int -> Int
fe247f476ecb Migrate systemT from atton/agda/systemT (13:5a81867278af)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
8 double O = O
fe247f476ecb Migrate systemT from atton/agda/systemT (13:5a81867278af)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
9 double (S n) = S (S (double n))
fe247f476ecb Migrate systemT from atton/agda/systemT (13:5a81867278af)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
10
fe247f476ecb Migrate systemT from atton/agda/systemT (13:5a81867278af)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
11
fe247f476ecb Migrate systemT from atton/agda/systemT (13:5a81867278af)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
12 infixl 30 _+_
fe247f476ecb Migrate systemT from atton/agda/systemT (13:5a81867278af)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
13 _+_ : Int -> Int -> Int
fe247f476ecb Migrate systemT from atton/agda/systemT (13:5a81867278af)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
14 n + O = n
fe247f476ecb Migrate systemT from atton/agda/systemT (13:5a81867278af)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
15 n + (S m) = S (n + m)
fe247f476ecb Migrate systemT from atton/agda/systemT (13:5a81867278af)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
16
fe247f476ecb Migrate systemT from atton/agda/systemT (13:5a81867278af)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
17 left-add-zero : (n : Int) -> O + n ≡ n
fe247f476ecb Migrate systemT from atton/agda/systemT (13:5a81867278af)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
18 left-add-zero O = refl
fe247f476ecb Migrate systemT from atton/agda/systemT (13:5a81867278af)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
19 left-add-zero (S n) = cong S (left-add-zero n)
fe247f476ecb Migrate systemT from atton/agda/systemT (13:5a81867278af)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
20
fe247f476ecb Migrate systemT from atton/agda/systemT (13:5a81867278af)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
21 left-add-one : (n : Int) -> (S n) ≡ S O + n
fe247f476ecb Migrate systemT from atton/agda/systemT (13:5a81867278af)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
22 left-add-one O = refl
fe247f476ecb Migrate systemT from atton/agda/systemT (13:5a81867278af)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
23 left-add-one (S n) = cong S (left-add-one n)
fe247f476ecb Migrate systemT from atton/agda/systemT (13:5a81867278af)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
24
fe247f476ecb Migrate systemT from atton/agda/systemT (13:5a81867278af)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
25 left-increment : (n m : Int) -> (S n) + m ≡ S (n + m)
fe247f476ecb Migrate systemT from atton/agda/systemT (13:5a81867278af)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
26 left-increment n O = refl
fe247f476ecb Migrate systemT from atton/agda/systemT (13:5a81867278af)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
27 left-increment n (S m) = cong S (left-increment n m)
fe247f476ecb Migrate systemT from atton/agda/systemT (13:5a81867278af)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
28
fe247f476ecb Migrate systemT from atton/agda/systemT (13:5a81867278af)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
29 sum-sym : (x : Int) (y : Int) -> x + y ≡ y + x
fe247f476ecb Migrate systemT from atton/agda/systemT (13:5a81867278af)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
30 sum-sym O O = refl
fe247f476ecb Migrate systemT from atton/agda/systemT (13:5a81867278af)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
31 sum-sym O (S y) = cong S (sum-sym O y)
fe247f476ecb Migrate systemT from atton/agda/systemT (13:5a81867278af)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
32 sum-sym (S x) O = cong S (sum-sym x O)
fe247f476ecb Migrate systemT from atton/agda/systemT (13:5a81867278af)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
33 sum-sym (S x) (S y) = begin
fe247f476ecb Migrate systemT from atton/agda/systemT (13:5a81867278af)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
34 (S x) + (S y)
fe247f476ecb Migrate systemT from atton/agda/systemT (13:5a81867278af)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
35 ≡⟨ refl ⟩
fe247f476ecb Migrate systemT from atton/agda/systemT (13:5a81867278af)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
36 S ((S x) + y)
fe247f476ecb Migrate systemT from atton/agda/systemT (13:5a81867278af)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
37 ≡⟨ cong S (sum-sym (S x) y) ⟩
fe247f476ecb Migrate systemT from atton/agda/systemT (13:5a81867278af)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
38 S (y + (S x))
fe247f476ecb Migrate systemT from atton/agda/systemT (13:5a81867278af)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
39 ≡⟨ (sym (left-increment y (S x))) ⟩
fe247f476ecb Migrate systemT from atton/agda/systemT (13:5a81867278af)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
40 (S y) + (S x)
fe247f476ecb Migrate systemT from atton/agda/systemT (13:5a81867278af)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
41 ∎
fe247f476ecb Migrate systemT from atton/agda/systemT (13:5a81867278af)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
42
fe247f476ecb Migrate systemT from atton/agda/systemT (13:5a81867278af)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
43 sum-assoc : (x y z : Int) -> x + (y + z) ≡ (x + y) + z
fe247f476ecb Migrate systemT from atton/agda/systemT (13:5a81867278af)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
44 sum-assoc O O O = refl
fe247f476ecb Migrate systemT from atton/agda/systemT (13:5a81867278af)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
45 sum-assoc O O (S z) = cong S (sum-assoc O O z)
fe247f476ecb Migrate systemT from atton/agda/systemT (13:5a81867278af)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
46 sum-assoc O (S y) O = refl
fe247f476ecb Migrate systemT from atton/agda/systemT (13:5a81867278af)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
47 sum-assoc O (S y) (S z) = cong S (sum-assoc O (S y) z)
fe247f476ecb Migrate systemT from atton/agda/systemT (13:5a81867278af)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
48 sum-assoc (S x) O O = refl
fe247f476ecb Migrate systemT from atton/agda/systemT (13:5a81867278af)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
49 sum-assoc (S x) O (S z) = cong S (sum-assoc (S x) O z)
fe247f476ecb Migrate systemT from atton/agda/systemT (13:5a81867278af)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
50 sum-assoc (S x) (S y) O = refl
fe247f476ecb Migrate systemT from atton/agda/systemT (13:5a81867278af)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
51 sum-assoc (S x) (S y) (S z) = cong S (sum-assoc (S x) (S y) z)
fe247f476ecb Migrate systemT from atton/agda/systemT (13:5a81867278af)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
52
fe247f476ecb Migrate systemT from atton/agda/systemT (13:5a81867278af)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
53
fe247f476ecb Migrate systemT from atton/agda/systemT (13:5a81867278af)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
54 infixl 40 _*_
fe247f476ecb Migrate systemT from atton/agda/systemT (13:5a81867278af)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
55 _*_ : Int -> Int -> Int
fe247f476ecb Migrate systemT from atton/agda/systemT (13:5a81867278af)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
56 n * O = O
fe247f476ecb Migrate systemT from atton/agda/systemT (13:5a81867278af)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
57 n * (S O) = n
fe247f476ecb Migrate systemT from atton/agda/systemT (13:5a81867278af)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
58 n * (S m) = n + (n * m)
fe247f476ecb Migrate systemT from atton/agda/systemT (13:5a81867278af)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
59
fe247f476ecb Migrate systemT from atton/agda/systemT (13:5a81867278af)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
60 right-mult-zero : (n : Int) -> n * O ≡ O
fe247f476ecb Migrate systemT from atton/agda/systemT (13:5a81867278af)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
61 right-mult-zero n = refl
fe247f476ecb Migrate systemT from atton/agda/systemT (13:5a81867278af)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
62
fe247f476ecb Migrate systemT from atton/agda/systemT (13:5a81867278af)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
63 right-mult-one : (n : Int) -> n * (S O) ≡ n
fe247f476ecb Migrate systemT from atton/agda/systemT (13:5a81867278af)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
64 right-mult-one n = refl
fe247f476ecb Migrate systemT from atton/agda/systemT (13:5a81867278af)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
65
fe247f476ecb Migrate systemT from atton/agda/systemT (13:5a81867278af)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
66 right-mult-distr-one : (n m : Int) -> n * (S m) ≡ n + (n * m)
fe247f476ecb Migrate systemT from atton/agda/systemT (13:5a81867278af)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
67 right-mult-distr-one O O = refl
fe247f476ecb Migrate systemT from atton/agda/systemT (13:5a81867278af)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
68 right-mult-distr-one O (S m) = refl
fe247f476ecb Migrate systemT from atton/agda/systemT (13:5a81867278af)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
69 right-mult-distr-one (S n) O = refl
fe247f476ecb Migrate systemT from atton/agda/systemT (13:5a81867278af)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
70 right-mult-distr-one (S n) (S m) = refl
fe247f476ecb Migrate systemT from atton/agda/systemT (13:5a81867278af)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
71
fe247f476ecb Migrate systemT from atton/agda/systemT (13:5a81867278af)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
72
fe247f476ecb Migrate systemT from atton/agda/systemT (13:5a81867278af)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
73 left-mult-zero : (n : Int) -> O * n ≡ O
fe247f476ecb Migrate systemT from atton/agda/systemT (13:5a81867278af)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
74 left-mult-zero O = refl
fe247f476ecb Migrate systemT from atton/agda/systemT (13:5a81867278af)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
75 left-mult-zero (S n) = begin
fe247f476ecb Migrate systemT from atton/agda/systemT (13:5a81867278af)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
76 O * (S n)
fe247f476ecb Migrate systemT from atton/agda/systemT (13:5a81867278af)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
77 ≡⟨ right-mult-distr-one O n ⟩
fe247f476ecb Migrate systemT from atton/agda/systemT (13:5a81867278af)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
78 O + (O * n)
fe247f476ecb Migrate systemT from atton/agda/systemT (13:5a81867278af)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
79 ≡⟨ sum-sym O (O * n) ⟩
fe247f476ecb Migrate systemT from atton/agda/systemT (13:5a81867278af)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
80 (O * n) + O
fe247f476ecb Migrate systemT from atton/agda/systemT (13:5a81867278af)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
81 ≡⟨ refl ⟩
fe247f476ecb Migrate systemT from atton/agda/systemT (13:5a81867278af)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
82 (O * n)
fe247f476ecb Migrate systemT from atton/agda/systemT (13:5a81867278af)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
83 ≡⟨ left-mult-zero n ⟩
fe247f476ecb Migrate systemT from atton/agda/systemT (13:5a81867278af)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
84 O
fe247f476ecb Migrate systemT from atton/agda/systemT (13:5a81867278af)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
85 ∎
fe247f476ecb Migrate systemT from atton/agda/systemT (13:5a81867278af)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
86
fe247f476ecb Migrate systemT from atton/agda/systemT (13:5a81867278af)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
87 left-mult-one : (n : Int) -> (S O) * n ≡ n
fe247f476ecb Migrate systemT from atton/agda/systemT (13:5a81867278af)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
88 left-mult-one O = refl
fe247f476ecb Migrate systemT from atton/agda/systemT (13:5a81867278af)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
89 left-mult-one (S n) = begin
fe247f476ecb Migrate systemT from atton/agda/systemT (13:5a81867278af)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
90 (S O) * S n
fe247f476ecb Migrate systemT from atton/agda/systemT (13:5a81867278af)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
91 ≡⟨ right-mult-distr-one (S O) n ⟩
fe247f476ecb Migrate systemT from atton/agda/systemT (13:5a81867278af)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
92 (S O) + ((S O) * n)
fe247f476ecb Migrate systemT from atton/agda/systemT (13:5a81867278af)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
93 ≡⟨ cong (_+_ (S O)) (left-mult-one n) ⟩
fe247f476ecb Migrate systemT from atton/agda/systemT (13:5a81867278af)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
94 (S O) + n
fe247f476ecb Migrate systemT from atton/agda/systemT (13:5a81867278af)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
95 ≡⟨ sum-sym (S O) n ⟩
fe247f476ecb Migrate systemT from atton/agda/systemT (13:5a81867278af)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
96 n + (S O)
fe247f476ecb Migrate systemT from atton/agda/systemT (13:5a81867278af)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
97 ≡⟨ refl ⟩
fe247f476ecb Migrate systemT from atton/agda/systemT (13:5a81867278af)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
98 S n
fe247f476ecb Migrate systemT from atton/agda/systemT (13:5a81867278af)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
99 ∎
fe247f476ecb Migrate systemT from atton/agda/systemT (13:5a81867278af)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
100
fe247f476ecb Migrate systemT from atton/agda/systemT (13:5a81867278af)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
101
fe247f476ecb Migrate systemT from atton/agda/systemT (13:5a81867278af)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
102 left-mult-distr-one : (n m : Int) -> (S n) * m ≡ m + (n * m)
fe247f476ecb Migrate systemT from atton/agda/systemT (13:5a81867278af)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
103 left-mult-distr-one O O = refl
fe247f476ecb Migrate systemT from atton/agda/systemT (13:5a81867278af)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
104 left-mult-distr-one O (S m) = begin
fe247f476ecb Migrate systemT from atton/agda/systemT (13:5a81867278af)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
105 (S O) * S m
fe247f476ecb Migrate systemT from atton/agda/systemT (13:5a81867278af)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
106 ≡⟨ left-mult-one (S m) ⟩
fe247f476ecb Migrate systemT from atton/agda/systemT (13:5a81867278af)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
107 S m
fe247f476ecb Migrate systemT from atton/agda/systemT (13:5a81867278af)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
108 ≡⟨ refl ⟩
fe247f476ecb Migrate systemT from atton/agda/systemT (13:5a81867278af)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
109 S m + O
fe247f476ecb Migrate systemT from atton/agda/systemT (13:5a81867278af)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
110 ≡⟨ cong (_+_ (S m)) (sym (left-mult-zero (S m))) ⟩
fe247f476ecb Migrate systemT from atton/agda/systemT (13:5a81867278af)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
111 S m + (O * S m)
fe247f476ecb Migrate systemT from atton/agda/systemT (13:5a81867278af)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
112 ∎
fe247f476ecb Migrate systemT from atton/agda/systemT (13:5a81867278af)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
113 left-mult-distr-one (S n) O = refl
fe247f476ecb Migrate systemT from atton/agda/systemT (13:5a81867278af)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
114 left-mult-distr-one (S n) (S m) = begin
fe247f476ecb Migrate systemT from atton/agda/systemT (13:5a81867278af)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
115 S (S n) * S m
fe247f476ecb Migrate systemT from atton/agda/systemT (13:5a81867278af)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
116 ≡⟨ right-mult-distr-one (S (S n)) m ⟩
fe247f476ecb Migrate systemT from atton/agda/systemT (13:5a81867278af)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
117 (S (S n)) + ((S (S n)) * m)
fe247f476ecb Migrate systemT from atton/agda/systemT (13:5a81867278af)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
118 ≡⟨ cong (\x -> (S (S n)) + x) (left-mult-distr-one (S n) m) ⟩
fe247f476ecb Migrate systemT from atton/agda/systemT (13:5a81867278af)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
119 S (S n) + (m + S n * m)
fe247f476ecb Migrate systemT from atton/agda/systemT (13:5a81867278af)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
120 ≡⟨ cong (\x -> x + (m + S n * m)) (left-add-one (S n)) ⟩
fe247f476ecb Migrate systemT from atton/agda/systemT (13:5a81867278af)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
121 (S O) + (S n) + (m + S n * m)
fe247f476ecb Migrate systemT from atton/agda/systemT (13:5a81867278af)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
122 ≡⟨ sum-assoc ((S O) + (S n)) m (S n * m) ⟩
fe247f476ecb Migrate systemT from atton/agda/systemT (13:5a81867278af)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
123 (S O) + (S n) + m + S n * m
fe247f476ecb Migrate systemT from atton/agda/systemT (13:5a81867278af)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
124 ≡⟨ cong (\x -> x + m + S n * m) (sum-sym (S O) (S n)) ⟩
fe247f476ecb Migrate systemT from atton/agda/systemT (13:5a81867278af)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
125 ((((S n) + (S O)) + m) + S n * m)
fe247f476ecb Migrate systemT from atton/agda/systemT (13:5a81867278af)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
126 ≡⟨ cong (\x -> x + (S n * m)) (sym (sum-assoc (S n) (S O) m))⟩
fe247f476ecb Migrate systemT from atton/agda/systemT (13:5a81867278af)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
127 (((S n) + ((S O) + m)) + S n * m)
fe247f476ecb Migrate systemT from atton/agda/systemT (13:5a81867278af)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
128 ≡⟨ cong (\x -> (S n + x + S n * m)) (sym (left-add-one m)) ⟩
fe247f476ecb Migrate systemT from atton/agda/systemT (13:5a81867278af)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
129 ((S n) + (S m) + S n * m)
fe247f476ecb Migrate systemT from atton/agda/systemT (13:5a81867278af)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
130 ≡⟨ cong (\x -> x + (S n * m)) (sum-sym (S n) (S m)) ⟩
fe247f476ecb Migrate systemT from atton/agda/systemT (13:5a81867278af)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
131 (S m) + (S n) + (S n * m)
fe247f476ecb Migrate systemT from atton/agda/systemT (13:5a81867278af)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
132 ≡⟨ sym (sum-assoc (S m) (S n) (S n * m)) ⟩
fe247f476ecb Migrate systemT from atton/agda/systemT (13:5a81867278af)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
133 (S m) + ((S n) + ((S n) * m))
fe247f476ecb Migrate systemT from atton/agda/systemT (13:5a81867278af)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
134 ≡⟨ cong (\x -> (S m) + x ) (sym (right-mult-distr-one (S n) m )) ⟩
fe247f476ecb Migrate systemT from atton/agda/systemT (13:5a81867278af)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
135 S m + S n * S m
fe247f476ecb Migrate systemT from atton/agda/systemT (13:5a81867278af)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
136 ∎
fe247f476ecb Migrate systemT from atton/agda/systemT (13:5a81867278af)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
137
fe247f476ecb Migrate systemT from atton/agda/systemT (13:5a81867278af)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
138
fe247f476ecb Migrate systemT from atton/agda/systemT (13:5a81867278af)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
139 mult-sym : (n m : Int) -> n * m ≡ m * n
fe247f476ecb Migrate systemT from atton/agda/systemT (13:5a81867278af)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
140 mult-sym n O = begin
fe247f476ecb Migrate systemT from atton/agda/systemT (13:5a81867278af)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
141 n * O
fe247f476ecb Migrate systemT from atton/agda/systemT (13:5a81867278af)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
142 ≡⟨ refl ⟩
fe247f476ecb Migrate systemT from atton/agda/systemT (13:5a81867278af)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
143 O
fe247f476ecb Migrate systemT from atton/agda/systemT (13:5a81867278af)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
144 ≡⟨ sym (left-mult-zero n) ⟩
fe247f476ecb Migrate systemT from atton/agda/systemT (13:5a81867278af)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
145 O * n
fe247f476ecb Migrate systemT from atton/agda/systemT (13:5a81867278af)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
146 ∎
fe247f476ecb Migrate systemT from atton/agda/systemT (13:5a81867278af)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
147 mult-sym n (S m) = begin
fe247f476ecb Migrate systemT from atton/agda/systemT (13:5a81867278af)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
148 n * (S m)
fe247f476ecb Migrate systemT from atton/agda/systemT (13:5a81867278af)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
149 ≡⟨ right-mult-distr-one n m ⟩
fe247f476ecb Migrate systemT from atton/agda/systemT (13:5a81867278af)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
150 n + (n * m)
fe247f476ecb Migrate systemT from atton/agda/systemT (13:5a81867278af)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
151 ≡⟨ cong (\x -> n + x ) (mult-sym n m) ⟩
fe247f476ecb Migrate systemT from atton/agda/systemT (13:5a81867278af)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
152 n + (m * n)
fe247f476ecb Migrate systemT from atton/agda/systemT (13:5a81867278af)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
153 ≡⟨ sym (left-mult-distr-one m n) ⟩
fe247f476ecb Migrate systemT from atton/agda/systemT (13:5a81867278af)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
154 (S m) * n
fe247f476ecb Migrate systemT from atton/agda/systemT (13:5a81867278af)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
155 ∎