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:

• We suggest more about the structure of the set.* In turn, the Agda compiler can infer more properties of this set.**

• Cleaner syntax: each constructor has one parameter less.

*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.

• Prove that 1 ∷ 2 ∷ [] ⊆ 1 ∷ 2 ∷ 3 ∷ [].
• Prove that 1 ∷ 2 ∷ 3 ∷ [] ⊆ 1 ∷ 2 ∷ [] is false.
2. Define a predicate for permutations.

3. Define a predicate for sorting.

Note that you can type ⊆ as \sub=.