CoeDep 使用例：正の自然数から自然数への型強制

match 式でありえないケースを自動的に排除できる例でもある。

/-- 正の自然数 -/
abbrev PosNat := { x : Nat // x > 0}

-- def PosNat.ofNat (n : Nat) (h : n > 0 := by omega) : PosNat := ⟨n, h⟩

def PosNat.ofSucc (n : Nat) : PosNat := ⟨n + 1, by omega⟩

instance (n : Nat) : CoeDep Nat (.succ n) PosNat where
  coe := PosNat.ofSucc n

/-- 正の自然数に対して定義された等比数列 -/
def geomseq (r : Nat) (x : PosNat) : Nat :=
  match x with
  | ⟨1, _⟩ => 1
  | ⟨n + 2, h⟩ => r * geomseq r ⟨n + 1, by omega⟩

-- 数値リテラルをそのまま入れると OfNat がないのでエラーになるが…
#check_failure geomseq 3 4

-- Nat → PosNat という依存型強制は定義できている！
#guard
  let four : Nat := 4
  geomseq 3 four = 27

Start by locating the repository’s existing Lean example entry point and checking how similar examples are organized. Use the issue’s PosNat, CoeDep, geomseq, #check_failure, and #guard example as the reference, and consider the work done when the example is incorporated in the project’s expected format and its checks pass.