「SF-LC」11 Rel

relation 与injective/surjective/bijective function 等相关的知识在 5. Tactics 里，为了避免每次都要 grep 我在这里写一下。

Relations

Recalling Relation

from FCT/TAPL/Wiki…

a possible connection between the components of a k-tuple.

I have been long confused with Unary Relations vs. Binary Relation on the Same Set (homogeneous relation) I thought they were same…but turns out they are totally different!

Unary/1-place relation is Predicate or Property!

Either defined via set X ⊆ P or x ∈ P, or defined via function P : X -> Bool or P : X -> {⊥, ⊤}. (usually used in Math. Logic)

Property = Indicator Fn = characteristic Fn = Boolean Predicate Fn = Predicate

• https://en.wikipedia.org/wiki/Property_(mathematics)
• https://en.wikipedia.org/wiki/Indicator_function

Binary Relation/2-place relation

Defined via two sets : R ⊆ X × Y or x, y ∈ R or xRy. (where x ∈ X, y ∈ Y.) or via function R: X × Y -> Bool.

Homogeneous Relation 同类（的）关系

Specifically! when X = Y, is called a homogeneous relation:

Noticed that we are still concerning relations of 2 elements!!, but they are from the same Set! (while 1-place relation concerning only 1 element.)

R ⊆ X × X
xRy where x ∈ X, y ∈ X

it’s written/spoken Binary relation on/over Set X. Properties e.g. reflexive, symmetric, transitive, are all properties of “Homogeneous Relation”!

Back to Coq

“relation” is a general idea. but in Coq standard lib it means “binary relation on a set X”

Coq identifier relation will always refer to a binary relation between some set and itself.

it’s defined as a family of Prop parameterized by two elements of X:

Definition relation (X: Type) := X → X → Prop.

Check le : nat -> nat -> Prop.
Check le : relation nat.

Basic Properties

ways to classifying relations. so theorems can be proved generically about certain sorts of relations

It’s pretty fun to see all mathematical things defined in Coq! (much more constructive)

Partial Function

function is defined as a special kind of binary relation.

Definition partial_function {X: Type} (R: relation X) :=
  ∀x y1 y2 : X, R x y1 → R x y2 → y1 = y2.

meaning that foreach input x ∈ X, there is a unique y ∈ Y corresponded.

But this only establish a partial function. because it doesn’t say anything about totality, to define total function, we require f map every x ∈ X.

• Total “Relation” ∀x ∀y (x ∈ X ∧ y ∈ X) ⇒ (xRy ∨ yRx).

totally different with total function but ask the binary relation holds between every pair.

Reflexive

Definition transitive {X: Type} (R: relation X) :=
  ∀a b c : X, (R a b) → (R b c) → (R a c).

Transitive

Definition transitive {X: Type} (R: relation X) :=
  ∀a b c : X, (R a b) → (R b c) → (R a c).

Symmetric & Antisymmetric

Definition symmetric {X: Type} (R: relation X) :=
  ∀a b : X, (R a b) → (R b a).
  
Definition antisymmetric {X: Type} (R: relation X) :=
  ∀a b : X, (R a b) → (R b a) → a = b.

Antisymmetric vs Asymmetric vs Non-symmetric (反对称 vs. 非对称 vs. 不-对称)

A relation is asymmetric if and only if it is both antisymmetric and irreflexive e.g. <= is neither symmetric nor asymmetric, but it’s antisymmetric… 反对称: 可以自反 (只能 reflexive 时对称) <= 非对称: 不能自反 < 不对称: 不是对称

Equivalence

Definition equivalence {X:Type} (R: relation X) :=
  (reflexive R) ∧ (symmetric R) ∧ (transitive R).

Partial Orders

A partial order under which every pair of elements is comparable is called a total order or linear order In the Coq standard library it’s called just order for short:

Definition order {X:Type} (R: relation X) :=
  (reflexive R) ∧ (antisymmetric R) ∧ (transitive R).

Preorders

a.k.a quasiorder

The subtyping relations are usually preorders.

(TAPL p185) because of the record permutation rule…there are many pairs of distinct types where each is a subtype of the other.

Definition preorder {X:Type} (R: relation X) :=
  (reflexive R) ∧ (transitive R).

Reflexive, Transitive Closure

Closure#Binary_relation_closures) Closure can be considered as Operations on bin-rel

As properties such as reflexive, transitive, the blah blah Closure are only talking about “homogeneous relations” i.e., Relation on a SINGLE set.

Reflexive Closure

Def. smallest reflexive relation on X containing R.

Operationally, as a = operator on a binary relation R:

R⁼ = R ∪ { (x, x) | x ∈ X }

and this obviously satisfy R⁼ ⊇ R.

Transitive Closure

Def. smallest transitive relation on X containing R.

Operationally, as a + operator on a binary relation R:

R+ = R ∪ { (x1,xn) | n > 1 ∧ (x1,x2), ..., (xn-1,xn) ∈ R }

We can also constructively and inductively definition using R^i where i = i-transitivity away.

Reflexive, Transitive Closure

R* = R⁼ ∪ R+

Why is it useful?

The idea is that a relation is extended s.t. the derived relation has the (reflexsive and) transitive property. — Prof. Arthur e.g. the “descendant” relation is the transitive closure of the “child” relation, the “derives-star (⇒⋆)” relation is the reflexive-transitive closure of the “derives (⇒)” relation. the “ε-closure” relation is the reflexive-transitive closure of the “ε-transition” relation. the “Kleene-star (Σ⋆)” relation is the reflexive-transitive closure of the “concatentation” relation.

Another way is to think them as “set closed under some operation”.

Back to Coq

Inductive clos_refl_trans {A: Type} (R: relation A) : relation A :=
  | rt_step x y (H : R x y) : clos_refl_trans R x y        (** original relation **)
  | rt_refl x : clos_refl_trans R x x                      (** reflexive  xRx              **)
  | rt_trans x y z                                         (** transitive xRy ∧ yRz → xRz  **)
        (Hxy : clos_refl_trans R x y)
        (Hyz : clos_refl_trans R y z) :
        clos_refl_trans R x z.

The above version will generate 2 IHs in rt_trans case. (since the proof tree has 2 branches).

Here is a better “linked-list”-ish one. (we will exclusively use this style)

Inductive clos_refl_trans_1n {A : Type} (R : relation A) (x : A) : A → Prop :=
  | rt1n_refl : clos_refl_trans_1n R x x
  | rt1n_trans (y z : A)
      (Hxy   : R x y) 
      (Hrest : clos_refl_trans_1n R y z) :
      clos_refl_trans_1n R x z.

In later chapter, we will define a decorator multi that can take any binary relation on a set and return its closure relation:

Inductive multi (X : Type) (R : relation X) : relation X :=
  | multi_refl : forall x     : X,                         multi R x x
  | multi_step : forall x y z : X, R x y -> multi R y z -> multi R x z

We name it step, standing for doing one step of this relation, and then we still have the rest (sub-structure) satisfied the closure relation.