Geb.Mathlib.Computability.Cobham.Cases

Imports

/-
Copyright (c) 2026 Terence Rokop. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Terence Rokop
-/
module

public import Geb.Mathlib.Computability.Cobham.Basic
public import Geb.Mathlib.Computability.Cobham.Scan

Definition by cases over Cobham's class

A combinator selecting among 2 ^ p expressions of arity one by the low p bits of a scrutinee, and applying the selected one to a second argument. It imposes no condition on the expressions it selects among; Cobham.cases's docstring records why.

Main definitions

Cobham.bits — the bits of a scrutinee word, false past its end.

Cobham.shiftRaw, Cobham.shiftW — a tree of arity two at the predecessor of argument zero.

Cobham.casesRaw, Cobham.casesW, Cobham.casesSem — the case tree, its admissible form, and its meaning.

Cobham.cases, Cobham.casesOf — the case tree as an expression of C, and at its declared arity.

Main statements

Cobham.bits_succ, Cobham.bits_succ_tail, Cobham.bits_ofFn, Cobham.ofFn_bits — peeling, dropping, and the round trip against List.ofFn. ofFn_bits recovers the scrutinee, truncated and zero-padded, from the family its bits spell.

Cobham.wIndexRoot_shiftRaw, Cobham.wValid_shiftRaw, Cobham.arity_shiftW, Cobham.recBounded_shiftW — the shift's arity, admissibility and recursion bound.

Cobham.semAt_shiftW, Cobham.casesSem_eq, Cobham.casesSem_eq_eval — the shift's meaning, the branch the scrutinee selects, and the identification with the meaning the expression carries.

Cobham.wIndexRoot_casesRaw, Cobham.arity_casesW — the case tree's arity.

Cobham.wValid_casesRaw — admissibility, from the branches' own.

Cobham.recBounded_casesW — the recursion bound, from the branches' own together with those cond and pred already carry.

Cobham.stepWord_predIterOf, Cobham.stepWord_prependOf, Cobham.baseWord_prependOf, Cobham.baseWord_constAtOf, Cobham.stepWord_constAtOf, Cobham.stepWord_diagOf — the words the combinators of Cobham/Basic.lean contribute.

Implementation notes

The scrutinee is consumed by shifting it into the recursive subtree rather than by scrutinising an iterated predecessor of a fixed argument. At an iterated predecessor the scrutinee is not a variable, so no case analysis reduces the boundedRec node of cond and the semantic theorem is unreachable; shifting leaves the scrutinee as argument zero itself. It is also linear rather than quadratic in the number of bits dispatched on.

cond's empty branch is directed at the same subtree as its head-false branch, which reads a scrutinee shorter than p as zero-padded and keeps casesSem_eq free of a hypothesis.

ofFn_bits is proved by structural induction on the width. The route through List.ext_getElem and omega depends on Classical.choice.

The word characterisations naming baseWord or stepWord are stated here rather than beside the definitions they characterise, baseWord and stepWord being declared in Cobham/Scan.lean, which imports Cobham/Basic.lean.

References

[Cobham1965]

Tags

Cobham, bounded recursion on notation, definition by cases

namespace Cobhampublic section

The bits of a scrutinee word, indexed by Fin p, false past the word's end.

@[`@[expose]` has no effect outside a `module` fileexpose] def bits (p : ℕ) (w : List Bool) : Fin p → Bool :=
  fun j ↦ w.getD j false

Peeling the low bit of a scrutinee's bit family.

theorem bits_succ (p : ℕ) (w : List Bool) :
    bits (p + 1) w = Fin.cons (w.getD 0 false) (bits p w.tail) := byp:ℕw:List Bool⊢ bits (p + 1) w = Fin.cons (w.getD 0 false) (bits p w.tail)
  refine funext fun i ↦ Fin.cases ?_ (fun _ ↦ ?_) irefine_1p:ℕw:List Booli:Fin (p + 1)⊢ bits (p + 1) w 0 = Fin.cons (w.getD 0 false) (bits p w.tail) 0refine_2p:ℕw:List Booli:Fin (p + 1)x✝:Fin p⊢ bits (p + 1) w x✝.succ = Fin.cons (w.getD 0 false) (bits p w.tail) x✝.succ
  ·refine_1p:ℕw:List Booli:Fin (p + 1)⊢ bits (p + 1) w 0 = Fin.cons (w.getD 0 false) (bits p w.tail) 0 rflAll goals completed! 🐙
  ·refine_2p:ℕw:List Booli:Fin (p + 1)x✝:Fin p⊢ bits (p + 1) w x✝.succ = Fin.cons (w.getD 0 false) (bits p w.tail) x✝.succ match w with
    | [] =>p:ℕw:List Booli:Fin (p + 1)x✝:Fin p⊢ bits (p + 1) [] x✝.succ = Fin.cons ([].getD 0 false) (bits p [].tail) x✝.succ rflAll goals completed! 🐙
    | _ :: _ =>p:ℕw:List Booli:Fin (p + 1)x✝:Fin phead✝:Booltail✝:List Bool⊢ bits (p + 1) (head✝ :: tail✝) x✝.succ = Fin.cons ((head✝ :: tail✝).getD 0 false) (bits p (head✝ :: tail✝).tail) x✝.succ rflAll goals completed! 🐙

Dropping the low bit of a scrutinee's family.

theorem bits_succ_tail (p : ℕ) (w : List Bool) :
    (fun i : Fin p ↦ bits (p + 1) w i.succ) = bits p w.tail := byp:ℕw:List Bool⊢ (fun i ↦ bits (p + 1) w i.succ) = bits p w.tail
  funext ip:ℕw:List Booli:Fin p⊢ bits (p + 1) w i.succ = bits p w.tail i
  match w with
  | [] =>p:ℕw:List Booli:Fin p⊢ bits (p + 1) [] i.succ = bits p [].tail i rflAll goals completed! 🐙
  | _ :: _ =>p:ℕw:List Booli:Fin phead✝:Booltail✝:List Bool⊢ bits (p + 1) (head✝ :: tail✝) i.succ = bits p (head✝ :: tail✝).tail i rflAll goals completed! 🐙

The bits of a spelled-out family are the family.

theorem bits_ofFn {p : ℕ} (f : Fin p → Bool) : bits p (List.ofFn f) = f :=
  funext fun j ↦ byp:ℕf:Fin p → Boolj:Fin p⊢ bits p (List.ofFn f) j = f j simp [bits]All goals completed! 🐙

A spelled-out bit family is the scrutinee truncated and zero-padded.

theorem ofFn_bits : ∀ (p : ℕ) (w : List Bool),
    List.ofFn (bits p w) = w.take p ++ List.replicate (p - w.length) false :=
  Nat.rec (fun w ↦ byw:List Bool⊢ List.ofFn (bits Nat.zero w) = List.take Nat.zero w ++ List.replicate (Nat.zero - w.length) false
      rw [List.ofFn_zero,w:List Bool⊢ [] = List.take Nat.zero w ++ List.replicate (Nat.zero - w.length) false List.take_zero,w:List Bool⊢ [] = [] ++ List.replicate (Nat.zero - w.length) false Nat.zero_sub,w:List Bool⊢ [] = [] ++ List.replicate 0 false List.replicate_zero,w:List Bool⊢ [] = [] ++ []
        List.append_nilw:List Bool⊢ [] = []]All goals completed! 🐙)
    (fun p ih w ↦ byp:ℕih:∀ (w : List Bool), List.ofFn (bits p w) = List.take p w ++ List.replicate (p - w.length) falsew:List Bool⊢ List.ofFn (bits p.succ w) = List.take p.succ w ++ List.replicate (p.succ - w.length) false
      rw [List.ofFn_succ,p:ℕih:∀ (w : List Bool), List.ofFn (bits p w) = List.take p w ++ List.replicate (p - w.length) falsew:List Bool⊢ (bits p.succ w 0 :: List.ofFn fun i ↦ bits p.succ w i.succ) =
  List.take p.succ w ++ List.replicate (p.succ - w.length) false bits_succ_tail,p:ℕih:∀ (w : List Bool), List.ofFn (bits p w) = List.take p w ++ List.replicate (p - w.length) falsew:List Bool⊢ bits p.succ w 0 :: List.ofFn (bits p w.tail) = List.take p.succ w ++ List.replicate (p.succ - w.length) false ihp:ℕih:∀ (w : List Bool), List.ofFn (bits p w) = List.take p w ++ List.replicate (p - w.length) falsew:List Bool⊢ bits p.succ w 0 :: (List.take p w.tail ++ List.replicate (p - w.tail.length) false) =
  List.take p.succ w ++ List.replicate (p.succ - w.length) false]p:ℕih:∀ (w : List Bool), List.ofFn (bits p w) = List.take p w ++ List.replicate (p - w.length) falsew:List Bool⊢ bits p.succ w 0 :: (List.take p w.tail ++ List.replicate (p - w.tail.length) false) =
  List.take p.succ w ++ List.replicate (p.succ - w.length) false
      match w with
      | [] =>p:ℕih:∀ (w : List Bool), List.ofFn (bits p w) = List.take p w ++ List.replicate (p - w.length) falsew:List Bool⊢ bits p.succ [] 0 :: (List.take p [].tail ++ List.replicate (p - [].tail.length) false) =
  List.take p.succ [] ++ List.replicate (p.succ - [].length) false
        simp only [List.tail_nil, List.take_nil, List.nil_append,
          List.length_nil, Nat.sub_zero, List.replicate_succ]p:ℕih:∀ (w : List Bool), List.ofFn (bits p w) = List.take p w ++ List.replicate (p - w.length) falsew:List Bool⊢ bits p.succ [] 0 :: List.replicate p false = false :: List.replicate p false
        rflAll goals completed! 🐙
      | _ :: _ =>p:ℕih:∀ (w : List Bool), List.ofFn (bits p w) = List.take p w ++ List.replicate (p - w.length) falsew:List Boolhead✝:Booltail✝:List Bool⊢ bits p.succ (head✝ :: tail✝) 0 ::
    (List.take p (head✝ :: tail✝).tail ++ List.replicate (p - (head✝ :: tail✝).tail.length) false) =
  List.take p.succ (head✝ :: tail✝) ++ List.replicate (p.succ - (head✝ :: tail✝).length) false
        simp only [List.take_succ_cons, List.length_cons, Nat.succ_sub_succ,
          List.cons_append]p:ℕih:∀ (w : List Bool), List.ofFn (bits p w) = List.take p w ++ List.replicate (p - w.length) falsew:List Boolhead✝:Booltail✝:List Bool⊢ bits p.succ (head✝ :: tail✝) 0 ::
    (List.take p (head✝ :: tail✝).tail ++ List.replicate (p - (head✝ :: tail✝).tail.length) false) =
  head✝ :: (List.take p tail✝ ++ List.replicate (p - tail✝.length) false)
        rflAll goals completed! 🐙)

A tree of arity two, carried to the predecessor of argument zero: its own argument zero becomes pred of the outer one, its argument one the outer argument one.

@[`@[expose]` has no effect outside a `module` fileexpose] def shiftRaw (e : sig.toPFunctor.W) : sig.toPFunctor.W :=
  WType.mk (.comp 2 2) fun d ↦
    match d with
    | .inl () => e
    | .inr i =>
      ![WType.mk (.comp 2 1) (fun c ↦
          match c with
          | .inl () => predRaw
          | .inr _ => WType.mk (.proj 2 0) Fin.elim0),
        WType.mk (.proj 2 1) Fin.elim0] i

A shifted tree has arity two, whatever it shifts.

theorem wIndexRoot_shiftRaw (e : sig.toPFunctor.W) :
    sig.wIndexRoot (shiftRaw e) = 2 := rfl

A shifted tree is admissible when what it shifts is, at arity two.

theorem wValid_shiftRaw (e : sig.toPFunctor.W) (he : sig.WValid e)
    (ha : sig.wIndexRoot e = 2) : sig.WValid (shiftRaw e) :=
  ⟨fun d ↦ match d with
    | .inl () => he
    | .inr i =>
      match i with
      | 0 =>
        ⟨fun c ↦ match c with
          | .inl () => pred.1.1.2
          | .inr _ => ⟨fun c ↦ c.elim0, funext fun c ↦ c.elim0⟩,
        funext fun c ↦ match c with
          | .inl () =>
            (sig.wIndexValid_index_eq_wIndexRoot predRaw).trans pred.2
          | .inr _ => rfl⟩
      | 1 => ⟨fun c ↦ c.elim0, funext fun c ↦ c.elim0⟩,
  funext fun d ↦ match d with
    | .inl () => (sig.wIndexValid_index_eq_wIndexRoot e).trans ha
    | .inr i => match i with | 0 => rfl | 1 => rfl⟩

A shifted tree, carrying its admissibility.

@[`@[expose]` has no effect outside a `module` fileexpose] def shiftW (e : sig.W) (he : arity e = 2) : sig.W :=
  ⟨shiftRaw e.1, wValid_shiftRaw e.1 e.2 he⟩

A shifted tree's arity, in the form fst_eval composes with.

theorem arity_shiftW (e : sig.W) (he : arity e = 2) :
    arity (shiftW e he) = 2 := rfl

A shifted tree reads the tail of argument zero.

theorem semAt_shiftW (e : sig.W) (he : arity e = 2) (sel x : List Bool) :
    semAt 2 (shiftW e he) (arity_shiftW e he) ![sel, x] =
      semAt 2 e he ![sel.tail, x] := bye:sig.Whe:arity e = 2sel:List Boolx:List Bool⊢ semAt 2 (shiftW e he) ⋯ ![sel, x] = semAt 2 e he ![sel.tail, x]
  refine congrArg (semAt 2 e he) (funext fun i : Fin 2 ↦ ?_)e:sig.Whe:arity e = 2sel:List Boolx:List Booli:Fin 2⊢ transport ⋯
    ((↑⟨⟨Shape.comp 2 2, fun b ↦
                ((fun b ↦
                        WType.elim (SlicePFunctor.W.ElimData ((n : ℕ) × Sem n) Sigma.fst)
                          (SlicePFunctor.W.elimStep sig ((n : ℕ) × Sem n) Sigma.fst evalStep eval._proof_1)
                          ((fun d ↦
                              match d with
                              | Sum.inl PUnit.unit => ↑e
                              | Sum.inr i =>
                                ![WType.mk (Shape.comp 2 1) fun c ↦
                                      match c with
                                      | Sum.inl PUnit.unit => predRaw
                                      | Sum.inr val => WType.mk (Shape.proj 2 0) Fin.elim0,
                                    WType.mk (Shape.proj 2 1) Fin.elim0]
                                  i)
                            b))
                      b).value
                  ⋯⟩,
              ⋯⟩).snd
        (Sum.inr i)).snd
    ![sel, x] =
  ![sel.tail, x] i
  match i with
  | 0 =>e:sig.Whe:arity e = 2sel:List Boolx:List Booli:Fin 2⊢ transport ⋯
    ((↑⟨⟨Shape.comp 2 2, fun b ↦
                ((fun b ↦
                        WType.elim (SlicePFunctor.W.ElimData ((n : ℕ) × Sem n) Sigma.fst)
                          (SlicePFunctor.W.elimStep sig ((n : ℕ) × Sem n) Sigma.fst evalStep eval._proof_1)
                          ((fun d ↦
                              match d with
                              | Sum.inl PUnit.unit => ↑e
                              | Sum.inr i =>
                                ![WType.mk (Shape.comp 2 1) fun c ↦
                                      match c with
                                      | Sum.inl PUnit.unit => predRaw
                                      | Sum.inr val => WType.mk (Shape.proj 2 0) Fin.elim0,
                                    WType.mk (Shape.proj 2 1) Fin.elim0]
                                  i)
                            b))
                      b).value
                  ⋯⟩,
              ⋯⟩).snd
        (Sum.inr 0)).snd
    ![sel, x] =
  ![sel.tail, x] 0
    match sel with
    | [] =>e:sig.Whe:arity e = 2sel:List Boolx:List Booli:Fin 2⊢ transport ⋯
    ((↑⟨⟨Shape.comp 2 2, fun b ↦
                ((fun b ↦
                        WType.elim (SlicePFunctor.W.ElimData ((n : ℕ) × Sem n) Sigma.fst)
                          (SlicePFunctor.W.elimStep sig ((n : ℕ) × Sem n) Sigma.fst evalStep eval._proof_1)
                          ((fun d ↦
                              match d with
                              | Sum.inl PUnit.unit => ↑e
                              | Sum.inr i =>
                                ![WType.mk (Shape.comp 2 1) fun c ↦
                                      match c with
                                      | Sum.inl PUnit.unit => predRaw
                                      | Sum.inr val => WType.mk (Shape.proj 2 0) Fin.elim0,
                                    WType.mk (Shape.proj 2 1) Fin.elim0]
                                  i)
                            b))
                      b).value
                  ⋯⟩,
              ⋯⟩).snd
        (Sum.inr 0)).snd
    ![[], x] =
  ![[].tail, x] 0 rflAll goals completed! 🐙
    | b :: _ =>e:sig.Whe:arity e = 2sel:List Boolx:List Booli:Fin 2b:Booltail✝:List Bool⊢ transport ⋯
    ((↑⟨⟨Shape.comp 2 2, fun b ↦
                ((fun b ↦
                        WType.elim (SlicePFunctor.W.ElimData ((n : ℕ) × Sem n) Sigma.fst)
                          (SlicePFunctor.W.elimStep sig ((n : ℕ) × Sem n) Sigma.fst evalStep eval._proof_1)
                          ((fun d ↦
                              match d with
                              | Sum.inl PUnit.unit => ↑e
                              | Sum.inr i =>
                                ![WType.mk (Shape.comp 2 1) fun c ↦
                                      match c with
                                      | Sum.inl PUnit.unit => predRaw
                                      | Sum.inr val => WType.mk (Shape.proj 2 0) Fin.elim0,
                                    WType.mk (Shape.proj 2 1) Fin.elim0]
                                  i)
                            b))
                      b).value
                  ⋯⟩,
              ⋯⟩).snd
        (Sum.inr 0)).snd
    ![b :: tail✝, x] =
  ![(b :: tail✝).tail, x] 0 cases bfalsee:sig.Whe:arity e = 2sel:List Boolx:List Booli:Fin 2tail✝:List Bool⊢ transport ⋯
    ((↑⟨⟨Shape.comp 2 2, fun b ↦
                ((fun b ↦
                        WType.elim (SlicePFunctor.W.ElimData ((n : ℕ) × Sem n) Sigma.fst)
                          (SlicePFunctor.W.elimStep sig ((n : ℕ) × Sem n) Sigma.fst evalStep eval._proof_1)
                          ((fun d ↦
                              match d with
                              | Sum.inl PUnit.unit => ↑e
                              | Sum.inr i =>
                                ![WType.mk (Shape.comp 2 1) fun c ↦
                                      match c with
                                      | Sum.inl PUnit.unit => predRaw
                                      | Sum.inr val => WType.mk (Shape.proj 2 0) Fin.elim0,
                                    WType.mk (Shape.proj 2 1) Fin.elim0]
                                  i)
                            b))
                      b).value
                  ⋯⟩,
              ⋯⟩).snd
        (Sum.inr 0)).snd
    ![false :: tail✝, x] =
  ![(false :: tail✝).tail, x] 0truee:sig.Whe:arity e = 2sel:List Boolx:List Booli:Fin 2tail✝:List Bool⊢ transport ⋯
    ((↑⟨⟨Shape.comp 2 2, fun b ↦
                ((fun b ↦
                        WType.elim (SlicePFunctor.W.ElimData ((n : ℕ) × Sem n) Sigma.fst)
                          (SlicePFunctor.W.elimStep sig ((n : ℕ) × Sem n) Sigma.fst evalStep eval._proof_1)
                          ((fun d ↦
                              match d with
                              | Sum.inl PUnit.unit => ↑e
                              | Sum.inr i =>
                                ![WType.mk (Shape.comp 2 1) fun c ↦
                                      match c with
                                      | Sum.inl PUnit.unit => predRaw
                                      | Sum.inr val => WType.mk (Shape.proj 2 0) Fin.elim0,
                                    WType.mk (Shape.proj 2 1) Fin.elim0]
                                  i)
                            b))
                      b).value
                  ⋯⟩,
              ⋯⟩).snd
        (Sum.inr 0)).snd
    ![true :: tail✝, x] =
  ![(true :: tail✝).tail, x] 0 <;>falsee:sig.Whe:arity e = 2sel:List Boolx:List Booli:Fin 2tail✝:List Bool⊢ transport ⋯
    ((↑⟨⟨Shape.comp 2 2, fun b ↦
                ((fun b ↦
                        WType.elim (SlicePFunctor.W.ElimData ((n : ℕ) × Sem n) Sigma.fst)
                          (SlicePFunctor.W.elimStep sig ((n : ℕ) × Sem n) Sigma.fst evalStep eval._proof_1)
                          ((fun d ↦
                              match d with
                              | Sum.inl PUnit.unit => ↑e
                              | Sum.inr i =>
                                ![WType.mk (Shape.comp 2 1) fun c ↦
                                      match c with
                                      | Sum.inl PUnit.unit => predRaw
                                      | Sum.inr val => WType.mk (Shape.proj 2 0) Fin.elim0,
                                    WType.mk (Shape.proj 2 1) Fin.elim0]
                                  i)
                            b))
                      b).value
                  ⋯⟩,
              ⋯⟩).snd
        (Sum.inr 0)).snd
    ![false :: tail✝, x] =
  ![(false :: tail✝).tail, x] 0truee:sig.Whe:arity e = 2sel:List Boolx:List Booli:Fin 2tail✝:List Bool⊢ transport ⋯
    ((↑⟨⟨Shape.comp 2 2, fun b ↦
                ((fun b ↦
                        WType.elim (SlicePFunctor.W.ElimData ((n : ℕ) × Sem n) Sigma.fst)
                          (SlicePFunctor.W.elimStep sig ((n : ℕ) × Sem n) Sigma.fst evalStep eval._proof_1)
                          ((fun d ↦
                              match d with
                              | Sum.inl PUnit.unit => ↑e
                              | Sum.inr i =>
                                ![WType.mk (Shape.comp 2 1) fun c ↦
                                      match c with
                                      | Sum.inl PUnit.unit => predRaw
                                      | Sum.inr val => WType.mk (Shape.proj 2 0) Fin.elim0,
                                    WType.mk (Shape.proj 2 1) Fin.elim0]
                                  i)
                            b))
                      b).value
                  ⋯⟩,
              ⋯⟩).snd
        (Sum.inr 0)).snd
    ![true :: tail✝, x] =
  ![(true :: tail✝).tail, x] 0 rflAll goals completed! 🐙
  | 1 =>e:sig.Whe:arity e = 2sel:List Boolx:List Booli:Fin 2⊢ transport ⋯
    ((↑⟨⟨Shape.comp 2 2, fun b ↦
                ((fun b ↦
                        WType.elim (SlicePFunctor.W.ElimData ((n : ℕ) × Sem n) Sigma.fst)
                          (SlicePFunctor.W.elimStep sig ((n : ℕ) × Sem n) Sigma.fst evalStep eval._proof_1)
                          ((fun d ↦
                              match d with
                              | Sum.inl PUnit.unit => ↑e
                              | Sum.inr i =>
                                ![WType.mk (Shape.comp 2 1) fun c ↦
                                      match c with
                                      | Sum.inl PUnit.unit => predRaw
                                      | Sum.inr val => WType.mk (Shape.proj 2 0) Fin.elim0,
                                    WType.mk (Shape.proj 2 1) Fin.elim0]
                                  i)
                            b))
                      b).value
                  ⋯⟩,
              ⋯⟩).snd
        (Sum.inr 1)).snd
    ![sel, x] =
  ![sel.tail, x] 1 rflAll goals completed! 🐙

A shifted tree's recursion bound, from what it shifts together with the predecessor's own.

theorem recBounded_shiftW (e : sig.W) (he : arity e = 2) (hr : RecBounded e) :
    RecBounded (shiftW e he) :=
  ⟨trivial, fun d ↦ match d with
    | .inl () => hr
    | .inr i =>
      match i with
      | 0 => ⟨trivial, fun c ↦ match c with
          | .inl () => pred.1.2
          | .inr _ => ⟨trivial, fun c ↦ c.elim0⟩⟩
      | 1 => ⟨trivial, fun c ↦ c.elim0⟩⟩

The case tree over p bits of argument zero, applying the selected branch to argument one. cond's empty branch points at its head-false branch, which reads a short scrutinee as zero-padded; each level shifts the scrutinee, so the branch index is read off the low bits in order.

@[`@[expose]` has no effect outside a `module` fileexpose] def casesRaw :
    (p : ℕ) → ((Fin p → Bool) → sig.toPFunctor.W) → sig.toPFunctor.W :=
  Nat.rec (motive := fun p ↦
      ((Fin p → Bool) → sig.toPFunctor.W) → sig.toPFunctor.W)
    (fun br ↦ liftRaw (br Fin.elim0))
    (fun _ ih br ↦
      WType.mk (.comp 2 4) fun d ↦
        match d with
        | .inl () => condRaw
        | .inr i =>
          ![WType.mk (.proj 2 0) Fin.elim0,
            shiftRaw (ih (fun t ↦ br (Fin.cons false t))),
            shiftRaw (ih (fun t ↦ br (Fin.cons true t))),
            shiftRaw (ih (fun t ↦ br (Fin.cons false t)))] i)

The case tree has arity two, whatever it branches over.

theorem wIndexRoot_casesRaw (p : ℕ) (br : (Fin p → Bool) → sig.toPFunctor.W) :
    sig.wIndexRoot (casesRaw p br) = 2 := byp:ℕbr:(Fin p → Bool) → sig.W⊢ sig.wIndexRoot (casesRaw p br) = 2
  cases p with
  | zero =>zerobr:(Fin 0 → Bool) → sig.W⊢ sig.wIndexRoot (casesRaw 0 br) = 2 exact wIndexRoot_liftRaw _All goals completed! 🐙
  | succ _ =>succn✝:ℕbr:(Fin (n✝ + 1) → Bool) → sig.W⊢ sig.wIndexRoot (casesRaw (n✝ + 1) br) = 2 rflAll goals completed! 🐙

The case tree is admissible when every branch is, at arity one. The motive generalizes over the branch family, the recursive calls reindexing it.

theorem wValid_casesRaw : ∀ (p : ℕ) (br : (Fin p → Bool) → sig.toPFunctor.W),
    (∀ v, sig.WValid (br v)) → (∀ v, sig.wIndexRoot (br v) = 1) →
    sig.WValid (casesRaw p br) :=
  Nat.rec (fun _ hv ha ↦ wValid_liftRaw _ (hv _) (ha _))
    (fun p ih _ hv ha ↦
      ⟨fun d ↦ match d with
        | .inl () => cond.1.1.2
        | .inr i =>
          match i with
          | 0 => ⟨fun c ↦ c.elim0, funext fun c ↦ c.elim0⟩
          | 1 => wValid_shiftRaw _ (ih _ (fun _ ↦ hv _) (fun _ ↦ ha _))
              (wIndexRoot_casesRaw p _)
          | 2 => wValid_shiftRaw _ (ih _ (fun _ ↦ hv _) (fun _ ↦ ha _))
              (wIndexRoot_casesRaw p _)
          | 3 => wValid_shiftRaw _ (ih _ (fun _ ↦ hv _) (fun _ ↦ ha _))
              (wIndexRoot_casesRaw p _),
      funext fun d ↦ match d with
        | .inl () => (sig.wIndexValid_index_eq_wIndexRoot condRaw).trans cond.2
        | .inr i =>
          match i with
          | 0 => rfl
          | 1 => (sig.wIndexValid_index_eq_wIndexRoot _).trans
              (wIndexRoot_shiftRaw _)
          | 2 => (sig.wIndexValid_index_eq_wIndexRoot _).trans
              (wIndexRoot_shiftRaw _)
          | 3 => (sig.wIndexValid_index_eq_wIndexRoot _).trans
              (wIndexRoot_shiftRaw _)⟩)

The case tree over expressions, carrying its admissibility.

@[`@[expose]` has no effect outside a `module` fileexpose] def casesW (p : ℕ) (br : (Fin p → Bool) → COf 1) : sig.W :=
  ⟨casesRaw p (fun v ↦ (br v).1.1.1),
    wValid_casesRaw p _ (fun v ↦ (br v).1.1.2) (fun v ↦ (br v).2)⟩

The case tree's arity, in the form fst_eval composes with.

theorem arity_casesW (p : ℕ) (br : (Fin p → Bool) → COf 1) :
    arity (casesW p br) = 2 :=
  wIndexRoot_casesRaw p _

The meaning of a case tree at its arity, read at the raw tree.

@[`@[expose]` has no effect outside a `module` fileexpose] def casesSem (p : ℕ) (br : (Fin p → Bool) → COf 1) : Sem 2 :=
  semAt 2 (casesW p br) (arity_casesW p br)

A case tree applies the branch its scrutinee selects to argument one, the scrutinee zero-padded past its end.

theorem casesSem_eq : ∀ (p : ℕ) (br : (Fin p → Bool) → COf 1)
    (sel x : List Bool),
    casesSem p br ![sel, x] = stepWord (br (bits p sel)) x :=
  Nat.rec
    (fun br sel x ↦ bybr:(Fin Nat.zero → Bool) → COf 1sel:List Boolx:List Bool⊢ casesSem Nat.zero br ![sel, x] = stepWord (br (bits Nat.zero sel)) x
      have hb : bits 0 sel = Fin.elim0 := funext fun i ↦ i.elim0br:(Fin Nat.zero → Bool) → COf 1sel:List Boolx:List Boolhb:bits 0 sel = Fin.elim0⊢ casesSem Nat.zero br ![sel, x] = stepWord (br (bits Nat.zero sel)) x
      rw [hbbr:(Fin Nat.zero → Bool) → COf 1sel:List Boolx:List Boolhb:bits 0 sel = Fin.elim0⊢ casesSem Nat.zero br ![sel, x] = stepWord (br Fin.elim0) x]br:(Fin Nat.zero → Bool) → COf 1sel:List Boolx:List Boolhb:bits 0 sel = Fin.elim0⊢ casesSem Nat.zero br ![sel, x] = stepWord (br Fin.elim0) x
      change semAt 1 (br Fin.elim0).1.1 (br Fin.elim0).2 (fun _ ↦ x) = _br:(Fin Nat.zero → Bool) → COf 1sel:List Boolx:List Boolhb:bits 0 sel = Fin.elim0⊢ (semAt 1 ↑↑(br Fin.elim0) ⋯ fun x_1 ↦ x) = stepWord (br Fin.elim0) x
      exact congrArg _ (funext fun i ↦ match i with | ⟨0, _⟩ => rfl)All goals completed! 🐙)
    (fun p ih br sel x ↦ byp:ℕih:∀ (br : (Fin p → Bool) → COf 1) (sel x : List Bool), casesSem p br ![sel, x] = stepWord (br (bits p sel)) xbr:(Fin p.succ → Bool) → COf 1sel:List Boolx:List Bool⊢ casesSem p.succ br ![sel, x] = stepWord (br (bits p.succ sel)) x
      rw [bits_succp:ℕih:∀ (br : (Fin p → Bool) → COf 1) (sel x : List Bool), casesSem p br ![sel, x] = stepWord (br (bits p sel)) xbr:(Fin p.succ → Bool) → COf 1sel:List Boolx:List Bool⊢ casesSem p.succ br ![sel, x] = stepWord (br (Fin.cons (sel.getD 0 false) (bits p sel.tail))) x]p:ℕih:∀ (br : (Fin p → Bool) → COf 1) (sel x : List Bool), casesSem p br ![sel, x] = stepWord (br (bits p sel)) xbr:(Fin p.succ → Bool) → COf 1sel:List Boolx:List Bool⊢ casesSem p.succ br ![sel, x] = stepWord (br (Fin.cons (sel.getD 0 false) (bits p sel.tail))) x
      match sel with
      | [] =>p:ℕih:∀ (br : (Fin p → Bool) → COf 1) (sel x : List Bool), casesSem p br ![sel, x] = stepWord (br (bits p sel)) xbr:(Fin p.succ → Bool) → COf 1sel:List Boolx:List Bool⊢ casesSem p.succ br ![[], x] = stepWord (br (Fin.cons ([].getD 0 false) (bits p [].tail))) x
        have h : casesSem (p + 1) br ![[], x] =
            casesSem p (fun s ↦ br (Fin.cons false s)) ![[], x] :=
          semAt_shiftW (casesW p fun s ↦ br (Fin.cons false s))
            (arity_casesW p _) [] xp:ℕih:∀ (br : (Fin p → Bool) → COf 1) (sel x : List Bool), casesSem p br ![sel, x] = stepWord (br (bits p sel)) xbr:(Fin p.succ → Bool) → COf 1sel:List Boolx:List Boolh:casesSem (p + 1) br ![[], x] = casesSem p (fun s ↦ br (Fin.cons false s)) ![[], x]⊢ casesSem p.succ br ![[], x] = stepWord (br (Fin.cons ([].getD 0 false) (bits p [].tail))) x
        rw [h,p:ℕih:∀ (br : (Fin p → Bool) → COf 1) (sel x : List Bool), casesSem p br ![sel, x] = stepWord (br (bits p sel)) xbr:(Fin p.succ → Bool) → COf 1sel:List Boolx:List Boolh:casesSem (p + 1) br ![[], x] = casesSem p (fun s ↦ br (Fin.cons false s)) ![[], x]⊢ casesSem p (fun s ↦ br (Fin.cons false s)) ![[], x] = stepWord (br (Fin.cons ([].getD 0 false) (bits p [].tail))) x ihp:ℕih:∀ (br : (Fin p → Bool) → COf 1) (sel x : List Bool), casesSem p br ![sel, x] = stepWord (br (bits p sel)) xbr:(Fin p.succ → Bool) → COf 1sel:List Boolx:List Boolh:casesSem (p + 1) br ![[], x] = casesSem p (fun s ↦ br (Fin.cons false s)) ![[], x]⊢ stepWord (br (Fin.cons false (bits p []))) x = stepWord (br (Fin.cons ([].getD 0 false) (bits p [].tail))) x]p:ℕih:∀ (br : (Fin p → Bool) → COf 1) (sel x : List Bool), casesSem p br ![sel, x] = stepWord (br (bits p sel)) xbr:(Fin p.succ → Bool) → COf 1sel:List Boolx:List Boolh:casesSem (p + 1) br ![[], x] = casesSem p (fun s ↦ br (Fin.cons false s)) ![[], x]⊢ stepWord (br (Fin.cons false (bits p []))) x = stepWord (br (Fin.cons ([].getD 0 false) (bits p [].tail))) x
        rflAll goals completed! 🐙
      | true :: t =>p:ℕih:∀ (br : (Fin p → Bool) → COf 1) (sel x : List Bool), casesSem p br ![sel, x] = stepWord (br (bits p sel)) xbr:(Fin p.succ → Bool) → COf 1sel:List Boolx:List Boolt:List Bool⊢ casesSem p.succ br ![true :: t, x] = stepWord (br (Fin.cons ((true :: t).getD 0 false) (bits p (true :: t).tail))) x
        have h : casesSem (p + 1) br ![true :: t, x] =
            casesSem p (fun s ↦ br (Fin.cons true s)) ![t, x] :=
          semAt_shiftW (casesW p fun s ↦ br (Fin.cons true s))
            (arity_casesW p _) (true :: t) xp:ℕih:∀ (br : (Fin p → Bool) → COf 1) (sel x : List Bool), casesSem p br ![sel, x] = stepWord (br (bits p sel)) xbr:(Fin p.succ → Bool) → COf 1sel:List Boolx:List Boolt:List Boolh:casesSem (p + 1) br ![true :: t, x] = casesSem p (fun s ↦ br (Fin.cons true s)) ![t, x]⊢ casesSem p.succ br ![true :: t, x] = stepWord (br (Fin.cons ((true :: t).getD 0 false) (bits p (true :: t).tail))) x
        rw [h,p:ℕih:∀ (br : (Fin p → Bool) → COf 1) (sel x : List Bool), casesSem p br ![sel, x] = stepWord (br (bits p sel)) xbr:(Fin p.succ → Bool) → COf 1sel:List Boolx:List Boolt:List Boolh:casesSem (p + 1) br ![true :: t, x] = casesSem p (fun s ↦ br (Fin.cons true s)) ![t, x]⊢ casesSem p (fun s ↦ br (Fin.cons true s)) ![t, x] =
  stepWord (br (Fin.cons ((true :: t).getD 0 false) (bits p (true :: t).tail))) x ihp:ℕih:∀ (br : (Fin p → Bool) → COf 1) (sel x : List Bool), casesSem p br ![sel, x] = stepWord (br (bits p sel)) xbr:(Fin p.succ → Bool) → COf 1sel:List Boolx:List Boolt:List Boolh:casesSem (p + 1) br ![true :: t, x] = casesSem p (fun s ↦ br (Fin.cons true s)) ![t, x]⊢ stepWord (br (Fin.cons true (bits p t))) x =
  stepWord (br (Fin.cons ((true :: t).getD 0 false) (bits p (true :: t).tail))) x]p:ℕih:∀ (br : (Fin p → Bool) → COf 1) (sel x : List Bool), casesSem p br ![sel, x] = stepWord (br (bits p sel)) xbr:(Fin p.succ → Bool) → COf 1sel:List Boolx:List Boolt:List Boolh:casesSem (p + 1) br ![true :: t, x] = casesSem p (fun s ↦ br (Fin.cons true s)) ![t, x]⊢ stepWord (br (Fin.cons true (bits p t))) x =
  stepWord (br (Fin.cons ((true :: t).getD 0 false) (bits p (true :: t).tail))) x
        rflAll goals completed! 🐙
      | false :: t =>p:ℕih:∀ (br : (Fin p → Bool) → COf 1) (sel x : List Bool), casesSem p br ![sel, x] = stepWord (br (bits p sel)) xbr:(Fin p.succ → Bool) → COf 1sel:List Boolx:List Boolt:List Bool⊢ casesSem p.succ br ![false :: t, x] = stepWord (br (Fin.cons ((false :: t).getD 0 false) (bits p (false :: t).tail))) x
        have h : casesSem (p + 1) br ![false :: t, x] =
            casesSem p (fun s ↦ br (Fin.cons false s)) ![t, x] :=
          semAt_shiftW (casesW p fun s ↦ br (Fin.cons false s))
            (arity_casesW p _) (false :: t) xp:ℕih:∀ (br : (Fin p → Bool) → COf 1) (sel x : List Bool), casesSem p br ![sel, x] = stepWord (br (bits p sel)) xbr:(Fin p.succ → Bool) → COf 1sel:List Boolx:List Boolt:List Boolh:casesSem (p + 1) br ![false :: t, x] = casesSem p (fun s ↦ br (Fin.cons false s)) ![t, x]⊢ casesSem p.succ br ![false :: t, x] = stepWord (br (Fin.cons ((false :: t).getD 0 false) (bits p (false :: t).tail))) x
        rw [h,p:ℕih:∀ (br : (Fin p → Bool) → COf 1) (sel x : List Bool), casesSem p br ![sel, x] = stepWord (br (bits p sel)) xbr:(Fin p.succ → Bool) → COf 1sel:List Boolx:List Boolt:List Boolh:casesSem (p + 1) br ![false :: t, x] = casesSem p (fun s ↦ br (Fin.cons false s)) ![t, x]⊢ casesSem p (fun s ↦ br (Fin.cons false s)) ![t, x] =
  stepWord (br (Fin.cons ((false :: t).getD 0 false) (bits p (false :: t).tail))) x ihp:ℕih:∀ (br : (Fin p → Bool) → COf 1) (sel x : List Bool), casesSem p br ![sel, x] = stepWord (br (bits p sel)) xbr:(Fin p.succ → Bool) → COf 1sel:List Boolx:List Boolt:List Boolh:casesSem (p + 1) br ![false :: t, x] = casesSem p (fun s ↦ br (Fin.cons false s)) ![t, x]⊢ stepWord (br (Fin.cons false (bits p t))) x =
  stepWord (br (Fin.cons ((false :: t).getD 0 false) (bits p (false :: t).tail))) x]p:ℕih:∀ (br : (Fin p → Bool) → COf 1) (sel x : List Bool), casesSem p br ![sel, x] = stepWord (br (bits p sel)) xbr:(Fin p.succ → Bool) → COf 1sel:List Boolx:List Boolt:List Boolh:casesSem (p + 1) br ![false :: t, x] = casesSem p (fun s ↦ br (Fin.cons false s)) ![t, x]⊢ stepWord (br (Fin.cons false (bits p t))) x =
  stepWord (br (Fin.cons ((false :: t).getD 0 false) (bits p (false :: t).tail))) x
        rflAll goals completed! 🐙)

The case tree's recursion bound, from the branches' own together with those cond and pred already carry.

theorem recBounded_casesW : ∀ (p : ℕ) (br : (Fin p → Bool) → COf 1),
    RecBounded (casesW p br) :=
  Nat.rec (fun br ↦ recBounded_liftRaw (br Fin.elim0))
    (fun p ih br ↦
      ⟨trivial, fun d ↦ match d with
        | .inl () => cond.1.2
        | .inr i =>
          match i with
          | 0 => ⟨trivial, fun c ↦ c.elim0⟩
          | 1 => recBounded_shiftW _ (arity_casesW p _)
              (ih (fun t ↦ br (Fin.cons false t)))
          | 2 => recBounded_shiftW _ (arity_casesW p _)
              (ih (fun t ↦ br (Fin.cons true t)))
          | 3 => recBounded_shiftW _ (arity_casesW p _)
              (ih (fun t ↦ br (Fin.cons false t)))⟩)

The case tree as an expression. Definition by cases imposes no condition on the expressions it selects among: every node the recursion introduces is a comp, whose RecBoundedValue is True, over proj together with the trees underlying cond and pred, which carry their own recursion bounds already.

@[`@[expose]` has no effect outside a `module` fileexpose] def cases (p : ℕ) (br : (Fin p → Bool) → COf 1) : C :=
  ⟨casesW p br, recBounded_casesW p br⟩

cases at its declared arity.

@[`@[expose]` has no effect outside a `module` fileexpose] def casesOf (p : ℕ) (br : (Fin p → Bool) → COf 1) : COf 2 :=
  ⟨cases p br, arity_casesW p br⟩

The meaning read at the raw tree is the meaning the expression carries. Unlike the scan combinator's counterpart this is not a rfl: arity_casesW is a theorem rather than a definitional equality, so the transport it carries is opaque.

theorem casesSem_eq_eval (p : ℕ) (br : (Fin p → Bool) → COf 1) :
    transport (casesOf p br).2 (casesOf p br).1.eval = casesSem p br :=
  transport_transport (fst_eval (casesW p br)) (arity_casesW p br)
    (eval (casesW p br)).2

The iterated predecessor drops k bits.

theorem stepWord_predIterOf : ∀ (k : ℕ) (u : List Bool),
    stepWord (predIterOf k) u = u.drop k :=
  Nat.rec (fun _ ↦ rfl)
    (fun j ih u ↦ byj:ℕih:∀ (u : List Bool), stepWord (predIterOf j) u = List.drop j uu:List Bool⊢ stepWord (predIterOf j.succ) u = List.drop j.succ u
      have hfun : (fun _ : Fin 1 ↦ stepWord (predIterOf j) u) =
          ![stepWord (predIterOf j) u] :=
        funext fun i ↦ match i with | ⟨0, _⟩ => rflj:ℕih:∀ (u : List Bool), stepWord (predIterOf j) u = List.drop j uu:List Boolhfun:(fun x ↦ stepWord (predIterOf j) u) = ![stepWord (predIterOf j) u]⊢ stepWord (predIterOf j.succ) u = List.drop j.succ u
      have h : stepWord (predIterOf (j + 1)) u =
          predSem ![stepWord (predIterOf j) u] := congrArg predSem hfunj:ℕih:∀ (u : List Bool), stepWord (predIterOf j) u = List.drop j uu:List Boolhfun:(fun x ↦ stepWord (predIterOf j) u) = ![stepWord (predIterOf j) u]h:stepWord (predIterOf (j + 1)) u = predSem ![stepWord (predIterOf j) u]⊢ stepWord (predIterOf j.succ) u = List.drop j.succ u
      rw [h,j:ℕih:∀ (u : List Bool), stepWord (predIterOf j) u = List.drop j uu:List Boolhfun:(fun x ↦ stepWord (predIterOf j) u) = ![stepWord (predIterOf j) u]h:stepWord (predIterOf (j + 1)) u = predSem ![stepWord (predIterOf j) u]⊢ predSem ![stepWord (predIterOf j) u] = List.drop j.succ u predSem_eq,j:ℕih:∀ (u : List Bool), stepWord (predIterOf j) u = List.drop j uu:List Boolhfun:(fun x ↦ stepWord (predIterOf j) u) = ![stepWord (predIterOf j) u]h:stepWord (predIterOf (j + 1)) u = predSem ![stepWord (predIterOf j) u]⊢ (stepWord (predIterOf j) u).tail = List.drop j.succ u ih u,j:ℕih:∀ (u : List Bool), stepWord (predIterOf j) u = List.drop j uu:List Boolhfun:(fun x ↦ stepWord (predIterOf j) u) = ![stepWord (predIterOf j) u]h:stepWord (predIterOf (j + 1)) u = predSem ![stepWord (predIterOf j) u]⊢ (List.drop j u).tail = List.drop j.succ u List.tail_dropj:ℕih:∀ (u : List Bool), stepWord (predIterOf j) u = List.drop j uu:List Boolhfun:(fun x ↦ stepWord (predIterOf j) u) = ![stepWord (predIterOf j) u]h:stepWord (predIterOf (j + 1)) u = predSem ![stepWord (predIterOf j) u]⊢ List.drop (j + 1) u = List.drop j.succ u]All goals completed! 🐙)

Prepending a word prepends it to the value a step contributes.

theorem stepWord_prependOf (e : COf 1) (r : List Bool) :
    ∀ u : List Bool, stepWord (prependOf u e) r = u ++ stepWord e r :=
  List.rec rfl (fun b v ih ↦ bye:COf 1r:List Boolb:Boolv:List Boolih:stepWord (prependOf v e) r = v ++ stepWord e r⊢ stepWord (prependOf (b :: v) e) r = b :: v ++ stepWord e r
    change b :: stepWord (prependOf v e) r = _e:COf 1r:List Boolb:Boolv:List Boolih:stepWord (prependOf v e) r = v ++ stepWord e r⊢ b :: stepWord (prependOf v e) r = b :: v ++ stepWord e r
    rw [ihe:COf 1r:List Boolb:Boolv:List Boolih:stepWord (prependOf v e) r = v ++ stepWord e r⊢ b :: (v ++ stepWord e r) = b :: v ++ stepWord e r]e:COf 1r:List Boolb:Boolv:List Boolih:stepWord (prependOf v e) r = v ++ stepWord e r⊢ b :: (v ++ stepWord e r) = b :: v ++ stepWord e r
    rflAll goals completed! 🐙)

Prepending a word to a nullary expression prepends it to the value.

theorem baseWord_prependOf (e : COf 0) :
    ∀ u : List Bool, baseWord (prependOf u e) = u ++ baseWord e :=
  List.rec rfl (fun b v ih ↦ bye:COf 0b:Boolv:List Boolih:baseWord (prependOf v e) = v ++ baseWord e⊢ baseWord (prependOf (b :: v) e) = b :: v ++ baseWord e
    change b :: baseWord (prependOf v e) = _e:COf 0b:Boolv:List Boolih:baseWord (prependOf v e) = v ++ baseWord e⊢ b :: baseWord (prependOf v e) = b :: v ++ baseWord e
    rw [ihe:COf 0b:Boolv:List Boolih:baseWord (prependOf v e) = v ++ baseWord e⊢ b :: (v ++ baseWord e) = b :: v ++ baseWord e]e:COf 0b:Boolv:List Boolih:baseWord (prependOf v e) = v ++ baseWord e⊢ b :: (v ++ baseWord e) = b :: v ++ baseWord e
    rflAll goals completed! 🐙)

The constant word is the base it contributes.

theorem baseWord_constAtOf (u : List Bool) : baseWord (constAtOf 0 u) = u :=
  (baseWord_prependOf (zeroAtOf 0) u).trans (List.append_nil u)

The constant word is the value a step contributes, whatever it reads.

theorem stepWord_constAtOf (u r : List Bool) :
    stepWord (constAtOf 1 u) r = u :=
  (stepWord_prependOf (zeroAtOf 1) r u).trans (List.append_nil u)

The diagonal reads its argument in both positions.

theorem stepWord_diagOf (e : COf 2) (u : List Bool) :
    stepWord (diagOf e) u = semAt 2 e.1.1 e.2 ![u, u] := bye:COf 2u:List Bool⊢ stepWord (diagOf e) u = semAt 2 ↑↑e ⋯ ![u, u]
  have hfun : (fun _ : Fin 2 ↦ u) = ![u, u] :=
    funext fun i ↦ match i with | 0 => rfl | 1 => rfle:COf 2u:List Boolhfun:(fun x ↦ u) = ![u, u]⊢ stepWord (diagOf e) u = semAt 2 ↑↑e ⋯ ![u, u]
  exact congrArg (semAt 2 e.1.1 e.2) hfunAll goals completed! 🐙

endend Cobham