# Library CoLoR.Util.Relation.RelExtras

CoLoR, a Coq library on rewriting and termination. See the COPYRIGHTS and LICENSE files.
• William Delobel, 2005-10-07
This file provides some basic results concerning relations that were missing in the standard library.

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

Ltac rewrite_lr term := apply (proj1 term).
Ltac rewrite_rl term := apply (proj2 term).

Ltac try_solve :=
simpl in *; try (intros; solve
[ contr
| discr
| auto with terms
| tauto
| congruence
]).