Performing Calculation in Interactive Theorem Proving
An LCF style tactic can be used to verify that the conclusion is a logical consequence of the premises, however, in mathematical practice, we often construct a conclusion in a proof step. This paper proposes a calculational style of tactic, and illustrates the characteristic and the realization issues of the tactics on the top of a theorem prover.
B. Li et al., "Performing Calculation in Interactive Theorem Proving", Applied Mechanics and Materials, Vols. 130-134, pp. 2924-2927, 2012