module Sets.Parameters_vs_Indices where

Import List

open import Data.Nat using (ℕ; zero; suc; _≤_; z≤n; s≤s)
open import Data.List using (List; []; _∷_)

Parameters vs. indices

The first index can be turned into a new parameter if each constructor has the same variable on the first index position (in the result type).

Example 1

data _≤′_ : ℕ → ℕ → Set where
  ≤′-refl : {m : ℕ} →                       m ≤′ m
  ≤′-step : {m : ℕ} → {n : ℕ} →  m ≤′ n  →  m ≤′ suc n

is similar to

data _≤′_ (m : ℕ) : ℕ → Set where
  ≤′-refl :                       m ≤′ m
  ≤′-step : {n : ℕ} →  m ≤′ n  →  m ≤′ suc n

Example 2

data _≤″_ : ℕ → ℕ → Set where
  ≤+ : ∀ {m n k} → m + n ≡ k → m ≤″ k

is similar to

data _≤″_ (m : ℕ) : ℕ → Set where
  ≤+ : ∀ {n k} → m + n ≡ k → m ≤″ k

which is similar to

data _≤″_ (m : ℕ) (k : ℕ) : Set where
  ≤+ : ∀ {n} → m + n ≡ k → m ≤″ k

Design decision

A parameter instead of an index is always a better choice

• We state more about the structure of the set.*
  In turn, the Agda compiler can infer more properties of the set.**
• Cleaner syntax: each constructor has one parameter less.

*The parameter can be fixed to get a simpler definition, for example

data 10≤′ : ℕ → Set where
  10≤′-refl :                       10≤′ 10
  10≤′-step : {n : ℕ} →  10≤′ n  →  10≤′ suc n

was made from _≤′_ with a simple substitution which is possible with _≤_.

**TODO: give examples.

Parameters vs. indices (2)

The parameters of the set are present as implicit arguments in the constructors.

TODO

General equality: _≡_

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

infix  _≡_

yields

refl {ℕ} {0} : 0 ≡ 0
refl {ℕ} {1} : 1 ≡ 1
refl {ℕ} {2} : 2 ≡ 2
...

so it represents equality!

_∈_ proposition

Another parametric definition:

data _∈_ {A : Set}(x : A) : List A → Set where
  first : ∀ {xs} → x ∈ x ∷ xs
  later : ∀ {y xs} → x ∈ xs → x ∈ y ∷ xs

infix  _∈_

Exercises

• Define _⊆_ {A : Set} : List A → List A → Set!
  • Prove that 1 ∷ 2 ∷ [] ⊆ 1 ∷ 2 ∷ 3 ∷ []!
  • Prove that 1 ∷ 2 ∷ 3 ∷ [] ⊆ 1 ∷ 2 ∷ [] is false!
• Define a permutation predicate!
• Define a sort predicate!

You can type ⊆ as \sub=.