A Small Proof that Fin is Injective

{-# 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 Fins 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 Fins. 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 Fins to Fins.

_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 Fins, 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 congs 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.