Closure Operations on Endorelations

Reflexive Closure

Recall that for an endorelation, e, to be reflexive, e must relate every value in its domain of definition to itself.

The reflexive closure of such a relation e is the smallest relation that contains e (relates all of the pairs related by e) and that also relates every value in the entire domain of definition to itself.

We will give two definitions of this operation. The first is as an inductive definition, and the second as a function that takes any endorelation and returns the relation that is its reflexive closure.

Here's the inductive definition, called ReflClosure. To use it, you apply it to any endorelation, called r here, and you get back a relation with two constructors for proving that any given pair is in this relation. The first constructor assures that every pair in e qualifies as a member. The second one assures that for any a, e a a holds. That is, every pair of a value with itself is in the reflexive closure.

inductive ReflClosure {α : Type u} (r : α → α → Prop) : α → α → Prop
| base  {a b : α} : r a b → ReflClosure r a b
| refl  (a : α)   : ReflClosure r a a

We can also define a reflexive closure function that, when applied to any endorelation returns the relation (represented as a membership predicate) that is its reflexive closure.

def reflexiveClosure' : Rel α α → Rel α α :=
  fun (e : Rel α α) (a b : α) => e a b ∨ a = b

def reflexiveClosure := fun (a b : α) => e a b ∨ a = b

Symmetric Closure

Similarly, the symmetric closure of an endorelation, e, is the smallest relation that contains e and has the fewest additional pairs needed to make it symmetric. Note that if e is empty, so is its symmetric closure, whereas the reflexive closure of an empty relation having a domain of definition that is not empty is never empty.

inductive SymmetricClosure {α : Type u} (r : α → α → Prop) : α → α → Prop
| base  {a b : α} : r a b → SymmetricClosure r a b
| flip  {a b : α} : r b a → SymmetricClosure r a b

def symmetricClosure {α : Type u} (r : α → α → Prop) : α → α → Prop :=
  fun a b => r a b ∨ r b a

Transitive Closure

inductive TransitiveClosure {α : Type u} (r : α → α → Prop) : α → α → Prop
| base  {a b : α} : r a b → TransitiveClosure r a b
| step  {a b c : α} : TransitiveClosure r a b → TransitiveClosure r b c → TransitiveClosure r a c

A functional form of this definition, taking a relation and returning its transitive closure, is more complicated, and not worth the time it'd take to introduce it here.

Reflexive Transitive Closure

It's often useful to deal with the reflexive and transitive closure of an endorelation, e. This requires only the addition of a refl constructor to the definition of transitive closure.

inductive ReflexiveTransitiveClosure {α : Type u} (r : α → α → Prop) : α → α → Prop
| base  {a b : α} : r a b → ReflexiveTransitiveClosure r a b
| refl  (a : α) : ReflexiveTransitiveClosure r a a
| step  {a b c : α} :
    ReflexiveTransitiveClosure r a b →
    ReflexiveTransitiveClosure r b c →
    ReflexiveTransitiveClosure r a c

As an interesting aside, first-order predicate logic is not expressive enough to be able to express the claim that even a specific relation is transitive, not to mention formalizing the property of being transitive generalized over all relations.

Thus ends our section on properties of relations.

end properties

Proving Properties of Relations

To prove that some relation, r, has some property P, assert and and show that there is a proof of (P r).

As an example, let's assert and prove that equality on the natural numbers is total. In other words, we claim that there's a proof of the proposition, isTotal (@Eq Nat). Recall that the @ disables the inference of implement arguments, here allowing the type, Nat, to be given explicitly.

One of the first steps in getting to a proof of such a proposition is to reduce the name of the property, such as isTotalRel, to its definition, and in Lean to its representation, as a logical predicate.

In an English language proof, you might say, "By the definition of isTotalRel, it will suffice for us to to show that ∀ x, ∃ y, r x y." You then go on to prove that more transparent form of the basic proposition at hand.

In Lean it's the same. You can unfold (expand) the definition of a term, such as isTotalRel, in a larger expression using the unfold tactic.

example : isTotalRel (@Eq Nat) :=
  by
    unfold isTotalRel
    sorry     -- Exercise!

Exercises

A Reflexive Endorelation is Necessarily Total

example : isReflexiveRel e → isTotalRel e :=
by
  intro h
  unfold isReflexiveRel at h
  unfold isTotalRel
  intro a
  use a
  exact (h a)

Equality is an Equivalence Relation.

To show that that equality on a type, α, (@Eq α), is an equivalence relation, we have to show that it's reflexive, symmetric, and transitive. We'll give the proof in a bottom up style, first proving each of the conjuncts, then composing them into a proof of the overall conjecture.

-- equality is reflective
theorem eqIsRefl {α : Type}: isReflexiveRel (@Eq α) :=
  fun _ => rfl

-- equality is symmetric
theorem eqIsSymm : @isSymmetricRel α (@Eq α) :=
  -- prove that for any a, b, if a = b ∈ r then b = a
  -- use proof of a = b to rewrite a to b in b = a
  -- yielding b = b, which Lean then proves using rfl
  fun (a b : α) (hab : a = b) =>
    by rw [hab]


-- equality is transitive
theorem eqIsTrans : @isTransitiveRel α (@Eq α) :=
  -- similar to last proof
  fun (a b c : α) (hab : a = b) (hbc : b = c) =>
    by rw [hab, hbc]

-- equality is an equivalence relation
theorem eqIsEquiv {α β: Type}: @isEquivalence α (@Eq α) :=
  -- just need to prove that Eq is refl,, symm, and trans
  ⟨ eqIsRefl, ⟨ eqIsSymm, eqIsTrans ⟩ ⟩ -- And.intros

The ⊆ Relation is a Partial Order

def subSetRel {α : Type} : Rel (Set α) (Set α) :=
  fun (s t : Set α) => s ⊆ t

#reduce @subSetRel
-- fun {α} s t => ∀ ⦃a : α⦄, a ∈ s → t a


example {α : Type}: (@isPartialOrder (Set α) (@subSetRel α))  :=
  And.intro
    -- @isReflexive α β r
    -- by the definition of isReflexive, show ∀ a, r a a
    (fun s =>               -- for any set
      fun a =>              -- for any a ∈ s
        fun ains => ains    -- a ∈ s
    )
    (
      And.intro
        -- @isAntisymmetric α β r
        -- ∀ (a b : α), r a b → r b a → a = b
        (
          fun (s1 s2 : Set α)
              (hab : subSetRel s1 s2)
              (hba : subSetRel s2 s1) =>
            (
              Set.ext   -- axiom: reduces s1 = s2 to bi-implication
              fun _ =>
                Iff.intro
                  (fun h => hab h)
                  (fun h => hba h)
            )
        )
        -- @isTransitive α β r
        -- ∀ (a b c : α), r a b → r b c → r a c
        (
          (
            fun _ _ _ hst htv =>
            (
              fun _ =>  -- for any member of a
                fun has =>
                  let hat := hst has
                  htv hat
            )
          )
        )
    )

The Inverse of an Injective Function is a Function

#check Rel.inv
example : isInjectiveFun r → isFunction (r.inv) :=
  fun hinjr =>   -- assume r is injective
  -- show inverse is a function
  -- assume r output, r.inv input, elements c b a
  fun c b a =>
  -- we need to show that r.inv is single valued
  -- assume r.inv associatss c with both b and a
      fun rinvcb rinvca =>
        hinjr.right b a c rinvcb rinvca

Homework

In this part of homework, we state and prove, as a theorem, the proposition that, for any natural number, n, the congruence mod n relation, on natural numbers, a and b, is an equivalence relation. We formalize these ideas by defining congModN (n : Nat) to be a family of relations, one for each value of n, each being a (different) equivalence relation on the natural numbers. That's not Lean, that's just the mathematics. The last detail, for a given n, is to specify the relation membership predicate on pairs, (a, b). Here, it will be that 1%n = b%n.

def congModN (n : Nat) : Rel Nat Nat :=
                      -- for a given n
  fun a b =>          -- the binary predicate
    a % n = b % n     -- that defines (congModN n)

HOMEWORK PROBLEM #1: FINISH IT OFF.

To get further warmed up, let's prove a congruence for some particular n. Let's make it 3. So what we expect is that 0, 3, 6, ... will be congruent mod n (mod 3). So will be 1, 4, 7, ... And also 2, 5, 8, .... We don't have to say 3, 6, 9, as they are just elements in the equivalence class for 0. So here we go: congruence mod 3 is an equivalence relation.

Congruence Mod 3 is an Equivalence Relation

example : isEquivalence (congModN 3) :=
by
  unfold isEquivalence

By the definition of equivalence, we must show

  isReflexiveRel (congModN 3) ∧
  isSymmetricRel (congModN 3) ∧
  isTransitiveRel (congModN 3)
```lean
constructor   -- applies first ∧ constructor

On ∧.left we need a prove that (congModN 3) is reflexive And on the right, that it's symmetrical and transitive

  -- reflexive
  unfold isReflexiveRel
  intro n
  unfold congModN
  rfl

  -- split conjunction
  constructor

  -- symmetric
  unfold isSymmetricRel
  intro a b
  unfold congModN
  intro h
  rw [h]

  -- transitive

-- EXERCISE: fill this hole.
  sorry

Congruence Mod n is an Equivalence Relation

Now we state and prove that for any n, conguence mod n is an equivalence relation.

example : ∀ (n : Nat), isEquivalence (congModN n) :=
fun n =>
  And.intro
  (
    fun a =>
      rfl
  )
  (
    And.intro
    (
      fun a b h =>
        by
          simp [congModN] at h
          simp [congModN]
          rw [h]
    )
    (
      fun a b c hab hbc =>
        by
          simp [congModN] at hab
          simp [congModN] at hbc
          simp [congModN]
          rw [hab]
          assumption
    )
  )

The Subset Relation is a Partial Order

theorem subsetPO (α : Type): isPartialOrder (@subSetRel α) :=
by
  unfold isPartialOrder
  apply And.intro
    (
      by
        unfold isReflexiveRel
        intro s
        unfold subSetRel
        intro t
        intro h
        assumption
    )
    (
      -- EXERCISE: Fill these holes.
      And.intro
        sorry
        sorry
    )

Well Founded Relations

end DMT1.Lectures.setsRelationsFunctions.propertiesOfRelations