I think liberal use of explicit subgoals (using "by") can be very good style, because it documents the steps through which you intend the proof to proceed.
Once you have finished (part of a proof), it is sometimes possible to shorten it if you so desire. For example, if this works: `l1` by metis_tac[th1,th2] >> `l2` by metis_tac[th3] >> res_tac >> metis_tac[th4] you might go back and see if metis_tac[th1,th2,th3,th4] works on its own, or if you could do `l1 /\ l2` by metis_tac[th1,th2,th3] or dispense with l1 altogether, etc. It's often easier to modify a proof that works, preserving its correctness, than to generate an "elegant" proof from scratch. On 17 November 2015 at 12:38, shengyu shen <[email protected]> wrote: > Dear all: > > I am a new learner of HOL, and I am following the examples given in > kananaskis-10-tutorial.pdf. > > I find those solution given in this tutorial seems very elegant with > METIS_TAC, but my solution to these examples include large number of "by" > mechanism like this : > > ‘h n = g n‘ by METIS_TAC [MY LEMMA] > > and each such line advance the proof by only a very very small step. > > I chose such a style because most of the time I try a to advance the proof > a large step with METIS_TAC, it complain "NO solution", which means some > particular lemma or theorem is missing, but no hints tell me what is > missing. > > So is it a bad habit to use so many "by" mechanism? how these successful > HOL user find their elegent proof? > > Thanks > Shen > > > ------------------------------------------------------------------------------ > > _______________________________________________ > hol-info mailing list > [email protected] > https://lists.sourceforge.net/lists/listinfo/hol-info > >
------------------------------------------------------------------------------
_______________________________________________ hol-info mailing list [email protected] https://lists.sourceforge.net/lists/listinfo/hol-info
