From 35956b7edf34b1ba3fb5c54f4eb108ab08eada03 Mon Sep 17 00:00:00 2001 From: Googler Date: Fri, 14 Feb 2020 01:03:46 -0800 Subject: [PATCH] Second update of HOL Light. PiperOrigin-RevId: 295094515 Change-Id: I5bc27bbba611324f9f1c090e5fa1cb79e03a0704 --- 100/arithmetic.ml | 13 +- 100/arithmetic_geometric_mean.ml | 31 ++- 100/ballot.ml | 108 ++++++++-- 100/bernoulli.ml | 36 +++- 100/bertrand.ml | 63 +++++- 100/birthday.ml | 53 +++-- 100/cantor.ml | 22 ++- 100/cayley_hamilton.ml | 37 +++- 100/ceva.ml | 53 ++++- 100/chords.ml | 24 ++- 100/circle.ml | 35 +++- 100/combinations.ml | 41 +++- 100/constructible.ml | 42 +++- 100/cosine.ml | 75 ++++--- 100/cubic.ml | 15 +- 100/derangements.ml | 38 +++- 100/desargues.ml | 56 ++++-- 100/descartes.ml | 33 +++- 100/dirichlet.ml | 52 ++++- 100/div3.ml | 17 +- 100/divharmonic.ml | 25 ++- 100/e_is_transcendental.ml | 57 ++++-- 100/euler.ml | 60 ++++-- 100/feuerbach.ml | 63 +++++- 100/four_squares.ml | 33 +++- 100/fourier.ml | 48 ++++- 100/friendship.ml | 158 ++++++++++----- 100/fta.ml | 24 ++- 100/gcd.ml | 25 ++- 100/heron.ml | 24 ++- 100/inclusion_exclusion.ml | 29 +++ 100/independence.ml | 39 +++- 100/isosceles.ml | 24 ++- 100/konigsberg.ml | 22 +++ 100/lagrange.ml | 91 +++++---- 100/leibniz.ml | 30 ++- 100/lhopital.ml | 24 ++- 100/liouville.ml | 33 +++- 100/minkowski.ml | 32 ++- 100/morley.ml | 39 +++- 100/pascal.ml | 330 ++++--------------------------- 100/perfect.ml | 28 ++- 100/pick.ml | 78 +++++++- 100/piseries.ml | 40 +++- 100/platonic.ml | 45 ++++- 100/pnt.ml | 53 ++++- 100/polyhedron.ml | 44 ++++- 100/primerecip.ml | 61 +++++- 100/ptolemy.ml | 22 ++- 100/pythagoras.ml | 14 +- 100/quartic.ml | 13 ++ 100/ramsey.ml | 27 +++ 100/ratcountable.ml | 37 +++- 100/realsuncountable.ml | 34 +++- 100/reciprocity.ml | 63 +++++- 100/sqrt.ml | 26 ++- 100/stirling.ml | 31 ++- 100/subsequence.ml | 49 +++-- 100/thales.ml | 64 +++++- 100/triangular.ml | 61 +++++- 100/two_squares.ml | 23 ++- 100/wilson.ml | 46 +++-- Complex/complex_transc.ml | 57 +++++- Complex/complexnumbers.ml | 52 ++++- Examples/machin.ml | 53 ++++- Examples/mangoldt.ml | 85 +++++++- Examples/sos.ml | 1 - Library/agm.ml | 68 ++++++- Library/analysis.ml | 3 + Library/calc_real.ml | 54 ++++- Library/integer.ml | 62 ++++++ Library/multiplicative.ml | 56 +++++- Library/pocklington.ml | 64 +++++- Library/poly.ml | 131 ++++++++---- Library/prime.ml | 25 +++ Library/wo.ml | 1 + Makefile | 4 +- Multivariate/cauchy.ml | 3 + Multivariate/cross.ml | 1 - Multivariate/lpspaces.ml | 81 +++++++- Multivariate/tarski.ml | 62 +++++- api/hol_light_prover.cc | 90 +++++++-- api/hol_light_prover.h | 15 +- api/proof_assistant.proto | 23 ++- api/subprocess_comm.cc | 3 +- api/theorem_fingerprint.cc | 10 +- api/theorem_fingerprint.h | 1 + bool.ml | 2 +- define.ml | 2 +- drule.ml | 2 +- farmhash_compatibility.h | 7 + import_proofs.ml | 6 +- ind_defs.ml | 2 +- log.ml | 8 +- normalize.ml | 100 ++++++++++ pair.ml | 2 +- parse_tactic.ml | 93 ++++++++- pb_printer.ml | 112 +---------- preterm.ml | 12 ++ printer.ml | 12 ++ recursion.ml | 2 +- sandboxee.ml | 96 +++++++-- str_list_fingerprint.cc | 32 --- tests/fingerprint_tests.ml | 48 +++++ tests/normalization_tests.ml | 2 +- tests/parse_tactic_tests.ml | 192 ++++++++++++++++++ tests/run_tests.ml | 1 + tests/test_common.ml | 14 ++ theorem_fingerprint.ml | 22 ++- theorem_fingerprint_c.cc | 35 ++++ 110 files changed, 3850 insertions(+), 872 deletions(-) create mode 100644 farmhash_compatibility.h create mode 100644 normalize.ml delete mode 100644 str_list_fingerprint.cc create mode 100644 tests/fingerprint_tests.ml create mode 100644 tests/parse_tactic_tests.ml create mode 100644 theorem_fingerprint_c.cc diff --git a/100/arithmetic.ml b/100/arithmetic.ml index cd3c9ea6..79a46440 100644 --- a/100/arithmetic.ml +++ b/100/arithmetic.ml @@ -2,12 +2,23 @@ (* Sum of an arithmetic series. *) (* ========================================================================= *) +set_jrh_lexer;; + +open Parser;; +open Tactics;; +open Simp;; +open Nums;; +open Arith;; +open Ints;; +open Iterate;; + + let ARITHMETIC_PROGRESSION_LEMMA = prove (`!n. nsum(0..n) (\i. a + d * i) = ((n + 1) * (2 * a + n * d)) DIV 2`, INDUCT_TAC THEN ASM_REWRITE_TAC[NSUM_CLAUSES_NUMSEG] THEN ARITH_TAC);; let ARITHMETIC_PROGRESSION = prove - (`!n. 1 <= n + (`!n. 1 <= n ==> nsum(0..n-1) (\i. a + d * i) = (n * (2 * a + (n - 1) * d)) DIV 2`, INDUCT_TAC THEN REWRITE_TAC[ARITHMETIC_PROGRESSION_LEMMA; SUC_SUB1] THEN ARITH_TAC);; diff --git a/100/arithmetic_geometric_mean.ml b/100/arithmetic_geometric_mean.ml index bde2ecdd..d7870375 100644 --- a/100/arithmetic_geometric_mean.ml +++ b/100/arithmetic_geometric_mean.ml @@ -1,8 +1,32 @@ (* ========================================================================= *) (* Arithmetic-geometric mean inequality. *) (* ========================================================================= *) +set_jrh_lexer;; +Pb_printer.set_file_tags ["Top100"; "arithmetic_geometric_mean.ml"];; + +open Parser;; +open Equal;; +open Bool;; +open Tactics;; +open Simp;; +open Theorems;; +open Class;; +open Nums;; +open Arith;; +open Calc_num;; +open Realax;; +open Calc_int;; +open Realarith;; +open Reals;; +open Calc_rat;; +open Ints;; +open Iterate;; +open Wo;; + +open Products;; + +open Transc;; -needs "Library/products.ml";; prioritize_real();; (* ------------------------------------------------------------------------- *) @@ -67,7 +91,7 @@ let AGM = prove ASM_CASES_TAC `n = 0` THENL [ASM_REWRITE_TAC[PRODUCT_CLAUSES_NUMSEG; ARITH; SUM_SING_NUMSEG] THEN REAL_ARITH_TAC; - REWRITE_TAC[ADD1] THEN STRIP_TAC THEN MATCH_MP_TAC REAL_LE_TRANS THEN + REWRITE_TAC[ADD1] THEN STRIP_TAC THEN MATCH_MP_TAC REAL_LE_TRANS THEN EXISTS_TAC `x(n + 1) * (sum(1..n) x / &n) pow n` THEN ASM_SIMP_TAC[LEMMA_3; GSYM REAL_OF_NUM_ADD; LE_1; ARITH_RULE `i <= n ==> i <= n + 1`] THEN @@ -78,8 +102,6 @@ let AGM = prove (* Finally, reformulate in the usual way using roots. *) (* ------------------------------------------------------------------------- *) -needs "Library/transc.ml";; - let AGM_ROOT = prove (`!n a. 1 <= n /\ (!i. 1 <= i /\ i <= n ==> &0 <= a(i)) ==> root n (product(1..n) a) <= sum(1..n) a / &n`, @@ -93,3 +115,4 @@ let AGM_ROOT = prove ASM_REWRITE_TAC[IN_NUMSEG; FINITE_NUMSEG]; MATCH_MP_TAC REAL_EQ_IMP_LE THEN MATCH_MP_TAC POW_ROOT_POS THEN ASM_SIMP_TAC[REAL_LE_DIV; REAL_POS; SUM_POS_LE_NUMSEG]]);; +Pb_printer.clear_file_tags();; diff --git a/100/ballot.ml b/100/ballot.ml index c424a4ea..cddc6d7f 100644 --- a/100/ballot.ml +++ b/100/ballot.ml @@ -2,7 +2,81 @@ (* Ballot problem. *) (* ========================================================================= *) -needs "Library/binomial.ml";; +set_jrh_lexer;; +open Lib;; +open Fusion;; +open Basics;; +open Printer;; +open Parser;; +open Equal;; +open Bool;; +open Drule;; +open Log;; +open Import_proofs;; +open Tactics;; +open Itab;; +open Replay;; +open Simp;; +open Embryo_extra;; +open Theorems;; +open Ind_defs;; +open Class;; +open Trivia;; +open Canon;; +open Meson;; +open Metis;; +open Quot;; +open Impconv;; +open Pair;; +open Nums;; +open Recursion;; +open Arith;; +open Wf;; +open Calc_num;; +open Normalizer;; +open Grobner;; +open Ind_types;; +open Lists;; +open Realax;; +open Calc_int;; +open Realarith;; +open Reals;; +open Calc_rat;; +open Ints;; +open Sets;; +open Iterate;; +open Cart;; +open Define;; +open Help;; +open Wo;; +open Binary;; +open Card;; +open Permutations;; +open Products;; +open Floor;; +open Misc;; +open Iter;; + +open Vectors;; +open Determinants;; +open Topology;; +open Convex;; +open Paths;; +open Polytope;; +open Degree;; +open Derivatives;; +open Clifford;; +open Integration;; +open Measure;; + +open Binomial;; +open Complexes;; +open Canal;; +open Transcendentals;; +open Realanalysis;; +open Moretop;; +open Cauchy;; + prioritize_num();; @@ -10,20 +84,20 @@ prioritize_num();; (* Restricted function space. *) (* ------------------------------------------------------------------------- *) -parse_as_infix("-->",(13,"right"));; +parse_as_infix("-->_ballot",(13,"right"));; let funspace = new_definition - `(s --> t) = {f:A->B | (!x. x IN s ==> f(x) IN t) /\ + `(s -->_ballot t) = {f:A->B | (!x. x IN s ==> f(x) IN t) /\ (!x. ~(x IN s) ==> f(x) = @y. T)}`;; let FUNSPACE_EMPTY = prove - (`({} --> t) = {(\x. @y. T)}`, + (`({} -->_ballot t) = {(\x. @y. T)}`, REWRITE_TAC[EXTENSION; IN_SING; funspace; IN_ELIM_THM; NOT_IN_EMPTY] THEN REWRITE_TAC[FUN_EQ_THM]);; let HAS_SIZE_FUNSPACE = prove (`!s:A->bool t:B->bool m n. - s HAS_SIZE m /\ t HAS_SIZE n ==> (s --> t) HAS_SIZE (n EXP m)`, + s HAS_SIZE m /\ t HAS_SIZE n ==> (s -->_ballot t) HAS_SIZE (n EXP m)`, REWRITE_TAC[HAS_SIZE; GSYM CONJ_ASSOC] THEN ONCE_REWRITE_TAC[IMP_CONJ] THEN REWRITE_TAC[RIGHT_FORALL_IMP_THM] THEN @@ -34,9 +108,9 @@ let HAS_SIZE_FUNSPACE = prove ALL_TAC] THEN REWRITE_TAC[GSYM HAS_SIZE] THEN REPEAT STRIP_TAC THEN SUBGOAL_THEN - `(x INSERT s) --> t = + `(x INSERT s) -->_ballot t = IMAGE (\(y:B,g) u:A. if u = x then y else g(u)) - {y,g | y IN t /\ g IN s --> t}` + {y,g | y IN t /\ g IN s -->_ballot t}` SUBST1_TAC THENL [REWRITE_TAC[EXTENSION; IN_IMAGE; funspace; IN_ELIM_THM] THEN ONCE_REWRITE_TAC[TAUT `(a /\ b /\ c) /\ d <=> d /\ a /\ b /\ c`] THEN @@ -67,7 +141,7 @@ let HAS_SIZE_FUNSPACE = prove MATCH_MP_TAC HAS_SIZE_PRODUCT THEN ASM_MESON_TAC[]);; let FINITE_FUNSPACE = prove - (`!s t. FINITE s /\ FINITE t ==> FINITE(s --> t)`, + (`!s t. FINITE s /\ FINITE t ==> FINITE(s -->_ballot t)`, MESON_TAC[HAS_SIZE_FUNSPACE; HAS_SIZE]);; (* ------------------------------------------------------------------------- *) @@ -80,14 +154,14 @@ let vote_INDUCT,vote_RECURSION = define_type let all_countings = new_definition `all_countings a b = let n = a + b in - CARD {f | f IN (1..n --> {A,B}) /\ + CARD {f | f IN (1..n -->_ballot {A,B}) /\ CARD { i | i IN 1..n /\ f(i) = A} = a /\ CARD { i | i IN 1..n /\ f(i) = B} = b}`;; let valid_countings = new_definition `valid_countings a b = let n = a + b in - CARD {f | f IN (1..n --> {A,B}) /\ + CARD {f | f IN (1..n -->_ballot {A,B}) /\ CARD { i | i IN 1..n /\ f(i) = A} = a /\ CARD { i | i IN 1..n /\ f(i) = B} = b /\ !m. 1 <= m /\ m <= n @@ -102,7 +176,7 @@ let vote_CASES = cases "vote" and vote_DISTINCT = distinctness "vote";; let FINITE_COUNTINGS = prove - (`FINITE {f | f IN (1..n --> {A,B}) /\ P f}`, + (`FINITE {f | f IN (1..n -->_ballot {A,B}) /\ P f}`, MATCH_MP_TAC FINITE_RESTRICT THEN MATCH_MP_TAC FINITE_FUNSPACE THEN REWRITE_TAC[FINITE_NUMSEG; FINITE_INSERT; FINITE_RULES]);; @@ -164,7 +238,7 @@ let VOTE_NOT_EQ = prove MESON_TAC[vote_CASES; vote_DISTINCT]);; let FUNSPACE_FIXED = prove - (`{f | f IN (s --> t) /\ (!i. i IN s ==> f i = a)} = + (`{f | f IN (s -->_ballot t) /\ (!i. i IN s ==> f i = a)} = if s = {} \/ a IN t then {(\i. if i IN s then a else @x. T)} else {}`, REWRITE_TAC[EXTENSION; NOT_IN_EMPTY] THEN GEN_TAC THEN COND_CASES_TAC THEN @@ -172,12 +246,12 @@ let FUNSPACE_FIXED = prove REWRITE_TAC[FUN_EQ_THM] THEN ASM_MESON_TAC[]);; let COUNTING_LEMMA = prove - (`CARD {f | f IN (1..(n+1) --> {A,B}) /\ P f} = - CARD {f | f IN (1..n --> {A,B}) /\ P (\i. if i = n + 1 then A else f i)} + - CARD {f | f IN (1..n --> {A,B}) /\ P (\i. if i = n + 1 then B else f i)}`, + (`CARD {f | f IN (1..(n+1) -->_ballot {A,B}) /\ P f} = + CARD {f | f IN (1..n -->_ballot {A,B}) /\ P (\i. if i = n + 1 then A else f i)} + + CARD {f | f IN (1..n -->_ballot {A,B}) /\ P (\i. if i = n + 1 then B else f i)}`, MATCH_MP_TAC EQ_TRANS THEN - EXISTS_TAC `CARD {f | f IN (1..(n+1) --> {A,B}) /\ f(n+1) = A /\ P f} + - CARD {f | f IN (1..(n+1) --> {A,B}) /\ f(n+1) = B /\ P f}` THEN + EXISTS_TAC `CARD {f | f IN (1..(n+1) -->_ballot {A,B}) /\ f(n+1) = A /\ P f} + + CARD {f | f IN (1..(n+1) -->_ballot {A,B}) /\ f(n+1) = B /\ P f}` THEN CONJ_TAC THENL [CONV_TAC "100/ballot.ml:SYM_CONV" SYM_CONV THEN MATCH_MP_TAC CARD_UNION_EQ THEN REWRITE_TAC[FINITE_COUNTINGS; EXTENSION; IN_INTER; IN_UNION] THEN diff --git a/100/bernoulli.ml b/100/bernoulli.ml index 29f70b74..06f04508 100644 --- a/100/bernoulli.ml +++ b/100/bernoulli.ml @@ -2,9 +2,38 @@ (* Bernoulli numbers and polynomials; sum of kth powers. *) (* ========================================================================= *) -needs "Library/binomial.ml";; -needs "Library/analysis.ml";; -needs "Library/transc.ml";; +set_jrh_lexer;; +Pb_printer.set_file_tags ["Top100"; "bernoulli.ml"];; + +open System;; +open Lib;; +open Fusion;; +open Basics;; +open Parser;; +open Equal;; +open Bool;; +open Drule;; +open Tactics;; +open Simp;; +open Theorems;; +open Class;; +open Meson;; +open Pair;; +open Nums;; +open Arith;; +open Calc_num;; +open Realax;; +open Calc_int;; +open Realarith;; +open Reals;; +open Calc_rat;; +open Ints;; +open Iterate;; +open Define;; + +open Binomial;; +open Analysis;; +open Transc;; prioritize_real();; @@ -272,3 +301,4 @@ time SOP_CONV `sum(0..n) (\k. &k pow 18)`;; time SOP_CONV `sum(0..n) (\k. &k pow 19)`;; time SOP_CONV `sum(0..n) (\k. &k pow 20)`;; time SOP_CONV `sum(0..n) (\k. &k pow 21)`;; +Pb_printer.clear_file_tags();; diff --git a/100/bertrand.ml b/100/bertrand.ml index 605716f8..789beeef 100644 --- a/100/bertrand.ml +++ b/100/bertrand.ml @@ -2,12 +2,63 @@ (* Proof of Bertrand conjecture and weak form of prime number theorem. *) (* ========================================================================= *) -needs "Library/prime.ml";; -needs "Library/pocklington.ml";; -needs "Library/analysis.ml";; -needs "Library/transc.ml";; -needs "Library/calc_real.ml";; -needs "Library/floor.ml";; +set_jrh_lexer;; +open System;; +open Lib;; +open Fusion;; +open Basics;; +open Nets;; +open Printer;; +open Parser;; +open Equal;; +open Bool;; +open Drule;; +open Log;; +open Import_proofs;; +open Tactics;; +open Itab;; +open Replay;; +open Simp;; +open Embryo_extra;; +open Theorems;; +open Ind_defs;; +open Class;; +open Trivia;; +open Canon;; +open Meson;; +open Metis;; +open Quot;; +open Impconv;; +open Pair;; +open Nums;; +open Recursion;; +open Arith;; +open Wf;; +open Calc_num;; +open Normalizer;; +open Grobner;; +open Ind_types;; +open Lists;; +open Realax;; +open Calc_int;; +open Realarith;; +open Reals;; +open Calc_rat;; +open Ints;; +open Sets;; +open Iterate;; +open Cart;; +open Define;; +open Help;; +open Wo;; + + +open Floor;; +open Analysis;; +open Transc;; +open Prime;; +open Pocklington;; +open Calc_real;; prioritize_real();; diff --git a/100/birthday.ml b/100/birthday.ml index 979e1ea6..21b737c9 100644 --- a/100/birthday.ml +++ b/100/birthday.ml @@ -2,16 +2,37 @@ (* Birthday problem. *) (* ========================================================================= *) +set_jrh_lexer;; +Pb_printer.set_file_tags ["Top100"; "100/birthday.ml"];; + +open Lib;; +open Printer;; +open Parser;; +open Equal;; +open Drule;; +open Tactics;; +open Simp;; +open Theorems;; +open Class;; +open Meson;; +open Pair;; +open Nums;; +open Arith;; +open Calc_num;; +open Realax;; +open Ints;; +open Sets;; + prioritize_num();; (* ------------------------------------------------------------------------- *) (* Restricted function space. *) (* ------------------------------------------------------------------------- *) -parse_as_infix("-->",(13,"right"));; +parse_as_infix("-->_bday",(13,"right"));; let funspace = new_definition - `(s --> t) = {f:A->B | (!x. x IN s ==> f(x) IN t) /\ + `(s -->_bday t) = {f:A->B | (!x. x IN s ==> f(x) IN t) /\ (!x. ~(x IN s) ==> f(x) = @y. T)}`;; (* ------------------------------------------------------------------------- *) @@ -19,13 +40,13 @@ let funspace = new_definition (* ------------------------------------------------------------------------- *) let FUNSPACE_EMPTY = prove - (`({} --> t) = {(\x. @y. T)}`, + (`({} -->_bday t) = {(\x. @y. T)}`, REWRITE_TAC[EXTENSION; IN_SING; funspace; IN_ELIM_THM; NOT_IN_EMPTY] THEN REWRITE_TAC[FUN_EQ_THM]);; let HAS_SIZE_FUNSPACE = prove (`!s:A->bool t:B->bool m n. - s HAS_SIZE m /\ t HAS_SIZE n ==> (s --> t) HAS_SIZE (n EXP m)`, + s HAS_SIZE m /\ t HAS_SIZE n ==> (s -->_bday t) HAS_SIZE (n EXP m)`, REWRITE_TAC[HAS_SIZE; GSYM CONJ_ASSOC] THEN ONCE_REWRITE_TAC[IMP_CONJ] THEN REWRITE_TAC[RIGHT_FORALL_IMP_THM] THEN @@ -36,9 +57,9 @@ let HAS_SIZE_FUNSPACE = prove ALL_TAC] THEN REWRITE_TAC[GSYM HAS_SIZE] THEN REPEAT STRIP_TAC THEN SUBGOAL_THEN - `(x INSERT s) --> t = + `(x INSERT s) -->_bday t = IMAGE (\(y:B,g) u:A. if u = x then y else g(u)) - {y,g | y IN t /\ g IN s --> t}` + {y,g | y IN t /\ g IN s -->_bday t}` SUBST1_TAC THENL [REWRITE_TAC[EXTENSION; IN_IMAGE; funspace; IN_ELIM_THM] THEN ONCE_REWRITE_TAC[TAUT `(a /\ b /\ c) /\ d <=> d /\ a /\ b /\ c`] THEN @@ -90,7 +111,7 @@ let FACT_DIV_MULT = prove let HAS_SIZE_FUNSPACE_INJECTIVE = prove (`!s:A->bool t:B->bool m n. s HAS_SIZE m /\ t HAS_SIZE n - ==> {f | f IN (s --> t) /\ + ==> {f | f IN (s -->_bday t) /\ (!x y. x IN s /\ y IN s /\ f x = f y ==> x = y)} HAS_SIZE (if n < m then 0 else (FACT n) DIV (FACT(n - m)))`, REWRITE_TAC[HAS_SIZE; GSYM CONJ_ASSOC] THEN @@ -106,11 +127,11 @@ let HAS_SIZE_FUNSPACE_INJECTIVE = prove ALL_TAC] THEN REWRITE_TAC[GSYM HAS_SIZE] THEN REPEAT STRIP_TAC THEN SUBGOAL_THEN - `{f | f IN (x INSERT s) --> t /\ + `{f | f IN (x INSERT s) -->_bday t /\ (!u v. u IN (x INSERT s) /\ v IN (x INSERT s) /\ f u = f v ==> u = v)} = IMAGE (\(y:B,g) u:A. if u = x then y else g(u)) {y,g | y IN t /\ - g IN {f | f IN (s --> (t DELETE y)) /\ + g IN {f | f IN (s -->_bday (t DELETE y)) /\ !u v. u IN s /\ v IN s /\ f u = f v ==> u = v}}` SUBST1_TAC THENL [REWRITE_TAC[EXTENSION; IN_IMAGE; funspace; IN_ELIM_THM] THEN @@ -181,16 +202,16 @@ let HAS_SIZE_DIFF = prove let BIRTHDAY_THM = prove (`!s:A->bool t:B->bool m n. s HAS_SIZE m /\ t HAS_SIZE n - ==> {f | f IN (s --> t) /\ + ==> {f | f IN (s -->_bday t) /\ ?x y. x IN s /\ y IN s /\ ~(x = y) /\ f(x) = f(y)} HAS_SIZE (if m <= n then (n EXP m) - (FACT n) DIV (FACT(n - m)) else n EXP m)`, REPEAT STRIP_TAC THEN REWRITE_TAC[SET_RULE - `{f:A->B | f IN (s --> t) /\ + `{f:A->B | f IN (s -->_bday t) /\ ?x y. x IN s /\ y IN s /\ ~(x = y) /\ f(x) = f(y)} = - (s --> t) DIFF - {f | f IN (s --> t) /\ + (s -->_bday t) DIFF + {f | f IN (s -->_bday t) /\ (!x y. x IN s /\ y IN s /\ f x = f y ==> x = y)}`] THEN REWRITE_TAC[ARITH_RULE `(if a <= b then x - y else x) = x - (if b < a then 0 else y)`] THEN @@ -217,9 +238,9 @@ let FACT_DIV_SIMP = prove let BIRTHDAY_THM_EXPLICIT = prove (`!s t. s HAS_SIZE 23 /\ t HAS_SIZE 365 - ==> 2 * CARD {f | f IN (s --> t) /\ + ==> 2 * CARD {f | f IN (s -->_bday t) /\ ?x y. x IN s /\ y IN s /\ ~(x = y) /\ f(x) = f(y)} - >= CARD (s --> t)`, + >= CARD (s -->_bday t)`, REPEAT GEN_TAC THEN DISCH_TAC THEN FIRST_ASSUM(MP_TAC o MATCH_MP BIRTHDAY_THM) THEN FIRST_ASSUM(MP_TAC o MATCH_MP HAS_SIZE_FUNSPACE) THEN @@ -230,3 +251,5 @@ let BIRTHDAY_THM_EXPLICIT = prove SIMP_TAC[DIV_REFL; GSYM LT_NZ; FACT_LT] THEN REWRITE_TAC[HAS_SIZE] THEN REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[] THEN CONV_TAC "100/birthday.ml:NUM_REDUCE_CONV" NUM_REDUCE_CONV);; + +Pb_printer.clear_file_tags();; diff --git a/100/cantor.ml b/100/cantor.ml index 03857653..8743ec0d 100644 --- a/100/cantor.ml +++ b/100/cantor.ml @@ -2,6 +2,22 @@ (* Cantor's theorem. *) (* ========================================================================= *) +set_jrh_lexer;; +Pb_printer.set_file_tags ["Top100"; "100/cantor.ml"];; + +open Lib;; +open Parser;; +open Equal;; +open Bool;; +open Drule;; +open Tactics;; +open Simp;; +open Class;; +open Trivia;; +open Meson;; +open Sets;; + + (* ------------------------------------------------------------------------- *) (* Ad hoc version for whole type. *) (* ------------------------------------------------------------------------- *) @@ -73,7 +89,7 @@ let CANTOR_TAYLOR = prove ASM_MESON_TAC[]);; let SURJECTIVE_COMPOSE = prove - (`(!y. ?x. f(x) = y) /\ (!z. ?y. g(y) = z) + (`(!y. ?x. f(x) = y) /\ (!z. ?y. g(y) = z) ==> (!z. ?x. (g o f) x = z)`, MESON_TAC[o_THM]);; @@ -93,5 +109,7 @@ let CANTOR_JOHNSTONE = prove (REWRITE_RULE[NOT_EXISTS_THM] CANTOR)) THEN REWRITE_TAC[] THEN MATCH_MP_TAC SURJECTIVE_COMPOSE THEN ASM_REWRITE_TAC[SURJECTIVE_IMAGE] THEN - MATCH_MP_TAC INJECTIVE_SURJECTIVE_PREIMAGE THEN + MATCH_MP_TAC INJECTIVE_SURJECTIVE_PREIMAGE THEN ASM_REWRITE_TAC[]);; + +Pb_printer.clear_file_tags();; diff --git a/100/cayley_hamilton.ml b/100/cayley_hamilton.ml index 7b1154aa..1d9b7f92 100644 --- a/100/cayley_hamilton.ml +++ b/100/cayley_hamilton.ml @@ -2,7 +2,41 @@ (* The Cayley-Hamilton theorem (for real matrices). *) (* ========================================================================= *) -needs "Multivariate/complexes.ml";; +set_jrh_lexer;; +Pb_printer.set_file_tags ["Top100"; "cayley_hamilton.ml"];; + +open Lib;; +open Printer;; +open Parser;; +open Equal;; +open Bool;; +open Drule;; +open Tactics;; +open Simp;; +open Theorems;; +open Class;; +open Trivia;; +open Meson;; +open Pair;; +open Nums;; +open Arith;; +open Calc_num;; +open Realax;; +open Calc_int;; +open Realarith;; +open Reals;; +open Calc_rat;; +open Ints;; +open Sets;; +open Iterate;; +open Cart;; +open Define;; +open Permutations;; +open Products;; +open Misc;; + +open Vectors;; +open Determinants;; (* ------------------------------------------------------------------------- *) (* Powers of a square matrix (mpow) and sums of matrices (msum). *) @@ -444,3 +478,4 @@ let CAYLEY_HAMILTON = prove MAP_EVERY EXISTS_TAC [`A:real^N^N`; `(\i. B i + C i):num->real^N^N`; `dimindex(:N)-1`] THEN SIMP_TAC[GSYM MSUM_ADD; FINITE_NUMSEG; MATRIX_CMUL_ADD_LDISTRIB]]);; +Pb_printer.clear_file_tags();; diff --git a/100/ceva.ml b/100/ceva.ml index 0dd66414..12e84a7c 100644 --- a/100/ceva.ml +++ b/100/ceva.ml @@ -2,8 +2,57 @@ (* #61: Ceva's theorem. *) (* ========================================================================= *) -needs "Multivariate/convex.ml";; -needs "Examples/sos.ml";; +set_jrh_lexer;; +open System;; +open Lib;; +open Fusion;; +open Basics;; +open Printer;; +open Parser;; +open Equal;; +open Bool;; +open Drule;; +open Log;; +open Import_proofs;; +open Tactics;; +open Itab;; +open Replay;; +open Simp;; +open Embryo_extra;; +open Theorems;; +open Ind_defs;; +open Class;; +open Trivia;; +open Canon;; +open Meson;; +open Metis;; +open Quot;; +open Impconv;; +open Pair;; +open Nums;; +open Recursion;; +open Arith;; +open Wf;; +open Calc_num;; +open Normalizer;; +open Grobner;; +open Ind_types;; +open Lists;; +open Realax;; +open Calc_int;; +open Realarith;; +open Reals;; +open Calc_rat;; +open Ints;; +open Sets;; +open Iterate;; +open Cart;; +open Define;; +open Help;; + +open Vectors;; +open Convex;; +open Sos;; prioritize_real();; diff --git a/100/chords.ml b/100/chords.ml index b5b0473e..77fede5d 100644 --- a/100/chords.ml +++ b/100/chords.ml @@ -2,7 +2,28 @@ (* #55: Theorem on product of segments of chords. *) (* ========================================================================= *) -needs "Multivariate/convex.ml";; +set_jrh_lexer;; +Pb_printer.set_file_tags ["Top100"; "chords.ml"];; + +open Lib;; +open Parser;; +open Equal;; +open Bool;; +open Tactics;; +open Simp;; +open Theorems;; +open Meson;; +open Pair;; +open Calc_num;; +open Realax;; +open Realarith;; +open Reals;; +open Calc_rat;; +open Sets;; +open Cart;; + +open Vectors;; +open Convex;; prioritize_real();; @@ -63,3 +84,4 @@ let SEGMENT_CHORDS = prove SIMP_TAC[dot; SUM_2; VECTOR_SUB_COMPONENT; DIMINDEX_2; VECTOR_ADD_COMPONENT; CART_EQ; FORALL_2; VECTOR_MUL_COMPONENT; ARITH] THEN CONV_TAC "100/chords.ml:REAL_RING" REAL_RING);; +Pb_printer.clear_file_tags();; diff --git a/100/circle.ml b/100/circle.ml index 9a3ffd0c..72ff5bfc 100644 --- a/100/circle.ml +++ b/100/circle.ml @@ -2,8 +2,38 @@ (* Area of a circle. *) (* ========================================================================= *) -needs "Multivariate/measure.ml";; -needs "Multivariate/realanalysis.ml";; +set_jrh_lexer;; +Pb_printer.set_file_tags ["Top100"; "circle.ml"];; + +open Lib;; +open Fusion;; +open Parser;; +open Equal;; +open Bool;; +open Drule;; +open Tactics;; +open Simp;; +open Theorems;; +open Class;; +open Trivia;; +open Calc_num;; +open Realax;; +open Calc_int;; +open Realarith;; +open Reals;; +open Calc_rat;; +open Sets;; +open Cart;; +open Misc;; + +open Vectors;; +open Determinants;; +open Topology;; +open Convex;; +open Integration;; +open Measure;; +open Transcendentals;; +open Realanalysis;; (* ------------------------------------------------------------------------- *) (* Circle area. Should maybe extend WLOG tactics for such scaling. *) @@ -138,3 +168,4 @@ let VOLUME_BALL = prove SIMP_TAC[GSYM INTERIOR_CBALL; GSYM VOLUME_CBALL] THEN REPEAT STRIP_TAC THEN MATCH_MP_TAC MEASURE_INTERIOR THEN SIMP_TAC[BOUNDED_CBALL; NEGLIGIBLE_CONVEX_FRONTIER; CONVEX_CBALL]);; +Pb_printer.clear_file_tags();; diff --git a/100/combinations.ml b/100/combinations.ml index d86e27cd..c46ba15b 100644 --- a/100/combinations.ml +++ b/100/combinations.ml @@ -2,6 +2,27 @@ (* Binomial coefficients and relation to number of combinations. *) (* ========================================================================= *) +set_jrh_lexer;; +Pb_printer.set_file_tags ["Top100"; "100/combinations.ml"];; + +open Lib;; +open Parser;; +open Equal;; +open Bool;; +open Tactics;; +open Simp;; +open Theorems;; +open Class;; +open Meson;; +open Nums;; +open Arith;; +open Calc_num;; +open Grobner;; +open Realax;; +open Ints;; +open Sets;; +open Define;; + prioritize_num();; (* ------------------------------------------------------------------------- *) @@ -34,12 +55,12 @@ let BINOM_FACT = prove REWRITE_TAC[ADD_CLAUSES; FACT; binom] THEN CONV_TAC "100/combinations.ml:NUM_RING" NUM_RING);; let BINOM_EXPLICIT = prove - (`!n k. binom(n,k) = + (`!n k. binom(n,k) = if n < k then 0 else FACT(n) DIV (FACT(k) * FACT(n - k))`, REPEAT STRIP_TAC THEN COND_CASES_TAC THEN ASM_SIMP_TAC[BINOM_LT] THEN POP_ASSUM MP_TAC THEN REWRITE_TAC[NOT_LT; LE_EXISTS] THEN STRIP_TAC THEN ASM_REWRITE_TAC[ADD_SUB2] THEN CONV_TAC "100/combinations.ml:SYM_CONV" SYM_CONV THEN - MATCH_MP_TAC DIV_UNIQ THEN EXISTS_TAC `0` THEN + MATCH_MP_TAC DIV_UNIQ THEN EXISTS_TAC `0` THEN SIMP_TAC[LT_MULT; FACT_LT; ADD_CLAUSES] THEN ONCE_REWRITE_TAC[ADD_SYM] THEN REWRITE_TAC[GSYM BINOM_FACT] THEN REWRITE_TAC[MULT_AC]);; @@ -74,11 +95,11 @@ let lemma = prove (* ------------------------------------------------------------------------- *) let BINOM_INDUCT = prove - (`!P. (!n. P n 0) /\ - (!k. P 0 (SUC k)) /\ + (`!P. (!n. P n 0) /\ + (!k. P 0 (SUC k)) /\ (!n k. P n (SUC k) /\ P n k ==> P (SUC n) (SUC k)) - ==> !m n. P m n`, - GEN_TAC THEN STRIP_TAC THEN REPEAT INDUCT_TAC THEN ASM_MESON_TAC[]);; + ==> !m n. P m n`, + GEN_TAC THEN STRIP_TAC THEN REPEAT INDUCT_TAC THEN ASM_MESON_TAC[]);; let NUMBER_OF_COMBINATIONS = prove (`!n m s:A->bool. @@ -108,9 +129,11 @@ let NUMBER_OF_COMBINATIONS = prove (* Explicit version. *) (* ------------------------------------------------------------------------- *) -let NUMBER_OF_COMBINATIONS_EXPLICIT = prove - (`!n m s:A->bool. - s HAS_SIZE n +let NUMBER_OF_COMBINATIONS_EXPLICIT = prove + (`!n m s:A->bool. + s HAS_SIZE n ==> {t | t SUBSET s /\ t HAS_SIZE m} HAS_SIZE (if n < m then 0 else FACT(n) DIV (FACT(m) * FACT(n - m)))`, REWRITE_TAC[REWRITE_RULE[BINOM_EXPLICIT] NUMBER_OF_COMBINATIONS]);; + +Pb_printer.clear_file_tags();; diff --git a/100/constructible.ml b/100/constructible.ml index 3c29cb13..89eeb57c 100644 --- a/100/constructible.ml +++ b/100/constructible.ml @@ -8,9 +8,44 @@ (* Dickson's "First Course in the Theory of Equations", chapter III. *) (* ========================================================================= *) -needs "Library/prime.ml";; -needs "Library/floor.ml";; -needs "Multivariate/transcendentals.ml";; +set_jrh_lexer;; +Pb_printer.set_file_tags ["Top100"; "constructible.ml"];; + +open Lib;; +open Fusion;; +open Basics;; +open Parser;; +open Equal;; +open Bool;; +open Drule;; +open Tactics;; +open Simp;; +open Theorems;; +open Ind_defs;; +open Class;; +open Meson;; +open Pair;; +open Nums;; +open Arith;; +open Calc_num;; +open Grobner;; +open Ind_types;; +open Realax;; +open Calc_int;; +open Realarith;; +open Reals;; +open Calc_rat;; +open Ints;; +open Sets;; +open Cart;; +open Define;; +open Wo;; +open Floor;; +open Misc;; + +open Vectors;; +open Transcendentals;; +open Prime;; prioritize_real();; @@ -896,3 +931,4 @@ let TRISECT_60_DEGREES = prove `&1 / &2 = &4 * c pow 3 - &3 * c <=> (&2 * c) pow 3 - &3 * (&2 * c) - &1 = &0`] THEN ASM_MESON_TAC[TRISECT_60_DEGREES_ALGEBRA; RADICAL_RULES]);; +Pb_printer.clear_file_tags();; diff --git a/100/cosine.ml b/100/cosine.ml index b6c844c5..4ace1a92 100644 --- a/100/cosine.ml +++ b/100/cosine.ml @@ -2,10 +2,36 @@ (* The law of cosines, of sines, and sum of angles of a triangle. *) (* ========================================================================= *) -needs "Multivariate/transcendentals.ml";; +set_jrh_lexer;; +Pb_printer.set_file_tags ["Top100"; "cosine.ml"];; + +open Lib;; +open Parser;; +open Equal;; +open Bool;; +open Drule;; +open Tactics;; +open Simp;; +open Theorems;; +open Class;; +open Meson;; +open Pair;; +open Calc_num;; +open Realax;; +open Calc_int;; +open Realarith;; +open Reals;; +open Calc_rat;; +open Ints;; +open Floor;; + +open Vectors;; +open Transcendentals;; prioritize_vector();; +(* TODO(smloos): Some duplicates with geom.ml, consider depending on geom.*) + (* ------------------------------------------------------------------------- *) (* Angle between vectors (always 0 <= angle <= pi). *) (* ------------------------------------------------------------------------- *) @@ -18,8 +44,8 @@ let vangle = new_definition (* Traditional geometric notion of angle (but always 0 <= theta <= pi). *) (* ------------------------------------------------------------------------- *) -let angle = new_definition - `angle(a,b,c) = vangle (a - b) (c - b)`;; +let cosine_angle = new_definition + `cosine_angle(a,b,c) = vangle (a - b) (c - b)`;; (* ------------------------------------------------------------------------- *) (* Lemmas (more than we need for this result). *) @@ -79,8 +105,8 @@ let VANGLE_EQ_PI = prove VECTOR_ARITH_TAC);; let ANGLE_EQ_PI = prove - (`!A B C:real^N. angle(A,B,C) = pi ==> dist(A,C) = dist(A,B) + dist(B,C)`, - REPEAT GEN_TAC THEN REWRITE_TAC[angle] THEN + (`!A B C:real^N. cosine_angle(A,B,C) = pi ==> dist(A,C) = dist(A,B) + dist(B,C)`, + REPEAT GEN_TAC THEN REWRITE_TAC[cosine_angle] THEN DISCH_THEN(MP_TAC o MATCH_MP VANGLE_EQ_PI) THEN REWRITE_TAC[VECTOR_ARITH `a + x % (b - c) = vec 0 <=> a = x % (c - b)`] THEN GEN_REWRITE_TAC "100/cosine.ml:(funpow 3 LAND_CONV)" (funpow 3 LAND_CONV) [NORM_SUB] THEN @@ -89,30 +115,30 @@ let ANGLE_EQ_PI = prove REWRITE_TAC[dist; NORM_SUB]);; let SIN_ANGLE_POS = prove - (`!A B C. &0 <= sin(angle(A,B,C))`, - SIMP_TAC[SIN_POS_PI_LE; angle; VANGLE_RANGE]);; + (`!A B C. &0 <= sin(cosine_angle(A,B,C))`, + SIMP_TAC[SIN_POS_PI_LE; cosine_angle; VANGLE_RANGE]);; let ANGLE = prove - (`!A B C. (A - C) dot (B - C) = dist(A,C) * dist(B,C) * cos(angle(A,C,B))`, - REWRITE_TAC[angle; dist; GSYM VANGLE]);; + (`!A B C. (A - C) dot (B - C) = dist(A,C) * dist(B,C) * cos(cosine_angle(A,C,B))`, + REWRITE_TAC[cosine_angle; dist; GSYM VANGLE]);; let ANGLE_REFL = prove - (`!A B. angle(A,A,B) = pi / &2 /\ - angle(B,A,A) = pi / &2`, - REWRITE_TAC[angle; vangle; VECTOR_SUB_REFL]);; + (`!A B. cosine_angle(A,A,B) = pi / &2 /\ + cosine_angle(B,A,A) = pi / &2`, + REWRITE_TAC[cosine_angle; vangle; VECTOR_SUB_REFL]);; let ANGLE_REFL_MID = prove - (`!A B. ~(A = B) ==> angle(A,B,A) = &0`, - SIMP_TAC[angle; vangle; VECTOR_SUB_EQ; GSYM NORM_POW_2; GSYM REAL_POW_2; + (`!A B. ~(A = B) ==> cosine_angle(A,B,A) = &0`, + SIMP_TAC[cosine_angle; vangle; VECTOR_SUB_EQ; GSYM NORM_POW_2; GSYM REAL_POW_2; REAL_DIV_REFL; ACS_1; REAL_POW_EQ_0; ARITH; NORM_EQ_0]);; let ANGLE_SYM = prove - (`!A B C. angle(A,B,C) = angle(C,B,A)`, - REWRITE_TAC[angle; vangle; VECTOR_SUB_EQ; DISJ_SYM; REAL_MUL_SYM; DOT_SYM]);; + (`!A B C. cosine_angle(A,B,C) = cosine_angle(C,B,A)`, + REWRITE_TAC[cosine_angle; vangle; VECTOR_SUB_EQ; DISJ_SYM; REAL_MUL_SYM; DOT_SYM]);; let ANGLE_RANGE = prove - (`!A B C. &0 <= angle(A,B,C) /\ angle(A,B,C) <= pi`, - REWRITE_TAC[angle; VANGLE_RANGE]);; + (`!A B C. &0 <= cosine_angle(A,B,C) /\ cosine_angle(A,B,C) <= pi`, + REWRITE_TAC[cosine_angle; VANGLE_RANGE]);; (* ------------------------------------------------------------------------- *) (* The law of cosines. *) @@ -121,9 +147,9 @@ let ANGLE_RANGE = prove let LAW_OF_COSINES = prove (`!A B C:real^N. dist(B,C) pow 2 = dist(A,B) pow 2 + dist(A,C) pow 2 - - &2 * dist(A,B) * dist(A,C) * cos(angle(B,A,C))`, + &2 * dist(A,B) * dist(A,C) * cos(cosine_angle(B,A,C))`, REPEAT GEN_TAC THEN - REWRITE_TAC[angle; ONCE_REWRITE_RULE[NORM_SUB] dist; GSYM VANGLE; + REWRITE_TAC[cosine_angle; ONCE_REWRITE_RULE[NORM_SUB] dist; GSYM VANGLE; NORM_POW_2] THEN VECTOR_ARITH_TAC);; @@ -133,7 +159,7 @@ let LAW_OF_COSINES = prove let LAW_OF_SINES = prove (`!A B C:real^N. - sin(angle(A,B,C)) * dist(B,C) = sin(angle(B,A,C)) * dist(A,C)`, + sin(cosine_angle(A,B,C)) * dist(B,C) = sin(cosine_angle(B,A,C)) * dist(A,C)`, REPEAT GEN_TAC THEN MATCH_MP_TAC REAL_POW_EQ THEN EXISTS_TAC `2` THEN SIMP_TAC[SIN_ANGLE_POS; DIST_POS_LE; REAL_LE_MUL; ARITH] THEN REWRITE_TAC[REAL_POW_MUL; MATCH_MP @@ -158,7 +184,7 @@ let LAW_OF_SINES = prove let TRIANGLE_ANGLE_SUM_LEMMA = prove (`!A B C:real^N. ~(A = B) /\ ~(A = C) /\ ~(B = C) - ==> cos(angle(B,A,C) + angle(A,B,C) + angle(B,C,A)) = -- &1`, + ==> cos(cosine_angle(B,A,C) + cosine_angle(A,B,C) + cosine_angle(B,C,A)) = -- &1`, REPEAT GEN_TAC THEN ONCE_REWRITE_TAC[GSYM VECTOR_SUB_EQ] THEN REWRITE_TAC[GSYM NORM_EQ_0] THEN MP_TAC(ISPECL [`A:real^N`; `B:real^N`; `C:real^N`] LAW_OF_COSINES) THEN @@ -169,7 +195,7 @@ let TRIANGLE_ANGLE_SUM_LEMMA = prove MP_TAC(ISPECL [`B:real^N`; `C:real^N`; `A:real^N`] LAW_OF_SINES) THEN REWRITE_TAC[COS_ADD; SIN_ADD; dist; NORM_SUB] THEN MAP_EVERY (fun t -> MP_TAC(SPEC t SIN_CIRCLE)) - [`angle(B:real^N,A,C)`; `angle(A:real^N,B,C)`; `angle(B:real^N,C,A)`] THEN + [`cosine_angle(B:real^N,A,C)`; `cosine_angle(A:real^N,B,C)`; `cosine_angle(B:real^N,C,A)`] THEN REWRITE_TAC[COS_ADD; SIN_ADD; ANGLE_SYM] THEN CONV_TAC "100/cosine.ml:REAL_RING" REAL_RING);; let COS_MINUS1_LEMMA = prove @@ -196,7 +222,7 @@ let COS_MINUS1_LEMMA = prove let TRIANGLE_ANGLE_SUM = prove (`!A B C:real^N. ~(A = B) /\ ~(A = C) /\ ~(B = C) - ==> angle(B,A,C) + angle(A,B,C) + angle(B,C,A) = pi`, + ==> cosine_angle(B,A,C) + cosine_angle(A,B,C) + cosine_angle(B,C,A) = pi`, REPEAT STRIP_TAC THEN MATCH_MP_TAC COS_MINUS1_LEMMA THEN ASM_SIMP_TAC[TRIANGLE_ANGLE_SUM_LEMMA; REAL_LE_ADD; ANGLE_RANGE] THEN MATCH_MP_TAC(REAL_ARITH @@ -208,3 +234,4 @@ let TRIANGLE_ANGLE_SUM = prove REPEAT(FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE RAND_CONV [GSYM VECTOR_SUB_EQ])) THEN REWRITE_TAC[GSYM NORM_EQ_0; dist; NORM_SUB] THEN REAL_ARITH_TAC);; +Pb_printer.clear_file_tags();; diff --git a/100/cubic.ml b/100/cubic.ml index 379470db..80522f8d 100644 --- a/100/cubic.ml +++ b/100/cubic.ml @@ -2,7 +2,19 @@ (* Cubic formula. *) (* ========================================================================= *) -needs "Complex/complex_transc.ml";; +set_jrh_lexer;; +Pb_printer.set_file_tags ["Top100"; "cubic.ml"];; + +open Parser;; +open Equal;; +open Tactics;; +open Simp;; +open Class;; +open Meson;; +open Pair;; + +open Complexnumbers;; +open Complex_transc;; prioritize_complex();; @@ -96,3 +108,4 @@ let CUBIC = prove ASM_MESON_TAC[CCBRT]; MP_TAC COMPLEX_POW_II_2 THEN CONV_TAC "100/cubic.ml:COMPLEX_RING" COMPLEX_RING; ASM_MESON_TAC[CSQRT]]);; +Pb_printer.clear_file_tags();; diff --git a/100/derangements.ml b/100/derangements.ml index 56b1e2fb..eb48de52 100644 --- a/100/derangements.ml +++ b/100/derangements.ml @@ -2,9 +2,40 @@ (* #88: Formula for the number of derangements: round[n!/e] *) (* ========================================================================= *) -needs "Library/transc.ml";; -needs "Library/calc_real.ml";; -needs "Library/floor.ml";; +set_jrh_lexer;; +Pb_printer.set_file_tags ["Top100"; "derangements.ml"];; + +open Lib;; +open Fusion;; +open Printer;; +open Parser;; +open Equal;; +open Bool;; +open Drule;; +open Tactics;; +open Simp;; +open Theorems;; +open Class;; +open Meson;; +open Pair;; +open Nums;; +open Arith;; +open Calc_num;; +open Realax;; +open Calc_int;; +open Realarith;; +open Reals;; +open Calc_rat;; +open Ints;; +open Sets;; +open Iterate;; +open Define;; + + +open Analysis;; +open Transc;; +open Calc_real;; +open Floor;; let PAIR_BETA_THM = GEN_BETA_CONV `(\(x,y). P x y) (a,b)`;; @@ -595,3 +626,4 @@ let THE_DERANGEMENTS_FORMULA = prove REPEAT STRIP_TAC THEN FIRST_X_ASSUM(MP_TAC o MATCH_MP NUMBER_OF_DERANGEMENTS) THEN ASM_SIMP_TAC[HAS_SIZE; DERANGEMENTS_EXP]);; +Pb_printer.clear_file_tags();; diff --git a/100/desargues.ml b/100/desargues.ml index 9dbda30d..e1a1995a 100644 --- a/100/desargues.ml +++ b/100/desargues.ml @@ -2,7 +2,38 @@ (* #87: Desargues's theorem. *) (* ========================================================================= *) -needs "Multivariate/cross.ml";; +set_jrh_lexer;; +Pb_printer.set_file_tags ["Top100"; "desargues.ml"];; + +open Lib;; +open Fusion;; +open Printer;; +open Parser;; +open Equal;; +open Bool;; +open Drule;; +open Tactics;; +open Simp;; +open Theorems;; +open Class;; +open Meson;; +open Quot;; +open Pair;; +open Nums;; +open Arith;; +open Calc_num;; +open Realax;; +open Calc_int;; +open Reals;; +open Calc_rat;; +open Ints;; +open Sets;; +open Cart;; +open Define;; + +open Vectors;; +open Determinants;; +open Cross;; (* ------------------------------------------------------------------------- *) (* A lemma we want to justify some of the axioms. *) @@ -190,8 +221,8 @@ let homop = prove (* Key equivalences of concepts in projective space and homogeneous coords. *) (* ------------------------------------------------------------------------- *) -let parallel = new_definition - `parallel x y <=> x cross y = vec 0`;; +let desargues_parallel = new_definition + `desargues_parallel x y <=> x cross y = vec 0`;; let ON_HOMOL = prove (`!p l. p on l <=> orthogonal (homop p) (homol l)`, @@ -202,16 +233,16 @@ let ON_HOMOL = prove MESON_TAC[homol; homop; direction_tybij]);; let EQ_HOMOL = prove - (`!l l'. l = l' <=> parallel (homol l) (homol l')`, + (`!l l'. l = l' <=> desargues_parallel (homol l) (homol l')`, REPEAT GEN_TAC THEN GEN_REWRITE_TAC "100/desargues.ml:(LAND_CONV o BINOP_CONV)" (LAND_CONV o BINOP_CONV) [homol] THEN REWRITE_TAC[projl; MESON[fst line_tybij; snd line_tybij] `mk_line((||) l) = mk_line((||) l') <=> (||) l = (||) l'`] THEN - REWRITE_TAC[PARDIR_EQUIV] THEN REWRITE_TAC[pardir; parallel] THEN + REWRITE_TAC[PARDIR_EQUIV] THEN REWRITE_TAC[pardir; desargues_parallel] THEN MESON_TAC[homol; direction_tybij]);; let EQ_HOMOP = prove - (`!p p'. p = p' <=> parallel (homop p) (homop p')`, + (`!p p'. p = p' <=> desargues_parallel (homop p) (homop p')`, REWRITE_TAC[homop_def; GSYM EQ_HOMOL] THEN MESON_TAC[point_tybij]);; @@ -220,8 +251,8 @@ let EQ_HOMOP = prove (* ------------------------------------------------------------------------- *) let PARALLEL_PROJL_HOMOL = prove - (`!x. parallel x (homol(projl x))`, - GEN_TAC THEN REWRITE_TAC[parallel] THEN ASM_CASES_TAC `x:real^3 = vec 0` THEN + (`!x. desargues_parallel x (homol(projl x))`, + GEN_TAC THEN REWRITE_TAC[desargues_parallel] THEN ASM_CASES_TAC `x:real^3 = vec 0` THEN ASM_REWRITE_TAC[CROSS_0] THEN MP_TAC(ISPEC `projl x` homol) THEN DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN GEN_REWRITE_TAC "100/desargues.ml:(LAND_CONV o ONCE_DEPTH_CONV)" (LAND_CONV o ONCE_DEPTH_CONV) [projl] THEN @@ -232,14 +263,14 @@ let PARALLEL_PROJL_HOMOL = prove ASM_MESON_TAC[direction_tybij]);; let PARALLEL_PROJP_HOMOP = prove - (`!x. parallel x (homop(projp x))`, + (`!x. desargues_parallel x (homop(projp x))`, REWRITE_TAC[homop_def; projp; REWRITE_RULE[] point_tybij] THEN REWRITE_TAC[PARALLEL_PROJL_HOMOL]);; let PARALLEL_PROJP_HOMOP_EXPLICIT = prove (`!x. ~(x = vec 0) ==> ?a. ~(a = &0) /\ homop(projp x) = a % x`, MP_TAC PARALLEL_PROJP_HOMOP THEN MATCH_MP_TAC MONO_FORALL THEN - REWRITE_TAC[parallel; CROSS_EQ_0; COLLINEAR_LEMMA] THEN + REWRITE_TAC[desargues_parallel; CROSS_EQ_0; COLLINEAR_LEMMA] THEN GEN_TAC THEN ASM_CASES_TAC `x:real^3 = vec 0` THEN ASM_REWRITE_TAC[homop] THEN MATCH_MP_TAC MONO_EXISTS THEN X_GEN_TAC `c:real` THEN ASM_CASES_TAC `c = &0` THEN @@ -289,7 +320,7 @@ let COLLINEAR_BRACKET = prove ASM_CASES_TAC `p1:point = p2` THENL [ASM_REWRITE_TAC[INSERT_AC; COLLINEAR_PAIR]; ALL_TAC] THEN POP_ASSUM MP_TAC THEN - REWRITE_TAC[parallel; COLLINEAR_TRIPLE; bracket; EQ_HOMOP; ON_HOMOL] THEN + REWRITE_TAC[desargues_parallel; COLLINEAR_TRIPLE; bracket; EQ_HOMOP; ON_HOMOL] THEN REPEAT STRIP_TAC THEN EXISTS_TAC `mk_line((||) (mk_dir(homop p1 cross homop p2)))` THEN MATCH_MP_TAC lemma THEN EXISTS_TAC `homop p1 cross homop p2` THEN @@ -297,7 +328,7 @@ let COLLINEAR_BRACKET = prove REWRITE_TAC[orthogonal] THEN ONCE_REWRITE_TAC[DOT_SYM] THEN ONCE_REWRITE_TAC[CROSS_TRIPLE] THEN ONCE_REWRITE_TAC[DOT_SYM] THEN ASM_REWRITE_TAC[DOT_CROSS_DET] THEN - REWRITE_TAC[GSYM projl; GSYM parallel; PARALLEL_PROJL_HOMOL]]);; + REWRITE_TAC[GSYM projl; GSYM desargues_parallel; PARALLEL_PROJL_HOMOL]]);; (* ------------------------------------------------------------------------- *) (* Rather crude shuffling of bracket triple into canonical order. *) @@ -397,3 +428,4 @@ let DESARGUES_DIRECT = prove CONJ_TAC THENL [POP_ASSUM MP_TAC THEN CONV_TAC "100/desargues.ml:REAL_RING" REAL_RING; ALL_TAC] THEN FIRST_X_ASSUM(MP_TAC o CONJUNCT1) THEN REWRITE_TAC[bracket; DET_3; VECTOR_3] THEN CONV_TAC "100/desargues.ml:REAL_RING" REAL_RING);; +Pb_printer.clear_file_tags();; diff --git a/100/descartes.ml b/100/descartes.ml index 625c5b64..5308b424 100644 --- a/100/descartes.ml +++ b/100/descartes.ml @@ -2,7 +2,37 @@ (* Rob Arthan's "Descartes's Rule of Signs by an Easy Induction". *) (* ========================================================================= *) -needs "Multivariate/realanalysis.ml";; +set_jrh_lexer;; +Pb_printer.set_file_tags ["Top100"; "descartes.ml"];; + +open Lib;; +open Fusion;; +open Parser;; +open Equal;; +open Bool;; +open Drule;; +open Tactics;; +open Simp;; +open Theorems;; +open Class;; +open Meson;; +open Pair;; +open Nums;; +open Arith;; +open Wf;; +open Calc_num;; +open Realax;; +open Calc_int;; +open Realarith;; +open Reals;; +open Calc_rat;; +open Ints;; +open Sets;; +open Iterate;; +open Wo;; + +open Realanalysis;; + (* ------------------------------------------------------------------------- *) (* A couple of handy lemmas. *) @@ -832,3 +862,4 @@ let DESCARTES_RULE_OF_SIGNS = prove REPEAT STRIP_TAC THEN UNDISCH_TAC `~(sum (0..m) (\j. b j * r pow j) = &0)` THEN ASM_SIMP_TAC[] THEN REWRITE_TAC[REAL_MUL_LZERO; SUM_0]);; +Pb_printer.clear_file_tags();; diff --git a/100/dirichlet.ml b/100/dirichlet.ml index 36bfffae..e0bf22f3 100644 --- a/100/dirichlet.ml +++ b/100/dirichlet.ml @@ -2,12 +2,51 @@ (* Dirichlet's theorem. *) (* ========================================================================= *) -needs "Library/products.ml";; -needs "Library/agm.ml";; -needs "Multivariate/transcendentals.ml";; -needs "Library/pocklington.ml";; -needs "Library/multiplicative.ml";; -needs "Examples/mangoldt.ml";; + +set_jrh_lexer;; +Pb_printer.set_file_tags ["Top100"; "dirichlet.ml"];; + +open Lib;; +open Fusion;; +open Parser;; +open Equal;; +open Bool;; +open Drule;; +open Tactics;; +open Simp;; +open Theorems;; +open Class;; +open Trivia;; +open Meson;; +open Pair;; +open Nums;; +open Arith;; +open Calc_num;; +open Realax;; +open Calc_int;; +open Realarith;; +open Reals;; +open Calc_rat;; +open Ints;; +open Sets;; +open Iterate;; +open Wo;; +open Products;; +open Floor;; +open Misc;; + +open Metric;; +open Vectors;; +open Topology;; +open Complexes;; +open Canal;; +open Transcendentals;; + +open Pocklington;; +open Prime;; +open Mangoldt;; +open Agm;; +open Multiplicative;; prioritize_real();; prioritize_complex();; @@ -2080,3 +2119,4 @@ let DIRICHLET = prove REPLICATE_TAC 4 AP_TERM_TAC THEN AP_THM_TAC THEN AP_TERM_TAC THEN REWRITE_TAC[EXTENSION; IN_ELIM_THM; IN_NUMSEG] THEN GEN_TAC THEN EQ_TAC THEN ASM_SIMP_TAC[] THEN ASM_ARITH_TAC);; +Pb_printer.clear_file_tags();; diff --git a/100/div3.ml b/100/div3.ml index 2af46d26..7bc57bb2 100644 --- a/100/div3.ml +++ b/100/div3.ml @@ -2,8 +2,20 @@ (* #85: divisibility by 3 rule *) (* ========================================================================= *) -needs "Library/prime.ml";; -needs "Library/pocklington.ml";; +set_jrh_lexer;; +Pb_printer.set_file_tags ["Top100"; "div3.ml"];; + +open Parser;; +open Equal;; +open Tactics;; +open Simp;; +open Nums;; +open Arith;; +open Calc_num;; +open Ints;; +open Iterate;; + +open Pocklington;; let EXP_10_CONG_3 = prove (`!n. (10 EXP n == 1) (mod 3)`, @@ -25,3 +37,4 @@ let DIVISIBILITY_BY_3 = prove (`3 divides (nsum(0..n) (\i. 10 EXP i * d(i))) <=> 3 divides (nsum(0..n) (\i. d i))`, MATCH_MP_TAC CONG_DIVIDES THEN REWRITE_TAC[SUM_CONG_3]);; +Pb_printer.clear_file_tags();; diff --git a/100/divharmonic.ml b/100/divharmonic.ml index 3b67e346..53b4afe5 100644 --- a/100/divharmonic.ml +++ b/100/divharmonic.ml @@ -2,6 +2,28 @@ (* Divergence of harmonic series. *) (* ========================================================================= *) +set_jrh_lexer;; +Pb_printer.set_file_tags ["Top100"; "divharmonic.ml"];; + +open Lib;; +open Parser;; +open Equal;; +open Bool;; +open Drule;; +open Tactics;; +open Simp;; +open Nums;; +open Arith;; +open Calc_num;; +open Realax;; +open Reals;; +open Calc_rat;; +open Ints;; +open Iterate;; + +open Analysis;; +open Transc;; + prioritize_real();; let HARMONIC_DIVERGES = prove @@ -31,7 +53,6 @@ let HARMONIC_DIVERGES = prove (* Formulation in terms of limits. *) (* ------------------------------------------------------------------------- *) -needs "Library/analysis.ml";; let HARMONIC_DIVERGES' = prove (`~(convergent (\n. sum(1..n) (\i. &1 / &i)))`, @@ -67,7 +88,6 @@ let HARMONIC_LEMMA = prove (* Germ of an alternative proof. *) (* ------------------------------------------------------------------------- *) -needs "Library/transc.ml";; let LOG_BOUND = prove (`&0 < x /\ x < &1 ==> ln(&1 + x) >= x / &2`, @@ -76,3 +96,4 @@ let LOG_BOUND = prove ASM_SIMP_TAC[LN_MONO_LE; REAL_EXP_POS_LT; REAL_LT_ADD; REAL_LT_01] THEN MP_TAC(SPEC `x / &2` REAL_EXP_BOUND_LEMMA) THEN POP_ASSUM_LIST(MP_TAC o end_itlist CONJ) THEN ARITH_TAC);; +Pb_printer.clear_file_tags();; diff --git a/100/e_is_transcendental.ml b/100/e_is_transcendental.ml index 333785f9..8a20b1e7 100644 --- a/100/e_is_transcendental.ml +++ b/100/e_is_transcendental.ml @@ -22,21 +22,53 @@ * jesse.bingham@gmail.com *) +set_jrh_lexer;; +Pb_printer.set_file_tags ["Top100"; "e_is_transcendental.ml"];; + +open Lib;; +open Fusion;; +open Basics;; +open Parser;; +open Equal;; +open Bool;; +open Drule;; +open Tactics;; +open Simp;; +open Theorems;; +open Class;; +open Trivia;; +open Canon;; +open Meson;; +open Pair;; +open Nums;; +open Recursion;; +open Arith;; +open Ind_types;; +open Lists;; +open Realax;; +open Calc_int;; +open Realarith;; +open Reals;; +open Calc_rat;; +open Ints;; +open Sets;; +open Iterate;; + +open Floor;; +open Binomial;; + (* this is needed since the sum from the HOL core (iter.ml, i think) * which is used below, gets overwritten when Library/analysis.ml is loaded. + NOTE(smloos): this has been moved to analysis.ml. *) -let OLD_SUM = sum;; - -(* required stuff from HOL Light library... *) -needs "Library/binomial.ml";; -needs "Library/analysis.ml";; -needs "Library/transc.ml";; -needs "Library/prime.ml";; -needs "Library/iter.ml";; -needs "Library/integer.ml";; -needs "Library/floor.ml";; -(* get def of transcendental from Harrison's Liouville proof *) -needs "100/liouville.ml";; +(* let OLD_SUM = sum;; *) + +open Analysis;; +open Transc;; +open Prime;; +open Integer;; +open Poly;; +open Liouville;; prioritize_real();; @@ -2894,3 +2926,4 @@ let TRANSCENDENTAL_E = prove( end;; Finale.TRANSCENDENTAL_E;; +Pb_printer.clear_file_tags();; diff --git a/100/euler.ml b/100/euler.ml index 19a33d42..91b9f006 100644 --- a/100/euler.ml +++ b/100/euler.ml @@ -2,7 +2,38 @@ (* Euler's partition theorem and other elementary partition theorems. *) (* ========================================================================= *) -loadt "Library/binary.ml";; +set_jrh_lexer;; +Pb_printer.set_file_tags ["Top100"; "euler.ml"];; + +open Lib;; +open Fusion;; +open Basics;; +open Printer;; +open Parser;; +open Equal;; +open Bool;; +open Drule;; +open Tactics;; +open Simp;; +open Theorems;; +open Class;; +open Trivia;; +open Meson;; +open Pair;; +open Nums;; +open Arith;; +open Calc_num;; +open Ind_types;; +open Realax;; +open Ints;; +open Sets;; +open Iterate;; +open Define;; + +open Binary;; + +prioritize_num();; + (* ------------------------------------------------------------------------- *) (* Some lemmas. *) @@ -29,16 +60,16 @@ let CARD_EQ_LEMMA = prove (* Breaking a number up into 2^something * odd_number. *) (* ------------------------------------------------------------------------- *) -let index = define - `index n = if n = 0 then 0 else if ODD n then 0 else SUC(index(n DIV 2))`;; +let euler_index = define + `euler_index n = if n = 0 then 0 else if ODD n then 0 else SUC(euler_index(n DIV 2))`;; let oddpart = define `oddpart n = if n = 0 then 0 else if ODD n then n else oddpart(n DIV 2)`;; let INDEX_ODDPART_WORK = prove - (`!n. n = 2 EXP (index n) * oddpart n /\ (ODD(oddpart n) <=> ~(n = 0))`, + (`!n. n = 2 EXP (euler_index n) * oddpart n /\ (ODD(oddpart n) <=> ~(n = 0))`, MATCH_MP_TAC num_WF THEN GEN_TAC THEN DISCH_TAC THEN - ONCE_REWRITE_TAC[index; oddpart] THEN + ONCE_REWRITE_TAC[euler_index; oddpart] THEN ASM_CASES_TAC `n = 0` THEN ASM_REWRITE_TAC[ARITH] THEN COND_CASES_TAC THEN ASM_REWRITE_TAC[ARITH; MULT_CLAUSES] THEN FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [NOT_ODD]) THEN @@ -47,7 +78,7 @@ let INDEX_ODDPART_WORK = prove ASM_MESON_TAC[ARITH_RULE `~(n = 0) /\ n = 2 * m ==> m < n /\ ~(m = 0)`]);; let INDEX_ODDPART_DECOMPOSITION = prove - (`!n. n = 2 EXP (index n) * oddpart n`, + (`!n. n = 2 EXP (euler_index n) * oddpart n`, MESON_TAC[INDEX_ODDPART_WORK]);; let ODD_ODDPART = prove @@ -69,9 +100,9 @@ let INDEX_ODDPART_UNIQUE = prove ARITH_TAC);; let INDEX_ODDPART = prove - (`!i m. ODD m ==> index(2 EXP i * m) = i /\ oddpart(2 EXP i * m) = m`, + (`!i m. ODD m ==> euler_index(2 EXP i * m) = i /\ oddpart(2 EXP i * m) = m`, REPEAT GEN_TAC THEN STRIP_TAC THEN - MP_TAC(SPECL [`i:num`; `m:num`; `index(2 EXP i * m)`; `oddpart(2 EXP i * m)`] + MP_TAC(SPECL [`i:num`; `m:num`; `euler_index(2 EXP i * m)`; `oddpart(2 EXP i * m)`] INDEX_ODDPART_UNIQUE) THEN REWRITE_TAC[GSYM INDEX_ODDPART_DECOMPOSITION; ODD_ODDPART] THEN ASM_REWRITE_TAC[MULT_EQ_0; EXP_EQ_0; ARITH] THEN ASM_MESON_TAC[ODD]);; @@ -157,7 +188,7 @@ let odd_of_distinct = new_definition \i. if ODD i then nsum {j | p(2 EXP j * i) = 1} (\j. 2 EXP j) else 0`;; let distinct_of_odd = new_definition - `distinct_of_odd p = \i. if (index i) IN bitset (p(oddpart i)) then 1 else 0`;; + `distinct_of_odd p = \i. if (euler_index i) IN bitset (p(oddpart i)) then 1 else 0`;; (* ------------------------------------------------------------------------- *) (* The critical properties. *) @@ -206,8 +237,8 @@ let SUPPORT_DISTINCT_OF_ODD = prove GEN_TAC THEN STRIP_TAC THEN X_GEN_TAC `i:num` THEN REPEAT STRIP_TAC THENL [REWRITE_TAC[ARITH_RULE `1 <= i <=> ~(i = 0)`] THEN DISCH_THEN SUBST_ALL_TAC THEN - UNDISCH_TAC `index 0 IN bitset (p (oddpart 0))` THEN - REWRITE_TAC[index; oddpart; ARITH] THEN + UNDISCH_TAC `euler_index 0 IN bitset (p (oddpart 0))` THEN + REWRITE_TAC[euler_index; oddpart; ARITH] THEN UNDISCH_THEN `!i. ~(p i = 0) ==> ODD i` (MP_TAC o SPEC `0`) THEN SIMP_TAC[ARITH; BITSET_0; NOT_IN_EMPTY]; ALL_TAC] THEN @@ -276,8 +307,8 @@ let NSUM_DISTINCT_OF_ODD = prove ALL_TAC] THEN SUBGOAL_THEN `{x | x IN 1 .. n /\ - ~((if index x IN bitset (p (oddpart x)) then 1 else 0) * x = 0)} = - {i | i IN 1..n /\ (index i) IN bitset (p(oddpart i))}` + ~((if euler_index x IN bitset (p (oddpart x)) then 1 else 0) * x = 0)} = + {i | i IN 1..n /\ (euler_index i) IN bitset (p(oddpart i))}` SUBST1_TAC THENL [REWRITE_TAC[EXTENSION; IN_ELIM_THM; MULT_EQ_0] THEN REWRITE_TAC[IN_NUMSEG; ARITH_RULE `(if p then 1 else 0) = 0 <=> ~p`] THEN @@ -299,7 +330,7 @@ let NSUM_DISTINCT_OF_ODD = prove [ASM_MESON_TAC[BITSET_0; NOT_IN_EMPTY]; ALL_TAC] THEN CONJ_TAC THENL [X_GEN_TAC `m:num` THEN STRIP_TAC THEN CONJ_TAC THENL - [MAP_EVERY EXISTS_TAC [`oddpart m`; `index m`] THEN + [MAP_EVERY EXISTS_TAC [`oddpart m`; `euler_index m`] THEN ASM_REWRITE_TAC[GSYM INDEX_ODDPART_DECOMPOSITION] THEN ASM_MESON_TAC[ODDPART_LE; LE_TRANS; ARITH_RULE `1 <= x <=> ~(x = 0)`; ODD_ODDPART; ODD]; @@ -385,3 +416,4 @@ let EULER_PARTITION_THEOREM = prove [MATCH_MP_TAC DISTINCT_OF_ODD_OF_DISTINCT; MATCH_MP_TAC ODD_OF_DISTINCT_OF_ODD] THEN ASM_REWRITE_TAC[]);; +Pb_printer.clear_file_tags();; diff --git a/100/feuerbach.ml b/100/feuerbach.ml index 6b1dee58..34f5bed5 100644 --- a/100/feuerbach.ml +++ b/100/feuerbach.ml @@ -2,7 +2,68 @@ (* Feuerbach's theorem. *) (* ========================================================================= *) -needs "Multivariate/convex.ml";; +set_jrh_lexer;; +open System;; +open Lib;; +open Fusion;; +open Basics;; +open Nets;; +open Printer;; +open Preterm;; +open Parser;; +open Equal;; +open Bool;; +open Drule;; +open Log;; +open Import_proofs;; +open Tactics;; +open Itab;; +open Replay;; +open Simp;; +open Embryo_extra;; +open Theorems;; +open Ind_defs;; +open Class;; +open Trivia;; +open Canon;; +open Meson;; +open Metis;; +open Quot;; +open Impconv;; +open Pair;; +open Nums;; +open Recursion;; +open Arith;; +open Wf;; +open Calc_num;; +open Normalizer;; +open Grobner;; +open Ind_types;; +open Lists;; +open Realax;; +open Calc_int;; +open Realarith;; +open Reals;; +open Calc_rat;; +open Ints;; +open Sets;; +open Iterate;; +open Cart;; +open Define;; +open Help;; +open Wo;; +open Binary;; +open Card;; +open Permutations;; +open Products;; +open Floor;; +open Misc;; +open Iter;; + +open Vectors;; +open Determinants;; +open Topology;; +open Convex;; (* ------------------------------------------------------------------------- *) (* Algebraic condition for two circles to be tangent to each other. *) diff --git a/100/four_squares.ml b/100/four_squares.ml index 8e4f33c3..64a99d2f 100644 --- a/100/four_squares.ml +++ b/100/four_squares.ml @@ -2,8 +2,36 @@ (* Theorems about representations as sums of 2 and 4 squares. *) (* ========================================================================= *) -needs "Library/prime.ml";; -needs "Library/analysis.ml";; (*** only for REAL_ARCH_LEAST! ***) +set_jrh_lexer;; +Pb_printer.set_file_tags ["Top100"; "four_squares.ml"];; + +open Lib;; +open Fusion;; +open Basics;; +open Parser;; +open Equal;; +open Bool;; +open Drule;; +open Tactics;; +open Simp;; +open Theorems;; +open Class;; +open Meson;; +open Pair;; +open Arith;; +open Calc_num;; +open Realax;; +open Calc_int;; +open Realarith;; +open Reals;; +open Calc_rat;; +open Ints;; +open Sets;; + +open Prime;; +open Analysis;; + +(*** "Library/analysis.ml" only for REAL_ARCH_LEAST! ***) prioritize_num();; @@ -946,3 +974,4 @@ let LAGRANGE_INT = prove STRIP_TAC THEN ASM_SIMP_TAC[INT_LE_SQUARE; INT_LE_ADD; INT_POW_2]]);; prioritize_num();; +Pb_printer.clear_file_tags();; diff --git a/100/fourier.ml b/100/fourier.ml index ba45b4ff..e4c62803 100644 --- a/100/fourier.ml +++ b/100/fourier.ml @@ -2,7 +2,52 @@ (* Square integrable functions R->R and basics of Fourier series. *) (* ========================================================================= *) -needs "Multivariate/lpspaces.ml";; +set_jrh_lexer;; +Pb_printer.set_file_tags ["Top100"; "fourier.ml"];; + +open Lib;; +open Fusion;; +open Printer;; +open Parser;; +open Equal;; +open Bool;; +open Drule;; +open Tactics;; +open Simp;; +open Theorems;; +open Ind_defs;; +open Class;; +open Trivia;; +open Meson;; +open Pair;; +open Nums;; +open Arith;; +open Calc_num;; +open Lists;; +open Realax;; +open Calc_int;; +open Realarith;; +open Reals;; +open Calc_rat;; +open Ints;; +open Sets;; +open Iterate;; +open Wo;; +open Card;; +open Floor;; +open Misc;; + +open Metric;; +open Vectors;; +open Determinants;; +open Topology;; +open Integration;; +open Complexes;; +open Canal;; +open Transcendentals;; +open Realanalysis;; + +open Lpspaces;; (* ------------------------------------------------------------------------- *) (* Somewhat general lemmas, but perhaps not enough to be installed. *) @@ -4633,3 +4678,4 @@ let FOURIER_FEJER_CESARO_SUMMABLE_SIMPLE = prove REWRITE_TAC[GSYM REAL_CONTINUOUS_ATREAL] THEN ASM_MESON_TAC[REAL_CONTINUOUS_ON_EQ_REAL_CONTINUOUS_AT; REAL_OPEN_UNIV; IN_UNIV]]);; +Pb_printer.clear_file_tags();; diff --git a/100/friendship.ml b/100/friendship.ml index aded29e9..ca802b38 100644 --- a/100/friendship.ml +++ b/100/friendship.ml @@ -5,8 +5,66 @@ (* MathOlymp.com, 2001. Apparently due to J. Q. Longyear and T. D. Parsons. *) (* ========================================================================= *) -needs "Library/prime.ml";; -needs "Library/pocklington.ml";; +set_jrh_lexer;; +open System;; +open Lib;; +open Fusion;; +open Basics;; +open Nets;; +open Printer;; +open Preterm;; +open Parser;; +open Equal;; +open Bool;; +open Drule;; +open Log;; +open Import_proofs;; +open Tactics;; +open Itab;; +open Replay;; +open Simp;; +open Embryo_extra;; +open Theorems;; +open Ind_defs;; +open Class;; +open Trivia;; +open Canon;; +open Meson;; +open Metis;; +open Quot;; +open Impconv;; +open Pair;; +open Nums;; +open Recursion;; +open Arith;; +open Wf;; +open Calc_num;; +open Normalizer;; +open Grobner;; +open Ind_types;; +open Lists;; +open Realax;; +open Calc_int;; +open Realarith;; +open Reals;; +open Calc_rat;; +open Ints;; +open Sets;; +open Iterate;; +open Cart;; +open Define;; +open Help;; +open Wo;; +open Binary;; +open Card;; +open Permutations;; +open Products;; +open Floor;; +open Misc;; +open Iter;; + +open Prime;; +open Pocklington;; (* ------------------------------------------------------------------------- *) (* Useful inductive breakdown principle ending at gcd. *) @@ -139,8 +197,8 @@ let ELEMENTS_PAIR_UP = prove let cycle = new_definition `cycle r k x <=> (!i. r (x i) (x(i + 1))) /\ (!i. x(i + k) = x(i))`;; -let path = new_definition - `path r k x <=> (!i. i < k ==> r (x i) (x(i + 1))) /\ +let friendship_path = new_definition + `friendship_path r k x <=> (!i. i < k ==> r (x i) (x(i + 1))) /\ (!i. k < i ==> x(i) = @x. T)`;; (* ------------------------------------------------------------------------- *) @@ -158,33 +216,33 @@ let CYCLE_MOD = prove MESON_TAC[CYCLE_OFFSET; DIVISION]);; let PATHS_MONO = prove - (`(!x y. r x y ==> s x y) ==> {x | path r k x} SUBSET {x | path s k x}`, - REWRITE_TAC[path; IN_ELIM_THM; SUBSET] THEN MESON_TAC[]);; + (`(!x y. r x y ==> s x y) ==> {x | friendship_path r k x} SUBSET {x | friendship_path s k x}`, + REWRITE_TAC[friendship_path; IN_ELIM_THM; SUBSET] THEN MESON_TAC[]);; let HAS_SIZE_PATHS = prove (`!N m r k. (:A) HAS_SIZE N /\ (!x. {y | r x y} HAS_SIZE m) - ==> {x:num->A | path r k x} HAS_SIZE (N * m EXP k)`, + ==> {x:num->A | friendship_path r k x} HAS_SIZE (N * m EXP k)`, REWRITE_TAC[RIGHT_FORALL_IMP_THM] THEN REPEAT GEN_TAC THEN STRIP_TAC THEN INDUCT_TAC THEN REWRITE_TAC[EXP; MULT_CLAUSES] THENL - [SUBGOAL_THEN `{x:num->A | path r 0 x} = + [SUBGOAL_THEN `{x:num->A | friendship_path r 0 x} = IMAGE (\a i. if i = 0 then a else @x. T) (:A)` SUBST1_TAC THENL - [REWRITE_TAC[EXTENSION; IN_ELIM_THM; IN_IMAGE; IN_UNIV; path; LT] THEN + [REWRITE_TAC[EXTENSION; IN_ELIM_THM; IN_IMAGE; IN_UNIV; friendship_path; LT] THEN REWRITE_TAC[FUN_EQ_THM; LT_NZ] THEN MESON_TAC[]; ALL_TAC] THEN MATCH_MP_TAC HAS_SIZE_IMAGE_INJ THEN ASM_REWRITE_TAC[IN_UNIV] THEN REWRITE_TAC[FUN_EQ_THM] THEN MESON_TAC[]; ALL_TAC] THEN SUBGOAL_THEN - `{x:num->A | path r (SUC k) x} = + `{x:num->A | friendship_path r (SUC k) x} = IMAGE (\(x,a) i. if i = SUC k then a else x i) - {x,a | x IN {x | path r k x} /\ a IN {u | r (x k) u}}` + {x,a | x IN {x | friendship_path r k x} /\ a IN {u | r (x k) u}}` SUBST1_TAC THENL [REWRITE_TAC[EXTENSION; IN_ELIM_THM; IN_IMAGE; EXISTS_PAIR_THM] THEN X_GEN_TAC `x:num->A` THEN REWRITE_TAC[PAIR_EQ] THEN ONCE_REWRITE_TAC[TAUT `(a /\ b) /\ c /\ d <=> c /\ d /\ a /\ b`] THEN REWRITE_TAC[RIGHT_EXISTS_AND_THM; UNWIND_THM1] THEN - REWRITE_TAC[FUN_EQ_THM; path; LT] THEN EQ_TAC THENL + REWRITE_TAC[FUN_EQ_THM; friendship_path; LT] THEN EQ_TAC THENL [STRIP_TAC THEN EXISTS_TAC `\i. if i = SUC k then @x. T else x(i):A` THEN EXISTS_TAC `x(SUC k):A` THEN SIMP_TAC[] THEN CONJ_TAC THENL [MESON_TAC[]; ALL_TAC] THEN @@ -202,7 +260,7 @@ let HAS_SIZE_PATHS = prove ONCE_REWRITE_TAC[ARITH_RULE `N * m * m EXP k = (N * m EXP k) * m`] THEN MATCH_MP_TAC HAS_SIZE_IMAGE_INJ THEN CONJ_TAC THENL [REWRITE_TAC[FORALL_PAIR_THM; IN_ELIM_PAIR_THM; IN_ELIM_THM] THEN - REWRITE_TAC[FUN_EQ_THM; path; PAIR_EQ] THEN REPEAT GEN_TAC THEN + REWRITE_TAC[FUN_EQ_THM; friendship_path; PAIR_EQ] THEN REPEAT GEN_TAC THEN STRIP_TAC THEN CONJ_TAC THENL [ALL_TAC; ASM_MESON_TAC[]] THEN X_GEN_TAC `i:num` THEN ASM_CASES_TAC `i = SUC k` THEN ASM_MESON_TAC[ARITH_RULE `k < SUC k`]; @@ -210,9 +268,9 @@ let HAS_SIZE_PATHS = prove ASM_SIMP_TAC[HAS_SIZE_PRODUCT_DEPENDENT]);; let FINITE_PATHS = prove - (`!r k. FINITE(:A) ==> FINITE {x:num->A | path r k x}`, + (`!r k. FINITE(:A) ==> FINITE {x:num->A | friendship_path r k x}`, REPEAT STRIP_TAC THEN MATCH_MP_TAC FINITE_SUBSET THEN - EXISTS_TAC `{x:num->A | path (\a b. T) k x}` THEN SIMP_TAC[PATHS_MONO] THEN + EXISTS_TAC `{x:num->A | friendship_path (\a b. T) k x}` THEN SIMP_TAC[PATHS_MONO] THEN MP_TAC(ISPECL [`CARD(:A)`; `CARD(:A)`; `\a:A b:A. T`; `k:num`] HAS_SIZE_PATHS) THEN ANTS_TAC THEN ASM_SIMP_TAC[HAS_SIZE; SET_RULE `{y | T} = (:A)`]);; @@ -220,11 +278,11 @@ let FINITE_PATHS = prove let HAS_SIZE_CYCLES = prove (`!r k. FINITE(:A) /\ ~(k = 0) ==> {x:num->A | cycle r k x} HAS_SIZE - CARD{x:num->A | path r k x /\ x(k) = x(0)}`, + CARD{x:num->A | friendship_path r k x /\ x(k) = x(0)}`, REPEAT STRIP_TAC THEN SUBGOAL_THEN `{x:num->A | cycle r k x} = - IMAGE (\x i. x(i MOD k)) {x | path r k x /\ x(k) = x(0)}` + IMAGE (\x i. x(i MOD k)) {x | friendship_path r k x /\ x(k) = x(0)}` SUBST1_TAC THENL [REWRITE_TAC[EXTENSION; IN_IMAGE; IN_ELIM_THM] THEN X_GEN_TAC `x:num->A` THEN EQ_TAC THENL @@ -233,7 +291,7 @@ let HAS_SIZE_CYCLES = prove REPEAT CONJ_TAC THENL [ASM_SIMP_TAC[FUN_EQ_THM; LT_IMP_LE; DIVISION] THEN ASM_MESON_TAC[CYCLE_MOD]; - SIMP_TAC[path; LT_IMP_LE] THEN REWRITE_TAC[GSYM NOT_LT] THEN + SIMP_TAC[friendship_path; LT_IMP_LE] THEN REWRITE_TAC[GSYM NOT_LT] THEN SIMP_TAC[ARITH_RULE `i < k ==> ~(k < i + 1)`] THEN ASM_MESON_TAC[cycle]; REWRITE_TAC[LE_0; LE_REFL] THEN ASM_MESON_TAC[cycle; ADD_CLAUSES]]; @@ -244,7 +302,7 @@ let HAS_SIZE_CYCLES = prove AP_TERM_TAC THEN MATCH_MP_TAC MOD_EQ THEN EXISTS_TAC `1` THEN REWRITE_TAC[MULT_CLAUSES]] THEN SUBGOAL_THEN `y((i + 1) MOD k):A = y(i MOD k + 1)` SUBST1_TAC THENL - [ALL_TAC; ASM_MESON_TAC[path; DIVISION]] THEN + [ALL_TAC; ASM_MESON_TAC[friendship_path; DIVISION]] THEN SUBGOAL_THEN `(i + 1) MOD k = (i MOD k + 1) MOD k` SUBST1_TAC THENL [MATCH_MP_TAC MOD_EQ THEN EXISTS_TAC `i DIV k` THEN REWRITE_TAC[ARITH_RULE `i + 1 = (m + 1) + ik <=> i = ik + m`] THEN @@ -260,10 +318,10 @@ let HAS_SIZE_CYCLES = prove MATCH_MP_TAC HAS_SIZE_IMAGE_INJ THEN CONJ_TAC THENL [ALL_TAC; REWRITE_TAC[HAS_SIZE] THEN MATCH_MP_TAC FINITE_SUBSET THEN - EXISTS_TAC `{x:num->A | path r k x}` THEN + EXISTS_TAC `{x:num->A | friendship_path r k x}` THEN ASM_SIMP_TAC[FINITE_PATHS] THEN SET_TAC[]] THEN MAP_EVERY X_GEN_TAC [`x:num->A`; `y:num->A`] THEN SIMP_TAC[IN_ELIM_THM] THEN - REWRITE_TAC[path; FUN_EQ_THM] THEN STRIP_TAC THEN X_GEN_TAC `i:num` THEN + REWRITE_TAC[friendship_path; FUN_EQ_THM] THEN STRIP_TAC THEN X_GEN_TAC `i:num` THEN REPEAT_TCL DISJ_CASES_THEN ASSUME_TAC (SPECL [`i:num`; `k:num`] LT_CASES) THENL [ASM_MESON_TAC[MOD_LT]; ASM_MESON_TAC[]; ASM_REWRITE_TAC[]] THEN @@ -279,22 +337,22 @@ let CARD_PATHCYCLES_STEP = prove (!x:A. {y | r x y} HAS_SIZE m) /\ (!x y. r x y ==> r y x) /\ (!x y. ~(x = y) ==> ?!z. r x z /\ r z y) - ==> {x | path r (k + 2) x /\ x(k + 2) = x(0)} HAS_SIZE - (m * CARD {x | path r k x /\ x(k) = x(0)} + - CARD {x | path r (k) x /\ ~(x(k) = x(0))})`, + ==> {x | friendship_path r (k + 2) x /\ x(k + 2) = x(0)} HAS_SIZE + (m * CARD {x | friendship_path r k x /\ x(k) = x(0)} + + CARD {x | friendship_path r (k) x /\ ~(x(k) = x(0))})`, REPEAT STRIP_TAC THEN REWRITE_TAC[SET_RULE - `{x | path r (k + 2) x /\ x(k + 2) = x(0)} = - {x | path r (k + 2) x /\ x k = x 0 /\ x(k + 2) = x(0)} UNION - {x | path r (k + 2) x /\ ~(x k = x 0) /\ x(k + 2) = x(0)}`] THEN + `{x | friendship_path r (k + 2) x /\ x(k + 2) = x(0)} = + {x | friendship_path r (k + 2) x /\ x k = x 0 /\ x(k + 2) = x(0)} UNION + {x | friendship_path r (k + 2) x /\ ~(x k = x 0) /\ x(k + 2) = x(0)}`] THEN MATCH_MP_TAC HAS_SIZE_UNION THEN GEN_REWRITE_TAC "100/friendship.ml:I" I [CONJ_ASSOC] THEN CONJ_TAC THENL [ALL_TAC; SET_TAC[]] THEN CONJ_TAC THENL [SUBGOAL_THEN - `{x:num->A | path r (k + 2) x /\ x k = x 0 /\ x (k + 2) = x 0} = + `{x:num->A | friendship_path r (k + 2) x /\ x k = x 0 /\ x (k + 2) = x 0} = IMAGE (\(x,a) i. if i = k + 1 then a else if i = k + 2 then x(0) else x(i)) - {x,a | x IN {x | path r k x /\ x(k) = x(0)} /\ + {x,a | x IN {x | friendship_path r k x /\ x(k) = x(0)} /\ a IN {u | r (x k) u}}` SUBST1_TAC THENL [ALL_TAC; @@ -309,7 +367,7 @@ let CARD_PATHCYCLES_STEP = prove DISCH_THEN(fun th -> MP_TAC th THEN MP_TAC(SPEC `0` th)) THEN REWRITE_TAC[ARITH_RULE `~(0 = k + 1) /\ ~(0 = k + 2)`] THEN DISCH_TAC THEN ASM_CASES_TAC `k:num < i` THENL - [ASM_MESON_TAC[path]; ALL_TAC] THEN + [ASM_MESON_TAC[friendship_path]; ALL_TAC] THEN DISCH_THEN(MP_TAC o SPEC `i:num`) THEN ASM_MESON_TAC[ARITH_RULE `k < k + 1 /\ k < k + 2`]; ALL_TAC] THEN @@ -317,7 +375,7 @@ let CARD_PATHCYCLES_STEP = prove MATCH_MP_TAC HAS_SIZE_PRODUCT_DEPENDENT THEN ASM_REWRITE_TAC[] THEN REWRITE_TAC[HAS_SIZE] THEN MATCH_MP_TAC FINITE_SUBSET THEN - EXISTS_TAC `{x:num->A | path r k x}` THEN CONJ_TAC THENL + EXISTS_TAC `{x:num->A | friendship_path r k x}` THEN CONJ_TAC THENL [ALL_TAC; SET_TAC[]] THEN ASM_MESON_TAC[HAS_SIZE; FINITE_PATHS]] THEN REWRITE_TAC[EXTENSION; IN_IMAGE] THEN @@ -329,17 +387,17 @@ let CARD_PATHCYCLES_STEP = prove EXISTS_TAC `(x:num->A) (k + 1)` THEN REWRITE_TAC[IN_ELIM_THM; LE_REFL; LE_0] THEN ASM_REWRITE_TAC[CONJ_ASSOC] THEN CONJ_TAC THENL - [ALL_TAC; ASM_MESON_TAC[path; ARITH_RULE `k < k + 2`]] THEN + [ALL_TAC; ASM_MESON_TAC[friendship_path; ARITH_RULE `k < k + 2`]] THEN CONJ_TAC THENL [ALL_TAC; - UNDISCH_TAC `path r (k + 2) (x:num->A)` THEN - SIMP_TAC[path; LT_IMP_LE; ARITH_RULE `i < k ==> i + 1 <= k`] THEN + UNDISCH_TAC `friendship_path r (k + 2) (x:num->A)` THEN + SIMP_TAC[friendship_path; LT_IMP_LE; ARITH_RULE `i < k ==> i + 1 <= k`] THEN SIMP_TAC[GSYM NOT_LT] THEN MESON_TAC[ARITH_RULE `i < k ==> i < k + 2`]] THEN X_GEN_TAC `i:num` THEN ASM_CASES_TAC `i = k + 1` THEN ASM_REWRITE_TAC[] THEN ASM_CASES_TAC `i = k + 2` THEN ASM_REWRITE_TAC[] THEN - FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [path]) THEN + FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [friendship_path]) THEN COND_CASES_TAC THEN ASM_REWRITE_TAC[] THEN DISCH_THEN(MP_TAC o SPEC `i:num` o CONJUNCT2) THEN ASM_REWRITE_TAC[ARITH_RULE @@ -356,7 +414,7 @@ let CARD_PATHCYCLES_STEP = prove CONJ_TAC THENL [ALL_TAC; REMOVE_THEN "*" (MP_TAC o SPEC `k:num`) THEN ASM_REWRITE_TAC[ARITH_RULE `~(k = k + 2) /\ ~(k = k + 1)`]] THEN - UNDISCH_TAC `path r k (z:num->A)` THEN ASM_REWRITE_TAC[path] THEN + UNDISCH_TAC `friendship_path r k (z:num->A)` THEN ASM_REWRITE_TAC[friendship_path] THEN SIMP_TAC[ARITH_RULE `k + 2 < i ==> k < i /\ ~(i = k + 1) /\ ~(i = k + 2)`] THEN STRIP_TAC THEN X_GEN_TAC `i:num` THEN DISCH_TAC THEN @@ -370,25 +428,25 @@ let CARD_PATHCYCLES_STEP = prove ==> i < k`]; ALL_TAC] THEN SUBGOAL_THEN - `{x:num->A | path r (k + 2) x /\ ~(x k = x 0) /\ x (k + 2) = x 0} = + `{x:num->A | friendship_path r (k + 2) x /\ ~(x k = x 0) /\ x (k + 2) = x 0} = IMAGE (\x i. if i = k + 1 then @z. r (x k) z /\ r z (x 0) else if i = k + 2 then x(0) else x(i)) - {x | path r k x /\ ~(x(k) = x(0))}` + {x | friendship_path r k x /\ ~(x(k) = x(0))}` SUBST1_TAC THENL [ALL_TAC; MATCH_MP_TAC HAS_SIZE_IMAGE_INJ THEN CONJ_TAC THENL [ALL_TAC; REWRITE_TAC[HAS_SIZE] THEN MATCH_MP_TAC FINITE_SUBSET THEN - EXISTS_TAC `{x:num->A | path r k x}` THEN CONJ_TAC THENL + EXISTS_TAC `{x:num->A | friendship_path r k x}` THEN CONJ_TAC THENL [ALL_TAC; SET_TAC[]] THEN ASM_MESON_TAC[HAS_SIZE; FINITE_PATHS]] THEN MAP_EVERY X_GEN_TAC [`x:num->A`; `y:num->A`] THEN REWRITE_TAC[IN_ELIM_THM] THEN STRIP_TAC THEN REWRITE_TAC[FUN_EQ_THM] THEN X_GEN_TAC `i:num` THEN ASM_CASES_TAC `k:num < i` THENL - [ASM_MESON_TAC[path]; ALL_TAC] THEN + [ASM_MESON_TAC[friendship_path]; ALL_TAC] THEN FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [FUN_EQ_THM]) THEN DISCH_THEN(MP_TAC o SPEC `i:num`) THEN ASM_MESON_TAC[ARITH_RULE `k < k + 1 /\ k < k + 2`]] THEN @@ -398,14 +456,14 @@ let CARD_PATHCYCLES_STEP = prove EXISTS_TAC `\i. if i <= k then x(i):A else @x. T` THEN ASM_REWRITE_TAC[LE_REFL; LE_0] THEN CONJ_TAC THENL [ALL_TAC; - UNDISCH_TAC `path r (k + 2) (x:num->A)` THEN - SIMP_TAC[path; LT_IMP_LE; ARITH_RULE `i < k ==> i + 1 <= k`] THEN + UNDISCH_TAC `friendship_path r (k + 2) (x:num->A)` THEN + SIMP_TAC[friendship_path; LT_IMP_LE; ARITH_RULE `i < k ==> i + 1 <= k`] THEN SIMP_TAC[GSYM NOT_LT] THEN MESON_TAC[ARITH_RULE `i < k ==> i < k + 2`]] THEN REWRITE_TAC[FUN_EQ_THM] THEN X_GEN_TAC `i:num` THEN ASM_CASES_TAC `i = k + 1` THEN ASM_REWRITE_TAC[] THENL [CONV_TAC "100/friendship.ml:SYM_CONV" SYM_CONV THEN MATCH_MP_TAC SELECT_UNIQUE THEN - UNDISCH_TAC `path r (k + 2) (x:num->A)` THEN REWRITE_TAC[path] THEN + UNDISCH_TAC `friendship_path r (k + 2) (x:num->A)` THEN REWRITE_TAC[friendship_path] THEN DISCH_THEN(MP_TAC o CONJUNCT1) THEN DISCH_THEN(fun th -> MP_TAC(SPEC `k:num` th) THEN MP_TAC(SPEC `k + 1` th)) THEN @@ -414,7 +472,7 @@ let CARD_PATHCYCLES_STEP = prove ALL_TAC] THEN ASM_CASES_TAC `i = k + 2` THEN ASM_REWRITE_TAC[] THEN COND_CASES_TAC THEN ASM_REWRITE_TAC[] THEN - UNDISCH_TAC `path r (k + 2) (x:num->A)` THEN REWRITE_TAC[path] THEN + UNDISCH_TAC `friendship_path r (k + 2) (x:num->A)` THEN REWRITE_TAC[friendship_path] THEN DISCH_THEN(MP_TAC o CONJUNCT2) THEN ASM_MESON_TAC[ARITH_RULE `~(i <= k) /\ ~(i = k + 1) /\ ~(i = k + 2) ==> k + 2 < i`]; @@ -423,7 +481,7 @@ let CARD_PATHCYCLES_STEP = prove ASM_REWRITE_TAC[ARITH_RULE `~(k + 2 = k + 1) /\ ~(0 = k + 1) /\ ~(0 = k + 2) /\ ~(k = k + 1) /\ ~(k = k + 2)`] THEN - REWRITE_TAC[path] THEN CONJ_TAC THEN X_GEN_TAC `i:num` THEN DISCH_TAC THENL + REWRITE_TAC[friendship_path] THEN CONJ_TAC THEN X_GEN_TAC `i:num` THEN DISCH_TAC THENL [REWRITE_TAC[ARITH_RULE `i + 1 = k + 2 <=> i = k + 1`] THEN ASM_CASES_TAC `i = k + 1` THEN ASM_REWRITE_TAC[] THENL [REWRITE_TAC[ARITH_RULE `(k + 1) + 1 = k + 1 <=> F`] THEN ASM_MESON_TAC[]; @@ -431,13 +489,13 @@ let CARD_PATHCYCLES_STEP = prove ASM_SIMP_TAC[ARITH_RULE `i < k + 2 ==> ~(i = k + 2)`] THEN REWRITE_TAC[EQ_ADD_RCANCEL] THEN COND_CASES_TAC THEN ASM_SIMP_TAC[] THENL [ASM_MESON_TAC[]; ALL_TAC] THEN - UNDISCH_TAC `path r k (y:num->A)` THEN REWRITE_TAC[path] THEN + UNDISCH_TAC `friendship_path r k (y:num->A)` THEN REWRITE_TAC[friendship_path] THEN DISCH_THEN(MATCH_MP_TAC o CONJUNCT1) THEN MAP_EVERY UNDISCH_TAC [`~(i:num = k)`; `~(i = k + 1)`; `i < k + 2`] THEN ARITH_TAC; ALL_TAC] THEN ASM_SIMP_TAC[ARITH_RULE `k + 2 < i ==> ~(i = k + 1) /\ ~(i = k + 2)`] THEN - ASM_MESON_TAC[path; ARITH_RULE `k + 2 < i ==> k < i`]);; + ASM_MESON_TAC[friendship_path; ARITH_RULE `k + 2 < i ==> k < i`]);; (* ------------------------------------------------------------------------- *) (* The first lemma about the number of cycles. *) @@ -595,7 +653,7 @@ let FRIENDSHIP = prove ASM_MESON_TAC[]; ALL_TAC] THEN SUBGOAL_THEN `EVEN(m)` ASSUME_TAC THENL - [UNDISCH_TAC `!x:person. degree x = (m:num)` THEN + [UNDISCH_TAC `!x:person. degree(x) = (m:num)` THEN DISCH_THEN(SUBST1_TAC o SYM o SPEC `a:person`) THEN EXPAND_TAC "degree" THEN MATCH_MP_TAC ELEMENTS_PAIR_UP THEN EXISTS_TAC `\x y:person. friend a x /\ friend a y /\ friend x y` THEN @@ -716,8 +774,8 @@ let FRIENDSHIP = prove ==> p divides nep2`) THEN MAP_EVERY EXISTS_TAC [`m - 1`; `CARD {x:num->person | cycle friend p x}`; - `CARD {x:num->person | path friend (p-2) x /\ x (p-2) = x 0}`; - `CARD {x:num->person | path friend (p-2) x /\ ~(x (p-2) = x 0)}`] THEN + `CARD {x:num->person | friendship_path friend (p-2) x /\ x (p-2) = x 0}`; + `CARD {x:num->person | friendship_path friend (p-2) x /\ ~(x (p-2) = x 0)}`] THEN ASM_REWRITE_TAC[] THEN CONJ_TAC THENL [MATCH_MP_TAC CYCLES_PRIME_LEMMA THEN ASM_REWRITE_TAC[]; ALL_TAC] THEN SUBGOAL_THEN `3 <= p` ASSUME_TAC THENL diff --git a/100/fta.ml b/100/fta.ml index 6e4fce8d..ec7b64f0 100644 --- a/100/fta.ml +++ b/100/fta.ml @@ -2,7 +2,28 @@ (* The fundamental theorem of arithmetic (unique prime factorization). *) (* ========================================================================= *) -needs "Library/prime.ml";; +set_jrh_lexer;; +Pb_printer.set_file_tags ["Top100"; "fta.ml"];; + +open Lib;; +open Parser;; +open Equal;; +open Bool;; +open Drule;; +open Tactics;; +open Simp;; +open Theorems;; +open Class;; +open Meson;; +open Pair;; +open Arith;; +open Calc_num;; +open Realax;; +open Ints;; +open Sets;; +open Iterate;; + +open Prime;; prioritize_num();; @@ -176,3 +197,4 @@ let FTA = prove FIRST_X_ASSUM(fun th -> SUBST1_TAC(SYM th) THEN AP_TERM_TAC) THEN MATCH_MP_TAC NPRODUCT_EQ_GEN THEN ASM_REWRITE_TAC[FINITE_DELETE] THEN SIMP_TAC[IN_DELETE; IN_ELIM_THM]]);; +Pb_printer.clear_file_tags();; diff --git a/100/gcd.ml b/100/gcd.ml index af582a00..21283e3b 100644 --- a/100/gcd.ml +++ b/100/gcd.ml @@ -2,7 +2,29 @@ (* Euclidean GCD algorithm. *) (* ========================================================================= *) -needs "Library/prime.ml";; +set_jrh_lexer;; +Pb_printer.set_file_tags ["Top100"; "gcd.ml"];; + +open Lib;; +open Fusion;; +open Basics;; +open Parser;; +open Equal;; +open Drule;; +open Tactics;; +open Simp;; +open Class;; +open Meson;; +open Arith;; +open Wf;; +open Realax;; +open Ints;; +open Define;; + +open Prime;; + +prioritize_num();; + let egcd = define `egcd(m,n) = if m = 0 then n @@ -39,3 +61,4 @@ let EGCD = prove (`!a b. (egcd (a,b) divides a /\ egcd (a,b) divides b) /\ (!e. e divides a /\ e divides b ==> e divides egcd (a,b))`, REWRITE_TAC[EGCD_GCD; GCD]);; +Pb_printer.clear_file_tags();; diff --git a/100/heron.ml b/100/heron.ml index b2716186..c770efbe 100644 --- a/100/heron.ml +++ b/100/heron.ml @@ -2,7 +2,28 @@ (* Heron's formula for the area of a triangle. *) (* ========================================================================= *) -needs "Multivariate/measure.ml";; +set_jrh_lexer;; +Pb_printer.set_file_tags ["Top100"; "heron.ml"];; + +open Lib;; +open Fusion;; +open Basics;; +open Parser;; +open Equal;; +open Bool;; +open Tactics;; +open Simp;; +open Pair;; +open Calc_num;; +open Realax;; +open Realarith;; +open Reals;; +open Calc_rat;; +open Cart;; +open Misc;; + +open Vectors;; +open Measure;; prioritize_real();; @@ -40,3 +61,4 @@ let HERON = prove SIMP_TAC[VECTOR_SUB_COMPONENT; ARITH; DIMINDEX_2] THEN SQRT_ELIM_TAC THEN SIMP_TAC[REAL_LE_SQUARE; REAL_LE_ADD] THEN CONV_TAC "100/heron.ml:REAL_RING" REAL_RING);; +Pb_printer.clear_file_tags();; diff --git a/100/inclusion_exclusion.ml b/100/inclusion_exclusion.ml index 905671f3..b8ab288c 100644 --- a/100/inclusion_exclusion.ml +++ b/100/inclusion_exclusion.ml @@ -2,6 +2,34 @@ (* Inclusion-exclusion principle, the usual and generalized forms. *) (* ========================================================================= *) +set_jrh_lexer;; +Pb_printer.set_file_tags ["Top100"; "inclusion_exclusion.ml"];; + +open Lib;; +open Fusion;; +open Parser;; +open Equal;; +open Bool;; +open Drule;; +open Tactics;; +open Simp;; +open Theorems;; +open Class;; +open Trivia;; +open Meson;; +open Nums;; +open Arith;; +open Wf;; +open Realax;; +open Calc_int;; +open Realarith;; +open Reals;; +open Calc_rat;; +open Ints;; +open Sets;; +open Iterate;; + + (* ------------------------------------------------------------------------- *) (* Simple set theory lemmas. *) (* ------------------------------------------------------------------------- *) @@ -416,3 +444,4 @@ let INCLUSION_EXCLUSION_REAL_FUNCTION = prove ASM_SIMP_TAC[PRODUCT_CLAUSES; CARD_CLAUSES; real_pow] THEN REAL_ARITH_TAC);; ***) +Pb_printer.clear_file_tags();; diff --git a/100/independence.ml b/100/independence.ml index 9d349fb1..71450ba6 100644 --- a/100/independence.ml +++ b/100/independence.ml @@ -23,8 +23,42 @@ (* for geometry see "http://en.wikipedia.org/wiki/Tarski's_axioms". *) (* ========================================================================= *) -needs "Multivariate/tarski.ml";; -needs "Multivariate/cauchy.ml";; +set_jrh_lexer;; +Pb_printer.set_file_tags ["Top100"; "independence.ml"];; + +open Lib;; +open Fusion;; +open Parser;; +open Equal;; +open Bool;; +open Drule;; +open Tactics;; +open Simp;; +open Theorems;; +open Class;; +open Trivia;; +open Meson;; +open Pair;; +open Calc_num;; +open Realax;; +open Calc_int;; +open Realarith;; +open Reals;; +open Calc_rat;; +open Ints;; +open Sets;; +open Cart;; +open Wo;; +open Misc;; + +open Vectors;; +open Topology;; +open Convex;; +open Complexes;; +open Transcendentals;; + +open Cauchy;; +open Tarski;; (* ------------------------------------------------------------------------- *) (* The semimetric we will use, directly on real^N first. Choose a sensible *) @@ -783,3 +817,4 @@ let TARSKI_AXIOM_11_NONEUCLIDEAN = prove TARSKI_AXIOM_11_EUCLIDEAN) THEN REWRITE_TAC[IN_IMAGE] THEN ANTS_TAC THENL [ASM SET_TAC[]; MATCH_MP_TAC MONO_EXISTS] THEN ASM_MESON_TAC[MEMBER_NOT_EMPTY; DEST_PLANE_NORM_LT; BETWEEN_NORM_LT]);; +Pb_printer.clear_file_tags();; diff --git a/100/isosceles.ml b/100/isosceles.ml index bbd42a63..e5b61616 100644 --- a/100/isosceles.ml +++ b/100/isosceles.ml @@ -2,8 +2,29 @@ (* Isosceles triangle theorem. *) (* ========================================================================= *) -needs "Multivariate/geom.ml";; +set_jrh_lexer;; +Pb_printer.set_file_tags ["Top100"; "isosceles.ml"];; +open Lib;; +open Fusion;; +open Parser;; +open Equal;; +open Bool;; +open Drule;; +open Tactics;; +open Simp;; +open Theorems;; +open Class;; +open Meson;; +open Reals;; +open Calc_rat;; +open Sets;; + +open Misc;; + +open Vectors;; +open Transcendentals;; +open Geom;; (* ------------------------------------------------------------------------- *) (* The theorem, according to Wikipedia. *) (* ------------------------------------------------------------------------- *) @@ -235,3 +256,4 @@ let ISOSCELES_TRIANGLE_6 = prove EXPAND_TAC "D" THEN REWRITE_TAC[midpoint] THEN REWRITE_TAC[VECTOR_ARITH `inv(&2) % (A + B) - A = inv(&2) % (B - A)`] THEN MESON_TAC[VECTOR_MUL_ASSOC]]);; +Pb_printer.clear_file_tags();; diff --git a/100/konigsberg.ml b/100/konigsberg.ml index 0cba5fd7..613de667 100644 --- a/100/konigsberg.ml +++ b/100/konigsberg.ml @@ -2,6 +2,26 @@ (* Impossibility of Eulerian path for bridges of Koenigsberg. *) (* ========================================================================= *) +set_jrh_lexer;; +Pb_printer.set_file_tags ["Top100"; "100/konigsberg.ml"];; + +open Lib;; +open Parser;; +open Bool;; +open Drule;; +open Tactics;; +open Simp;; +open Theorems;; +open Ind_defs;; +open Class;; +open Meson;; +open Pair;; +open Arith;; +open Calc_num;; +open Ints;; +open Sets;; +open Iterate;; + let edges = new_definition `edges(E:E->bool,V:V->bool,Ter:E->V->bool) = E`;; @@ -234,3 +254,5 @@ connected; cf: http://math.arizona.edu/~lagatta/class/fa05/m105/graphtheorynotes.pdf *****) + +Pb_printer.clear_file_tags();; diff --git a/100/lagrange.ml b/100/lagrange.ml index 4a1abc70..d4148f52 100644 --- a/100/lagrange.ml +++ b/100/lagrange.ml @@ -2,39 +2,56 @@ (* Very trivial group theory, just to reach Lagrange theorem. *) (* ========================================================================= *) -loadt "Library/prime.ml";; +set_jrh_lexer;; +open Lib;; +open Printer;; +open Parser;; +open Equal;; +open Bool;; +open Drule;; +open Tactics;; +open Simp;; +open Theorems;; +open Class;; +open Meson;; +open Pair;; +open Sets;; +open Prime;; (* ------------------------------------------------------------------------- *) (* Definition of what a group is. *) (* ------------------------------------------------------------------------- *) +(* Copy the same precedence and associativity as normal ** operator. *) +parse_as_infix("lagrange_group", (20, "right"));; + let group = new_definition - `group(g,( ** ),i,(e:A)) <=> + `group(g,( lagrange_group ),i,(e:A)) <=> (e IN g) /\ (!x. x IN g ==> i(x) IN g) /\ - (!x y. x IN g /\ y IN g ==> (x ** y) IN g) /\ - (!x y z. x IN g /\ y IN g /\ z IN g ==> (x ** (y ** z) = (x ** y) ** z)) /\ - (!x. x IN g ==> (x ** e = x) /\ (e ** x = x)) /\ - (!x. x IN g ==> (x ** i(x) = e) /\ (i(x) ** x = e))`;; + (!x y. x IN g /\ y IN g ==> (x lagrange_group y) IN g) /\ + (!x y z. x IN g /\ y IN g /\ z IN g ==> (x lagrange_group (y lagrange_group z) = (x lagrange_group y) lagrange_group z)) /\ + (!x. x IN g ==> (x lagrange_group e = x) /\ (e lagrange_group x = x)) /\ + (!x. x IN g ==> (x lagrange_group i(x) = e) /\ (i(x) lagrange_group x = e))`;; (* ------------------------------------------------------------------------- *) (* Notion of a subgroup. *) (* ------------------------------------------------------------------------- *) let subgroup = new_definition - `subgroup h (g,( ** ),i,(e:A)) <=> h SUBSET g /\ group(h,( ** ),i,e)`;; + `subgroup h (g,( lagrange_group ),i,(e:A)) <=> h SUBSET g /\ group(h,( lagrange_group ),i,e)`;; (* ------------------------------------------------------------------------- *) (* Lagrange theorem, introducing the coset representatives. *) (* ------------------------------------------------------------------------- *) let GROUP_LAGRANGE_COSETS = prove - (`!g h ( ** ) i e. - group (g,( ** ),i,e:A) /\ subgroup h (g,( ** ),i,e) /\ FINITE g + (`!g h ( lagrange_group ) i e. + group (g,( lagrange_group ),i,e:A) /\ subgroup h (g,( lagrange_group ),i,e) /\ FINITE g ==> ?q. (CARD(g) = CARD(q) * CARD(h)) /\ - (!b. b IN g ==> ?a x. a IN q /\ x IN h /\ (b = a ** x))`, + (!b. b IN g ==> ?a x. a IN q /\ x IN h /\ (b = a lagrange_group x))`, REPEAT GEN_TAC THEN REWRITE_TAC[group; subgroup; SUBSET] THEN STRIP_TAC THEN ABBREV_TAC - `coset = \a:A. {b:A | b IN g /\ (?x:A. x IN h /\ (b = a ** x))}` THEN + `coset = \a:A. {b:A | b IN g /\ (?x:A. x IN h /\ (b = a lagrange_group x))}` THEN SUBGOAL_THEN `!a:A. a IN g ==> a IN (coset a)` ASSUME_TAC THENL [GEN_TAC THEN DISCH_TAC THEN EXPAND_TAC "coset" THEN ASM_SIMP_TAC[IN_ELIM_THM] THEN ASM_MESON_TAC[]; @@ -47,13 +64,13 @@ let GROUP_LAGRANGE_COSETS = prove ASM_SIMP_TAC[IN_ELIM_THM; SUBSET]; ALL_TAC] THEN SUBGOAL_THEN - `!a:A x:A y. a IN g /\ x IN g /\ y IN g /\ ((a ** x) :A = a ** y) + `!a:A x:A y. a IN g /\ x IN g /\ y IN g /\ ((a lagrange_group x) :A = a lagrange_group y) ==> (x = y)` ASSUME_TAC THENL [REPEAT STRIP_TAC THEN - SUBGOAL_THEN `(e:A ** x:A):A = e ** y` (fun th -> ASM_MESON_TAC[th]) THEN + SUBGOAL_THEN `(e:A lagrange_group x:A):A = e lagrange_group y` (fun th -> ASM_MESON_TAC[th]) THEN SUBGOAL_THEN - `((i(a):A ** a:A) ** x) = (i(a) ** a) ** y` + `((i(a):A lagrange_group a:A) lagrange_group x) = (i(a) lagrange_group a) lagrange_group y` (fun th -> ASM_MESON_TAC[th]) THEN ASM_MESON_TAC[]; ALL_TAC] THEN @@ -61,7 +78,7 @@ let GROUP_LAGRANGE_COSETS = prove ASSUME_TAC THENL [REPEAT STRIP_TAC THEN SUBGOAL_THEN - `(coset:A->A->bool) (a:A) = IMAGE (\x. a ** x) (h:A->bool)` + `(coset:A->A->bool) (a:A) = IMAGE (\x. a lagrange_group x) (h:A->bool)` SUBST1_TAC THENL [EXPAND_TAC "coset" THEN REWRITE_TAC[EXTENSION; IN_ELIM_THM; IN_IMAGE; IN_ELIM_THM] THEN @@ -70,13 +87,13 @@ let GROUP_LAGRANGE_COSETS = prove MATCH_MP_TAC CARD_IMAGE_INJ THEN ASM_REWRITE_TAC[] THEN ASM_MESON_TAC[]; ALL_TAC] THEN - SUBGOAL_THEN `!x:A y. x IN g /\ y IN g ==> (i(x ** y) = i(y) ** i(x))` + SUBGOAL_THEN `!x:A y. x IN g /\ y IN g ==> (i(x lagrange_group y) = i(y) lagrange_group i(x))` ASSUME_TAC THENL [REPEAT STRIP_TAC THEN FIRST_ASSUM MATCH_MP_TAC THEN - EXISTS_TAC `(x:A ** y:A) :A` THEN ASM_SIMP_TAC[] THEN + EXISTS_TAC `(x:A lagrange_group y:A) :A` THEN ASM_SIMP_TAC[] THEN MATCH_MP_TAC EQ_TRANS THEN - EXISTS_TAC `(x:A ** (y ** i(y))) ** i(x)` THEN + EXISTS_TAC `(x:A lagrange_group (y lagrange_group i(y))) lagrange_group i(x)` THEN ASM_MESON_TAC[]; ALL_TAC] THEN SUBGOAL_THEN `!x:A. x IN g ==> (i(i(x)) = x)` ASSUME_TAC THENL @@ -89,13 +106,13 @@ let GROUP_LAGRANGE_COSETS = prove ((coset a) INTER (coset b) = {})` ASSUME_TAC THENL [REPEAT STRIP_TAC THEN - ASM_CASES_TAC `((i:A->A)(b) ** a:A) IN (h:A->bool)` THENL + ASM_CASES_TAC `((i:A->A)(b) lagrange_group a:A) IN (h:A->bool)` THENL [DISJ1_TAC THEN EXPAND_TAC "coset" THEN REWRITE_TAC[EXTENSION; IN_ELIM_THM] THEN GEN_TAC THEN AP_TERM_TAC THEN SUBGOAL_THEN - `!x:A. x IN h ==> (b ** (i(b) ** a:A) ** x = a ** x) /\ - (a ** i(i(b) ** a) ** x = b ** x)` + `!x:A. x IN h ==> (b lagrange_group (i(b) lagrange_group a:A) lagrange_group x = a lagrange_group x) /\ + (a lagrange_group i(i(b) lagrange_group a) lagrange_group x = b lagrange_group x)` (fun th -> EQ_TAC THEN REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[] THEN ASM_MESON_TAC[th]) THEN ASM_SIMP_TAC[]; @@ -106,21 +123,21 @@ let GROUP_LAGRANGE_COSETS = prove DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN DISCH_THEN(CONJUNCTS_THEN2 (X_CHOOSE_THEN `y:A` STRIP_ASSUME_TAC) (X_CHOOSE_THEN `z:A` STRIP_ASSUME_TAC)) THEN - SUBGOAL_THEN `(i(b:A) ** a ** y):A = i(b) ** b ** z` ASSUME_TAC THENL + SUBGOAL_THEN `(i(b:A) lagrange_group a lagrange_group y):A = i(b) lagrange_group b lagrange_group z` ASSUME_TAC THENL [ASM_MESON_TAC[]; ALL_TAC] THEN - SUBGOAL_THEN `(i(b:A) ** a:A ** y):A = e ** z` ASSUME_TAC THENL + SUBGOAL_THEN `(i(b:A) lagrange_group a:A lagrange_group y):A = e lagrange_group z` ASSUME_TAC THENL [ASM_MESON_TAC[]; ALL_TAC] THEN - SUBGOAL_THEN `(i(b:A) ** a:A ** y):A = z` ASSUME_TAC THENL + SUBGOAL_THEN `(i(b:A) lagrange_group a:A lagrange_group y):A = z` ASSUME_TAC THENL [ASM_MESON_TAC[]; ALL_TAC] THEN - SUBGOAL_THEN `((i(b:A) ** a:A) ** y):A = z` ASSUME_TAC THENL + SUBGOAL_THEN `((i(b:A) lagrange_group a:A) lagrange_group y):A = z` ASSUME_TAC THENL [ASM_MESON_TAC[]; ALL_TAC] THEN - SUBGOAL_THEN `((i(b:A) ** a:A) ** y) ** i(y) = z ** i(y)` ASSUME_TAC THENL + SUBGOAL_THEN `((i(b:A) lagrange_group a:A) lagrange_group y) lagrange_group i(y) = z lagrange_group i(y)` ASSUME_TAC THENL [ASM_MESON_TAC[]; ALL_TAC] THEN - SUBGOAL_THEN `(i(b:A) ** a:A) ** (y ** i(y)) = z ** i(y)` ASSUME_TAC THENL + SUBGOAL_THEN `(i(b:A) lagrange_group a:A) lagrange_group (y lagrange_group i(y)) = z lagrange_group i(y)` ASSUME_TAC THENL [ASM_MESON_TAC[]; ALL_TAC] THEN - SUBGOAL_THEN `(i(b:A) ** a:A) ** e = z ** i(y)` ASSUME_TAC THENL + SUBGOAL_THEN `(i(b:A) lagrange_group a:A) lagrange_group e = z lagrange_group i(y)` ASSUME_TAC THENL [ASM_MESON_TAC[]; ALL_TAC] THEN - SUBGOAL_THEN `(i(b:A) ** a:A):A = z ** i(y)` ASSUME_TAC THENL + SUBGOAL_THEN `(i(b:A) lagrange_group a:A):A = z lagrange_group i(y)` ASSUME_TAC THENL [ASM_MESON_TAC[]; ALL_TAC] THEN ASM_MESON_TAC[]; ALL_TAC] THEN @@ -136,7 +153,7 @@ let GROUP_LAGRANGE_COSETS = prove [REWRITE_TAC[IN] THEN MATCH_MP_TAC SELECT_AX THEN ASM_MESON_TAC[IN]; ALL_TAC] THEN - FIRST_ASSUM(fun th -> GEN_REWRITE_TAC "100/lagrange.ml:(LAND_CONV o RAND_CONV o RATOR_CONV)" (LAND_CONV o RAND_CONV o RATOR_CONV) + FIRST_ASSUM(fun th -> GEN_REWRITE_TAC "100/lagrange.ml:(LAND_CONV o RAND_CONV o RATOR_CONV)" (LAND_CONV o RAND_CONV o RATOR_CONV) [SYM th]) THEN REWRITE_TAC[] THEN ABBREV_TAC `C = (@)((coset:A->A->bool) b)` THEN @@ -189,7 +206,7 @@ let GROUP_LAGRANGE_COSETS = prove ALL_TAC] THEN SUBGOAL_THEN `!a:A x:A a' x'. a IN q /\ a' IN q /\ x IN h /\ x' IN h /\ - ((a' ** x') :A = a ** x) ==> (a' = a) /\ (x' = x)` + ((a' lagrange_group x') :A = a lagrange_group x) ==> (a' = a) /\ (x' = x)` ASSUME_TAC THENL [REPEAT GEN_TAC THEN EXPAND_TAC "q" THEN REWRITE_TAC[IN_ELIM_THM] THEN MATCH_MP_TAC(TAUT `(c ==> a /\ b ==> d) ==> a /\ b /\ c ==> d`) THEN @@ -211,12 +228,12 @@ let GROUP_LAGRANGE_COSETS = prove ONCE_ASM_REWRITE_TAC[] THEN AP_TERM_TAC THEN FIRST_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[] THEN EXPAND_TAC "coset" THEN REWRITE_TAC[IN_ELIM_THM] THEN - ASM_REWRITE_TAC[] THEN EXISTS_TAC `(x:A ** (i:A->A)(x')):A` THEN - ASM_SIMP_TAC[] THEN UNDISCH_TAC `(a':A ** x':A):A = a ** x` THEN - DISCH_THEN(MP_TAC o C AP_THM `(i:A->A) x'` o AP_TERM `(**):A->A->A`) THEN + ASM_REWRITE_TAC[] THEN EXISTS_TAC `(x:A lagrange_group (i:A->A)(x')):A` THEN + ASM_SIMP_TAC[] THEN UNDISCH_TAC `(a':A lagrange_group x':A):A = a lagrange_group x` THEN + DISCH_THEN(MP_TAC o C AP_THM `(i:A->A) x'` o AP_TERM `(lagrange_group):A->A->A`) THEN DISCH_THEN(SUBST1_TAC o SYM) THEN ASM_MESON_TAC[]; ALL_TAC] THEN - SUBGOAL_THEN `g = IMAGE (\(a:A,x:A). (a ** x):A) {(a,x) | a IN q /\ x IN h}` + SUBGOAL_THEN `g = IMAGE (\(a:A,x:A). (a lagrange_group x):A) {(a,x) | a IN q /\ x IN h}` SUBST1_TAC THENL [REWRITE_TAC[EXTENSION; IN_IMAGE; IN_ELIM_THM] THEN REWRITE_TAC[EXISTS_PAIR_THM] THEN @@ -247,8 +264,8 @@ let GROUP_LAGRANGE_COSETS = prove (* ------------------------------------------------------------------------- *) let GROUP_LAGRANGE = prove - (`!g h ( ** ) i e. - group (g,( ** ),i,e:A) /\ subgroup h (g,( ** ),i,e) /\ FINITE g + (`!g h ( lagrange_group ) i e. + group (g,( lagrange_group ),i,e:A) /\ subgroup h (g,( lagrange_group ),i,e) /\ FINITE g ==> (CARD h) divides (CARD g)`, REPEAT GEN_TAC THEN DISCH_THEN(MP_TAC o MATCH_MP GROUP_LAGRANGE_COSETS) THEN MESON_TAC[DIVIDES_LMUL; DIVIDES_REFL]);; diff --git a/100/leibniz.ml b/100/leibniz.ml index 975253e6..2fb0b953 100644 --- a/100/leibniz.ml +++ b/100/leibniz.ml @@ -2,7 +2,34 @@ (* #26: Leibniz's series for pi *) (* ========================================================================= *) -needs "Library/transc.ml";; +set_jrh_lexer;; +Pb_printer.set_file_tags ["Top100"; "leibniz.ml"];; + +open Lib;; +open Fusion;; +open Basics;; +open Parser;; +open Equal;; +open Bool;; +open Drule;; +open Tactics;; +open Simp;; +open Theorems;; +open Class;; +open Meson;; +open Nums;; +open Arith;; +open Calc_num;; +open Realax;; +open Calc_int;; +open Realarith;; +open Reals;; +open Calc_rat;; +open Ints;; +open Iterate;; + +open Analysis;; +open Transc;; prioritize_real();; @@ -300,3 +327,4 @@ let LEIBNIZ_PI = prove `abs(s1 - sx) < e / &6 ==> ~(abs(sx - s) < e / &2) ==> ~(abs(s1 - s) < e / &3)`)) THEN ASM_REAL_ARITH_TAC);; +Pb_printer.clear_file_tags();; diff --git a/100/lhopital.ml b/100/lhopital.ml index 93e178f1..598deb3f 100644 --- a/100/lhopital.ml +++ b/100/lhopital.ml @@ -2,7 +2,28 @@ (* #64: L'Hopital's rule. *) (* ========================================================================= *) -needs "Library/analysis.ml";; +set_jrh_lexer;; +Pb_printer.set_file_tags ["Top100"; "lhopital.ml"];; + +open Lib;; +open Fusion;; +open Preterm;; +open Parser;; +open Equal;; +open Bool;; +open Drule;; +open Tactics;; +open Simp;; +open Theorems;; +open Class;; +open Meson;; +open Realax;; +open Calc_int;; +open Realarith;; +open Reals;; +open Calc_rat;; + +open Analysis;; override_interface ("-->",`(tends_real_real)`);; @@ -198,3 +219,4 @@ let LHOPITAL = prove ASM_SIMP_TAC[REAL_ARITH `&0 < abs(x - c) /\ &0 < abs z /\ abs z < abs(x - c) ==> ~(x + z = c)`] THEN ASM_REWRITE_TAC[REAL_SUB_REFL; REAL_ABS_NUM]);; +Pb_printer.clear_file_tags();; diff --git a/100/liouville.ml b/100/liouville.ml index 5f05211c..ceabc49b 100644 --- a/100/liouville.ml +++ b/100/liouville.ml @@ -2,8 +2,36 @@ (* Liouville approximation theorem. *) (* ========================================================================= *) -needs "Library/floor.ml";; -needs "Library/poly.ml";; +set_jrh_lexer;; +Pb_printer.set_file_tags ["Top100"; "liouville.ml"];; + +open Lib;; +open Parser;; +open Equal;; +open Bool;; +open Drule;; +open Tactics;; +open Simp;; +open Theorems;; +open Class;; +open Meson;; +open Pair;; +open Nums;; +open Arith;; +open Calc_num;; +open Lists;; +open Realax;; +open Calc_int;; +open Realarith;; +open Reals;; +open Calc_rat;; +open Ints;; +open Sets;; +open Iterate;; + +open Floor;; +open Analysis;; +open Poly;; (* ------------------------------------------------------------------------- *) (* Definition of algebraic and transcendental. *) @@ -427,3 +455,4 @@ let TRANSCENDENTAL_LIOUVILLE = prove GEN_REWRITE_TAC "100/liouville.ml:LAND_CONV" LAND_CONV [ARITH_RULE `k = k * 1`] THEN MATCH_MP_TAC LE_MULT2 THEN REWRITE_TAC[LE_ADD] THEN REWRITE_TAC[FACT_LT; ARITH_RULE `1 <= x <=> 0 < x`]);; +Pb_printer.clear_file_tags();; diff --git a/100/minkowski.ml b/100/minkowski.ml index ab42cd32..92d0c197 100644 --- a/100/minkowski.ml +++ b/100/minkowski.ml @@ -2,7 +2,34 @@ (* Minkowski's convex body theorem. *) (* ========================================================================= *) -needs "Multivariate/measure.ml";; +set_jrh_lexer;; +Pb_printer.set_file_tags ["Top100"; "minkowski.ml"];; + +open Lib;; +open Parser;; +open Equal;; +open Bool;; +open Drule;; +open Tactics;; +open Simp;; +open Theorems;; +open Class;; +open Meson;; +open Calc_num;; +open Realax;; +open Calc_int;; +open Realarith;; +open Reals;; +open Calc_rat;; +open Sets;; +open Cart;; +open Floor;; + +open Vectors;; +open Topology;; +open Convex;; +open Integration;; +open Measure;; (* ------------------------------------------------------------------------- *) (* An ad hoc lemma. *) @@ -92,7 +119,7 @@ let BLICHFELDT = prove EXISTS_TAC `x + (v - u):real^N` THEN ASM_REWRITE_TAC[VECTOR_ARITH `x = x + (v - u) <=> v:real^N = u`] THEN ASM_SIMP_TAC[VECTOR_SUB_COMPONENT; VECTOR_ADD_COMPONENT] THEN - ASM_SIMP_TAC[REAL_ARITH `x - (x + v - u):real = u - v`; + ASM_SIMP_TAC[REAL_ARITH `x - (x + v - u):real = u - v`; INTEGER_CLOSED]] THEN REPEAT CONJ_TAC THENL [SUBGOAL_THEN @@ -284,3 +311,4 @@ let MINKOWSKI_COMPACT = prove ASM_SIMP_TAC[REAL_ARITH `&0 < x ==> abs x = x`] THEN ASM_SIMP_TAC[REAL_DIV_RMUL; REAL_LT_IMP_NZ] THEN UNDISCH_TAC `&0 < d` THEN REAL_ARITH_TAC);; +Pb_printer.clear_file_tags();; diff --git a/100/morley.ml b/100/morley.ml index 42fa332b..faab5033 100644 --- a/100/morley.ml +++ b/100/morley.ml @@ -2,8 +2,42 @@ (* Formalization of Alain Connes's paper "A new proof of Morley's theorem". *) (* ========================================================================= *) -needs "Library/iter.ml";; -needs "Multivariate/geom.ml";; +set_jrh_lexer;; +Pb_printer.set_file_tags ["Top100"; "morley.ml"];; + +open Lib;; +open Fusion;; +open Basics;; +open Parser;; +open Equal;; +open Bool;; +open Drule;; +open Tactics;; +open Simp;; +open Theorems;; +open Class;; +open Trivia;; +open Meson;; +open Pair;; +open Nums;; +open Arith;; +open Calc_num;; +open Realax;; +open Calc_int;; +open Realarith;; +open Reals;; +open Calc_rat;; +open Sets;; + +open Floor;; +open Iter;; + +open Vectors;; +open Convex;; +open Complexes;; +open Transcendentals;; + +open Geom;; (* ------------------------------------------------------------------------- *) (* Reflection about the line[0,e^{i t}] *) @@ -464,3 +498,4 @@ let MORLEY = prove MATCH_MP_TAC ALGEBRAIC_LEMMA THEN MAP_EVERY EXISTS_TAC [`b1:complex`; `b2:complex`; `b3:complex`] THEN PURE_ASM_REWRITE_TAC[] THEN REWRITE_TAC[]);; +Pb_printer.clear_file_tags();; diff --git a/100/pascal.ml b/100/pascal.ml index 47ad4076..840bb7b7 100644 --- a/100/pascal.ml +++ b/100/pascal.ml @@ -2,302 +2,37 @@ (* Pascal's hexagon theorem for projective and affine planes. *) (* ========================================================================= *) -needs "Multivariate/cross.ml";; - -(* ------------------------------------------------------------------------- *) -(* A lemma we want to justify some of the axioms. *) -(* ------------------------------------------------------------------------- *) - -let NORMAL_EXISTS = prove - (`!u v:real^3. ?w. ~(w = vec 0) /\ orthogonal u w /\ orthogonal v w`, - REPEAT GEN_TAC THEN ONCE_REWRITE_TAC[ORTHOGONAL_SYM] THEN - MP_TAC(ISPEC `{u:real^3,v}` ORTHOGONAL_TO_SUBSPACE_EXISTS) THEN - REWRITE_TAC[FORALL_IN_INSERT; NOT_IN_EMPTY; DIMINDEX_3] THEN - DISCH_THEN MATCH_MP_TAC THEN MATCH_MP_TAC LET_TRANS THEN - EXISTS_TAC `CARD {u:real^3,v}` THEN CONJ_TAC THEN - SIMP_TAC[DIM_LE_CARD; FINITE_INSERT; FINITE_EMPTY] THEN - SIMP_TAC[CARD_CLAUSES; FINITE_INSERT; FINITE_EMPTY] THEN ARITH_TAC);; - -(* ------------------------------------------------------------------------- *) -(* Type of directions. *) -(* ------------------------------------------------------------------------- *) - -let direction_tybij = new_type_definition "direction" ("mk_dir","dest_dir") - (MESON[BASIS_NONZERO; LE_REFL; DIMINDEX_GE_1] `?x:real^3. ~(x = vec 0)`);; - -parse_as_infix("||",(11,"right"));; -parse_as_infix("_|_",(11,"right"));; - -let perpdir = new_definition - `x _|_ y <=> orthogonal (dest_dir x) (dest_dir y)`;; - -let pardir = new_definition - `x || y <=> (dest_dir x) cross (dest_dir y) = vec 0`;; - -let DIRECTION_CLAUSES = prove - (`((!x. P(dest_dir x)) <=> (!x. ~(x = vec 0) ==> P x)) /\ - ((?x. P(dest_dir x)) <=> (?x. ~(x = vec 0) /\ P x))`, - MESON_TAC[direction_tybij]);; - -let [PARDIR_REFL; PARDIR_SYM; PARDIR_TRANS] = (CONJUNCTS o prove) - (`(!x. x || x) /\ - (!x y. x || y <=> y || x) /\ - (!x y z. x || y /\ y || z ==> x || z)`, - REWRITE_TAC[pardir; DIRECTION_CLAUSES] THEN VEC3_TAC);; - -let PARDIR_EQUIV = prove - (`!x y. ((||) x = (||) y) <=> x || y`, - REWRITE_TAC[FUN_EQ_THM] THEN - MESON_TAC[PARDIR_REFL; PARDIR_SYM; PARDIR_TRANS]);; - -let DIRECTION_AXIOM_1 = prove - (`!p p'. ~(p || p') ==> ?l. p _|_ l /\ p' _|_ l /\ - !l'. p _|_ l' /\ p' _|_ l' ==> l' || l`, - REWRITE_TAC[perpdir; pardir; DIRECTION_CLAUSES] THEN REPEAT STRIP_TAC THEN - MP_TAC(SPECL [`p:real^3`; `p':real^3`] NORMAL_EXISTS) THEN - MATCH_MP_TAC MONO_EXISTS THEN - POP_ASSUM_LIST(MP_TAC o end_itlist CONJ) THEN VEC3_TAC);; - -let DIRECTION_AXIOM_2 = prove - (`!l l'. ?p. p _|_ l /\ p _|_ l'`, - REWRITE_TAC[perpdir; DIRECTION_CLAUSES] THEN - MESON_TAC[NORMAL_EXISTS; ORTHOGONAL_SYM]);; - -let DIRECTION_AXIOM_3 = prove - (`?p p' p''. - ~(p || p') /\ ~(p' || p'') /\ ~(p || p'') /\ - ~(?l. p _|_ l /\ p' _|_ l /\ p'' _|_ l)`, - REWRITE_TAC[perpdir; pardir; DIRECTION_CLAUSES] THEN MAP_EVERY - (fun t -> EXISTS_TAC t THEN SIMP_TAC[BASIS_NONZERO; DIMINDEX_3; ARITH]) - [`basis 1 :real^3`; `basis 2 : real^3`; `basis 3 :real^3`] THEN - VEC3_TAC);; - -let DIRECTION_AXIOM_4_WEAK = prove - (`!l. ?p p'. ~(p || p') /\ p _|_ l /\ p' _|_ l`, - REWRITE_TAC[DIRECTION_CLAUSES; pardir; perpdir] THEN REPEAT STRIP_TAC THEN - SUBGOAL_THEN - `orthogonal (l cross basis 1) l /\ orthogonal (l cross basis 2) l /\ - ~((l cross basis 1) cross (l cross basis 2) = vec 0) \/ - orthogonal (l cross basis 1) l /\ orthogonal (l cross basis 3) l /\ - ~((l cross basis 1) cross (l cross basis 3) = vec 0) \/ - orthogonal (l cross basis 2) l /\ orthogonal (l cross basis 3) l /\ - ~((l cross basis 2) cross (l cross basis 3) = vec 0)` - MP_TAC THENL [POP_ASSUM MP_TAC THEN VEC3_TAC; MESON_TAC[CROSS_0]]);; - -let ORTHOGONAL_COMBINE = prove - (`!x a b. a _|_ x /\ b _|_ x /\ ~(a || b) - ==> ?c. c _|_ x /\ ~(a || c) /\ ~(b || c)`, - REWRITE_TAC[DIRECTION_CLAUSES; pardir; perpdir] THEN - REPEAT STRIP_TAC THEN EXISTS_TAC `a + b:real^3` THEN - POP_ASSUM_LIST(MP_TAC o end_itlist CONJ) THEN VEC3_TAC);; - -let DIRECTION_AXIOM_4 = prove - (`!l. ?p p' p''. ~(p || p') /\ ~(p' || p'') /\ ~(p || p'') /\ - p _|_ l /\ p' _|_ l /\ p'' _|_ l`, - MESON_TAC[DIRECTION_AXIOM_4_WEAK; ORTHOGONAL_COMBINE]);; - -let line_tybij = define_quotient_type "line" ("mk_line","dest_line") `(||)`;; - -let PERPDIR_WELLDEF = prove - (`!x y x' y'. x || x' /\ y || y' ==> (x _|_ y <=> x' _|_ y')`, - REWRITE_TAC[perpdir; pardir; DIRECTION_CLAUSES] THEN VEC3_TAC);; - -let perpl,perpl_th = - lift_function (snd line_tybij) (PARDIR_REFL,PARDIR_TRANS) - "perpl" PERPDIR_WELLDEF;; - -let line_lift_thm = lift_theorem line_tybij - (PARDIR_REFL,PARDIR_SYM,PARDIR_TRANS) [perpl_th];; - -let LINE_AXIOM_1 = line_lift_thm DIRECTION_AXIOM_1;; -let LINE_AXIOM_2 = line_lift_thm DIRECTION_AXIOM_2;; -let LINE_AXIOM_3 = line_lift_thm DIRECTION_AXIOM_3;; -let LINE_AXIOM_4 = line_lift_thm DIRECTION_AXIOM_4;; - -let point_tybij = new_type_definition "point" ("mk_point","dest_point") - (prove(`?x:line. T`,REWRITE_TAC[]));; - -parse_as_infix("on",(11,"right"));; - -let on = new_definition `p on l <=> perpl (dest_point p) l`;; - -let POINT_CLAUSES = prove - (`((p = p') <=> (dest_point p = dest_point p')) /\ - ((!p. P (dest_point p)) <=> (!l. P l)) /\ - ((?p. P (dest_point p)) <=> (?l. P l))`, - MESON_TAC[point_tybij]);; - -let POINT_TAC th = REWRITE_TAC[on; POINT_CLAUSES] THEN ACCEPT_TAC th;; - -let AXIOM_1 = prove - (`!p p'. ~(p = p') ==> ?l. p on l /\ p' on l /\ - !l'. p on l' /\ p' on l' ==> (l' = l)`, - POINT_TAC LINE_AXIOM_1);; - -let AXIOM_2 = prove - (`!l l'. ?p. p on l /\ p on l'`, - POINT_TAC LINE_AXIOM_2);; - -let AXIOM_3 = prove - (`?p p' p''. ~(p = p') /\ ~(p' = p'') /\ ~(p = p'') /\ - ~(?l. p on l /\ p' on l /\ p'' on l)`, - POINT_TAC LINE_AXIOM_3);; - -let AXIOM_4 = prove - (`!l. ?p p' p''. ~(p = p') /\ ~(p' = p'') /\ ~(p = p'') /\ - p on l /\ p' on l /\ p'' on l`, - POINT_TAC LINE_AXIOM_4);; - -(* ------------------------------------------------------------------------- *) -(* Mappings from vectors in R^3 to projective lines and points. *) -(* ------------------------------------------------------------------------- *) - -let projl = new_definition - `projl x = mk_line((||) (mk_dir x))`;; - -let projp = new_definition - `projp x = mk_point(projl x)`;; - -(* ------------------------------------------------------------------------- *) -(* Mappings in the other direction, to (some) homogeneous coordinates. *) -(* ------------------------------------------------------------------------- *) - -let PROJL_TOTAL = prove - (`!l. ?x. ~(x = vec 0) /\ l = projl x`, - GEN_TAC THEN - SUBGOAL_THEN `?d. l = mk_line((||) d)` (CHOOSE_THEN SUBST1_TAC) THENL - [MESON_TAC[fst line_tybij; snd line_tybij]; - REWRITE_TAC[projl] THEN EXISTS_TAC `dest_dir d` THEN - MESON_TAC[direction_tybij]]);; - -let homol = new_specification ["homol"] - (REWRITE_RULE[SKOLEM_THM] PROJL_TOTAL);; - -let PROJP_TOTAL = prove - (`!p. ?x. ~(x = vec 0) /\ p = projp x`, - REWRITE_TAC[projp] THEN MESON_TAC[PROJL_TOTAL; point_tybij]);; - -let homop_def = new_definition - `homop p = homol(dest_point p)`;; - -let homop = prove - (`!p. ~(homop p = vec 0) /\ p = projp(homop p)`, - GEN_TAC THEN REWRITE_TAC[homop_def; projp; MESON[point_tybij] - `p = mk_point l <=> dest_point p = l`] THEN - MATCH_ACCEPT_TAC homol);; - -(* ------------------------------------------------------------------------- *) -(* Key equivalences of concepts in projective space and homogeneous coords. *) -(* ------------------------------------------------------------------------- *) - -let parallel = new_definition - `parallel x y <=> x cross y = vec 0`;; - -let ON_HOMOL = prove - (`!p l. p on l <=> orthogonal (homop p) (homol l)`, - REPEAT GEN_TAC THEN - GEN_REWRITE_TAC "100/pascal.ml:(LAND_CONV o ONCE_DEPTH_CONV)" (LAND_CONV o ONCE_DEPTH_CONV) [homop; homol] THEN - REWRITE_TAC[on; projp; projl; REWRITE_RULE[] point_tybij] THEN - REWRITE_TAC[GSYM perpl_th; perpdir] THEN BINOP_TAC THEN - MESON_TAC[homol; homop; direction_tybij]);; - -let EQ_HOMOL = prove - (`!l l'. l = l' <=> parallel (homol l) (homol l')`, - REPEAT GEN_TAC THEN - GEN_REWRITE_TAC "100/pascal.ml:(LAND_CONV o BINOP_CONV)" (LAND_CONV o BINOP_CONV) [homol] THEN - REWRITE_TAC[projl; MESON[fst line_tybij; snd line_tybij] - `mk_line((||) l) = mk_line((||) l') <=> (||) l = (||) l'`] THEN - REWRITE_TAC[PARDIR_EQUIV] THEN REWRITE_TAC[pardir; parallel] THEN - MESON_TAC[homol; direction_tybij]);; - -let EQ_HOMOP = prove - (`!p p'. p = p' <=> parallel (homop p) (homop p')`, - REWRITE_TAC[homop_def; GSYM EQ_HOMOL] THEN - MESON_TAC[point_tybij]);; - -(* ------------------------------------------------------------------------- *) -(* A "welldefinedness" result for homogeneous coordinate map. *) -(* ------------------------------------------------------------------------- *) - -let PARALLEL_PROJL_HOMOL = prove - (`!x. parallel x (homol(projl x))`, - GEN_TAC THEN REWRITE_TAC[parallel] THEN ASM_CASES_TAC `x:real^3 = vec 0` THEN - ASM_REWRITE_TAC[CROSS_0] THEN MP_TAC(ISPEC `projl x` homol) THEN - DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN - GEN_REWRITE_TAC "100/pascal.ml:(LAND_CONV o ONCE_DEPTH_CONV)" (LAND_CONV o ONCE_DEPTH_CONV) [projl] THEN - DISCH_THEN(MP_TAC o AP_TERM `dest_line`) THEN - REWRITE_TAC[MESON[fst line_tybij; snd line_tybij] - `dest_line(mk_line((||) l)) = (||) l`] THEN - REWRITE_TAC[PARDIR_EQUIV] THEN REWRITE_TAC[pardir] THEN - ASM_MESON_TAC[direction_tybij]);; - -let PARALLEL_PROJP_HOMOP = prove - (`!x. parallel x (homop(projp x))`, - REWRITE_TAC[homop_def; projp; REWRITE_RULE[] point_tybij] THEN - REWRITE_TAC[PARALLEL_PROJL_HOMOL]);; - -let PARALLEL_PROJP_HOMOP_EXPLICIT = prove - (`!x. ~(x = vec 0) ==> ?a. ~(a = &0) /\ homop(projp x) = a % x`, - MP_TAC PARALLEL_PROJP_HOMOP THEN MATCH_MP_TAC MONO_FORALL THEN - REWRITE_TAC[parallel; CROSS_EQ_0; COLLINEAR_LEMMA] THEN - GEN_TAC THEN ASM_CASES_TAC `x:real^3 = vec 0` THEN - ASM_REWRITE_TAC[homop] THEN MATCH_MP_TAC MONO_EXISTS THEN - X_GEN_TAC `c:real` THEN ASM_CASES_TAC `c = &0` THEN - ASM_REWRITE_TAC[homop; VECTOR_MUL_LZERO]);; - -(* ------------------------------------------------------------------------- *) -(* Brackets, collinearity and their connection. *) -(* ------------------------------------------------------------------------- *) - -let bracket = define - `bracket[a;b;c] = det(vector[homop a;homop b;homop c])`;; - -let COLLINEAR = new_definition - `COLLINEAR s <=> ?l. !p. p IN s ==> p on l`;; - -let COLLINEAR_SINGLETON = prove - (`!a. COLLINEAR {a}`, - REWRITE_TAC[COLLINEAR; FORALL_IN_INSERT; NOT_IN_EMPTY] THEN - MESON_TAC[AXIOM_1; AXIOM_3]);; - -let COLLINEAR_PAIR = prove - (`!a b. COLLINEAR{a,b}`, - REPEAT GEN_TAC THEN ASM_CASES_TAC `a:point = b` THEN - ASM_REWRITE_TAC[INSERT_AC; COLLINEAR_SINGLETON] THEN - REWRITE_TAC[COLLINEAR; FORALL_IN_INSERT; NOT_IN_EMPTY] THEN - ASM_MESON_TAC[AXIOM_1]);; - -let COLLINEAR_TRIPLE = prove - (`!a b c. COLLINEAR{a,b,c} <=> ?l. a on l /\ b on l /\ c on l`, - REWRITE_TAC[COLLINEAR; FORALL_IN_INSERT; NOT_IN_EMPTY]);; - -let COLLINEAR_BRACKET = prove - (`!p1 p2 p3. COLLINEAR {p1,p2,p3} <=> bracket[p1;p2;p3] = &0`, - let lemma = prove - (`!a b c x y. - x cross y = vec 0 /\ ~(x = vec 0) /\ - orthogonal a x /\ orthogonal b x /\ orthogonal c x - ==> orthogonal a y /\ orthogonal b y /\ orthogonal c y`, - REWRITE_TAC[orthogonal] THEN VEC3_TAC) in - REPEAT GEN_TAC THEN EQ_TAC THENL - [REWRITE_TAC[COLLINEAR_TRIPLE; bracket; ON_HOMOL; LEFT_IMP_EXISTS_THM] THEN - MP_TAC homol THEN MATCH_MP_TAC MONO_FORALL THEN - GEN_TAC THEN DISCH_THEN(MP_TAC o CONJUNCT1) THEN - REWRITE_TAC[DET_3; orthogonal; DOT_3; VECTOR_3; CART_EQ; - DIMINDEX_3; FORALL_3; VEC_COMPONENT] THEN - CONV_TAC "100/pascal.ml:REAL_RING" REAL_RING; - ASM_CASES_TAC `p1:point = p2` THENL - [ASM_REWRITE_TAC[INSERT_AC; COLLINEAR_PAIR]; ALL_TAC] THEN - POP_ASSUM MP_TAC THEN - REWRITE_TAC[parallel; COLLINEAR_TRIPLE; bracket; EQ_HOMOP; ON_HOMOL] THEN - REPEAT STRIP_TAC THEN - EXISTS_TAC `mk_line((||) (mk_dir(homop p1 cross homop p2)))` THEN - MATCH_MP_TAC lemma THEN EXISTS_TAC `homop p1 cross homop p2` THEN - ASM_REWRITE_TAC[ORTHOGONAL_CROSS] THEN - REWRITE_TAC[orthogonal] THEN ONCE_REWRITE_TAC[DOT_SYM] THEN - ONCE_REWRITE_TAC[CROSS_TRIPLE] THEN ONCE_REWRITE_TAC[DOT_SYM] THEN - ASM_REWRITE_TAC[DOT_CROSS_DET] THEN - REWRITE_TAC[GSYM projl; GSYM parallel; PARALLEL_PROJL_HOMOL]]);; +set_jrh_lexer;; +Pb_printer.set_file_tags ["Top100"; "pascal.ml"];; + +open Lib;; +open Fusion;; +open Parser;; +open Equal;; +open Bool;; +open Drule;; +open Tactics;; +open Simp;; +open Theorems;; +open Class;; +open Trivia;; +open Meson;; +open Pair;; +open Lists;; +open Realax;; +open Calc_int;; +open Reals;; +open Calc_rat;; +open Sets;; +open Cart;; + +open Vectors;; +open Determinants;; + +open Cross;; +open Desargues;; + +(* NOTE: Many duplicate theorems and definitions from desargues.ml are removed*) (* ------------------------------------------------------------------------- *) (* Conics and bracket condition for 6 points to be on a conic. *) @@ -508,7 +243,7 @@ let COLLINEAR_PROJECTIVIZE = prove [`a:real^2`; `b:real^2`; `c:real^2`] THEN MAP_EVERY (MP_TAC o CONJUNCT1 o C SPEC homop) [`projp(homogenize a)`; `projp(homogenize b)`; `projp(homogenize c)`] THEN - REWRITE_TAC[parallel; cross; CART_EQ; DIMINDEX_3; FORALL_3; VECTOR_3; + REWRITE_TAC[desargues_parallel; cross; CART_EQ; DIMINDEX_3; FORALL_3; VECTOR_3; DET_3; VEC_COMPONENT] THEN CONV_TAC "100/pascal.ml:REAL_RING" REAL_RING]);; @@ -623,3 +358,4 @@ let PASCAL_AFFINE_CIRCLE = prove REWRITE_TAC[DOT_2; VECTOR_SUB_COMPONENT] THEN REAL_ARITH_TAC; REPLICATE_TAC 5 (EXISTS_TAC `&0`) THEN EXISTS_TAC `&1` THEN REWRITE_TAC[EXTENSION; IN_ELIM_THM] THEN REAL_ARITH_TAC]]);; +Pb_printer.clear_file_tags();; diff --git a/100/perfect.ml b/100/perfect.ml index d916d1eb..a76a5157 100644 --- a/100/perfect.ml +++ b/100/perfect.ml @@ -2,7 +2,32 @@ (* Perfect number theorems. *) (* ========================================================================= *) -needs "Library/prime.ml";; +set_jrh_lexer;; +Pb_printer.set_file_tags ["Top100"; "perfect.ml"];; + +open Lib;; +open Fusion;; +open Parser;; +open Equal;; +open Bool;; +open Drule;; +open Tactics;; +open Simp;; +open Theorems;; +open Class;; +open Trivia;; +open Meson;; +open Pair;; +open Nums;; +open Arith;; +open Calc_num;; +open Realax;; +open Ints;; +open Sets;; +open Iterate;; +open Wo;; + +open Prime;; prioritize_num();; @@ -281,3 +306,4 @@ let PERFECT_EULER = prove ASM_REWRITE_TAC[LT_MULT_RCANCEL] THEN MATCH_MP_TAC(ARITH_RULE `2 EXP 0 < a ==> 1 < a`) THEN REWRITE_TAC[LT_EXP] THEN UNDISCH_TAC `~(r = 0)` THEN ARITH_TAC]);; +Pb_printer.clear_file_tags();; diff --git a/100/pick.ml b/100/pick.ml index 22dd2647..8c5a28b9 100644 --- a/100/pick.ml +++ b/100/pick.ml @@ -2,9 +2,81 @@ (* Pick's theorem. *) (* ========================================================================= *) -needs "Multivariate/polytope.ml";; -needs "Multivariate/measure.ml";; -needs "Multivariate/moretop.ml";; +set_jrh_lexer;; +open System;; +open Lib;; +open Fusion;; +open Basics;; +open Nets;; +open Printer;; +open Preterm;; +open Parser;; +open Equal;; +open Bool;; +open Drule;; +open Log;; +open Import_proofs;; +open Tactics;; +open Itab;; +open Replay;; +open Simp;; +open Embryo_extra;; +open Theorems;; +open Ind_defs;; +open Class;; +open Trivia;; +open Canon;; +open Meson;; +open Metis;; +open Quot;; +open Impconv;; +open Pair;; +open Nums;; +open Recursion;; +open Arith;; +open Wf;; +open Calc_num;; +open Normalizer;; +open Grobner;; +open Ind_types;; +open Lists;; +open Realax;; +open Calc_int;; +open Realarith;; +open Reals;; +open Calc_rat;; +open Ints;; +open Sets;; +open Iterate;; +open Cart;; +open Define;; +open Help;; +open Wo;; +open Binary;; +open Card;; +open Permutations;; +open Products;; +open Floor;; +open Misc;; +open Iter;; + +open Vectors;; +open Determinants;; +open Topology;; +open Convex;; +open Paths;; +open Polytope;; +open Degree;; +open Derivatives;; +open Clifford;; +open Integration;; +open Measure;; +open Binomial;; +open Complexes;; +open Canal;; +open Transcendentals;; +open Realanalysis;; +open Moretop;; prioritize_real();; diff --git a/100/piseries.ml b/100/piseries.ml index f29f3667..cd999790 100644 --- a/100/piseries.ml +++ b/100/piseries.ml @@ -2,12 +2,39 @@ (* Taylor series for tan and cot, via partial fractions expansion of cot. *) (* ========================================================================= *) -needs "Library/analysis.ml";; -needs "Library/transc.ml";; -needs "Library/floor.ml";; -needs "Library/poly.ml";; -needs "Examples/machin.ml";; -needs "Library/iter.ml";; +set_jrh_lexer;; +Pb_printer.set_file_tags ["Top100"; "piseries.ml"];; + +open Lib;; +open Fusion;; +open Basics;; +open Parser;; +open Equal;; +open Bool;; +open Drule;; +open Tactics;; +open Simp;; +open Theorems;; +open Class;; +open Meson;; +open Pair;; +open Nums;; +open Recursion;; +open Arith;; +open Calc_num;; +open Realax;; +open Calc_int;; +open Realarith;; +open Reals;; +open Calc_rat;; +open Ints;; + +open Floor;; +open Iter;; +open Analysis;; +open Transc;; +open Poly;; +open Machin;; (* ------------------------------------------------------------------------- *) (* Compatibility stuff for some old proofs. *) @@ -3305,3 +3332,4 @@ let TAYLOR_COTXX_SQRT_BOUND = prove REWRITE_TAC[real_div; REAL_MUL_LZERO; REAL_ADD_RID] THEN ONCE_REWRITE_TAC[MULT_SYM] THEN ASM_SIMP_TAC[GSYM REAL_POW_POW; SQRT_POW_2; REAL_LT_IMP_LE]);; +Pb_printer.clear_file_tags();; diff --git a/100/platonic.ml b/100/platonic.ml index 5faf8e46..c7bfd108 100644 --- a/100/platonic.ml +++ b/100/platonic.ml @@ -2,8 +2,48 @@ (* The five Platonic solids exist and there are no others. *) (* ========================================================================= *) -needs "100/polyhedron.ml";; -needs "Multivariate/cross.ml";; +set_jrh_lexer;; +Pb_printer.set_file_tags ["Top100"; "platonic.ml"];; + +open Lib;; +open Fusion;; +open Basics;; +open Printer;; +open Parser;; +open Equal;; +open Bool;; +open Drule;; +open Tactics;; +open Simp;; +open Theorems;; +open Class;; +open Trivia;; +open Meson;; +open Pair;; +open Arith;; +open Calc_num;; +open Grobner;; +open Lists;; +open Realax;; +open Calc_int;; +open Realarith;; +open Reals;; +open Calc_rat;; +open Ints;; +open Sets;; +open Iterate;; +open Cart;; +open Wo;; +open Misc;; + +open Vectors;; +open Determinants;; +open Topology;; +open Convex;; +open Polytope;; + +open Polyhedron;; +open Cross;; prioritize_real();; @@ -2175,3 +2215,4 @@ let ICOSAHEDRON_CONGRUENT_FACETS = prove f2 face_of std_icosahedron /\ aff_dim f2 = &2 ==> f1 congruent f2`, CONGRUENT_FACES_TAC ICOSAHEDRON_FACETS);; +Pb_printer.clear_file_tags();; diff --git a/100/pnt.ml b/100/pnt.ml index b9f5e875..56c4f2fe 100644 --- a/100/pnt.ml +++ b/100/pnt.ml @@ -2,9 +2,55 @@ (* "Second proof" of Prime Number Theorem from Newman's book. *) (* ========================================================================= *) -needs "Multivariate/cauchy.ml";; -needs "Library/pocklington.ml";; -needs "Examples/mangoldt.ml";; +set_jrh_lexer;; +Pb_printer.set_file_tags ["Top100"; "pnt.ml"];; + +open Lib;; +open Fusion;; +open Parser;; +open Equal;; +open Bool;; +open Drule;; +open Tactics;; +open Simp;; +open Theorems;; +open Class;; +open Trivia;; +open Meson;; +open Pair;; +open Nums;; +open Arith;; +open Calc_num;; +open Realax;; +open Calc_int;; +open Realarith;; +open Reals;; +open Calc_rat;; +open Ints;; +open Sets;; +open Iterate;; +open Cart;; +open Wo;; +open Products;; +open Floor;; +open Misc;; + +open Metric;; +open Vectors;; +open Topology;; +open Convex;; +open Paths;; +open Derivatives;; +open Integration;; +open Complexes;; +open Canal;; +open Transcendentals;; +open Realanalysis;; + +open Cauchy;; +open Prime;; +open Pocklington;; +open Mangoldt;; prioritize_real();; prioritize_complex();; @@ -4314,3 +4360,4 @@ let PNT = prove ASM_SIMP_TAC[real_div; REAL_MUL_LID; REAL_SUB_LE; ARITH_RULE `&2 < x ==> &0 <= x`] THEN MATCH_MP_TAC REAL_LE_INV2 THEN ASM_REAL_ARITH_TAC);; +Pb_printer.clear_file_tags();; diff --git a/100/polyhedron.ml b/100/polyhedron.ml index b169e71f..c80db27d 100644 --- a/100/polyhedron.ml +++ b/100/polyhedron.ml @@ -2,10 +2,45 @@ (* Formalization of Jim Lawrence's proof of Euler's relation. *) (* ========================================================================= *) -needs "Multivariate/polytope.ml";; -needs "Library/binomial.ml";; -needs "100/inclusion_exclusion.ml";; -needs "100/combinations.ml";; +set_jrh_lexer;; +Pb_printer.set_file_tags ["Top100"; "polyhedron.ml"];; + +open Lib;; +open Fusion;; +open Basics;; +open Parser;; +open Equal;; +open Bool;; +open Drule;; +open Tactics;; +open Simp;; +open Theorems;; +open Class;; +open Trivia;; +open Meson;; +open Pair;; +open Arith;; +open Calc_num;; +open Realax;; +open Calc_int;; +open Realarith;; +open Reals;; +open Calc_rat;; +open Ints;; +open Sets;; +open Iterate;; +open Cart;; +open Wo;; +open Misc;; + +open Metric;; +open Vectors;; +open Topology;; +open Convex;; +open Polytope;; +open Binomial;; +open Inclusion_exclusion;; +open Combinations;; prioritize_real();; @@ -2203,3 +2238,4 @@ let EULER_RELATION = prove x + z = y + &2`] THEN REWRITE_TAC[REAL_OF_NUM_ADD; REAL_OF_NUM_EQ] THEN DISCH_THEN SUBST1_TAC THEN REWRITE_TAC[ADD_SUB2]]);; +Pb_printer.clear_file_tags();; diff --git a/100/primerecip.ml b/100/primerecip.ml index ea4727c2..a7269751 100644 --- a/100/primerecip.ml +++ b/100/primerecip.ml @@ -6,8 +6,65 @@ (* Now load other stuff needed. *) (* ------------------------------------------------------------------------- *) -needs "100/bertrand.ml";; -needs "100/divharmonic.ml";; +set_jrh_lexer;; +open System;; +open Lib;; +open Fusion;; +open Basics;; +open Nets;; +open Printer;; +open Preterm;; +open Parser;; +open Equal;; +open Bool;; +open Drule;; +open Log;; +open Import_proofs;; +open Tactics;; +open Itab;; +open Replay;; +open Simp;; +open Embryo_extra;; +open Theorems;; +open Ind_defs;; +open Class;; +open Trivia;; +open Canon;; +open Meson;; +open Metis;; +open Quot;; +open Impconv;; +open Pair;; +open Nums;; +open Recursion;; +open Arith;; +open Wf;; +open Calc_num;; +open Normalizer;; +open Grobner;; +open Ind_types;; +open Lists;; +open Realax;; +open Calc_int;; +open Realarith;; +open Reals;; +open Calc_rat;; +open Ints;; +open Sets;; +open Iterate;; +open Cart;; +open Define;; +open Help;; +open Wo;; + +open Floor;; +open Analysis;; +open Transc;; +open Prime;; +open Pocklington;; +open Calc_real;; +open Bertrand;; +open Divharmonic;; (* ------------------------------------------------------------------------- *) (* Variant of induction. *) diff --git a/100/ptolemy.ml b/100/ptolemy.ml index 7ecb9fcc..b9de2af9 100644 --- a/100/ptolemy.ml +++ b/100/ptolemy.ml @@ -2,7 +2,26 @@ (* Ptolemy's theorem. *) (* ========================================================================= *) -needs "Multivariate/transcendentals.ml";; +set_jrh_lexer;; +Pb_printer.set_file_tags ["Top100"; "ptolemy.ml"];; + +open Lib;; +open Fusion;; +open Basics;; +open Parser;; +open Equal;; +open Bool;; +open Drule;; +open Tactics;; +open Simp;; +open Realax;; +open Realarith;; +open Calc_rat;; +open Cart;; +open Misc;; + +open Vectors;; +open Transcendentals;; (* ------------------------------------------------------------------------- *) (* Some 2-vector special cases. *) @@ -67,3 +86,4 @@ let PTOLEMY = prove [`a / &2`; `b / &2`; `c / &2`; `d / &2`] THEN REWRITE_TAC[SIN_SUB; SIN_ADD; COS_ADD; SIN_PI; COS_PI] THEN CONV_TAC "100/ptolemy.ml:REAL_RING" REAL_RING);; +Pb_printer.clear_file_tags();; diff --git a/100/pythagoras.ml b/100/pythagoras.ml index 968f9f55..a3104ea6 100644 --- a/100/pythagoras.ml +++ b/100/pythagoras.ml @@ -3,8 +3,17 @@ (* implicit in the definition of "norm", but maybe this is still nontrivial. *) (* ========================================================================= *) -needs "Multivariate/misc.ml";; -needs "Multivariate/vectors.ml";; +set_jrh_lexer;; +Pb_printer.set_file_tags ["Top100"; "pythagoras.ml"];; + +open Parser;; +open Tactics;; +open Simp;; +open Calc_num;; +open Calc_rat;; +open Cart;; + +open Vectors;; (* ------------------------------------------------------------------------- *) (* Direct vector proof (could replace 2 by N and the proof still runs). *) @@ -28,3 +37,4 @@ let PYTHAGORAS = prove SIMP_TAC[NORM_POW_2; orthogonal; dot; SUM_2; DIMINDEX_2; VECTOR_SUB_COMPONENT; ARITH] THEN CONV_TAC "100/pythagoras.ml:REAL_RING" REAL_RING);; +Pb_printer.clear_file_tags();; diff --git a/100/quartic.ml b/100/quartic.ml index 6a892825..cadc7f3a 100644 --- a/100/quartic.ml +++ b/100/quartic.ml @@ -1,3 +1,14 @@ +set_jrh_lexer;; +Pb_printer.set_file_tags ["Top100"; "100/quartic.ml"];; + +open Parser;; +open Tactics;; +open Simp;; +open Class;; +open Realax;; +open Calc_rat;; + + prioritize_real();; (* ------------------------------------------------------------------------- *) @@ -200,3 +211,5 @@ let QUARTIC_CASES = prove x = --a / &4 - R / &2 + E / &2 \/ x = --a / &4 - R / &2 - E / &2)`, CONV_TAC "100/quartic.ml:REAL_FIELD" REAL_FIELD);; + +Pb_printer.clear_file_tags();; diff --git a/100/ramsey.ml b/100/ramsey.ml index abe0825b..b241ef7c 100644 --- a/100/ramsey.ml +++ b/100/ramsey.ml @@ -4,6 +4,31 @@ (* Port to HOL Light of a HOL88 proof done on 9th May 1994 *) (* ======================================================================== *) +set_jrh_lexer;; +Pb_printer.set_file_tags ["Top100"; "100/ramsey.ml"];; + +open Lib;; +open Fusion;; +open Basics;; +open Parser;; +open Equal;; +open Bool;; +open Drule;; +open Tactics;; +open Replay;; +open Simp;; +open Theorems;; +open Class;; +open Meson;; +open Nums;; +open Arith;; +open Calc_num;; +open Realax;; +open Ints;; +open Sets;; + +prioritize_num();; + (* ------------------------------------------------------------------------- *) (* HOL88 compatibility. *) (* ------------------------------------------------------------------------- *) @@ -1276,3 +1301,5 @@ let RAMSEY = prove( REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[SUBSET_REFL]; MAP_EVERY MATCH_MP_TAC [RAMSEY_LEMMA3; RAMSEY_LEMMA2; RAMSEY_LEMMA1] THEN POP_ASSUM MATCH_ACCEPT_TAC]);; + +Pb_printer.clear_file_tags();; diff --git a/100/ratcountable.ml b/100/ratcountable.ml index 8469d623..989518d1 100644 --- a/100/ratcountable.ml +++ b/100/ratcountable.ml @@ -2,7 +2,23 @@ (* Theorem 3: countability of rational numbers. *) (* ========================================================================= *) -needs "Library/card.ml";; +set_jrh_lexer;; +Pb_printer.set_file_tags ["Top100"; "ratcountable.ml"];; + +open Parser;; +open Equal;; +open Tactics;; +open Simp;; +open Theorems;; +open Meson;; +open Pair;; +open Calc_num;; +open Realax;; +open Calc_int;; +open Reals;; +open Calc_rat;; +open Sets;; +open Card;; prioritize_real();; @@ -10,8 +26,8 @@ prioritize_real();; (* Definition of rational and countable. *) (* ------------------------------------------------------------------------- *) -let rational = new_definition - `rational(r) <=> ?p q. ~(q = 0) /\ (abs(r) = &p / &q)`;; +let ratcountable_rational = new_definition + `ratcountable_rational(r) <=> ?p q. ~(q = 0) /\ (abs(r) = &p / &q)`;; let countable = new_definition `countable s <=> s <=_c (UNIV:num->bool)`;; @@ -21,14 +37,14 @@ let countable = new_definition (* ------------------------------------------------------------------------- *) let COUNTABLE_RATIONALS = prove - (`countable { x:real | rational(x)}`, + (`countable { x:real | ratcountable_rational(x)}`, REWRITE_TAC[countable] THEN TRANS_TAC CARD_LE_TRANS `{ x:real | ?p q. x = &p / &q } *_c (UNIV:num->bool)` THEN CONJ_TAC THENL [REWRITE_TAC[LE_C; EXISTS_PAIR_THM; mul_c] THEN EXISTS_TAC `\(x,b). if b = 0 then x else --x` THEN CONV_TAC "100/ratcountable.ml:(ONCE_DEPTH_CONV GEN_BETA_CONV)" (ONCE_DEPTH_CONV GEN_BETA_CONV) THEN - REWRITE_TAC[IN_ELIM_THM; rational; IN_UNIV; PAIR_EQ] THEN + REWRITE_TAC[IN_ELIM_THM; ratcountable_rational; IN_UNIV; PAIR_EQ] THEN MESON_TAC[REAL_ARITH `(abs(x) = a) ==> (x = a) \/ x = --a`]; ALL_TAC] THEN MATCH_MP_TAC CARD_MUL_ABSORB_LE THEN REWRITE_TAC[num_INFINITE] THEN @@ -36,7 +52,7 @@ let COUNTABLE_RATIONALS = prove [REWRITE_TAC[LE_C; EXISTS_PAIR_THM; mul_c; IN_UNIV] THEN EXISTS_TAC `\(p,q). &p / &q` THEN CONV_TAC "100/ratcountable.ml:(ONCE_DEPTH_CONV GEN_BETA_CONV)" (ONCE_DEPTH_CONV GEN_BETA_CONV) THEN - REWRITE_TAC[IN_ELIM_THM; rational] THEN MESON_TAC[]; + REWRITE_TAC[IN_ELIM_THM; ratcountable_rational] THEN MESON_TAC[]; MESON_TAC[CARD_MUL_ABSORB_LE; CARD_LE_REFL; num_INFINITE]]);; (* ------------------------------------------------------------------------- *) @@ -47,11 +63,11 @@ let denumerable = new_definition `denumerable s <=> s =_c (UNIV:num->bool)`;; let DENUMERABLE_RATIONALS = prove - (`denumerable { x:real | rational(x)}`, + (`denumerable { x:real | ratcountable_rational(x)}`, REWRITE_TAC[denumerable; GSYM CARD_LE_ANTISYM] THEN REWRITE_TAC[GSYM countable; COUNTABLE_RATIONALS] THEN REWRITE_TAC[le_c] THEN EXISTS_TAC `&` THEN - SIMP_TAC[IN_ELIM_THM; IN_UNIV; REAL_OF_NUM_EQ; rational] THEN + SIMP_TAC[IN_ELIM_THM; IN_UNIV; REAL_OF_NUM_EQ; ratcountable_rational] THEN X_GEN_TAC `p:num` THEN MAP_EVERY EXISTS_TAC [`p:num`; `1`] THEN REWRITE_TAC[REAL_DIV_1; REAL_ABS_NUM; ARITH_EQ]);; @@ -60,9 +76,10 @@ let DENUMERABLE_RATIONALS = prove (* ------------------------------------------------------------------------- *) let DENUMERABLE_RATIONALS_EXPAND = prove - (`?rat:num->real. (!n. rational(rat n)) /\ - (!x. rational x ==> ?!n. x = rat n)`, + (`?rat:num->real. (!n. ratcountable_rational(rat n)) /\ + (!x. ratcountable_rational x ==> ?!n. x = rat n)`, MP_TAC DENUMERABLE_RATIONALS THEN REWRITE_TAC[denumerable] THEN ONCE_REWRITE_TAC[CARD_EQ_SYM] THEN REWRITE_TAC[eq_c] THEN REWRITE_TAC[IN_UNIV; IN_ELIM_THM] THEN MATCH_MP_TAC MONO_EXISTS THEN MESON_TAC[]);; +Pb_printer.clear_file_tags();; diff --git a/100/realsuncountable.ml b/100/realsuncountable.ml index e2d1fcb4..2fea4f0c 100644 --- a/100/realsuncountable.ml +++ b/100/realsuncountable.ml @@ -2,7 +2,36 @@ (* #22: non-denumerability of continuum (= uncountability of the reals). *) (* ========================================================================= *) -needs "Library/card.ml";; +set_jrh_lexer;; +Pb_printer.set_file_tags ["Top100"; "realsuncountable.ml"];; + +open Lib;; +open Fusion;; +open Parser;; +open Equal;; +open Bool;; +open Drule;; +open Tactics;; +open Simp;; +open Theorems;; +open Class;; +open Meson;; +open Pair;; +open Nums;; +open Arith;; +open Calc_num;; +open Realax;; +open Calc_int;; +open Realarith;; +open Reals;; +open Calc_rat;; +open Ints;; +open Sets;; +open Iterate;; + +open Card;; + +open Analysis;; prioritize_real();; @@ -122,8 +151,6 @@ let UNCOUNTABLE_CANONICAL = prove (* Injection of canonical digits into the reals. *) (* ------------------------------------------------------------------------- *) -needs "Library/analysis.ml";; - prioritize_real();; let SUM_BINSEQUENCE_LBOUND = prove @@ -254,3 +281,4 @@ let UNCOUNTABLE_REALS = prove [MATCH_MP_TAC(REAL_ARITH `b < a ==> a = b ==> F`); MATCH_MP_TAC(REAL_ARITH `a < b ==> a = b ==> F`)] THEN MATCH_MP_TAC SUMINF_INJ_LEMMA THEN ASM_MESON_TAC[]);; +Pb_printer.clear_file_tags();; diff --git a/100/reciprocity.ml b/100/reciprocity.ml index 242579a1..cf41228c 100644 --- a/100/reciprocity.ml +++ b/100/reciprocity.ml @@ -2,8 +2,67 @@ (* Quadratic reciprocity. *) (* ========================================================================= *) -needs "Library/prime.ml";; -needs "Library/pocklington.ml";; +set_jrh_lexer;; +open System;; +open Lib;; +open Fusion;; +open Basics;; +open Nets;; +open Printer;; +open Preterm;; +open Parser;; +open Equal;; +open Bool;; +open Drule;; +open Log;; +open Import_proofs;; +open Tactics;; +open Itab;; +open Replay;; +open Simp;; +open Embryo_extra;; +open Theorems;; +open Ind_defs;; +open Class;; +open Trivia;; +open Canon;; +open Meson;; +open Metis;; +open Quot;; +open Impconv;; +open Pair;; +open Nums;; +open Recursion;; +open Arith;; +open Wf;; +open Calc_num;; +open Normalizer;; +open Grobner;; +open Ind_types;; +open Lists;; +open Realax;; +open Calc_int;; +open Realarith;; +open Reals;; +open Calc_rat;; +open Ints;; +open Sets;; +open Iterate;; +open Cart;; +open Define;; +open Help;; +open Wo;; +open Binary;; +open Card;; +open Permutations;; +open Products;; +open Floor;; +open Misc;; +open Iter;; +open Vectors;; + +open Prime;; +open Pocklington;; prioritize_num();; diff --git a/100/sqrt.ml b/100/sqrt.ml index c282b2dc..f7bc2a05 100644 --- a/100/sqrt.ml +++ b/100/sqrt.ml @@ -2,9 +2,28 @@ (* Irrationality of sqrt(2) and more general results. *) (* ========================================================================= *) -needs "Library/prime.ml";; (* For number-theoretic lemmas *) -needs "Library/floor.ml";; (* For definition of rationals *) -needs "Multivariate/vectors.ml";; (* For square roots *) +set_jrh_lexer;; +Pb_printer.set_file_tags ["Top100"; "sqrt.ml"];; + +open Lib;; +open Parser;; +open Equal;; +open Drule;; +open Tactics;; +open Simp;; +open Class;; +open Meson;; +open Calc_num;; +open Realax;; +open Calc_int;; +open Realarith;; +open Reals;; +open Calc_rat;; +open Ints;; +open Floor;; + +open Vectors;; +open Prime;; (* ------------------------------------------------------------------------- *) (* Most general irrationality of square root result. *) @@ -40,3 +59,4 @@ let IRRATIONAL_SQRT_PRIME = prove let IRRATIONAL_SQRT_2 = prove (`~rational(sqrt(&2))`, SIMP_TAC[IRRATIONAL_SQRT_PRIME; PRIME_2]);; +Pb_printer.clear_file_tags();; diff --git a/100/stirling.ml b/100/stirling.ml index 22869174..3d5b202e 100644 --- a/100/stirling.ml +++ b/100/stirling.ml @@ -2,8 +2,34 @@ (* Stirling's approximation. *) (* ========================================================================= *) -needs "Library/analysis.ml";; -needs "Library/transc.ml";; +set_jrh_lexer;; +Pb_printer.set_file_tags ["Top100"; "stirling.ml"];; + +open Lib;; +open Fusion;; +open Preterm;; +open Parser;; +open Equal;; +open Bool;; +open Drule;; +open Tactics;; +open Simp;; +open Theorems;; +open Class;; +open Meson;; +open Pair;; +open Nums;; +open Arith;; +open Calc_num;; +open Realax;; +open Calc_int;; +open Realarith;; +open Reals;; +open Calc_rat;; +open Ints;; + +open Analysis;; +open Transc;; override_interface("-->",`(tends_num_real)`);; @@ -595,3 +621,4 @@ let STIRLING = prove REWRITE_TAC[] THEN ONCE_REWRITE_TAC[SEQ_SUC] THEN SIMP_TAC[real_div; REAL_MUL_LID; REAL_MUL_ASSOC; REAL_MUL_LINV; REAL_MUL_RID; REAL_OF_NUM_EQ; NOT_SUC]);; +Pb_printer.clear_file_tags();; diff --git a/100/subsequence.ml b/100/subsequence.ml index c95f1af9..7e166b48 100644 --- a/100/subsequence.ml +++ b/100/subsequence.ml @@ -2,9 +2,34 @@ (* #73: Erdos-Szekeres theorem on ascending / descending subsequences. *) (* ========================================================================= *) +set_jrh_lexer;; +Pb_printer.set_file_tags ["Top100"; "100/subsequence.ml"];; + +open Lib;; +open Fusion;; +open Basics;; +open Parser;; +open Equal;; +open Bool;; +open Tactics;; +open Simp;; +open Theorems;; +open Class;; +open Meson;; +open Arith;; +open Calc_num;; +open Realax;; +open Realarith;; +open Ints;; +open Sets;; +open Iterate;; +open Define;; + + + let lemma = prove (`!f s. s = UNIONS (IMAGE (\a. {x | x IN s /\ f(x) = a}) (IMAGE f s))`, - REPEAT GEN_TAC THEN GEN_REWRITE_TAC "100/subsequence.ml:I" I [EXTENSION] THEN GEN_TAC THEN + REPEAT GEN_TAC THEN GEN_REWRITE_TAC "100/subsequence.ml:I" I [EXTENSION] THEN GEN_TAC THEN REWRITE_TAC[IN_UNIONS; IN_ELIM_THM; IN_IMAGE] THEN REWRITE_TAC[LEFT_AND_EXISTS_THM] THEN GEN_REWRITE_TAC "100/subsequence.ml:RAND_CONV" RAND_CONV [SWAP_EXISTS_THM] THEN @@ -15,11 +40,11 @@ let lemma = prove (* ------------------------------------------------------------------------- *) let PIGEONHOLE_LEMMA = prove - (`!f:A->B s n. + (`!f:A->B s n. FINITE s /\ (n - 1) * CARD(IMAGE f s) < CARD s ==> ?t a. t SUBSET s /\ t HAS_SIZE n /\ (!x. x IN t ==> f(x) = a)`, REPEAT GEN_TAC THEN DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN - MP_TAC(ISPECL [`f:A->B`; `s:A->bool`] lemma) THEN DISCH_THEN(fun th -> + MP_TAC(ISPECL [`f:A->B`; `s:A->bool`] lemma) THEN DISCH_THEN(fun th -> GEN_REWRITE_TAC "100/subsequence.ml:(LAND_CONV o funpow 2 RAND_CONV)" (LAND_CONV o funpow 2 RAND_CONV) [th]) THEN ONCE_REWRITE_TAC[GSYM CONTRAPOS_THM] THEN REWRITE_TAC[NOT_LT] THEN STRIP_TAC THEN GEN_REWRITE_TAC "100/subsequence.ml:RAND_CONV" RAND_CONV [MULT_SYM] THEN MATCH_MP_TAC @@ -42,7 +67,7 @@ let PIGEONHOLE_LEMMA = prove (* ------------------------------------------------------------------------- *) let mono_on = define - `mono_on (f:num->real) r s <=> + `mono_on (f:num->real) r s <=> !i j. i IN s /\ j IN s /\ i <= j ==> r (f i) (f j)`;; let MONO_ON_SUBSET = prove @@ -60,7 +85,7 @@ let ERDOS_SZEKERES = prove REPEAT STRIP_TAC THEN SUBGOAL_THEN `!i. i IN (1..m*n+1) - ==> ?k. (?s. s SUBSET (1..m*n+1) /\ s HAS_SIZE k /\ + ==> ?k. (?s. s SUBSET (1..m*n+1) /\ s HAS_SIZE k /\ mono_on f (<=) s /\ i IN s /\ (!j. j IN s ==> i <= j)) /\ (!l. (?s. s SUBSET (1..m*n+1) /\ s HAS_SIZE l /\ mono_on f (<=) s /\ i IN s /\ (!j. j IN s ==> i <= j)) @@ -100,25 +125,25 @@ let ERDOS_SZEKERES = prove MP_TAC THENL [MATCH_MP_TAC PIGEONHOLE_LEMMA THEN REWRITE_TAC[FINITE_NUMSEG; CARD_NUMSEG_1; ADD_SUB] THEN - MATCH_MP_TAC LET_TRANS THEN EXISTS_TAC `n * CARD(1..m)` THEN + MATCH_MP_TAC LET_TRANS THEN EXISTS_TAC `n * CARD(1..m)` THEN CONJ_TAC THENL [ALL_TAC; REWRITE_TAC[CARD_NUMSEG_1] THEN ARITH_TAC] THEN - REWRITE_TAC[LE_MULT_LCANCEL] THEN DISJ2_TAC THEN + REWRITE_TAC[LE_MULT_LCANCEL] THEN DISJ2_TAC THEN MATCH_MP_TAC CARD_SUBSET THEN REWRITE_TAC[FINITE_NUMSEG] THEN ASM_REWRITE_TAC[SUBSET; FORALL_IN_IMAGE] THEN ASM_MESON_TAC[IN_NUMSEG]; ALL_TAC] THEN MATCH_MP_TAC MONO_EXISTS THEN X_GEN_TAC `u:num->bool` THEN - DISCH_THEN(X_CHOOSE_THEN `k:num` STRIP_ASSUME_TAC) THEN + DISCH_THEN(X_CHOOSE_THEN `k:num` STRIP_ASSUME_TAC) THEN ASM_REWRITE_TAC[mono_on] THEN MAP_EVERY X_GEN_TAC [`i:num`; `j:num`] THEN - REWRITE_TAC[LE_LT; real_ge] THEN STRIP_TAC THEN + REWRITE_TAC[LE_LT; real_ge] THEN STRIP_TAC THEN ASM_REWRITE_TAC[REAL_LE_REFL] THEN - REMOVE_THEN "*" (fun th -> + REMOVE_THEN "*" (fun th -> MP_TAC(SPEC `i:num` th) THEN MP_TAC(SPEC `j:num` th)) THEN ANTS_TAC THENL [ASM_MESON_TAC[SUBSET]; ALL_TAC] THEN DISCH_THEN(X_CHOOSE_THEN `s:num->bool` STRIP_ASSUME_TAC o CONJUNCT1) THEN ANTS_TAC THENL [ASM_MESON_TAC[SUBSET]; ALL_TAC] THEN DISCH_THEN(MP_TAC o SPEC `k + 1` o CONJUNCT2) THEN ASM_SIMP_TAC[ARITH_RULE `~(k + 1 <= k)`; GSYM REAL_NOT_LT] THEN - REWRITE_TAC[CONTRAPOS_THM] THEN + REWRITE_TAC[CONTRAPOS_THM] THEN DISCH_TAC THEN EXISTS_TAC `(i:num) INSERT s` THEN REPEAT CONJ_TAC THENL [ASM SET_TAC[]; REWRITE_TAC[HAS_SIZE_CLAUSES; GSYM ADD1] THEN ASM_MESON_TAC[NOT_LT]; @@ -129,3 +154,5 @@ let ERDOS_SZEKERES = prove REWRITE_TAC[mono_on; IN_INSERT] THEN ASM_MESON_TAC[REAL_LE_REFL; REAL_LE_TRANS; REAL_LT_IMP_LE; NOT_LE; LT_REFL; LE_TRANS]);; + +Pb_printer.clear_file_tags();; diff --git a/100/thales.ml b/100/thales.ml index 9eccc50f..a577e3ee 100644 --- a/100/thales.ml +++ b/100/thales.ml @@ -2,7 +2,67 @@ (* Thales's theorem. *) (* ========================================================================= *) -needs "Multivariate/convex.ml";; +set_jrh_lexer;; +open System;; +open Lib;; +open Fusion;; +open Basics;; +open Nets;; +open Printer;; +open Preterm;; +open Parser;; +open Equal;; +open Bool;; +open Drule;; +open Log;; +open Import_proofs;; +open Tactics;; +open Itab;; +open Replay;; +open Simp;; +open Embryo_extra;; +open Theorems;; +open Ind_defs;; +open Class;; +open Trivia;; +open Canon;; +open Meson;; +open Metis;; +open Quot;; +open Impconv;; +open Pair;; +open Nums;; +open Recursion;; +open Arith;; +open Wf;; +open Calc_num;; +open Normalizer;; +open Grobner;; +open Ind_types;; +open Lists;; +open Realax;; +open Calc_int;; +open Realarith;; +open Reals;; +open Calc_rat;; +open Ints;; +open Sets;; +open Iterate;; +open Cart;; +open Define;; +open Help;; +open Wo;; +open Binary;; +open Card;; +open Permutations;; +open Products;; +open Floor;; +open Misc;; +open Iter;; + +open Vectors;; +open Convex;; +open Sos;; prioritize_real();; @@ -48,7 +108,7 @@ let THALES = prove (* But for another natural version, we need to use the reals. *) (* ------------------------------------------------------------------------- *) -needs "Examples/sos.ml";; +(* "Examples/sos.ml" already loaded *) (* ------------------------------------------------------------------------- *) (* The following, which we need as a lemma, needs the reals specifically. *) diff --git a/100/triangular.ml b/100/triangular.ml index d9068149..bed254f4 100644 --- a/100/triangular.ml +++ b/100/triangular.ml @@ -2,7 +2,64 @@ (* Sum of reciprocals of triangular numbers. *) (* ========================================================================= *) -needs "Multivariate/misc.ml";; (*** Just for REAL_ARCH_INV! ***) +set_jrh_lexer;; +open System;; +open Lib;; +open Fusion;; +open Basics;; +open Nets;; +open Printer;; +open Preterm;; +open Parser;; +open Equal;; +open Bool;; +open Drule;; +open Log;; +open Import_proofs;; +open Tactics;; +open Itab;; +open Replay;; +open Simp;; +open Embryo_extra;; +open Theorems;; +open Ind_defs;; +open Class;; +open Trivia;; +open Canon;; +open Meson;; +open Metis;; +open Quot;; +open Impconv;; +open Pair;; +open Nums;; +open Recursion;; +open Arith;; +open Wf;; +open Calc_num;; +open Normalizer;; +open Grobner;; +open Ind_types;; +open Lists;; +open Realax;; +open Calc_int;; +open Realarith;; +open Reals;; +open Calc_rat;; +open Ints;; +open Sets;; +open Iterate;; +open Cart;; +open Define;; +open Help;; + +open Analysis;; + +(* Misc not compatible with Analysis *) +(* +open Misc;; +*) + +(*** "Multivariate/misc.ml" Just for REAL_ARCH_INV! ***) prioritize_real();; @@ -61,8 +118,6 @@ let TRIANGLE_CONVERGES = prove (* In terms of limits. *) (* ------------------------------------------------------------------------- *) -needs "Library/analysis.ml";; - override_interface ("-->",`(tends_num_real)`);; let TRIANGLE_CONVERGES' = prove diff --git a/100/two_squares.ml b/100/two_squares.ml index 2c05435a..8576cac8 100644 --- a/100/two_squares.ml +++ b/100/two_squares.ml @@ -2,7 +2,27 @@ (* Representation of primes == 1 (mod 4) as sum of 2 squares. *) (* ========================================================================= *) -needs "Library/prime.ml";; +set_jrh_lexer;; +Pb_printer.set_file_tags ["Top100"; "two_squares.ml"];; + +open Lib;; +open Parser;; +open Equal;; +open Bool;; +open Drule;; +open Tactics;; +open Simp;; +open Theorems;; +open Class;; +open Meson;; +open Pair;; +open Arith;; +open Calc_num;; +open Realax;; +open Ints;; +open Sets;; + +open Prime;; prioritize_num();; @@ -261,3 +281,4 @@ let SUM_OF_TWO_SQUARES = prove ASM_REWRITE_TAC[MULT_CLAUSES; ADD_CLAUSES] THEN ASM_CASES_TAC `x = 1` THEN ASM_REWRITE_TAC[] THEN REWRITE_TAC[MULT_CLAUSES] THEN ARITH_TAC]]);; +Pb_printer.clear_file_tags();; diff --git a/100/wilson.ml b/100/wilson.ml index 986b798a..01350efd 100644 --- a/100/wilson.ml +++ b/100/wilson.ml @@ -2,8 +2,31 @@ (* Wilson's theorem. *) (* ========================================================================= *) -needs "Library/prime.ml";; -needs "Library/pocklington.ml";; +set_jrh_lexer;; +Pb_printer.set_file_tags ["Top100"; "wilson.ml"];; + +open Lib;; +open Fusion;; +open Parser;; +open Equal;; +open Bool;; +open Drule;; +open Tactics;; +open Simp;; +open Theorems;; +open Class;; +open Meson;; +open Pair;; +open Nums;; +open Arith;; +open Calc_num;; +open Realax;; +open Ints;; +open Sets;; +open Iterate;; + +open Prime;; +open Pocklington;; prioritize_num();; @@ -11,14 +34,14 @@ prioritize_num();; (* Definition of iterated product. *) (* ------------------------------------------------------------------------- *) -let product = new_definition `product = iterate ( * )`;; +let iterated_product = new_definition `iterated_product = iterate ( * )`;; let PRODUCT_CLAUSES = prove - (`(!f. product {} f = 1) /\ + (`(!f. iterated_product {} f = 1) /\ (!x f s. FINITE(s) - ==> (product (x INSERT s) f = - if x IN s then product s f else f(x) * product s f))`, - REWRITE_TAC[product; GSYM NEUTRAL_MUL] THEN + ==> (iterated_product (x INSERT s) f = + if x IN s then iterated_product s f else f(x) * iterated_product s f))`, + REWRITE_TAC[iterated_product; GSYM NEUTRAL_MUL] THEN ONCE_REWRITE_TAC[SWAP_FORALL_THM] THEN MATCH_MP_TAC ITERATE_CLAUSES THEN REWRITE_TAC[MONOIDAL_MUL]);; @@ -27,14 +50,14 @@ let PRODUCT_CLAUSES = prove (* ------------------------------------------------------------------------- *) let FACT_PRODUCT = prove - (`!n. FACT(n) = product(1..n) (\i. i)`, + (`!n. FACT(n) = iterated_product(1..n) (\i. i)`, INDUCT_TAC THEN REWRITE_TAC[FACT; NUMSEG_CLAUSES; ARITH; PRODUCT_CLAUSES] THEN ASM_SIMP_TAC[ARITH_RULE `1 <= SUC n`; PRODUCT_CLAUSES; FINITE_NUMSEG] THEN REWRITE_TAC[IN_NUMSEG] THEN ARITH_TAC);; let FACT_PRODUCT_ALT = prove - (`!n. FACT(n) = product(2..n) (\i. i)`, + (`!n. FACT(n) = iterated_product(2..n) (\i. i)`, GEN_TAC THEN REWRITE_TAC[FACT_PRODUCT] THEN DISJ_CASES_TAC(ARITH_RULE `n = 0 \/ 1 <= n`) THEN ASM_REWRITE_TAC[num_CONV `1`; NUMSEG_CLAUSES] THEN @@ -51,7 +74,7 @@ let PRODUCT_PAIRUP_INDUCT = prove (`!f r n s. FINITE s /\ CARD s = n /\ (!x:A. x IN s ==> ?!y. y IN s /\ ~(y = x) /\ (f(x) * f(y) == 1) (mod r)) - ==> (product s f == 1) (mod r)`, + ==> (iterated_product s f == 1) (mod r)`, GEN_TAC THEN GEN_TAC THEN MATCH_MP_TAC num_WF THEN X_GEN_TAC `n:num` THEN DISCH_TAC THEN X_GEN_TAC `s:A->bool` THEN ASM_CASES_TAC `s:A->bool = {}` THEN @@ -94,7 +117,7 @@ let PRODUCT_PAIRUP = prove (`!f r s. FINITE s /\ (!x:A. x IN s ==> ?!y. y IN s /\ ~(y = x) /\ (f(x) * f(y) == 1) (mod r)) - ==> (product s f == 1) (mod r)`, + ==> (iterated_product s f == 1) (mod r)`, REPEAT STRIP_TAC THEN MATCH_MP_TAC PRODUCT_PAIRUP_INDUCT THEN EXISTS_TAC `CARD(s:A->bool)` THEN ASM_REWRITE_TAC[]);; @@ -198,3 +221,4 @@ let WILSON_EQ = prove [MATCH_MP_TAC DIVIDES_ADD_REVR THEN EXISTS_TAC `n - 1` THEN ASM_SIMP_TAC[ARITH_RULE `~(n = 0) ==> n - 1 + 1 = n`]; REWRITE_TAC[DIVIDES_ONE] THEN ASM_MESON_TAC[PRIME_1]]);; +Pb_printer.clear_file_tags();; diff --git a/Complex/complex_transc.ml b/Complex/complex_transc.ml index 52ebe626..d4fc798b 100644 --- a/Complex/complex_transc.ml +++ b/Complex/complex_transc.ml @@ -2,9 +2,60 @@ (* Complex transcendental functions. *) (* ========================================================================= *) -needs "Library/transc.ml";; -needs "Library/floor.ml";; -needs "Complex/complexnumbers.ml";; + +set_jrh_lexer;; +open System;; +open Lib;; +open Fusion;; +open Basics;; +open Nets;; +open Printer;; +open Preterm;; +open Parser;; +open Equal;; +open Bool;; +open Drule;; +open Log;; +open Import_proofs;; +open Tactics;; +open Itab;; +open Replay;; +open Simp;; +open Embryo_extra;; +open Theorems;; +open Ind_defs;; +open Class;; +open Trivia;; +open Canon;; +open Meson;; +open Metis;; +open Quot;; +open Impconv;; +open Pair;; +open Nums;; +open Recursion;; +open Arith;; +open Wf;; +open Calc_num;; +open Normalizer;; +open Grobner;; +open Ind_types;; +open Lists;; +open Realax;; +open Calc_int;; +open Realarith;; +open Reals;; +open Calc_rat;; +open Ints;; +open Sets;; +open Iterate;; +open Cart;; +open Define;; +open Help;; + +open Transc;; +open Floor;; +open Complexnumbers;; unparse_as_infix "exp";; remove_interface "exp";; diff --git a/Complex/complexnumbers.ml b/Complex/complexnumbers.ml index 0f5e0b8f..add71599 100644 --- a/Complex/complexnumbers.ml +++ b/Complex/complexnumbers.ml @@ -2,7 +2,57 @@ (* Basic definitions and properties of complex numbers. *) (* ========================================================================= *) -needs "Library/transc.ml";; +set_jrh_lexer;; +open System;; +open Lib;; +open Fusion;; +open Basics;; +open Nets;; +open Printer;; +open Preterm;; +open Parser;; +open Equal;; +open Bool;; +open Drule;; +open Log;; +open Import_proofs;; +open Tactics;; +open Itab;; +open Replay;; +open Simp;; +open Embryo_extra;; +open Theorems;; +open Ind_defs;; +open Class;; +open Trivia;; +open Canon;; +open Meson;; +open Metis;; +open Quot;; +open Impconv;; +open Pair;; +open Nums;; +open Recursion;; +open Arith;; +open Wf;; +open Calc_num;; +open Normalizer;; +open Grobner;; +open Ind_types;; +open Lists;; +open Realax;; +open Calc_int;; +open Realarith;; +open Reals;; +open Calc_rat;; +open Ints;; +open Sets;; +open Iterate;; +open Cart;; +open Define;; +open Help;; + +open Transc;; prioritize_real();; diff --git a/Examples/machin.ml b/Examples/machin.ml index 4b5fddd5..9b3dd214 100644 --- a/Examples/machin.ml +++ b/Examples/machin.ml @@ -2,7 +2,58 @@ (* Derivation of Machin's formula and other similar ones. *) (* ========================================================================= *) -needs "Library/transc.ml";; +set_jrh_lexer;; +open System;; +open Lib;; +open Fusion;; +open Basics;; +open Nets;; +open Printer;; +open Preterm;; +open Parser;; +open Equal;; +open Bool;; +open Drule;; +open Log;; +open Import_proofs;; +open Tactics;; +open Itab;; +open Replay;; +open Simp;; +open Embryo_extra;; +open Theorems;; +open Ind_defs;; +open Class;; +open Trivia;; +open Canon;; +open Meson;; +open Metis;; +open Quot;; +open Impconv;; +open Pair;; +open Nums;; +open Recursion;; +open Arith;; +open Wf;; +open Calc_num;; +open Normalizer;; +open Grobner;; +open Ind_types;; +open Lists;; +open Realax;; +open Calc_int;; +open Realarith;; +open Reals;; +open Calc_rat;; +open Ints;; +open Sets;; +open Iterate;; +open Cart;; +open Define;; +open Help;; + +open Analysis;; +open Transc;; let REAL_LE_1_POW2 = prove (`!n. &1 <= &2 pow n`, diff --git a/Examples/mangoldt.ml b/Examples/mangoldt.ml index 9a5f9c7b..ef3a89bf 100644 --- a/Examples/mangoldt.ml +++ b/Examples/mangoldt.ml @@ -2,8 +2,89 @@ (* Mangoldt function and elementary Chebyshev/Mertens results. *) (* ========================================================================= *) -needs "Library/pocklington.ml";; -needs "Multivariate/transcendentals.ml";; +set_jrh_lexer;; +open System;; +open Lib;; +open Fusion;; +open Basics;; +open Nets;; +open Printer;; +open Preterm;; +open Parser;; +open Equal;; +open Bool;; +open Drule;; +open Log;; +open Import_proofs;; +open Tactics;; +open Itab;; +open Replay;; +open Simp;; +open Embryo_extra;; +open Theorems;; +open Ind_defs;; +open Class;; +open Trivia;; +open Canon;; +open Meson;; +open Metis;; +open Quot;; +open Impconv;; +open Pair;; +open Nums;; +open Recursion;; +open Arith;; +open Wf;; +open Calc_num;; +open Normalizer;; +open Grobner;; +open Ind_types;; +open Lists;; +open Realax;; +open Calc_int;; +open Realarith;; +open Reals;; +open Calc_rat;; +open Ints;; +open Sets;; +open Iterate;; +open Cart;; +open Define;; +open Help;; +open Wo;; +open Binary;; +open Card;; +open Permutations;; +open Products;; +open Floor;; +open Misc;; +open Iter;; +open Vectors;; +open Determinants;; +open Topology;; +open Convex;; +open Paths;; +open Polytope;; +open Degree;; +open Derivatives;; +open Clifford;; +open Integration;; +open Measure;; + +open Binomial;; +open Complexes;; +open Canal;; +open Transcendentals;; +open Realanalysis;; +open Moretop;; +open Cauchy;; + +open Prime;; +open Pocklington;; + +open Transcendentals;; + + prioritize_real();; diff --git a/Examples/sos.ml b/Examples/sos.ml index 776fb587..87b63144 100644 --- a/Examples/sos.ml +++ b/Examples/sos.ml @@ -24,7 +24,6 @@ open Realarith;; open Reals;; open Calc_rat;; open Ints;; -open Analysis;; prioritize_real();; diff --git a/Library/agm.ml b/Library/agm.ml index 9b6a16ff..55e7df15 100644 --- a/Library/agm.ml +++ b/Library/agm.ml @@ -2,7 +2,73 @@ (* Arithmetic-geometric mean inequality. *) (* ========================================================================= *) -needs "Library/products.ml";; +set_jrh_lexer;; +open System;; +open Lib;; +open Fusion;; +open Basics;; +open Nets;; +open Printer;; +open Preterm;; +open Parser;; +open Equal;; +open Bool;; +open Drule;; +open Log;; +open Import_proofs;; +open Tactics;; +open Itab;; +open Replay;; +open Simp;; +open Embryo_extra;; +open Theorems;; +open Ind_defs;; +open Class;; +open Trivia;; +open Canon;; +open Meson;; +open Metis;; +open Quot;; +open Impconv;; +open Pair;; +open Nums;; +open Recursion;; +open Arith;; +open Wf;; +open Calc_num;; +open Normalizer;; +open Grobner;; +open Ind_types;; +open Lists;; +open Realax;; +open Calc_int;; +open Realarith;; +open Reals;; +open Calc_rat;; +open Ints;; +open Sets;; +open Iterate;; +open Cart;; +open Define;; +open Help;; +open Wo;; + +(* Removed for analysis deps *) +(* +open Binary;; +open Card;; +open Permutations;; +*) + +open Products;; + +(* +open Floor;; +open Misc;; +*) + +open Iter;; + prioritize_real();; diff --git a/Library/analysis.ml b/Library/analysis.ml index 4d7c041b..8b458f5c 100644 --- a/Library/analysis.ml +++ b/Library/analysis.ml @@ -1859,6 +1859,9 @@ let sum_EXISTS = prove let sum_DEF = new_specification ["psum"] sum_EXISTS;; +(* sum will be overwritten, but e_is_transcendental still needs the old one. *) +let OLD_SUM = sum;; + let sum = prove (`(sum(n,0) f = &0) /\ (sum(n,SUC m) f = sum(n,m) f + f(n + m))`, diff --git a/Library/calc_real.ml b/Library/calc_real.ml index db371447..6bd22cb8 100644 --- a/Library/calc_real.ml +++ b/Library/calc_real.ml @@ -2,7 +2,59 @@ (* Calculation with real numbers (Boehm-style but by inference). *) (* ========================================================================= *) -needs "Library/transc.ml";; +set_jrh_lexer;; +open System;; +open Lib;; +open Fusion;; +open Basics;; +open Nets;; +open Printer;; +open Preterm;; +open Parser;; +open Equal;; +open Bool;; +open Drule;; +open Log;; +open Import_proofs;; +open Tactics;; +open Itab;; +open Replay;; +open Simp;; +open Embryo_extra;; +open Theorems;; +open Ind_defs;; +open Class;; +open Trivia;; +open Canon;; +open Meson;; +open Metis;; +open Quot;; +open Impconv;; +open Pair;; +open Nums;; +open Recursion;; +open Arith;; +open Wf;; +open Calc_num;; +open Normalizer;; +open Grobner;; +open Ind_types;; +open Lists;; +open Realax;; +open Calc_int;; +open Realarith;; +open Reals;; +open Calc_rat;; +open Ints;; +open Sets;; +open Iterate;; +open Cart;; +open Define;; +open Help;; + +open Analysis;; +open Transc;; + let REAL_SUB_SUM0 = prove (`!x y m. sum(0,m) x - sum(0,m) y = sum(0,m) (\i. x i - y i)`, diff --git a/Library/integer.ml b/Library/integer.ml index 51c0df5e..a0cbb901 100644 --- a/Library/integer.ml +++ b/Library/integer.ml @@ -4,6 +4,68 @@ (* This is similar to stuff in Library/prime.ml etc. for natural numbers. *) (* ========================================================================= *) +set_jrh_lexer;; +open System;; +open Lib;; +open Fusion;; +open Basics;; +open Nets;; +open Printer;; +open Preterm;; +open Parser;; +open Equal;; +open Bool;; +open Drule;; +open Log;; +open Import_proofs;; +open Tactics;; +open Itab;; +open Replay;; +open Simp;; +open Embryo_extra;; +open Theorems;; +open Ind_defs;; +open Class;; +open Trivia;; +open Canon;; +open Meson;; +open Metis;; +open Quot;; +open Impconv;; +open Pair;; +open Nums;; +open Recursion;; +open Arith;; +open Wf;; +open Calc_num;; +open Normalizer;; +open Grobner;; +open Ind_types;; +open Lists;; +open Realax;; +open Calc_int;; +open Realarith;; +open Reals;; +open Calc_rat;; +open Ints;; +open Sets;; +open Iterate;; +open Cart;; +open Define;; +open Help;; +open Wo;; + +(* Removed for analysis deps *) +(* +open Binary;; +open Card;; +open Permutations;; +open Products;; +open Floor;; +open Misc;; +open Iter;; +*) + prioritize_int();; (* ------------------------------------------------------------------------- *) diff --git a/Library/multiplicative.ml b/Library/multiplicative.ml index 56e0af3e..64682538 100644 --- a/Library/multiplicative.ml +++ b/Library/multiplicative.ml @@ -2,8 +2,60 @@ (* Multiplicative functions into N or R (could add Z, C etc.) *) (* ========================================================================= *) -needs "Library/prime.ml";; -needs "Library/pocklington.ml";; +set_jrh_lexer;; +open System;; +open Lib;; +open Fusion;; +open Basics;; +open Nets;; +open Printer;; +open Parser;; +open Equal;; +open Bool;; +open Drule;; +open Log;; +open Import_proofs;; +open Tactics;; +open Itab;; +open Replay;; +open Simp;; +open Embryo_extra;; +open Theorems;; +open Ind_defs;; +open Class;; +open Trivia;; +open Canon;; +open Meson;; +open Metis;; +open Quot;; +open Impconv;; +open Pair;; +open Nums;; +open Recursion;; +open Arith;; +open Wf;; +open Calc_num;; +open Normalizer;; +open Grobner;; +open Ind_types;; +open Lists;; +open Realax;; +open Calc_int;; +open Realarith;; +open Reals;; +open Calc_rat;; +open Ints;; +open Sets;; +open Iterate;; +open Cart;; +open Define;; +open Help;; +open Wo;; + +open Iter;; + +open Prime;; +open Pocklington;; (* ------------------------------------------------------------------------- *) (* Definition of multiplicativity of functions into N. *) diff --git a/Library/pocklington.ml b/Library/pocklington.ml index 0b06ab48..013c38ae 100644 --- a/Library/pocklington.ml +++ b/Library/pocklington.ml @@ -2,8 +2,68 @@ (* HOL primality proving via Pocklington-optimized Pratt certificates. *) (* ========================================================================= *) -needs "Library/iter.ml";; -needs "Library/prime.ml";; +set_jrh_lexer;; +open System;; +open Lib;; +open Fusion;; +open Basics;; +open Nets;; +open Printer;; +open Parser;; +open Equal;; +open Bool;; +open Drule;; +open Log;; +open Import_proofs;; +open Tactics;; +open Itab;; +open Replay;; +open Simp;; +open Embryo_extra;; +open Theorems;; +open Ind_defs;; +open Class;; +open Trivia;; +open Canon;; +open Meson;; +open Metis;; +open Quot;; +open Impconv;; +open Pair;; +open Nums;; +open Recursion;; +open Arith;; +open Wf;; +open Calc_num;; +open Normalizer;; +open Grobner;; +open Ind_types;; +open Lists;; +open Realax;; +open Calc_int;; +open Realarith;; +open Reals;; +open Calc_rat;; +open Ints;; +open Sets;; +open Iterate;; +open Cart;; +open Define;; +open Help;; +open Wo;; + +(* Removed for analysis compatibility *) +(* +open Binary;; +open Card;; +open Permutations;; +open Products;; +open Floor;; +open Misc;; +*) + +open Iter;; +open Prime;; prioritize_num();; diff --git a/Library/poly.ml b/Library/poly.ml index 977607e8..01ec8a3c 100644 --- a/Library/poly.ml +++ b/Library/poly.ml @@ -2,7 +2,58 @@ (* Properties of real polynomials (not canonically represented). *) (* ========================================================================= *) -needs "Library/analysis.ml";; +set_jrh_lexer;; +open System;; +open Lib;; +open Fusion;; +open Basics;; +open Nets;; +open Printer;; +open Preterm;; +open Parser;; +open Equal;; +open Bool;; +open Drule;; +open Log;; +open Import_proofs;; +open Tactics;; +open Itab;; +open Replay;; +open Simp;; +open Embryo_extra;; +open Theorems;; +open Ind_defs;; +open Class;; +open Trivia;; +open Canon;; +open Meson;; +open Metis;; +open Quot;; +open Impconv;; +open Pair;; +open Nums;; +open Recursion;; +open Arith;; +open Wf;; +open Calc_num;; +open Normalizer;; +open Grobner;; +open Ind_types;; +open Lists;; +open Realax;; +open Calc_int;; +open Realarith;; +open Reals;; +open Calc_rat;; +open Ints;; +open Sets;; +open Iterate;; +open Cart;; +open Define;; +open Help;; + +open Analysis;; + prioritize_real();; @@ -817,16 +868,16 @@ let POLY_ORDER = prove (* Definition of order. *) (* ------------------------------------------------------------------------- *) -let order = new_definition - `order a p = @n. ([--a; &1] exp n) divides p /\ +let poly_order = new_definition + `poly_order a p = @n. ([--a; &1] exp n) divides p /\ ~(([--a; &1] exp (SUC n)) divides p)`;; let ORDER = prove (`!p a n. ([--a; &1] exp n) divides p /\ ~(([--a; &1] exp (SUC n)) divides p) <=> - (n = order a p) /\ + (n = poly_order a p) /\ ~(poly p = poly [])`, - REPEAT GEN_TAC THEN REWRITE_TAC[order] THEN + REPEAT GEN_TAC THEN REWRITE_TAC[poly_order] THEN EQ_TAC THEN STRIP_TAC THENL [SUBGOAL_THEN `~(poly p = poly [])` ASSUME_TAC THENL [FIRST_ASSUM(UNDISCH_TAC o check is_neg o concl) THEN @@ -840,24 +891,24 @@ let ORDER = prove let ORDER_THM = prove (`!p a. ~(poly p = poly []) - ==> ([--a; &1] exp (order a p)) divides p /\ - ~(([--a; &1] exp (SUC(order a p))) divides p)`, + ==> ([--a; &1] exp (poly_order a p)) divides p /\ + ~(([--a; &1] exp (SUC(poly_order a p))) divides p)`, MESON_TAC[ORDER]);; let ORDER_UNIQUE = prove (`!p a n. ~(poly p = poly []) /\ ([--a; &1] exp n) divides p /\ ~(([--a; &1] exp (SUC n)) divides p) - ==> (n = order a p)`, + ==> (n = poly_order a p)`, MESON_TAC[ORDER]);; let ORDER_POLY = prove - (`!p q a. (poly p = poly q) ==> (order a p = order a q)`, + (`!p q a. (poly p = poly q) ==> (poly_order a p = poly_order a q)`, REPEAT STRIP_TAC THEN - ASM_REWRITE_TAC[order; divides; FUN_EQ_THM; POLY_MUL]);; + ASM_REWRITE_TAC[poly_order; divides; FUN_EQ_THM; POLY_MUL]);; let ORDER_ROOT = prove - (`!p a. (poly p a = &0) <=> (poly p = poly []) \/ ~(order a p = 0)`, + (`!p a. (poly p a = &0) <=> (poly p = poly []) \/ ~(poly_order a p = 0)`, REPEAT GEN_TAC THEN ASM_CASES_TAC `poly p = poly []` THEN ASM_REWRITE_TAC[poly] THEN EQ_TAC THENL [DISCH_THEN(MP_TAC o REWRITE_RULE[POLY_LINEAR_DIVIDES]) THEN @@ -870,8 +921,8 @@ let ORDER_ROOT = prove REWRITE_TAC[FUN_EQ_THM; POLY_MUL; poly] THEN REAL_ARITH_TAC; DISCH_TAC THEN FIRST_ASSUM(MP_TAC o SPEC `a:real` o MATCH_MP ORDER_THM) THEN - UNDISCH_TAC `~(order a p = 0)` THEN - SPEC_TAC(`order a p`,`n:num`) THEN + UNDISCH_TAC `~(poly_order a p = 0)` THEN + SPEC_TAC(`poly_order a p`,`n:num`) THEN INDUCT_TAC THEN ASM_REWRITE_TAC[poly_exp; NOT_SUC] THEN DISCH_THEN(MP_TAC o CONJUNCT1) THEN REWRITE_TAC[divides] THEN DISCH_THEN(X_CHOOSE_THEN `s:real list` SUBST1_TAC) THEN @@ -879,7 +930,7 @@ let ORDER_ROOT = prove let ORDER_DIVIDES = prove (`!p a n. ([--a; &1] exp n) divides p <=> - (poly p = poly []) \/ n <= order a p`, + (poly p = poly []) \/ n <= poly_order a p`, REPEAT GEN_TAC THEN ASM_CASES_TAC `poly p = poly []` THEN ASM_REWRITE_TAC[] THENL [ASM_REWRITE_TAC[divides] THEN EXISTS_TAC `[]:real list` THEN @@ -888,14 +939,14 @@ let ORDER_DIVIDES = prove let ORDER_DECOMP = prove (`!p a. ~(poly p = poly []) - ==> ?q. (poly p = poly (([--a; &1] exp (order a p)) ** q)) /\ + ==> ?q. (poly p = poly (([--a; &1] exp (poly_order a p)) ** q)) /\ ~([--a; &1] divides q)`, REPEAT STRIP_TAC THEN FIRST_ASSUM(MP_TAC o MATCH_MP ORDER_THM) THEN DISCH_THEN(CONJUNCTS_THEN2 MP_TAC ASSUME_TAC o SPEC `a:real`) THEN DISCH_THEN(X_CHOOSE_TAC `q:real list` o REWRITE_RULE[divides]) THEN EXISTS_TAC `q:real list` THEN ASM_REWRITE_TAC[] THEN DISCH_THEN(X_CHOOSE_TAC `r: real list` o REWRITE_RULE[divides]) THEN - UNDISCH_TAC `~([-- a; &1] exp SUC (order a p) divides p)` THEN + UNDISCH_TAC `~([-- a; &1] exp SUC (poly_order a p) divides p)` THEN ASM_REWRITE_TAC[] THEN REWRITE_TAC[divides] THEN EXISTS_TAC `r:real list` THEN ASM_REWRITE_TAC[POLY_MUL; FUN_EQ_THM; poly_exp] THEN @@ -907,11 +958,11 @@ let ORDER_DECOMP = prove let ORDER_MUL = prove (`!a p q. ~(poly (p ** q) = poly []) ==> - (order a (p ** q) = order a p + order a q)`, + (poly_order a (p ** q) = poly_order a p + poly_order a q)`, REPEAT GEN_TAC THEN DISCH_THEN(fun th -> ASSUME_TAC th THEN MP_TAC th) THEN REWRITE_TAC[POLY_ENTIRE; DE_MORGAN_THM] THEN STRIP_TAC THEN - SUBGOAL_THEN `(order a p + order a q = order a (p ** q)) /\ + SUBGOAL_THEN `(poly_order a p + poly_order a q = poly_order a (p ** q)) /\ ~(poly (p ** q) = poly [])` MP_TAC THENL [ALL_TAC; MESON_TAC[]] THEN REWRITE_TAC[GSYM ORDER] THEN CONJ_TAC THENL @@ -932,14 +983,14 @@ let ORDER_MUL = prove SUBGOAL_THEN `[--a; &1] divides (r ** s)` MP_TAC THENL [ALL_TAC; ASM_REWRITE_TAC[POLY_PRIMES]] THEN REWRITE_TAC[divides] THEN EXISTS_TAC `t:real list` THEN - SUBGOAL_THEN `poly ([-- a; &1] exp (order a p) ** r ** s) = - poly ([-- a; &1] exp (order a p) ** ([-- a; &1] ** t))` + SUBGOAL_THEN `poly ([-- a; &1] exp (poly_order a p) ** r ** s) = + poly ([-- a; &1] exp (poly_order a p) ** ([-- a; &1] ** t))` MP_TAC THENL [ALL_TAC; MESON_TAC[POLY_MUL_LCANCEL; POLY_EXP_PRIME_EQ_0]] THEN - SUBGOAL_THEN `poly ([-- a; &1] exp (order a q) ** - [-- a; &1] exp (order a p) ** r ** s) = - poly ([-- a; &1] exp (order a q) ** - [-- a; &1] exp (order a p) ** + SUBGOAL_THEN `poly ([-- a; &1] exp (poly_order a q) ** + [-- a; &1] exp (poly_order a p) ** r ** s) = + poly ([-- a; &1] exp (poly_order a q) ** + [-- a; &1] exp (poly_order a p) ** [-- a; &1] ** t)` MP_TAC THENL [ALL_TAC; MESON_TAC[POLY_MUL_LCANCEL; POLY_EXP_PRIME_EQ_0]] THEN @@ -949,15 +1000,15 @@ let ORDER_MUL = prove let ORDER_DIFF = prove (`!p a. ~(poly (diff p) = poly []) /\ - ~(order a p = 0) - ==> (order a p = SUC (order a (diff p)))`, + ~(poly_order a p = 0) + ==> (poly_order a p = SUC (poly_order a (diff p)))`, REPEAT GEN_TAC THEN DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN SUBGOAL_THEN `~(poly p = poly [])` MP_TAC THENL [ASM_MESON_TAC[POLY_DIFF_ZERO]; ALL_TAC] THEN DISCH_THEN(X_CHOOSE_THEN `q:real list` MP_TAC o SPEC `a:real` o MATCH_MP ORDER_DECOMP) THEN - SPEC_TAC(`order a p`,`n:num`) THEN + SPEC_TAC(`poly_order a p`,`n:num`) THEN INDUCT_TAC THEN REWRITE_TAC[NOT_SUC; SUC_INJ] THEN STRIP_TAC THEN MATCH_MP_TAC ORDER_UNIQUE THEN ASM_REWRITE_TAC[] THEN @@ -1017,21 +1068,21 @@ let POLY_SQUAREFREE_DECOMP_ORDER = prove (poly p = poly (q ** d)) /\ (poly (diff p) = poly (e ** d)) /\ (poly d = poly (r ** p ++ s ** diff p)) - ==> !a. order a q = (if order a p = 0 then 0 else 1)`, + ==> !a. poly_order a q = (if poly_order a p = 0 then 0 else 1)`, REPEAT STRIP_TAC THEN - SUBGOAL_THEN `order a p = order a q + order a d` MP_TAC THENL - [MATCH_MP_TAC EQ_TRANS THEN EXISTS_TAC `order a (q ** d)` THEN + SUBGOAL_THEN `poly_order a p = poly_order a q + poly_order a d` MP_TAC THENL + [MATCH_MP_TAC EQ_TRANS THEN EXISTS_TAC `poly_order a (q ** d)` THEN CONJ_TAC THENL [MATCH_MP_TAC ORDER_POLY THEN ASM_REWRITE_TAC[]; MATCH_MP_TAC ORDER_MUL THEN FIRST_ASSUM(fun th -> GEN_REWRITE_TAC "Library/poly.ml:(RAND_CONV o LAND_CONV)" (RAND_CONV o LAND_CONV) [SYM th]) THEN ASM_MESON_TAC[POLY_DIFF_ZERO]]; ALL_TAC] THEN - ASM_CASES_TAC `order a p = 0` THEN ASM_REWRITE_TAC[] THENL + ASM_CASES_TAC `poly_order a p = 0` THEN ASM_REWRITE_TAC[] THENL [ARITH_TAC; ALL_TAC] THEN - SUBGOAL_THEN `order a (diff p) = - order a e + order a d` MP_TAC THENL - [MATCH_MP_TAC EQ_TRANS THEN EXISTS_TAC `order a (e ** d)` THEN + SUBGOAL_THEN `poly_order a (diff p) = + poly_order a e + poly_order a d` MP_TAC THENL + [MATCH_MP_TAC EQ_TRANS THEN EXISTS_TAC `poly_order a (e ** d)` THEN CONJ_TAC THENL [ASM_MESON_TAC[ORDER_POLY]; ASM_MESON_TAC[ORDER_MUL]]; ALL_TAC] THEN SUBGOAL_THEN `~(poly p = poly [])` ASSUME_TAC THENL @@ -1040,15 +1091,15 @@ let POLY_SQUAREFREE_DECOMP_ORDER = prove ASM_REWRITE_TAC[] THEN DISCH_THEN(fun th -> MP_TAC th THEN MP_TAC(AP_TERM `PRE` th)) THEN REWRITE_TAC[PRE] THEN DISCH_THEN(ASSUME_TAC o SYM) THEN - SUBGOAL_THEN `order a (diff p) <= order a d` MP_TAC THENL - [SUBGOAL_THEN `([--a; &1] exp (order a (diff p))) divides d` + SUBGOAL_THEN `poly_order a (diff p) <= poly_order a d` MP_TAC THENL + [SUBGOAL_THEN `([--a; &1] exp (poly_order a (diff p))) divides d` MP_TAC THENL [ALL_TAC; ASM_MESON_TAC[POLY_ENTIRE; ORDER_DIVIDES]] THEN SUBGOAL_THEN - `([--a; &1] exp (order a (diff p))) divides p /\ - ([--a; &1] exp (order a (diff p))) divides (diff p)` + `([--a; &1] exp (poly_order a (diff p))) divides p /\ + ([--a; &1] exp (poly_order a (diff p))) divides (diff p)` MP_TAC THENL [REWRITE_TAC[ORDER_DIVIDES; LE_REFL] THEN DISJ2_TAC THEN - REWRITE_TAC[ASSUME `order a (diff p) = PRE (order a p)`] THEN + REWRITE_TAC[ASSUME `poly_order a (diff p) = PRE (poly_order a p)`] THEN ARITH_TAC; DISCH_THEN(CONJUNCTS_THEN MP_TAC) THEN REWRITE_TAC[divides] THEN REWRITE_TAC[ASSUME `poly d = poly (r ** p ++ s ** diff p)`] THEN @@ -1065,7 +1116,7 @@ let POLY_SQUAREFREE_DECOMP_ORDER = prove let rsquarefree = new_definition `rsquarefree p <=> ~(poly p = poly []) /\ - !a. (order a p = 0) \/ (order a p = 1)`;; + !a. (poly_order a p = 0) \/ (poly_order a p = 1)`;; (* ------------------------------------------------------------------------- *) (* Standard squarefree criterion and rephasing of squarefree decomposition. *) diff --git a/Library/prime.ml b/Library/prime.ml index 49f5ae7f..af377a96 100644 --- a/Library/prime.ml +++ b/Library/prime.ml @@ -2,6 +2,31 @@ (* Basic theory of divisibility, gcd, coprimality and primality (over N). *) (* ========================================================================= *) +set_jrh_lexer;; +open System;; +open Lib;; +open Fusion;; +open Basics;; +open Parser;; +open Equal;; +open Bool;; +open Drule;; +open Tactics;; +open Simp;; +open Theorems;; +open Class;; +open Meson;; +open Pair;; +open Nums;; +open Arith;; +open Calc_num;; +open Grobner;; +open Realax;; +open Ints;; +open Sets;; +open Iterate;; +open Cart;; + prioritize_num();; (* ------------------------------------------------------------------------- *) diff --git a/Library/wo.ml b/Library/wo.ml index ec2dc41d..c33d5e2b 100644 --- a/Library/wo.ml +++ b/Library/wo.ml @@ -12,6 +12,7 @@ open Lib;; open Fusion;; open Basics;; open Printer;; +open Preterm;; open Parser;; open Equal;; open Bool;; diff --git a/Makefile b/Makefile index 2c913fed..8c2f91dc 100644 --- a/Makefile +++ b/Makefile @@ -37,10 +37,10 @@ PP=-pp "camlp5r $(CAMLP5_REVISED) ./pa_j_tweak.cmo $(OCAML_LIB)/nums.cma ./syste %.cmx: %.ml system.cmo pa_j_tweak.cmo $(OCAMLOPT) $(OCAMLFLAGS) $(PP) -I $(CAMLP5_LIB) -c $@ $< -CORE_SRCS=system hol_native lib fusion basics nets printer theorem_fingerprint preterm parser equal pb_printer debug_mode bool drule log import_proofs tactics itab replay simp theorems ind_defs class trivia canon meson metis quot impconv pair nums recursion arith wf calc_num normalizer grobner ind_types lists realax calc_int realarith reals calc_rat ints sets iterate cart define parse_tactic +CORE_SRCS=system hol_native lib fusion basics nets printer theorem_fingerprint preterm parser equal normalize pb_printer debug_mode bool drule log import_proofs tactics itab replay simp theorems ind_defs class trivia canon meson metis quot impconv pair nums recursion arith wf calc_num normalizer grobner ind_types lists realax calc_int realarith reals calc_rat ints sets iterate cart define parse_tactic SANDBOXEE_SRCS=$(CORE_SRCS) comms sandboxee -CORE_OBJS=str_list_fingerprint comms_wrapper subprocess +CORE_OBJS=theorem_fingerprint_c comms_wrapper subprocess CORE_LIBS=nums.cmxa str.cmxa quotation.cmx hol_light_sandboxee: $(addsuffix .cmx, $(SANDBOXEE_SRCS)) $(addsuffix .o, $(CORE_OBJS)) $(OCAMLOPT) -o $@ $(OCAMLFLAGS) -I $(CAMLP5_LIB)\ diff --git a/Multivariate/cauchy.ml b/Multivariate/cauchy.ml index e76d469b..2940931b 100644 --- a/Multivariate/cauchy.ml +++ b/Multivariate/cauchy.ml @@ -23823,3 +23823,6 @@ let JORDAN_SCHOENFLIES_S2 = prove FIRST_X_ASSUM MATCH_MP_TAC THEN ASM SET_TAC[]);; Pb_printer.clear_file_tags();; + +(* This is the last file in the "complex" dataset. Clear the library_tags. *) +Pb_printer.library_tags := [];; diff --git a/Multivariate/cross.ml b/Multivariate/cross.ml index 90c6f250..9bfddab1 100644 --- a/Multivariate/cross.ml +++ b/Multivariate/cross.ml @@ -52,7 +52,6 @@ open Vectors;; open Determinants;; open Topology;; - prioritize_vector();; (* ------------------------------------------------------------------------- *) diff --git a/Multivariate/lpspaces.ml b/Multivariate/lpspaces.ml index fdf44ba5..270910c6 100644 --- a/Multivariate/lpspaces.ml +++ b/Multivariate/lpspaces.ml @@ -2,7 +2,86 @@ (* L_p spaces for functions R^m->R^n based on an arbitrary set. *) (* ========================================================================= *) -needs "Multivariate/realanalysis.ml";; +set_jrh_lexer;; +open System;; +open Lib;; +open Fusion;; +open Basics;; +open Nets;; +open Printer;; +open Preterm;; +open Parser;; +open Equal;; +open Bool;; +open Drule;; +open Log;; +open Import_proofs;; +open Tactics;; +open Itab;; +open Replay;; +open Simp;; +open Embryo_extra;; +open Theorems;; +open Ind_defs;; +open Class;; +open Trivia;; +open Canon;; +open Meson;; +open Metis;; +open Quot;; +open Impconv;; +open Pair;; +open Nums;; +open Recursion;; +open Arith;; +open Wf;; +open Calc_num;; +open Normalizer;; +open Grobner;; +open Ind_types;; +open Lists;; +open Realax;; +open Calc_int;; +open Realarith;; +open Reals;; +open Calc_rat;; +open Ints;; +open Sets;; +open Iterate;; +open Cart;; +open Define;; +open Help;; +open Wo;; +open Binary;; +open Card;; +open Permutations;; +open Products;; +open Floor;; +open Misc;; +open Iter;; +open Vectors;; +open Determinants;; +open Topology;; +open Convex;; +open Paths;; +open Polytope;; +open Degree;; +open Derivatives;; +open Clifford;; +open Integration;; +open Measure;; + +open Metric;; + +open Binomial;; +open Complexes;; +open Canal;; +open Transcendentals;; +open Realanalysis;; +open Moretop;; +open Cauchy;; + +open Realanalysis;; (* ------------------------------------------------------------------------- *) (* The space L_p of measurable functions f with |f|^p integrable (on s). *) diff --git a/Multivariate/tarski.ml b/Multivariate/tarski.ml index 670ab747..d137c0ad 100644 --- a/Multivariate/tarski.ml +++ b/Multivariate/tarski.ml @@ -2,7 +2,67 @@ (* Proof that Tarski's axioms for geometry hold in Euclidean space. *) (* ========================================================================= *) -needs "Multivariate/convex.ml";; +set_jrh_lexer;; +open System;; +open Lib;; +open Fusion;; +open Basics;; +open Nets;; +open Printer;; +open Preterm;; +open Parser;; +open Equal;; +open Bool;; +open Drule;; +open Log;; +open Import_proofs;; +open Tactics;; +open Itab;; +open Replay;; +open Simp;; +open Embryo_extra;; +open Theorems;; +open Ind_defs;; +open Class;; +open Trivia;; +open Canon;; +open Meson;; +open Metis;; +open Quot;; +open Impconv;; +open Pair;; +open Nums;; +open Recursion;; +open Arith;; +open Wf;; +open Calc_num;; +open Normalizer;; +open Grobner;; +open Ind_types;; +open Lists;; +open Realax;; +open Calc_int;; +open Realarith;; +open Reals;; +open Calc_rat;; +open Ints;; +open Sets;; +open Iterate;; +open Cart;; +open Define;; +open Help;; +open Wo;; +open Binary;; +open Card;; +open Permutations;; +open Products;; +open Floor;; +open Misc;; +open Iter;; +open Vectors;; +open Determinants;; +open Topology;; +open Convex;; (* ------------------------------------------------------------------------- *) (* Axiom 1 (reflexivity for equidistance). *) diff --git a/api/hol_light_prover.cc b/api/hol_light_prover.cc index 95d64d90..e2fc7eac 100644 --- a/api/hol_light_prover.cc +++ b/api/hol_light_prover.cc @@ -1,9 +1,10 @@ #include "hol_light_prover.h" +#include + // Ignore this comment (1). // Ignore this comment (2). #include "proof_assistant.pb.h" -#include "theorem_fingerprint.h" // Ignore this comment (3). #include "google/protobuf/stubs/status.h" // Ignore this comment (5). @@ -27,6 +28,8 @@ enum Request { kRegisterTheorem = 9, kCompareLastTheorem = 10, kDefineType = 11, + kNegateGoal = 12, + kApplyRule = 13, }; // LINT.ThenChange(//hol_light/sandboxee.ml) @@ -57,6 +60,25 @@ util::StatusOr HolLightProver::ApplyTactic( return response; } +util::StatusOr HolLightProver::ApplyRule( + const ApplyRuleRequest& request) { + RETURN_IF_ERROR(comm_->SendInt(kApplyRule)); + RETURN_IF_ERROR(comm_->SendString(request.rule())); + LOG(INFO) << "Calling HOL Light to apply rule; setting timer (in ms):" + << request.timeout_ms(); + auto timer = comm_->GetTimer(request.timeout_ms()); + RETURN_IF_ERROR(comm_->GetStatus()); + ApplyRuleResponse response; + int64 result; + RETURN_IF_ERROR(comm_->ReceiveInt(&result)); + if (result == kOk) { + RETURN_IF_ERROR(ReceiveTheorem(response.mutable_theorem())); + } else { + RETURN_IF_ERROR(comm_->ReceiveString(response.mutable_error())); + } + return response; +} + util::StatusOr HolLightProver::VerifyProof( const VerifyProofRequest& request) { VerifyProofResponse response; @@ -99,6 +121,15 @@ StatusOr HolLightProver::GetGoals() { return goals; } +StatusOr HolLightProver::NegateGoal(const Theorem& goal) { + RETURN_IF_ERROR(comm_->SendInt(kNegateGoal)); + RETURN_IF_ERROR(SendGoal(goal)); + RETURN_IF_ERROR(comm_->GetStatus()); + string negated_goal_as_term; + RETURN_IF_ERROR(comm_->ReceiveString(&negated_goal_as_term)); + return negated_goal_as_term; +} + Status HolLightProver::ReceiveGoals(GoalList* goals) { int64 n, m; RETURN_IF_ERROR(comm_->ReceiveInt(&n)); @@ -127,6 +158,19 @@ Status HolLightProver::SendGoal(const Theorem& goal) { return util::OkStatus(); } +Status HolLightProver::ReceiveTheorem(Theorem* theorem) { + int64 n; + theorem->set_tag(Theorem::THEOREM); + RETURN_IF_ERROR(comm_->ReceiveInt(&n)); + for (int64 i = 0; i < n; ++i) { + string* term = (i == 0) ? theorem->mutable_pretty_printed() + : (i == 1) ? theorem->mutable_conclusion() + : theorem->add_hypotheses(); + RETURN_IF_ERROR(comm_->ReceiveString(term)); + } + return util::OkStatus(); +} + Status HolLightProver::SendTheorem(const Theorem& theorem) { RETURN_IF_ERROR(comm_->SendInt(1 + theorem.hypotheses_size())); RETURN_IF_ERROR(comm_->SendString(theorem.conclusion())); @@ -150,7 +194,7 @@ Status HolLightProver::RegisterLastTheorem() { Status HolLightProver::CompareLastTheorem(const Theorem& theorem) { RETURN_IF_ERROR(comm_->SendInt(kCompareLastTheorem)); - RETURN_IF_ERROR(comm_->SendInt(Fingerprint(theorem))); + RETURN_IF_ERROR(SendTheorem(theorem)); return comm_->GetStatus(); } @@ -170,13 +214,16 @@ Status HolLightProver::Define(const Definition& def) { return comm_->GetStatus(); } -Status HolLightProver::DefineType(const TypeDefinition& def) { +Status HolLightProver::DefineType(const TypeDefinition& def, + int64* fingerprint_result) { RETURN_IF_ERROR(comm_->SendInt(kDefineType)); RETURN_IF_ERROR(comm_->SendString(def.type_name())); RETURN_IF_ERROR(comm_->SendString(def.abs_name())); RETURN_IF_ERROR(comm_->SendString(def.rep_name())); RETURN_IF_ERROR(comm_->SendInt(def.theorem_arg())); - return comm_->GetStatus(); + RETURN_IF_ERROR(comm_->GetStatus()); + RETURN_IF_ERROR(comm_->ReceiveInt(fingerprint_result)); + return util::OkStatus(); } Status HolLightProver::SetTermEncoding(int encoding) { @@ -188,32 +235,47 @@ Status HolLightProver::SetTermEncoding(int encoding) { StatusOr HolLightProver::RegisterTheorem( const RegisterTheoremRequest& request) { const auto& theorem = request.theorem(); - LOG(INFO) << "Registering " << theorem.fingerprint() << "."; - Status status = CheatTheorem(theorem); + // Disallow theorems with hypotheses RegisterTheoremResponse response; - response.set_fingerprint(request.theorem().fingerprint()); + if (!theorem.hypotheses().empty()) { + response.set_error_msg("Theorem with hypotheses are not supported."); + return response; + } + int64 fingerprint_from_ocaml; + Status status = CheatTheorem(theorem, &fingerprint_from_ocaml); if (!status.ok()) { response.set_error_msg(status.ToString()); } - LOG(INFO) << "Registered " << theorem.fingerprint() << "."; + if (status.ok() && request.theorem().has_fingerprint() && + request.theorem().fingerprint() != fingerprint_from_ocaml) { + std::ostringstream msg; + msg << "Fingerprint " << request.theorem().fingerprint() + << " in RegisterTheoremRequest does not match fingerprint " + << fingerprint_from_ocaml << " returned from HOL Light.\n"; + response.set_error_msg(msg.str()); + } + response.set_fingerprint(fingerprint_from_ocaml); return response; } -Status HolLightProver::CheatTheorem(const Theorem& theorem) { +Status HolLightProver::CheatTheorem(const Theorem& theorem, + int64* fingerprint_result) { switch (theorem.tag()) { case Theorem::TYPE_DEFINITION: - return DefineType(theorem.type_definition()); + return DefineType(theorem.type_definition(), fingerprint_result); case Theorem::DEFINITION: { RETURN_IF_ERROR(comm_->SendInt(kRegisterTheorem)); RETURN_IF_ERROR(SendTheorem(theorem)); - RETURN_IF_ERROR(comm_->SendInt(Fingerprint(theorem))); - return comm_->GetStatus(); + RETURN_IF_ERROR(comm_->GetStatus()); + RETURN_IF_ERROR(comm_->ReceiveInt(fingerprint_result)); + return util::OkStatus(); } case Theorem::THEOREM: { RETURN_IF_ERROR(comm_->SendInt(kRegisterTheorem)); RETURN_IF_ERROR(SendTheorem(theorem)); - RETURN_IF_ERROR(comm_->SendInt(Fingerprint(theorem))); - return comm_->GetStatus(); + RETURN_IF_ERROR(comm_->GetStatus()); + RETURN_IF_ERROR(comm_->ReceiveInt(fingerprint_result)); + return util::OkStatus(); } default: return util::UnimplementedError(::absl::StrCat( diff --git a/api/hol_light_prover.h b/api/hol_light_prover.h index b4ed35e6..45bdc207 100644 --- a/api/hol_light_prover.h +++ b/api/hol_light_prover.h @@ -4,6 +4,7 @@ #include "compatibility.h" #include + #include "proof_assistant.pb.h" #include "comm.h" // Ignore this comment (4). @@ -24,6 +25,10 @@ class HolLightProver { util::StatusOr ApplyTactic( const ApplyTacticRequest& request); + // Apply a rule. The response is either a new theorem, or a string indicating + // why application of the rule failed. Not expected to return non-OK status. + util::StatusOr ApplyRule(const ApplyRuleRequest& request); + // Verifies that a proof is sound. util::StatusOr VerifyProof( const VerifyProofRequest& request); @@ -57,15 +62,16 @@ class HolLightProver { util::Status CompareLastTheorem(const Theorem& theorem); // Cheats the given theorem, so that it can be specified later using - // ToTacticArgument. - util::Status CheatTheorem(const Theorem& theorem); + // ToTacticArgument. Returns the fingerprint computed by OCaml. + util::Status CheatTheorem(const Theorem& theorem, int64* fingerprint_result); // Defines a new symbol, where the definition contains the type of definition // and the defining term. Some definition types require additional parameters. util::Status Define(const Definition& definition); // Defines a new type. - util::Status DefineType(const TypeDefinition& definition); + util::Status DefineType(const TypeDefinition& definition, + int64* fingerprint_result); // Determines how terms will be represented as strings henceforth. // (1=pretty printed, 2=sexpr) @@ -76,8 +82,11 @@ class HolLightProver { util::Status VerifyProofImpl(const VerifyProofRequest& request); util::Status SendGoal(const Theorem& goal); util::Status SendTheorem(const Theorem& theorem); + util::Status ReceiveTheorem(Theorem* theorem); util::Status ReceiveGoals(GoalList* goals); + util::StatusOr NegateGoal(const Theorem& goal); + private: Comm* comm_; }; diff --git a/api/proof_assistant.proto b/api/proof_assistant.proto index 894a898a..f881eb27 100644 --- a/api/proof_assistant.proto +++ b/api/proof_assistant.proto @@ -43,8 +43,10 @@ message Theorem { } optional string name = 4; - // Hypotheses must be strings that represent theorems. - // Currently only goals (tag = GOAL) are allowed to have hypotheses. + // Hypotheses may only be used by THEOREMs, while GOALs should use the + // assumptions field. + // Note that old data may have GOALs with hypotheses. In this case, each + // string stores a term 'x' that represents a theorem 'x |- x'. repeated string hypotheses = 1; // Conclusion is a string representing a term. @@ -77,6 +79,10 @@ message Theorem { // Fingerprint of the goal that resulted in this theorem. Used for exporting // proofs. optional int64 goal_fingerprint = 12; + + // Protos with tag=GOAL can have assumptions. Cannot also have hypotheses. + // Assumptions must not have GOAL tag themselves. + repeated Theorem assumptions = 13; } message GoalList { @@ -97,6 +103,19 @@ message ApplyTacticResponse { } } +message ApplyRuleRequest { + // Fully formed rule application, including all parameters. + optional string rule = 1; + optional int64 timeout_ms = 3 [default = 5000]; +} + +message ApplyRuleResponse { + oneof result { + Theorem theorem = 1; + string error = 2; + } +} + message VerifyProofRequest { optional Theorem goal = 1; // TODO(kbk): Add description, why need theorem in addition to goal. diff --git a/api/subprocess_comm.cc b/api/subprocess_comm.cc index 7846141b..5e6295f8 100644 --- a/api/subprocess_comm.cc +++ b/api/subprocess_comm.cc @@ -1,6 +1,7 @@ #include "subprocess_comm.h" #include + #include #include #include @@ -25,7 +26,7 @@ SubprocessComm::SubprocessComm() : ok_(google::protobuf::util::Status::OK), comms_failure_(google::protobuf::util::Status( google::protobuf::util::error::INTERNAL, - "Communication with sandbox failed.")), + "Communication with sandbox (subprocess_comm.cc) failed.")), subprocess_(Subprocess::Start(kHolPath)), comms_(subprocess_.comms()) { std::cout << "Waiting for hol-light to get ready." << std::endl << std::flush; diff --git a/api/theorem_fingerprint.cc b/api/theorem_fingerprint.cc index 39e8a158..20af56fa 100644 --- a/api/theorem_fingerprint.cc +++ b/api/theorem_fingerprint.cc @@ -14,6 +14,9 @@ constexpr uint64 kMask = (static_cast(1) << 62) - 1; int64 Fingerprint(const Theorem& theorem) { // LINT.IfChange + if (!theorem.hypotheses().empty() && !theorem.assumptions().empty()) { + LOG(ERROR) << "Goal can only have one of hypotheses or assumptions."; + } if (!theorem.has_conclusion() && theorem.has_fingerprint()) { // Needed for theorems in tactic parameters that may only be logged as fps. return theorem.fingerprint(); @@ -23,8 +26,13 @@ int64 Fingerprint(const Theorem& theorem) { uint64 tmp = farmhash::Fingerprint64(hypothesis); fp = farmhash::Fingerprint(fp, tmp); } + for (const auto& assumption : theorem.assumptions()) { + uint64 tmp = Fingerprint(assumption); + tmp = tmp + 1; // Ensures that "[t1 |- t2], t3", "[|-t1, |-t2], t3" differ + fp = farmhash::Fingerprint(fp, tmp); + } int64 result = static_cast(fp & kMask); - // LINT.ThenChange(//hol_light/theorem_fingerprint.cc) + // LINT.ThenChange(//hol_light/theorem_fingerprint_c.cc) if (theorem.has_fingerprint() && theorem.fingerprint() != result) { LOG(ERROR) << "Inconsistent fingerprints in Theorem protobuf."; } diff --git a/api/theorem_fingerprint.h b/api/theorem_fingerprint.h index 3f96b826..f41d7a23 100644 --- a/api/theorem_fingerprint.h +++ b/api/theorem_fingerprint.h @@ -6,6 +6,7 @@ namespace deepmath { // Returns a stable fingerprint of the given theorem. +// DEPRECATED: use either the python or the ocaml version. int64 Fingerprint(const Theorem& theorem); // Returns tactic parameter referencing the given theorem, in a format diff --git a/bool.ml b/bool.ml index e8170178..4caf63ea 100644 --- a/bool.ml +++ b/bool.ml @@ -54,7 +54,7 @@ let find_basic_definition (tm : term) : thm option = with Not_found -> None;; let new_basic_definition_log_opt (log: bool) tm = - let normalized_tm = Pb_printer.normalize_term tm in + let normalized_tm = Normalize.normalize_term tm in match find_basic_definition normalized_tm with Some thm -> thm | None -> diff --git a/define.ml b/define.ml index a2df6050..cbe0a607 100644 --- a/define.ml +++ b/define.ml @@ -1012,7 +1012,7 @@ let define = f,itlist GEN avs (itlist PROVE_HYP (CONJUNCTS th) (end_itlist CONJ ths)) in fun tm -> let last_known_constant = last_constant() in - let normalized_tm = Pb_printer.normalize_term tm in + let normalized_tm = Normalize.normalize_term tm in match find_define_definition normalized_tm with Some thm -> warn true "Benign redefinition"; diff --git a/drule.ml b/drule.ml index 2eb5619a..ce5c8594 100644 --- a/drule.ml +++ b/drule.ml @@ -499,7 +499,7 @@ let find_drule_definition_string (s : string) : thm option = let new_definition_log_opt (log: bool) tm = - let normalized_tm = Pb_printer.normalize_term tm in + let normalized_tm = Normalize.normalize_term tm in match find_drule_definition normalized_tm with Some thm -> thm (* Redefinition *) | None -> diff --git a/farmhash_compatibility.h b/farmhash_compatibility.h new file mode 100644 index 00000000..7ef5c1d8 --- /dev/null +++ b/farmhash_compatibility.h @@ -0,0 +1,7 @@ +#include "farmhash.h" + +namespace farmhash { +inline uint64_t Fingerprint(uint64_t x, uint64_t y) { + return Fingerprint(Uint128(x, y)); +} +} // namespace farmhash diff --git a/import_proofs.ml b/import_proofs.ml index 038b27d6..e235de13 100644 --- a/import_proofs.ml +++ b/import_proofs.ml @@ -28,7 +28,7 @@ let goal_fingerprint (g: goal) : int = let asl, (concl: term) = g in (if length asl > 0 then failwith "Cannot handle assumptions for goal fingerprints"); - Theorem_fingerprint.term_fingerprint ([], Pb_printer.normalize_term concl);; + Theorem_fingerprint.term_fingerprint ([], Normalize.normalize_term concl);; let proof_index_contains (g: goal) : bool = Hashtbl.mem proof_index (goal_fingerprint g);; @@ -44,10 +44,10 @@ let proof_of_goal (g: goal) : wrapped_proof = failwith ("No proof found for goal with index " ^ string_of_int goal_fp);; (* Call this function to 'import' a proof. *) -let register_proof (goal_fp: int) (t: wrapped_proof) (in_core: bool) = +let register_proof (goal_fp: int) (t: wrapped_proof) (in_core: bool) : unit = (* Printf.eprintf "register_proof for %d\n%!" goal_fp; *) if Hashtbl.mem proof_index goal_fp then - failwith "register_proof: tried to register two proofs for the same goal." + Printf.printf "Error in register_proof: tried to register two proofs for fingerprint %d for the same goal.\n\!" goal_fp else Hashtbl.add proof_index goal_fp t; if not in_core then Hashtbl.add has_to_be_checked goal_fp ();; diff --git a/ind_defs.ml b/ind_defs.ml index 3c95a919..e4d9e3d4 100644 --- a/ind_defs.ml +++ b/ind_defs.ml @@ -386,7 +386,7 @@ let prove_inductive_relations_exist,new_inductive_definition = let th2 = generalize_schematic_variables true fvs th1 in derive_existence th2 and new_inductive_definition (tm : term) : thm * thm * thm = - let normalized_tm = Pb_printer.normalize_term tm in + let normalized_tm = Normalize.normalize_term tm in match find_inductive_definition normalized_tm with Some (thtr: (thm*thm*thm)) -> warn true "Benign redefinition of inductive predicate"; diff --git a/log.ml b/log.ml index 31c67bd7..336a59a3 100644 --- a/log.ml +++ b/log.ml @@ -536,7 +536,7 @@ let tactic_argument_term fmt (t: term) : unit = pp_print_string fmt " parameters {"; pp_print_string fmt " parameter_type: TERM"; pp_print_string fmt " term: \""; - sexp_print fmt (sexp_term (Pb_printer.normalize_term t)); + sexp_print fmt (sexp_term (Normalize.normalize_term t)); pp_print_string fmt "\""; pp_print_string fmt "}";; @@ -573,7 +573,7 @@ let tactic_argument_thm fmt ptype (srcs: src list) : unit = tactic_argument_thms fmt ptype (fun th -> - print_thm_pb fmt (normalize_theorem th) "THEOREM" (fun _ -> ())) + print_thm_pb fmt (Normalize.normalize_theorem th) "THEOREM" (fun _ -> ())) (map extract_thm srcs);; let tactic_arguments_pb fmt (taclog : src tactic_log) = @@ -710,7 +710,7 @@ let rec print_prooflog_pb pp_print_string fmt "nodes {"; pp_print_string fmt " goal {"; - print_goal_pb fmt (goal_to_tuple g) tag (fun _ -> ()); + print_goal_pb fmt (goal_to_tuple g) "GOAL" (fun _ -> ()); pp_print_string fmt "}"; pp_print_string fmt " status: PROVED"; print_tactic_application_pb fmt tl subgoals; @@ -733,7 +733,7 @@ let rec print_prooflog_pb let log_proof (log : src proof_log) (th: thm) : unit = if List.length (hyp th) == 0 then try_to_print - (print_prooflog_pb (Pb_printer.normalize_theorem th) "THEOREM") + (print_prooflog_pb (Normalize.normalize_theorem th) "THEOREM") log prooflog_pb_fmt;; diff --git a/normalize.ml b/normalize.ml new file mode 100644 index 00000000..01f860cd --- /dev/null +++ b/normalize.ml @@ -0,0 +1,100 @@ +set_jrh_lexer;; +open Lib;; +open Fusion;; +open Printer;; + + +(* ---------------------------------------------------------------------------*) +(* Normalization of GEN%PVARs *) +(* ---------------------------------------------------------------------------*) + +let is_genpvar_name (var_name: string) : bool = + let re = Str.regexp "GEN%PVAR%[0-9]+" in (* matches vars like GEN%PVAR%8342 *) + Str.string_match re var_name 0;; + +let is_genpvar (tm: term) : bool = + is_var tm && (is_genpvar_name o fst o dest_var) tm;; + +let is_genpvar_abstraction (tm: term) : bool = + is_abs tm && (is_genpvar o fst o dest_abs) tm;; + +(* Traverse term bottom up; create and combine conversion to rename GEN%PVARs *) +let rec normalize_genpvars_conv (nesting: int) (tm: term) : Equal.conv = + match tm with + Var(s,ty) -> + REFL (* = ALL_CONV *) + | Const(s,ty) -> + REFL (* = ALL_CONV *) + | Comb(l,r) -> + Equal.COMB2_CONV + (normalize_genpvars_conv nesting l) + (normalize_genpvars_conv nesting r) + | Abs(var,body) -> + if is_genpvar var + then + let body_conv = normalize_genpvars_conv (nesting+1) body in + let rename_conv = Equal.ALPHA_CONV + (mk_var ("GEN%PVAR%" ^ string_of_int nesting, type_of var)) in + Equal.EVERY_CONV [Equal.ABS_CONV body_conv; rename_conv] + else + Equal.ABS_CONV (normalize_genpvars_conv nesting body);; + +let normalize_genpvars_conv (tm: term) : Equal.conv = + normalize_genpvars_conv 0 tm;; + +let assert_no_hypotheses (th: thm) : unit = + if List.length (Fusion.hyp th) != 0 then + failwith ( + Printf.sprintf + "Theorem with hypotheses encountered during normalization: %s" + (str_of_sexp (sexp_thm th)) + ) + else ();; + +let normalize_genpvars (th: thm) : thm = + Equal.CONV_RULE (normalize_genpvars_conv (concl th)) th;; + +let normalize_genpvars_in_term (tm: term) : term = + let conversion_theorem = normalize_genpvars_conv tm tm in + assert_no_hypotheses conversion_theorem; + (snd o dest_eq o concl) conversion_theorem;; + +(* ---------------------------------------------------------------------------*) +(* Normalization of generic types *) +(* ---------------------------------------------------------------------------*) + +let is_gen_tvar_name (tvar_name: string) : bool = + let re = Str.regexp "\\?[0-9]+" in (* matches types of the form ?928342 *) + Str.string_match re tvar_name 0;; + +let is_gen_tvar tvar = (is_gen_tvar_name o dest_vartype) tvar;; + +let normalizing_type_substitutions (tms : term list) : + (hol_type * hol_type) list = + let tvars = remove_duplicates__stable + (List.concat (map type_vars_in_term__stable tms)) in + let gen_tvars = filter is_gen_tvar tvars in + List.mapi + (fun idx tvar -> mk_vartype ("?" ^ string_of_int idx), tvar) + gen_tvars;; + +(* Instantiates types of the form ? by ?. *) +let normalize_generic_type_variables (th: thm) : thm = + let hyps, concl = dest_thm th in + INST_TYPE (normalizing_type_substitutions (concl::hyps)) th;; + +let normalize_generic_type_variables_terms (tms: term list) : term list = + let substitutions = normalizing_type_substitutions tms in + map (inst substitutions) tms;; + +(* ---------------------------------------------------------------------------*) +(* Normalization functions for terms and theorems. *) +(* ---------------------------------------------------------------------------*) + +let normalize_terms (tms: term list) : term list = + normalize_generic_type_variables_terms (map normalize_genpvars_in_term tms);; + +let normalize_term (tm: term) : term = hd (normalize_terms [tm]);; + +let normalize_theorem (th: thm) : thm = + normalize_generic_type_variables (normalize_genpvars th);; diff --git a/pair.ml b/pair.ml index f142770b..7c512dd0 100644 --- a/pair.ml +++ b/pair.ml @@ -197,7 +197,7 @@ let new_definition_log_opt : bool -> term -> thm = fun arg -> let gv = genvar(type_of arg) in gv,depair gv arg in fun (log: bool) (tm: term) -> - let normalized_tm = Pb_printer.normalize_term tm in + let normalized_tm = Normalize.normalize_term tm in match find_pair_definition normalized_tm with Some thm -> warn true "Benign redefinition"; diff --git a/parse_tactic.ml b/parse_tactic.ml index 6b2acdc6..7bcb29f4 100644 --- a/parse_tactic.ml +++ b/parse_tactic.ml @@ -3,10 +3,12 @@ open Lib;; open Fusion;; open Tactics;; open Equal;; +open Simp;; open Theorem_fingerprint;; module Parse : sig - val parse : string -> tactic + val parse : string -> tactic;; + val parse_rule : string -> thm;; end = struct type data = string * int @@ -72,6 +74,8 @@ struct let (thp : thm parser), add_th = keyword_parser "thm" let (tcp : tactic parser), add_tc = keyword_parser "tactic" + let (rule_p : thm parser), add_rule = keyword_parser "rule" + let (term_rule_p : (term -> thm) parser), add_term_rule = keyword_parser "term_rule" let (convp : conv parser), add_conv = keyword_parser "conv" let (convfnp : (conv -> conv) parser), add_convfn = keyword_parser "convfn" @@ -114,6 +118,7 @@ struct fn Ints.ARITH_TAC, "ARITH_TAC"; fn Meson.ASM_MESON_TAC thl, "ASM_MESON_TAC"; fn Metis.ASM_METIS_TAC thl, "ASM_METIS_TAC"; + fn Metis.METIS_TAC thl, "METIS_TAC"; fn Ind_defs.BACKCHAIN_TAC th, "BACKCHAIN_TAC"; fn CHEAT_TAC, "CHEAT_TAC"; fn CHOOSE_TAC th, "CHOOSE_TAC"; @@ -153,6 +158,73 @@ struct fn X_CHOOSE_TAC tm th, "X_CHOOSE_TAC"; fn X_GEN_TAC tm, "X_GEN_TAC"; ] + let EQ_IMP_RULE_LEFT = (fun th -> + fst (Bool.EQ_IMP_RULE th)) + let EQ_IMP_RULE_RIGHT = (fun th -> + snd (Bool.EQ_IMP_RULE th)) + let () = add_rule [ + (* A rule produces a thm from various arguments, usually another thm. *) + fn ASM_REWRITE_RULE thl th, "ASM_REWRITE_RULE"; + fn BETA_RULE th, "BETA_RULE"; + fn CONV_RULE conv th, "CONV_RULE"; + fn DEDUCT_ANTISYM_RULE th th, "DEDUCT_ANTISYM_RULE"; + (* EQ_IMP_RULE thm->thm*thm so split into left and right. *) + fn EQ_IMP_RULE_LEFT th, "EQ_IMP_RULE_LEFT"; + fn EQ_IMP_RULE_RIGHT th, "EQ_IMP_RULE_RIGHT"; + fn Bool.IMP_ANTISYM_RULE th th, "IMP_ANTISYM_RULE"; + fn ONCE_ASM_REWRITE_RULE thl th, "ONCE_ASM_REWRITE_RULE"; + fn ONCE_REWRITE_RULE thl th, "ONCE_REWRITE_RULE"; + fn ONCE_SIMP_RULE thl th, "ONCE_SIMP_RULE"; + fn PURE_ASM_REWRITE_RULE thl th, "PURE_ASM_REWRITE_RULE"; + fn PURE_ONCE_ASM_REWRITE_RULE thl th, "PURE_ONCE_ASM_REWRITE_RULE"; + fn PURE_ONCE_REWRITE_RULE thl th, "PURE_ONCE_REWRITE_RULE"; + fn PURE_REWRITE_RULE thl th, "PURE_REWRITE_RULE"; + fn PURE_SIMP_RULE thl th, "PURE_SIMP_RULE"; + fn REWRITE_RULE thl th, "REWRITE_RULE"; + fn Class.SELECT_RULE th, "SELECT_RULE"; + fn SIMP_RULE thl th, "SIMP_RULE"; + (* Other rule-like transformations, but not named *_RULE *) + fn Bool.SPEC_ALL th, "SPEC_ALL"; + fn Bool.CONJ th th, "CONJ"; + fn Bool.CONJUNCT1 th, "CONJUNCT1"; + fn Bool.CONJUNCT2 th, "CONJUNCT2"; + fn Bool.DISCH_ALL th, "DISCH_ALL"; + fn Bool.DISJ_CASES th th th, "DISJ_CASES"; + fn Bool.EQF_ELIM th, "EQF_ELIM"; + fn Bool.EQF_INTRO th, "EQF_INTRO"; + fn Bool.EQT_ELIM th, "EQT_ELIM"; + fn Bool.EQT_INTRO th, "EQT_INTRO"; + fn Fusion.EQ_MP th th, "EQ_MP"; + fn Bool.EXISTENCE th, "EXISTENCE"; + fn Bool.GEN_ALL th, "GEN_ALL"; + fn Equal.GSYM th, "GSYM"; + fn Bool.IMP_TRANS th th, "IMP_TRANS"; + fn Ints.INT_OF_REAL_THM th, "INT_OF_REAL_THM"; + fn Arith.LE_IMP th, "LE_IMP"; + fn Drule.MATCH_MP th th, "MATCH_MP"; + fn Drule.MK_CONJ th th, "MK_CONJ"; + fn Drule.MK_DISJ th th, "MK_DISJ"; + fn Bool.MP th th, "MP"; + fn Bool.NOT_ELIM th, "NOT_ELIM"; + fn Bool.NOT_INTRO th, "NOT_INTRO"; + fn Bool.PROVE_HYP th th, "PROVE_HYP"; + fn Reals.REAL_LET_IMP th, "REAL_LET_IMP"; + fn Reals.REAL_LE_IMP th, "REAL_LE_IMP"; + fn Bool.SIMPLE_DISJ_CASES th th, "SIMPLE_DISJ_CASES"; + fn Equal.SUBS thl th, "SUBS"; + fn Equal.SYM th, "SYM"; + fn Fusion.TRANS th th, "TRANS"; + fn Bool.UNDISCH th, "UNDISCH"; + fn Bool.UNDISCH_ALL th, "UNDISCH_ALL"; + (* RULES that require a term argument *) + (* NOTE: these are only the term rules that end _RULE *) + fn Ints.ARITH_RULE tm, "ARITH_RULE"; + fn Canon.CONJ_ACI_RULE tm, "CONJ_ACI_RULE"; + fn Canon.DISJ_ACI_RULE tm, "DISJ_ACI_RULE"; + fn Ints.INTEGER_RULE tm, "INTEGER_RULE"; + fn Ints.NUMBER_RULE tm, "NUMBER_RULE"; + fn Sets.SET_RULE tm, "SET_RULE"; + ] let () = add_conv [ fn BETA_CONV, "BETA_CONV"; fn Class.CONTRAPOS_CONV, "CONTRAPOS_CONV"; @@ -175,16 +247,27 @@ struct fn composel convfnl, "COMPOSE"; ] - let parse s = ASSUM_LIST (fun thl -> - let (tc, d) = tcp thl (s, 0) in - if empty d then tc else + let return_if_empty retv d = + if empty d then retv else let (s1, i) = d in let remainder = String.sub s1 i (String.length s1 - i) in - fail d "end of input" remainder) + fail d "end of input" remainder + + let parse s = ASSUM_LIST (fun thl -> + let (tc, d) = tcp thl (s, 0) in + return_if_empty tc d) let () = add_th [fn Theorem_fingerprint.thm_of_index n, "THM"] (* A named theorem can be referred to by name in a tactic parameter *) let name_thm name theorem = add_th [fn theorem, name] + + (* Parse strings into corresponding rules *) + let parse_rule (s:string):thm = + (* Piggy-backing on generic parser, which expects asl as env. + passing empty list for env, ASSUM params are always illegal *) + let (rulec, d) = rule_p [] (s, 0) in + return_if_empty rulec d + end include Parse diff --git a/pb_printer.ml b/pb_printer.ml index 37243709..0f155e5a 100644 --- a/pb_printer.ml +++ b/pb_printer.ml @@ -36,101 +36,6 @@ let pb_string_of_thm (th: thm) : string = let no_newlines = Str.global_replace (Str.regexp "\n") " " th_string in Str.global_replace (Str.regexp " ") " " no_newlines;; -(* ---------------------------------------------------------------------------*) -(* Normalization of GEN%PVARs *) -(* ---------------------------------------------------------------------------*) - -let is_genpvar_name (var_name: string) : bool = - let re = Str.regexp "GEN%PVAR%[0-9]+" in (* matches vars like GEN%PVAR%8342 *) - Str.string_match re var_name 0;; - -let is_genpvar (tm: term) : bool = - is_var tm && (is_genpvar_name o fst o dest_var) tm;; - -let is_genpvar_abstraction (tm: term) : bool = - is_abs tm && (is_genpvar o fst o dest_abs) tm;; - -(* Traverse term bottom up; create and combine conversion to rename GEN%PVARs *) -let rec normalize_genpvars_conv (nesting: int) (tm: term) : Equal.conv = - match tm with - Var(s,ty) -> - REFL (* = ALL_CONV *) - | Const(s,ty) -> - REFL (* = ALL_CONV *) - | Comb(l,r) -> - Equal.COMB2_CONV - (normalize_genpvars_conv nesting l) - (normalize_genpvars_conv nesting r) - | Abs(var,body) -> - if is_genpvar var - then - let body_conv = normalize_genpvars_conv (nesting+1) body in - let rename_conv = Equal.ALPHA_CONV - (mk_var ("GEN%PVAR%" ^ string_of_int nesting, type_of var)) in - Equal.EVERY_CONV [Equal.ABS_CONV body_conv; rename_conv] - else - Equal.ABS_CONV (normalize_genpvars_conv nesting body);; - -let normalize_genpvars_conv (tm: term) : Equal.conv = - normalize_genpvars_conv 0 tm;; - -let assert_no_hypotheses (th: thm) : unit = - if List.length (Fusion.hyp th) != 0 then - failwith ( - Printf.sprintf - "Theorem with hypotheses encountered during normalization: %s" - (str_of_sexp (sexp_thm th)) - ) - else ();; - -let normalize_genpvars (th: thm) : thm = - Equal.CONV_RULE (normalize_genpvars_conv (concl th)) th;; - -let normalize_genpvars_in_term (tm: term) : term = - let conversion_theorem = normalize_genpvars_conv tm tm in - assert_no_hypotheses conversion_theorem; - (snd o dest_eq o concl) conversion_theorem;; - -(* ---------------------------------------------------------------------------*) -(* Normalization of generic types *) -(* ---------------------------------------------------------------------------*) - -let is_gen_tvar_name (tvar_name: string) : bool = - let re = Str.regexp "\\?[0-9]+" in (* matches types of the form ?928342 *) - Str.string_match re tvar_name 0;; - -let is_gen_tvar tvar = (is_gen_tvar_name o dest_vartype) tvar;; - -let normalizing_type_substitutions (tms : term list) : - (hol_type * hol_type) list = - let tvars = remove_duplicates__stable - (List.concat (map type_vars_in_term__stable tms)) in - let gen_tvars = filter is_gen_tvar tvars in - List.mapi - (fun idx tvar -> mk_vartype ("?" ^ string_of_int idx), tvar) - gen_tvars;; - -(* Instantiates types of the form ? by ?. *) -let normalize_generic_type_variables (th: thm) : thm = - let hyps, concl = dest_thm th in - INST_TYPE (normalizing_type_substitutions (concl::hyps)) th;; - -let normalize_generic_type_variables_terms (tms: term list) : term list = - let substitutions = normalizing_type_substitutions tms in - map (inst substitutions) tms;; - -(* ---------------------------------------------------------------------------*) -(* Normalization functions for terms and theorems. *) -(* ---------------------------------------------------------------------------*) - -let normalize_terms (tms: term list) : term list = - normalize_generic_type_variables_terms (map normalize_genpvars_in_term tms);; - -let normalize_term (tm: term) : term = hd (normalize_terms [tm]);; - -let normalize_theorem (th: thm) : thm = - normalize_generic_type_variables (normalize_genpvars th);; - (* ---------------------------------------------------------------------------*) (* Protobuf printer functions *) (* ---------------------------------------------------------------------------*) @@ -146,7 +51,8 @@ let print_int_pb (fmt: Format.formatter) (field_name: string) i : unit = let print_goal_pb (fmt: Format.formatter) ((assumptions, conclusion): term list * term) (tag: string) (definition_printer : Format.formatter -> unit) : unit = - let conclusion::assumptions = normalize_terms (conclusion::assumptions) in + let conclusion::assumptions = + Normalize.normalize_terms (conclusion::assumptions) in print_int_pb fmt "fingerprint" (Theorem_fingerprint.term_fingerprint (assumptions, conclusion)); List.iter @@ -197,12 +103,12 @@ let print_definition let thm_db_print_definition (log: bool) (definition_type: string) (th: thm) (term: term) (recursion_thm: thm option) (constants: (string*hol_type) list) : unit = - let th = normalize_theorem th in + let th = Normalize.normalize_theorem th in Theorem_fingerprint.register_thm th; if not log then () else match thm_db_fmt with Some fmt -> - let term = normalize_term term in + let term = Normalize.normalize_term term in pp_print_string fmt "theorems {"; print_thm_pb fmt th "DEFINITION" (print_definition @@ -215,7 +121,7 @@ let thm_db_print_definition (log: bool) (definition_type: string) (th: thm) let thm_db_print_theorem (th: thm) (source: string) (goal_fingerprint : int option) : unit = - let th = normalize_theorem th in + let th = Normalize.normalize_theorem th in if not (Theorem_fingerprint.thm_is_known th) then ( Theorem_fingerprint.register_thm th; match thm_db_fmt with @@ -235,7 +141,7 @@ let thm_db_print_theorem (th: thm) let print_type_definition (tyname: string) (absname: string) (repname: string) (th_arg: thm) : Format.formatter -> unit = - let th_arg = normalize_theorem th_arg in + let th_arg = Normalize.normalize_theorem th_arg in fun fmt -> pp_print_string fmt (" type_name: \"" ^ tyname ^ "\""); pp_print_string fmt (" abs_name: \"" ^ absname ^ "\""); @@ -245,7 +151,7 @@ let print_type_definition (tyname: string) (absname: string) (repname: string) let thm_db_print_type_definition (tyname: string) (absname: string) (repname: string) (th_arg: thm) (th_result: thm) : unit = thm_db_print_theorem th_arg "type_definition_helper" None; - let th_result = normalize_theorem th_result in + let th_result = Normalize.normalize_theorem th_result in Theorem_fingerprint.register_thm th_result; match thm_db_fmt with Some fmt -> @@ -261,9 +167,9 @@ let thm_db_print_type_definition (tyname: string) let thm_db_print_specification (log: bool) (definition_type: string) (constants: string list) (thm_arg: thm) (th: thm) : unit = - let thm_arg = normalize_theorem thm_arg in + let thm_arg = Normalize.normalize_theorem thm_arg in thm_db_print_theorem thm_arg "specification" None; - let th = normalize_theorem th in + let th = Normalize.normalize_theorem th in Theorem_fingerprint.register_thm th; if not log then () else match thm_db_fmt with diff --git a/preterm.ml b/preterm.ml index f3d5515f..4b312b72 100644 --- a/preterm.ml +++ b/preterm.ml @@ -79,6 +79,18 @@ let prioritize_overload ty = with Failure _ -> ()) (!the_overload_skeletons);; +let print_overload overload = + do_list + (fun (s, ty) -> + report(s)) + overload;; + +let print_interface interface = + do_list + (fun (s1, (s2, ty)) -> + report((s1 ^ " ; " ^ s2))) + interface;; + (* ------------------------------------------------------------------------- *) (* Type abbreviations. *) (* ------------------------------------------------------------------------- *) diff --git a/printer.ml b/printer.ml index c1613cec..6077e877 100644 --- a/printer.ml +++ b/printer.ml @@ -96,6 +96,18 @@ let unparse_as_infix,parse_as_infix,get_infix_status,infixes = (fun n -> assoc n (!infix_list)), (fun () -> !infix_list);; +(* Helpful print methods for inspecting the infix_list. *) +let report_infix = + (fun inf -> + (report ((fst inf) ^ " " + ^ (string_of_int (fst (snd inf))) ^ " " + ^ (snd (snd inf))))) + +let report_infixes = + let infxs = infixes() in + (fun () -> + (map report_infix infxs));; + (* ------------------------------------------------------------------------- *) (* Interface mapping. *) (* ------------------------------------------------------------------------- *) diff --git a/recursion.ml b/recursion.ml index bb22a2e9..5664bba0 100644 --- a/recursion.ml +++ b/recursion.ml @@ -127,7 +127,7 @@ let new_recursive_definition ax tm = with Failure s -> Printf.eprintf "Error parsing term from sexp: %s\n with error %s\n%!" term_str s); *) - let normalized_tm = Pb_printer.normalize_term tm in + let normalized_tm = Normalize.normalize_term tm in match find_recursive_definition normalized_tm with Some thm -> warn true "Benign redefinition of recursive function"; diff --git a/sandboxee.ml b/sandboxee.ml index 5658ecd2..644e3103 100644 --- a/sandboxee.ml +++ b/sandboxee.ml @@ -3,6 +3,9 @@ open Fusion;; open Printer;; open Tactics;; open Theorem_fingerprint;; +open List;; + +let MAX_TERM_LENGTH = 10000;; (* 10k characters*) type response_atom = String of string | Int of int @@ -23,7 +26,7 @@ let define_inductive (tm: term) : unit = let th1, th2, th3 = Ind_defs.new_inductive_definition tm in List.map register_thm [th1; th2; th3]; ();; -let specification (constants: string list) (spec_thm_fingerprint: int) : unit = +let specification (constants: string list) (spec_thm_fingerprint: int) : int = let spec_thm : thm = thm_of_index spec_thm_fingerprint in register_thm (Nums.new_specification constants spec_thm);; @@ -31,13 +34,28 @@ let current_goals() = try let (_,gs,_)::_ = !current_goalstack in gs with Match_failure _ -> [] let send_goals gs = - let str_of_tm t = String (Printer.encode_term t) in + let str_of_tm t = + let raw_string = Printer.encode_term t in + (if String.length raw_string > MAX_TERM_LENGTH then + raise (Failure "HOL Light term in resulting goal exceeds MAX_TERM_LENGTH.")); + String raw_string in let serialize (asl,w) = (* Format: [pretty_printed, conclusion, assumptions]*) let terms = w::(List.map (fun (_,t) -> Fusion.concl t) asl) in let strings = String (string_of_goal (asl, w)) :: List.map str_of_tm terms in (Int (List.length strings)) :: strings in (Int (List.length gs))::(List.flatten (List.map serialize gs)) +let send_thm th = (* Format: [pretty_printed, conclusion, hypotheses] *) + let str_of_tm t = + let raw_string = Printer.encode_term t in + (if String.length raw_string > MAX_TERM_LENGTH then + raise (Failure "HOL Light term in resulting goal exceeds MAX_TERM_LENGTH.")); + String raw_string in + let hyps, w = dest_thm(th) in + let terms = w::hyps in + let strings = String (string_of_thm th) + :: List.map str_of_tm terms in + (Int (List.length strings)) :: strings let repeat n f = let rec repeat_tr n l = if n > 0 then repeat_tr (n-1) (f()::l) else l in List.rev (repeat_tr n []) @@ -67,6 +85,31 @@ let with_timeout f x = ignore_timeout (); res;; +(******************* Support negating a goal. *******************) + +(* Tactic to bind a free variable in a goal. *) +let SPEC_OUTERMOST_TAC g = SPEC_TAC (hd (frees (snd g)), hd (frees (snd g))) g;; + +(* Tactic to move to conclusion first assumption is the assumption list.*) +let UNDISCH_HD_TAC (asm, c) = UNDISCH_TAC (concl (snd (hd asm))) (asm, c);; + +(* Takes as input a goal, and returns a term which is supposed to represent + * the negation of the goal *) +let negate_goal input_goal = + let _, no_asm_subgoals, _ = REPEAT UNDISCH_HD_TAC input_goal in + let no_asm_goal = (match no_asm_subgoals with + | g::[] -> g + | _ -> failwith "negate_goal: expected 1 subgoal pulling assumptions." + ) in + let _, no_frees_subgoals, _ = REPEAT SPEC_OUTERMOST_TAC no_asm_goal in + let input_goal_as_term = (match no_frees_subgoals with + | (_, t)::[] -> t + | _ -> failwith "negate_goal: expected 1 subgoal with no assumptions here" + ) in + Bool.mk_neg input_goal_as_term;; + +(******************* handle_request *******************) + let kOk = Int 0 let kError = Int 1 let handle_request() = @@ -88,13 +131,16 @@ let handle_request() = (match definition_type with "BASIC" -> let tm : term = Parser.decode_term def_term in - register_thm (Bool.log_new_basic_definition tm) + register_thm (Bool.log_new_basic_definition tm); + () | "DRULE" -> let tm : term = Parser.decode_term def_term in - register_thm (Drule.new_definition tm) + register_thm (Drule.new_definition tm); + () | "PAIR" -> let tm : term = Parser.decode_term def_term in - register_thm (Pair.new_definition tm) + register_thm (Pair.new_definition tm); + () | "SPEC" -> let spec_thm: int = Comms.receive_int() in let num_constants: int = Comms.receive_int() in @@ -103,21 +149,25 @@ let handle_request() = else (let c = Comms.receive_string() in c::read_constants (n-1)) in let constants : string list = read_constants num_constants in - specification constants spec_thm + specification constants spec_thm; + () | "RECURSIVE" -> let tm : term = Parser.decode_term def_term in (*Printf.eprintf "Decoded term: %s\n%!" (str_of_sexp (sexp_term tm));*) let rec_thm_fp: int = Comms.receive_int() in let rec_thm: thm = thm_of_index rec_thm_fp in let ret_thm: thm = Recursion.new_recursive_definition rec_thm tm in - register_thm ret_thm + register_thm ret_thm; + () | "INDUCTIVE" -> let tm : term = Parser.decode_term def_term in define_inductive tm | "DEFINE" -> let tm : term = Parser.decode_term def_term in let ret_thm = Define.define tm in - register_thm ret_thm); [] + register_thm ret_thm; + () + ); [] (* end of match definition_type *) | 7 (* = kSetEncoding *) -> let _ = Printer.current_encoding := (match Comms.receive_int() with | 1 (* = TE_PRETTY *) -> Printer.Pretty @@ -140,11 +190,15 @@ let handle_request() = with e -> [kError;String (Printexc.to_string e)]) | 9 (* = kRegisterTheorem *) -> let gs = receive_string_list() in - let index = Comms.receive_int() in - Theorem_fingerprint.index_thm index (Drule.mk_thm (to_term_list gs)); - [] + let thm_to_register = Drule.mk_thm (to_term_list gs) in +(* let fingerprint = Theorem_fingerprint.fingerprint(thm_to_register) in *) + let fingerprint = register_thm thm_to_register in +(* Theorem_fingerprint.index_thm fingerprint (thm_to_register); *) + [Int fingerprint] | 10 (* = kCompareLastTheorem *) -> - let expected = Comms.receive_int() in + let gs = receive_string_list() in + let thm_to_register = Drule.mk_thm (to_term_list gs) in + let expected = Theorem_fingerprint.fingerprint(thm_to_register) in let fingerprint = Theorem_fingerprint.fingerprint(fst (top_thm())) in (if fingerprint != expected then failwith ("Last theorem is not THM " ^ string_of_int expected ^ @@ -158,10 +212,24 @@ let handle_request() = let thm_arg_fp : int = Comms.receive_int() in let thm_arg : thm = thm_of_index thm_arg_fp in let ret_thm = Class.new_type_definition tyname (absname, repname) thm_arg in - register_thm ret_thm; - [] + let fingerprint = register_thm ret_thm in + [Int fingerprint] + | 12 (* = kNegateGoal *) -> + let gs = receive_string_list() in + let negated_goal_as_term = negate_goal (to_goal gs) in + [String (Printer.encode_term negated_goal_as_term)] + | 13 (* = kApplyRule *) -> + let rule_str = Comms.receive_string() in + (try + with_timeout (fun rule_str -> + (* Wrapping the rule application in the timeout-sensitive part *) + let th = Parse_tactic.parse_rule rule_str in + kOk::(send_thm th) + ) rule_str + with e -> [kError;String (Printexc.to_string e)]) ) in result + with e -> [kError;String (Printexc.to_string e)] let () = diff --git a/str_list_fingerprint.cc b/str_list_fingerprint.cc deleted file mode 100644 index 095eca12..00000000 --- a/str_list_fingerprint.cc +++ /dev/null @@ -1,32 +0,0 @@ -#include "caml/memory.h" -#include "caml/mlvalues.h" -#include "farmhash.h" - -namespace { -// The maximum signed int in 64-bit Ocaml is 2**62-1. -// We drop an additional bit to avoid unsigned->signed conversion subtleties. -constexpr uint64_t kMask = (static_cast(1) << 62) - 1; -} // namespace - -namespace farmhash { -inline uint64_t Fingerprint(uint64_t x, uint64_t y) { - return Fingerprint(Uint128(x, y)); -} -} // namespace farmhash - -extern "C" { - -CAMLprim value TheoremFingerprint(value str_list) { - CAMLparam1(str_list); - bool first_iteration = true; - uint64_t result = 0; - while (str_list != Val_emptylist) { - const auto& s = Field(str_list, 0); - uint64_t f = farmhash::Fingerprint64(String_val(s), caml_string_length(s)); - result = first_iteration ? f : farmhash::Fingerprint(result, f); - str_list = Field(str_list, 1); - first_iteration = false; - } - CAMLreturn(Val_long(result & kMask)); -} -} diff --git a/tests/fingerprint_tests.ml b/tests/fingerprint_tests.ml new file mode 100644 index 00000000..249e6546 --- /dev/null +++ b/tests/fingerprint_tests.ml @@ -0,0 +1,48 @@ +(* These tests correspond to testFingerprintEqualToOCamlImplementation + in third_party/deepmath/deephol/theorem_fingerprint_test.py *) + +set_jrh_lexer;; +open Lib;; +open Fusion;; +open Printer;; +open Pb_printer;; +open Test_common;; + + +let true_term = Parser.parse_term "T";; +let false_term = Parser.parse_term "F";; + +let theorems = [ + Sets.IN_UNION; (* theorem without GEN%PVARS and ?types *) + Sets.INSERT; (* theorem with GEN%PVAR *) + ASSUME true_term; + Bool.ADD_ASSUM false_term (ASSUME true_term); (* multiple hypotheses *) + ];; +let expected_fingerprints = [975856962495483397; 345492714299286815; 4420649969775231556; 2661800747689726299];; + +(* The following comments are helpful for debugging: *) +(* printf "%s\n%!" (Printer.str_of_sexp (Printer.sexp_term Fingerprint_tests.true_term));; *) +(* printf "%s\n%!" (Printer.str_of_sexp (Printer.sexp_thm (Fusion.ASSUME Fingerprint_tests.true_term)));; *) +(* printf "%s\n%!" (Printer.str_of_sexp (Printer.sexp_thm (Bool.ADD_ASSUM Fingerprint_tests.false_term (Fusion.ASSUME Fingerprint_tests.true_term))));; *) + +let fingerprint_matches (theorem, expected_fp: thm * int) : unit = + let thm_fp = Theorem_fingerprint.fingerprint theorem in + assert_equal_int thm_fp expected_fp;; + +register_tests "Fingerprints match expected values." + fingerprint_matches (zip theorems expected_fingerprints);; + +let term_fingerprint_matches ((t, expected_fp): term * int) : unit = + let term_fp : int = Theorem_fingerprint.term_fingerprint ([], t) in + assert_equal_int term_fp expected_fp;; + +register_tests "Fingerprint of term matches expected value." + term_fingerprint_matches [(true_term, 70761607289060832)];; + + +let goal_fingerprint_matches ((goal, expected_fp): (thm list * term) * int) : unit = + let goal_fp : int = Theorem_fingerprint.goal_fingerprint goal in + assert_equal_int goal_fp expected_fp;; + +register_tests "Fingerprint of goal matches expected value." + goal_fingerprint_matches [(([ASSUME true_term], true_term), 4196583489440000546)];; diff --git a/tests/normalization_tests.ml b/tests/normalization_tests.ml index 57df00b4..ef63715a 100644 --- a/tests/normalization_tests.ml +++ b/tests/normalization_tests.ml @@ -4,7 +4,7 @@ open Fusion;; open Printer;; open Pb_printer;; open Test_common;; - +open Normalize;; let idempotent_term_normalization : term -> unit = assert_idempotent assert_equal_terms normalize_term;; diff --git a/tests/parse_tactic_tests.ml b/tests/parse_tactic_tests.ml new file mode 100644 index 00000000..e54620e2 --- /dev/null +++ b/tests/parse_tactic_tests.ml @@ -0,0 +1,192 @@ +(* Integration tests for parse_tactic and parse_rule. *) + +set_jrh_lexer;; +open Lib;; +open Fusion;; +open Parser;; +open Printer;; +open Pb_printer;; +open Tactics;; +open Simp;; +open Log;; +open Parse_tactic;; +open Test_common;; + +Printer.current_encoding := Printer.Pretty;; + +let true_term = Parser.parse_term "T";; +let false_term = Parser.parse_term "F";; + +let theorems = [ + Sets.IN_UNION; (* 975856962495483397; theorem without GEN%PVARS and ?types *) + Sets.INSERT; (* 345492714299286815; theorem with GEN%PVAR *) + ASSUME true_term; + Bool.ADD_ASSUM false_term (ASSUME true_term); (* multiple hypotheses *) + Bool.IMP_DEF; + Sets.FORALL_IN_UNION; (* 4052081339122143671 *) + ASSUME `p /\ q`; (* 3653885712938130508 *) + ASSUME `f = ((\x y. x + y) y)`; (* 1748915323273844750 *) + Equal.SYM(ASSUME `x:num = y`); (* 237159312591742290 *) + Equal.SYM(ASSUME `y:num = x`); (* 3739319715096271711 *) + Bool.SPEC_ALL Arith.GT; (* 1636085460980557391 *) + Class.TAUT `p /\ q ==> q /\ p`; (* 3093559110319623167 *) + Class.TAUT `q /\ p ==> p /\ q`; (* 262723677586854601 *) + Nums.INFINITY_AX; (* 650638948164601243 *) +];; +List.iter (fun t -> Theorem_fingerprint.register_thm t; ()) theorems;; +let string_of_fp = string_of_int o Theorem_fingerprint.fingerprint;; +let theorem_fingerprints = "[ THM " ^ (String.concat " ; THM " + (map string_of_fp theorems)) ^ " ]";; +printf "%s%!" theorem_fingerprints;; + +let asm_goals: goal list = [ + ([("", ASSUME `p:bool`)], `p:bool`); +] + +let goals: goal list = asm_goals @ [ + ([], `p`); + ([], `x = x`); + ([], `y = y /\ x = x`); + ([], `y = y ==> x = x`); + ([], `!P s t:A->bool. + (!x. x IN s UNION t ==> P x) <=> + (!x. x IN s ==> P x) /\ (!x. x IN t ==> P x)`); (* FORALL_IN_UNION *) + ];; + +(* Test parsing with assumptions from the assumption list *) +let asm_string_tactics: string list = [ + "REWRITE_TAC [ ASSUM 0 ]"; +];; +let asm_expected_tactics: tactic list = [ + Simp.ASM_REWRITE_TAC []; +];; + +(* Test tactic parsing for tactics with/without theorem lists *) +let string_tactics: string list = [ + "CONJ_TAC "; + "DISCH_TAC "; + "SIMP_TAC [ ]"; + "MESON_TAC [ ]"; + "MP_TAC THM 975856962495483397 "; + "REWRITE_TAC [ ]"; + "REWRITE_TAC [ THM 975856962495483397 ]"; + "REWRITE_TAC [ THM 345492714299286815 ]"; + "REWRITE_TAC " ^ theorem_fingerprints; +];; +let expected_tactics: tactic list = [ + CONJ_TAC; + DISCH_TAC; + SIMP_TAC []; + Meson.MESON_TAC []; + MP_TAC Sets.IN_UNION; + Simp.REWRITE_TAC []; + Simp.REWRITE_TAC [Sets.IN_UNION]; + Simp.REWRITE_TAC [Sets.INSERT]; + Simp.REWRITE_TAC theorems; +];; + +(* Turn tactic applications into sexpressions, catch tactic failures*) +let try_tactic (t:tactic): goal -> string = (fun g -> + try + let _, goals, _: goalstate = t g in + String.concat "; " (map (str_of_sexp o sexp_goal) goals) + with Failure f -> "Failure: " ^ f);; + +let assert_same_tactic_behavior_goals + (goals:goal list) (actual, expected: tactic * tactic): unit = + let res_actual = map (try_tactic actual) goals in + let res_expected = map (try_tactic expected) goals in + assert_equal_list res_actual res_expected;; + +let assert_same_tactic_behavior = assert_same_tactic_behavior_goals goals;; +let asm_assert_same_tactic_behavior = + assert_same_tactic_behavior_goals asm_goals;; + +let actual_tactics = map Parse_tactic.parse string_tactics in + register_tests "Parsed tactics exhibit expected behavior on set of goals." + assert_same_tactic_behavior (zip actual_tactics expected_tactics);; + +let actual_tactics = map Parse_tactic.parse asm_string_tactics in + register_tests + "Parsed tactics with asl arguments exhibit expected behavior." + asm_assert_same_tactic_behavior (zip actual_tactics asm_expected_tactics);; + + +(* Tests for parse_rule *) +let input_output : (string * thm) list = [ + "REWRITE_RULE [ THM 975856962495483397 ] THM 4052081339122143671", + REWRITE_RULE [Sets.IN_UNION] Sets.FORALL_IN_UNION; + "ARITH_RULE `x = 1 ==> y <= 1 \/ x < y`", + Ints.ARITH_RULE `x = 1 ==> y <= 1 \/ x < y`; + "ASM_REWRITE_RULE [ ] THM 3653885712938130508", + ASM_REWRITE_RULE [] (ASSUME `p /\ q`); + "BETA_RULE THM 1748915323273844750", + Equal.BETA_RULE (ASSUME `f = ((\x y. x + y) y)`); + "CONJ_ACI_RULE `(a /\ b) /\ (a /\ c) <=> (a /\ (c /\ a)) /\ b`", + Canon.CONJ_ACI_RULE `(a /\ b) /\ (a /\ c) <=> (a /\ (c /\ a)) /\ b`; + "DEDUCT_ANTISYM_RULE THM 237159312591742290 THM 3739319715096271711", + DEDUCT_ANTISYM_RULE (Equal.SYM(ASSUME `x:num = y`)) (Equal.SYM(ASSUME `y:num = x`)); + "DISJ_ACI_RULE `(p \/ q) \/ (q \/ r) <=> r \/ q \/ p`", + Canon.DISJ_ACI_RULE `(p \/ q) \/ (q \/ r) <=> r \/ q \/ p`; + "EQ_IMP_RULE_LEFT THM 1636085460980557391", + fst (Bool.EQ_IMP_RULE (Bool.SPEC_ALL Arith.GT)); + "EQ_IMP_RULE_RIGHT THM 1636085460980557391", + snd (Bool.EQ_IMP_RULE (Bool.SPEC_ALL Arith.GT)); + "IMP_ANTISYM_RULE THM 3093559110319623167 THM 262723677586854601", + Bool.IMP_ANTISYM_RULE (Class.TAUT `p /\ q ==> q /\ p`) (Class.TAUT `q /\ p ==> p /\ q`); + "INTEGER_RULE `!x y n:int. (x == y) (mod n) ==> (n divides x <=> n divides y)`", + Ints.INTEGER_RULE `!x y n:int. (x == y) (mod n) ==> (n divides x <=> n divides y)`; + "NUMBER_RULE `!a b a' b'. ~(gcd(a,b) = 0) /\ a = a' * gcd(a,b) /\ b = b' * gcd(a,b) ==> coprime(a',b')`", + Ints.NUMBER_RULE + `!a b a' b'. ~(gcd(a,b) = 0) /\ a = a' * gcd(a,b) /\ b = b' * gcd(a,b) + ==> coprime(a',b')`; + "ONCE_ASM_REWRITE_RULE " ^ theorem_fingerprints ^ " THM 975856962495483397", + ONCE_ASM_REWRITE_RULE theorems Sets.IN_UNION; + "ONCE_REWRITE_RULE " ^ theorem_fingerprints ^ " THM 345492714299286815", + ONCE_REWRITE_RULE theorems Sets.INSERT; + "ONCE_SIMP_RULE " ^ theorem_fingerprints ^ " THM 4052081339122143671", + ONCE_SIMP_RULE theorems Sets.FORALL_IN_UNION; + "PURE_ASM_REWRITE_RULE " ^ theorem_fingerprints ^ " THM 3653885712938130508", + PURE_ASM_REWRITE_RULE theorems (ASSUME `p /\ q`); + "PURE_ONCE_ASM_REWRITE_RULE " ^ theorem_fingerprints ^ " THM 1748915323273844750", + PURE_ONCE_ASM_REWRITE_RULE theorems (ASSUME `f = ((\x y. x + y) y)`); + "PURE_ONCE_REWRITE_RULE " ^ theorem_fingerprints ^ " THM 237159312591742290", + PURE_ONCE_REWRITE_RULE theorems (Equal.SYM(ASSUME `x:num = y`)); + "PURE_REWRITE_RULE " ^ theorem_fingerprints ^ " THM 1636085460980557391", + PURE_REWRITE_RULE theorems (Bool.SPEC_ALL Arith.GT); + "PURE_SIMP_RULE [ ] THM 3093559110319623167", + PURE_SIMP_RULE [] (Class.TAUT `p /\ q ==> q /\ p`); + "REWRITE_RULE " ^ theorem_fingerprints ^ " THM 3093559110319623167", + REWRITE_RULE theorems (Class.TAUT `p /\ q ==> q /\ p`); + "SELECT_RULE THM 650638948164601243", + Class.SELECT_RULE (Nums.INFINITY_AX); + "SET_RULE `{x | ~(x IN s <=> x IN t)} = (s DIFF t) UNION (t DIFF s)`", + Sets.SET_RULE `{x | ~(x IN s <=> x IN t)} = (s DIFF t) UNION (t DIFF s)`; + "SIMP_RULE " ^ theorem_fingerprints ^ " THM 3093559110319623167", + SIMP_RULE theorems (Class.TAUT `p /\ q ==> q /\ p`); + "SPEC_ALL THM 4052081339122143671", + Bool.SPEC_ALL Sets.FORALL_IN_UNION; + "CONJ THM 3093559110319623167 THM 262723677586854601", + Bool.CONJ (Class.TAUT `p /\ q ==> q /\ p`) (Class.TAUT `q /\ p ==> p /\ q`); + "CONJUNCT1 THM 3653885712938130508", + Bool.CONJUNCT1 (ASSUME `p /\ q`); + "CONJUNCT2 THM 3653885712938130508", + Bool.CONJUNCT2 (ASSUME `p /\ q`); + "DISCH_ALL THM 2661800747689726299", + Bool.DISCH_ALL (Bool.ADD_ASSUM false_term (ASSUME true_term)); + "MATCH_MP THM 3093559110319623167 THM 3653885712938130508", + Drule.MATCH_MP (Class.TAUT `p /\ q ==> q /\ p`) (ASSUME `p /\ q`); + "MP THM 3093559110319623167 THM 3653885712938130508", + Bool.MP (Class.TAUT `p /\ q ==> q /\ p`) (ASSUME `p /\ q`); + "GEN_ALL THM 1636085460980557391", + Bool.GEN_ALL (Bool.SPEC_ALL Arith.GT); + "GSYM THM 237159312591742290", + Equal.GSYM (Equal.SYM(ASSUME `x:num = y`)); +];; + +let results: (thm * thm) list = + map (fun s, th -> (Parse_tactic.parse_rule s, th)) input_output in + let assert_equal_theorem_pair (th1, th2) = assert_normalized_equal_theorems th1 th2 in + register_tests "Parsed rules result in equal output theorems." + assert_equal_theorem_pair results;; + diff --git a/tests/run_tests.ml b/tests/run_tests.ml index 164daf9f..01626e41 100644 --- a/tests/run_tests.ml +++ b/tests/run_tests.ml @@ -19,3 +19,4 @@ printf "Running %d tests\n%!" total_tests;; List.iter run_test !test_cases;; printf "\nTests succeeded: %d\nTests failed: %d\n%!" !successful_tests !failed_tests;; + diff --git a/tests/test_common.ml b/tests/test_common.ml index 1dd987a9..39a89be9 100644 --- a/tests/test_common.ml +++ b/tests/test_common.ml @@ -23,15 +23,29 @@ let assert_equal (x: string) (y: string) = if String.equal x y then () else failwith (sprintf "Assertion failed: '%s' not equal to '%s'" x y);; +let assert_equal_list (x: string list) (y: string list) = + if length x == length y then () + else failwith (sprintf "Assertion failed: assert_equal_list: Different length lists "); + List.iter (fun a, e -> assert_equal a e) (zip x y);; + let assert_equal_generic (fmt: 'a -> string) (x: 'a) (y: 'a) = let x, y = fmt x, fmt y in assert_equal x y;; +let assert_equal_int (x: int) (y: int) = + assert_equal_generic (Printf.sprintf "%d") x y;; + let assert_equal_terms tm1 tm2 = assert_equal_generic (str_of_sexp o sexp_term) tm1 tm2;; let assert_equal_theorems th1 th2 = assert_equal_generic (str_of_sexp o sexp_thm) th1 th2;; +(* S-expression of th1 and th2 are equal after normalizing. *) +let assert_normalized_equal_theorems th1 th2 = + assert_equal_theorems + (Normalize.normalize_theorem th1) + (Normalize.normalize_theorem th2);; + let assert_idempotent (assert_equal: 'a -> 'a -> unit) (f: 'a -> 'a) (x: 'a) = assert_equal (f x) (f (f x));; diff --git a/theorem_fingerprint.ml b/theorem_fingerprint.ml index ea096a94..0efadf8e 100644 --- a/theorem_fingerprint.ml +++ b/theorem_fingerprint.ml @@ -4,16 +4,24 @@ open Lib;; open Fusion;; open Printer;; -external str_list_fingerprint : string list -> int = "TheoremFingerprint";; +external str_list_fingerprint : string -> string list -> int list -> int = "TheoremFingerprint";; +(* Second argument is only supposed to be a string, but that somehow didn't + work. Now we pass a string list of length 1. *) +(* external goal_int_fingerprint : int list -> string list -> int = "GoalFingerprint";; *) (* Fingerprinting for terms that are not considered theorems in the ocaml *) (* typesystem, but of which we know that they are theorems. *) (* USE WITH CARE! *) -let term_fingerprint ((hyp_terms, term): term list * term) : int = - str_list_fingerprint (List.map (str_of_sexp o sexp_term) (term::hyp_terms));; +let to_string = str_of_sexp o sexp_term;; +let term_fingerprint ((hyp_terms, concl): term list * term) : int = + str_list_fingerprint (to_string concl) (List.map to_string hyp_terms) [];; let fingerprint (th: thm) : int = term_fingerprint (dest_thm th);; +let goal_fingerprint ((assum, concl): thm list * term) : int = + let assum_fps = List.map fingerprint assum in + str_list_fingerprint ((str_of_sexp o sexp_term) concl) [] assum_fps;; + let theorem_index = Hashtbl.create 1000;; @@ -35,7 +43,7 @@ let index_thm (i: int) (thm: thm) : unit = else Hashtbl.add theorem_index i thm;; -let register_thm thm : unit = - if not (thm_is_known thm) - then index_thm (fingerprint thm) thm - else ();; +let register_thm thm : int = + let fp = fingerprint thm in + (if not (thm_is_known thm) then index_thm fp thm); + fp;; diff --git a/theorem_fingerprint_c.cc b/theorem_fingerprint_c.cc new file mode 100644 index 00000000..660c2eff --- /dev/null +++ b/theorem_fingerprint_c.cc @@ -0,0 +1,35 @@ +#include "caml/memory.h" +#include "caml/mlvalues.h" +#include "farmhash_compatibility.h" + + +namespace { +// The maximum signed int in 64-bit Ocaml is 2**62-1. +// We drop an additional bit to avoid unsigned->signed conversion subtleties. +constexpr uint64 kMask = (static_cast(1) << 62) - 1; +} // namespace + +extern "C" { + +CAMLprim value TheoremFingerprint(value concl_str, value hyp_strings, + value assum_fingerprints) { + CAMLparam3(concl_str, hyp_strings, assum_fingerprints); + // LINT.IfChange + uint64 result = farmhash::Fingerprint64(String_val(concl_str), + caml_string_length(concl_str)); + while (hyp_strings != Val_emptylist) { + const auto& s = Field(hyp_strings, 0); + uint64 f = farmhash::Fingerprint64(String_val(s), caml_string_length(s)); + result = farmhash::Fingerprint(result, f); + hyp_strings = Field(hyp_strings, 1); + } + while (assum_fingerprints != Val_emptylist) { + uint64 f = Long_val(Field(assum_fingerprints, 0)); + f = f + 1; // Ensures that "[t1 |- t2], t3" and "[|-t1, |-t2], t3" differ + result = farmhash::Fingerprint(result, f); + assum_fingerprints = Field(assum_fingerprints, 1); + } + CAMLreturn(Val_long(result & kMask)); + // LINT.ThenChange(//hol_light/api/theorem_fingerprint.cc) +} +}