-- A comment looks like this.

module 1-agda-demo where

-- Every agda file has to start with the above line `module [x] where` where `[x]` is the filename.

-- We define inductive types (GADTS) in the following way.

data Bool : Set where
  true : Bool
  false : Bool

-- Compare with the Haskell GADT syntax (only the `:`s are different and we wouldn't put `: Set`).

not : Bool → Bool
not true = false
not false = true

-- Define `not` by the following.
-- 1. Type `not b = ?`
-- 2. Type C-c C-l (`load`), and the question mark turns into a hole. 
-- 3. Put your cursor in the hole, and type C-y C-. or C-c C-. (Goal and hypotheses)
-- 4. Type C-c C-c (`case`) then `b` to do pattern matching.
-- 5. You can put your cursor in the first hole and do 3 again.
-- 6. Type the "answer" in the first hole and then C-c C-space (`give`)
-- 7. Do the same for the second hole.

if_then_else_ : Bool → Bool → Bool → Bool
if true then b else _ = b
if _ then _ else c = c

-- Notice how infix notation is defined.
-- You can use `_` as in Haskell.

id : {A : Set} → A → A
id = λ x → x

-- When the goal type has one constructor (as is the case for `A → A`, you can use C-c C-r (refine)).
-- You can also try C-c C-a (auto for this one).

exampleId : Bool → Bool
exampleId = id

data ℕ : Set where
  zero : ℕ
  succ : ℕ → ℕ

{-# BUILTIN NATURAL ℕ #-}

-- This is a /pragma/, that identifies the ℕ that we just defined with the built in naturals. This improves performance, but also gives us the usual names for the natural numbers.

isZero : ℕ → Bool
isZero 0 = true
isZero _ = false

_+_ : ℕ → ℕ → ℕ
zero + m = m
succ n + m = succ (n + m)

equalNat : ℕ -> ℕ -> Bool
equalNat zero zero = true
equalNat zero (succ m) = false
equalNat (succ n) zero = false
equalNat (succ n) (succ m) = equalNat n m

-- You can compute the values by using C-c C-n (`compute normal form`)
-- Compute the normal form of equalNat (1 + 2) 3

data EqualNat : ℕ -> ℕ -> Set where
  equalZero : EqualNat zero zero
  equalSucc : {n m : ℕ} → EqualNat n m → EqualNat (succ n) (succ m)

-- We can't compute the normal form anymore to figure out if 1 + 2 and 3 are equal. Instead we prove it.

testAddition : EqualNat (1 + 2) 3
testAddition = equalSucc (equalSucc (equalSucc equalZero))

EqualIsReflexive : (n : ℕ) → EqualNat n n
EqualIsReflexive zero = equalZero
EqualIsReflexive (succ n) = equalSucc (EqualIsReflexive n)

testAdditionAgain : EqualNat (1 + 2) 3
testAdditionAgain = EqualIsReflexive 3

EqualIsTransitive : {l m n : ℕ} → EqualNat l m → EqualNat m n → EqualNat l n
EqualIsTransitive {0} {0} {n} equalZero f = f
EqualIsTransitive {succ l} {succ m} {succ n} (equalSucc e) (equalSucc f) = equalSucc (EqualIsTransitive e f)

-- You can give inductive hypotheses names that appear in the hypotheses by using a let expression

EqualIsTransitive2 : {l m n : ℕ} → EqualNat l m → EqualNat m n → EqualNat l n
EqualIsTransitive2 {0} {0} {n} equalZero f = f
EqualIsTransitive2 {succ l} {succ m} {succ n} (equalSucc e) (equalSucc f) = 
  let ih = EqualIsTransitive2 {l} {m} {n} in equalSucc (ih e f)

EqualIsSymmetric : {m n : ℕ} → EqualNat m n → EqualNat n m
EqualIsSymmetric equalZero = equalZero
EqualIsSymmetric (equalSucc e) = equalSucc (EqualIsSymmetric e)

record EquivalenceRelations (A : Set) : Set₁ where
  field
    R : A → A → Set
    refl : (a : A) → R a a
    sym : {a b : A} → R a b → R b a
    trans : {a b c : A} → R a b → R b c → R a c

EqualNatInstance : EquivalenceRelations ℕ
EqualNatInstance = record { R = EqualNat ; refl = EqualIsReflexive ; sym = EqualIsSymmetric ; trans = EqualIsTransitive}