Finite basis for inductive types

induction.lean

universes i j k l m

def empty.elim (A : Sort i) (H : empty) : A :=
@empty.rec (λ e, A) H

def iso0 {A} {C : (empty → A) → Sort i} (f : empty → A) (H : C (empty.elim A)) : C f :=
eq.rec H (funext (empty.rec _) : empty.elim A = f)

def iso1 {A} {C : (unit → A) → Sort i} (f : unit → A) (H : C (λu, f ())) : C f :=
eq.rec H (funext (λu, unit.rec rfl u) : (λu, f ()) = f)

def iso_sigma {A X} {P : X → Sort i}
   (C: (psigma P → A) → Sort j) (f : psigma P → A)
   (H : C (λs, psigma.rec (λa b, f ⟨a, b⟩) s)) : C f :=
eq.rec H (funext (λ ⟨a, b⟩, rfl) : (λs, psigma.rec (λa b, f ⟨a, b⟩) s : psigma P → A) = f)

def iso_sum {A X Y} (C : (psum X Y → A) → Sort i) (f : psum X Y → A)
    (H : C (λs, psum.rec (λx, f (psum.inl x)) (λx, f (psum.inr x)) s)) : C f :=
eq.rec H (funext (λs, psum.rec (λa, rfl) (λb, rfl) s) :
 (λs, psum.rec (λx, f (psum.inl x)) (λx, f (psum.inr x)) s : psum X Y → A) = f)

-- Case 1: The inductive type is not in Prop, and lives in a universe above j,k.
-- In this case, we can eliminate into every sort.
section
  variables {α : Sort i} {β : Sort j} {ξ : β → Sort k}
    (p : β → α) (π : Π (b : β), ξ b → α)
  inductive ind : Π (a : α), Sort (max j k l 1)
  | intro (b : β) : (Π (x : ξ b), ind (π b x)) → ind (p b)

  def induction : α → Sort (max j k l 1) := @ind.{i j k l} α β ξ p π
  local notation `P` := induction p π

  def induction.intro : Π (b : β), (Π (x : ξ b), P (π b x)) → P (p b) :=
  @ind.intro α β ξ p π
  local notation `intro` := induction.intro p π

  @[elab_as_eliminator] def induction.rec :
    Π {C : Π (a : α), P a → Sort m},
      (Π (b : β) (u : Π (x : ξ b), P (π b x)),
         (Π (x : ξ b), C (π b x) (u x)) → C (p b) (intro b u)) →
       Π (a : α) (c : P a), C a c :=
  @ind.rec α β ξ p π
  local notation `elim` := @induction.rec α β ξ p π

  def induction.eq (C e b u) :
    elim C e (p b) (intro b u) = e b u (λx, elim C e (π b x) (u x)) := rfl
end

def Nat : Type :=
induction.{1 1 1 1} (λb, ()) (λb (x:cond b empty unit), ()) ()
private def Nat.intro : Π (b : bool),
       (cond b empty unit → Nat) → Nat :=
induction.intro (λb, ()) (λb (x:cond b empty unit), ())
def Nat.zero : Nat := Nat.intro tt (empty.elim Nat)
def Nat.succ (n : Nat) : Nat := Nat.intro ff (λ_, n)

def Nat.rec {C : Nat → Type l}
 (H0 : C Nat.zero) (Hs : Πa, C a → C (Nat.succ a)) (n : Nat) : C n :=
have Πb (u : cond b empty unit → Nat), (Πx, C (u x)) → C (Nat.intro b u),
from λb u, match b, u with
| ff, (u: unit → Nat) := λf : Π (x : unit), C (u x),
  show C (Nat.intro ff u), from iso1 u (by exact Hs (u ()) (f ()))
| tt, (u: empty → Nat) := λf : Π (x : empty), C (u x),
  show C (Nat.intro tt u), from iso0 u (by exact H0)
end,
@induction.rec _ _ _ (λb, ()) (λb (x:cond b empty unit), ())
  (λu, match u with () := C end) this () n

section
  variables {C : Nat → Type}
            (z : C Nat.zero)
            (s : Π (n : Nat), C n → C (Nat.succ n))
            (n : Nat)
  def f : Π (n : Nat), C n := Nat.rec z s
  example : f z s (Nat.succ n) = s n (f z s n) := rfl
  example : f z s Nat.zero = z := rfl
end

/- the key identities -/

example (A : Sort i) (C : (empty → A) → Sort j) (H : C (empty.elim A)) : 
  iso0 (empty.elim A) H = H := rfl

example (A : Sort i) (C : (unit → A) → Sort j) (a : A) (H : C (λ x, a)) : 
  iso1 (λ x, a) H = H := rfl

example (A : Sort i) (X : Sort j) (P : X → Sort k) (C: (psigma P → A) → Sort l) (f : Π(a:X), P a → A) 
    (H : C (@psigma.rec _ _ (λ_, A) f)) :
  iso_sigma C (@psigma.rec _ _ (λ_, A) f) H = H := rfl

example (A X Y) (C : (psum X Y → A) → Sort i) (f : psum X Y → A)
    (H : C (λs, psum.rec (λx, f (psum.inl x)) (λx, f (psum.inr x)) s)) :
  iso_sum C (λs, psum.rec (λx, f (psum.inl x)) (λx, f (psum.inr x)) s) H = H := rfl

-- Case 2: The inductive type may possibly be Prop, but is larger than the universes j,k.
-- In this case, we can only eliminate into Prop.
-- In principle, we can do case 2 & 3 in one go, using the universe imax (max j k) l, but
-- Lean doesn't accept this.

-- Unlike case 1 and case 3, this one has poor coverage - it is impossible to prove some
-- facts about equality of members.
section
  variables {α : Sort i} {β : Sort j} {ξ : β → Sort k}
    (p : β → α) (π : Π (b : β), ξ b → α)
  inductive sind : Π (a : α), Sort (max j k l)
  | intro (b : β) : (Π (x : ξ b), sind (π b x)) → sind (p b)

  def sinduction : α → Sort (max j k l) := @sind α β ξ p π
  local notation `P` := sinduction p π

  def sinduction.intro : Π (b : β), (Π (x : ξ b), P (π b x)) → P (p b) :=
  @sind.intro α β ξ p π
  local notation `intro` := sinduction.intro p π

  @[elab_as_eliminator] def sinduction.rec :
    Π {C : Π (a : α), P a → Prop},
      (Π (b : β) (u : Π (x : ξ b), P (π b x)),
         (Π (x : ξ b), C (π b x) (u x)) → C (p b) (intro b u)) →
       Π (a : α) (c : P a), C a c :=
  @sind.rec α β ξ p π
  local notation `elim` := @sinduction.rec α β ξ p π

  def sinduction.eq (C e b u) :
    elim C e (p b) (intro b u) = e b u (λx, elim C e (π b x) (u x)) := rfl
end

-- Case 3: The inductive type is Prop. It does not need to be larger than j,k (impredicative).
-- In this case, we can only eliminate into Prop.
section
  variables {α : Sort i} {β : Sort j} {ξ : β → Sort k}
    (p : β → α) (π : Π (b : β), ξ b → α)
  inductive pind : Π (a : α), Prop
  | intro (b : β) : (Π (x : ξ b), pind (π b x)) → pind (p b)

  def pinduction : α → Prop := @pind.{i j k} α β ξ p π
  local notation `P` := pinduction p π

  def pinduction.intro : Π (b : β), (Π (x : ξ b), P (π b x)) → P (p b) :=
  @pind.intro α β ξ p π
  local notation `intro` := pinduction.intro p π

  @[elab_as_eliminator] def pinduction.rec :
    Π {C : Π (a : α), P a → Prop},
      (Π (b : β) (u : Π (x : ξ b), P (π b x)),
         (Π (x : ξ b), C (π b x) (u x)) → C (p b) (intro b u)) →
       Π (a : α) (c : P a), C a c :=
  @pind.drec α β ξ p π
  local notation `elim` := @pinduction.rec α β ξ p π

  def pinduction.eq (C e b u) :
    elim C e (p b) (intro b u) = e b u (λx, elim C e (π b x) (u x)) := rfl
end

-- Case 4: The inductive type is Prop, but there is only one constructor and the parameters
-- are either in Prop, or in the return type. In this case, we can eliminate into any sort.
section
  variables {α : Sort i} {β : Sort j} {ξ : β → Sort k}
    (p : β → α) (π : Π (b : β), ξ b → α)
    (r : α → β) (h : function.left_inverse r p)
  inductive p1ind : Π (a : α) (b : β), Prop
  | intro (b : β) : (Π (x : ξ b), p1ind (π b x) (r (π b x))) → p1ind (p b) b

  lemma p1ind.lem {a : α} {b : β} (c : p1ind p π r a b) : p b = a :=
  p1ind.cases_on c (λb' _, rfl)

  lemma p1ind.lem2 (h : function.left_inverse r p)
    {a : α} {b : β} (c : p1ind p π r a b) : b = r a :=
  by rw [← p1ind.lem p π r c, h]

  def p1induction (a : α) : Prop := p1ind.{i j k} p π r a (r a)
  local notation `P` := p1induction p π r

  def p1induction.intro (h : function.left_inverse r p)
    (b : β) (u : Π (x : ξ b), P (π b x)) : P (p b) :=
  @eq.rec β b (p1ind p π r (p b)) (p1ind.intro b u) _ (eq.symm (h b))

  local notation `intro` := p1induction.intro p π r h

  @[elab_as_eliminator] def p1induction.rec
    {C : Π (a : α), P a → Sort m}
    (e : Π (b : β) (u : Π (x : ξ b), P (π b x)),
         (Π (x : ξ b), C (π b x) (u x)) → C (p b) (intro b u))
    (a : α) (c : P a) : C a c :=
  @p1ind.drec α β ξ p π r
    (λa b c, C a $ @eq.rec _ _ _ c _ $ p1ind.lem2 p π r h c)
    (λb u I, e b u I) _ (r a) c

  meta def p1induction.rec2
    {C : Π (a : α), P a → Sort m}
    (e : Π (b : β) (u : Π (x : ξ b), P (π b x)),
         (Π (x : ξ b), C (π b x) (u x)) → C (p b) (intro b u)) :
    Π (a : α) (c : P a), C a c :=
  λa c,
  have u : ∀x, P (π (r a) x), from p1ind.cases_on c (λb u, u),
  have C (p (r a)) (p1induction.intro p π r h (r a) u), from
    e (r a) u (λx, p1induction.rec2 (π (r a) x) _),
  match p (r a), p1ind.lem p π r c, p1induction.intro p π r h (r a) u, this with
  | .(a), rfl, c, (c' : C .(a) c) := c'
  end

  -- A type-incorrect version of rec2 after erasing Props.
  meta def p1induction.rec3
    (C : α → Sort m)
    (e : Π (b : β), (Π (x : ξ b), C (π b x)) → C (p b)) :
    Π (a : α), C a :=
  λa, cast (sorry : C (p (r a)) = C a) $ e (r a) (λx, p1induction.rec3 (π (r a) x))

  local notation `elim` := @p1induction.rec α β ξ p π r h

  -- Does not hold definitionally unless h is also a definitional equality
  def p1induction.eq (C e b u) :
    elim C e (p b) (intro b u) = e b u (λx, elim C e (π b x) (u x)) :=
    show @p1ind.drec α β ξ p π r
    (λa b c, C a $ @eq.rec _ _ _ c _ $ p1ind.lem2 p π r h c)
    (λb u I, e b u I) _ (r (p b))
    (@eq.rec β b (p1ind p π r (p b)) (p1ind.intro b u) _ (eq.symm (h b)))
       = e b u (λx, elim C e (π b x) (u x)), from
    match r (p b), eq.symm (h b) with ._, rfl := rfl end
end