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 (that is, in the result type).

Example 1.

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

which 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

which 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

It is always a better to use a parameter instead of an index, because:

*The parameter can be fixed in order to get a simpler definition, c.f.

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 _≤_.

Generic equality: _≡_

Consider the following definition


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

infix 4 _≡_

that yields the following judgements:

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

so we can come the conclusion that it actually represents equality.

_∈_ proposition

Consider another parametric definition:


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

infix 4 _∈_

Exercises

  1. Define _⊆_ {A : Set} : List A → List A → Set.

  2. Define a predicate for permutations.

  3. Define a predicate for sorting.

Note that you can type ⊆ as \sub=.