无需选择公理在Coq中实现存在唯一性公理的见证函数及相关证明求解

First, let's address your core questions: your initial setup is reasonable, and the uniqueness axiom (uniq_axiom) isn't strictly needed for this existence proof (though it will be critical if you later want to show your fn is unique). Let's walk through the proof step-by-step, and also clarify the intensional vs extensional equality question.

1. Intensional vs Extensional Equality: Is Your Axiom Too Strict? #

Your exist_axiom uses intensional equality (=) for functions, which in Coq means the function terms are syntactically identical (up to conversion). For most mathematical purposes, extensional equality (two functions are equal if they return equal results for all inputs) is more natural.

If you want to adjust to extensional equality, you'd rewrite exist_axiom like this:

exist_axiom : forall (f : subset -> set), exists (x : set), forall (y : subset), f y = op (subset_incl y) x ;

And uniq_axiom would similarly use extensional equality for the function equality premise. However, your current intensional axiom is stronger (it implies extensional equality), so we can work with it as-is for now.

2. Completing the witness_fcn Proof #

You've already laid the groundwork by defining fn using the witness from exist_axiom. Here's how to finish the proof, with explanations for each step:

First, you'll need to import functional extensionality (to connect pointwise equality to function equality) if you don't have it already:

Require Import Coq.Logic.FunctionalExtensionality.

Now, let's finish the proof:

Definition witness_fcn : forall (M : MRE), forall (f : set M -> set M), exists (fn : set M -> set M), forall (x : subset M), (fun y => f (op M (subset_incl M x) y)) = (fun y => op M (subset_incl M x) (fn y)).
Proof.
  intros M f.
  pose (fn0 := fun y => exist_axiom M (fun x => f (op M (subset_incl M x) y))).
  exists (fun y => ex_proj1 (fn0 y)).
  intros x.
  unfold fn0.
  (* Reduce function equality to pointwise equality via functional extensionality *)
  apply functional_extensionality.
  intros y.
  (* Define the function we'll apply exist_axiom to *)
  pose (g := fun x' => f (op M (subset_incl M x') y)).
  (* Extract the witness x0 from exist_axiom for g *)
  destruct (exist_axiom M g) as [x0 Hg].
  (* Hg gives us intensional equality between g and the op-based function *)
  rewrite Hg.
  (* x0 is exactly the projection of exist_axiom M g, so both sides are identical *)
  reflexivity.
Qed.

Key Steps Explained: #

• Functional Extensionality: We use functional_extensionality to turn the goal of proving two functions are equal into proving they return equal results for every y—this is a standard axiom in Coq for working with function equality.
• Destructing exist_axiom: The destruct tactic pulls out the witness x0 guaranteed by exist_axiom for our function g. The hypothesis Hg confirms g is intensionally equal to fun x' => op (subset_incl x') x0.
• Rewrite and Reflexivity: Rewriting with Hg replaces g x with op (subset_incl x) x0, and since x0 is exactly the projection of exist_axiom M g, the two sides are syntactically identical—reflexivity closes the goal.

3. When Does uniq_axiom Come Into Play? #

You haven't needed uniq_axiom yet because this is an existence proof. However, if you later want to prove that the fn you constructed is unique (i.e., if there's another function fn' satisfying the same property, then fn = fn'), uniq_axiom will be essential—it guarantees that the witness from exist_axiom is the only one that works, so you can use it to show fn and fn' must be equal.

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