setoid_rewrite在模式匹配场景下失效的技术求助（附Monoid示例）

Hey there! I totally get where you're stuck with setoid_rewrite not playing nice with functional extensionality in your Monoid setup. Let's walk through why this happens and how to fix it step by step.

The Root of the Problem #

When you add pointwise_eq_ext (pointwise equality extensionality) to your context, setoid_rewrite needs two key things to work with function-type Monoids:

1. A Setoid instance that defines what "equality" means for functions (pointwise equivalence, in your case).
2. Proper instances to confirm your Monoid operations (mappend/* and mzero) respect this equivalence relation.

Without these, Coq can't figure out how to apply rewrite rules across function types using setoid equality.

Step 1: Define the Pointwise Setoid for Functions #

First, we need to tell Coq that two functions are equivalent if they produce equivalent results for every input. Here's how to define that Setoid instance:

Instance pointwise_setoid (A : Type) (B : Type) `{Setoid B} : Setoid (A -> B) := {
  equiv := fun f g => forall x, f x ≈ g x;
  Equivalence_equiv := {|
    Equivalence_Reflexive := fun f x => reflexivity;
    Equivalence_Symmetric := fun f g H x => symmetry (H x);
    Equivalence_Transitive := fun f g h H1 H2 x => transitivity (H1 x) (H2 x)
  |}
}.

This instance formalizes the pointwise equivalence you're relying on with pointwise_eq_ext.

Step 2: Prove Monoid Operations Are Proper #

setoid_rewrite requires that operations preserve the setoid equivalence. We need to prove this for both mappend and mzero:

For mappend (*):

Instance mappend_proper `{Monoid (A -> B)} `{Setoid B} :
  Proper (equiv ==> equiv ==> equiv) mappend.
Proof.
  intros f1 f2 Hf g1 g2 Hg x.
  unfold equiv in *.
  rewrite Hf, Hg.
  reflexivity.
Qed.

This confirms that if f1 ≈ f2 and g1 ≈ g2, then f1 * g1 ≈ f2 * g2 (pointwise, of course).

For mzero:

Instance mzero_proper `{Monoid (A -> B)} `{Setoid B} :
  Proper (equiv) mzero.
Proof.
  intros x. reflexivity.
Qed.

This ensures mzero (when it's a constant function) is equivalent to itself across all inputs.

Step 3: Link Functional Extensionality to Setoid Equivalence #

Your pointwise_eq_ext axiom connects pointwise propositional equality to function equality. We need to tie this to our setoid equivalence so setoid_rewrite can use it:

Lemma pointwise_equiv_eq `{Setoid B} (f g : A -> B) :
  (forall x, f x = g x) <-> f ≈ g.
Proof.
  split; intros H.
  - intro x; apply H.
  - intro x; apply H.
Qed.

This lemma lets you switch between propositional equality and setoid equivalence whenever you need to apply functional extensionality during rewrites.

Step 4: Use setoid_rewrite Successfully #

Let's put it all together with a concrete example. Suppose we have a Monoid over functions A -> B (where B is a Monoid), and we want to rewrite using the left_unit law:

Context {A : Type} {B : Type} `{Monoid B} `{MonoidLaws B} `{Setoid B}.

-- Define the function Monoid instance
Let monoid_fun := @Monoid (A -> B) {|
  mzero := fun _ => mzero;
  mappend := fun f g x => f x * g x
|}.

-- Prove the left unit law for this function Monoid
Let monoid_laws_fun : MonoidLaws (A -> B) := {|
  left_unit := fun f x => left_unit (f x)
|}.

-- Now we can use setoid_rewrite!
Lemma test (f : A -> B) : mzero * f ≈ f.
Proof.
  setoid_rewrite left_unit.
  reflexivity.
Qed.

Here, setoid_rewrite left_unit works because Coq recognizes it can apply the left_unit law pointwise across the function, thanks to our Setoid and Proper instances.

Key Takeaway #

The main issue was missing the infrastructure to let Coq understand how equality works for function-type Monoids. By defining the pointwise Setoid, proving operations are Proper, and linking to functional extensionality, you unlock setoid_rewrite for these scenarios.

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