Hey Marco,
Thanks. That's what I was searching for :)
Regards,
Robert
> ---------- Forwarded message ----------
> From: Marco Maggesi <[email protected]>
> To: "[email protected]" <[email protected]>
> Cc:
> Date: Thu, 21 May 2015 15:52:38 +0200
> Subject: Re: [Hol-info] EQ_MP as a TAC?
> Dear Robert,
>
> I don't think that HOL Light has such a tactic, but it is not difficult to
> implement it (see below).
>
> For everyday work, you may want to delegate this kind of low-level logical
> steps to a decision procedure like MESON.
> For instance:
>
> g `(a <=> b) /\ a ==> b`;;
> e (REPEAT STRIP_TAC);;
> e (SUBGOAL_THEN `a:bool` (fun th -> ASM_MESON_TAC[th]));;
>
> If you are lucky and the equality has the right orientation, (i.e. `b <=>
> a` instead of `a <=> b`) you can simply use rewriting:
>
> g `(b <=> a) /\ a ==> b`;;
> e (REPEAT STRIP_TAC);;
> e (ASM_REWRITE_TAC[]);;
>
> You can also define yourself a tactic that implements exactly the EQ_MP
> rule:
>
> let EQ_MP_TAC =
> let pth = MESON [] `(a <=> b) ==> a ==> b` in
> fun th -> MATCH_MP_TAC (MATCH_MP pth th);;
>
> g `(a <=> b) /\ a ==> b`;;
> e (REPEAT STRIP_TAC);;
> e (FIRST_X_ASSUM EQ_MP_TAC);;
>
> Personally I like very much the following tactic (not part of HOL Light)
> for this kind of situations:
>
> let CUT_TAC : term -> tactic =
> let th = MESON [] `(p ==> q) /\ p ==> q`
> and ptm = `p:bool` in
> fun tm -> MATCH_MP_TAC (INST [tm,ptm] th) THEN CONJ_TAC;;
>
> here is how I use it:
>
> g `(b <=> a) /\ a ==> b`;;
> e (REPEAT STRIP_TAC);;
> e (CUT_TAC `a:bool`);;
> e (ASM_REWRITE_TAC[]);;
>
>
> Marco
>
>
>
> 2015-05-21 14:43 GMT+02:00 Petros Papapanagiotou <[email protected]>:
>
>> Dear Robert,
>>
>> I am not sure what you are trying to accomplish. Do you have an example
>> goal?
>>
>> Again, there may be better ways of doing this, but I keep this useful
>> (though sometimes confusing) shortcut handy:
>>
>> let EQ_MP_THEN thmtc = fun x -> FIRST_ASSUM (fun y -> (thmtc (EQ_MP x
>> y)));;
>>
>> Given a thm_tactic and a theorem thm of the form |- p <=> q it tries to
>> use EQ_MP thm with the first matching assumption, then applies the
>> thm_tactic to the result.
>>
>> Trivial example:
>> g `p /\ q ==> q /\ p`;;
>> e DISCH_TAC;;
>> e (EQ_MP_THEN ACCEPT_TAC (SPECL [`p:bool`;`q:bool`] CONJ_SYM));;
>>
>> or if you want to use an assumed equivalence:
>> g `p ==> (p <=> q) ==> q`;;
>> e (REPEAT DISCH_TAC);;
>> e (FIRST_ASSUM (EQ_MP_THEN ACCEPT_TAC));;
>>
>> Hope this helps.
>>
>> Regards,
>> Petros
>>
>>
>>
>> On 21/05/2015 13:00, Robert White wrote:
>> > Dear all,
>> >
>> >
>> > I wonder if there is a way I can use TAC for EQ_MP.
>> >
>> > I'm sorry I'm not very familiar with bottom up proofs.
>> >
>> > A1 |- t1 <=> t2 A2 |- t1'
>> > ----------------------------- EQ_MP
>> > A1 u A2 |- t2
>> >
>> > Thanks!
>> > --
>> >
>> > Regards,
>> > Robert
>> >
>> >
>> >
>> ------------------------------------------------------------------------------
>> > One dashboard for servers and applications across Physical-Virtual-Cloud
>> > Widest out-of-the-box monitoring support with 50+ applications
>> > Performance metrics, stats and reports that give you Actionable Insights
>> > Deep dive visibility with transaction tracing using APM Insight.
>> > http://ad.doubleclick.net/ddm/clk/290420510;117567292;y
>> >
>> >
>> >
>> > _______________________________________________
>> > hol-info mailing list
>> > [email protected]
>> > https://lists.sourceforge.net/lists/listinfo/hol-info
>> >
>>
>> --
>> Petros Papapanagiotou, Ph.D.
>> CISA, School of Informatics
>> The University of Edinburgh
>>
>> Email: [email protected]
>>
>> ---
>> The University of Edinburgh is a charitable body, registered in
>> Scotland, with registration number SC005336.
>>
>>
>> ------------------------------------------------------------------------------
>> One dashboard for servers and applications across Physical-Virtual-Cloud
>> Widest out-of-the-box monitoring support with 50+ applications
>> Performance metrics, stats and reports that give you Actionable Insights
>> Deep dive visibility with transaction tracing using APM Insight.
>> http://ad.doubleclick.net/ddm/clk/290420510;117567292;y
>> _______________________________________________
>> hol-info mailing list
>> [email protected]
>> https://lists.sourceforge.net/lists/listinfo/hol-info
>>
>
>
>
> ---------- Forwarded message ----------
> From: Marco Maggesi <[email protected]>
> To: "[email protected]" <[email protected]>
> Cc:
> Date: Thu, 21 May 2015 16:20:32 +0200
> Subject: Re: [Hol-info] Intuitionistic basic_rewrites?
> Dear Robert,
>
> you can use PURE_REWRITE_TAC which uses only the given list of rewrites.
>
> Or you can change the set basic_rewrites with the command
> set_basic_rewrites.
> E.g.,
>
> let rthl = CONJUNCTS (MESON[] `~T = F /\ ~F = T`);;
> set_basic_rewrites rthl;;
>
> Marco
>
>
>
> 2015-05-21 15:18 GMT+02:00 Robert White <[email protected]>:
>
>> Hello again,
>>
>> I understand that HOL is a reasoner for classical logic so there is no
>> surprise when I want to prove something using rewriting I get a set of
>> rules as basic_rewrites where we can find ~ ~t <=> t; there.
>>
>> So here comes the question, is there a way we can get intuitionistic set
>> or rewriting rules in HOL Light already to do pure constructive logic
>> reasoning?
>>
>> Thanks again.
>>
>> --
>>
>> Regards,
>> Robert White <http://www.dptinfo.ens-cachan.fr/~swang/>(Shuai Wang)
>> INRIA Deducteam <https://www.rocq.inria.fr/deducteam/>
>>
>>
>> ------------------------------------------------------------------------------
>> One dashboard for servers and applications across Physical-Virtual-Cloud
>> Widest out-of-the-box monitoring support with 50+ applications
>> Performance metrics, stats and reports that give you Actionable Insights
>> Deep dive visibility with transaction tracing using APM Insight.
>> http://ad.doubleclick.net/ddm/clk/290420510;117567292;y
>> _______________________________________________
>> hol-info mailing list
>> [email protected]
>> https://lists.sourceforge.net/lists/listinfo/hol-info
>>
>>
>
>
> ------------------------------------------------------------------------------
> One dashboard for servers and applications across Physical-Virtual-Cloud
> Widest out-of-the-box monitoring support with 50+ applications
> Performance metrics, stats and reports that give you Actionable Insights
> Deep dive visibility with transaction tracing using APM Insight.
> http://ad.doubleclick.net/ddm/clk/290420510;117567292;y
> _______________________________________________
> hol-info mailing list
> [email protected]
> https://lists.sourceforge.net/lists/listinfo/hol-info
>
>
--
Regards,
Robert White <http://www.dptinfo.ens-cachan.fr/~swang/>(Shuai Wang)
INRIA Deducteam <https://www.rocq.inria.fr/deducteam/>
------------------------------------------------------------------------------
One dashboard for servers and applications across Physical-Virtual-Cloud
Widest out-of-the-box monitoring support with 50+ applications
Performance metrics, stats and reports that give you Actionable Insights
Deep dive visibility with transaction tracing using APM Insight.
http://ad.doubleclick.net/ddm/clk/290420510;117567292;y
_______________________________________________
hol-info mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
