Hi,
I know it is not really what John asked for, but, well, just for fun, I
developped a conversion and a tactic to deal with this kind of goals
(in some sense, it can thus be considered as an "Easy button").
From my (basic) tests it should work quite well.
Please find them in the attached file.
USAGE:
The tactic is called CARD_TAC.
EXAMPLES:
`CARD {1,2,3} = 3`
# e CARD_TAC
val it : goalstack = No subgoals
`CARD {1,2,3,3} = 3`
# e CARD_TAC
val it : goalstack = No subgoals
`~(CARD {1,2,3,4} = 3)`
# e CARD_TAC
val it : goalstack = No subgoals
The conversion is called CARD_CONV:
EXAMPLES:
# CARD_CONV `CARD {1,2,3}`
val it : thm = |- CARD {1, 2, 3} = 3
# CARD_CONV `CARD {1,2,3,3}`
val it : thm = |- CARD {1, 2, 3, 3} = 3
However, this is for sets of numbers only, e.g. it does not work for reals.
COUNTER-EXAMPLE:
`CARD {&1, &2, &3} = 3`
# e CARD_TAC;;
val it : goalstack = 1 subgoal (1 total)
`(if &1 = &2 \/ &1 = &3
then if &2 = &3 then 1 else 2
else SUC (if &2 = &3 then 1 else 2)) =
3`
Indeed, computing the cardinal requires that you can decide the equality
for the type of the elements.
For these situations, the tactic (and the conversion) takes an optional
parameter (called "dp" for "Decision Procedure") to decide the equality
of elements:
EXAMPLES:
`CARD {&1,&2,&3} = 3`
# e(CARD_TAC ~dp:REAL_ARITH);;
val it : goalstack = No subgoals
`CARD {&1,&3,&2,&3} = 3`
# e(CARD_TAC ~dp:REAL_ARITH);;
val it : goalstack = No subgoals
Since we use a decision procedure, we can even handle trickier
situations, involving reasoning about the elements:
TRICKIER EXAMPLES:
`CARD {2,1+1,3-1,2*1} = 1`
# e(CARD_TAC ~dp:ARITH_RULE)
val it : goalstack = No subgoals
`CARD {&1, &2 / &2} = 1`
# e(CARD_TAC ~dp:REAL_ARITH);;
val it : goalstack = No subgoals
Cheers,
V.
Le 04/11/12 14:34, Petros Papapanagiotou a écrit :
I have also experienced some pain trying to achieve simple calculations
for sets in HOL Light (to the point where I chose to change my
formalisation to using lists).
Unfortunately, to my knowledge, HOL Light only provides SET_TAC as an
automated tactic for sets, which is often insufficient for such
calculations.
I tried this particular example and came up with a proof based on
CARD_CLAUSES, assuming you have already proven the cardinality of a
singleton set, ie. CARD {4} = 1:
g `CARD {4} = 1 ==> (CARD {3,4} = 2)`;;
e (SUBGOAL_TAC "" `FINITE {4}`
[REWRITE_TAC[FINITE_RULES;FINITE_INSERT]]);; (* You need finiteness to
reason about cardinality. *)
e (FIRST_ASSUM (SUBST1_TAC o (MATCH_MP (ISPEC `3` (CONJUNCT2
CARD_CLAUSES)))));;
e (DISCH_THEN SUBST1_TAC);;
e (REWRITE_TAC[IN_SING]);;
e (NUM_REDUCE_TAC);;
I'm sure there are others that can suggest better proofs.
More generally it might be easier to build small lemmas to help reason
about such computations more easily, such as:
let CARD_SING = prove ( `!a:A . CARD {a} = 1`, REWRITE_TAC[ONE;MATCH_MP
(ISPECL [`a:A`;`{}:A->bool`] (CONJUNCT2 CARD_CLAUSES)) FINITE_EMPTY;
CARD_CLAUSES;NOT_IN_EMPTY]);;
At least for me it has been standard practice to build my own little
libraries of lemmas to make reasoning about a particular theory easier
and more tailored to my needs.
--
Vincent ARAVANTINOS - PostDoctoral Fellow - Concordia University, Hardware
Verification Group
http://users.encs.concordia.ca/~vincent/
let CARD_CONV =
let T = `T` and F = `F` in
let T_OR_F_CONV c t = try EQT_INTRO (c t) with _ -> c (mk_eq (t,`F`)) in
fun ?dp ->
let dp_filter =
match dp with
|None -> I
|Some dp ->
REWRITE_RULE[COND_DEF] o CONV_RULE (DEPTH_CONV (fun t ->
if t <> T && t <> F then T_OR_F_CONV dp t else failwith "trivial"))
in
fun t ->
let card,s = dest_comb t in
if name_of card <> "CARD" then failwith "Not a `CARD x`-like term";
let rec CARD_CONV_rec s =
try
let _,[x;s'] = strip_comb s in
let fs',cs' = CARD_CONV_rec s' in
let finite,_ = dest_comb (concl fs') in
let fs = ISPEC x (MATCH_MP (CONJUNCT2 CARD_CLAUSES) fs') in
let fs_bis = REWRITE_RULE[cs';NOT_IN_EMPTY;IN_INSERT;ARITH_EQ] fs in
EQT_ELIM (REWRITE_CONV[fs';FINITE_INSERT] (mk_icomb (finite,s))),
CONV_RULE (DEPTH_CONV NUM_SUC_CONV) (dp_filter fs_bis)
with Match_failure _ -> FINITE_EMPTY,CONJUNCT1 CARD_CLAUSES
in
snd (CARD_CONV_rec s);;
let CARD_TAC ?dp =
CONV_TAC (DEPTH_CONV (CARD_CONV ?dp)) THEN REWRITE_TAC[ARITH_EQ];;
------------------------------------------------------------------------------
LogMeIn Central: Instant, anywhere, Remote PC access and management.
Stay in control, update software, and manage PCs from one command center
Diagnose problems and improve visibility into emerging IT issues
Automate, monitor and manage. Do more in less time with Central
http://p.sf.net/sfu/logmein12331_d2d
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
