(* 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;;