wenkokke/lecture1.agda

## lecture1.agda
{-(- by Wen Kokke, borrowing heavily from CS410-17 lecture 1 by Conor McBride -)-}

module lecture1 where

module sum-and-product-types where

{--------------------------------------------------------------------------------}
-- so Coq and Agda are kinda the same, yet very different

-- * it's said Coq looks like ML and Agda looks like Haskell
--   (I don't really know ML, but I know Haskell, so for me...)

  data Bool : Set where
    true  : Bool
    false : Bool

{-+}
  not : Bool → Bool
  not b = ?
{+-}

-- * bad news? Agda doesn't really have tactics...
--   (it forces you wrote write programs by hand)
--   (but it doesn't force you to learn magic, i.e. Ltac)

-- * good news? Agda has a lot fewer quirks than Coq...
--   (overall, I'd say it is a lot easier to get what is going on in Agda)

-- * this is as good a time as any to bring up Unicode


{--------------------------------------------------------------------------------}
-- so how about we write some Agda?

  data 𝟎 : Set where -- we input 𝟎 as \B0
    -- we can _only_ construct values of a datatype using its constructors.
    -- there are _no_ constructors for the empty type, so there are no values.

{-+}
  nope : {A : Set} → 𝟎 → A -- should probably talk about those braces {_}
  nope e = ?
{+-}

  record 𝟏 : Set where -- we input 𝟏 as \B1
    -- we can construct instances of record types by giving values for all their
    -- fields. I'd put an empty "field" section here but Agda's parser doesn't
    -- like those. anyway, there aren't any fields, so:

  unit : 𝟏
  unit = record {}

  you-figure-it-out : 𝟏 -- honestly, this is a pretty easy request
  you-figure-it-out = _


{--------------------------------------------------------------------------------}
-- so we've got 𝟎 and 𝟏, what about + and ×?

  data _+_ (A B : Set) : Set where
    inl : A → A + B
    inr : B → A + B

-- you should tell them what do those underscores mean

  Π : (A : Set) (B : A → Set) → Set
  Π A B = (x : A) → B x

  record Σ (A : Set) (B : A → Set) : Set where
    constructor _,_
    field
      fst : A
      snd : B fst
  open Σ public -- bring `_,_`, `fst`, and `snd` into scope and export them

-- what does that have to do with _×_?

  _×_ : (A B : Set) → Set -- we input × as \x
  A × B = Σ A λ _ → B -- this lambda looks funky, maybe talk about it


{--------------------------------------------------------------------------------}
-- why do you insist on calling these 𝟎, 𝟏, _+_, and _×_?!

  infix 10 _↔_ -- we input ↔ as \<->

  _↔_ : (A B : Set) → Set
  A ↔ B = (A → B) × (B → A)

{-+} -- maybe talk about that ∀ and those {_}?
  ×-comm : ∀ {A B} → A × B → B × A -- we input ∀ as \all
  ×-comm = ?
{+-}

{-+}
  ×-assLR : ∀ {A B C} → A × (B × C) → (A × B) × C
  ×-assLR = ?
{+-}

{-+}
  ×-idR : ∀ {A} → A ↔ A × 𝟏
  ×-idR = ?
{+-}


{--------------------------------------------------------------------------------}
-- why do you insist on calling these 𝟎, 𝟏, _+_, and _×_?!

{-+}
  +-comm : ∀ {A B} → A + B → B + A
  +-comm = {!!}
{+-}

{-+}
  +-assLR : ∀ {A B C} → (A + B) + C → A + (B + C)
  +-assLR = {!!}
{+-}

{-+}
  +-idR : ∀ {A} → A + 𝟎 → A
  +-idR = {!!}
{+-}

{-+}
  ×+-dist : ∀ {A B C} → A × (B + C) → (A × B) + (A × C)
  ×+-dist = ?
{+-}


{-+----------------------------------------------------------------------------+-}

module naturals where

  open sum-and-product-types using (_↔_; _,_; 𝟎; 𝟏; unit)

{--------------------------------------------------------------------------------}
-- OK, we're convinced, but can't we just have normal + and × instead?
-- (no, not really, because I've used those identifiers already)

  data ℕ : Set where -- we input ℕ as \bN
    zero : ℕ
    suc  : ℕ → ℕ

  {-# BUILTIN NATURAL ℕ #-} -- means we can write 0, 1, 2, etc.

  _+_ : ℕ → ℕ → ℕ
  zero  + y = y
  suc x + y = suc (x + y)

  ex1 : ℕ
  ex1 = 4 + 5

-- but how do we write equalities? _↔_ won't really cut it for ℕ...

  ex2 : ℕ ↔ ℕ
  ex2 = (λ x → x) , (λ _ → 4)


-- here be lies that I've hidden from you:
-- we can tell Agda about _+_ so that it can optimize it better

  {-# BUILTIN NATPLUS _+_ #-}

{--------------------------------------------------------------------------------}
-- right, so how do we build equalities?
-- (Coq kinda hides this definition from you, but it's there as well)

  infix 10 _≡_

  data _≡_ {A : Set} : A → A → Set where
    refl : ∀ {x} → x ≡ x

{-+} -- make sure you write this using a dot pattern
  sym : ∀ {A} {x y : A} → x ≡ y → y ≡ x
  sym p = ?
{+-}

{-+}
  trans : ∀ {A} {x y z : A} → x ≡ y → y ≡ z → x ≡ z
  trans p q = ?
{+-}

{-+}
  cong : ∀ {A B} {x y} (f : A → B) → x ≡ y → f x ≡ f y
  cong f p = ?
{+-}


{-+----------------------------------------------------------------------------+-}

-- here be lies that I've hidden from you:
-- we can tell Agda about our equality so we can use it with 'rewrite'

  {-# BUILTIN EQUALITY _≡_ #-}

{--------------------------------------------------------------------------------}
-- right, so how do we build equalities? let's do some proofs!

{-+}
  +-idR : ∀ x → x ≡ x + 0
  +-idR x = ?
{+-}

{-+}
  +-suc : ∀ x y → 1 + (x + y) ≡ x + (1 + y)
  +-suc x y = ?
{+-}

{-+}
  +-comm : ∀ x y → x + y ≡ y + x
  +-comm x y = ?
{+-}

{-+}
  +-assLR : ∀ x y z → x + (y + z) ≡ (x + y) + z
  +-assLR x y z = ?
{+-}


{--------------------------------------------------------------------------------}
-- if you want to do this, you're free to -- but I'm not gonna

  _*_ : ℕ → ℕ → ℕ
  zero  * y = 0
  suc x * y = y + (x * y)

{-+}
  *-idR : ∀ x → x ≡ x * 0
  *-idR x = ?
{+-}

{-+}
  *-suc : ∀ x y → 1 * (x * y) ≡ x * (1 * y)
  *-suc x y = ?
{+-}

{-+}
  *-comm : ∀ x y → x * y ≡ y * x
  *-comm x y = ?
{+-}

{-+}
  *-assLR : ∀ x y z → x * (y * z) ≡ (x * y) * z
  *-assLR x y z = ?
{+-}

{-+}
  *+-dist : ∀ x y z → x * (y + z) → (x * y) + (x * z)
  *+-dist x y z = ?
{+-}


{-+----------------------------------------------------------------------------+-}

-- here be lies that I've hidden from you:
-- we can tell Agda about _+_ so that it can optimize it better

  {-# BUILTIN NATTIMES _*_ #-}

{--------------------------------------------------------------------------------}
-- but what if the proofs get really large? I don't wanna work that hard!

  data _≤_ : ℕ → ℕ → Set where -- we input ≤ as \<= or \le
    refl : ∀ {x} → 0 ≤ x
    step : ∀ {x y} → x ≤ y → suc x ≤ suc y

  ex3 : 4 ≤ 5
  ex3 = step (step (step (step refl)))

  -- this looks like it's going to be a problem...

  _≤?_ : ℕ → ℕ → Set
  zero  ≤? y     = 𝟏 -- that's the unit type
  suc x ≤? zero  = 𝟎 -- that's the empty type
  suc x ≤? suc y = x ≤? y

{-+}
  prove : ∀ x y → x ≤? y → x ≤ y
  prove x y p = ?
{+-}

{-+}
  ex4 : 112 ≤ 482
  ex4 = ?
{+-}

## lecture2.agda
{-# OPTIONS --type-in-type #-} -- minor cheats follow
module lecture2 where

open import Agda.Builtin.FromNat using (Number)
open import Data.Bool using (Bool; true; false; _∧_; if_then_else_)
open import Data.Empty using () renaming (⊥ to 𝟎)
open import Data.Maybe using (Maybe; just; nothing)
open import Data.Nat using (ℕ; suc; zero; _≤?_)
open import Data.Product using (_×_; _,_) renaming (proj₁ to fst; proj₂ to snd)
open import Data.Unit using (tt) renaming (⊤ to 𝟏)
open import Function as F using (case_of_)
open import Relation.Nullary.Decidable using (True; toWitness)
open import Relation.Binary.PropositionalEquality using (_≡_; _≢_; refl; cong₂)

-- here be cheats: in order to overload natural number notation,
-- we need to specify how it works for naturals... which is easy

instance
  NatNumber : Number ℕ
  NatNumber = record
    { Constraint = F.const 𝟏
    ; fromNat    = λ n → n
    }

∧-split : ∀ {b₁ b₂} → b₁ ∧ b₂ ≡ true → b₁ ≡ true × b₂ ≡ true
∧-split {false} {_}     ()
∧-split {true}  {false} ()
∧-split {true}  {true}  _ = (refl , refl)

module coq-style-1 where

{-------------------------------------------------------------------------}
  -- we're gonna talk about the simply-typed lambda calculus
  -- let's have some types, and a function to compare types, ok?

  data Type : Set where
    ⋆   : Type {- *mumble* we don't really care what our atomic type is -}
    _⇒_ : Type → Type → Type

  -- and something to check when types are equal

  _==_ : Type → Type → Bool
  ⋆       == ⋆       = true
  ⋆       == (C ⇒ D) = false
  (A ⇒ B) == ⋆       = false
  (A ⇒ B) == (C ⇒ D) = A == C ∧ B == D

  -- in coq, you'd use this function and then prove

  ==⟶≡ : ∀ A B → A == B ≡ true → A ≡ B
  ==⟶≡ ⋆         ⋆         p = refl
  ==⟶≡ ⋆         (B₁ ⇒ B₂) ()
  ==⟶≡ (A₁ ⇒ A₂) ⋆         ()
  ==⟶≡ (A₁ ⇒ A₂) (B₁ ⇒ B₂) p =
    -- ∧-split : ∀{b₁ b₂} → b₁ ∧ b₂ ≡ true → b₁ ≡ true × b₂ ≡ true
    case ∧-split p of λ{
      (p₁ , p₂) → cong₂ _⇒_ (==⟶≡ A₁ B₁ p₁) (==⟶≡ A₂ B₂ p₂) }

  -- and that way, you'd know your boolean function wasn't doing
  -- something incredibly stupid...
  -- like mine was, just now when I wrote these slides...

  -- anyway, anyone notice anything similar between _==_ and ==⟶≡?


module agda-style-1 where

  open coq-style-1 public using (Type; ⋆; _⇒_)


{-------------------------------------------------------------------------}
  -- hah, I tricked all of you!
  -- this lecture is about cultural differences between agda and coq...

  -- this is how you encode negation, "if you give me something of
  -- that type, I'll give you something which lives in the empty type"

  ¬_ : Set → Set
  ¬ P = P → 𝟎

  data Dec (P : Set) : Set where
    yes : ( p :   P) → Dec P
    no  : (¬p : ¬ P) → Dec P

  -- watch out, when we start writing this function, some scary things
  -- will start appearing -- keep in mind what it's all about:
  --
  --   a pattern match reveals information,
  --   and we don't want to just callously throw that away

  {-+}
  _≟_ : (A B : Type) → Dec (A ≡ B)
  A ≟ B = ?
  {+-}

  -- right, so we can _actually_ compare types now


module coq-style-2 where

  open coq-style-1 public using (Type; ⋆; _⇒_)
  open import Agda.Builtin.Nat using (_==_)


{-------------------------------------------------------------------------}
  -- I didn't lie, we're going to talk about the lambda calculus

  Id : Set
  Id = ℕ

  infixr 10 λ[_∶_]_
  infixl 20 _∙_

  data Term : Set where
    # : Id → Term
    λ[_∶_]_ : Id → Type → Term → Term
    _∙_ : Term → Term → Term

  -- let's look at some sample programs

  I = λ[ 0 ∶ ⋆ ] # 0
  K = λ[ 0 ∶ ⋆ ] λ[ 1 ∶ ⋆ ] # 0
  W = λ[ 0 ∶ ⋆ ] # 5

  -- right, we also need junk like substitution, reductions, etc...
  -- let's ignore that -- we don't have forever -- let's look at typing


{-------------------------------------------------------------------------}
  -- if we wanna look at typing, though, we have to basically redo
  -- the Maps stuff from the homework

  Ctxt : Set
  Ctxt = Id → Maybe Type

  ∅ : Ctxt
  ∅ = λ _ → nothing

  _,_∶_ : Ctxt → Id → Type → Ctxt
  (Γ , x ∶ A) y =
    -- warning, cheats: that _==_ has type ℕ → ℕ → Bool
    if x == y then just A else Γ y

  _∶_∈_ : Id → Type → Ctxt → Set
  x ∶ A ∈ Γ = Γ x ≡ just A

  -- fine, that looks about right, we can worry about theorems later

  -- by which I mean not at all


  infix 15 _,_∶_ _∶_∈_
  infix 5 _⊢_∶_ _⊢_

{-------------------------------------------------------------------------}
  -- now, TYPING!

  data _⊢_∶_ (Γ : Ctxt) : Term → Type → Set where

    Ax  : ∀ {x A} →

      x ∶ A ∈ Γ →
      ----------- (Ax)
      Γ ⊢ # x ∶ A

    ⇒I : ∀ {x N A B} →

      Γ , x ∶ A ⊢ N ∶ B →
      ------------------------ (⇒I)
      Γ ⊢ λ[ x ∶ A ] N ∶ A ⇒ B

    ⇒E : ∀ {L M A B} →

      Γ ⊢ L ∶ A ⇒ B → Γ ⊢ M ∶ A →
      -------------------------- (⇒E)
      Γ ⊢ L ∙ M ∶ B

  -- this predicate is actually doing two things at the same time
  -- let's make that a little bit clearer


{-------------------------------------------------------------------------}
  -- this predicate is actually doing two things at the same time
  -- let's make that a little bit clearer

  -- let's remove as much of the type clutter as we can... easily

  _∈_ : Id → Ctxt → Set
  x ∈ Γ = Γ x ≢ nothing

  data _⊢_ (Γ : Ctxt) : Term → Set where

    Ax? : ∀ {x} →

      x ∈ Γ →
      ------- (Ax?)
      Γ ⊢ # x

    ⇒I? : ∀ {x N A} →

      Γ , x ∶ A ⊢ N →
      ---------------- (⇒I?)
      Γ ⊢ λ[ x ∶ A ] N

    ⇒E? : ∀ {L M} →

      Γ ⊢ L → Γ ⊢ M →
      --------------- (⇒E?)
      Γ ⊢ L ∙ M

  -- what predicate did we just encode? (albeit clumsily)


module agda-style-2 where

  open agda-style-1

{-------------------------------------------------------------------------}
  -- how can we clean up this predicate? what if we could prove that the
  -- type for variables had exactly n elements, and Γ provided a type for
  -- each of them?

  -- what does the type with exactly n elements look like?
  --
  --   * 0 lives in all types with at least 1 element
  --
  --   * if n lives in the type with m elements,
  --     then n + 1 lives in the type with m + 1 elements
  --

  data Fin : ℕ → Set where
    zero : {n : ℕ} → Fin (suc n)
    suc  : {n : ℕ} → Fin n → Fin (suc n)

  f3of6 : Fin 6
  f3of6 = suc (suc (suc (zero {n = 2})))

  f3of7 : Fin 7
  f3of7 = suc (suc (suc (zero {n = 3})))

  -- and now?


-- here be cheats: if we want to be able to use natural number
-- notation for finite types, then we better have some constraints
open import Data.Fin using (Fin; suc; zero; fromℕ≤)

instance
  FinNumber : ∀ {n} → Number (Fin n)
  FinNumber {n} = record
    { Constraint = λ{m → True (suc m ≤? n)}
    ; fromNat    = λ{m {{p}} → fromℕ≤ (toWitness p)}
    }

module agda-style-3 where

  open agda-style-1

{-------------------------------------------------------------------------}
  -- and now?
  -- we encode terms, with only a finite number of possibilities for vars

  data Term (n : ℕ) : Set where
    #     : Fin n → Term n
    λ[_]_ : Type → Term (suc n) → Term n
    _∙_   : Term n → Term n → Term n

  -- oh, I forgot to tell you, we can write 0, 1, 2... for Fin too,
  -- as long as agda can figure out the upper bound
  f5in7 : Fin 7
  f5in7 = 5 {- there is some secret magic involved, though -}

  -- anyway, this is the identity function
  I : Term 0
  I = λ[ ⋆ ] # 0
  --  ^        |
  --  \________/
  --
  --  ^^^^^^^^^^
  -- this is how binding works in de Bruijn notation

  -- once more
  K : Term 0
  K = λ[ ⋆ ] λ[ ⋆ ] # 1
  --  ^               |
  --  \_______________/

  -- this term still exists, but now mentions that it exists _in context_
  W : Term 1
  W = {- some stuff is expected here -} λ[ ⋆ ] # 1
  --                 ^                           |
  --                 \___________________________/
  --
  -- we wrote # 5 last time, but those were names, these are indices
  -- so the index # 1 is just as good as the name # 5 or # 1203
  -- the only point is that it should move out of scope


module agda-style-4 where

  open agda-style-1

{-------------------------------------------------------------------------}
  -- right, so now we have well-scoped terms...
  -- why not restrict it to well-scoped, well-typed terms?

  data Vec (A : Set) : ℕ → Set where
    []  : Vec A 0
    _∷_ : ∀ {n} (x : A) (xs : Vec A n) → Vec A (suc n)

  _‼_ : ∀ {n} {A} → Vec A n → Fin n → A
  (x ∷ _ ) ‼ zero  = x
  (_ ∷ xs) ‼ suc i = xs ‼ i

  Ctxt : ℕ → Set
  Ctxt n = Vec Type n

  data _⊢_ {n : ℕ} : Ctxt n → Type → Set where

    # : {Γ : Ctxt n} (x : Fin n) →

      ----------- (Ax)
      Γ ⊢ (Γ ‼ x)

    λ[_]_ : {Γ : Ctxt n} (A : Type) {B : Type} →

      A ∷ Γ ⊢ B →
      ----------- (⇒I)
      Γ ⊢ A ⇒ B

    _∙_ : {Γ : Ctxt n} {A B : Type} →

      Γ ⊢ A ⇒ B → Γ ⊢ A →
      ------------------- (⇒E)
      Γ ⊢ B

  -- now we cannot ever write ill-typed terms

  I : {A : Type} → [] ⊢ A ⇒ A
  I {A} = λ[ A ] # 0

  K : {A B : Type} → [] ⊢ A ⇒ (B ⇒ A)
  K {A} {B} = λ[ A ] λ[ B ] # 1


  infix 5 _⊢_

{-------------------------------------------------------------------------}
  -- is this fun? I don't know

  -- anyway, we (probably) don't have time to talk about reduction
  -- but what's the moral of the story?

  -- we have been systematically been pushing effort that we'd have
  -- to expend proving things into things that agda knows, simply
  -- because of the representation that we're using

  -- in that vein, one last trick, mock reduction:

  ⟦_⟧ : Type → Set
  ⟦ ⋆     ⟧ = ℕ -- why not?
  ⟦ A ⇒ B ⟧ = ⟦ A ⟧ → ⟦ B ⟧

  data Env⟦_⟧ : {n : ℕ} → Vec Type n → Set where
    []  : Env⟦ [] ⟧
    _∷_ : ∀ {n} {A : Type} {Γ : Vec Type n} →
          ⟦ A ⟧ → Env⟦ Γ ⟧ → Env⟦ A ∷ Γ ⟧

  lookup : ∀ {n} {Γ : Ctxt n} (x : Fin n) → Env⟦ Γ ⟧ → ⟦ Γ ‼ x ⟧
  lookup zero    (x ∷ _) = x
  lookup (suc i) (_ ∷ e) = lookup i e

  ⟪_⟫ : ∀ {n} {Γ : Ctxt n} {A : Type} →
        Γ ⊢ A → Env⟦ Γ ⟧ → ⟦ A ⟧
  ⟪ # x      ⟫ e = lookup x e
  ⟪ λ[ A ] M ⟫ e = λ x → ⟪ M ⟫ (x ∷ e)
  ⟪ M ∙ N    ⟫ e = ⟪ M ⟫ e (⟪ N ⟫ e)

  id : ℕ → ℕ
  id = ⟪ I ⟫ []

  test-id : id ≡ λ x → x
  test-id = refl

  const : ℕ → ℕ → ℕ
  const = ⟪ K ⟫ []

  test-const : const ≡ λ x y → x
  test-const = refl


-- -}
	{-(- by Wen Kokke, borrowing heavily from CS410-17 lecture 1 by Conor McBride -)-}

	module lecture1 where

	module sum-and-product-types where

	{--------------------------------------------------------------------------------}
	-- so Coq and Agda are kinda the same, yet very different

	-- * it's said Coq looks like ML and Agda looks like Haskell
	-- (I don't really know ML, but I know Haskell, so for me...)

	data Bool : Set where
	true : Bool
	false : Bool

	{-+}
	not : Bool → Bool
	not b = ?
	{+-}

	-- * bad news? Agda doesn't really have tactics...
	-- (it forces you wrote write programs by hand)
	-- (but it doesn't force you to learn magic, i.e. Ltac)

	-- * good news? Agda has a lot fewer quirks than Coq...
	-- (overall, I'd say it is a lot easier to get what is going on in Agda)

	-- * this is as good a time as any to bring up Unicode



	{--------------------------------------------------------------------------------}
	-- so how about we write some Agda?

	data 𝟎 : Set where -- we input 𝟎 as \B0
	-- we can _only_ construct values of a datatype using its constructors.
	-- there are _no_ constructors for the empty type, so there are no values.

	{-+}
	nope : {A : Set} → 𝟎 → A -- should probably talk about those braces {_}
	nope e = ?
	{+-}

	record 𝟏 : Set where -- we input 𝟏 as \B1
	-- we can construct instances of record types by giving values for all their
	-- fields. I'd put an empty "field" section here but Agda's parser doesn't
	-- like those. anyway, there aren't any fields, so:

	unit : 𝟏
	unit = record {}

	you-figure-it-out : 𝟏 -- honestly, this is a pretty easy request
	you-figure-it-out = _



	{--------------------------------------------------------------------------------}
	-- so we've got 𝟎 and 𝟏, what about + and ×?

	data _+_ (A B : Set) : Set where
	inl : A → A + B
	inr : B → A + B

	-- you should tell them what do those underscores mean

	Π : (A : Set) (B : A → Set) → Set
	Π A B = (x : A) → B x

	record Σ (A : Set) (B : A → Set) : Set where
	constructor _,_
	field
	fst : A
	snd : B fst
	open Σ public -- bring `_,_`, `fst`, and `snd` into scope and export them

	-- what does that have to do with _×_?

	_×_ : (A B : Set) → Set -- we input × as \x
	A × B = Σ A λ _ → B -- this lambda looks funky, maybe talk about it



	{--------------------------------------------------------------------------------}
	-- why do you insist on calling these 𝟎, 𝟏, _+_, and _×_?!

	infix 10 _↔_ -- we input ↔ as \<->

	_↔_ : (A B : Set) → Set
	A ↔ B = (A → B) × (B → A)

	{-+} -- maybe talk about that ∀ and those {_}?
	×-comm : ∀ {A B} → A × B → B × A -- we input ∀ as \all
	×-comm = ?
	{+-}

	{-+}
	×-assLR : ∀ {A B C} → A × (B × C) → (A × B) × C
	×-assLR = ?
	{+-}

	{-+}
	×-idR : ∀ {A} → A ↔ A × 𝟏
	×-idR = ?
	{+-}



	{--------------------------------------------------------------------------------}
	-- why do you insist on calling these 𝟎, 𝟏, _+_, and _×_?!

	{-+}
	+-comm : ∀ {A B} → A + B → B + A
	+-comm = {!!}
	{+-}

	{-+}
	+-assLR : ∀ {A B C} → (A + B) + C → A + (B + C)
	+-assLR = {!!}
	{+-}

	{-+}
	+-idR : ∀ {A} → A + 𝟎 → A
	+-idR = {!!}
	{+-}

	{-+}
	×+-dist : ∀ {A B C} → A × (B + C) → (A × B) + (A × C)
	×+-dist = ?
	{+-}



	{-+----------------------------------------------------------------------------+-}

	module naturals where

	open sum-and-product-types using (_↔_; _,_; 𝟎; 𝟏; unit)

	{--------------------------------------------------------------------------------}
	-- OK, we're convinced, but can't we just have normal + and × instead?
	-- (no, not really, because I've used those identifiers already)

	data ℕ : Set where -- we input ℕ as \bN
	zero : ℕ
	suc : ℕ → ℕ

	{-# BUILTIN NATURAL ℕ #-} -- means we can write 0, 1, 2, etc.

	_+_ : ℕ → ℕ → ℕ
	zero + y = y
	suc x + y = suc (x + y)

	ex1 : ℕ
	ex1 = 4 + 5

	-- but how do we write equalities? _↔_ won't really cut it for ℕ...

	ex2 : ℕ ↔ ℕ
	ex2 = (λ x → x) , (λ _ → 4)



	-- here be lies that I've hidden from you:
	-- we can tell Agda about _+_ so that it can optimize it better

	{-# BUILTIN NATPLUS _+_ #-}

	{--------------------------------------------------------------------------------}
	-- right, so how do we build equalities?
	-- (Coq kinda hides this definition from you, but it's there as well)

	infix 10 _≡_

	data _≡_ {A : Set} : A → A → Set where
	refl : ∀ {x} → x ≡ x

	{-+} -- make sure you write this using a dot pattern
	sym : ∀ {A} {x y : A} → x ≡ y → y ≡ x
	sym p = ?
	{+-}

	{-+}
	trans : ∀ {A} {x y z : A} → x ≡ y → y ≡ z → x ≡ z
	trans p q = ?
	{+-}

	{-+}
	cong : ∀ {A B} {x y} (f : A → B) → x ≡ y → f x ≡ f y
	cong f p = ?
	{+-}



	{-+----------------------------------------------------------------------------+-}

	-- here be lies that I've hidden from you:
	-- we can tell Agda about our equality so we can use it with 'rewrite'

	{-# BUILTIN EQUALITY _≡_ #-}

	{--------------------------------------------------------------------------------}
	-- right, so how do we build equalities? let's do some proofs!

	{-+}
	+-idR : ∀ x → x ≡ x + 0
	+-idR x = ?
	{+-}

	{-+}
	+-suc : ∀ x y → 1 + (x + y) ≡ x + (1 + y)
	+-suc x y = ?
	{+-}

	{-+}
	+-comm : ∀ x y → x + y ≡ y + x
	+-comm x y = ?
	{+-}

	{-+}
	+-assLR : ∀ x y z → x + (y + z) ≡ (x + y) + z
	+-assLR x y z = ?
	{+-}



	{--------------------------------------------------------------------------------}
	-- if you want to do this, you're free to -- but I'm not gonna

	_*_ : ℕ → ℕ → ℕ
	zero * y = 0
	suc x * y = y + (x * y)

	{-+}
	-idR : ∀ x → x ≡ x 0
	*-idR x = ?
	{+-}

	{-+}
	-suc : ∀ x y → 1 (x * y) ≡ x * (1 * y)
	*-suc x y = ?
	{+-}

	{-+}
	-comm : ∀ x y → x y ≡ y * x
	*-comm x y = ?
	{+-}

	{-+}
	-assLR : ∀ x y z → x (y * z) ≡ (x * y) * z
	*-assLR x y z = ?
	{+-}

	{-+}
	+-dist : ∀ x y z → x (y + z) → (x * y) + (x * z)
	*+-dist x y z = ?
	{+-}



	{-+----------------------------------------------------------------------------+-}

	-- here be lies that I've hidden from you:
	-- we can tell Agda about _+_ so that it can optimize it better

	{-# BUILTIN NATTIMES _*_ #-}

	{--------------------------------------------------------------------------------}
	-- but what if the proofs get really large? I don't wanna work that hard!

	data _≤_ : ℕ → ℕ → Set where -- we input ≤ as \<= or \le
	refl : ∀ {x} → 0 ≤ x
	step : ∀ {x y} → x ≤ y → suc x ≤ suc y

	ex3 : 4 ≤ 5
	ex3 = step (step (step (step refl)))

	-- this looks like it's going to be a problem...

	_≤?_ : ℕ → ℕ → Set
	zero ≤? y = 𝟏 -- that's the unit type
	suc x ≤? zero = 𝟎 -- that's the empty type
	suc x ≤? suc y = x ≤? y

	{-+}
	prove : ∀ x y → x ≤? y → x ≤ y
	prove x y p = ?
	{+-}

	{-+}
	ex4 : 112 ≤ 482
	ex4 = ?
	{+-}
	{-# OPTIONS --type-in-type #-} -- minor cheats follow
	module lecture2 where

	open import Agda.Builtin.FromNat using (Number)
	open import Data.Bool using (Bool; true; false; _∧_; if_then_else_)
	open import Data.Empty using () renaming (⊥ to 𝟎)
	open import Data.Maybe using (Maybe; just; nothing)
	open import Data.Nat using (ℕ; suc; zero; _≤?_)
	open import Data.Product using (_×_; _,_) renaming (proj₁ to fst; proj₂ to snd)
	open import Data.Unit using (tt) renaming (⊤ to 𝟏)
	open import Function as F using (case_of_)
	open import Relation.Nullary.Decidable using (True; toWitness)
	open import Relation.Binary.PropositionalEquality using (_≡_; _≢_; refl; cong₂)

	-- here be cheats: in order to overload natural number notation,
	-- we need to specify how it works for naturals... which is easy

	instance
	NatNumber : Number ℕ
	NatNumber = record
	{ Constraint = F.const 𝟏
	; fromNat = λ n → n
	}

	∧-split : ∀ {b₁ b₂} → b₁ ∧ b₂ ≡ true → b₁ ≡ true × b₂ ≡ true
	∧-split {false} {_} ()
	∧-split {true} {false} ()
	∧-split {true} {true} _ = (refl , refl)

	module coq-style-1 where

	{-------------------------------------------------------------------------}
	-- we're gonna talk about the simply-typed lambda calculus
	-- let's have some types, and a function to compare types, ok?

	data Type : Set where
	⋆ : Type {- mumble we don't really care what our atomic type is -}
	_⇒_ : Type → Type → Type

	-- and something to check when types are equal

	_==_ : Type → Type → Bool
	⋆ == ⋆ = true
	⋆ == (C ⇒ D) = false
	(A ⇒ B) == ⋆ = false
	(A ⇒ B) == (C ⇒ D) = A == C ∧ B == D

	-- in coq, you'd use this function and then prove

	==⟶≡ : ∀ A B → A == B ≡ true → A ≡ B
	==⟶≡ ⋆ ⋆ p = refl
	==⟶≡ ⋆ (B₁ ⇒ B₂) ()
	==⟶≡ (A₁ ⇒ A₂) ⋆ ()
	==⟶≡ (A₁ ⇒ A₂) (B₁ ⇒ B₂) p =
	-- ∧-split : ∀{b₁ b₂} → b₁ ∧ b₂ ≡ true → b₁ ≡ true × b₂ ≡ true
	case ∧-split p of λ{
	(p₁ , p₂) → cong₂ _⇒_ (==⟶≡ A₁ B₁ p₁) (==⟶≡ A₂ B₂ p₂) }

	-- and that way, you'd know your boolean function wasn't doing
	-- something incredibly stupid...
	-- like mine was, just now when I wrote these slides...

	-- anyway, anyone notice anything similar between _==_ and ==⟶≡?



	module agda-style-1 where

	open coq-style-1 public using (Type; ⋆; _⇒_)


	{-------------------------------------------------------------------------}
	-- hah, I tricked all of you!
	-- this lecture is about cultural differences between agda and coq...

	-- this is how you encode negation, "if you give me something of
	-- that type, I'll give you something which lives in the empty type"

	¬_ : Set → Set
	¬ P = P → 𝟎

	data Dec (P : Set) : Set where
	yes : ( p : P) → Dec P
	no : (¬p : ¬ P) → Dec P

	-- watch out, when we start writing this function, some scary things
	-- will start appearing -- keep in mind what it's all about:
	--
	-- a pattern match reveals information,
	-- and we don't want to just callously throw that away

	{-+}
	_≟_ : (A B : Type) → Dec (A ≡ B)
	A ≟ B = ?
	{+-}

	-- right, so we can _actually_ compare types now








	module coq-style-2 where

	open coq-style-1 public using (Type; ⋆; _⇒_)
	open import Agda.Builtin.Nat using (_==_)


	{-------------------------------------------------------------------------}
	-- I didn't lie, we're going to talk about the lambda calculus

	Id : Set
	Id = ℕ

	infixr 10 λ[_∶_]_
	infixl 20 _∙_

	data Term : Set where
	# : Id → Term
	λ[_∶_]_ : Id → Type → Term → Term
	_∙_ : Term → Term → Term

	-- let's look at some sample programs

	I = λ[ 0 ∶ ⋆ ] # 0
	K = λ[ 0 ∶ ⋆ ] λ[ 1 ∶ ⋆ ] # 0
	W = λ[ 0 ∶ ⋆ ] # 5

	-- right, we also need junk like substitution, reductions, etc...
	-- let's ignore that -- we don't have forever -- let's look at typing












	{-------------------------------------------------------------------------}
	-- if we wanna look at typing, though, we have to basically redo
	-- the Maps stuff from the homework

	Ctxt : Set
	Ctxt = Id → Maybe Type

	∅ : Ctxt
	∅ = λ _ → nothing

	_,_∶_ : Ctxt → Id → Type → Ctxt
	(Γ , x ∶ A) y =
	-- warning, cheats: that _==_ has type ℕ → ℕ → Bool
	if x == y then just A else Γ y

	_∶_∈_ : Id → Type → Ctxt → Set
	x ∶ A ∈ Γ = Γ x ≡ just A

	-- fine, that looks about right, we can worry about theorems later

	-- by which I mean not at all
















	infix 15 _,_∶_ _∶_∈_
	infix 5 _⊢_∶_ _⊢_

	{-------------------------------------------------------------------------}
	-- now, TYPING!

	data _⊢_∶_ (Γ : Ctxt) : Term → Type → Set where

	Ax : ∀ {x A} →

	x ∶ A ∈ Γ →
	----------- (Ax)
	Γ ⊢ # x ∶ A

	⇒I : ∀ {x N A B} →

	Γ , x ∶ A ⊢ N ∶ B →
	------------------------ (⇒I)
	Γ ⊢ λ[ x ∶ A ] N ∶ A ⇒ B

	⇒E : ∀ {L M A B} →

	Γ ⊢ L ∶ A ⇒ B → Γ ⊢ M ∶ A →
	-------------------------- (⇒E)
	Γ ⊢ L ∙ M ∶ B

	-- this predicate is actually doing two things at the same time
	-- let's make that a little bit clearer









	{-------------------------------------------------------------------------}
	-- this predicate is actually doing two things at the same time
	-- let's make that a little bit clearer

	-- let's remove as much of the type clutter as we can... easily

	_∈_ : Id → Ctxt → Set
	x ∈ Γ = Γ x ≢ nothing

	data _⊢_ (Γ : Ctxt) : Term → Set where

	Ax? : ∀ {x} →

	x ∈ Γ →
	------- (Ax?)
	Γ ⊢ # x

	⇒I? : ∀ {x N A} →

	Γ , x ∶ A ⊢ N →
	---------------- (⇒I?)
	Γ ⊢ λ[ x ∶ A ] N

	⇒E? : ∀ {L M} →

	Γ ⊢ L → Γ ⊢ M →
	--------------- (⇒E?)
	Γ ⊢ L ∙ M

	-- what predicate did we just encode? (albeit clumsily)







	module agda-style-2 where

	open agda-style-1

	{-------------------------------------------------------------------------}
	-- how can we clean up this predicate? what if we could prove that the
	-- type for variables had exactly n elements, and Γ provided a type for
	-- each of them?

	-- what does the type with exactly n elements look like?
	--
	-- * 0 lives in all types with at least 1 element
	--
	-- * if n lives in the type with m elements,
	-- then n + 1 lives in the type with m + 1 elements
	--

	data Fin : ℕ → Set where
	zero : {n : ℕ} → Fin (suc n)
	suc : {n : ℕ} → Fin n → Fin (suc n)

	f3of6 : Fin 6
	f3of6 = suc (suc (suc (zero {n = 2})))

	f3of7 : Fin 7
	f3of7 = suc (suc (suc (zero {n = 3})))

	-- and now?












	-- here be cheats: if we want to be able to use natural number
	-- notation for finite types, then we better have some constraints
	open import Data.Fin using (Fin; suc; zero; fromℕ≤)

	instance
	FinNumber : ∀ {n} → Number (Fin n)
	FinNumber {n} = record
	{ Constraint = λ{m → True (suc m ≤? n)}
	; fromNat = λ{m {{p}} → fromℕ≤ (toWitness p)}
	}

	module agda-style-3 where

	open agda-style-1

	{-------------------------------------------------------------------------}
	-- and now?
	-- we encode terms, with only a finite number of possibilities for vars

	data Term (n : ℕ) : Set where
	# : Fin n → Term n
	λ[_]_ : Type → Term (suc n) → Term n
	_∙_ : Term n → Term n → Term n

	-- oh, I forgot to tell you, we can write 0, 1, 2... for Fin too,
	-- as long as agda can figure out the upper bound
	f5in7 : Fin 7
	f5in7 = 5 {- there is some secret magic involved, though -}

	-- anyway, this is the identity function
	I : Term 0
	I = λ[ ⋆ ] # 0
	-- ^ \|
	-- \________/
	--
	-- ^^^^^^^^^^
	-- this is how binding works in de Bruijn notation

	-- once more
	K : Term 0
	K = λ[ ⋆ ] λ[ ⋆ ] # 1
	-- ^ \|
	-- \_______________/

	-- this term still exists, but now mentions that it exists _in context_
	W : Term 1
	W = {- some stuff is expected here -} λ[ ⋆ ] # 1
	-- ^ \|
	-- \___________________________/
	--
	-- we wrote # 5 last time, but those were names, these are indices
	-- so the index # 1 is just as good as the name # 5 or # 1203
	-- the only point is that it should move out of scope











	module agda-style-4 where

	open agda-style-1

	{-------------------------------------------------------------------------}
	-- right, so now we have well-scoped terms...
	-- why not restrict it to well-scoped, well-typed terms?

	data Vec (A : Set) : ℕ → Set where
	[] : Vec A 0
	_∷_ : ∀ {n} (x : A) (xs : Vec A n) → Vec A (suc n)

	_‼_ : ∀ {n} {A} → Vec A n → Fin n → A
	(x ∷ _ ) ‼ zero = x
	(_ ∷ xs) ‼ suc i = xs ‼ i

	Ctxt : ℕ → Set
	Ctxt n = Vec Type n

	data _⊢_ {n : ℕ} : Ctxt n → Type → Set where

	# : {Γ : Ctxt n} (x : Fin n) →

	----------- (Ax)
	Γ ⊢ (Γ ‼ x)

	λ[_]_ : {Γ : Ctxt n} (A : Type) {B : Type} →

	A ∷ Γ ⊢ B →
	----------- (⇒I)
	Γ ⊢ A ⇒ B

	_∙_ : {Γ : Ctxt n} {A B : Type} →

	Γ ⊢ A ⇒ B → Γ ⊢ A →
	------------------- (⇒E)
	Γ ⊢ B

	-- now we cannot ever write ill-typed terms

	I : {A : Type} → [] ⊢ A ⇒ A
	I {A} = λ[ A ] # 0

	K : {A B : Type} → [] ⊢ A ⇒ (B ⇒ A)
	K {A} {B} = λ[ A ] λ[ B ] # 1








	infix 5 _⊢_

	{-------------------------------------------------------------------------}
	-- is this fun? I don't know

	-- anyway, we (probably) don't have time to talk about reduction
	-- but what's the moral of the story?

	-- we have been systematically been pushing effort that we'd have
	-- to expend proving things into things that agda knows, simply
	-- because of the representation that we're using

	-- in that vein, one last trick, mock reduction:

	⟦_⟧ : Type → Set
	⟦ ⋆ ⟧ = ℕ -- why not?
	⟦ A ⇒ B ⟧ = ⟦ A ⟧ → ⟦ B ⟧

	data Env⟦_⟧ : {n : ℕ} → Vec Type n → Set where
	[] : Env⟦ [] ⟧
	_∷_ : ∀ {n} {A : Type} {Γ : Vec Type n} →
	⟦ A ⟧ → Env⟦ Γ ⟧ → Env⟦ A ∷ Γ ⟧

	lookup : ∀ {n} {Γ : Ctxt n} (x : Fin n) → Env⟦ Γ ⟧ → ⟦ Γ ‼ x ⟧
	lookup zero (x ∷ _) = x
	lookup (suc i) (_ ∷ e) = lookup i e

	⟪_⟫ : ∀ {n} {Γ : Ctxt n} {A : Type} →
	Γ ⊢ A → Env⟦ Γ ⟧ → ⟦ A ⟧
	⟪ # x ⟫ e = lookup x e
	⟪ λ[ A ] M ⟫ e = λ x → ⟪ M ⟫ (x ∷ e)
	⟪ M ∙ N ⟫ e = ⟪ M ⟫ e (⟪ N ⟫ e)

	id : ℕ → ℕ
	id = ⟪ I ⟫ []

	test-id : id ≡ λ x → x
	test-id = refl

	const : ℕ → ℕ → ℕ
	const = ⟪ K ⟫ []

	test-const : const ≡ λ x y → x
	test-const = refl






	-- -}