Note: The solution below should really be considered as just a path for
some brainstorming.
There are some easy cases where it won't work.
For instance, with a goal of the form `!x:real. R x ==> P (x/x) ==> Q x`
which is not a logical consequence of `!x:real. R x ==> x<> 0 /\ P (x/x)
==> Q x`
(in this case, the application of the tactic will diverge).
Le 26/11/2012 19:30, Vincent Aravantinos a écrit :
Hi Michael,
Another possibility to solve this problem is to add the required
assumption as a conjunction with the atomic proposition in which the
rewrite occurs.
For instance `!x. x <> 0 ==> P (x/x)` would be turned into `!x. x <>
0 ==> x <> 0 /\ P 1`.
Here is a quick-hack implementation which achieves this (I say quick
hack because it makes use of METIS/MESON in HOL4/HOL-Light, one could
probably get rid of it):
HOL-Light:
let MP_REWRITE_TAC th (_,c as g) =
let (p,c') = dest_imp (concl (SPEC_ALL th)) in
let l,r = (dest_eq o snd o strip_forall) c' in
let add_context ctxt k t =
try k (mk_conj (ctxt,t)),None with _ -> k t,Some ctxt in
let common k = function t,None -> k t,None | t,Some c -> add_context
c k t in
let mk_opt_conj = function
|None,None -> None
|Some _ as x,None | None,(Some _ as x) -> x
|Some x,Some y -> Some(mk_conj(x,y))
in
let rec new_concl t =
try
let i = term_match [] l t in
add_context (instantiate i p) I (instantiate i r)
with _ ->
match t with
|Abs(v,b) -> common (curry mk_abs v) (new_concl b)
|Comb(t1,t2) ->
let t1',c1 = new_concl t1 and t2',c2 = new_concl t2 in
common I (mk_comb(t1',t2'),mk_opt_conj(c1,c2))
|Const _ | Var _ -> t,None
in
MATCH_MP_TAC (MESON[th] (mk_imp (fst (new_concl c),c))) g;;
HOL4:
fun MP_REWRITE_TAC th g =
let
val (p,c') = dest_imp (concl (SPEC_ALL th))
val (l,r) = (dest_eq o snd o strip_forall) c'
fun add_context ctxt k t =
(k (mk_conj (ctxt,t)),NONE) handle _ => (k t,SOME ctxt)
fun common k (t,NONE) = (k t,NONE)
| common k (t,SOME c) = add_context c k t
fun mk_opt_conj (NONE,NONE) = NONE
| mk_opt_conj (SOME x,NONE) = SOME x
| mk_opt_conj (NONE,SOME x) = SOME x
| mk_opt_conj (SOME x,SOME y) = SOME(mk_conj(x,y))
fun new_concl t =
let val (s,t) = match_term l t in
add_context (subst s (inst t p)) I (subst s (inst t r))
end
handle _ =>
if is_var t orelse is_const t then (t,NONE) else
let val (v,b) = dest_abs t in
common (curry mk_abs v) (new_concl b)
end
handle _ =>
let
val (t1,t2) = dest_comb t
val (t1',c1) = new_concl t1
val (t2',c2) = new_concl t2
in
common I (mk_comb(t1',t2'),mk_opt_conj(c1,c2))
end
val c = snd g
in
MATCH_MP_TAC (METIS_PROVE[th] (mk_imp (fst (new_concl c),c))) g
end;
Cheers,
V.
Le 22/11/2012 19:02, Michael Norrish a écrit :
Note that this approach will fail if the term to be rewritten is under a
variable binding.
MP_REWRITE_TAC REAL_DIV_REFL ([], ``!x. x<> 0 ==> P (x/x)``)
gives back an unprovable x<> 0 as a new subgoal, and also fails to simplify the
bound x/x in the "original" branch. (Put `x*x + 1` in `x` if you want a
slightly more realistic instance; the simplifier can obviously discharge the
side-condition on the original by itself.)
Even with the quantification gone, the x<> 0 assumption also needs to be
stripped as well to make MP_REWRITE_TAC do the right thing.
For this reason, I think the best solution (I don't have one right now!) to this
problem would integrate with the simplifier and its ability to accumulate
context as it traverses a term.
Michael
On 23/11/12 07:31, Vincent Aravantinos wrote:
Hi list,
I often face the following small but annoying problem:
* Situation:
- I have a theorem (say, "Th") of the form "P ==> t = u"
ex: REAL_DIV_REFL
(|- !x. ~(x =&0) ==> x / x =&1 in HOL-Light, |- !x. x<> 0 ==> (x
/ x = 1) in HOL4)
- the conclusion of my goal is a (big) term containing a subterm
(say, " t' ") matching t
ex: a big expression with a subterm t / t somewhere deep inside the
term
* My aim: rewrite t' into u' using Th
* Solution:
- make a subgoal to prove P' (the instance of P corresponding to t')
ex: t / t<> &0
(assume t is a big expression to make it annoying to type in)
- use this subgoal to rewrite the original goal
* Problem:
What annoys me in this frequent use case is that I have to explicitly
state the subgoal P' whereas it seems it can be automatized.
So, questions:
- Am I the only one to find this annoying? :-)
- If not, I imagine there might already exist a tactic that solves
this recurrent problem, but if so I did not find it ?
* Possible solution:
If not, I developed my own tactic which a couple of students here at
HVG have been using and found useful.
Please find below the implementation in HOL4 and HOL Light, the
tactic is called "MP_REWRITE_TAC".
In order to use it, e.g., for the above situation, just use:
e(MP_REWRITE_TAC REAL_DIV_REFL)
then the tactic will:
- search the goal for a subterm matching t (if several matches it
takes the first one it finds),
- introduce a subgoal for the corresponding P',
- rewrite the original goal with Th, taking P' into account.
- add P' to the set of assumptions of the original goal, so that it
can be reused later if needed.
Regards,
V.
Code:
HOL-Light:
let MP_REWRITE_TAC th (_,c as g) =
let sel = lhs o snd o strip_forall o snd o dest_imp in
let PART_MATCH = PART_MATCH sel (SPEC_ALL th) in
let th = ref TRUTH in
ignore (find_term (fun t -> try th := PART_MATCH t; true with _ ->
false) c);
(SUBGOAL_THEN (lhand (concl !th)) (fun x ->
REWRITE_TAC[MP !th x] THEN STRIP_ASSUME_TAC x)) g;;
HOL4:
fun MP_REWRITE_TAC th g =
let
val sel = lhs o snd o strip_forall o snd o dest_imp
val PART_MATCH = PART_MATCH sel (SPEC_ALL th)
val th = ref TRUTH
val _ =
find_term (fn t => (th := PART_MATCH t; true) handle _ => false)
(snd g)
in
(SUBGOAL_THEN (lhand (concl (!th))) (fn x =>
REWRITE_TAC[MP (!th) x] THEN STRIP_ASSUME_TAC x)) g
end;
------------------------------------------------------------------------------
Monitor your physical, virtual and cloud infrastructure from a single
web console. Get in-depth insight into apps, servers, databases, vmware,
SAP, cloud infrastructure, etc. Download 30-day Free Trial.
Pricing starts from $795 for 25 servers or applications!
http://p.sf.net/sfu/zoho_dev2dev_nov
_______________________________________________
hol-info mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
--
Vincent Aravantinos
Postdoctoral Fellow, Concordia University, Hardware Verification Group
http://users.encs.concordia.ca/~vincent
--
Vincent Aravantinos
Postdoctoral Fellow, Concordia University, Hardware Verification Group
http://users.encs.concordia.ca/~vincent
------------------------------------------------------------------------------
Monitor your physical, virtual and cloud infrastructure from a single
web console. Get in-depth insight into apps, servers, databases, vmware,
SAP, cloud infrastructure, etc. Download 30-day Free Trial.
Pricing starts from $795 for 25 servers or applications!
http://p.sf.net/sfu/zoho_dev2dev_nov
_______________________________________________
hol-info mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
