Library Coq.ssr.ssrsetoid


Compatibility layer for under and setoid_rewrite.
This file is intended to be required by Require Import Setoid.
In particular, we can use the under tactic with other relations than eq or iff, e.g. a RewriteRelation, by doing: Require Import ssreflect. Require Setoid.
This file's instances have priority 12 > other stdlib instances and each Under_rel instance comes with a Hint Cut directive (otherwise Ring_polynom.v won't compile because of unbounded search).
(Note: this file could be skipped when porting under to stdlib2.)

Require Import ssrclasses.
Require Import ssrunder.
Require Import RelationClasses.
Require Import Relation_Definitions.

Reconcile Coq.Classes.RelationClasses.Reflexive with Coq.ssr.ssrclasses.Reflexive

Instance compat_Reflexive :
  forall {A} {R : relation A},
    RelationClasses.Reflexive R ->
    ssrclasses.Reflexive R | 12.

Add instances so that 'Under[ F i ] terms, that is, Under_rel T R (F i) (?G i) terms, can be manipulated with rewrite/setoid_rewrite with lemmas on R. Note that this requires that R is a Prop relation, otherwise a bool relation may need to be "lifted": see the TestPreOrder section in test-suite/ssr/under.v

Instance Under_subrelation {A} (R : relation A) : subrelation R (Under_rel _ R) | 12.


Instance Under_Reflexive {A} (R : relation A) :
  RelationClasses.Reflexive R ->
  RelationClasses.Reflexive (Under_rel.Under_rel A R) | 12.



Instance Under_Symmetric {A} (R : relation A) :
  RelationClasses.Symmetric R ->
  RelationClasses.Symmetric (Under_rel.Under_rel A R) | 12.


Instance Under_Transitive {A} (R : relation A) :
  RelationClasses.Transitive R ->
  RelationClasses.Transitive (Under_rel.Under_rel A R) | 12.


Instance Under_PreOrder {A} (R : relation A) :
  RelationClasses.PreOrder R ->
  RelationClasses.PreOrder (Under_rel.Under_rel A R) | 12.


Instance Under_PER {A} (R : relation A) :
  RelationClasses.PER R ->
  RelationClasses.PER (Under_rel.Under_rel A R) | 12.


Instance Under_Equivalence {A} (R : relation A) :
  RelationClasses.Equivalence R ->
  RelationClasses.Equivalence (Under_rel.Under_rel A R) | 12.