How to finish this bijection featuring finite inductive type

Stream: new members

[Xinyi Zhang]

I started with Lean 4 recently and I'm doing a project which uses finite types. In Lean 4, Fin n is used as a finite ordinal. But it turns out that it is easier to construct elements of inductive types (you define them that way).

The two can be used to construct two different notions of finite type:

inductive Sum2 (A B : Type) : Type
| inl (a : A) : Sum2 A B
| inr (b : B) : Sum2 A B

def f (n : Nat) : Sum2 (Fin n) (Fin 1) → Fin (n+1)
| Sum2.inl i => ⟨i.val, Nat.lt_succ_of_lt i.isLt⟩       -- left side stays same
| Sum2.inr _ => ⟨n, Nat.lt_succ_self n⟩

def g (n : Nat) : Fin (n+1) → Sum2 (Fin n) (Fin 1)
| ⟨k, _⟩ =>
  if hk : k < n then
    Sum2.inl ⟨k, hk⟩
  else
    Sum2.inr ⟨0, Nat.zero_lt_succ 0⟩

theorem fgId (n : Nat) (x : Fin (n+1)) :
  f n (g n x) = x := by
sorry

theorem gfId (n : Nat) (x : Sum2 (Fin n) (Fin 1)) :
    g n (f n x) = x := by
sorry

Finishing the proofs of these (filling in the sorry's) will lead immediately to a bijection between the two kinds of finite type.

I can't find how this can be done though. Can someone help me to complete the two theorems?

[Kevin Buzzard]

Unfold the definition of g and use the split tactic

[Xinyi Zhang]

I got it from that thanks a ton! Here's one side:

import Mathlib.Tactic

inductive Sum2 (A B : Type) : Type
| inl (a : A) : Sum2 A B
| inr (b : B) : Sum2 A B

def f (n : Nat) : Sum2 (Fin n) (Fin 1) → Fin (n+1)
| Sum2.inl i => ⟨i.val, Nat.lt_succ_of_lt i.isLt⟩       -- left side stays same
| Sum2.inr _ => ⟨n, Nat.lt_succ_self n⟩

def g (n : Nat) : Fin (n+1) → Sum2 (Fin n) (Fin 1)
| ⟨k, _⟩ =>
  if hk : k < n then
    Sum2.inl ⟨k, hk⟩
  else
    Sum2.inr ⟨0, Nat.zero_lt_succ 0⟩

theorem fg_branch_lt (n k : Nat) (hk : k < n) (isLt : k < n+1) :
  f n (Sum2.inl ⟨k, hk⟩) = ⟨k, isLt⟩ := by
  simp [f]

theorem fg_branch_ge (n k : Nat) (hk : ¬ (k < n)) (isLt : k < n+1) :
  f n (Sum2.inr ⟨0, Nat.zero_lt_succ 0⟩) = ⟨k, isLt⟩ := by
  have h_eq : k = n := by
    have h_le : k ≤ n := Nat.le_of_lt_succ isLt
    have h_ge : n ≤ k := by
      by_contra h
      apply hk
      exact Nat.lt_of_not_ge h
    exact Nat.le_antisymm h_le h_ge
  simp [f, h_eq]

theorem fgId (n : Nat) (x : Fin (n+1)) :
  f n (g n x) = x := by
cases x with
| mk k isLt =>
  by_cases hk : k < n
  · simp [g, hk]  -- now goal is literally f n (Sum2.inl ⟨k, hk⟩) = ⟨k, isLt⟩
    apply fg_branch_lt
  · simp [g, hk]  -- now goal is f n (Sum2.inr ⟨0,_⟩) = ⟨k, isLt⟩
    apply fg_branch_ge
    exact hk

I'm working on the other presently.

[Xinyi Zhang]

That one is simpler:

theorem gfId2 (n : Nat) (x : Sum2 (Fin n) (Fin 1)) :
  g n (f n x) = x := by
  cases x with
  | inl a =>
    simp [f, g]
  | inr b =>
    simp [f, g]
    -- now b : Fin 1, the only value is 0
    apply Fin.eq_of_val_eq
    simp