Mercurial > hg > Members > atton > agda > systemT

annotate int.agda @ 8:e191792472f8

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