Mercurial > hg > Members > atton > agda > systemT
view int.agda @ 3:7138e79615b3
Proof add-sym
author | Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> |
---|---|
date | Wed, 21 May 2014 14:41:45 +0900 |
parents | |
children | 6b1230883bfa |
line wrap: on
line source
open import systemT open import Relation.Binary.PropositionalEquality open ≡-Reasoning module int where _+_ : Int -> Int -> Int n + O = n n + (S m) = S (n + m) plus-one : (n m : Int) -> (S n) + m ≡ S (n + m) plus-one n O = sym refl plus-one n (S m) = cong S (plus-one n m) double : Int -> Int double O = O double (S n) = S (S (double n)) sum-sym : (n : Int) (m : Int) -> n + m ≡ m + n sum-sym O O = refl sum-sym O (S m) = cong S (sum-sym O m) sum-sym (S n) O = cong S (sum-sym n O) sum-sym (S n) (S m) = begin (S n) + (S m) ≡⟨ refl ⟩ S ((S n) + m) ≡⟨ cong S (plus-one n m)⟩ S (S (n + m)) ≡⟨ cong (\x -> S (S x)) (sum-sym n m) ⟩ S (S (m + n)) ≡⟨ sym (cong S (plus-one m n)) ⟩ S ((S m) + n) ≡⟨ refl ⟩ (S m) + (S n) ∎