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.