Backwards reasoning works something like this: to prove 'forall n: P n', it is sufficient to prove 'P 0' and 'P n => P (succ n)', so if you have 'forall n: P n' as your so-called proof goal, you can use the induction tactic to transform that into two goals: 'P 0' and 'P n => P (succ n)'. You then have to separately prove both goals. The tactic system then basically build the actual proof by putting everything on a stack and applying in reverse: once you've proved both goals, it knows it can apply the forward-reasoning induction proof function to construct a proof of the original statements from the two proofs you gave.
> the difference between agda and Coq seems like the difference between purely functional and imperative programming.
Bold, bold :) I'll have to try Agda before I can comment on that. Coq proofs do seem a bit inperative, so there's that.