Coq函数式编程证明中函数扩展性的困扰及解决方案咨询

Hey there! I totally get where you're coming from—dealing with functional extensionality (funext) in Coq when working with function-heavy constructs like optics, state monads, or even custom monad classes can feel like wading through endless boilerplate. Let's walk through some practical, actionable strategies to make this process way smoother.

Start with Coq's Built-In Tools for Quick Wins #

Coq has built-in support for functional extensionality that you can leverage with minimal setup:

• First, import the core funext axiom with Require Import Coq.Logic.FunctionalExtensionality.
• Use the extensionality tactic to automatically reduce a function equality goal f = g to forall x, f x = g x. This is a huge time-saver—no more manually applying the functional_extensionality axiom every time.

For example, if you're proving a monad law that requires showing two bind expressions are equal:

Require Import Coq.Logic.FunctionalExtensionality.

Class Monad (m : Type -> Type) := {
  ret : forall {X}, X -> m X ;
  bind : forall {A B}, m A -> (A -> m B) -> m B ;
  bind_ret : forall {A B} (a : A) (f : A -> m B), bind (ret a) f = f a
}.

Lemma bind_assoc_simpl {m} {Monad m} {A B C} (ma : m A) (f : A -> m B) (g : B -> m C) :
    bind (bind ma f) g = bind ma (fun a => bind (f a) g).
Proof.
  intros.
  extensionality x.  (* Reduces the function equality to point-wise equality *)
  (* Now you can focus on proving the equality for a specific x, using your monad laws *)
Abort.

Leverage Setoid Rewriting for Complex Equivalences #

When working with nested functions or custom algebraic structures (like optics), setoid rewriting lets you work with functional equivalence (i.e., forall x, f x = g x) as a first-class relation, avoiding repetitive funext steps.

Here's how to set it up:

Require Import Coq.Setoids.Setoid.

(* Define a reusable functional equivalence relation *)
Definition func_eq {A B : Type} (f g : A -> B) := forall x, f x = g x.

(* Register it as a setoid relation (reflexive, symmetric, transitive) *)
Add Parametric Relation {A B} : (A -> B) func_eq
  reflexivity proved by (fun f x => eq_refl)
  symmetry proved by (fun f g H x => eq_sym (H x))
  transitivity proved by (fun f g h H1 H2 x => eq_trans (H1 x) (H2 x))
  as func_rel.

Now you can use setoid_rewrite to replace functions with their equivalents directly. For example, if you have H : func_eq f g, you can run setoid_rewrite H to swap f with g in your goal—Coq automatically handles the extensionality under the hood.

Use the Equations Library to Automate Extensibility #

The Equations library is a game-changer for function-centric proofs. It automatically handles many extensibility concerns when you define recursive or dependent functions, and generates proof obligations that play nicely with funext.

After installing Equations, you can use it to define your monad (or optics) and streamline proofs:

From Equations Require Import Equations.

Class Monad (m : Type -> Type) := {
  ret : forall {X}, X -> m X ;
  bind : forall {A B}, m A -> (A -> m B) -> m B ;
  bind_ret : forall {A B} (a : A) (f : A -> m B), bind (ret a) f = f a
}.

(* Equations' tactics like `rewrite` or `refine` automatically account for function extensionality *)
Lemma bind_compose {m} {Monad m} {A B C} (f : A -> m B) (g : B -> m C) :
    bind (fun a => f a) g = fun a => bind (f a) g.
Proof.
  intros.
  funext.  (* Equations makes this step even more seamless, but it's still optional *)
  apply bind_ret.
Qed.

Abstract Common Funext Patterns into Lemmas #

If you find yourself repeating the same funext-based reasoning (e.g., proving that a monadic operation preserves function equality), turn those patterns into reusable lemmas. This cuts down on boilerplate and makes your proofs more readable.

For example:

Lemma bind_preserves_func_eq {m} {Monad m} {A B C} (f : A -> m B) (g1 g2 : B -> m C) :
    (forall b, bind (f b) g1 = bind (f b) g2) ->
    bind (fun a => f a) g1 = bind (fun a => f a) g2.
Proof.
  intros H.
  funext.
  apply H.
Qed.

Now, whenever you need this specific pattern, just apply bind_preserves_func_eq instead of redoing the funext step manually.

For Heavy-Duty Proofs: Try HoTT Foundations #

If you're working on deeply function-centric projects (like formalizing optics or advanced monad theory), consider switching to Coq's Homotopy Type Theory (HoTT) library. In HoTT, functional extensionality isn't an axiom—it's a theorem built into the type theory. This means you get extensionality for free, without needing to import extra axioms or write boilerplate. The tradeoff is a learning curve, but it's worth it for long-term proof efficiency.

内容的提问来源于stack exchange，提问作者neutropolis