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 <
[email protected]> 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
> [email protected]
> https://lists.sourceforge.net/lists/listinfo/hol-info
>
>
------------------------------------------------------------------------------
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
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
