irule is an “improved” version of match_mp_tac; mp_then is an improved version
of imp_res_tac (strictly, imp_res_then).
Alternatively, irule applies an introduction rule to the goal (“backwards”);
mp_then applies an elimination rule to assumptions.
I agree about the stripping of conjunctions. My temptation is to just remove
that feature entirely; making the user follow up with rpt conj_tac if that’s
what they want doesn’t seem much of an imposition.
Michael
From: Ramana Kumar <ramana.ku...@cl.cam.ac.uk>
Date: Thursday, 24 August 2017 at 09:41
To: "Norrish, Michael (Data61, Canberra City)" <michael.norr...@data61.csiro.au>
Cc: hol-info <hol-info@lists.sourceforge.net>
Subject: Re: [Hol-info] Strange tactics bug when using match_mp_tac
I have a couple of comments/questions on irule:
- I think mp_then is supposed to be better still. Am I right? (Or are they
serving different purposes?)
- I find it annoying that irule produces lots of new subgoals for the
hypotheses. Is there a version that doesn't strip all the conjunctions, so they
can be worked on together?
On 24 August 2017 at 09:22,
<michael.norr...@data61.csiro.au<mailto:michael.norr...@data61.csiro.au>> wrote:
Eta-expanding as you did is nicer, I think.
You might also consider using irule; it is supposed to be an improved
match_mp_tac (i.e., does more things), and it doesn’t have the particular
problem with exceptions. Indeed, one of its improvements is that it subsumes
{MATCH_}ACCEPT_TAC.
Michael
On 23/8/17, 17:28, "Heiko Becker"
<heikobecke...@gmail.com<mailto:heikobecke...@gmail.com>> wrote:
Thank you for the fix. With this I could come up with a solution that I
find ok for the moment:
val my_match_mp_tac = (fn thm => (fn gs => match_mp_tac thm gs))
This allows to at least not have the HOL_ERR handling, but I guess it
depends what one finds nicer.
Heiko
On 08/23/2017 09:03 AM,
michael.norr...@data61.csiro.au<mailto:michael.norr...@data61.csiro.au> wrote:
> You are being caught by the fact that match_mp_tac thm can throw an
exception before the tactic is ever applied to a goal. In particular, if the
theorem passed to match_mp_tac is not an implication an exception is thrown
immediately.
>
> You can fix this by handling that possible exception:
>
> fun simple_apply thm = ACCEPT_TAC thm ORELSE (match_mp_tac thm handle
HOL_ERR _ => ALL_TAC)
>
> This arguably a poor design for match_mp_tac, and should perhaps be
changed.
>
> Michael
>
>
>
> On 23/8/17, 16:55, "Heiko Becker"
<hbec...@mpi-sws.org<mailto:hbec...@mpi-sws.org>> wrote:
>
> Hello everyone,
>
> while working on some custom tactics, I noticed some strange behavior
> related to combining tactics with match_mp_tac and the ORELSE
tactical:
>
> I am trying to write a tactic takes a theorem and first tries out
> whether it is already a proof of the current goal with ACCEPT_TAC.
> If this does not succeed, the tactic should try matching the theorem
> with match_mp_tac.
>
> Here is what I have come up with:
>
> fun simple_apply thm = (ACCEPT_TAC thm) ORELSE (match_mp_tac
thm);
>
> I have defined a test tactic, to see whether ACCEPT_TAC works as I
> expect it to work:
>
> fun dumb_apply thm = (ACCEPT_TAC thm) ORELSE (FAIL_TAC
"Unreachable");
>
> Strangely the simple_apply tactic does not work in cases, where the
> dumb_apply tactic works:
>
> val test_thm = Q.prove (
> ` !(n:num) (P:num -> bool).
> P n ==>
> P n`,
> rpt gen_tac
> DISCH_THEN ASSUME_TAC
> qpat_x_assum `P n` (fn thm => simple_apply thm) (* Fails with
"No
> parse of quotation leads to success" *)
> qpat_x_assum `P n` (fn thm => dumb_apply thm) (* Proves the
goal *)
> );
>
>
> Can someone explain to me what I did wrong with the simple_apply
tactic?
>
>
> Thanks,
>
>
> Heiko
>
>
------------------------------------------------------------------------------
> Check out the vibrant tech community on one of the world's most
> engaging tech sites, Slashdot.org! http://sdm.link/slashdot
> _______________________________________________
> hol-info mailing list
> hol-info@lists.sourceforge.net<mailto:hol-info@lists.sourceforge.net>
> https://lists.sourceforge.net/lists/listinfo/hol-info
>
>
------------------------------------------------------------------------------
Check out the vibrant tech community on one of the world's most
engaging tech sites, Slashdot.org! http://sdm.link/slashdot
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net<mailto:hol-info@lists.sourceforge.net>
https://lists.sourceforge.net/lists/listinfo/hol-info
------------------------------------------------------------------------------
Check out the vibrant tech community on one of the world's most
engaging tech sites, Slashdot.org! http://sdm.link/slashdot
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
