## A Small Proof that Fin is Injective

## Imports etc.

{-# OPTIONS --safe --without-K #-} module Post where open import Data.Fin using (Fin; suc; zero; _≟_) open import Data.Nat using (ℕ; suc; zero; _+_; compare; equal; greater; less) open import Data.Nat.Properties using (+-comm) open import Data.Bool using (not; T) open import Relation.Nullary using (yes; no; does; ¬_) open import Data.Product using (Σ; Σ-syntax; proj₁; proj₂; _,_) open import Data.Unit using (tt; ⊤) open import Function using (_∘_; id; _⟨_⟩_) open import Relation.Binary.PropositionalEquality using (subst; trans; cong; sym; _≡_; refl; _≢_) open import Data.Empty using (⊥-elim; ⊥) variable n m : ℕ

Here’s a puzzle: can you prove that `Fin`

is injective?
That’s the type constructor, by the way, not the type itself. Here’s the
type of the proof we want:

Goal : Set₁ Goal = ∀ {n m} → Fin n ≡ Fin m → n ≡ m

I’m going to present a proof of this lemma that has a couple interesting features. You should try it yourself before reading on, though: it’s difficult, but great practice for understanding Agda’s type system.

First off, I should say that it’s not really a “new” proof: it’s
basically Andras
Kovac’s proof, with one key change. That proof, as well as this one,
goes `--without-K`

: because I actually use this proof in some
work I’m doing in Cubical Agda at the moment, this was non optional. It
does make things significantly harder, and disallows nice tricks like
the ones
used by effectfully.

# Computational Inequalities

The trick we’re going to use comes courtesy of James Wood. The central idea is the following type:

_≢ᶠ_ : Fin n → Fin n → Set x ≢ᶠ y = T (not (does (x ≟ y)))

This proof of inequality of `Fin`

s is different from the
usual definition, which might be something like:

_≢ᶠ′_ : Fin n → Fin n → Set x ≢ᶠ′ y = x ≡ y → ⊥

Our definition is based on the decidable equality of two
`Fin`

s. It also uses the standard library’s new
`Dec`

type. Basically, we get better computation behaviour
from our definition. It behaves as if it were defined like so:

_≢ᶠ″_ : Fin n → Fin n → Set zero ≢ᶠ″ zero = ⊥ zero ≢ᶠ″ suc y = ⊤ suc x ≢ᶠ″ zero = ⊤ suc x ≢ᶠ″ suc y = x ≢ᶠ″ y

The benefit of this, in contrast to `_≢ᶠ′_`

, is that each
case becomes a definitional equality we don’t have to prove. Compare the
two following proofs of congruence under `suc`

:

cong-suc″ : ∀ {x y : Fin n} → x ≢ᶠ″ y → suc x ≢ᶠ″ suc y cong-suc″ p = p cong-suc′ : ∀ {x y : Fin n} → x ≢ᶠ′ y → suc x ≢ᶠ′ suc y cong-suc′ {n = suc n} p q = p (cong fpred q) where fpred : Fin (suc (suc n)) → Fin (suc n) fpred (suc x) = x fpred zero = zero

# The Proof

First, we will describe an “injection” for functions from
`Fin`

s to `Fin`

s.

_F↣_ : ℕ → ℕ → Set n F↣ m = Σ[ f ∈ (Fin n → Fin m) ] ∀ {x y} → x ≢ᶠ y → f x ≢ᶠ f y

We’re using the negated from of injectivity here, which is usually
avoided in constructive settings. It actually works a little better for
us here, though. Since we’re working in the domain of `Fin`

s,
and since our proof is prop-valued, it’s almost like we’re working in
classical logic.

Next, we have the workhorse of the proof, the `shrink`

lemma:

shift : (x y : Fin (suc n)) → x ≢ᶠ y → Fin n shift zero (suc y) x≢y = y shift {suc _} (suc x) zero x≢y = zero shift {suc _} (suc x) (suc y) x≢y = suc (shift x y x≢y) shift-inj : ∀ (x y z : Fin (suc n)) y≢x z≢x → y ≢ᶠ z → shift x y y≢x ≢ᶠ shift x z z≢x shift-inj zero (suc y) (suc z) y≢x z≢x neq = neq shift-inj {suc _} (suc x) zero (suc z) y≢x z≢x neq = tt shift-inj {suc _} (suc x) (suc y) zero y≢x z≢x neq = tt shift-inj {suc _} (suc x) (suc y) (suc z) y≢x z≢x neq = shift-inj x y z y≢x z≢x neq shrink : suc n F↣ suc m → n F↣ m shrink (f , inj) .proj₁ x = shift (f zero) (f (suc x)) (inj tt) shrink (f , inj) .proj₂ p = shift-inj (f zero) (f (suc _)) (f (suc _)) (inj tt) (inj tt) (inj p)

This will give us the inductive step for the overall proof. Notice
the absence of any `cong`

s or the like: the computation
behaviour of `≢ᶠ`

saves us on that particular front. Also we
don’t have to use `⊥-elim`

at any point: again, because of
the computation behaviour of `≢ᶠ`

, Agda knows that certain
cases are unreachable, so we don’t even have to define them.

Next, we derive the proof that a `Fin`

cannot inject into
a smaller `Fin`

.

¬plus-inj : ∀ n m → ¬ (suc (n + m) F↣ m) ¬plus-inj zero (suc m) inj = ¬plus-inj zero m (shrink inj) ¬plus-inj (suc n) m (f , inj) = ¬plus-inj n m (f ∘ suc , inj) ¬plus-inj zero zero (f , _) with f zero ... | ()

That’s actually the bulk of the proof done: the rest is Lego, joining up the pieces and types. First, we give the normal definition of injectivity:

Injective : ∀ {a b} {A : Set a} {B : Set b} → (A → B) → Set _ Injective f = ∀ {x y} → f x ≡ f y → x ≡ y _↣_ : ∀ {a b} → Set a → Set b → Set _ A ↣ B = Σ (A → B) Injective

Then we convert from one to the other:

toFin-inj : (Fin n ↣ Fin m) → n F↣ m toFin-inj f .proj₁ = f .proj₁ toFin-inj (f , inj) .proj₂ {x} {y} x≢ᶠy with x ≟ y | f x ≟ f y ... | no ¬p | yes p = ¬p (inj p) ... | no _ | no _ = tt

And finally we have our proof:

n≢sn+m : ∀ n m → Fin n ≢ Fin (suc (n + m)) n≢sn+m n m n≡m = ¬plus-inj m n (toFin-inj (subst (_↣ Fin n) (n≡m ⟨ trans ⟩ cong (Fin ∘ suc) (+-comm n m)) (id , id))) Fin-inj : Injective Fin Fin-inj {n} {m} n≡m with compare n m ... | equal _ = refl ... | less n k = ⊥-elim (n≢sn+m n k n≡m) ... | greater m k = ⊥-elim (n≢sn+m m k (sym n≡m)) _ : Goal _ = Fin-inj

All in all, the proof is about 36 lines, which is pretty short for what it does.