1

我不能将 Ssreflect 的重写与 setoid 一起使用。虽然我认为这些信息与解决问题无关，但我在 coq 中使用了这种类别理论的表述：https ://github.com/jwiegley/category-theory 。

据我所知，如果RewriteRelation可以解析出合适的Typeclass实例，Ssreflect的重写可以使用用户定义的等价关系。

Context { x y : obj[C]}.

About RewriteRelation.
(* ∀ A : Type, crelation A → Prop *)

Instance equivrw : (@RewriteRelation (x ~> y) (@equiv (x ~> y) (homset x y))) := {}. (* defined and correctly type-checked *)
About equivrw.
(* RewriteRelation equiv (coq omits implicit arguments) *)

Lemma test_rwrel (a b c : x ~> y) : (@equiv (x ~> y) (homset x y) a b) -> (@equiv (x ~> y) (homset x y)  b c) -> (@equiv (x ~> y) (homset x y) a c).
Proof.
    move => ->.
    (* Fails: not a rewritable relation: (a ≈ b) in rule __top_assumption_ *)

使用默认的重写策略代替工作（即使没有手动声明实例，因为类似的东西已经在库中声明）。

什么好笑的：

Instance equivrw : (@RewriteRelation False equiv) := {}.
Lemma test_rwrel (a b c : False) : (equiv a b) -> (equiv b c) -> (equiv a c).
Proof.
    move => ->.
    by []. 
Qed.

这工作正常。

为什么 SSReflect 不使用我手动声明为通过用户定义的等效重写的 RewriteRelation 实例？提前致谢。

编辑： 我已经弄清楚为什么 Ssreflect 看不到我的关系。显然，您可以添加要与 Ssreflect 的重写一起使用的关系，仅Add Parametric Relation在手册中记录，并且RewriteRelation实例不会更改任何内容。我试图使用公理创建一个假关系并将其添加Add Parametric Relation并rewriting正常工作。但现在我又遇到了麻烦。我希望能够使用的关系具有类型crelation (x ~> y)（即(x ~> y) -> (x ~> y) -> Type），但要使用Add Parametric Relation我需要一个具有类型的术语relation (x ~> y)（即(x ~> y) -> (x ~> y) -> Prop。为什么在标准库中定义了两种不同类型的关系（relation和crelation）？我怎么能将 a 转换crelation为 arelation没有得到宇宙不一致错误？而且我仍然不明白为什么上面的例子False有效。

4

1 回答 1

2

将关系声明为 是不够的，也没有必要RewriteRelation。您必须证明确保重写在逻辑上有效的属性，最常见的是传递性（但您通常还需要自反性，甚至还需要对称性）。

正如您已经注意到的那样，setoid 重写插件实际上由两个孪生系统组成，一个用于关系 in Prop，一个用于关系 in Type（其模块名称以 为前缀C）。您通常只使用其中一种，具体取决于您的关系类型。

我不确定 SSReflect 是否会改变事情，但这里是一个没有它的 setoid 重写的示例用法：

  1. Require Setoid.激活插件。
  2. Require Import CEquivalence.如果你使用Type关系，或者Require Import Equivalence.如果你使用Prop关系。
  3. 实现等价关系属性的实例（任何Reflexive, Symmetric, Transitive, 或Equivalence所有 3 个）。
  4. Proper如果您要重写的术语不在目标的顶层，您可能还必须证明引理。

请注意，在第 3 步，如果您不/不能证明所有三个属性，那么您将不允许在所有方向上重写。

据我所知，Add Parametric Relation您可能在文档中找到的命令只是对这些实例脱糖的样板。但在我看来，作为用户，它们增加了不必要的间接层；直接声明实例会使事情更容易理解（特别是如果您已经熟悉类型类）。

Require Setoid. (* 1 *)
Require Import CMorphisms. (* 2 *)

Axiom obj : Type.
Axiom equiv : obj -> obj -> Type.
Axiom cat : forall a b c, equiv a b -> equiv b c -> equiv a c.

(* 3 *)
Instance Transitive_equiv : Transitive equiv.
Proof.
  exact cat.
Qed.

(* Example usage *)
Goal forall a b c,
    equiv a b -> equiv b c -> equiv a c.
Proof.
  intros a b c H1 H2.
  rewrite H1.
  (* or,
  rewrite H2
  *)
于 2020-02-03T17:41:07.743 回答