Skip to content

Conversion logging #4

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
szegedy wants to merge 4 commits into
base: master
Choose a base branch
from
Open

Conversion logging #4

Show file tree
Hide file tree
Changes from 2 commits
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
e001b69
Ruby script to find all parameters of CONV_TAC
szegedy Mar 28, 2017
8f46f59
Added loogging of CONV_TAC.
szegedy Mar 28, 2017
c8fad59
Added forgotten file log.ml
szegedy Mar 28, 2017
1357d91
Merge remote-tracking branch 'origin/master'
szegedy Mar 28, 2017
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
4 changes: 2 additions & 2 deletions 100/arithmetic_geometric_mean.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -13,7 +13,7 @@ prioritize_real();;
let LEMMA_1 = prove
(`!x n. x pow (n + 1) - (&n + &1) * x + &n =
(x - &1) pow 2 * sum(1..n) (\k. &k * x pow (n - k))`,
CONV_TAC(ONCE_DEPTH_CONV SYM_CONV) THEN GEN_TAC THEN INDUCT_TAC THEN
(CONV_TAC "(ONCE_DEPTH_CONV SYM_CONV)") (ONCE_DEPTH_CONV SYM_CONV) THEN GEN_TAC THEN INDUCT_TAC THEN
REWRITE_TAC[SUM_CLAUSES_NUMSEG; ARITH_EQ; ADD_CLAUSES] THENL
[REAL_ARITH_TAC; REWRITE_TAC[ARITH_RULE `1 <= SUC n`]] THEN
SIMP_TAC[ARITH_RULE `k <= n ==> SUC n - k = SUC(n - k)`; SUB_REFL] THEN
Expand Down Expand Up @@ -57,7 +57,7 @@ let LEMMA_3 = prove
ASM_SIMP_TAC[REAL_LE_RDIV_EQ; REAL_POW_LT] THEN
MATCH_MP_TAC EQ_IMP THEN AP_THM_TAC THEN AP_TERM_TAC THEN
REWRITE_TAC[REAL_POW_ADD] THEN UNDISCH_TAC `~(b = &0)` THEN
CONV_TAC REAL_FIELD);;
(CONV_TAC "REAL_FIELD") REAL_FIELD);;

let AGM = prove
(`!n a. 1 <= n /\ (!i. 1 <= i /\ i <= n ==> &0 <= a(i))
Expand Down
14 changes: 7 additions & 7 deletions 100/ballot.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -42,7 +42,7 @@ let HAS_SIZE_FUNSPACE = prove
ONCE_REWRITE_TAC[TAUT `(a /\ b /\ c) /\ d <=> d /\ a /\ b /\ c`] THEN
REWRITE_TAC[PAIR_EQ; EXISTS_PAIR_THM; GSYM CONJ_ASSOC] THEN
REWRITE_TAC[RIGHT_EXISTS_AND_THM; UNWIND_THM1] THEN
CONV_TAC(ONCE_DEPTH_CONV GEN_BETA_CONV) THEN
(CONV_TAC "(ONCE_DEPTH_CONV GEN_BETA_CONV)") (ONCE_DEPTH_CONV GEN_BETA_CONV) THEN
X_GEN_TAC `f:A->B` THEN EQ_TAC THENL
[STRIP_TAC THEN MAP_EVERY EXISTS_TAC
[`(f:A->B) x`; `\u. if u = x then @y. T else (f:A->B) u`] THEN
Expand All @@ -54,7 +54,7 @@ let HAS_SIZE_FUNSPACE = prove
ALL_TAC] THEN
MATCH_MP_TAC HAS_SIZE_IMAGE_INJ THEN CONJ_TAC THENL
[REWRITE_TAC[FORALL_PAIR_THM; IN_ELIM_THM] THEN
CONV_TAC(ONCE_DEPTH_CONV GEN_BETA_CONV) THEN
(CONV_TAC "(ONCE_DEPTH_CONV GEN_BETA_CONV)") (ONCE_DEPTH_CONV GEN_BETA_CONV) THEN
ONCE_REWRITE_TAC[TAUT `(a /\ b) /\ d <=> d /\ a /\ b`] THEN
REWRITE_TAC[PAIR_EQ; EXISTS_PAIR_THM; GSYM CONJ_ASSOC] THEN
REWRITE_TAC[RIGHT_EXISTS_AND_THM; UNWIND_THM1] THEN
Expand Down Expand Up @@ -179,7 +179,7 @@ let COUNTING_LEMMA = prove
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
CONJ_TAC THENL
[CONV_TAC SYM_CONV THEN MATCH_MP_TAC CARD_UNION_EQ THEN
[(CONV_TAC "SYM_CONV") SYM_CONV THEN MATCH_MP_TAC CARD_UNION_EQ THEN
REWRITE_TAC[FINITE_COUNTINGS; EXTENSION; IN_INTER; IN_UNION] THEN
REWRITE_TAC[IN_ELIM_THM; NOT_IN_EMPTY] THEN
MESON_TAC[vote_CASES; vote_DISTINCT];
Expand Down Expand Up @@ -252,7 +252,7 @@ let ALL_COUNTINGS_SUC = prove
SUBST1_TAC(ARITH_RULE `(a + 1) + (b + 1) = (a + b + 1) + 1`) THEN
SUBST1_TAC(ARITH_RULE `(a + 1) + b = a + b + 1`) THEN
ABBREV_TAC `n = a + b + 1` THEN
CONV_TAC(ONCE_DEPTH_CONV let_CONV) THEN
(CONV_TAC "(ONCE_DEPTH_CONV let_CONV)") (ONCE_DEPTH_CONV let_CONV) THEN
GEN_REWRITE_TAC LAND_CONV [COUNTING_LEMMA] THEN
REWRITE_TAC[] THEN BINOP_TAC THEN
ONCE_REWRITE_TAC[COND_RAND] THEN ONCE_REWRITE_TAC[COND_RATOR] THEN
Expand All @@ -270,7 +270,7 @@ let VALID_COUNTINGS_SUC = prove
SUBST1_TAC(ARITH_RULE `(a + 1) + (b + 1) = (a + b + 1) + 1`) THEN
SUBST1_TAC(ARITH_RULE `(a + 1) + b = a + b + 1`) THEN
ABBREV_TAC `n = a + b + 1` THEN
CONV_TAC(ONCE_DEPTH_CONV let_CONV) THEN
(CONV_TAC "(ONCE_DEPTH_CONV let_CONV)") (ONCE_DEPTH_CONV let_CONV) THEN
GEN_REWRITE_TAC LAND_CONV [COUNTING_LEMMA] THEN REWRITE_TAC[] THEN
ONCE_REWRITE_TAC[COND_RAND] THEN ONCE_REWRITE_TAC[COND_RATOR] THEN
REWRITE_TAC[vote_DISTINCT] THEN
Expand Down Expand Up @@ -326,7 +326,7 @@ let VALID_COUNTINGS = prove
ASM_SIMP_TAC[GSYM REAL_OF_NUM_EQ; GSYM REAL_OF_NUM_MUL; GSYM REAL_OF_NUM_ADD;
GSYM REAL_OF_NUM_SUC; GSYM REAL_OF_NUM_SUB; REAL_OF_NUM_LE; LT_NZ;
ARITH_RULE `~(a <= b) ==> b <= SUC a /\ SUC b <= a /\ SUC b <= SUC a`] THEN
CONV_TAC REAL_RING);;
(CONV_TAC "REAL_RING") REAL_RING);;

let BALLOT = prove
(`!a b. &(valid_countings a b) =
Expand All @@ -344,4 +344,4 @@ let BALLOT = prove
ASM_SIMP_TAC[GSYM REAL_OF_NUM_EQ; GSYM REAL_OF_NUM_MUL; GSYM REAL_OF_NUM_ADD;
GSYM REAL_OF_NUM_SUC; GSYM REAL_OF_NUM_SUB;
ARITH_RULE `~(a <= b) ==> SUC b <= SUC a`] THEN
CONV_TAC REAL_FIELD);;
(CONV_TAC "REAL_FIELD") REAL_FIELD);;
6 changes: 3 additions & 3 deletions 100/bernoulli.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -86,7 +86,7 @@ let DIFF_BERNPOLY = prove
ASM_SIMP_TAC[GSYM REAL_OF_NUM_SUB; ARITH_RULE `k <= n ==> k <= n + 1`] THEN
UNDISCH_TAC `k <= n:num` THEN
REWRITE_TAC[GSYM REAL_OF_NUM_ADD; GSYM REAL_OF_NUM_LE] THEN
ABBREV_TAC `z = x pow (n - k)` THEN CONV_TAC REAL_FIELD);;
ABBREV_TAC `z = x pow (n - k)` THEN (CONV_TAC "REAL_FIELD") REAL_FIELD);;

(* ------------------------------------------------------------------------- *)
(* Hence the key stepping recurrence. *)
Expand Down Expand Up @@ -125,7 +125,7 @@ let RECURRENCE_BERNPOLY = prove
REWRITE_TAC[real_pow; REAL_MUL_LZERO; REAL_SUB_RZERO; REAL_MUL_RID] THEN
REWRITE_TAC[BERNOULLI; ADD1] THEN
COND_CASES_TAC THEN ASM_REWRITE_TAC[ARITH; real_pow; REAL_MUL_LID] THEN
CONV_TAC SYM_CONV THEN REWRITE_TAC[REAL_ENTIRE; REAL_POW_EQ_0] THEN
(CONV_TAC "SYM_CONV") SYM_CONV THEN REWRITE_TAC[REAL_ENTIRE; REAL_POW_EQ_0] THEN
ASM_REWRITE_TAC[ADD_SUB]);;

(* ------------------------------------------------------------------------- *)
Expand Down Expand Up @@ -163,7 +163,7 @@ let SUM_CONV =
let BINOM_CONV =
let pth = prove
(`a * b * x = FACT c ==> x = (FACT c) DIV (a * b)`,
REPEAT STRIP_TAC THEN CONV_TAC SYM_CONV THEN
REPEAT STRIP_TAC THEN (CONV_TAC "SYM_CONV") SYM_CONV THEN
MATCH_MP_TAC DIV_UNIQ THEN EXISTS_TAC `0` THEN CONJ_TAC THENL
[POP_ASSUM MP_TAC THEN ARITH_TAC;
POP_ASSUM MP_TAC THEN ONCE_REWRITE_TAC[GSYM CONTRAPOS_THM] THEN
Expand Down
Loading