Library cawu.rel


Utilities for working with binary relations


Require Import coinduction.
Set Implicit Arguments.

Pairs and sets of pairs


Definition pair A (x y: A) := fun x= y=.
Lemma leq_pair A (x y: A) (R: A A Prop): R x y pair x y R.
Proof. firstorder congruence. Qed.
Global Opaque pair.
Lemma in_pair0 A b (x y: A): t b (pair x y) x y.
Proof. now apply (id_t b), leq_pair. Qed.
Lemma in_pair1 I A b (x y: I A): i, t b (sup_all (fun ipair (x i) (y i))) (x i) (y i).
Proof. intros. apply (id_t b). rewrite leq_pair. now repeat eapply eleq_xsup_all. Qed.
Lemma in_pair2 I J A b (x y: I J A): i j, t b (sup_all (fun isup_all (fun jpair (x i j) (y i j)))) (x i j) (y i j).
Proof. intros. apply (id_t b). rewrite leq_pair. now repeat eapply eleq_xsup_all. Qed.
Lemma in_pair3 I J K A b (x y: I J K A): i j k, t b (sup_all (fun isup_all (fun jsup_all (fun kpair (x i j k) (y i j k))))) (x i j k) (y i j k).
Proof. intros. apply (id_t b). rewrite leq_pair. now repeat eapply eleq_xsup_all. Qed.

Friendly coinduction tactic, for relations

(it just goes back and forth between the above encoding of sets of pairs, and Coq's native symbols)

Ltac coinduction R H :=
  let rec init :=
    lazymatch goal with
    | |- x, _let x:=fresh x in intro x; init; revert x; rewrite <-sup_all_spec
    | |- gfp _ _ _rewrite leq_pair
  end in
  init; apply coinduction;
  match goal with |- ?Rb body ?b _
    set (R:=Rb) at -1;
    repeat setoid_rewrite sup_all_spec;
    setoid_rewrite <-leq_pair;
    first
      [ pose proof (in_pair0 b _ _: t b R _ _) as H
      | pose proof (in_pair1 b _ _: i, t b R _ _) as H
      | pose proof (in_pair2 b _ _: i j, t b R _ _) as H
      | pose proof (in_pair3 b _ _: i j k, t b R _ _) as H
      ];
    clearbody R
  end.

Generic definitions and results about relations

squaring function
Program Definition square {A}: mon (A A Prop) :=
  {| body R x y := exists2 z, R x z & R z y |}.
Next Obligation. cbv. firstorder. Qed.

converse function (an involution)
Program Definition converse {A}: mon (A A Prop) :=
  {| body R x y := R y x |}.
Next Obligation. cbv. firstorder. Qed.

Instance Involution_converse {A}: Involution (@converse A).
Proof. now intros ? ?. Qed.

provided that const eq, square, and converse are below t, we have that gfp b, t R, and T f R are always equivalence relations.
Section s.
  Variables (A: Type) (b: mon (relation A)).
  Hypothesis eq_t: const eq t b.
  Hypothesis converse_t: converse t b.
  Hypothesis square_t: square t b.
  Lemma Equivalence_T f R: Equivalence (t (B b) f R).
  Proof.
    constructor.
    intro. now apply (ftT_T f eq_t).
    intros x y. apply (ftT_T f converse_t).
    intros ? y ???. apply (ftT_T f square_t). y; assumption.
  Qed.
  Lemma Equivalence_t R: Equivalence (t b R).
  Proof.
    constructor.
    intro. now apply (ft_t eq_t).
    intros x y. apply (ft_t converse_t).
    intros ? y ???. apply (ft_t square_t). y; assumption.
  Qed.
  Corollary Equivalence_gfp: Equivalence (gfp b).
  Proof Equivalence_t bot.
End s.

R is always a subrelation of t R and T f R
Instance rel_gfp_T A b f (R: relation A): subrelation (gfp b) (t (B b) f R).
Proof. refine (gfp_T _ f R). Qed.

Instance rel_gfp_t A b (R: relation A): subrelation (gfp b) (t b R).
Proof. refine (gfp_t _ R). Qed.

Contexts

unary context: unary_ctx f(R) = {(f x, f y) | x R y }
Program Definition unary_ctx S (f: S S): mon (S S Prop) :=
  {| body R := sup_all (fun x
               sup (R x) (fun pair (f x) (f ))) |}.
Next Obligation.
  Transparent pair. Opaque plus.
  cbv; firstorder subst; eauto.
  Transparent plus. Opaque pair.
Qed.

Lemma leq_unary_ctx S f R T:
  @unary_ctx S f R T x , R x T (f x) (f ).
Proof.
  unfold unary_ctx. setoid_rewrite sup_all_spec.
  setoid_rewrite sup_spec.
  setoid_rewrite <-leq_pair. firstorder.
Qed.
Lemma in_unary_ctx S (f: S S) (R: S S Prop) x :
  R x unary_ctx f R (f x) (f ).
Proof. intros. now applyleq_unary_ctx. Qed.
Global Opaque unary_ctx.

such a function is always symmetric
Lemma unary_sym S (f: S S): compat converse (unary_ctx f).
Proof. intro R. simpl. apply leq_unary_ctx. intros. now apply in_unary_ctx. Qed.

if it is below t, then the function f always preserves t R
Lemma unary_proper S (f: S S) b:
  (unary_ctx f) t b R, Proper (t b R ==> t b R) f.
Proof. intros H R x Hx. apply (ft_t H). now apply (in_unary_ctx f). Qed.


binary context: unary_ctx f(R) = {(f x x', f y y') | x R y, x' R y' }
Program Definition binary_ctx S (f: S S S): mon (S S Prop) :=
  {| body R := sup_all (fun x
               sup_all (fun y
               sup (R x) (fun
               sup (R y) (fun pair (f x y) (f ))))) |}.
Next Obligation.
  Transparent pair. Opaque plus.
  cbv; firstorder subst; eauto 8.
  Transparent plus. Opaque pair.
Qed.

Lemma leq_binary_ctx S f R T:
  @binary_ctx S f R T x , R x y , R y T (f x y) (f ).
Proof.
  unfold binary_ctx. do 2 setoid_rewrite sup_all_spec.
  do 2 setoid_rewrite sup_spec.
  setoid_rewrite <-leq_pair. firstorder.
Qed.
Lemma in_binary_ctx S (f: S S S) (R: S S Prop) x y :
  R x R y binary_ctx f R (f x y) (f ).
Proof. intros. now applyleq_binary_ctx. Qed.
Global Opaque binary_ctx.

such a function is always symmetric
Lemma binary_sym S (f: S S S): compat converse (binary_ctx f).
Proof. intro R. simpl. apply leq_binary_ctx. intros. now apply in_binary_ctx. Qed.

if it is below t, then the function f always preserves t R
Lemma binary_proper S (f: S S S) b:
  binary_ctx f t b R, Proper (t b R ==> t b R ==> t b R) f.
Proof. intros H R x Hx y Hy. apply (ft_t H). now apply (in_binary_ctx f). Qed.