CODEWITHSUNDEEP
coqssreflect
jabberabbe
jabberabbe

Reputation: 35

SsrReflect and setoid rewriting

I can't use Ssreflect's rewrite with setoids. Although I don't think this information is relevant to solve the problem, I'm using this formulation of category theory in coq: https://github.com/jwiegley/category-theory.

As far as I know, Ssreflect's rewriting can use user-defined equivalence relations if a suitable RewriteRelation Typeclass instance can be resolved.

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_ *)

Using the default rewrite tactic instead works (even without manually declaring the instance, because something similar is already declared in the library).

Something funny:

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.

This works fine.

Why doesn't SSReflect use the RewriteRelation instance I have manually declared to rewrite by user-defined equivalence? Thanks in advance.

EDIT: I have figured out why Ssreflect doesn't see my relation. Apparently, you can add relations to be used with Ssreflect's rewrite only with Add Parametric Relation which is documented in the manual, and RewriteRelation instances don't change anything. I have tried to create a fake relation using axioms and adding it with Add Parametric Relation and rewriting works correctly. But now I'm again in trouble. The relation that I want to be able to use has type crelation (x ~> y) (which is (x ~> y) -> (x ~> y) -> Type), but to use Add Parametric Relation I need a term with type relation (x ~> y) (which is (x ~> y) -> (x ~> y) -> Prop. Why two different kinds of relations (relation and crelation) have been defined in the standard library? How can I convert a crelation to a relation without getting universe inconsistency errors? And I still can't understand why the above example with False works.

Upvotes: 1

Views: 550

Answers (1)

Li-yao Xia
Li-yao Xia

Reputation: 33389

It's not sufficient nor necessary to declare a relation as a RewriteRelation. You must prove properties that ensure that the rewriting is logically valid, the most common one being transitivity (but you often want also reflexivity, and even symmetry as well).

As you have noticed already, the setoid rewriting plugin is actually made of two twin systems, one for relations in Prop, and one for relations in Type (whose module names are prefixed with C). You generally use just one or the other, depending on the sort of your relations.

I'm not sure whether SSReflect changes things, but here is an example usage of setoid rewriting without it:

  1. Require Setoid. to activate the plugin.
  2. Require Import CEquivalence. if you use Type relations, or Require Import Equivalence. if you use Prop relations.
  3. Implement instances for properties of equivalence relations (any of Reflexive, Symmetric, Transitive, or Equivalence for all 3).
  4. You may also have to prove Proper lemmas if the terms you are rewriting are not at the toplevel of the goal.

Note that at step 3, if you do not/cannot prove all three properties, then you will not be allowed to rewrite in all directions.

To the best of my knowledge, commands such as Add Parametric Relation you may find in the documentation are just boilerplate that desugar to these instances. But in my opinion as a user, they add an unnecessary layer of indirection; declaring the instances directly makes things more understandable (especially if you're already familiar with type classes).

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
  *)

Upvotes: 2

Related Questions