MATH.12:4.2 - Recover what each proof step supplies
Begin at the desired conclusion and follow the steps needed to produce its object. Give each supplied value a name. For a lemma used along the way, recover the obtaining operation when the next step consumes its output as data.
The following constructions give a small working repertoire:
| Form of the argument | Construction to recover | How its result is used |
|---|---|---|
| Given x, construct t(x) | A function x ↦ t(x) | Supply a particular input and evaluate t at that input. |
| Construct both b and c | The pair (b,c) | Project the component needed by the next step, or retain both. |
| Establish one of two cases constructively | A tag naming the chosen case and the data for that case | Select the corresponding branch using that tag. |
| Exhibit y and establish R(x,y) | A pair containing y and its justification | Return y; use the second component when the next argument needs the property. |
| Use an already constructed operation f on a value a | The application f(a) | Feed the returned value to the next construction. |
A constructive disjunction carries which case holds. If the source argument provides no such choice, name the missing decision before turning it into a conditional program.
For an inductive argument, recover the base and constructor operations through MATH.4. That pattern also handles a step that needs a stronger result. The present method assembles the values supplied by those operations with the other proof steps.