Library CoLoR.Util.Relation.GDomainBij

CoLoR, a Coq library on rewriting and termination. See the COPYRIGHTS and LICENSE files.
  • Leo Ducas, 2007-08-06
Given a list Dom, we make a bijection between element of Dom and [0,n-1], and relation restricted to Dom with relation restricted to [1,n].

Set Implicit Arguments.


Section S.

  Variables (A : Type) (eq_dec : forall x y : A, {x=y}+{~x=y}) (Dom : list A).

Definition of the bijection of graphs

  Definition rel_on_nat (R : relation A) i j :=
    match Dom[i] with
    | None => False
    | Some a =>
      match Dom[j] with
      | None => False
      | Some b => R a b
      end
    end.

  Definition rel_on_dom (S : relation nat) a b :=
    match find_first (eq a) (eq_dec a) Dom with
    | None => False
    | Some p =>
      match find_first (eq b) (eq_dec b) Dom with
      | None => False
      | Some q => S p q
      end
    end.

Basic properties

  Section basic_props.

    Variables (R : relation A) (S : relation nat).

    Lemma rel_on_nat_intro i j a b :
      Dom[i] = Some a -> Dom[j] = Some b -> R a b -> rel_on_nat R i j.

    Lemma rel_on_dom_intro i j a b :
      find_first (eq a) (eq_dec a) Dom = Some i ->
      find_first (eq b) (eq_dec b) Dom = Some j -> S i j -> rel_on_dom S a b.

    Lemma rel_on_nat_elim a b : rel_on_nat R a b ->
      exists x, exists y, R x y /\ Dom [a] = Some x /\ Dom [b] = Some y.

    Lemma rel_on_nat_is_restricted :
      is_restricted (rel_on_nat R) (nats_decr_lt (length Dom)).

    Lemma rel_on_dom_elim x y : rel_on_dom S x y ->
      exists a, exists b, S a b /\ Dom [a] = Some x /\ Dom [b] = Some y.


    Lemma rel_on_dom_elim2 x y : rel_on_dom S x y ->
      exists a, exists b, S a b
                          /\ find_first (eq x) (eq_dec x) Dom = Some a
                          /\ find_first (eq y) (eq_dec y) Dom = Some b.


    Variable Rdec : forall x y, {R x y}+{~R x y}.

    Lemma rel_on_nat_dec x y : {rel_on_nat R x y}+{~rel_on_nat R x y}.

  End basic_props.


Bijection

  Section bijection.

    Variables (R : relation A) (restriction : is_restricted R Dom).

    Lemma dom_change x y : rel_on_dom (rel_on_nat R) x y <-> R x y.

  End bijection.

composition is mapped to composition

  Section compose.

    Variables (R S : relation nat)
              (restriction : is_restricted R (nats_decr_lt (length Dom)))
              (restriction' : is_restricted S (nats_decr_lt (length Dom)))
              (Dom_nodup : nodup Dom).

    Lemma dom_change_compose x y:
      rel_on_dom (R @ S) x y <-> (rel_on_dom R @ rel_on_dom S) x y.

  End compose.

iteration mapped to iteration

  Section iter.

    Variables (R : relation A) (restriction : is_restricted R Dom)
              (Dom_nodup : nodup Dom).

    Lemma iter_preserve_restriction n : is_restricted (iter R n) Dom.

    Lemma dom_change_iter : forall n x y,
        rel_on_dom (iter (rel_on_nat R) n) x y <-> iter R n x y.

    Lemma dom_change_tc x y : rel_on_dom (rel_on_nat R !) x y <-> R! x y.

  End iter.

intersection mapped to intersection

  Section intersection.

    Variables R S : relation nat.

    Lemma dom_change_inter x y : rel_on_dom (intersection R S) x y
      <-> rel_on_dom R x y /\ rel_on_dom S x y.

  End intersection.

transposition mapped to transposition

  Section transpose.

    Variable R : relation nat.

    Lemma dom_change_transp x y :
      rel_on_dom (transp R) x y <-> transp (rel_on_dom R) x y.

  End transpose.

SCC mapped to SCC

  Section domSCC.

    Variables (R : relation A) (restriction : is_restricted R Dom)
              (Dom_nodup : nodup Dom).

    Lemma dom_change_SCC x y :
      rel_on_dom (SCC (rel_on_nat R)) x y <-> SCC R x y.

  End domSCC.

End S.