Induction rules for reflexive, transitive closure
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.