Performing Calculation in Interactive Theorem Proving
Bing Li, Chen Zhao, Lian Li · Applied Mechanics and Materials · 2011
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.