関数と structure: funext と ext

関数の等式は，すべての入力で値が等しいことを示せば証明できます． この原理を関数外延性と呼び，Lean では funext を使います．

example (f g : Nat → Nat) (h : ∀ x : Nat, f x = g x) : f = g := by
  funext x
  exact h x

structure についても，field ごとの等式から structure 全体の等式を示すことがあります． @[ext] を付けておくと，ext tactic が使う外延性補題が生成されます．

@[ext]
structure PointForExt where
  x : Nat
  y : Nat

example (p q : PointForExt) (hx : p.x = q.x) (hy : p.y = q.y) : p = q := by
  ext
  · exact hx
  · exact hy

演習

funext を使って，点ごとの等式から関数の等式を証明してください．

example (f g : Nat → Nat) (h : ∀ n : Nat, f n = g n) : f = g := by
  sorry