induction principle 的生成

這裡參考的是 Code Generation for Higher Inductive Types 中的紀錄

首先我們規範 inductive data types 的 form 如下

\begin{aligned} \text{data } &D (a_1 : A_1) \dots (a_n : A_n) : I_1 \to \cdots \to I_m \to \text{Type where} \\ &c_1 : \Delta_1 \to D\ a_1 \dots a_n\ e_{11} \dots e_{1m} \\ &\dots \\ &c_r : \Delta_r \to D\ a_1 \dots a_n\ e_{r1} \dots e_{rm} \end{aligned}

我們會生成以下形式的 induction principle

\begin{aligned} D_{ind} &: (a_1 : A_1) \to \dots \to (a_n : A_n) \\ &\to (i_1 : I_1) \to \dots \to (i_m : I_m) \\ &\to (\text{target} : D\ a_1 \dots a_n\ i_1 \dots i_m) \\ &\to (C : (i_1 : I_1) \to \dots \to (i_m : I_m) \to D\ a_1 \dots a_n\ i_1 \dots i_m \to \text{Type}) \\ &\to (f_1 : \Delta_1' \to C\ e_{11} \dots e_{1m} (c_1\ \Delta_1) \\ & \dots \\ &\to (f_r : \Delta_r' \to C\ e_{r1} \dots e_{rm} (c_r\ \Delta_r) \\ &\to C\ i_1 ... i_m\ \text{target} \end{aligned}

$a_i$ 跟 $i_j$ 的差別就是， $i_j$ 涉及到使用者可以實例化的部分，比如

data Vec (A : Type) : Nat -> Type where
  nil : Vec A 0
  cons : {n : Nat} -> A -> Vec A n -> Vec A (suc n)

這個案例中的 $a_1 : A_1$ 就是 A : Type，而 $i_1 : I_1$ 是 _ : Nat。這裡 nil 的 $\Delta$ 是空的，而 cons 的 $\Delta$ 是 {n : Nat}, (_ : A), (_ : Vec A n)。

而 $e_{ij}$ 分別是 0 跟 suc n，這就是使用者可以選擇不同 witness 填入的部分。

在 $\Delta$ 的生成部分可以看到特定標記成了 $\Delta'$ ，這個意思是說

如果 $(y : B) \in \Delta$ 而且 $B = D\ a \dots e \dots$ ，那 $\Delta'$ 中應該生成 (y : B), (y' : C e ... y)
如果 $(y : B) \in \Delta$ 而且 $B = \psi \to D\ a \dots e \dots$ ，那 $\Delta'$ 中應該生成 (y : B), (y' : Ψ -> C e ... (y Ψ))
除此之外 $\Delta'$ 只需要把 $\Delta$ 中的 binding $(y : B)$ 複製一遍就好了

所以 Vec 得到的 induction principle 就應該是

Vec.ind : (A : Type) -> (i : Nat) -> (target : Vec A i)
        -> (C : (i : Nat) -> D A i -> Type)
        -> (case_nil : C 0 nil)
        -> (case_cons : {n : Nat}
                        -> (a : A)
                        -> (as : Vec A n)
                        -> (as' : C n as)
                        -> C (suc n) (cons {n} a as))
        -> C i target