# what is routine induction?

I read a paper which mentioned routine induction many times. But when I google it, there are nothing showed up.

I think routine induction means the induction on the structure, analyzing possible cases in proofs. am I right?

Just to make sure, I am asking it here.

• Could you refer to the paper that you read? – nekketsuuu Mar 14 '17 at 6:39
• It might be that routine is used in the non-technical sense. A routine induction is the same as a pedestrian induction. – Yuval Filmus Mar 14 '17 at 7:38
• @nekketsuuu The paper is at the link gabbay.org.uk/papers/nomu-jv.pdf. – alim Mar 14 '17 at 8:14
• @YuvalFilmus could you give an example of pedestrian induction? – alim Mar 14 '17 at 8:15
• @alim It's just plain induction. Take any proof by induction in an introduction to proofs course. – Yuval Filmus Mar 14 '17 at 8:35

Sometimes an author will say that you can find a proof by "following your nose". This means that the structure of the theorem strongly suggests one (or at most a few) next steps. This (combined with some searching) is what's behind Coq's auto tactic, Agda's Agsy tool, and the Djinn tool. Structural induction is the "follow your nose" step you get when faced with the problem of proving something about all members of an inductively defined type like an abstract syntax tree. So an elliptical "by structural induction" is really the statement of "do the obvious thing; there are no surprises".