1
(************************************************************************)
2
(* v * The Coq Proof Assistant / The Coq Development Team *)
3
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
4
(* \VV/ **************************************************************)
5
(* // * This file is distributed under the terms of the *)
6
(* * GNU Lesser General Public License Version 2.1 *)
7
(************************************************************************)
9
(* Morphism instances for relations.
11
Author: Matthieu Sozeau
12
Institution: LRI, CNRS UMR 8623 - UniversitÃcopyright Paris Sud
13
91405 Orsay, France *)
15
Require Import Relation_Definitions.
16
Require Import Coq.Classes.Morphisms.
17
Require Import Coq.Program.Program.
19
(** Morphisms for relations *)
21
Instance relation_conjunction_morphism : Morphism (relation_equivalence (A:=A) ==>
22
relation_equivalence ==> relation_equivalence) relation_conjunction.
23
Proof. firstorder. Qed.
25
Instance relation_disjunction_morphism : Morphism (relation_equivalence (A:=A) ==>
26
relation_equivalence ==> relation_equivalence) relation_disjunction.
27
Proof. firstorder. Qed.
29
(* Predicate equivalence is exactly the same as the pointwise lifting of [iff]. *)
33
Lemma predicate_equivalence_pointwise (l : list Type) :
34
Morphism (@predicate_equivalence l ==> pointwise_lifting iff l) id.
35
Proof. do 2 red. unfold predicate_equivalence. auto. Qed.
37
Lemma predicate_implication_pointwise (l : list Type) :
38
Morphism (@predicate_implication l ==> pointwise_lifting impl l) id.
39
Proof. do 2 red. unfold predicate_implication. auto. Qed.
41
(** The instanciation at relation allows to rewrite applications of relations [R x y] to [R' x y] *)
42
(* when [R] and [R'] are in [relation_equivalence]. *)
44
Instance relation_equivalence_pointwise :
45
Morphism (relation_equivalence ==> pointwise_relation A (pointwise_relation A iff)) id.
46
Proof. intro. apply (predicate_equivalence_pointwise (cons A (cons A nil))). Qed.
48
Instance subrelation_pointwise :
49
Morphism (subrelation ==> pointwise_relation A (pointwise_relation A impl)) id.
50
Proof. intro. apply (predicate_implication_pointwise (cons A (cons A nil))). Qed.
53
Lemma inverse_pointwise_relation A (R : relation A) :
54
relation_equivalence (pointwise_relation A (inverse R)) (inverse (pointwise_relation A R)).
55
Proof. intros. split; firstorder. Qed.