Built with Alectryon, running Coq+SerAPI v8.10.0+0.7.0. Coq sources are in this panel; goals and messages will appear in the other. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑ Ctrl+↓ to navigate, Ctrl+🖱️ to focus.

(************************************************************************)
(*         *   The Coq Proof Assistant / The Coq Development Team       *)
(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
(* <O___,, *       (see CREDITS file for the list of authors)           *)
(*   \VV/  **************************************************************)
(*    //   *    This file is distributed under the terms of the         *)
(*         *     GNU Lesser General Public License Version 2.1          *)
(*         *     (see LICENSE file for the text of the license)         *)
(************************************************************************)

Morphism instances for relations.

Author: Matthieu Sozeau Institution: LRI, CNRS UMR 8623 - University Paris Sud

Require Import Relation_Definitions.
Require Import Coq.Classes.Morphisms.
Require Import Coq.Program.Program.

Generalizable Variables A l.

Morphisms for relations

Instance relation_conjunction_morphism : Proper (relation_equivalence (A:=A) ==>
  relation_equivalence ==> relation_equivalence) relation_conjunction.forall A : Type,
Proper
  (relation_equivalence ==>
   relation_equivalence ==> relation_equivalence)
  relation_conjunction
  Proof.forall A : Type,
Proper
  (relation_equivalence ==>
   relation_equivalence ==> relation_equivalence)
  relation_conjunction firstorder. Qed.

Instance relation_disjunction_morphism : Proper (relation_equivalence (A:=A) ==>
  relation_equivalence ==> relation_equivalence) relation_disjunction.forall A : Type,
Proper
  (relation_equivalence ==>
   relation_equivalence ==> relation_equivalence)
  relation_disjunction
  Proof.forall A : Type,
Proper
  (relation_equivalence ==>
   relation_equivalence ==> relation_equivalence)
  relation_disjunction firstorder. Qed.

(* Predicate equivalence is exactly the same as the pointwise lifting of [iff]. *)

Lemma predicate_equivalence_pointwise (l : Tlist) :
  Proper (@predicate_equivalence l ==> pointwise_lifting iff l) id.l:Tlist
Proper
  (predicate_equivalence ==> pointwise_lifting iff l)
  id
Proof.l:Tlist
Proper
  (predicate_equivalence ==> pointwise_lifting iff l)
  id do 2 red.l:Tlist
forall x y : predicate l,
predicate_equivalence x y ->
pointwise_lifting iff l (id x) (id y) unfold predicate_equivalence.l:Tlist
forall x y : predicate l,
pointwise_lifting iff l x y ->
pointwise_lifting iff l (id x) (id y) auto. Qed.

Lemma predicate_implication_pointwise (l : Tlist) :
  Proper (@predicate_implication l ==> pointwise_lifting impl l) id.l:Tlist
Proper
  (predicate_implication ==> pointwise_lifting impl l)
  id
Proof.l:Tlist
Proper
  (predicate_implication ==> pointwise_lifting impl l)
  id do 2 red.l:Tlist
forall x y : predicate l,
predicate_implication x y ->
pointwise_lifting impl l (id x) (id y) unfold predicate_implication.l:Tlist
forall x y : predicate l,
pointwise_lifting impl l x y ->
pointwise_lifting impl l (id x) (id y) auto. Qed.

The instantiation at relation allows rewriting applications of relations R x y to R' x y when R and R' are in relation_equivalence.

Instance relation_equivalence_pointwise :
  Proper (relation_equivalence ==> pointwise_relation A (pointwise_relation A iff)) id.forall A : Type,
Proper
  (relation_equivalence ==>
   pointwise_relation A (pointwise_relation A iff)) id
Proof.forall A : Type,
Proper
  (relation_equivalence ==>
   pointwise_relation A (pointwise_relation A iff)) id intro.A:Type
Proper
  (relation_equivalence ==>
   pointwise_relation A (pointwise_relation A iff)) id apply (predicate_equivalence_pointwise (Tcons A (Tcons A Tnil))). Qed.

Instance subrelation_pointwise :
  Proper (subrelation ==> pointwise_relation A (pointwise_relation A impl)) id.forall A : Type,
Proper
  (subrelation ==>
   pointwise_relation A (pointwise_relation A impl))
  id
Proof.forall A : Type,
Proper
  (subrelation ==>
   pointwise_relation A (pointwise_relation A impl))
  id intro.A:Type
Proper
  (subrelation ==>
   pointwise_relation A (pointwise_relation A impl))
  id apply (predicate_implication_pointwise (Tcons A (Tcons A Tnil))). Qed.


Lemma flip_pointwise_relation A (R : relation A) :
  relation_equivalence (pointwise_relation A (flip R)) (flip (pointwise_relation A R)).A:Type
R:relation A
relation_equivalence (pointwise_relation A (flip R))
  (flip (pointwise_relation A R))
Proof.A:Type
R:relation A
relation_equivalence (pointwise_relation A (flip R))
  (flip (pointwise_relation A R)) intros.A:Type
R:relation A
relation_equivalence (pointwise_relation A (flip R))
  (flip (pointwise_relation A R)) split; firstorder. Qed.