代码之家 › 专栏 › 技术社区 › Siddharth Bhat

“嵌套”匹配的正确实例

coq-tactic coq

Siddharth Bhat · 技术社区 · 7 年前

我有一个形式的引理 FnEquivInner f g 暗示 outer t (bind t f) === outer t (bind t g) (下面是完整的示例)。

我想知道 Proper 我需要为之写作的实例 outer 让我表演 rewrite 在这种情况下,替换 f 具有 g 在召唤中 外面的 .

一般来说,一个人怎么写? 适当的 模式不平凡的实例?

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.

1 回复 | 直到 7 年前

Jason Gross 7 年前

如果你 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_重写 通过。

不过,我想你会想要

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

如果我写这个,那么 SooIDIDR重写 失败。让我们再仔细检查一下类型日志,这次寻找应用后出错的地方。 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.

然后 SooIDIDR重写 再次通过。

注意,你必须填写 ? -前缀关系( ?R , ?r 等)你有任何自反关系。

你可能会问“为什么这个黑魔法有用?”答案是 本子关系 是COQ通常出错的地方。大致上,这意味着,“我的数据库中没有与您要查找的内容匹配的内容;让我盲目地尝试数据库中的所有内容,看看其中是否有任何内容足够接近可以工作。”*(其中“足够接近”意味着“是的子关系”。)因此,我们查找coq在其搜索中出错的位置,并在该位置之前立即查看以查看是什么它在看。(通常有许多步骤 partial_application_tactic ,将参数从函数中删除;这就是为什么只需要一个 适当的 实例为 bind ,而不是一个 bind t 另一个是为了 fun t => bind t f )

*有时候这很有用,因为 eq 是每一个自反关系的子关系,所以你可以在不使用关系的时候使用。 情商 。但大多数时候, 本子关系 不是你想要的。