附錄 C：Lean / Haskell 基礎小範例速查#

-- 命題 P -> Q 的證明，就是一個函數
modusPonens :: (P -> Q) -> P -> Q
modusPonens f p = f p

-- 「且」的消去律
proj1 :: (a, b) -> a
proj1 (a, _) = a

-- 「或」的引入律
introLeft :: a -> Either a b
introLeft a = Left a

-- 分配律：(A and (B or C)) -> ((A and B) or (A and C))
distrib :: (a, Either b c) -> Either (a, b) (a, c)
distrib (a, Left b)  = Left (a, b)
distrib (a, Right c) = Right (a, c)

data Nat = Z | S Nat

data List a = Nil | Cons a (List a)

data Tree a = Leaf | Node (Tree a) a (Tree a)

-- fold 的型別（初始代數的消去子）
foldr :: (a -> b -> b) -> b -> [a] -> b
foldr f z []     = z
foldr f z (x:xs) = f x (foldr f z xs)

class Functor f where
  fmap :: (a -> b) -> f a -> f b

class Functor f => Applicative f where
  pure  :: a -> f a
  (<*>) :: f (a -> b) -> f a -> f b

class Applicative f => Monad f where
  (>>=) :: f a -> (a -> f b) -> f b

data Maybe a = Nothing | Just a

instance Functor Maybe where
  fmap _ Nothing  = Nothing
  fmap g (Just x) = Just (g x)

instance Monad Maybe where
  return = Just
  Nothing  >>= _ = Nothing
  Just x   >>= f = f x

safeDiv :: Int -> Int -> Maybe Int
safeDiv _ 0 = Nothing
safeDiv x y = Just (x `div` y)

-- 錯誤處理的鏈式合成
example :: Maybe Int
example = safeDiv 10 2 >>= safeDiv 5

newtype State s a = State { runState :: s -> (a, s) }

instance Monad (State s) where
  return a = State $ \s -> (a, s)
  m >>= f  = State $ \s ->
    let (a, s') = runState m s
    in runState (f a) s'

curry :: ((a, b) -> c) -> a -> b -> c
curry f a b = f (a, b)

uncurry :: (a -> b -> c) -> (a, b) -> c
uncurry f (a, b) = f a b

-- 恆等函數
def id' (a : Nat) : Nat := a

-- 簡單定理
theorem add_zero (n : Nat) : n + 0 = n := by simp

theorem add_comm_proof (n m : Nat) : n + m = m + n := by
  rw [Nat.add_comm]

-- 依賴型別：向量長度在型別中
inductive Vec (α : Type) : Nat → Type where
  | nil : Vec α 0
  | cons : α → Vec α n → Vec α (n + 1)

-- head 的型別保證不會出界
def Vec.head : Vec α (n + 1) → α
  | .cons x _ => x

-- ∀ 的證明就是一個（依賴）函數
example : ∀ n : Nat, n = n := fun n => rfl

-- ∃ 的證明是「一個值 + 一個性質證明」
example : ∃ n : Nat, n * n = 25 := ⟨5, rfl⟩

def add : Nat → Nat → Nat
  | 0,     m => m
  | n + 1, m => (add n m) + 1

theorem add_zero' (n : Nat) : add n 0 = n := by
  induction n with
  | zero => rfl
  | succ k ih => rw [add, ih]

-- 在 Lean 中，本書第一篇的所有邏輯恆等式都能機器檢查
theorem and_distrib (A B C : Prop) :
    A ∧ (B ∨ C) → (A ∧ B) ∨ (A ∧ C) := by
  intro ⟨a, bOrC⟩
  match bOrC with
  | .inl b => exact .inl ⟨a, b⟩
  | .inr c => exact .inr ⟨a, c⟩