setoid_rewrite 模式匹配场景失败

Question

，我被告知如何用setoid_rewrite对付functional_extensionality。不幸的是，我已经发现这个不错的解决方案在以下情况下不起作用。认为我们定义了 Monoid class:

Class Monoid (m : Type) :=
{ mzero : m
; mappend : m -> m -> m
}.
Notation "m1 * m2" := (mappend m1 m2) (at level 40, left associativity).

Class MonoidLaws m `{Monoid m} :=
{ left_unit  : forall m, mzero * m = m (* ; other laws... *) }.

如果我们在里面加上图片，monoid_proof变得微不足道：

Require Import Coq.Logic.FunctionalExtensionality.
Require Import Coq.Setoids.Setoid.
Require Import Coq.Classes.Morphisms.

Generalizable All Variables.

Instance pointwise_eq_ext {A B : Type} `(sb : subrelation B RB eq)
  : subrelation (pointwise_relation A RB) eq.
Proof.
  intros f g Hfg.
  apply functional_extensionality.
  intro x.
  apply sb.
  apply (Hfg x).
Qed.

Example monoid_proof `{ml : MonoidLaws m} :
  (fun m => mzero * m) = (fun m => m).
Proof. now setoid_rewrite left_unit. Qed.

但是，如果相同的幺半群表达式作为 option_fold 的参数出现，策略失败：

Definition option_fold {A B} (some : A -> B) (none : B) (oa : option A) : B :=
  match oa with
  | Some a => some a
  | None => none
  end.

(* Expression is an argument for [option_fold] *)
Example monoid_proof' `{ml : MonoidLaws m} :
  forall om,
    option_fold (fun m => mzero * m) mzero om = option_fold (fun m => m) mzero om.
Proof. intros. now setoid_rewrite left_unit. (* error! *) Qed.

我不熟悉 setoid_rewrite 的细节，但似乎模式匹配符合阻止此策略的上下文正确执行。有什么办法教教setoid_rewrite如何处理这种情况？我一直在尝试提供几个 subrelation 实例，但我缺乏理解整体的理论背景图片。一个通用的解决方案会很棒，但我会很高兴有一个特别重写参数中表达式的方法（嵌套） option_fold.

的调用

Answer 1

pointwise_eq_ext 实例让您可以像这样重写目标：

(fun m => mzero * m) = (fun m => m)

但是如果您在某些上下文中使用您的函数，事情就会中断。要解决此问题，您需要添加以下子关系：

Instance subrel_eq_respect {A B : Type}
         `(sa : subrelation A RA eq)
         `(sb : subrelation B eq RB) :
   subrelation eq (respectful RA RB).
Proof. intros f g -> a a' Raa'. apply sb. f_equal. apply (sa _ _ Raa'). Qed.

您可能想看看 Matthieu Sozeau 在 this Coq Club post 中的完整代码。

setoid_rewrite 模式匹配场景失败

setoid_rewrite fails in pattern matching scenario

pattern-matching

substitution

coq