A collection of proof exercises about integers I created and solved for fun.

IntExercise.agda

{- Given the defintion of the natural numbers ℕ from the standard library ... -}

open import Level using () renaming (zero to ℓ₀)
open import Data.Nat using (ℕ) renaming (_+_ to _+ℕ_; suc to nsuc; zero to nzero)
import Relation.Binary as B
import Relation.Binary.Core as B
import Relation.Binary.PropositionalEquality as P
open import Function using (flip)
open P using (_≡_)

{- ... and given the following statements about operations on them ... -}

npred : ℕ → ℕ
npred nzero = nzero
npred (nsuc n) = n

postulate +ℕ-assoc : ∀ m n o → (m +ℕ n) +ℕ o ≡ m +ℕ (n +ℕ o)

postulate +ℕ-right-identity : ∀ n → n +ℕ nzero ≡ n

postulate +ℕ-suc : ∀ m n → m +ℕ nsuc n ≡ nsuc (m +ℕ n)

postulate +ℕ-comm : ∀ m n → m +ℕ n ≡ n +ℕ m

postulate +ℕ-add-injective : ∀ k m n → m +ℕ k ≡ n +ℕ k → m ≡ n

{- ... use this data type representing the set of integers ℤ by pairs of natural numbers and ... -}

data ℤ : Set where
  I : ℕ → ℕ → ℤ

{- ... 1. implement these operations on ℤ and... -}

embedℕ : ℕ → ℤ
embedℕ n = {!!}

zero : ℤ
zero = {!!}

suc : ℤ -> ℤ
suc z = {!!}

pred : ℤ -> ℤ
pred z = {!!}

infixl 6 _+_
_+_ : ℤ → ℤ → ℤ
a + b = {!!}

-_ : ℤ → ℤ
- a = {!!}

infix 4 _≈_
_≈_ : ℤ → ℤ → Set
a ≈ b = {!!}

{- ... 2. prove these statements about operations on ℤ -}

refl-≈ : ∀{i} → i ≈ i
refl-≈ {i} = {!!}

sym-≈ : ∀{i j} → i ≈ j → j ≈ i
sym-≈ {i} {j} p = {!!}

trans-≈ : ∀{i j k} → i ≈ j → j ≈ k → i ≈ k
trans-≈ {i} {j} {k} p q = {!!}

≡-to-≈ : ∀ m n → m ≡ n → m ≈ n
≡-to-≈ a b eq = {!!}

ℤ≈ : B.Setoid ℓ₀ ℓ₀
ℤ≈ = record { Carrier = ℤ ; _≈_ = _≈_ ; isEquivalence = record { refl = refl-≈ ; sym = sym-≈ ; trans = trans-≈ } }

+-assoc : ∀ m n o → (m + n) + o ≈ m + (n + o)
+-assoc m n o = {!!}

suc-pred-identity : ∀ n → suc (pred n) ≈ n
suc-pred-identity n = {!!}

+-right-identity : ∀ n → n + zero ≈ n
+-right-identity n = {!!}

+-suc : ∀ m n → m + suc n ≈ suc (m + n)
+-suc a b = {!!}

+-comm : ∀ m n → m + n ≈ n + m
+-comm a b = {!!}

+-right-inverse : ∀ n → n + (- n) ≈ zero
+-right-inverse n = {!!}

+-add-injective : ∀ k m n → m + k ≈ n + k → m ≈ n
+-add-injective k m n = {!!}

{- Good Luck! -}