# Induction rules for reflexive, transitive closure

I'm trying to solve an exercise on inductive definitions, the premiss is:

Let $\to$ be a relation on $A$ and $\to^*$ its reflexive, transitive closure, which is defined by following two rules:

1. $a \to^*a$ (reflexive)
2. ${a \to^*b \quad b \to c \over a \to^*c }$ (step)

The questions are:

1. What are the induction rules for $\to^*$?
2. Show that $\to^*$ is reflexive.
3. Show that $\to^*$ is transitive.

The first question startles me, I view ${a \to^*b \quad b \to c \over a \to^*c }$ as the induction rule. Is this the complete answer?

And can I show the reflexivity with ${a \to^*b \quad b \to a \over a \to^*a }$?

Here's a fully formal articulation in the language of Agda. First, inductive rules correspond to indexed families.

data Star {A : Set}(R : A → A → Set) : A → A → Set where
Refl : {a : A} → Star R a a
Trans : {a b c : A} → Star R a b → R b c → Star R a c


Here the Refl data constructor corresponds to your first rule, and the Trans data constructor corresponds to your second rule. R represents $\to$, so Star R corresponds to $\to^*$. The induction rule corresponds to the eliminator for the data type, i.e. roughly the fold on that type (though things are a bit more complicated in a dependently typed language).

ind : {A : Set}{R : A → A → Set}{P : A → A → Set}
→ ({a : A} → P a a) → ({a b c : A} → P a b → R b c → P a c)
→ {a b : A} → Star R a b → P a b
ind r t Refl = r
ind r t (Trans s x) = t (ind r t s) x


This says that if you give me some binary relation $P$ and you show that $\forall a \in A. P(a,a)$ holds and $\forall a,b,c\in A. P(a,b)\land R(b,c) \Rightarrow P(a,c)$ (i.e. when $P(a,b)$ and $R(b,c)$ hold, then $P(a,c)$ holds) then I can provide you a proof of $P(a,c)$ whenever $R^*(a,c)$ holds, where $R^*$ is the reflexive, transitive closure of $R$.

Question 2 is completely trivial. The formal proof of the statement is Refl. Question 3 is not much harder. It's asking to show that if $a \to^* b$ and $b \to^* c$ then $a \to^* c$, while the inductive rule only gives the case when $b \to c$ in a single step. Obviously, we just need to recursively apply the single-step rule. This leads to the following code:

trans : {A : Set}{R : A → A → Set}{a b c : A} → Star R a b → Star R b c → Star R a c
trans r Refl = r
trans r (Trans s x) = Trans (trans r s) x


For your purposes, you should probably define the equivalent of trans in terms of the induction rule, i.e. in terms of ind. I'll leave that as a very simple exercise.

• Thanks for the explanation. It helped me understand the Star type in Agda. – Henry Story Oct 28 '20 at 13:03
1. No. Induction rules for this case look like this:

Let $$P$$ be some property of relations on $$A$$ (you already know some examples of such properties: symmetry, transitivity, etc.). To show that $$P(\rightarrow^*)$$ holds Let $$P$$ be some binary relation on $$A$$. To show that $$P(a, b)$$ holds whenever $$a \rightarrow^* b$$, it should be enough to prove something that only mentions $$\rightarrow$$ and $$P$$, but not $$\rightarrow^*$$. What? Namely, there will be 2 premisses, one corresponding to "reflective" and another to "step".

2. Well, first you'd need to prove that $$a \rightarrow^* b$$ and $$b \rightarrow a$$ hold for any $$a$$ and $$b$$, and of course you can't. The puzzling thing is that the proof is utterly trivial. Does it maybe say "transitive" instead?

• Also - proving transitivity is the next subtask. Since you already mentioned it, I'll include it :) – mike Apr 24 '17 at 14:42
• 2. Surely $\to^*$ is reflexive, by definition rule 1: $a \to^*a$. – Thumbnail Apr 24 '17 at 14:43
• Could you elbaborate on 1, e.g. transitivity only comes into play when you consider $\to^*$, not if you only look at $\to$. – mike Apr 24 '17 at 14:59
• What I currently have for 1 is: ${n~\in~\mathbb{N}\quad \to^*:= \to^n \quad P(\to^{n-1}~\circ~\to)\over P(\to^n) }$ – mike Apr 24 '17 at 14:59
• @mike I did (decided to add a paragraph there instead of a comment). I'll tell you that your suggested answer is wrong because 1) the conclusion should be $P(\rightarrow^*)$; 2) $:=$ normally means "set". It makes no sense to place as a premise of a rule. If you mean "equals", then this rule would be inapplicable whenever there is no such $n$: a very simple example is $A = \mathbb{N}, P(x,y) := y = x+1$. – Alexey Romanov Apr 24 '17 at 15:13