agda-arithmetic/basicarithmetic.agda at main · haoming-li-ling/agda-arithmetic · GitHub

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; refl; cong; sym)
open Eq.≡-Reasoning using (begin_; _≡⟨⟩_; step-≡; _∎)

data ℕ : Set where
  zero : ℕ
  suc  : ℕ → ℕ

-- + (Addition)
_+_ : ℕ → ℕ → ℕ
zero + n = n
(suc m) + n = suc (m + n)

-- Addition: Right Identity Zero
+-identityʳ : ∀ (m : ℕ) → m + zero ≡ m
+-identityʳ zero =
  begin
    zero + zero
  ≡⟨⟩
    zero
  ∎
+-identityʳ (suc x) =
  begin
    suc x + zero
  ≡⟨⟩
    suc (x + zero)
  ≡⟨ cong suc (+-identityʳ x) ⟩
    suc x
  ∎

-- Addition: Preposition of Suc
+-suc : ∀ (m n : ℕ) → m + suc n ≡ suc (m + n)
+-suc zero n =
  begin
   zero + suc n
 ≡⟨⟩
   suc n
 ≡⟨⟩
   suc (zero + n)
 ∎
+-suc (suc m) n =
  begin
    suc m + suc n
  ≡⟨⟩
    suc (m + suc n)
  ≡⟨ cong suc (+-suc m n) ⟩
    suc (suc (m + n))
  ≡⟨⟩
    suc (suc m + n)
  ∎

-- * (Multiplication)
_*_ : ℕ → ℕ → ℕ
zero * n = zero
(suc m) * n  = n + (m * n)

-- Multiplication: Right Identity Zero
*-identityʳ : ∀ (n : ℕ) → zero * n ≡ zero
*-identityʳ zero =
  begin
    zero * zero
  ≡⟨⟩
    zero
  ∎
*-identityʳ (suc x) =
  begin
    zero * suc x
  ≡⟨⟩
    zero
  ∎

-- Multiplication: Preposition of Suc
*-suc : ∀ (m n : ℕ) → (suc m) * n ≡ n + (m * n)
*-suc zero n rewrite *-identityʳ n = refl
*-suc (suc m) n rewrite *-suc m n = refl