MATH.4:4.4 - Define the operation and establish its result

For a natural-number input, let b be the base witness and let step(n,y) produce a witness for n+1 from one for n. Define:

F(0)=b

F(n+1)=step(n,F(n)).

The base argument establishes P(0,F(0)). The step argument establishes P(n+1,F(n+1)) from P(n,F(n)). Induction therefore establishes the property for every natural number.

For another finite inductive input, give one defining clause and one property argument per constructor. Recursive calls use its immediate constituents. Evaluation terminates because these calls descend through a finite input construction, provided the operations within each clause terminate.

When different constructor expressions represent one object, the recursion first gives a function of expressions. To obtain a function of the represented object, establish that all its permitted expressions yield the same required output, using MATH.2. Alternatively, supply an additional rule that chooses one construction from the object. Keeping the construction as part of the input is also useful when its history matters.

For example, build a finite set with Empty and Insert(a,S) for a outside S. Returning [] at the base and prepending a at each step gives a list containing each element once. Yet Insert(1,Insert(2,Empty)) and Insert(2,Insert(1,Empty)) represent the same set and return [1,2] and [2,1]. Both are valid witnesses, but these clauses define a function of the insertion construction. If a function of the set is required and its elements have a supplied total order, strengthen the output requirement to an increasing list and insert each element in order. The unique increasing list then makes the output independent of insertion order. This repair uses the ordering operation and a stronger specification.

A dependent-type description can package the output with a proof of its property. Its first projection returns the witness; the other component justifies that witness for the stated input. An ordinary mathematical presentation may instead give the function and proof separately. Use the presentation needed for the receiving work.