Thank you Ramana, that is a good answer. I will use LEAST_ELIM_TAC and
DEEP_INTRO_TAC
as you suggest.
Peter
On Wed, Jun 8, 2016 at 7:15 PM, Ramana Kumar <ramana.ku...@cl.cam.ac.uk>
wrote:
> Hi Peter,
>
> I'm not sure I can explain why HO_MATCH_MP_TAC is not powerful enough for
> this kind of match, but I can say what would use instead in this situation.
> Namely, numLib.LEAST_ELIM_TAC. More generally, I would use DEEP_INTRO_TAC
> with theorems such as LEAST_ELIM, which is how LEAST_ELIM_TAC is
> implemented.
>
> Cheers,
> Ramana
>
> On 9 June 2016 at 07:35, Peter Vincent Homeier <
> palan...@trustworthytools.com> wrote:
>
>> I am trying to apply HO_MATCH_MP_TAC, but it is not successfully matching
>> the consequent of the theorem to the current goal the way I thought it
>> would. The example below is not meant to be a provable theorem, just a
>> simple instance to show this issue.
>>
>> By the way, HO_PART_MATCH fails for this case as well.
>>
>> I can certainly force the matching to work by providing explicit
>> substitutions, such as shown below, but this is both ugly and not robust
>> for proof maintenance. The explicit substitutions show the original theorem
>> can match the goal, but the matching substitution is not found by higher
>> order matching in this case.
>>
>> What am I not understanding here? Why does higher order matching fail?
>>
>> Transcript:
>>
>> ---------------------------------------------------------------------
>> HOL-4 [Kananaskis 11 (stdknl, built Tue May 24 15:32:51 2016)]
>>
>> For introductory HOL help, type: help "hol";
>> To exit type <Control>-D
>> ---------------------------------------------------------------------
>> [extending loadPath with Holmakefile INCLUDES variable]
>> [In non-standard heap:
>> /usr/local/hol/cakeml/cakeml-master/candle/set-theory/heap]
>> > > > > load "bitTheory";
>> val it = (): unit
>> > g `BIT (LEAST n. BIT n x) x`;
>> val it =
>> Proof manager status: 1 proof.
>> 1. Incomplete goalstack:
>> Initial goal:
>>
>> BIT (LEAST n. BIT n x) x
>>
>>
>> :
>> proofs
>> > whileTheory.LEAST_ELIM;
>> val it =
>> |- ∀Q P. (∃n. P n) ∧ (∀n. (∀m. m < n ⇒ ¬P m) ∧ P n ⇒ Q n) ⇒ Q ($LEAST
>> P):
>> thm
>> > e(HO_MATCH_MP_TAC whileTheory.LEAST_ELIM);
>> OK..
>>
>> Exception raised at Tactic.HO_MATCH_MP_TAC:
>> at HolKernel.ho_match_term:
>> at Term.dest_comb:
>> not a comb
>> Exception-
>> HOL_ERR
>> {message =
>> "at HolKernel.ho_match_term:\nat Term.dest_comb:\nnot a comb",
>> origin_function = "HO_MATCH_MP_TAC", origin_structure = "Tactic"}
>> raised
>>
>>
>> > (BETA_RULE o SPECL[``\a. BIT a x``,``\n. BIT n x``])
>> whileTheory.LEAST_ELIM;
>> val it =
>> |- (∃n. BIT n x) ∧ (∀n. (∀m. m < n ⇒ ¬BIT m x) ∧ BIT n x ⇒ BIT n x) ⇒
>> BIT (LEAST n. BIT n x) x:
>> thm
>> > e(HO_MATCH_MP_TAC ((BETA_RULE o SPECL[``\a. BIT a x``,``\n. BIT n x``])
>> whileTheory.LEAST_ELIM));
>> OK..
>> 1 subgoal:
>> val it =
>>
>> (∃n. BIT n x) ∧ ∀n. (∀m. m < n ⇒ ¬BIT m x) ∧ BIT n x ⇒ BIT n x
>>
>> :
>> proof
>> >
>>
>> Thanks for your help.
>>
>> Peter
>>
>>
>>
>> "In Your majesty ride prosperously
>> because of truth, humility, and righteousness;
>> and Your right hand shall teach You awesome things." (Psalm 45:4)
>>
>>
>> ------------------------------------------------------------------------------
>> What NetFlow Analyzer can do for you? Monitors network bandwidth and
>> traffic
>> patterns at an interface-level. Reveals which users, apps, and protocols
>> are
>> consuming the most bandwidth. Provides multi-vendor support for NetFlow,
>> J-Flow, sFlow and other flows. Make informed decisions using capacity
>> planning reports.
>> https://ad.doubleclick.net/ddm/clk/305295220;132659582;e
>> _______________________________________________
>> hol-info mailing list
>> hol-info@lists.sourceforge.net
>> https://lists.sourceforge.net/lists/listinfo/hol-info
>>
>>
>
--
"In Your majesty ride prosperously
because of truth, humility, and righteousness;
and Your right hand shall teach You awesome things." (Psalm 45:4)
------------------------------------------------------------------------------
What NetFlow Analyzer can do for you? Monitors network bandwidth and traffic
patterns at an interface-level. Reveals which users, apps, and protocols are
consuming the most bandwidth. Provides multi-vendor support for NetFlow,
J-Flow, sFlow and other flows. Make informed decisions using capacity
planning reports. https://ad.doubleclick.net/ddm/clk/305295220;132659582;e
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
