(* initialization of search structures *) (* module Init = struct *) flyspeck_needs "usr/thales/searching.hl";; module Init_search = struct open Hales_tactic;; open Searching;; (* ========================================================================== *) (* REWRITE SUGGEST *) update_database();; (* let search_result_dump_march7_2012_8am = ["Trigonometry2.COLLINEAR_TRANSABLE"; "Trigonometry2.COLLINEAR_TRANSABLE"; "Trigonometry2.COLLINEAR_TRANSABLE"; "Trigonometry2.COLLINEAR_TRANSABLE"; "COLLINEAR_LEMMA_ALT"; "WEDGE_LUNE_GT"; "COLLINEAR_3_AFFINE_HULL"; "Sphere.aff"; "AFFINE_HULL_2_ALT"; "Marchal_cells_2.RADIAL_VS_RADIAL_NORM"; "Conforming.SOL_UNIONS"; "Vol1.sol"; "AFF_DIM_CONVEX_HULL"; "Hypermap.lemma_in_disjoint"; "FACE_OF_DISJOINT_INTERIOR"; "real_div"; "SUM_RMUL"; "VECTOR_MUL_RZERO"; "SUM_CLAUSES"; "Packing3.SING_UNION_EQ_INSERT"; "VSUM_LMUL"; "Collect_geom.IN_AFFINE_HULL_IMP_COLLINEAR"; "AFF_DIM_2"; "AFF_DIM_INSERT"; "AFF_DIM_SUBSET"; "Polyhedron.AFF_DIM_INTERIOR_EQ_3"; "AFF_DIM_EQ_AFFINE_HULL"; "CONVEX_HULL_EQ"; "Marchal_cells.CONVEX_HULL_SUBSET"; "Upfzbzm_support_lemmas.SUM_SET_OF_2_ELEMENTS"; "SUM_SUBSET_SIMPLE"; "HAS_SIZE_1_EXISTS"; "HAS_SIZE_0"; "SUM_UNION"; "SUM_POS_LE"; "sgn_gt"; "FACE_OF_IMP_CONVEX"; "POLYTOPE_UNION_CONVEX_HULL_FACETS"; "SUBSET_RELATIVE_INTERIOR"; "EXPLICIT_SUBSET_RELATIVE_INTERIOR_CONVEX_HULL"; "Geomdetail.SUM_DIS3"; "face_of"; "FACE_OF_CONVEX_HULL_SUBSET"; "Geomdetail.VSUM_DIS3"; "Collect_geom.NOT_COLLINEAR_IMP_2_UNEQUAL"; "Marchal_cells_2.VSUM_CLAUSES_alt"; "NOT_IN_EMPTY"; "UNION_EMPTY"; "aff_gt_def"; "CONVEX_AFF_GT"; "affsign"; "Sphere.aff_gt_def"; "AZIM_REFL"; "AZIM_BASE_SHIFT_LT"; "Counting_spheres.EMPTY_NOT_EXISTS_IN"; "wedge"; "NORM_NEG"; "dist"; "IN_BALL"; "VECTOR_MUL_ASSOC"; "Polyhedron.fchanged"; "NORMBALL_BALL"; "Sphere.radial"; "Polyhedron.CARD_SET_OF_EDGE_INEQ_1_POLYHEDRON"; "Polyhedron.POLYTOPE_FAN80"; "Conforming.PIIJBJK"; "Polyhedron.POLYHEDRON_FAN"; "Conforming.MEASURABLE_TOPOLOGICAL_COMPONENT_YFAN_INTER_BALL"; "Polyhedron.FCHANGED_IN_COMPONENT"; "primitive"; "MEASURABLE_RULES"; "Sphere.cone0"; "solid_triangle"; "Vol1.volume_prop_fix"; "Sphere.eventually_radial"; "MEASURABLE_BALL_WEDGE"; "MEASURE_SUBSET"; "NORM_EQ_0"; "DOT_EQ_0"; "NORM_POS_LE"; "Real_ext.REAL_PROP_NN_MUL2"; "Calc_derivative.invert_den_le"; "DOT_SYM"; "Collect_geom.EQ_POW2_COND"; "Trigonometry2.DIV_POW2"; "DOT_LZERO"; "Calc_derivative.invert_den_eq"; "VECTOR_MUL_EQ_0"; "REAL_EQ_MUL_LCANCEL"; "NORM_POS_LT"; "SQRT_POS_LT"; "ABS_SQUARE_LT_1"; "Calc_derivative.invert_den_lt"; "REAL_LT_MUL"; "Trigonometry1.DOT_COS"; "Trigonometry2.NOT_ZERO_EQ_POW2_LT"; "REAL_LT_MUL"; "REAL_LT_RMUL"; "Trigonometry2.UNIT_BOUNDED_IN_TOW_FORMS"; "SQRT_POW_2"; "NORM_EQ_0"; "Collect_geom.DIST_POW2_DOT"; "Tarjjuw.CHANGE_TARJJUW_4"; "NORM_POS_LE"; "Real_ext.REAL_PROP_NN_MUL2"; "NORM_POW_2"; "DOT_SQUARE_NORM"; "Trigonometry2.MUL_POW2"; "Tactics_jordan.REAL_POW_2_LT"; "DOT_SYM"; "Polyhedron.INTERIOR_AFFINIE_HUL_EQ_UNIV"; "Counting_spheres.affine_facet_hyper"; "RELATIVE_INTERIOR_SUBSET"; "INTERIOR_SUBSET_RELATIVE_INTERIOR"; "facet_of"; "POLYHEDRON_IMP_CONVEX"; "Ldurdpn.SUBSET_P_HULL"; "HULL_HULL"; "HULL_MONO"; "VECTOR_MUL_LID"; "Marchal_cells_2.AFFINE_SUBSET_KY_LEMMA"; "RELATIVE_INTERIOR_SUBSET"; "FACE_OF_STILLCONVEX"; "FACE_OF_DISJOINT_RELATIVE_INTERIOR"; "REAL_LT_MUL"; "REAL_LT_LMUL"; "REAL_LT_DIV"; "Local_lemmas.REAL_LT_DIV_NEG"; "Trigonometry2.LT_IMP_ABS_REFL"; "NORM_POW_2"; "NORM_MUL"; "DOT_LMUL"; "DIST_0"; "VECTOR_SUB_RZERO"; "rconesgn"; "rcone_gt"; "Polyhedron.REDUCE_POINT_FACET_EXISTS"; "POLYHEDRON_COLLINEAR_FACES"; "DOT_POS_LT"; "DOT_RZERO"; "facet_of"; "DOT_LMUL"; "Trigonometry2.EXISTS_OTHOR_VECTOR_DIFFF_VEC0"; "Trigonometry2.EXISTS_UNIT_OTHOR_VECTOR"; "INJECTIVE_PAD2D3D"; "COMPLEX_VEC_0"; "COMPLEX_VEC_0"; "Counting_spheres.facet_rep_def"; "CX_INJ"; "COMPLEX_NORM_CX"; "POLYTOPE_EQ_BOUNDED_POLYHEDRON"; "POLYTOPE_IMP_CONVEX"; "POLYTOPE_IMP_COMPACT"; "EXTREME_POINT_EXISTS_CONVEX"; "FACE_OF_SING"; "FACE_OF_POLYHEDRON_SUBSET_FACET"; "POLYTOPE_FACET_EXISTS"];; let remove_work_in_progress = Lib.subtract search_result_dump_march7_2012_8am ["AZIM_BASE_SHIFT_LT"];; map refresh_rewrite_stag remove_work_in_progress;; (* augment_search_results search_result_dump_march7_2012_8am;; *) remove_rewrite_tag "POLYHEDRON_COLLINEAR_FACES";; map refresh_rewrite_stag ["SQRT_POS_LE";"SUBSET_INTER";"VECTOR_MUL_RZERO";"VECTOR_ADD_RID"; "VECTOR_SUB_RZERO";"VECTOR_ADD_LID";"VECTOR_SUB_LZERO";"IN_UNIV"; "Local_lemmas.EXISTS_IN";"Collect_geom.IN_SET2";"DOT_RMUL";"DOT_LMUL"; "FORALL_PAIR_THM";"EXISTS_PAIRED_THM";"Hales_tactic.GSYM_EXISTS_PAIRED_THM"; "IN_SING"];; *) (* ========================================================================== *) (* tactic patterns *) map add_tactic_pattern [(match_g[`(@):(A->bool)->A`],"SELECT_ELIM_TAC","remove @", fun t-> SELECT_ELIM_TAC); (match_g[`(@):(A->bool)->A`],"SELECT_TAC","remove @ with subgoals", fun t-> SELECT_TAC); (match_g[full `(\x. f x = \x. g x)`],"ABS_TAC","strip abstractions from equality", fun t-> ABS_TAC); (match_g[full ` ((p ==> q) ==> r)`],"ANTS_TAC","ants", fun t-> ANTS_TAC); (match_g_no_ho[full ` (f x = g x)`],"AP_THM_TAC","drop the function argument", fun t-> AP_THM_TAC); (match_g_no_ho[full ` (f x y = f x' y)`],"AP_THM_TAC THEN AP_TERM_TAC","show first args of a binary function are equal", fun t-> AP_THM_TAC THEN AP_TERM_TAC); (match_g[`(\x. f) y`],"BETA_TAC","beta reduce", fun t-> BETA_TAC); (match_g[full ` (f x y = f x' y')`],"BINOP_TAC","show binary function args equal", fun t-> BINOP_TAC); (match_g[full ` (f x = f x' )`],"AP_TERM_TAC","show function args equal", fun t-> AP_TERM_TAC); (match_g[full `(a /\ b)`],"CONJ_TAC","split into two subgoals", fun t-> CONJ_TAC); (match_g[full `(a ==>b)`],"DISCH_TAC","discharge antecedent", fun t -> DISCH_TAC); (match_g[full `(a <=> b)`],"EQ_TAC","split <=> into two conditionals", fun t -> EQ_TAC); (match_g[full `(?x. t)`],"EXISTS_TAC","specify existence", fun t -> failwith "syntax: EXISTS_TAC `u`"); (match_g[full `(!x. t)`],"GEN_TAC","remove universal", fun t-> GEN_TAC); (match_g[full `((f:A->B) = g)`],"MATCH_MP_TAC EQ_EXT","apply to arg", fun t-> MATCH_MP_TAC EQ_EXT); (* was ONCE_REWRITE_TAC[FUN_EQ_THM] *) (match_g[full `(!(x:num). t)`],"INDUCT_TAC","induction", fun t->INDUCT_TAC); (match_g[full `(!(n:A list). P)`],"LIST_INDUCT_TAC","structure induction on lists", fun t->LIST_INDUCT_TAC); (match_g[full `(f x = g y)`],"MK_COMB_TAC","show equality of functions and args", fun t->MK_COMB_TAC); (match_g[full`x <= (z:real)`],"MATCH_MP_TAC REAL_LE_TRANS","x <= y /\ y <= z ", fun t -> MATCH_MP_TAC REAL_LE_TRANS); (match_g[full`x < (z:real)`],"MATCH_MP_TAC REAL_LET_TRANS","x <= y /\ y < z ", fun t -> MATCH_MP_TAC REAL_LET_TRANS); (match_g[full`x < (z:real)`],"MATCH_MP_TAC REAL_LTE_TRANS","x < y /\ y <= z", fun t -> MATCH_MP_TAC REAL_LTE_TRANS); (match_asm[ full `x \/ y`],"FIRST_X_ASSUM DISJ_CASES_TAC","split x \/ y assumption", fun t -> FIRST_X_ASSUM DISJ_CASES_TAC); (match_asm[full `?(x:A). y`],"FIRST_X_ASSUM CHOOSE_TAC","choose existential quant in assumption list", fun t-> FIRST_X_ASSUM CHOOSE_TAC); (match_asm[full `x /\ y`],"FIRST_X_ASSUM (CONJUNCTS_THEN ASSUME_TAC)","split asumption conjunction", fun t->FIRST_X_ASSUM (CONJUNCTS_THEN ASSUME_TAC)); ];; add_tactic_pattern (match_g[`let x = (y:A) in (z:B)`],"LET_TAC","let elimination", fun t -> LET_TAC);; add_tactic_pattern (match_g[full `(a:A->bool) = b`],"MATCH_MP_TAC SUBSET_ANTISYM", "subset conjunction", fun t -> MATCH_MP_TAC SUBSET_ANTISYM);; (* ========================================================================== *) (* ABBREVIATIONS OF TACTICS *) tactic_abbreviations:= [ ("fun","fun"); ("then","THEN"); ("real","REAL_ARITH_TAC"); ("se","SELECT_TAC"); ("if","COND_CASES_TAC"); ("cc","COND_CASES_TAC"); ("r","REWRITE_TAC"); ("mp","MP_TAC"); ("ra","REAL_ARITH"); ("aru","ARITH_RULE"); ("field","REAL_FIELD"); ("fieldt","(CONV_TAC REAL_FIELD)"); ("ar","ASM_REWRITE_TAC"); ("hc","HYP_CONJ_TAC"); ("rt/a","ASM_REWRITE_TAC"); ("r/a","ASM_REWRITE_TAC"); ("r/o","ONCE_REWRITE_TAC"); ("rt/o","ONCE_REWRITE_TAC"); ("mmp","MATCH_MP_TAC"); ("st","WEAKER_STRIP_TAC"); ("st/r","REPEAT WEAKER_STRIP_TAC"); ("str","STRIP_TAC"); ("str/r","REPEAT STRIP_TAC"); ("e","EXISTS_TAC"); ("m","MESON_TAC"); ("mt/a","ASM_MESON_TAC"); ("m/a","ASM_MESON_TAC"); ("am","ASM_MESON_TAC"); ("c","CONJ_TAC"); ("a","ASSUME_TAC"); ("g","GEN_TAC"); ("g/r","REPEAT GEN_TAC"); ("sc","SUBCONJ_TAC"); ("su","SUBST1_TAC"); ("si","SIMP_TAC"); ("si/a","ASM_SIMP_TAC"); ("asi","ASM_SIMP_TAC"); ("sg","SUBGOAL_THEN"); ("d","DISCH_TAC"); ("an","ANTS_TAC"); ("le","LET_TAC"); ("l","LET_TAC"); ("rat","REAL_ARITH_TAC"); ("p","POP_ASSUM"); ("p/r","REPEAT POP_ASSUM"); ("by","BY"); ("exv","EXISTSv_TAC"); ("mu", "MESON"); ("gv","X_GENv_TAC"); ("sym","GSYM"); ("specl","ISPECL"); ("spec","ISPEC"); ("o","o"); ("rr","REWRITE_RULE"); ("orr","ONCE_REWRITE_RULE"); ("pbc","PROOF_BY_CONTR_TAC"); ("taut","TAUT"); ("snd","snd"); ("asl","asl"); ("let","let"); ("in","in"); ("@","SELECT_TAC"); ("/\\","CONJ_TAC"); ("!","GEN_TAC"); ];; abbrev ("fexp","FULL_EXPAND_TAC");; abbrev ("ispecl","ISPECL");; abbrev ("ispec","ISPEC");; abbrev ("t","t");; abbrev ("beta","BETA_TAC");; abbrev ("subconj","SUBCONJ_TAC");; abbrev ("fassum","FIRST_ASSUM");; abbrev ("fa","FIRST_ASSUM");; abbrev ("d/r","REPEAT DISCH_TAC");; abbrev ("comment","COMMENT");; abbrev ("name","NAME");; abbrev ("rot","ROT_TAC");; unabbrev ("rau");; abbrev ("arith","arith");; abbrev ("aa","ARITH_TAC");; abbrev ("rep","REPLICATE_TAC");; abbrev ("simp","SIMP_TAC");; abbrev ("contr","PROOF_BY_CONTR_TAC");; abbrev ("set","SET_TAC");; (* abbrev ("sth","SEARCH_THEN");;*) abbrev ("ets","ENOUGH_TO_SHOW_TAC");; abbrev ("mm","MATCH_MP");; abbrev ("calc","Calc_derivative.CALC_ID_TAC");; abbrev ("gm","GMATCH_SIMP_TAC");; abbrev ("w","w");; abbrev ("asl","asl");; abbrev ("replicate","replicate");; abbrev ("2","2");; abbrev ("fxast","FIRST_X_ASSUM_ST");; abbrev ("fast","FIRST_ASSUM_ST");; abbrev ("@","@");; abbrev ("map","map");; abbrev ("dt/r","REPEAT DISCH_TAC");; abbrev ("1","1");; abbrev ("2","2");; abbrev ("3","3");; abbrev ("4","4");; abbrev ("5","5");; abbrev ("uni","uni");; abbrev ("intro","INTRO_TAC");; abbrev ("conj2","CONJ2_TAC");; abbrev ("subconj2","SUBCONJ2_TAC");; abbrev ("name","RENAME_FREE_VAR");; abbrev ("rebind","REBIND_TAC");; abbrev ("s","s");; abbrev ("copy","COPY_TAC");; abbrev ("exl","GEXISTL_TAC");; abbrev ("orelse","ORELSE");; abbrev ("t","t");; abbrev ("typ","TYPIFY");; abbrev ("vat","VECTOR_ARITH_TAC");; abbrev ("smp","(C SUBGOAL_THEN MP_TAC)");; abbrev ("sat","(C SUBGOAL_THEN ASSUME_TAC)");; abbrev ("s1","(C SUBGOAL_THEN SUBST1_TAC)");; abbrev ("e","");; abbrev ("abbrev","TYPED_ABBREV_TAC");; abbrev ("strip/r","REPEAT STRIP_TAC");; abbrev ("act","act");; abbrev ("ls","LOCAL_STEP_TAC()");; abbrev ("ra","RULE_ASSUM_TAC");; abbrev ("rule","RULE_ASSUM_TAC");; abbrev ("asm","ASM_TAC");; abbrev ("gtyp","TYPIFY_GOAL_THEN");; abbrev ("setr","SET_RULE");; abbrev ("nconj","nCONJ_TAC");; abbrev ("nrt","NUM_REDUCE_TAC");; abbrev ("grt","GEN_REWRITE_TAC");; abbrev ("land","LAND_CONV");; abbrev ("rand","RAND_CONV");; abbrev ("odc","ONCE_DEPTH_CONV");; abbrev ("the","the");; (* follow your nose, type "fyn" to use *) add_your_nose(match_g[`&a + &b`],"REWRITE_TAC[REAL_OF_NUM_ADD]","&m + &n");; add_your_nose(match_g[`&a = &b`],"REWRITE_TAC[REAL_OF_NUM_EQ]","&m = &n");; add_your_nose(match_g[`&x < &y`],"REWRITE_TAC[ REAL_OF_NUM_LT]","&x < &y");; add_your_nose(match_g[`&x <= &y`],"REWRITE_TAC[ REAL_OF_NUM_LE]","&x <= &y");; add_your_nose(match_g[full `(!(x:A). t)`],"GEN_TAC","GEN_TAC");; add_your_nose(match_g[`&0 < sqrt x`],"GMATCH_SIMP_TAC SQRT_POS_LT","&0 < sqrt _");; add_your_nose(match_g[`&0 <= sqrt x`],"GMATCH_SIMP_TAC SQRT_POS_LE","&0 <= sqrt _");; add_your_nose(match_g[`x IN {}`],"REWRITE_TAC[NOT_IN_EMPTY]","_ IN {}");; add_your_nose(match_g[`sqrt x <= sqrt y`],"GMATCH_SIMP_TAC SQRT_MONO_LE_EQ","sqrt _ <= sqrt _");; add_your_nose(match_g[`sqrt x < sqrt y`],"GMATCH_SIMP_TAC SQRT_MONO_LT_EQ","sqrt _ < sqrt _");; add_your_nose(match_g[`&0 < x * y`],"GMATCH_SIMP_TAC REAL_LT_MUL_EQ","&0 < pos1 * pow2");; add_your_nose(match_g[`x * x <= y * y`],"GMATCH_SIMP_TAC Misc_defs_and_lemmas.ABS_SQUARE_LE","x * x <= y * y");; add_your_nose(match_g[`&0 <= x/y`],"GMATCH_SIMP_TAC REAL_LE_DIV","&0 <= x/y");; add_your_nose(match_g[`&0 <= x * y`],"GMATCH_SIMP_TAC REAL_LE_MUL","&0 <= x *y");; add_your_nose(match_g[`&0 <= x * x`],"REWRITE_TAC[ REAL_LE_SQUARE]","&0 <= x *y");; add_your_nose(match_g[`sqrt x pow 2`],"GMATCH_SIMP_TAC SQRT_POW_2","sqrt x pow 2");; add_your_nose(match_g[`x /z <= y`],"GMATCH_SIMP_TAC REAL_LE_LDIV_EQ","x /z <= y");; add_your_nose(match_g[`&0 <= x pow 2`],"REWRITE_TAC[ REAL_LE_POW_2]","&0 <= x pow 2");; add_your_nose(match_g[`x < sqrt y`],"GMATCH_SIMP_TAC REAL_LT_RSQRT","x < sqrt y");; add_your_nose(match_g[`x /z <= y/ z`],"GMATCH_SIMP_TAC REAL_LE_DIV2_EQ","x/z <= y/z");; add_your_nose(match_g[`sqrt(y*y)`],"GMATCH_SIMP_TAC Nonlinear_lemma.sqrtxx","sqrt(x*x)");; add_your_nose(match_g[`x * y <= x * z`],"GMATCH_SIMP_TAC Real_ext.REAL_LE_LMUL_IMP","x * y <= x * z");; add_your_nose(match_g[`x < y/ z`],"GMATCH_SIMP_TAC REAL_LT_RDIV_EQ","x < y/z");; add_your_nose(match_g[`&0 < x/y`],"GMATCH_SIMP_TAC REAL_LT_DIV","&0 < x/y");; add_your_nose(match_g[`sqrt x * sqrt y`],"GMATCH_SIMP_TAC (GSYM SQRT_MUL)","sqrt x * sqrt y");; add_your_nose(match_g[`x * x < y * y`],"GMATCH_SIMP_TAC Misc_defs_and_lemmas.ABS_SQUARE","x * x < y*y");; add_your_nose(match_g[`&0 < y pow 2`],"REWRITE_TAC[GSYM Trigonometry2.NOT_ZERO_EQ_POW2_LT]","&0 < x pow 2");; add_your_nose(match_g[`x * y < x * z`],"GMATCH_SIMP_TAC REAL_LT_LMUL_EQ","x * y < x*z");; add_your_nose(match_g[`sqrt x = &0`],"GMATCH_SIMP_TAC SQRT_EQ_0","sqrt x = &0");; add_your_nose(match_g[`x <= y/z`],"GMATCH_SIMP_TAC REAL_LE_RDIV_EQ","x <= y/z");; add_your_nose(match_g[`x * x < y * y`],"GMATCH_SIMP_TAC Misc_defs_and_lemmas.ABS_SQUARE","x * x < y * y");; add_your_nose(match_g[`inv y <= inv x`],"GMATCH_SIMP_TAC REAL_LE_INV2","inv y <= inv x");; add_your_nose(match_g[`&0 < inv x`],"GMATCH_SIMP_TAC REAL_LT_INV","&0 < inv x");; add_your_nose(match_g[`&0 <= inv x`],"REWRITE_TAC[REAL_LE_INV_EQ]","&0 <= inv x");; add_your_nose(match_g[`abs(a*b)`],"REWRITE_TAC[REAL_ABS_MUL]","abs(a*b)");; let gnose s t prompt = add_your_nose(match_g[t],"GMATCH_SIMP_TAC "^s,prompt);; let wnose s t prompt = add_your_nose(match_g[t],"REWRITE_TAC["^s^"]",prompt);; let mnose s t prompt = add_your_nose(match_g[t],"MATCH_MP_TAC "^s,prompt);; wnose "VECTOR_MUL_LCANCEL" `a % v = a % w` "a % v = a % w";; wnose "VECTOR_MUL_ASSOC" `a % b % w` "a % b % w";; wnose "VECTOR_MUL_LID" `&1 % w` "&1 % w`";; wnose "Counting_spheres.AZIM_NN" `&0 <= azim a b c d` "0 <= azim";; wnose "DIST_EQ_0" `dist(x,y) = &0` "dist(x,y) = &0";; wnose "DIST_REFL" `dist(x,x) = &0` "dist(x,x) = &0";; wnose "DIST_POS_LE" `&0 <= dist(x,y)` "&0 <= dist(x,y)";; wnose "VECTOR_SUB_RZERO" `v - vec 0` "v - vec 0";; wnose "GSYM DIST_NZ" `&0 < dist(x,y)` "&0 < dist(x,y)";; wnose "NORM_POS_LE" `&0 <= norm x` "&0 <= norm x";; wnose "NORM_MUL" `norm (a % w)` "norm (a % w)";; wnose "DOT_EQ_0" `w dot w = &0` "w dot w = &0";; wnose "GSYM REAL_EQ_SQUARE_ABS" `a pow 2 = b pow 2` "a pow 2 = b pow 2 <=> abs a = abs b";; wnose "NORM_EQ_0" `norm v = &0` "norm v = &0";; wnose "DOT_POS_LT" `&0 < x dot x` "&0 < x dot x";; wnose "WITHINREAL_UNIV" `net within (:real)` "within (:real)";; gnose "Merge_ineq.sqrtpow2" `sqrt x * sqrt x` "sqrt x * sqrt x";; gnose "(GSYM Trigonometry2.POW2_COND)" `a pow 2 <= b pow 2` "a pow 2 <= b pow 2";; wnose "POW_2_SQRT_ABS" `sqrt(x pow 2)` "sqrt (x pow 2)";; mnose "REAL_LE_RSQRT" `y <= sqrt x` "y <= sqrt x";; end;;