open import Equality

-- In Emacs Agda mode, type "\bN" to get the symbol ℕ.

data ℕ : Set where
  zero : ℕ
  succ : ℕ -> ℕ

{-# BUILTIN NATURAL ℕ #-}

add : ℕ -> ℕ -> ℕ
add zero y = y
add (succ x) y = succ (add x y)

-- C-c C-c: automatically do a case split on a variable

lemma-add-m-zero : ∀ (m : ℕ) -> m == add m zero
lemma-add-m-zero zero = refl
lemma-add-m-zero (succ m) = context succ ind-hyp
  where
    ind-hyp : m == add m zero
    ind-hyp = lemma-add-m-zero m

lemma-add-m-succ : ∀ (m n : ℕ) -> succ (add m n) == add m (succ n)
lemma-add-m-succ zero n = refl
lemma-add-m-succ (succ m) n = context succ (lemma-add-m-succ m n)

lemma-add-commutative : ∀ (n : ℕ) -> ∀ (m : ℕ) -> add n m == add m n
lemma-add-commutative zero m = lemma-add-m-zero m
lemma-add-commutative (succ n) m =
  equational succ (add n m)
          by context succ (lemma-add-commutative n m)
      equals succ (add m n)
          by lemma-add-m-succ m n
      equals add m (succ n)

    -- Pencil-and-paper proof:
    -- succ (add n m) == succ (add m n)   (by induction hypothesis)
    --                == add m (succ n)   (maybe this needs a lemma?)

-- "context" takes a function f and a proof of x == y and produces a
-- proof of f x == f y

-- ----------------------------------------------------------------------
-- Ways of putting comments into an Agda file:

-- Agda:
-- -- one-line comment
-- {- block comment -}

-- Java:
-- // one-line comment
-- /* block comment */

-- ----------------------------------------------------------------------
-- The following notations are equivalent:
-- 
-- ∀ (n : ℕ) -> ∀ (m : ℕ) -> add n m == add m n
-- 
-- (n : ℕ) -> (m : ℕ) -> add n m == add m n
--
-- ∀ (n m : ℕ) -> add n m == add m n
--
-- (n m : ℕ) -> add n m == add m n
--
-- ∀ n m -> add n m == add m n
--
-- BUT THIS DOES NOT WORK:
-- n m -> add n m == add m n

-- ----------------------------------------------------------------------
-- want to show that 2+5 == 5+2

claim : ∀ x -> add x 5 == add 5 x
claim x = lemma-add-commutative _ _

claim2 : ∀ x y -> add x y == add y x
claim2 x y = lemma-add-commutative x {!!}

-- add ?0 x = add y x
-- add x ?0 = add x y

-- ----------------------------------------------------------------------
-- Identifiers, infix notation

-- Identifiers are e.g. "variables" such as x, y, z.

datax : ℕ
datax = 5

-- In most programming languages, identifiers can only use very
-- limited symbols, like lower-case letters, digits, underscores, and
-- sometimes upper-case letters, but identifiers typically have to
-- start with a lower-case letter.
--
-- x, x1, camelCase, this_is_an_identifier
--
-- In Agda, almost *any* sequence of symbols can be used as an
-- identifier.

%^&* : ℕ
%^&* = 5

x+y : ℕ -> ℕ -> ℕ
x+y x y = {!!}

claim3 : ∀ (x y : ℕ) -> add x y == add x y
claim3 x y = refl

-- Exceptions: the following characters cannot be used in identifiers:
-- '(', ')', '{', '}', '\', '@'. There might be some additional
-- exceptions as well.

-- ----------------------------------------------------------------------
-- Infix notation

-- The underscore '_' can be used as part of the name of an
-- identifier, just like any other symbol. However, it has a slightly
-- special meaning.

_+_ : ℕ -> ℕ -> ℕ
_+_ zero y = y
_+_ (succ x) y = succ (_+_ x y)

-- If an identifier contains the '_' character, it creates an infix
-- notation.
--
-- Then we can write
--
-- _+_ 2 5
--
-- or
--
-- 2 + 5
--
-- interchangably.

-- Another example
data Bool : Set where
  true : Bool
  false : Bool

if_then_else_ : Bool -> ℕ -> ℕ -> ℕ
if_then_else_ true x y = x
if_then_else_ false x y = y

_! : ℕ -> ℕ
n ! = {!!}

fac : ℕ -> ℕ
fac n = {!!}

-- Now we can write
--
-- if true then 5 else 7
--
-- instead of
--
-- if_then_else_ true 5 7

<_||_> : ℕ -> ℕ -> ℕ
<_||_> x y = x

-- ----------------------------------------------------------------------
-- Precedence

_*_ : ℕ -> ℕ -> ℕ
_*_ x y = {!!}

n : ℕ
n = 1 + (2 * 4)