computer engineer • phd candidate • real life person
A Duad will be represented as a pair of integers.
Duad : Set
Duad = ℤ × ℤ
We can define addition, subtraction, multiplication, and division:
module Operations where
-- Addition
_⊕_ : Duad → Duad → Duad
(a , b) ⊕ (c , d) = a * d + b * c , b * d
-- Multiplication
_×_ : Duad → Duad → Duad
(a , b) × (c , d) = a * c , b * d
-- Subtraction
_⊝_ : Duad → Duad → Duad
(a , b) ⊝ (c , d) = a * d - b * c , b * d
-- Division
_÷_ : Duad → Duad → Duad
(a , b) ÷ (c , d) = a * d , b * c
We refer to the first and second component of a Duad as height and length, respectively. And, we can scale a duad by an integer:
-- Height
h : Duad → ℤ
h (a , b) = b
-- Length
l : Duad → ℤ
l (a , b) = a
-- Scaling
scale-by : ℤ → Duad → Duad
scale-by r (a , b) = r * a , r * b
To show that two duads are equal, it is sufficient to show that their first components are equal and their second components are equal:
mk-≡ : ∀ {a b c d : ℤ} → a ≡ c → b ≡ d → (a , b) ≡ (c , d)
mk-≡ = ≡.cong₂ _,_
Addition of Duads is commutative.
For duads
(a , b)
and
(c , d)
,
we first expand out the definitions of
_⊕_
, giving
(a , b) ⊕ (c , d) = a * d + b * c , b * d
, and
(c , d) ⊕ (a , b) = c * b + d * a , d * b
.
Showing equality amounts to
a proof that
a * d + b * c ≡ c * b + d * a
and a proof that
b * d ≡ d * b
.
⊕-comm : ∀ p q → p ⊕ q ≡ q ⊕ p
⊕-comm (a , b) (c , d) = mk-≡ ad+bc≡cb+da bd≡db
We show that the heights are equal using commutativity of integer multiplication and commutativity of integer addition:
ad+bc≡cb+da : a * d + b * c ≡ c * b + d * a
ad+bc≡cb+da = begin
a * d + b * c ≡⟨ ≡.cong₂ _+_ (*-comm a d) (*-comm b c) ⟩
d * a + c * b ≡⟨ +-comm (d * a) (c * b) ⟩
c * b + d * a ∎
That the lengths are equal follows directly from commutativity of integer multiplication:
bd≡db : b * d ≡ d * b
bd≡db = *-comm b d