H3: Relacje



Require Import H2.
Require Import FunctionalExtensionality.

Require Import Nat.
Require Import List.
Import ListNotations.

Prerekwizyty:
W tym rozdziale zajmiemy się badaniem relacji. Poznamy podstawowe rodzaje relacji, ich właściwości, a także zależności i przekształcenia między nimi. Rozdział będzie raczej matematyczny.

Relacje binarne

Zacznijmy od przypomnienia klasyfikacji zdań, predykatów i relacji:
Istnieje jednak zasadnicza różnica między definiowaniem "zwykłych" funkcji oraz definiowaniem relacji: zwykłe funkcje możemy definiować jedynie przez dopasowanie do wzorca i rekurencję, zaś relacje możemy poza tymi metodami definiować także przez indukcję, dzięki czemu możemy wyrazić więcej konceptów niż za pomocą rekursji.

Definition hrel (A B : Type) : Type := A -> B -> Prop.

Najważniejszym rodzajem relacji są relacje binarne, czyli relacje biorące dwa argumenty. To właśnie im poświęcimy ten rozdział, pominiemy zaś relacje biorące trzy i więcej argumentów. Określenia "relacja binarna" będę używał zarówno na określenie relacji binarnych heterogenicznych (czyli biorących dwa argumnty różnych typów) jak i na określenie relacji binarnych homogenicznych (czyli biorących dwa argumenty tego samego typu).

Identyczność relacji


Definition subrelation {A B : Type} (R S : hrel A B) : Prop :=
  forall (a : A) (b : B), R a b -> S a b.

Notation "R --> S" := (subrelation R S) (at level 40).

Definition same_hrel {A B : Type} (R S : hrel A B) : Prop :=
  subrelation R S /\ subrelation S R.

Notation "R <--> S" := (same_hrel R S) (at level 40).

Zacznijmy od ustalenia, jakie relacje będziemy uznawać za "identyczne". Okazuje się, że używanie równości eq do porównywania zdań nie ma zbyt wiele sensu. Jest tak dlatego, że nie interesuje nas postać owych zdań, a jedynie ich logiczna zawartość.
Z tego powodu właściwym dla zdań pojęciem "identyczności" jest równoważność, czyli <->. Podobnie jest w przypadku relacji: uznamy dwie relacje za identyczne, gdy dla wszystkich argumentów zwracają one równoważne zdania.
Formalnie wyrazimy to nieco na około, za pomocą pojęcia subrelacji. R jest subrelacją S, jeżeli R a b implikuje S a b dla wszystkich a : A i b : B. Możemy sobie wyobrażać, że jeżeli R jest subrelacją S, to w relacji R są ze sobą tylko niektóre pary argumentów, które są w relacji S, a inne nie.

Ćwiczenie


Inductive le' : nat -> nat -> Prop :=
    | le'_0 : forall n : nat, le' 0 n
    | le'_SS : forall n m : nat, le' n m -> le' (S n) (S m).

Udowodnij, że powyższa definicja le' porządku "mniejszy lub równy" na liczbach naturalnych jest tą samą relacją, co le. Być może przyda ci się kilka lematów pomocniczych.


Lemma le_le'_same : le <--> le'.

Uporawszy się z pojęciem "identyczności" relacji możemy przejść dalej, a mianowicie do operacji, jakie możemy wykonywać na relacjach.

Operacje na relacjach


Definition Rcomp
  {A B C : Type} (R : hrel A B) (S : hrel B C) : hrel A C :=
    fun (a : A) (c : C) => exists b : B, R a b /\ S b c.

Definition Rid {A : Type} : hrel A A := @eq A.

Podobnie jak w przypadku funkcji, najważniejszą operacją jest składanie relacji, a najważniejszą relacją — równość. Składanie jest łączne, zaś równość jest elementem neutralnym tego składania. Musimy jednak zauważyć, że mówiąc o łączności relacji mamy na myśli coś innego, niż w przypadku funkcji.

Lemma Rcomp_assoc :
  forall
    (A B C D : Type) (R : hrel A B) (S : hrel B C) (T : hrel C D),
      Rcomp R (Rcomp S T) <--> Rcomp (Rcomp R S) T.

Lemma Rid_left :
  forall (A B : Type) (R : hrel A B),
    Rcomp (@Rid A) R <--> R.

Lemma Rid_right :
  forall (A B : Type) (R : hrel A B),
    Rcomp R (@Rid B) <--> R.

Składanie funkcji jest łączne, gdyż złożenie trzech funkcji z dowolnie rozstawionymi nawiasami daje wynik identyczny w sensie eq. Składanie relacji jest łączne, gdyż złożenie trzech relacji z dowolnie rozstawionymi nawiasami daje wynik identyczny w sensie same_hrel.
Podobnie sprawa ma się w przypadku stwierdzenia, że eq jest elementem nautralnym składania relacji.

Definition Rinv {A B : Type} (R : hrel A B) : hrel B A :=
  fun (b : B) (a : A) => R a b.

Rinv to operacja, która zamienia miejscami argumenty relacji. Relację Rinv R będziemy nazywać relacją odwrotną do R.

Lemma Rinv_Rcomp :
  forall (A B C : Type) (R : hrel A B) (S : hrel B C),
    Rinv (Rcomp R S) <--> Rcomp (Rinv S) (Rinv R).

Lemma Rinv_Rid :
  forall A : Type, same_hrel (@Rid A) (Rinv (@Rid A)).

Złożenie dwóch relacji możemy odwrócić, składając ich odwrotności w odwrotnej kolejności. Odwrotnością relacji identycznościowej jest zaś ona sama.

Definition Rnot {A B : Type} (R : hrel A B) : hrel A B :=
  fun (a : A) (b : B) => ~ R a b.

Definition Rand {A B : Type} (R S : hrel A B) : hrel A B :=
  fun (a : A) (b : B) => R a b /\ S a b.

Definition Ror {A B : Type} (R S : hrel A B) : hrel A B :=
  fun (a : A) (b : B) => R a b \/ S a b.

Pozostałe trzy operacje na relacjach odpowiadają spójnikom logicznym — mamy więc negację relacji oraz koniunkcję i dysjunkcję dwóch relacji. Zauważ, że operacje te możemy wykonywać jedynie na relacjach o takich samych typach argumentów.
Sporą część naszego badania relacji przeznaczymy na sprawdzanie, jak powyższe operacj mają się do różnych specjalnych rodzajów relacji. Nim to się stanie, zbadajmy jednak właściwości samych operacji.

Definition RTrue {A B : Type} : hrel A B :=
  fun (a : A) (b : B) => True.

Definition RFalse {A B : Type} : hrel A B :=
  fun (a : A) (b : B) => False.

Zacznijmy od relacjowych odpowiedników True i False. Przydadzą się nam one do wyrażania właściwości Rand oraz Ror.


Lemma Rnot_double :
  forall (A B : Type) (R : hrel A B),
    R --> Rnot (Rnot R).

Lemma Rand_assoc :
  forall (A B : Type) (R S T : hrel A B),
    Rand R (Rand S T) <--> Rand (Rand R S) T.

Lemma Rand_comm :
  forall (A B : Type) (R S : hrel A B),
    Rand R S <--> Rand S R.

Lemma Rand_RTrue_l :
  forall (A B : Type) (R : hrel A B),
    Rand RTrue R <--> R.

Lemma Rand_RTrue_r :
  forall (A B : Type) (R : hrel A B),
    Rand R RTrue <--> R.

Lemma Rand_RFalse_l :
  forall (A B : Type) (R : hrel A B),
    Rand RFalse R <--> RFalse.

Lemma Rand_RFalse_r :
  forall (A B : Type) (R : hrel A B),
    Rand R RFalse <--> RFalse.

Lemma Ror_assoc :
  forall (A B : Type) (R S T : hrel A B),
    Ror R (Ror S T) <--> Ror (Ror R S) T.

Lemma Ror_comm :
  forall (A B : Type) (R S : hrel A B),
    Ror R S <--> Ror S R.

Lemma Ror_RTrue_l :
  forall (A B : Type) (R : hrel A B),
    Ror RTrue R <--> RTrue.

Lemma Ror_RTrue_r :
  forall (A B : Type) (R : hrel A B),
    Ror R RTrue <--> RTrue.

Lemma Ror_RFalse_l :
  forall (A B : Type) (R : hrel A B),
    Ror RFalse R <--> R.

Lemma Ror_RFalse_r :
  forall (A B : Type) (R : hrel A B),
    Ror R RFalse <--> R.

To nie wszystkie właściwości tych operacji, ale myślę, że widzisz już, dokąd to wszystko zmierza. Jako, że Rnot, Rand i Ror pochodzą bezpośrednio od spójników logicznych not, and i or, dziedziczą one po nich wszystkie ich właściwości.
Fenomen ten nie jest w żaden sposób specyficzny dla relacji i operacji na nich - z pewnością spotkamy się z nim ponownie w nadchodzących rozdziałach. Tymczasem przyjrzyjmy się bliżej specjalnym rodzajom relacji.

Rodzaje relacji heterogenicznych


Class LeftUnique {A B : Type} (R : hrel A B) : Prop :=
{
    left_unique :
      forall (a a' : A) (b : B), R a b -> R a' b -> a = a'
}.

Class RightUnique {A B : Type} (R : hrel A B) : Prop :=
{
    right_unique :
      forall (a : A) (b b' : B), R a b -> R a b' -> b = b'
}.

Dwoma podstawowymi rodzajami relacji są relacje unikalne z lewej i prawej strony. Relacja lewostronnie unikalna to taka, dla której każde b : B jest w relacji z co najwyżej jednym a : A. Analogicznie definiujemy relacje prawostronnie unikalne.

Instance LeftUnique_eq (A : Type) : LeftUnique (@eq A).

Instance RightUnique_eq (A : Type) : RightUnique (@eq A).

Najbardziej elementarną intuicję stojącą za tymi koncepcjami można przedstawić na przykładzie relacji równości: jeżeli dwa obiekty są równe jakiemuś trzeciemu obiektowi, to muszą być także równe sobie nawzajem.
Pojęcie to jest jednak bardziej ogólne i dotyczy także relacji, które nie są homogeniczne. W szczególności jest ono różne od pojęcia relacji przechodniej, które pojawi się już niedługo.

Instance LeftUnique_Rcomp :
  forall (A B C : Type) (R : hrel A B) (S : hrel B C),
    LeftUnique R -> LeftUnique S -> LeftUnique (Rcomp R S).

Instance RightUnique_Rcomp :
  forall (A B C : Type) (R : hrel A B) (S : hrel B C),
    RightUnique R -> RightUnique S -> RightUnique (Rcomp R S).

Składanie zachowuje oba rodzaje relacji unikalnych. Nie ma tu co za dużo filozofować — żeby się przekonać, narysuj obrazek. TODO.

Instance LeftUnique_Rinv :
  forall (A B : Type) (R : hrel A B),
    RightUnique R -> LeftUnique (Rinv R).

Instance RightUnique_Rinv :
  forall (A B : Type) (R : hrel A B),
    LeftUnique R -> RightUnique (Rinv R).

Już na pierwszy rzut oka widać, że pojęcia te są w pewien sposób symetryczne. Aby uchwycić tę symetrię, możemy posłużyć się operacją Rinv. Okazuje się, że zamiana miejscami argumentów relacji lewostronnie unikalnej daje relację prawostronnie unikalną i vice versa.

Instance LeftUnique_Rand :
  forall (A B : Type) (R S : hrel A B),
    LeftUnique R -> LeftUnique (Rand R S).

Instance RightUnique_Rand :
  forall (A B : Type) (R S : hrel A B),
    RightUnique R -> RightUnique (Rand R S).

Lemma Ror_not_LeftUnique :
  exists (A B : Type) (R S : hrel A B),
    LeftUnique R /\ LeftUnique S /\ ~ LeftUnique (Ror R S).

Lemma Ror_not_RightUnique :
  exists (A B : Type) (R S : hrel A B),
    RightUnique R /\ RightUnique S /\ ~ RightUnique (Ror R S).

Koniunkcja relacji unikalnej z inną daje relację unikalną, ale dysjunkcja nawet dwóch relacji unikalnych nie musi dawać w wyniku relacji unikalnej. Wynika to z interpretacji operacji na relacjach jako operacji na kolekcjach par.
Wyobraźmy sobie, że relacja R : hrel A B to kolekcja par p : A * B. Jeżeli para jest elementem kolekcji, to jej pierwszy komponent jest w relacji R z jej drugim komponentem. Dysjunkcję relacji R i S w takim układzie stanowi kolekcja, która zawiera zarówno pary z kolekcji odpowiadającej R, jak i te z kolekcji odpowiadającej S. Koniunkcja odpowiada kolekcji par, które są zarówno w kolekcji odpowiadającej R, jak i tej odpowiadającej S.
Tak więc dysjunkcja R i S może do R "dorzucić" jakieś pary, ale nie może ich zabrać. Analogicznie, koniunkcja R i S może zabrać pary z R, ale nie może ich dodać.
Teraz interpretacja naszego wyniku jest prosta. W przypadku relacji lewostronnie unikalnych jeżeli każde b : B jest w relacji z co najwyżej jednym a : A, to potencjalne zabranie jakichś par z tej relacji niczego nie zmieni. Z drugiej strony, nawet jeżeli obie relacje są lewostronnie unikalne, to dodanie do R par z S może spowodować wystąpienie powtórzeń, co niszczy unikalność.

Lemma Rnot_not_LeftUnique :
  exists (A B : Type) (R : hrel A B),
    LeftUnique R /\ ~ LeftUnique (Rnot R).

Lemma Rnot_not_RightUnique :
  exists (A B : Type) (R : hrel A B),
    LeftUnique R /\ ~ LeftUnique (Rnot R).

Negacja relacji unikalnej również nie musi być unikalna. Spróbuj podać interpretację tego wyniku z punktu widzenia operacji na kolekcjach par.

Ćwiczenie

Znajdź przykład relacji, która:


Class LeftTotal {A B : Type} (R : hrel A B) : Prop :=
{
    left_total : forall a : A, exists b : B, R a b
}.

Class RightTotal {A B : Type} (R : hrel A B) : Prop :=
{
    right_total : forall b : B, exists a : A, R a b
}.

Kolejnymi dwoma rodzajami heterogenicznych relacji binarnych są relacje lewo- i prawostronnie totalne. Relacja lewostronnie totalna to taka, że każde a : A jest w relacji z jakimś elementem B. Definicja relacji prawostronnie totalnej jest analogiczna.
Za pojęciem tym nie stoją jakieś wielkie intuicje: relacja lewostronnie totalna to po prostu taka, w której żaden element a : A nie jest "osamotniony".

Instance LeftTotal_eq :
  forall A : Type, LeftTotal (@eq A).

Instance RightTotal_eq :
  forall A : Type, RightTotal (@eq A).

Równość jest relacją totalną, gdyż każdy term x : A jest równy samemu sobie.

Instance LeftTotal_Rcomp :
  forall (A B C : Type) (R : hrel A B) (S : hrel B C),
    LeftTotal R -> LeftTotal S -> LeftTotal (Rcomp R S).

Instance RightTotal_Rcomp :
  forall (A B C : Type) (R : hrel A B) (S : hrel B C),
    RightTotal R -> RightTotal S -> RightTotal (Rcomp R S).

Instance RightTotal_Rinv :
  forall (A B : Type) (R : hrel A B),
    LeftTotal R -> RightTotal (Rinv R).

Instance LeftTotal_Rinv :
  forall (A B : Type) (R : hrel A B),
    RightTotal R -> LeftTotal (Rinv R).

Między lewo- i prawostronną totalnością występuje podobna symetria jak między dwoma formami unikalności: relacja odwrotna do lewostronnie totalnej jest prawostronnie totalna i vice versa. Totalność jest również zachowywana przez składanie.

Lemma Rand_not_LeftTotal :
  exists (A B : Type) (R S : hrel A B),
    LeftTotal R /\ LeftTotal S /\ ~ LeftTotal (Rand R S).

Lemma Rand_not_RightTotal :
  exists (A B : Type) (R S : hrel A B),
    RightTotal R /\ RightTotal S /\ ~ RightTotal (Rand R S).

Lemma LeftTotal_Ror :
  forall (A B : Type) (R S : hrel A B),
    LeftTotal R -> LeftTotal (Ror R S).

Lemma RightTotal_Ror :
  forall (A B : Type) (R S : hrel A B),
    RightTotal R -> RightTotal (Ror R S).

Związki totalności z koniunkcją i dysjunkcją relacji są podobne jak w przypadku unikalności, lecz tym razem to dysjunkcja zachowuje właściwość, a koniunkcja ją niszczy. Wynika to z tego, że dysjunkcja nie zabiera żadnych par z relacji, więc nie może uszkodzić totalności. Z drugiej strony koniunkcja może zabrać jakąś parę, a wtedy relacja przestaje być totalna.

Lemma Rnot_not_LeftTotal :
  exists (A B : Type) (R : hrel A B),
    RightTotal R /\ ~ RightTotal (Rnot R).

Lemma Rnot_not_RightTotal :
  exists (A B : Type) (R : hrel A B),
    RightTotal R /\ ~ RightTotal (Rnot R).

Negacja relacji totalnej nie może być totalna. Nie ma się co dziwić — negacja wyrzuca z relacji wszystkie pary, których w niej nie było, a więc pozbywa się czynnika odpowiedzialnego za totalność.

Ćwiczenie

Znajdź przykład relacji, która:
Bonusowe punkty za relację, która jest "naturalna", tzn. nie została wymyślona na chama specjalnie na potrzeby zadania.


Rodzaje relacji heterogenicznych v2

Poznawszy cztery właściwości, jakie relacje mogą posiadać, rozważymy teraz relacje, które posiadają dwie lub więcej z tych właściwości.

Class Functional {A B : Type} (R : hrel A B) : Prop :=
{
    F_LT :> LeftTotal R;
    F_RU :> RightUnique R;
}.

Lewostronną totalność i prawostronną unikalność możemy połączyć, by uzyskać pojęcie relacji funkcyjnej. Relacja funkcyjna to relacja, która ma właściwości takie, jak funkcje — każdy lewostronny argument a : A jest w relacji z dokładnie jednym b : B po prawej stronie.

Instance fun_to_Functional {A B : Type} (f : A -> B)
  : Functional (fun (a : A) (b : B) => f a = b).


Z każdej funkcji można w prosty sposób zrobić relację funkcyjną, ale bez dodatkowych aksjomatów nie jesteśmy w stanie z relacji funkcyjnej zrobić funkcji. Przemilczając kwestie aksjomatów możemy powiedzieć więc, że relacje funkcyjne odpowiadają funkcjom.

Instance Functional_eq :
  forall A : Type, Functional (@eq A).

Równość jest rzecz jasna relacją funkcyjną. Funkcją odpowiadającą relacji @eq A jest funkcja identycznościowa @id A.

Instance Functional_Rcomp :
  forall (A B C : Type) (R : hrel A B) (S : hrel B C),
    Functional R -> Functional S -> Functional (Rcomp R S).

Złożenie relacji funkcyjnych również jest relacją funkcyjną. Nie powinno nas to dziwić — wszakże relacje funkcyjne odpowiadają funkcjom, a złożenie funkcji jest przecież funkcją. Jeżeli lepiej mu się przyjrzeć, to okazuje się, że składanie funkcji odpowiada składaniu relacji, a stąd już prosta droga do wniosku, że złożenie relacji funkcyjnych jest relacją funkcyjną.

Lemma Rinv_not_Functional :
  exists (A B : Type) (R : hrel A B),
    Functional R /\ ~ Functional (Rinv R).

Odwrotność relacji funkcyjnej nie musi być funkcyjna. Dobrą wizualicją tego faktu może być np. funkcja f(x) = x^2 na liczbach rzeczywistych. Z pewnością jest to funkcja, a zatem relacja funkcyjna. Widać to na jej wykresie — każdemu punktowi dziedziny odpowiada dokładnie jeden punkt przeciwdziedziny. Jednak po wykonaniu operacji Rinv, której odpowiada tutaj obrócenie układu współrzędnych o 90 stopni, nie otrzymujemy wcale wykresu funkcji. Wprost przeciwnie — niektórym punktom z osi X na takim wykresie odpowiadają dwa punkty na osi Y (np. punktowi 4 odpowiadają 2 i -2). Stąd wnioskujemy, że odwrócenie relacji funkcyjnej f nie daje w wyniku relacji funkcyjnej.

Lemma Rand_not_Functional :
  exists (A B : Type) (R S : hrel A B),
    Functional R /\ Functional S /\ ~ Functional (Rand R S).

Lemma Ror_not_Functional :
  exists (A B : Type) (R S : hrel A B),
    Functional R /\ Functional S /\ ~ Functional (Ror R S).

Lemma Rnot_not_Functional :
  exists (A B : Type) (R : hrel A B),
    Functional R /\ ~ Functional (Rnot R).

Ani koniunkcje, ani dysjunkcje, ani negacje relacji funkcyjnych nie muszą być wcale relacjami funkcyjnymi. Jest to po części konsekwencją właściwości relacji lewostronnie totalnych i prawostronnie unikalnych: pierwsze mają problem z Rand, a drugie z Ror, oba zaś z Rnot.

Ćwiczenie

Możesz zadawać sobie pytanie: po co nam w ogóle pojęcie relacji funkcyjnej, skoro mamy funkcje? Funkcje muszą być obliczalne (ang. computable) i to na mocy definicji, zaś relacje — niekonieczne. Czasem prościej może być najpierw zdefiniować relację, a dopiero później pokazać, że jest funkcyjna. Czasem zdefiniowanie danego bytu jako funkcji może być niemożliwe.
Funkcję Collatza klasycznie definiuje się w ten sposób: jeżeli n jest parzyste, to f(n) = n/2. W przeciwnym przypadku f(n) = 3n + 1.
Zaimplementuj tę funkcję w Coqu. Spróbuj zaimplementować ją zarówno jako funkcję rekurencyjną, jak i relację. Czy twoja funkcja dokładnie odpowiada powyższej specyfikacji? Czy jesteś w stanie pokazać, że twoja relacja jest funkcyjna?
Udowodnij, że f(42) = 1.


Class Injective {A B : Type} (R : hrel A B) : Prop :=
{
    I_Fun :> Functional R;
    I_LU :> LeftUnique R;
}.

Instance inj_to_Injective :
  forall (A B : Type) (f : A -> B),
    injective f -> Injective (fun (a : A) (b : B) => f a = b).

Relacje funkcyjne, które są lewostronnie unikalne, odpowiadają funkcjom injektywnym.

Instance Injective_eq :
  forall A : Type, Injective (@eq A).

Instance Injective_Rcomp :
  forall (A B C : Type) (R : hrel A B) (S : hrel B C),
    Injective R -> Injective S -> Injective (Rcomp R S).

Lemma Rinv_not_Injective :
  exists (A B : Type) (R : hrel A B),
    Injective R /\ ~ Injective (Rinv R).

Lemma Rand_not_Injective :
  exists (A B : Type) (R S : hrel A B),
    Injective R /\ Injective S /\ ~ Injective (Rand R S).

Lemma Ror_not_Injective :
  exists (A B : Type) (R S : hrel A B),
    Injective R /\ Injective S /\ ~ Injective (Ror R S).

Lemma Rnot_not_Injective :
  exists (A B : Type) (R : hrel A B),
    Injective R /\ ~ Injective (Rnot R).

Właściwości relacji injektywnych są takie, jak funkcji injektywnych, gdyż te pojęcia ściśle sobie odpowiadają.

Ćwiczenie

Udowodnij, że powyższe zdanie nie kłamie.

Lemma injective_Injective :
  forall (A B : Type) (f : A -> B),
    injective f <-> Injective (fun (a : A) (b : B) => f a = b).
Proof.
  split.
    compute; intros. repeat split; intros.
      exists (f a). reflexivity.
      rewrite <- H0, <- H1. reflexivity.
      apply H. rewrite H0, H1. reflexivity.
    destruct 1 as [[[] []] []]. red. intros.
      apply left_unique0 with (f x').
        assumption.
        reflexivity.
Qed.

(* end hide *)

Class Surjective {A B : Type} (R : hrel A B) : Prop :=
{
    S_Fun :> Functional R;
    S_RT :> RightTotal R;
}.

Instance sur_to_Surjective :
  forall (A B : Type) (f : A -> B),
    surjective f -> Surjective (fun (a : A) (b : B) => f a = b).

Relacje funkcyjne, które są prawostronnie totalne, odpowiadają funkcjom surjektywnym.

Instance Surjective_eq :
  forall A : Type, Surjective (@eq A).

Instance Surjective_Rcomp :
  forall (A B C : Type) (R : hrel A B) (S : hrel B C),
    Surjective R -> Surjective S -> Surjective (Rcomp R S).

Lemma Rinv_not_Surjective :
  exists (A B : Type) (R : hrel A B),
    Surjective R /\ ~ Surjective (Rinv R).

Lemma Rand_not_Surjective :
  exists (A B : Type) (R S : hrel A B),
    Surjective R /\ Surjective S /\ ~ Surjective (Rand R S).

Lemma Ror_not_Surjective :
  exists (A B : Type) (R S : hrel A B),
    Surjective R /\ Surjective S /\ ~ Surjective (Ror R S).

Lemma Rnot_not_Surjective :
  exists (A B : Type) (R : hrel A B),
    Surjective R /\ ~ Surjective (Rnot R).

Właściwości relacji surjektywnych także są podobne do tych, jakie są udziałem relacji funkcyjnych.

Class Bijective {A B : Type} (R : hrel A B) : Prop :=
{
    B_Fun :> Functional R;
    B_LU :> LeftUnique R;
    B_RT :> RightTotal R;
}.

Instance bij_to_Bijective :
  forall (A B : Type) (f : A -> B),
    bijective f -> Bijective (fun (a : A) (b : B) => f a = b).

Relacje funkcyjne, które są lewostronnie totalne (czyli injektywne) oraz prawostronnie totalne (czyli surjektywne), odpowiadają bijekcjom.

Instance Bijective_eq :
  forall A : Type, Bijective (@eq A).

Instance Bijective_Rcomp :
  forall (A B C : Type) (R : hrel A B) (S : hrel B C),
    Bijective R -> Bijective S -> Bijective (Rcomp R S).

Instance Bijective_Rinv :
  forall (A B : Type) (R : hrel A B),
    Bijective R -> Bijective (Rinv R).

Lemma Rand_not_Bijective :
  exists (A B : Type) (R S : hrel A B),
    Bijective R /\ Bijective S /\ ~ Bijective (Rand R S).

Lemma Ror_not_Bijective :
  exists (A B : Type) (R S : hrel A B),
    Bijective R /\ Bijective S /\ ~ Bijective (Ror R S).

Lemma Rnot_not_Bijective :
  exists (A B : Type) (R : hrel A B),
    Bijective R /\ ~ Bijective (Rnot R).

Właściwości relacji bijektywnych różnią się jednym szalenie istotnym detalem od właściwości relacji funkcyjnych, injektywnych i surjektywnych: odwrotność relacji bijektywnej jest relacją bijektywną.

Rodzaje relacji homogenicznych


Definition rel (A : Type) : Type := hrel A A.

Relacje homogeniczne to takie, których wszystkie argumenty są tego samego typu. Warunek ten pozwala nam na wyrażenie całej gamy nowych właściwości, które relacje takie mogą posiadać.
Uwaga terminologiczna: w innych pracach to, co nazwałem Antireflexive bywa zazwyczaj nazywane Irreflexive. Ja przyjąłem następujące reguły tworzenia nazw różnych rodzajów relacji:

Zwrotność


Class Reflexive {A : Type} (R : rel A) : Prop :=
{
    reflexive : forall x : A, R x x
}.

Class Irreflexive {A : Type} (R : rel A) : Prop :=
{
    irreflexive : exists x : A, ~ R x x
}.

Class Antireflexive {A : Type} (R : rel A) : Prop :=
{
    antireflexive : forall x : A, ~ R x x
}.

Relacja R jest zwrotna (ang. reflexive), jeżeli każdy x : A jest w relacji sam ze sobą. Przykładem ze świata rzeczywistego może być relacja "x jest blisko y". Jest oczywiste, że każdy jest blisko samego siebie.

Instance Reflexive_empty :
  forall R : rel Empty_set, Reflexive R.

Okazuje się, że wszystkie relacje na Empty_set (a więc także na wszystkich innych typach pustych) są zwrotne. Nie powinno cię to w żaden sposób zaskakiwać — jest to tzw. pusta prawda (ang. vacuous truth), zgodnie z którą wszystkie zdania kwantyfikowane uniwersalnie po typie pustym są prawdziwe. Wszyscy w pustym pokoju są debilami.

Instance Reflexive_eq {A : Type} : Reflexive (@eq A).

Instance Reflexive_RTrue :
  forall A : Type, Reflexive (@RTrue A A).

Lemma RFalse_nonempty_not_Reflexive :
  forall A : Type, A -> ~ Reflexive (@RFalse A A).

Najważniejszym przykładem relacji zwrotnej jest równość. eq jest relacją zwrotną, gdyż ma konstruktor eq_refl, który głosi, że każdy obiekt jest równy samemu sobie. Zwrotna jest też relacja RTrue, gdyż każdy obiekt jest w jej przypadku w relacji z każdym, a więc także z samym sobą. Zwrotna nie jest za to relacja RFalse na typie niepustym, gdyż tam żaden obiekt nie jest w relacji z żadnym, a więc nie może także być w relacji z samym sobą.

Lemma eq_subrelation_Reflexive :
  forall (A : Type) (R : rel A), Reflexive R ->
    subrelation (@eq A) R.

Równość jest "najmniejszą" relacją zwrotną w tym sensie, że jest ona subrelacją każdej relacji zwrotnej. Intuicyjnym uzasadnieniem jest fakt, że w definicji eq poza konstruktorem eq_refl, który daje zwrotność, nie ma niczego innego.

Instance Reflexive_Rcomp :
  forall (A : Type) (R S : rel A),
    Reflexive R -> Reflexive S -> Reflexive (Rcomp R S).

Instance Reflexive_Rinv :
  forall (A : Type) (R : rel A),
    Reflexive R -> Reflexive (Rinv R).

Instance Reflexive_Rand :
  forall (A : Type) (R S : rel A),
    Reflexive R -> Reflexive S -> Reflexive (Rand R S).

Instance Reflexive_Ror :
  forall (A : Type) (R S : rel A),
    Reflexive R -> Reflexive (Ror R S).

Jak widać, złożenie, odwrotność i koniunkcja relacji zwrotnych są zwrotne. Dysjunkcja posiada natomiast dużo mocniejszą właściwość: dysjunkcja dowolnej relacji z relacją zwrotną daje relację zwrotną. Tak więc dysjunkcja R z eq pozwala nam łatwo "dodać" zwrotność do R. Słownie dysjunkcja z eq odpowiada zwrotowi "lub równy", który możemy spotkać np. w wyrażeniach "mniejszy lub równy", "większy lub równy".
Właściwością odwrotną do zwrotności jest antyzwrotność. Relacja antyzwrotna to taka, że żaden x : A nie jest w relacji sam ze sobą.

Instance Antireflexive_neq :
  forall (A : Type), Antireflexive (fun x y : A => x <> y).

Instance Antireflexive_lt : Antireflexive lt.

Typowymi przykładami relacji antyzwrotnych są nierówność <> oraz porządek "mniejszy niż" (<) na liczbach naturalnych. Ze względu na sposób działania ludzkiego mózgu antyzwrotna jest cała masa relacji znanych nam z codziennego życia: "x jest matką y", "x jest ojcem y", "x jest synem y", "x jest córką y", "x jest nad y", "x jest pod y", "x jest za y", "x jest przed y", etc.

Lemma Antireflexive_empty :
  forall R : rel Empty_set, Antireflexive R.

Lemma eq_nonempty_not_Antireflexive :
  forall A : Type, A -> ~ Antireflexive (@eq A).

Lemma RTrue_nonempty_not_Antireflexive :
  forall A : Type, A -> ~ Antireflexive (@RTrue A A).

Instance Antireflexive_RFalse :
  forall A : Type, Antireflexive (@RFalse A A).

Równość na typie niepustym nie jest antyzwrotna, gdyż jest zwrotna (wzajemne związki między tymi dwoma pojęciami zbadamy już niedługo). Antyzwrotna nie jest także relacja RTrue na typie niepustym, gdyż co najmniej jeden element jest w relacji z samym sobą. Antyzwrotna jest za to relacja pusta (RFalse).

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

Instance Antireflexive_Rinv :
  forall (A : Type) (R : rel A),
    Antireflexive R -> Antireflexive (Rinv R).

Instance Antireflexive_Rand :
  forall (A : Type) (R S : rel A),
    Antireflexive R -> Antireflexive (Rand R S).

Instance Antireflexive_Ror :
  forall (A : Type) (R S : rel A),
    Antireflexive R -> Antireflexive S -> Antireflexive (Ror R S).

Złożenie relacji antyzwrotnych nie musi być antyzwrotne, ale odwrotność i dysjunkcja już tak, zaś koniunkcja dowolnej relacji z relacją antyzwrotną daje nam relację antyzwrotną. Dzięki temu możemy dowolnej relacji R "zabrać" zwrotność koniunkcjując ją z <>.
Kolejną właściwością jest niezwrotność. Relacja niezwrotna to taka, która nie jest zwrotna. Zauważ, że pojęcie to zasadniczo różni się od pojęcia relacji antyzwrotnej: tutaj mamy kwantyfikator exists, tam zaś forall.

Instance Irreflexive_neq_nonempty :
  forall A : Type, A -> Irreflexive (Rnot (@eq A)).

Instance Irreflexive_gt : Irreflexive gt.

Typowym przykładem relacji niezwrotnej jest nierówność x <> y. Jako, że każdy obiekt jest równy samemu sobie, to żaden obiekt nie może być nierówny samemu sobie. Zauważ jednak, że typ A musi być niepusty, gdyż w przeciwnym wypadku nie mamy czego dać kwantyfikatorowi exists.
Innym przykładem relacji niezwrotnej jest porządek "większy niż" na liczbach naturalnych. Porządkami zajmiemy się już niedługo.

Lemma empty_not_Irreflexive :
  forall R : rel Empty_set, ~ Irreflexive R.

Lemma eq_empty_not_Irreflexive :
  ~ Irreflexive (@eq Empty_set).

Lemma eq_nonempty_not_Irreflexive :
  forall A : Type, A -> ~ Irreflexive (@eq A).

Równość jest zwrotna, a więc nie może być niezwrotna. Zauważ jednak, że musimy podać aż dwa osobne dowody tego faktu: jeden dla typu pustego Empty_set, a drugi dla dowolnego typu niepustego. Wynika to z tego, że nie możemy sprawdzić, czy dowolny typ A jest pusty, czy też nie.

Lemma RTrue_empty_not_Irreflexive :
  ~ Irreflexive (@RTrue Empty_set Empty_set).

Lemma RTrue_nonempty_not_Irreflexive :
  forall A : Type, A -> ~ Irreflexive (@RTrue A A).

Lemma RFalse_empty_not_Irreflexive :
  ~ Irreflexive (@RFalse Empty_set Empty_set).

Instance Irreflexive_RFalse_nonempty :
  forall A : Type, A -> Irreflexive (@RFalse A A).

Podobnej techniki możemy użyć, aby pokazać, że relacja pełna (RTrue) nie jest niezwrotna. Inaczej jest jednak w przypadku RFalse — na typie pustym nie jest ona niezwrotna, ale na dowolnym typie niepustym już owszem.

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

Złożenie relacji niezwrotnych nie musi być niezwrotne. Przyjrzyj się uważnie definicji Rcomp, a z pewnością uda ci się znaleźć jakiś kontrprzykład.

Instance Irreflexive_Rinv :
  forall (A : Type) (R : rel A),
    Irreflexive R -> Irreflexive (Rinv R).

Instance Irreflexive_Rand :
  forall (A : Type) (R S : rel A),
    Irreflexive R -> Irreflexive (Rand R S).

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

Odwrotność relacji niezwrotnej jest niezwrotna. Koniunkcja dowolnej relacji z relacją niezwrotną daje relację niezwrotną. Tak więc za pomocą koniunkcji i dysjunkcji możemy łatwo dawać i zabierać zwrotność różnym relacjom. Okazuje się też, że dysjunkcja nie zachowuje niezwrotności.
Na zakończenie zbadajmy jeszcze, jakie związki zachodzą pomiędzy zwrotnością, antyzwrotnością i niezwrotnością.

Instance Reflexive_Rnot :
  forall (A : Type) (R : rel A),
    Antireflexive R -> Reflexive (Rnot R).

Instance Antireflexive_Rnot :
  forall (A : Type) (R : rel A),
    Reflexive R -> Antireflexive (Rnot R).

Podstawowa zależność między nimi jest taka, że negacja relacji zwrotnej jest antyzwrotna, zaś negacja relacji antyzwrotnej jest zwrotna.

Lemma Reflexive_Antireflexive_empty :
  forall R : rel Empty_set, Reflexive R /\ Antireflexive R.

Lemma Reflexive_Antireflexive_nonempty :
  forall (A : Type) (R : rel A),
    A -> Reflexive R -> Antireflexive R -> False.

Każda relacja na typie pustym jest jednocześnie zwrotna i antyzwrotna, ale nie może taka być żadna relacja na typie niepustym.

Instance Irreflexive_nonempty_Antireflexive :
  forall (A : Type) (R : rel A),
    A -> Antireflexive R -> Irreflexive R.

Związek między niezwrotnością i antyzwrotnością jest nadzwyczaj prosty: każda relacja antyzwrotna na typie niepustym jest też niezwrotna.

Symetria


Class Symmetric {A : Type} (R : rel A) : Prop :=
{
    symmetric : forall x y : A, R x y -> R y x
}.

Class Antisymmetric {A : Type} (R : rel A) : Prop :=
{
    antisymmetric : forall x y : A, R x y -> ~ R y x
}.

Class Asymmetric {A : Type} (R : rel A) : Prop :=
{
    asymmetric : exists x y : A, R x y /\ ~ R y x
}.

Relacja jest symetryczna, jeżeli kolejność podawania argumentów nie ma znaczenia. Przykładami ze świata rzeczywistego mogą być np. relacje "jest blisko", "jest obok", "jest naprzeciwko".

Lemma Symmetric_char :
  forall (A : Type) (R : rel A),
    Symmetric R <-> same_hrel (Rinv R) R.

Alterntywną charakteryzacją symetrii może być stwierdzenie, że relacja symetryczna to taka, która jest swoją własną odwrotnością.

Instance Symmetric_eq :
  forall A : Type, Symmetric (@eq A).

Instance Symmetric_RTrue :
  forall A : Type, Symmetric (@RTrue A A).

Instance Symmetric_RFalse :
  forall A : Type, Symmetric (@RFalse A A).

Równość, relacja pełna i pusta są symetryczne.

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

Złożenie relacji symetrycznych nie musi być symetryczne.

Instance Symmetric_Rinv :
  forall (A : Type) (R : rel A),
    Symmetric R -> Symmetric (Rinv R).

Instance Symmetric_Rand :
  forall (A : Type) (R S : rel A ),
    Symmetric R -> Symmetric S -> Symmetric (Rand R S).

Instance Symmetric_Ror :
  forall (A : Type) (R S : rel A ),
    Symmetric R -> Symmetric S -> Symmetric (Ror R S).

Instance Symmetric_Rnot :
  forall (A : Type) (R : rel A ),
    Symmetric R -> Symmetric (Rnot R).

Pozostałe operacje (odwracanie, koniunkcja, dysjunkcja, negacja) zachowują symetrię.
Relacja antysymetryczna to przeciwieństwo relacji symetrycznej — jeżeli x jest w relacji z y, to y nie może być w relacji z x. Sporą klasę przykładów stanowią różne relacje służące do porównywania: "x jest wyższy od y", "x jest silniejszy od y", "x jest bogatszy od y".

Lemma Antisymmetric_empty :
  forall R : rel Empty_set, Antisymmetric R.

Lemma eq_nonempty_not_Antisymmetric :
  forall A : Type, A -> ~ Antisymmetric (@eq A).

Lemma RTrue_nonempty_not_Antisymmetric :
  forall A : Type, A -> ~ Antisymmetric (@RTrue A A).

Instance RFalse_Antiymmetric :
  forall A : Type, Antisymmetric (@RFalse A A).

Każda relacja na typie pustym jest antysymetryczna. Równość nie jest antysymetryczna, podobnie jak relacja pełna (ale tylko na typie niepustym). Relacja pusta jest antysymetryczna, gdyż przesłanka R x y występująca w definicji antysymetrii jest zawsze fałszywa.


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

Instance Antisymmetric_Rinv :
  forall (A : Type) (R : rel A),
    Antisymmetric R -> Antisymmetric (Rinv R).

Instance Antisymmetric_Rand :
  forall (A : Type) (R S : rel A),
    Antisymmetric R -> Antisymmetric (Rand R S).

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

Lemma Rnot_not_Antisymmetric :
  exists (A : Type) (R : rel A),
    Antisymmetric R /\ ~ Antisymmetric (Rnot R).

Lemma empty_not_Asymmetric :
  forall R : rel Empty_set, ~ Asymmetric R.

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

Instance Asymmetric_Rinv :
  forall (A : Type) (R : rel A),
    Asymmetric R -> Asymmetric (Rinv R).

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

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

Przechodniość (TODO)


Class Transitive {A : Type} (R : rel A) : Prop :=
{
    transitive : forall x y z : A, R x y -> R y z -> R x z
}.

Instance Transitive_eq :
  forall A : Type, Transitive (@eq A).

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

Instance Transitive_Rinv :
  forall (A : Type) (R : rel A),
    Transitive R -> Transitive (Rinv R).

Instance Transitive_Rand :
  forall (A : Type) (R S : rel A),
    Transitive R -> Transitive S -> Transitive (Rand R S).

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

Lemma Rnot_not_Transitive :
  exists (A : Type) (R : rel A),
    Transitive R /\ ~ Transitive (Rnot R).

Inne (TODO)


Class Total {A : Type} (R : rel A) : Prop :=
{
    total : forall x y : A, R x y \/ R y x
}.


Instance Total_Rinv :
  forall (A : Type) (R : rel A),
    Total R -> Total (Rinv R).


Instance Total_Ror :
  forall (A : Type) (R S : rel A),
    Total R -> Total S -> Total (Ror R S).

Lemma Rnot_not_Total :
  exists (A : Type) (R : rel A),
    Total R /\ ~ Total (Rnot R).

Instance Total_Reflexive :
  forall (A : Type) (R : rel A),
    Total R -> Reflexive R.

Class Trichotomous {A : Type} (R : rel A) : Prop :=
{
    trichotomous : forall x y : A, R x y \/ x = y \/ R y x
}.

Instance Trichotomous_empty :
  forall R : rel Empty_set, Trichotomous R.

Instance Trichotomous_eq_singleton :
  forall A : Type, (forall x y : A, x = y) -> Trichotomous (@eq A).

Instance Total_Trichotomous :
  forall (A : Type) (R : rel A),
    Total R -> Trichotomous R.

Lemma eq_not_Trichotomous :
  exists A : Type, ~ Trichotomous (@eq A).


Instance Trichotomous_Rinv :
  forall (A : Type) (R : rel A),
    Trichotomous R -> Trichotomous (Rinv R).



Lemma Rnot_not_Trichotomous :
  exists (A : Type) (R : rel A),
    Trichotomous R /\ ~ Trichotomous (Rnot R).

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

Instance Dense_eq :
  forall A : Type, Dense (@eq A).

Instance Dense_Rinv :
  forall (A : Type) (R : rel A),
    Dense R -> Dense (Rinv R).



Instance Dense_Ror :
  forall (A : Type) (R S : rel A),
    Dense R -> Dense S -> Dense (Ror R S).


Relacje równoważności (TODO)


Class Equivalence {A : Type} (R : rel A) : Prop :=
{
    Equivalence_Reflexive :> Reflexive R;
    Equivalence_Symmetric :> Symmetric R;
    Equivalence_Transitive :> Transitive R;
}.

Instance Equivalence_eq :
  forall A : Type, Equivalence (@eq A).


Instance Equivalence_Rinv :
  forall (A : Type) (R : rel A),
    Equivalence R -> Equivalence (Rinv R).

Instance Equivalence_Rand :
  forall (A : Type) (R S : rel A),
    Equivalence R -> Equivalence S -> Equivalence (Rand R S).

Inductive Threee : Type := One | Two | Three.



Relacje apartheidu (TODO)


Class Apartness {A : Type} (R : A -> A -> Prop) : Prop :=
{
    Apartness_Antireflexive :> Antireflexive R;
    Apartness_Symmetric :> Symmetric R;
    Apartness_Cotransitive :
      forall x y : A, R x y -> forall z : A, R x z \/ R z y;
}.

Instance Apartness_Rinv :
  forall (A : Type) (R : rel A),
    Apartness R -> Apartness (Rinv R).

Instance Apartness_Ror :
  forall (A : Type) (R S : rel A),
    Apartness R -> Apartness S -> Apartness (Ror R S).

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

Słabe relacje homogeniczne (TODO)



Class Univalent {A : Type} (R : rel A) : Prop :=
{
    univalent : forall x y : A, R x y -> R y x -> x = y
}.

Instance Univalent_eq :
  forall A : Type, Univalent (@eq A).

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

Instance Univalent_Rinv :
  forall (A : Type) (R : rel A),
    Univalent R -> Univalent (Rinv R).

Instance Univalent_Rand :
  forall (A : Type) (R S : rel A),
    Univalent R -> Univalent S ->
      Univalent (Rand R S).

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

Lemma Rnot_not_Univalent :
  exists (A : Type) (R : rel A),
    Univalent R /\ ~ Univalent (Rnot R).

Class Univalent' {A : Type} {E : rel A}
  (H : Equivalence E) (R : rel A) : Prop :=
{
    wasym : forall x y : A, R x y -> R y x -> E x y
}.

Instance Univalent_equiv :
  forall (A : Type) (E : rel A) (H : Equivalence E),
    Univalent' H E.

Lemma Rcomp_not_Univalent' :
  exists (A : Type) (E R S : rel A), forall H : Equivalence E,
    Univalent' H R /\ Univalent' H S /\
      ~ Univalent' H (Rcomp R S).

Instance Univalent'_Rinv :
  forall (A : Type) (E : rel A) (H : Equivalence E) (R : rel A),
    Univalent' H R -> Univalent' H (Rinv R).

Instance Univalent'_Rand :
  forall (A : Type) (E : rel A) (H : Equivalence E) (R S : rel A),
    Univalent' H R -> Univalent' H S ->
      Univalent' H (Rand R S).

Lemma Ror_not_Univalent' :
  exists (A : Type) (E R S : rel A), forall H : Equivalence E,
    Univalent' H R /\ Univalent' H S /\
      ~ Univalent' H (Ror R S).

Lemma Rnot_not_Univalent' :
  exists (A : Type) (E R : rel A), forall H : Equivalence E,
    Univalent' H R /\ ~ Univalent' H (Rnot R).

Złożone relacje homogeniczne (TODO)


Class Preorder {A : Type} (R : rel A) : Prop :=
{
    Preorder_refl :> Reflexive R;
    Preorder_trans :> Transitive R;
}.

Class PartialOrder {A : Type} (R : rel A) : Prop :=
{
    PartialOrder_Preorder :> Preorder R;
    PartialOrder_Univalent :> Univalent R;
}.

Class TotalOrder {A : Type} (R : rel A) : Prop :=
{
    TotalOrder_PartialOrder :> PartialOrder R;
    TotalOrder_Total : Total R;
}.

Class StrictPreorder {A : Type} (R : rel A) : Prop :=
{
    StrictPreorder_Antireflexive :> Antireflexive R;
    StrictPreorder_Transitive :> Transitive R;
}.

Class StrictPartialOrder {A : Type} (R : rel A) : Prop :=
{
    StrictPartialOrder_Preorder :> StrictPreorder R;
    StrictPartialOrder_Univalent :> Antisymmetric R;
}.

Class StrictTotalOrder {A : Type} (R : rel A) : Prop :=
{
    StrictTotalOrder_PartialOrder :> StrictPartialOrder R;
    StrictTotalOrder_Total : Total R;
}.

Domknięcia (TODO)


Require Import Classes.RelationClasses.

Uwaga, najnowszy pomysł: przedstawić domknięcia w taki sposób, żeby niepostrzeżenie przywyczajały do monad.

Class Closure
  {A : Type}
  (Cl : (A -> A -> Prop) -> (A -> A -> Prop)) : Prop :=
{
    pres :
      forall R S : A -> A -> Prop,
        (forall x y : A, R x y -> S x y) ->
          forall x y : A, Cl R x y -> Cl S x y;
    step :
      forall R : A -> A -> Prop,
        forall x y : A, R x y -> Cl R x y;
    join :
      forall R : A -> A -> Prop,
        forall x y : A, Cl (Cl R) x y -> Cl R x y;
}.

Inductive refl_clos {A : Type} (R : rel A) : rel A :=
    | rc_step : forall x y : A, R x y -> refl_clos R x y
    | rc_refl : forall x : A, refl_clos R x x.

#[refine]
Instance Closure_refl_clos {A : Type} : Closure (@refl_clos A) :=
{
    step := rc_step;
}.
Proof.
  induction 2.
    constructor. apply H. assumption.
    constructor 2.
  inversion 1; subst.
    assumption.
    constructor 2.
Qed.


Instance Reflexive_rc :
  forall (A : Type) (R : rel A), Reflexive (refl_clos R).

Lemma subrelation_rc :
  forall (A : Type) (R : rel A), subrelation R (refl_clos R).

Lemma rc_smallest :
  forall (A : Type) (R S : rel A),
    subrelation R S -> Reflexive S -> subrelation (refl_clos R) S.

Lemma rc_idempotent :
  forall (A : Type) (R : rel A),
    refl_clos (refl_clos R) <--> refl_clos R.

Lemma rc_Rinv :
  forall (A : Type) (R : rel A),
    Rinv (refl_clos (Rinv R)) <--> refl_clos R.

Inductive symm_clos {A : Type} (R : rel A) : rel A :=
    | sc_step :
        forall x y : A, R x y -> symm_clos R x y
    | sc_symm :
        forall x y : A, symm_clos R x y -> symm_clos R y x.


Instance Symmetric_sc :
  forall (A : Type) (R : rel A), Symmetric (symm_clos R).

Lemma subrelation_sc :
  forall (A : Type) (R : rel A), subrelation R (symm_clos R).

Lemma sc_smallest :
  forall (A : Type) (R S : rel A),
    subrelation R S -> Symmetric S -> subrelation (symm_clos R) S.

Lemma sc_idempotent :
  forall (A : Type) (R : rel A),
    symm_clos (symm_clos R) <--> symm_clos R.

Lemma sc_Rinv :
  forall (A : Type) (R : rel A),
    Rinv (symm_clos (Rinv R)) <--> symm_clos R.

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


Instance Transitive_tc :
  forall (A : Type) (R : rel A), Transitive (trans_clos R).

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

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

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

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

Inductive equiv_clos {A : Type} (R : rel A) : rel A :=
  | ec_step :
      forall x y : A, R x y -> equiv_clos R x y
  | ec_refl :
      forall x : A, equiv_clos R x x
  | ec_symm :
      forall x y : A, equiv_clos R x y -> equiv_clos R y x
  | ec_trans :
      forall x y z : A,
        equiv_clos R x y -> equiv_clos R y z -> equiv_clos R x z.


Instance Equivalence_ec :
  forall (A : Type) (R : rel A), Equivalence (equiv_clos R).

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

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

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

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

Domknięcie zwrotnosymetryczne


Definition rsc {A : Type} (R : rel A) : rel A :=
  refl_clos (symm_clos R).


Instance Reflexive_rsc :
  forall (A : Type) (R : rel A), Reflexive (rsc R).

Instance Symmetric_rsc :
  forall (A : Type) (R : rel A), Symmetric (rsc R).

Lemma subrelation_rsc :
  forall (A : Type) (R : rel A), subrelation R (rsc R).

Lemma rsc_smallest :
  forall (A : Type) (R S : rel A),
    subrelation R S -> Reflexive S -> Symmetric S ->
      subrelation (rsc R) S.

Lemma rsc_idempotent :
  forall (A : Type) (R : rel A),
    rsc (rsc R) <--> rsc R.

Lemma rsc_Rinv :
  forall (A : Type) (R : rel A),
    Rinv (rsc (Rinv R)) <--> rsc R.

Domknięcie równoważnościowe v2


Definition rstc {A : Type} (R : rel A) : rel A :=
  trans_clos (symm_clos (refl_clos R)).

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

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

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

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.

Lemma subrelation_rstc :
  forall (A : Type) (R : rel A), subrelation R (rstc R).

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

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

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

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

Instance Equivalence_same_hrel :
  forall A B : Type,
    Equivalence (@same_hrel A B).

Lemma rstc_idempotent :
  forall (A : Type) (R : rel A),
    rstc (rstc R) <--> rstc R.
Proof.
  split.
    induction 1.
      induction H.
        induction H.
          assumption.
          reflexivity.
        symmetry. assumption.
      rewrite IHtrans_clos1. assumption.
    repeat intro. do 3 constructor. assumption.
Qed.
(* end hide *)


Redukcje (TODO)


Definition rr {A : Type} (R : rel A) : rel A :=
  fun x y : A => R x y /\ x <> y.

Instance Antireflexive_rr :
  forall (A : Type) (R : rel A), Antireflexive (rr R).

Definition LEM : Prop :=
  forall P : Prop, P \/ ~ P.

Lemma rr_rc :
  LEM ->
    forall (A : Type) (R : rel A),
      Reflexive R -> refl_clos (rr R) <--> R.