"nested" 匹配的正确实例

Question

我有一个形式为 FnEquivInner f g 的引理 outer t (bind t f) === outer t (bind t g)（下面发布了完整示例）。

我想了解我需要为 outer 编写什么样的 Proper 实例，让我在这种情况下执行 rewrite，以将 f 替换为g 在 outer 的调用中。

一般来说，如何编写 Proper 个模式不平凡的实例？

Require Import Setoid.
Require Import Morphisms.

Section PROPERINSTANCE.

  Variable T: Type.
  Variable inner:  T -> (T -> T) -> T.
  Variable outer : T -> (T -> T)  -> T.
  Variable bind: T -> (T -> T) -> (T -> T).

  Variable equiv: T -> T -> Prop.
  Infix "===" := equiv (at level 50).

  Variable equivalence_equiv: Equivalence equiv.

  (** Check that equivalence can be found by Coq *)
  Lemma check_equiv_refl: forall (t: T), t === t.
    reflexivity.
  Qed.

  Definition FnEquivInner (f g: T -> T): Prop := forall (t: T),
      inner t f === inner t g.

  (** This is a part of my theory *)
  Variable FnEquivOuter:
    forall (f g: T -> T)
      (t t1: T)
      (EQUIVINNER: FnEquivInner f g),
      outer t1 (bind t f) === outer t1 (bind t g).

  (** This is not a made up example to push coq, I have an actual theorem like this:
   * https://github.com/bollu/vellvm/blob/master/src/coq/Memory.v#L923
     inner = memEffect
     outer = memD
     bind = bindM
   *)


  Lemma useFnEquivOuter:
    forall (f g: T -> T)
      (t: T)
      (EQUIVINNER: FnEquivInner f g),
      outer t (bind t f) === outer t (bind t g).
  Proof.
    intros.
    (** What should the Proper instance look like so that if I have a FnEquivInner witness,
  I can `rewrite` using it? *)
    setoid_rewrite EQUIVINNER.
  Qed.

End PROPERINSTANCE.

Answer 1

如果您 Set Typeclasses Debug. 然后 try setoid_rewrite EQUIVINNER，并查找包含 looking for 的行，这些行紧接在提到 proper_subrelation 的行之前，您将看到

Debug: 1.1-1: looking for (Proper (?R ==> FnEquivInner ==> ?r) bind) with backtracking
Debug: 1.1-1.2-2.1-1: looking for (Proper (?R --> FnEquivInner --> Basics.flip ?r) bind) with backtracking
Debug: 1.3-2.1-1: looking for (Proper (FnEquivInner --> Basics.flip ?r) (bind t)) with backtracking

这基本上是 Proper 个实例的列表，您可以添加这些实例来为 setoid_rewrite 进行类型类解析。

例如，如果我写

Global Instance: Proper (eq ==> FnEquivInner ==> eq) bind. Admitted.

然后 setoid_rewrite 通过。

不过，我假设您会想要类似

的东西

Global Instance bind_Proper : Proper (eq ==> FnEquivInner ==> FnEquivInner) bind. Admitted.

如果我这样写，那么 setoid_rewrite 就会失败。让我们再次挖掘 typeclass 日志，这次是寻找在应用 bind_Proper 后分辨率出错的地方。按照与上面相同的规则，我们看到符合上述条件的第一行是

Debug: 2.1-1: looking for (Proper (?R ==> FnEquivInner ==> ?r) outer) with backtracking

如果我加上

Global Instance outer_Proper: Proper (eq ==> FnEquivInner ==> equiv) outer. Admitted.

然后 setoid_rewrite 再次通过。

请注意，您可以使用任何您喜欢的自反关系来填充 ? 前缀关系（?R、?r 等）。

你可能会问 "why does this black magic work?" 答案是 proper_subrelation 是 Coq 通常出错的地方。粗略地说，这意味着 "I have nothing in my database matching what you're looking for; let me blindly try everything in my database and see if any of them are maybe close enough to work."*（其中 "close enough" 意味着 "is a subrelation of"。）所以我们寻找 Coq 在其搜索中出错的地方，我们紧接着在那之前查看它是什么正在看。（partial_application_tactic 通常有很多步骤，它从函数中剥离参数；这就是为什么 bind 只需要一个 Proper 实例，而不是 bind t 和另一个 fun t => bind t f.)

*有时这实际上很有用，因为 eq 是每个自反关系的子关系，因此当您可以只使用 eq 时，您可以不用输入关系。但大多数时候，proper_subrelation并不是你想要的。

"nested" 匹配的正确实例

Proper instance for "nested" matching

coq

coq-tactic