[Proved that ⊕ is associative.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20080501180110] move ./FixitiesOK.agda ./AlgebraicProperties.agda
hunk ./AlgebraicProperties.agda 2
--- The fixity declarations in Language are sensible
+-- Some algebraic properties
hunk ./AlgebraicProperties.agda 5
-module FixitiesOK where
+module AlgebraicProperties where
hunk ./AlgebraicProperties.agda 13
+open import Algebra
hunk ./AlgebraicProperties.agda 15
+open import Relation.Binary.PropositionalEquality
+open import Data.Nat.Properties using (ℕ-commutativeSemiring)
+
+------------------------------------------------------------------------
+-- A lemma
+
+cast : forall {n₁ n₂ x i} ->
+       n₁ ≡ n₂ -> x ⇓[ i ] val n₁ -> x ⇓[ i ] val n₂
+cast ≡-refl x = x
+
+------------------------------------------------------------------------
+-- Associativity
+
+-- These properties show that the fixity declarations make sense.
+
+-- _⊕_ is associative.
+
+⊕-assoc : Associative _⊕_
+⊕-assoc x y z = equal ⟶ ⟵
+  where
+  assoc = CommutativeSemiring.+-assoc ℕ-commutativeSemiring
+
+  ⟶ : (x ⊕ y) ⊕ z ⊑ x ⊕ (y ⊕ z)
+  ⟶ Int                 = Int
+  ⟶ (Add₃ (Add₁ x y) z) = Add₃ x (Add₃ y z)
+  ⟶ (Add₂ Int)          = Int
+  ⟶ (Add₂ (Add₃ x y))   = Add₃ x (Add₂ y)
+  ⟶ (Add₂ (Add₂ x))     = Add₂ x
+  ⟶ {i = i} (Add₁ {n = n₃} (Add₁ {m = n₁} {n = n₂} x⇓ y⇓) z⇓) =
+    cast (≡-sym (assoc n₁ n₂ n₃)) (Add₁ x⇓ (Add₁ y⇓ z⇓))
+
+  ⟵ : x ⊕ (y ⊕ z) ⊑ (x ⊕ y) ⊕ z
+  ⟵ Int                 = Int
+  ⟵ (Add₃ x Int)        = Int
+  ⟵ (Add₃ x (Add₂ y))   = Add₂ (Add₃ x y)
+  ⟵ (Add₃ x (Add₃ y z)) = Add₃ (Add₁ x y) z
+  ⟵ (Add₂ x)            = Add₂ (Add₂ x)
+  ⟵ {i = i} (Add₁ {m = n₁} x⇓ (Add₁ {m = n₂} {n = n₃} y⇓ z⇓)) =
+    cast (assoc n₁ n₂ n₃) (Add₁ (Add₁ x⇓ y⇓) z⇓)
hunk ./Everything.agda 10
-import FixitiesOK
+import AlgebraicProperties