Mercurial > hg > Members > atton > agda > systemT

comparison int.agda @ 13:5a81867278af default tip

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Imporve proof for sum-sym
author Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
date Fri, 23 May 2014 13:53:30 +0900
parents ce0c3af2c34e
children
comparison
equal deleted inserted replaced
12:ce0c3af2c34e 13:5a81867278af
24 24
25 left-increment : (n m : Int) -> (S n) + m ≡ S (n + m) 25 left-increment : (n m : Int) -> (S n) + m ≡ S (n + m)
26 left-increment n O = refl 26 left-increment n O = refl
27 left-increment n (S m) = cong S (left-increment n m) 27 left-increment n (S m) = cong S (left-increment n m)
28 28
29 sum-sym : (n : Int) (m : Int) -> n + m ≡ m + n 29 sum-sym : (x : Int) (y : Int) -> x + y ≡ y + x
30 sum-sym O O = refl 30 sum-sym O O = refl
31 sum-sym O (S m) = cong S (sum-sym O m) 31 sum-sym O (S y) = cong S (sum-sym O y)
32 sum-sym (S n) O = cong S (sum-sym n O) 32 sum-sym (S x) O = cong S (sum-sym x O)
33 sum-sym (S n) (S m) = begin 33 sum-sym (S x) (S y) = begin
34 (S n) + (S m) 34 (S x) + (S y)
35 ≡⟨ refl ⟩ 35 ≡⟨ refl ⟩
36 S ((S n) + m) 36 S ((S x) + y)
37 ≡⟨ cong S (left-increment n m)⟩ 37 ≡⟨ cong S (sum-sym (S x) y) ⟩
38 S (S (n + m)) 38 S (y + (S x))
39 ≡⟨ cong (\x -> S (S x)) (sum-sym n m) ⟩ 39 ≡⟨ (sym (left-increment y (S x))) ⟩
40 S (S (m + n)) 40 (S y) + (S x)
41 ≡⟨ sym (cong S (left-increment m n)) ⟩
42 S ((S m) + n)
43 ≡⟨ refl ⟩
44 (S m) + (S n)
45 ∎ 41 ∎
46 42
47 sum-assoc : (x y z : Int) -> x + (y + z) ≡ (x + y) + z 43 sum-assoc : (x y z : Int) -> x + (y + z) ≡ (x + y) + z
48 sum-assoc O O O = refl 44 sum-assoc O O O = refl
49 sum-assoc O O (S z) = cong S (sum-assoc O O z) 45 sum-assoc O O (S z) = cong S (sum-assoc O O z)