Library CoLoR.Util.Relation.RelExtras
CoLoR, a Coq library on rewriting and termination.
See the COPYRIGHTS and LICENSE files.
This file provides some basic results concerning relations that were
missing in the standard library.
- Adam Koprowski, 2004-09-06
- William Delobel, 2005-10-07
Set Implicit Arguments.
strict order
Section StrictOrder.
Variables (A : Type) (R : relation A).
Record strict_order : Prop := {
sord_trans : transitive R;
sord_irrefl : irreflexive R }.
Variable so : strict_order.
Lemma so_not_symmetric : forall a b, R a b -> R b a -> False.
Variables (eq : relation A)
(Req_compat : Proper (eq ==> eq ==> impl) R)
(eq_Equivalence : Equivalence eq).
Lemma so_strict : forall x y, eq x y -> ~R x y.
End StrictOrder.
module types for setoids with decidable equality
Module Type SetA.
Parameter A : Type.
End SetA.
Module Type Eqset.
Parameter A : Type.
Parameter eqA : relation A.
Notation "X =A= Y" := (eqA X Y) (at level 70).
Declare Instance eqA_Equivalence : Equivalence eqA.
Hint Resolve (Seq_refl A eqA eqA_Equivalence) : sets.
Hint Resolve (Seq_trans A eqA eqA_Equivalence) : sets.
Hint Resolve (Seq_sym A eqA eqA_Equivalence) : sets.
End Eqset.
Module Type Eqset_dec.
Declare Module Export Eq : Eqset.
Parameter eqA_dec : forall x y, {x =A= y} + {~x =A= y}.
End Eqset_dec.
Module Eqset_def (A : SetA) <: Eqset.
Definition A := A.A.
Definition eqA := eq (A:=A).
Instance eqA_Equivalence : Equivalence eqA.
Hint Resolve (Seq_refl A eqA eqA_Equivalence) : sets.
Hint Resolve (Seq_trans A eqA eqA_Equivalence) : sets.
Hint Resolve (Seq_sym A eqA eqA_Equivalence) : sets.
End Eqset_def.
module types for ordered setoids
Section Eqset_def_gtA_eqA_compat.
Variables (A : Type) (gtA : relation A).
Instance Eqset_def_gtA_eqA_compat : Proper (eq ==> eq ==> impl) gtA.
End Eqset_def_gtA_eqA_compat.
Module Type Ord.
Parameter A : Type.
Declare Module Export S : Eqset with Definition A := A.
Parameter gtA : relation A.
Notation "X >A Y" := (gtA X Y) (at level 70).
Declare Instance gtA_eqA_compat : Proper (eqA ==> eqA ==> impl) gtA.
Hint Resolve gtA_eqA_compat : sets.
End Ord.
Module OrdLemmas (Export P : Ord).
Definition ltA := transp gtA.
Definition geA x y := ~ ltA x y.
Definition leA x y := ~ gtA x y.
Definition AccA := Acc ltA.
Notation "X <A Y" := (ltA X Y) (at level 70).
Notation "X >=A Y" := (geA X Y) (at level 70).
Notation "X <=A Y" := (leA X Y) (at level 70).
Hint Unfold ltA geA leA AccA : sets.
Instance gtA_morph : Proper (eqA ==> eqA ==> iff) gtA.
Instance ltA_morph : Proper (eqA ==> eqA ==> iff) ltA.
Instance AccA_morph : Proper (eqA ==> iff) AccA.
End OrdLemmas.
Module Type Poset.
Parameter A : Type.
Declare Module Export O : Ord with Definition A := A.
Parameter gtA_so : strict_order gtA.
Hint Resolve (sord_trans gtA_so) : sets.
Hint Resolve (sord_irrefl gtA_so) : sets.
Hint Resolve (so_not_symmetric gtA_so) : sets.
Hint Resolve (so_strict gtA_so gtA_eqA_compat eqA_Equivalence) : sets.
End Poset.
Module nat_ord <: Ord.
Module natSet <: SetA.
Definition A := nat.
Definition eqA_dec := eq_nat_dec.
End natSet.
Module S := Eqset_def natSet.
Definition A := nat.
Definition gtA := gt.
Instance gtA_eqA_compat : Proper (eq ==> eq ==> impl) gt.
End nat_ord.
specification
Section Specif.
Inductive sigPS2 (A : Type) (P : A -> Prop) (Q : A -> Set) : Type :=
existPS2 : forall x, P x -> Q x -> sigPS2 (A:=A) P Q.
Notation "{ x : A # P & Q }"
:= (sigPS2 (fun x : A => P) (fun x : A => Q)) : type_scope.
Variables (A : Type) (P Q : A -> Prop).
Definition proj1_sig2 (e: sig2 P Q) :=
match e with
| exist2 _ _ a p q => a
end.
End Specif.
tactics