An example of two logically equivalent definitions in Lean, but with different "shapes".

indfin.lean

-- How easy is it to convert between two "obviously" equivalent
-- definitions? This file contains an example of doing this,
-- for two definitions of the typical "finite set of size n",
-- that is, the set {0, 1, 2, 3, ..., n-1}.

----------------------------------------------------------------
-- Core library definition.
----------------------------------------------------------------

-- The core library defines the type "fin n" as a record type
-- with two fields: "val" is a natural number, and "is_lt" is a
-- proof that "val < n".

#print fin
/-
@[pp_using_anonymous_constructor]
structure fin : ℕ → Type
fields:
fin.val : Π {n : ℕ}, fin n → ℕ
fin.is_lt : ∀ {n : ℕ} (c : fin n), c.val < n
-/

----------------------------------------------------------------
-- Alternative definition.
----------------------------------------------------------------

-- For the alternative, let's use an inductive definition: an
-- element of finite set {0, 1, 2, ..., n-1} is either zero, or
-- the successor of an element of the previous finite set
-- {0, 1, 2, ..., n-2}. We'll call this type "indfin n".

-- This mirrors the definition of "Fin n" in Agda's standard
-- library, see:
-- https://agda.github.io/agda-stdlib/Data.Fin.Base.html

inductive indfin : forall (n : nat), Type
| zero : forall (n : nat), indfin (n+1)
| succ : forall (n : nat) (i : indfin n), indfin (n+1)

----------------------------------------------------------------
-- The API for a Lean type.
----------------------------------------------------------------

-- In Lean, a new type definition comes with a few primitives,
-- from which everything else can be derived/implemented:
--
-- 1. The type name, which allows writing type annotations,
--    like "x : T" (among other uses).
--
-- 2. The type constructors, which allow creating values of the
--    new type.
--
-- 3. The type eliminator, "T.rec", which allows creating
--    dependently-typed functions with "T" as domain.
--
-- 4. A computational reduction rule for each constructor,
--    which simplifies expressions where the eliminator is
--    applied directly to a constructor.
--
-- In this file, the approach we take to showing the
-- equivalence between two types "T₁" and "T₂" is to emulate
-- the primitive API for "T₁" using "T₂", and vice versa.
--
-- 1. The type names "T₁" and "T₂" can be used as-is.
--
-- 2. The type constructors can be given by normal functions,
--    which construct an element of "T₁" from the data used to
--    construct an element of "T₂", and vice versa.
--
-- 3. Similarly, the eliminators can be normal functions.
--
-- 4. We can't add user-defined reduction rules, but we can get
--    almost the same result by proving the corresponding
--    propositional equalities.

----------------------------------------------------------------
-- The "fin" type supports the "indfin" API.
----------------------------------------------------------------

-- The first constructor for "indfin", followed by its
-- implementation using "fin".
#check @indfin.zero
/-
indfin.zero : Π (n : ℕ), indfin (n + 1)
-/
def fin.indfin.zero :
  forall (n : nat), fin (n+1) :=
    fun n, ⟨0, nat.zero_lt_succ n⟩

-- The second constructor for "indfin", followed by its
-- implementation using "fin".
#check @indfin.succ
/-
indfin.succ : Π (n : ℕ), indfin n → indfin (n + 1)
-/
def fin.indfin.succ :
  forall (n : nat) (i : fin n), fin (n+1) :=
    fun n, @fin.rec _ (fun _, fin (n+1))
    (fun val (is_lt : val < n),
      ⟨val+1, nat.succ_lt_succ is_lt⟩)

-- The eliminator for "indfin", followed by its implementation
-- using "fin".
#check @indfin.rec
/-
indfin.rec :
  Π {C : Π (n : ℕ), indfin n → Sort u},
    (Π (n : ℕ), C (n + 1) (indfin.zero n)) →
    (Π (n : ℕ) (i : indfin n),
      C n i → C (n + 1) (indfin.succ n i)) →
    Π {n : ℕ} (i : indfin n), C n i
-/
def fin.indfin.rec :
  forall {C : forall n (i : fin n), Sort*},
  (forall n, C (n+1) (fin.indfin.zero n)) ->
  (forall n (i : fin n), C n i -> C (n+1) (fin.indfin.succ n i)) ->
  forall n (i : fin n), C n i :=
    fun C zero succ, @nat.rec
    (fun n, forall (i : fin n), C n i)
    (fun i, fin.elim0 i)
    (fun n (recur : forall (i : fin n), C n i),
      fin.rec (@nat.rec
        (fun val, forall (is_lt : val < n+1), C (n+1) ⟨val, is_lt⟩)
        (fun is_lt, zero n)
        (fun val _ (is_lt : val+1 < n+1),
          let i : fin n := ⟨val, nat.lt_of_succ_lt_succ is_lt⟩
          in succ n i (recur i))))

-- The first reduction rule for "indfin".
example {C zero succ n} :
  (@indfin.rec C zero succ (n+1) (indfin.zero n)) =
  (zero n) :=
    rfl
-- The corresponding equality for "fin".
lemma fin.indfin.rec.on_zero {C zero succ n} :
  (@fin.indfin.rec C zero succ (n+1) (fin.indfin.zero n)) =
  (zero n) :=
    rfl

-- The second reduction rule for "indfin".
example {C zero succ n i} :
  (@indfin.rec C zero succ (n+1) (indfin.succ n i)) =
  (succ n i (@indfin.rec C zero succ n i)) :=
    rfl
-- The corresponding equality for "fin".
lemma fin.indfin.rec.on_succ {C zero succ n} : forall {i},
  (@fin.indfin.rec C zero succ (n+1) (fin.indfin.succ n i)) =
  (succ n i (@fin.indfin.rec C zero succ n i)) :=
    @fin.rec _
    (fun (i : fin n),
      (@fin.indfin.rec C zero succ (n+1) (fin.indfin.succ n i)) =
      (succ n i (@fin.indfin.rec C zero succ n i)))
    (fun val (is_lt : val < n), rfl)

----------------------------------------------------------------
-- The "indfin" type supports the "fin" API.
----------------------------------------------------------------

-- The only constructor for "fin", followed by its
-- implementation using "indfin".
#check @fin.mk
/-
fin.mk : Π {n : ℕ} (val : ℕ), val < n → fin n
-/
def indfin.fin.mk :
  forall {n : nat} (val : nat) (is_lt : val < n), (indfin n) :=
    @nat.rec
    (fun n, forall val (is_lt : val < n), indfin n)
    (fun val is_lt, false.elim (nat.not_lt_zero val is_lt))
    (fun n (recur : forall val (is_lt : val < n), indfin n),
      @nat.rec
      (fun val, forall (is_lt : val < n+1), indfin (n+1))
      (fun _, indfin.zero n)
      (fun val _ (is_lt : val+1 < n+1),
        indfin.succ n
        (recur val (nat.lt_of_succ_lt_succ is_lt))))

-- The field extractors "fin.val" and "fin.is_lt" are normally
-- implemented from the eliminator "fin.rec", but it's useful
-- to define them directly for "indfin".
def indfin.val :
  forall {n : nat} (i : indfin n), nat :=
    @indfin.rec
    (fun _ _, nat)
    (fun _, nat.zero)
    (fun _ _, nat.succ)

def indfin.is_lt :
  forall {n : nat} (i : indfin n), (i.val < n) :=
    @indfin.rec
    (fun n i, (i.val < n))
    nat.zero_lt_succ
    (fun _ _, nat.succ_lt_succ)

-- It's also useful to have a couple of equalities which relate
-- the emulated constructor "indfin.mk" and the emulated field
-- extractors.
lemma indfin.of_fin_mk :
  forall {n : nat} (i : indfin n),
  (indfin.fin.mk i.val i.is_lt) = i :=
    @indfin.rec
    (fun n i, (indfin.fin.mk i.val i.is_lt) = i)
    (fun _, rfl)
    (fun n i, @eq.rec (indfin n)
      (indfin.fin.mk i.val i.is_lt)
      (fun (x : indfin n),
        (indfin.fin.mk
          (indfin.succ n i).val
          (indfin.succ n i).is_lt)
        = indfin.succ n x)
      rfl i)

lemma indfin.val_of_fin_mk :
  forall {n : nat} (val : nat) (is_lt : val < n),
  (indfin.fin.mk val is_lt).val = val :=
    @nat.rec
    (fun n, forall val (is_lt : val < n), (indfin.fin.mk val is_lt).val = val)
    (fun val is_lt, false.elim (nat.not_lt_zero val is_lt))
    (fun n (recur : forall val (is_lt : val < n), (indfin.fin.mk val is_lt).val = val),
      @nat.rec
      (fun val, forall (is_lt : val < n+1), (indfin.fin.mk val is_lt).val = val)
      (fun is_lt, @eq.refl nat 0)
      (fun val _ (is_lt : val+1 < n+1),
        congr_arg nat.succ
        (recur val (nat.lt_of_succ_lt_succ is_lt))))

-- Note that there's no need for a corresponding lemma for
-- is_lt, because of proof irrelevance for Props.
-- Also, the type of "fin.is_lt" depends on the value of
-- "fin.val", so the relevant equation is maybe more
-- complicated than expected.
example {n : nat} (val : nat) (is_lt : val < n) :
  (indfin.fin.mk val is_lt).is_lt =
  (eq.rec is_lt (indfin.val_of_fin_mk val is_lt).symm) :=
    rfl

-- The eliminator for "fin", followed by its implementation
-- using "indfin". The actual work is done in the equalities
-- proved above, and the body of this definition is essentially
-- just a type-cast.
#check @fin.rec
/-
fin.rec :
  Π {n : ℕ} {C : fin n → Sort u},
  (Π (val : ℕ) (is_lt : val < n), C ⟨val, is_lt⟩) →
  Π (i : fin n), C i
-/
def indfin.fin.rec :
  forall {n : nat} {C : indfin n -> Sort*}
  (mk : forall (val : nat) (is_lt : val < n), C (indfin.fin.mk val is_lt))
  (i : indfin n), C i :=
    fun n C mk i, (@eq.rec _ _ C (mk i.val i.is_lt) _ (i.of_fin_mk))

-- The only reduction rule for "fin".
example {n C mk val is_lt} :
  (@fin.rec n C mk (fin.mk val is_lt)) =
  (mk val is_lt) :=
    rfl
-- The corresponding equality for "indfin". This involves many
-- type-casts to satisfy the type system, and was very
-- challenging to write.
lemma indfin.fin.rec.on_mk {n C mk val is_lt} :
  (@indfin.fin.rec n C mk (indfin.fin.mk val is_lt)) =
  (mk val is_lt) :=
    let
      i : (indfin n) :=
        (indfin.fin.mk val is_lt),
      v_is_lt : forall v (h : val = v), (v < n) :=
        (@eq.rec nat val (fun v, v < n) is_lt)
    in
      @eq.drec nat val
      (fun v (h : val = v),
        @eq (C i)
        (@eq.rec (indfin n)
          (indfin.fin.mk v (v_is_lt v h))
          C (mk v (v_is_lt v h))
          i (@eq.drec nat val
            (fun v (h : val = v),
              (indfin.fin.mk v (v_is_lt v h)) = i)
            (eq.refl i)
            v h))
        (mk val is_lt))
      (@eq.refl (C i) (mk val is_lt))
      i.val (indfin.val_of_fin_mk val is_lt).symm

----------------------------------------------------------------
-- Proving the formal equivalence.
----------------------------------------------------------------

-- With each of "fin" and "indfin" now having an implementation
-- of the the other type's low-level API, it should be easy to
-- write a bijection between them (and prove that it's a
-- bijection).

-- It seems easier to pick one of the two APIs and use it with
-- both types. For example, the following definitions and
-- lemmas use the "indfin" API (and all definitions/proofs are
-- of the same shape, split into a zero case and a succ case).

def fin_of_indfin :
  forall {n : nat}, (indfin n) -> (fin n) :=
    @indfin.rec
    (fun n i, fin n)
    fin.indfin.zero
    (fun n i recur, fin.indfin.succ n recur)

def indfin_of_fin :
  forall {n : nat}, (fin n) -> (indfin n) :=
    @fin.indfin.rec
    (fun n i, indfin n)
    indfin.zero
    (fun n i recur, indfin.succ n recur)

lemma fin_of_indfin_of_fin :
  forall {n : nat} (i : fin n),
  (fin_of_indfin (indfin_of_fin i)) = i :=
    @fin.indfin.rec
    (fun n i, (fin_of_indfin (indfin_of_fin i)) = i)
    (fun n, rfl)
    (fun n i recur, @eq.trans (fin (n+1))
      (fin_of_indfin (indfin_of_fin (fin.indfin.succ n i)))
      (fin_of_indfin (indfin.succ n (indfin_of_fin i)))
      (fin.indfin.succ n i)
      (congr_arg fin_of_indfin fin.indfin.rec.on_succ)
      (congr_arg (fin.indfin.succ n) recur))

lemma indfin_of_fin_of_indfin :
  forall {n : nat} (i : indfin n),
  (indfin_of_fin (fin_of_indfin i)) = i :=
    @indfin.rec
    (fun n i, (indfin_of_fin (fin_of_indfin i)) = i)
    (fun n, rfl)
    (fun n i recur, @eq.trans (indfin (n+1))
      (indfin_of_fin (fin.indfin.succ n (fin_of_indfin i)))
      (indfin.succ n (indfin_of_fin (fin_of_indfin i)))
      (indfin.succ n i)
      fin.indfin.rec.on_succ
      (congr_arg (indfin.succ n) recur))

-- We could instead use the other API, for "fin", and get a
-- different shape for the definitions/proofs.

def fin_of_indfin₂ {n : nat} :
  (indfin n) -> (fin n) :=
    @indfin.fin.rec n
    (fun i, fin n)
    fin.mk

def indfin_of_fin₂ {n : nat} :
  (fin n) -> (indfin n) :=
    @fin.rec n
    (fun i, indfin n)
    indfin.fin.mk

lemma fin_of_indfin_of_fin₂ {n : nat} :
  forall (i : fin n),
  (fin_of_indfin₂ (indfin_of_fin₂ i)) = i :=
    @fin.rec n
    (fun i, (fin_of_indfin₂ (indfin_of_fin₂ i)) = i)
    (fun val (is_lt : val < n), indfin.fin.rec.on_mk)

lemma indfin_of_fin_of_indfin₂ {n : nat} :
  forall (i : indfin n),
  (indfin_of_fin₂ (fin_of_indfin₂ i)) = i :=
    @indfin.fin.rec n
    (fun i, (indfin_of_fin₂ (fin_of_indfin₂ i)) = i)
    (fun val (is_lt : val < n), congr_arg indfin_of_fin₂
      (@indfin.fin.rec.on_mk n (fun i, fin n) fin.mk val is_lt))

-- It's also probably possible to show that
--
--       fin_of_indfin = fin_of_indfin₂
--
-- and
--
--       indfin_of_fin = indfin_of_fin₂
--
-- and many other equalities involving what these bijections to
-- to constructors and eliminators, but this file is long
-- enough as it is.