summaryrefslogtreecommitdiff
path: root/theories/Classes/RelationClasses.v
diff options
context:
space:
mode:
Diffstat (limited to 'theories/Classes/RelationClasses.v')
-rw-r--r--theories/Classes/RelationClasses.v85
1 files changed, 44 insertions, 41 deletions
diff --git a/theories/Classes/RelationClasses.v b/theories/Classes/RelationClasses.v
index 94c51bf1..cf05d9d4 100644
--- a/theories/Classes/RelationClasses.v
+++ b/theories/Classes/RelationClasses.v
@@ -1,13 +1,13 @@
(* -*- coding: utf-8 -*- *)
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(** * Typeclass-based relations, tactics and standard instances
+(** * Typeclass-based relations, tactics and standard instances
This is the basic theory needed to formalize morphisms and setoids.
@@ -15,8 +15,6 @@
Institution: LRI, CNRS UMR 8623 - University Paris Sud
*)
-(* $Id: RelationClasses.v 14641 2011-11-06 11:59:10Z herbelin $ *)
-
Require Export Coq.Classes.Init.
Require Import Coq.Program.Basics.
Require Import Coq.Program.Tactics.
@@ -143,9 +141,9 @@ Program Instance impl_Transitive : Transitive impl.
(** Logical equivalence. *)
-Program Instance iff_Reflexive : Reflexive iff.
-Program Instance iff_Symmetric : Symmetric iff.
-Program Instance iff_Transitive : Transitive iff.
+Instance iff_Reflexive : Reflexive iff := iff_refl.
+Instance iff_Symmetric : Symmetric iff := iff_sym.
+Instance iff_Transitive : Transitive iff := iff_trans.
(** Leibniz equality. *)
@@ -158,14 +156,14 @@ Instance eq_Transitive {A} : Transitive (@eq A) := @eq_trans A.
(** A [PreOrder] is both Reflexive and Transitive. *)
Class PreOrder {A} (R : relation A) : Prop := {
- PreOrder_Reflexive :> Reflexive R ;
- PreOrder_Transitive :> Transitive R }.
+ PreOrder_Reflexive :> Reflexive R | 2 ;
+ PreOrder_Transitive :> Transitive R | 2 }.
(** A partial equivalence relation is Symmetric and Transitive. *)
Class PER {A} (R : relation A) : Prop := {
- PER_Symmetric :> Symmetric R ;
- PER_Transitive :> Transitive R }.
+ PER_Symmetric :> Symmetric R | 3 ;
+ PER_Transitive :> Transitive R | 3 }.
(** Equivalence relations. *)
@@ -210,17 +208,21 @@ Local Open Scope list_scope.
(** A compact representation of non-dependent arities, with the codomain singled-out. *)
-Fixpoint arrows (l : list Type) (r : Type) : Type :=
+(* Note, we do not use [list Type] because it imposes unnecessary universe constraints *)
+Inductive Tlist : Type := Tnil : Tlist | Tcons : Type -> Tlist -> Tlist.
+Local Infix "::" := Tcons.
+
+Fixpoint arrows (l : Tlist) (r : Type) : Type :=
match l with
- | nil => r
+ | Tnil => r
| A :: l' => A -> arrows l' r
end.
(** We can define abbreviations for operation and relation types based on [arrows]. *)
-Definition unary_operation A := arrows (A::nil) A.
-Definition binary_operation A := arrows (A::A::nil) A.
-Definition ternary_operation A := arrows (A::A::A::nil) A.
+Definition unary_operation A := arrows (A::Tnil) A.
+Definition binary_operation A := arrows (A::A::Tnil) A.
+Definition ternary_operation A := arrows (A::A::A::Tnil) A.
(** We define n-ary [predicate]s as functions into [Prop]. *)
@@ -228,23 +230,23 @@ Notation predicate l := (arrows l Prop).
(** Unary predicates, or sets. *)
-Definition unary_predicate A := predicate (A::nil).
+Definition unary_predicate A := predicate (A::Tnil).
(** Homogeneous binary relations, equivalent to [relation A]. *)
-Definition binary_relation A := predicate (A::A::nil).
+Definition binary_relation A := predicate (A::A::Tnil).
(** We can close a predicate by universal or existential quantification. *)
-Fixpoint predicate_all (l : list Type) : predicate l -> Prop :=
+Fixpoint predicate_all (l : Tlist) : predicate l -> Prop :=
match l with
- | nil => fun f => f
+ | Tnil => fun f => f
| A :: tl => fun f => forall x : A, predicate_all tl (f x)
end.
-Fixpoint predicate_exists (l : list Type) : predicate l -> Prop :=
+Fixpoint predicate_exists (l : Tlist) : predicate l -> Prop :=
match l with
- | nil => fun f => f
+ | Tnil => fun f => f
| A :: tl => fun f => exists x : A, predicate_exists tl (f x)
end.
@@ -253,30 +255,30 @@ Fixpoint predicate_exists (l : list Type) : predicate l -> Prop :=
For an operator on [Prop] this lifts the operator to a binary operation. *)
Fixpoint pointwise_extension {T : Type} (op : binary_operation T)
- (l : list Type) : binary_operation (arrows l T) :=
+ (l : Tlist) : binary_operation (arrows l T) :=
match l with
- | nil => fun R R' => op R R'
+ | Tnil => fun R R' => op R R'
| A :: tl => fun R R' =>
fun x => pointwise_extension op tl (R x) (R' x)
end.
(** Pointwise lifting, equivalent to doing [pointwise_extension] and closing using [predicate_all]. *)
-Fixpoint pointwise_lifting (op : binary_relation Prop) (l : list Type) : binary_relation (predicate l) :=
+Fixpoint pointwise_lifting (op : binary_relation Prop) (l : Tlist) : binary_relation (predicate l) :=
match l with
- | nil => fun R R' => op R R'
+ | Tnil => fun R R' => op R R'
| A :: tl => fun R R' =>
forall x, pointwise_lifting op tl (R x) (R' x)
end.
(** The n-ary equivalence relation, defined by lifting the 0-ary [iff] relation. *)
-Definition predicate_equivalence {l : list Type} : binary_relation (predicate l) :=
+Definition predicate_equivalence {l : Tlist} : binary_relation (predicate l) :=
pointwise_lifting iff l.
(** The n-ary implication relation, defined by lifting the 0-ary [impl] relation. *)
-Definition predicate_implication {l : list Type} :=
+Definition predicate_implication {l : Tlist} :=
pointwise_lifting impl l.
(** Notations for pointwise equivalence and implication of predicates. *)
@@ -297,15 +299,15 @@ Infix "\∙/" := predicate_union (at level 85, right associativity) : predicate_
(** The always [True] and always [False] predicates. *)
-Fixpoint true_predicate {l : list Type} : predicate l :=
+Fixpoint true_predicate {l : Tlist} : predicate l :=
match l with
- | nil => True
+ | Tnil => True
| A :: tl => fun _ => @true_predicate tl
end.
-Fixpoint false_predicate {l : list Type} : predicate l :=
+Fixpoint false_predicate {l : Tlist} : predicate l :=
match l with
- | nil => False
+ | Tnil => False
| A :: tl => fun _ => @false_predicate tl
end.
@@ -315,6 +317,7 @@ Notation "∙⊥∙" := false_predicate : predicate_scope.
(** Predicate equivalence is an equivalence, and predicate implication defines a preorder. *)
Program Instance predicate_equivalence_equivalence : Equivalence (@predicate_equivalence l).
+
Next Obligation.
induction l ; firstorder.
Qed.
@@ -343,18 +346,18 @@ Program Instance predicate_implication_preorder :
from the general ones. *)
Definition relation_equivalence {A : Type} : relation (relation A) :=
- @predicate_equivalence (_::_::nil).
+ @predicate_equivalence (_::_::Tnil).
Class subrelation {A:Type} (R R' : relation A) : Prop :=
- is_subrelation : @predicate_implication (A::A::nil) R R'.
+ is_subrelation : @predicate_implication (A::A::Tnil) R R'.
-Implicit Arguments subrelation [[A]].
+Arguments subrelation {A} R R'.
Definition relation_conjunction {A} (R : relation A) (R' : relation A) : relation A :=
- @predicate_intersection (A::A::nil) R R'.
+ @predicate_intersection (A::A::Tnil) R R'.
Definition relation_disjunction {A} (R : relation A) (R' : relation A) : relation A :=
- @predicate_union (A::A::nil) R R'.
+ @predicate_union (A::A::Tnil) R R'.
(** Relation equivalence is an equivalence, and subrelation defines a partial order. *)
@@ -362,10 +365,10 @@ Set Automatic Introduction.
Instance relation_equivalence_equivalence (A : Type) :
Equivalence (@relation_equivalence A).
-Proof. exact (@predicate_equivalence_equivalence (A::A::nil)). Qed.
+Proof. exact (@predicate_equivalence_equivalence (A::A::Tnil)). Qed.
Instance relation_implication_preorder A : PreOrder (@subrelation A).
-Proof. exact (@predicate_implication_preorder (A::A::nil)). Qed.
+Proof. exact (@predicate_implication_preorder (A::A::Tnil)). Qed.
(** *** Partial Order.
A partial order is a preorder which is additionally antisymmetric.
@@ -393,7 +396,7 @@ Program Instance subrelation_partial_order :
Next Obligation.
Proof.
- unfold relation_equivalence in *. firstorder.
+ unfold relation_equivalence in *. compute; firstorder.
Qed.
Typeclasses Opaque arrows predicate_implication predicate_equivalence
@@ -420,7 +423,7 @@ Instance equivalence_rewrite_relation `(Equivalence A eqA) : RewriteRelation eqA
(** Strict Order *)
-Class StrictOrder {A : Type} (R : relation A) := {
+Class StrictOrder {A : Type} (R : relation A) : Prop := {
StrictOrder_Irreflexive :> Irreflexive R ;
StrictOrder_Transitive :> Transitive R
}.
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-18 05:17:06 +0000