### Email Archive: hol-info (read-only)

 2003: 2004: 2005: 2006: 2007: 2008: 2009: 2010: 2011: 2012: 2013: Jan Feb Mar Apr May Jun Jul Aug (12) Sep (8) Oct (20) Nov (21) Dec (3) Jan (16) Feb (11) Mar (26) Apr (15) May (17) Jun (10) Jul (3) Aug (4) Sep (11) Oct Nov (11) Dec (8) Jan (16) Feb (18) Mar (22) Apr (23) May (17) Jun (22) Jul (10) Aug (9) Sep (13) Oct (26) Nov (26) Dec (31) Jan (29) Feb (35) Mar (20) Apr (23) May (35) Jun (17) Jul (18) Aug (11) Sep (18) Oct (12) Nov (16) Dec (27) Jan (27) Feb (22) Mar (15) Apr (38) May (26) Jun (24) Jul (8) Aug (20) Sep (21) Oct (23) Nov (20) Dec (24) Jan (16) Feb (19) Mar (24) Apr (54) May (24) Jun (21) Jul (20) Aug (12) Sep (19) Oct (28) Nov (26) Dec (34) Jan (22) Feb (15) Mar (20) Apr (33) May (27) Jun (30) Jul (23) Aug (13) Sep (21) Oct (19) Nov (29) Dec (22) Jan (36) Feb (30) Mar (58) Apr (38) May (34) Jun (35) Jul (22) Aug (8) Sep (40) Oct (27) Nov (29) Dec (23) Jan (31) Feb (39) Mar (30) Apr (49) May (38) Jun (27) Jul (11) Aug (13) Sep (20) Oct (28) Nov (23) Dec (18) Jan (36) Feb (39) Mar (61) Apr (71) May (188) Jun (117) Jul (132) Aug (153) Sep (32) Oct (44) Nov (64) Dec (56) Jan (85) Feb (36) Mar (44) Apr (130) May (43) Jun Jul Aug Sep Oct Nov Dec
S M T W T F S
1 2 3 4 5 6 7
(2) (5) (1) (1)
8 9 10 11 12 13 14
(4) (3) (3) (1)
15 16 17 18 19 20 21
(1)     (1) (1)
22 23 24 25 26 27 28
(3)   (1)
29 30
(2)
 hol-builds hol-info hol-checkins hol-developers Nested Flat Threaded Ultimate Show 25 Show 50 Show 75 Show 100
 [Hol-info] Simple Mathematical induction From: Tony Johnson - 2009-11-11 22:29 Hi, How would I go about proving something simple like this? 1 + 2 + 3 + \dots + n = \frac{n(n+1)}{2} Thanks, 

 Re: [Hol-info] Simple Mathematical induction From: Michael Norrish - 2009-11-11 23:27 Tony Johnson wrote: > How would I go about proving something simple like this? > 1 + 2 + 3 + \dots + n = \frac{n(n+1)}{2} First you need to define your summation. Life is usually easiest if you define things by pattern-matching recursion: val sum_def = Define (sum 0 = 0) /\ (sum (SUC n) = SUC n + sum n) ; Such a definition is a prime candidate for automatic rewriting, so I would then add the definition to the built-in simpset val _ = export_rewrites ["sum_def"] Then you get to state your theorem. Proving things with DIV is usually a pain, so I recast by multiplying both sides by two: val sum_form = store_thm( "sum_form", 2 * sum n = n * (n + 1), ) What's the ? First an induction Induct_on n THEN ... Following induction steps by rewriting is usually safe, so Induct_on n THEN SRW_TAC [][] This eliminates the base case automatically and gives the goal 2 * (SUC n + sum n) = SUC n * (SUC n + 1) ------------------------------------------- 2 * sum n = n * (n + 1) where the formula below the line is the inductive hypothesis. The IH would apply as a rewrite if the multiplication had been pushed into the addition. This is the theorem arithmeticTheory.LEFT_ADD_DISTRIB. Let's assume you have done an open arithmeticTheory so that we don't have to use fully-qualified names everywhere. Then, we can modify our tactic to be Induct_on n THEN SRW_TAC [][LEFT_ADD_DISTRIB] THEN ... This gives 2 * SUC n + (n * n + n) = SUC n * SUC n + SUC n ------------------------------------------------- 2 * sum n = n * (n + 1) The IH has been applied and now our goal is pure arithmetic. As it stands it is not a useful instance of a Presburger formula because of the n * n and the SUC n * SUC n. But the latter can be expanded to a formula including the former with the use of the standard MULT_CLAUSES, which includes the conjuncts |- SUC n * m = n * m + m |- n * SUC m = n + n * m So, we modify the tactic to be Induct_on n THEN SRW_TAC [][LEFT_ADD_DISTRIB, MULT_CLAUSES] THEN ... This gives a goal of 2 + 2 * n + (n * n + n) = n + n * n + (SUC n + 1) --------------------------------------------------- 2 * sum n = n * (n + 1) This is now a good instance of a Presburger formula (with n*n substituted out for an arbitrary variable), meaning that DECIDE_TAC will solve it. So our final tactic is Induct_on n THEN SRW_TAC [][LEFT_ADD_DISTRIB, MULT_CLAUSES] THEN DECIDE_TAC and the final proof looks like val sum_form = store_thm( "sum_form", 2 * sum n = n * (n + 1), Induct_on n THEN SRW_TAC [][LEFT_ADD_DISTRIB, MULT_CLAUSES] THEN DECIDE_TAC) The form with division can subsequently be done (in a slightly hacky way) as val sum_form_div = store_thm( "sum_form_div", sum n = n * (n + 1) DIV 2, SRW_TAC [][Once EQ_SYM_EQ] THEN MATCH_MP_TAC DIV_UNIQUE THEN Q.EXISTS_TAC 0 THEN SRW_TAC [][GSYM sum_form, MULT_COMM]); Michael. 

 [Hol-info] pred_set question From: Michael Norrish - 2009-11-11 22:31 Hi Jianjun, > I have difficulty proving something like > !x y z. ((x UNION y = z) /\ DISJOINT x y) ==> (x = z DIFF y). > Any help please? Simple equalities on sets usually fall over if you attack them with extensionality and METIS_TAC. In this case, the tactic SRW_TAC [][DISJOINT_DEF, EXTENSION] THEN METIS_TAC [] does the job (assuming that you have pred_setTheory open to pick up the theorems DISJOINT_DEF and EXTENSION). Michael. 

 [Hol-info] Call for Bids (ITP 2011) From: Lawrence Paulson - 2009-11-11 15:29 It is time to begin the process of selecting a host for ITP 2011, the International Conference on Interactive Theorem Proving. Following tradition from TPHOLs, the hosts of the previous conference (ITP 2010) are running the process. There are two phases: solicitation of bids and voting. This message concerns the first phase. A long-standing TPHOLs convention is that the conference should be held in a continent different from the location of the previous meeting, and therefore no bids to host ITP 2011 in Europe will be accepted. Based on ITP and TPHOLs history, ITP 2011 will likely be held in July, August or September. (The ACL2 Workshop has taken place at various times of year.) Bids should be sent to itp10@... and should include at least the following information: - name and email address of a contact person - names of other people involved - address of website for the bid - approximate dates of the conference - structure (e.g., k workshop days and n days of presentations followed by excursion...) - advantages of the proposed venue An example of a previous winning bid is here: http://web2.comlab.ox.ac.uk/oucl/conferences/TPHOLs2005/bid.html Deadline for all bids is Monday, 4 January 2010. Shortly after that, the bids will be made public and the voting phase will take place. The people eligible to vote are those who are seriously thinking of attending ITP 2011. The voting system used will be Single Transferable Vote between all received bids. (Note: ACL2 papers will be welcome at ITP 2011, regardless of whether or not there is a separate ACL2 workshop in 2011.) Matt Kaufmann and Larry Paulson