# Exercises

## Exercise 1

Complete a proof score of the commutativity of `+`

in `NAT+`

.

## Exercise 2

After finishing the proofs of the associativity and the commutativity of `+`

, those properties can be declared by adding to the attribute `assoc comm`

to `+`

. Consider the following modules:

mod! NAT+AC {
pr(NAT+)
op _+_ : Nat Nat -> Nat { assoc comm }
}
mod! NAT* {
pr(NAT+AC)
op _*_ : Nat Nat -> Nat
eq 0 * M:Nat = 0 .
eq s(N:Nat) * M:Nat = M + (N * M) .
}

Prove the distributive law, that is, `i * (j + k) = (i * j) + (i * k)`

in `NAT*`

.

## Exercise 3

Consider why `NAT+AC`

does not include equations of the associative and the commutative laws instead of the attributes. What kinds of trouble happen in the following module?

mod! NAT+AC2 {
pr(NAT+)
-- associativity on _+_
eq (I:Nat + J:Nat) + K:Nat = I + (J + K) .
-- commutativity on _+_
eq I:Nat + J:Nat = J + I .
}

[Next]

Original Copyright © Takahiro Seino, all rights reserved.