D1j: Domknięcie przechodnie i systemy przepisywania [TODO]


Require Import Lia.

From Typonomikon Require Export BC2i.

Require Import Classes.RelationClasses.

Domknięcia (TODO)

Domknięcie przechodnie


Inductive tc {A : Type} (R : rel A) : rel A :=
| tc_step : forall x y : A, R x y -> tc R x y
| tc_trans : forall x y z : A, R x y -> tc R y z -> tc R x z.


#[export]
Instance Transitive_tc :
  forall (A : Type) (R : rel A),
    Transitive (tc R).

Lemma subrelation_tc :
  forall (A : Type) (R : rel A), subrelation R (tc R).

Lemma tc_smallest :
  forall (A : Type) (R S : rel A),
    subrelation R S -> Transitive S ->
      subrelation (tc R) S.

Lemma tc_idempotent :
  forall (A : Type) (R : rel A),
    tc (tc R) <--> tc R.

Lemma tc_Rinv :
  forall (A : Type) (R : rel A),
    Rinv (tc (Rinv R)) <--> tc R.

Ćwiczenie (alternatywne domknięcie przechodnie)

Przyjrzyj się poniższej definicji domknięcia przechodniego. Udowodnij, że jest ona równoważna oryginalnej definicji. Czy poniższa definicja jest lepsza czy gorsza od oryginalnej?

Inductive tc' {A : Type} (R : rel A) : rel A :=
| tc'_step :
    forall x y : A, R x y -> tc' R x y
| tc'_trans :
    forall x y z : A,
      tc' R x y -> tc' R y z -> tc' R x z.


Lemma tc_tc' :
  forall (A : Type) (R : rel A),
    tc R <--> tc' R.

Domknięcie zwrotnoprzechodnie


Inductive rtc {A : Type} (R : rel A) : rel A :=
(* | rtc_step  : forall x y : A, R x y ->  *)
| rtc_refl : forall x : A, rtc R x x
| rtc_trans : forall x y z : A, R x y -> rtc R y z -> rtc R x z.

Lemma rtc_step :
  forall {A : Type} (R : rel A) (x y : A),
    R x y -> rtc R x y.

#[export]
Instance Reflexive_rtc :
  forall {A : Type} (R : rel A),
    Reflexive (rtc R).

#[export]
Instance Transitive_rtc :
  forall {A : Type} (R : rel A),
    Transitive (rtc R).

Lemma rtc_RTrue_spec :
  forall A : Type, rtc (@RTrue A A) <--> RTrue.

Ćwiczneie (alternatywna definicja)

Pokaż, że poniższa alternatywna definicja domknięcia zwrotno-przechodniego jest równoważna oryginalnej. Która jest lepsza?

Definition rtc' {A : Type} (R : rel A) : rel A :=
  rc (tc R).

Lemma rtc_rtc' :
  forall {A : Type} (R : rel A),
    rtc R <--> rtc' R.

Domknięcie równoważnościowe


Definition ec {A : Type} (R : rel A) : rel A :=
  rtc (sc R).


#[export]
Instance Reflexive_ec :
  forall {A : Type} (R : rel A),
    Reflexive (ec R).

#[export]
Instance Symmetric_ec :
  forall {A : Type} (R : rel A),
    Symmetric (ec R).

#[export]
Instance Transitive_ec :
  forall {A : Type} (R : rel A),
    Transitive (ec R).

#[export]
Instance Equivalence_ec :
  forall (A : Type) (R : rel A), Equivalence (ec R).

Lemma subrelation_ec :
  forall (A : Type) (R : rel A), subrelation R (ec R).

Lemma ec_smallest :
  forall (A : Type) (R S : rel A),
    subrelation R S -> Equivalence S ->
      subrelation (ec R) S.

Lemma ec_idempotent :
  forall (A : Type) (R : rel A),
    ec (ec R) <--> ec R.

Lemma ec_Rinv :
  forall (A : Type) (R : rel A),
    Rinv (ec (Rinv R)) <--> ec R.

Ćwiczenie (alternatywne definicje)

Pokaż, że poniższe alternatywne definicje domknięcia równoważnościowego są równoważne oryginalnej. Która definicja jest najlepsza?

Inductive equiv_clos {A : Type} (R : rel A) : rel A :=
| equiv_clos_step :
    forall x y : A, R x y -> equiv_clos R x y
| equiv_clos_refl :
    forall x : A, equiv_clos R x x
| equiv_clos_symm :
    forall x y : A, equiv_clos R x y -> equiv_clos R y x
| equiv_clos_trans :
    forall x y z : A,
      equiv_clos R x y -> equiv_clos R y z -> equiv_clos R x z.


#[export]
Instance Equivalence_equiv_clos :
  forall (A : Type) (R : rel A), Equivalence (equiv_clos R).

Lemma ec_equiv_clos :
  forall {A : Type} (R : rel A),
    ec R <--> equiv_clos R.

Definition rstc {A : Type} (R : rel A) : rel A :=
  tc' (sc' (rc R)).


#[export]
Instance Reflexive_rstc :
  forall {A : Type} (R : rel A),
    Reflexive (rstc R).

#[export]
Instance Symmetric_rstc :
  forall {A : Type} (R : rel A),
    Symmetric (rstc R).

#[export]
Instance Transitive_rstc :
  forall {A : Type} (R : rel A),
    Transitive (rstc R).

#[export]
Instance Equivalence_rstc :
  forall (A : Type) (R : rel A),
    Equivalence (rstc R).

Lemma rstc_equiv_clos :
  forall {A : Type} (R : rel A),
    rstc R <--> equiv_clos R.

Inductive EquivalenceClosure {A : Type} (R : rel A) : rel A :=
| EC_step : forall x y : A, R x y -> EquivalenceClosure R x y
| EC_refl : forall x : A, EquivalenceClosure R x x
| EC_symm : forall x y : A, R x y -> EquivalenceClosure R y x
| EC_trans : forall x y z : A, R x y -> EquivalenceClosure R y z -> EquivalenceClosure R x z.

#[global] Hint Constructors EquivalenceClosure : core.

#[export]
Instance Reflexive_EquivalenceClosure :
  forall {A : Type} (R : rel A),
    Reflexive (EquivalenceClosure R).

#[export]
Instance Symmetric_EquivalenceClosure :
  forall {A : Type} (R : rel A),
    Symmetric (EquivalenceClosure R).

#[export]
Instance Transitive_EquivalenceClosure :
  forall {A : Type} (R : rel A),
    Transitive (EquivalenceClosure R).

Lemma EquivalenceClosure_equiv_clos :
  forall {A : Type} (R : rel A),
    EquivalenceClosure R <--> equiv_clos R.

Definition EquivalenceClosure' {A : Type} (R : rel A) : rel A :=
  rc (tc' (sc' R)).

#[export]
Instance Reflexive_EquivalenceClosure' :
  forall {A : Type} (R : rel A),
    Reflexive (EquivalenceClosure' R).

#[export]
Instance Symmetric_EquivalenceClosure' :
  forall {A : Type} (R : rel A),
    Symmetric (EquivalenceClosure' R).

#[export]
Instance Transitive_EquivalenceClosure' :
  forall {A : Type} (R : rel A),
    Transitive (EquivalenceClosure' R).

Lemma EquivalenceClosure'_equiv_clos :
  forall {A : Type} (R : rel A),
    EquivalenceClosure' R <--> equiv_clos R.

Domknięcie cyrkularne


Inductive CircularClosure {A : Type} (R : rel A) : rel A :=
| CC_step :
    forall x y : A, R x y -> CircularClosure R x y
| CC_circ :
    forall x y z : A,
      CircularClosure R x y -> CircularClosure R y z ->
        CircularClosure R z x.

#[export]
Instance Circular_CircularClosure
  {A : Type} (R : rel A) : Circular (CircularClosure R).

Cosik o systemach przepisywania (TODO)

Właściwość diamentu


Class Diamond {A : Type} (R : rel A) : Prop :=
  diamond :
    forall x y z : A,
      R x y -> R x z ->
        exists w : A, R y w /\ R z w.

#[export]
Instance Diamond_RTrue :
  forall A : Type, Diamond (@RTrue A A).

#[export]
Instance Diamond_RFalse :
  forall A : Type, Diamond (@RFalse A A).

#[export]
Instance Diamond_eq :
  forall A : Type, Diamond (@eq A).

#[export]
Instance Diamond_lt :
  Diamond lt.

#[export]
Instance Diamond_le :
  Diamond le.

Lemma not_Diamond_gt :
  ~ Diamond gt.

#[export]
Instance Diamond_ge :
  Diamond ge.

Lemma not_Diamond_Rinv :
  exists (A : Type) (R : rel A),
    Diamond R /\ ~ Diamond (Rinv R).

Lemma not_Diamond_Rcomp :
  exists (A : Type) (R S : rel A),
    Diamond R /\ Diamond S /\ ~ Diamond (Rcomp R S).

Lemma not_Diamond_Rnot :
  exists (A : Type) (R : rel A),
    Diamond R /\ ~ Diamond (Rnot R).

Lemma not_Diamond_Ror :
  exists (A : Type) (R S : rel A),
    Diamond R /\ Diamond S /\ ~ Diamond (Ror R S).

Lemma not_Diamond_Rand :
  exists (A : Type) (R S : rel A),
    Diamond R /\ Diamond S /\ ~ Diamond (Rand R S).

Relacje lokalnie konfluentne


Class LocallyConfluent {A : Type} (R : rel A) : Prop :=
  locally_confluent :
    forall x y z : A, R x y -> R x z -> exists w : A, rtc R y w /\ rtc R z w.

#[export]
Instance LocallyConfluent_RTrue :
  forall A : Type, LocallyConfluent (@RTrue A A).

#[export]
Instance LocallyConfluent_RFalse :
  forall A : Type, LocallyConfluent (@RFalse A A).

#[export]
Instance LocallyConfluent_eq :
  forall A : Type, LocallyConfluent (@eq A).

#[export]
Instance LocallyConfluent_Diamond :
  forall {A : Type} (R : rel A),
    Diamond R -> LocallyConfluent R.

Lemma not_LocallyConfluent_gt :
  ~ LocallyConfluent gt.

Lemma not_LocallyConfluent_Rinv :
  exists (A : Type) (R : rel A),
    LocallyConfluent R /\ ~ LocallyConfluent (Rinv R).

Lemma not_LocallyConfluent_Rcomp :
  exists (A : Type) (R S : rel A),
    LocallyConfluent R /\ LocallyConfluent S /\ ~ LocallyConfluent (Rcomp R S).

Lemma not_LocallyConfluent_Rnot :
  exists (A : Type) (R : rel A),
    LocallyConfluent R /\ ~ LocallyConfluent (Rnot R).

Lemma not_LocallyConfluent_Ror :
  exists (A : Type) (R S : rel A),
    LocallyConfluent R /\ LocallyConfluent S /\ ~ LocallyConfluent (Ror R S).

Lemma not_LocallyConfluent_Rand :
  exists (A : Type) (R S : rel A),
    LocallyConfluent R /\ LocallyConfluent S /\ ~ LocallyConfluent (Rand R S).

Relacje konfluentne


Class Confluent {A : Type} (R : rel A) : Prop :=
  confluent :
    forall x y z : A, rtc R x y -> rtc R x z -> exists w : A, rtc R y w /\ rtc R z w.

#[export]
Instance Confluent_RTrue :
  forall A : Type, Confluent (@RTrue A A).

#[export]
Instance Confluent_RFalse :
  forall A : Type, Confluent (@RFalse A A).

#[export]
Instance Confluent_eq :
  forall A : Type, Confluent (@eq A).

Lemma not_Confluent_Rinv :
  exists (A : Type) (R : rel A),
    Confluent R /\ ~ Confluent (Rinv R).

Lemma not_Confluent_Rcomp :
  exists (A : Type) (R S : rel A),
    Confluent R /\ Confluent S /\ ~ Confluent (Rcomp R S).

Lemma not_Confluent_Rnot :
  exists (A : Type) (R : rel A),
    Confluent R /\ ~ Confluent (Rnot R).

Lemma not_Confluent_Ror :
  exists (A : Type) (R S : rel A),
    Confluent R /\ Confluent S /\ ~ Confluent (Ror R S).

#[export]
Instance Confluent_Rand :
  forall {A : Type} (R S : rel A),
    Confluent R -> Confluent S -> Confluent (Rand R S).

Lemma not_Confluent_Rand :
  exists (A : Type) (R S : rel A),
    Confluent R /\ Confluent S /\ ~ Confluent (Rand R S).