Induction rules for reflexive, transitive closure

Question

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 }$?

Answer 1

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.

Answer 2

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?