定义同类型多个函数的高效方法

Great question! Duplicating parameter signatures across related predicates (like your metric axioms) is a classic example of redundant code that’s error-prone and hard to maintain—let’s fix this with idiomatic Coq patterns.

Option 1: Extract a Reusable Predicate Type #

First, we can define a generic type that captures the common structure of all your metric predicates: every predicate takes a type X and a distance function d : X -> X -> R, then returns a proposition.

(* Define a reusable type for metric predicates *)
Definition MetricPred (X : Type) := (X -> X -> R) -> Prop.

Now you can use this type to define your specific metric conditions without repeating the boilerplate parameter setup:

Definition metric_non_negative : forall {X : Type}, MetricPred X :=
  fun {X} d => forall x y : X, d x y >= 0.

Definition metric_identical_arguments : forall {X : Type}, MetricPred X :=
  fun {X} d => forall x y : X, d x y = 0 <-> x = y.

This cuts out the duplicated {X : Type} (d : X -> X -> R) lines entirely. If you ever need to adjust the signature of the distance function (e.g., switch from R to another ordered field), you only have to update the MetricPred definition once.

Option 2: Use a Record for Structured Metric Axioms #

Since metric spaces have a fixed set of axioms (non-negativity, identity of indiscernibles, symmetry, triangle inequality), a more idiomatic approach in Coq is to wrap all these conditions into a single Record type. This aligns perfectly with the mathematical definition of a metric space and eliminates redundancy entirely:

Record Metric (X : Type) : Type := {
  dist : X -> X -> R;  (* The core distance function *)
  dist_non_neg : forall x y : X, dist x y >= 0;
  dist_zero_iff_eq : forall x y : X, dist x y = 0 <-> x = y;
  dist_sym : forall x y : X, dist x y = dist y x;
  dist_triangle : forall x y z : X, dist x z <= dist x y + dist y z
}.

Now, instead of defining separate predicates, you have a single type Metric X that represents all valid metrics on X. If you need to reference an individual axiom (like non-negativity), you can use the record projection: e.g., dist_non_neg my_metric where my_metric : Metric X.

This approach is especially useful if you’re going to work with metric spaces extensively—it keeps all related axioms grouped, makes proofs cleaner, and avoids scattered predicate definitions.

Bonus: Shorten with Implicit Wrappers #

If you prefer to keep individual predicate definitions but want even less boilerplate, you can use a simple higher-order wrapper with implicit parameters:

Definition for_metric {X : Type} (P : (X -> X -> R) -> Prop) := P.

(* Define your predicates concisely *)
Definition metric_non_negative := for_metric (fun d => forall x y, d x y >= 0).
Definition metric_identical_arguments := for_metric (fun d => forall x y, d x y = 0 <-> x = y).

Coq’s implicit argument mechanism will automatically infer the X parameter when you use these predicates, so you don’t have to specify it manually.

All these approaches eliminate the copy-paste redundancy you’re trying to avoid, making your code more maintainable and aligned with good Coq programming practices.

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