06.3 依賴型別：當型別可以依賴於值的時候#

-- Lean 4：加法交換律，證明就是一個「型別為定理」的項
theorem add_comm (n m : ℕ) : n + m = m + n := by
  induction n with
  | zero => simp
  | succ k ih => simp [Nat.succ_add, ih]
-- 這段「程式」通過型別檢查 = 定理被形式化證明
-- 註：Lean 中 `n + m = m + n` 本身就是一個型別（Eq 是歸納型別）！

-- 「長度 n 的向量」：依賴型別的招牌例子
inductive Vec (α : Type) : Nat → Type where
  | nil  : Vec α 0
  | cons : α → {n : Nat} → Vec α n → Vec α (n + 1)

-- 「安全取第 i 項」：i < n 這個**數學條件**直接寫進型別
def safeGet {α : Type} {n : Nat} (v : Vec α n) (i : Nat) (h : i < n) : α :=
  match v, i, h with
  | Vec.cons x _,  0,      _ => x
  | Vec.cons _ xs, i + 1,  _ => safeGet xs i (Nat.lt_of_succ_lt_succ h)
-- 呼叫 safeGet v 5 h 時，h : 5 < n 必須在編譯期存在：
-- 越界不再是執行期異常，而是型別錯誤！

# 對照：Python 只能「執行期檢查 + 型別註記閹割版」
from typing import Generic, TypeVar, NewType

T = TypeVar("T")
Length = NewType("Length", int)

class Vec(Generic[T]):
    def __init__(self, items: list[T]):
        self.items = items
    def __len__(self) -> int:
        return len(self.items)

def safe_get(v: Vec[T], i: int) -> T:
    # 長度條件無法進入型別；只能執行期檢查
    if i >= len(v.items):
        raise IndexError(f"index {i} out of range for length {len(v.items)}")
    return v.items[i]
# 差距一目了然：依賴型別把「if 檢查」搬進了型別系統

-- 矩陣乘法：只有「內維吻合」的呼叫能通過編譯
def matMul {m n p : Nat} (A : Mat m n) (B : Mat n p) : Mat m p := ...
-- matMul A B 若 A 的行數 ≠ B 的列數，根本型別不合
-- 對照 NumPy：shape mismatch 是執行期 ValueError

-- 「質數」作為型別：{ p : Nat // IsPrime p }（子型別/refinement）
def IsPrime : Nat → Prop
  | 0 | 1 => False
  | p => p ≥ 2 ∧ ∀ d, d ∣ p → d = 1 ∨ d = p

def Prime : Type := { p : Nat // IsPrime p }

-- 函數「給定任意 n > 1，存在質數 p > n」（歐幾里得）
theorem exists_prime_gt : ∀ n : Nat, ∃ p, p > n ∧ IsPrime p := ...
-- ∃ 是 Σ 型的 Prop 版；∀ 是 Π 型——邏輯連接詞全部成為型別構造子

-- 當型別可以依賴值，「所有型別的型別」= 宇宙（universe）
-- 但 Type : Type 會重建羅素悖論（Girard 悖論，1972）！
-- 解法：層級宇宙——這正是 04.3 羅素分層的再現
#check (Type 0 : Type 1)   -- Type 0 是 Type 1 的元素，但不包含自身

-- 已排序陣列的二分查找：回傳「要嘛找到（帶索引），要嘛證明不存在」
inductive FindResult (a : Type) (xs : Array a) (target : a) : Type where
  | found : (i : Nat) → (i < xs.size) → xs[i] = target → FindResult a xs target
  | notFound : (∀ i, (h : i < xs.size) → xs[i] ≠ target) → FindResult a xs target
-- 這個和型的兩個分支各自攜帶「證明」：
-- found 帶「這個索引真的是目標」的證明
-- notFound 帶「任何索引都不是」的證明——不可能出現「沒找到但其實在」的 bug

def binary_search(xs: list[int], target: int) -> int | None:
    """回傳 target 的索引，不存在則 None。
    註解說「不存在則 None」——但編譯器不知道，只有測試知道。
    依賴型別版本（上方 Lean）把這句話變成型別的一部分。"""
    lo, hi = 0, len(xs)
    while lo < hi:
        mid = (lo + hi) // 2
        if xs[mid] == target: return mid
        if xs[mid] < target:  lo = mid + 1
        else:                 hi = mid
    return None