formal_ineqs/lib/ssreflect/ssreflect.hl

   1 (* =========================================================== *)
   2 (* SSReflect/HOL Light support library                         *)
   3 (* See http://code.google.com/p/flyspeck/downloads/list        *)
   4 (* Author: Alexey Solovyev                                     *)
   5 (* Date: 2012-10-27                                            *)
   6 (* =========================================================== *)
   7
   8 (* A special definition for introducing equalities with the construction move eq: a => b *)
   9 let ssreflect_eq_def = new_definition `!v P. ssreflect_eq (v:A) (P:bool) = P`;;
  10
  11
  12 (* Generalizes given variables in a term *)
  13 let gen_variables binders tm =
  14   if type_of tm <> bool_ty then
  15     if length binders = 0 then tm
  16     else
  17       failwith "gen_variables: bool term is required"
  18   else
  19     let f_vars = map dest_var (frees tm) in
  20     let find_type name = assoc name f_vars in
  21     let gen_variable var_name tm =
  22       let var =
  23         try mk_var (var_name, find_type var_name)
  24         with Failure _ ->
  25           failwith ("gen_variables: variable "^var_name
  26                     ^" is not free in the term "^(string_of_term tm)) in
  27         mk_forall (var, tm) in
  28       itlist gen_variable binders tm;;
  29
  30
  31 (* Combined type of theorems and terms *)
  32 type arg_type = Arg_theorem of thm | Arg_term of term | Arg_type of hol_type;;
  33
  34 let get_arg_thm arg =
  35   match arg with
  36     | Arg_theorem th -> th
  37     | _ -> failwith "A theorem expected";;
  38
  39 let get_arg_term arg =
  40   match arg with
  41     | Arg_term tm -> tm
  42     | _ -> failwith "A term expected";;
  43
  44 let get_arg_type arg =
  45   match arg with
  46     | Arg_type ty -> ty
  47     | _ -> failwith "A type expected";;
  48
  49
  50 (* Converts a theorem tactic into a tactic which accepts thm_term arguments *)
  51 let thm_tac (ttac : thm_tactic) = ttac o get_arg_thm;;
  52 let term_tac (ttac : term -> tactic) = ttac o get_arg_term;;
  53 let type_tac (ttac : hol_type -> tactic) arg = ttac o get_arg_type;;
  54
  55
  56 let conv_thm_tac (ttac : thm_tactic->tactic) (arg_tac : arg_type->tactic) =
  57   ttac (fun th -> arg_tac (Arg_theorem th));;
  58
  59
  60
  61 (* Based on the code from tactics.ml *)
  62 (* Applies the second tactic to either the first subgoal or
  63    the last subgoal *)
  64 let (THENL_FIRST),(THENL_LAST) =
  65   let propagate_empty i [] = []
  66   and propagate_thm th i [] = INSTANTIATE_ALL i th in
  67   let compose_justs n just1 just2 i ths =
  68     let ths1,ths2 = chop_list n ths in
  69     (just1 i ths1)::(just2 i ths2) in
  70   let rec seqapply l1 l2 = match (l1,l2) with
  71      ([],[]) -> null_meta,[],propagate_empty
  72    | ((tac:tactic)::tacs),((goal:goal)::goals) ->
  73             let ((mvs1,insts1),gls1,just1) = tac goal in
  74             let goals' = map (inst_goal insts1) goals in
  75             let ((mvs2,insts2),gls2,just2) = seqapply tacs goals' in
  76             ((union mvs1 mvs2,compose_insts insts1 insts2),
  77              gls1@gls2,compose_justs (length gls1) just1 just2)
  78    | _,_ -> failwith "seqapply: Length mismatch" in
  79   let justsequence just1 just2 insts2 i ths =
  80     just1 (compose_insts insts2 i) (just2 i ths) in
  81   let tacsequence ((mvs1,insts1),gls1,just1) tacl =
  82     let ((mvs2,insts2),gls2,just2) = seqapply tacl gls1 in
  83     let jst = justsequence just1 just2 insts2 in
  84     let just = if gls2 = [] then propagate_thm (jst null_inst []) else jst in
  85     ((union mvs1 mvs2,compose_insts insts1 insts2),gls2,just) in
  86   let (thenl_first: tactic -> tactic -> tactic) =
  87     fun tac1 tac2 g ->
  88       let _,gls,_ as gstate = tac1 g in
  89         if gls = [] then failwith "No subgoals"
  90         else
  91           let tac_list = tac2 :: (replicate ALL_TAC (length gls - 1)) in
  92             tacsequence gstate tac_list
  93   and (thenl_last: tactic -> tactic -> tactic) =
  94     fun tac1 tac2 g ->
  95       let _,gls,_ as gstate = tac1 g in
  96         if gls = [] then failwith "No subgoals"
  97         else
  98           let tac_list = (replicate ALL_TAC (length gls - 1)) @ [tac2] in
  99             tacsequence gstate tac_list in
 100     thenl_first, thenl_last;;
 101
 102
 103 (* Rotates the goalstack *)
 104 let (THENL_ROT: int -> tactic -> tactic) =
 105   fun n tac g ->
 106     let gstate = tac g in
 107       rotate n gstate;;
 108
 109
 110 (* Repeats the given tactic exactly n times and then repeats the same tactic at most m times *)
 111 let repeat_tactic n m tac =
 112   let rec replicate_at_most m tac =
 113     if m <= 0 then ALL_TAC else (tac THEN replicate_at_most (m - 1) tac) ORELSE ALL_TAC in
 114   REPLICATE_TAC n tac THEN replicate_at_most m tac;;
 115
 116
 117
 118 (* Returns all free variables in the goal *)
 119 let get_context_vars (g : goal) =
 120   let list, g_tm = g in
 121   let tms = g_tm :: map (concl o snd) list in
 122   let f_vars = setify (flat (map frees tms)) in
 123     map (fun v -> ((fst o dest_var) v, v)) f_vars;;
 124
 125
 126 (* Clears the given assumption *)
 127 let clear_assumption name =
 128   TRY (REMOVE_THEN name (fun th -> ALL_TAC));;
 129
 130
 131 (* DISCH_THEN (LABEL_TAC name) for assumptions and X_GEN_TAC name for variables *)
 132 let move labels =
 133   (* Automatically introduces an assumption for a top-level ssreflect_eq *)
 134   let move_eq (g:goal) =
 135     let g_tm = snd g in
 136     let tac =
 137       try
 138         let eq_tm = (rator o fst o dest_imp) g_tm in
 139           if (fst o dest_const o rator) eq_tm = "ssreflect_eq" then
 140             let label = (fst o dest_var o rand) eq_tm in
 141               DISCH_THEN (LABEL_TAC label o PURE_ONCE_REWRITE_RULE[ssreflect_eq_def])
 142           else
 143             ALL_TAC
 144       with Failure _ -> ALL_TAC in
 145       tac g in
 146
 147   let move1 name (g:goal) =
 148     let g_tm = snd g in
 149     let tac =
 150       if is_forall g_tm then
 151         let tm0, g_tm1 = dest_forall g_tm in
 152         let tm = mk_var (name, type_of tm0) in
 153           if name = "_" then
 154             GEN_TAC
 155           else
 156             X_GEN_TAC tm
 157       else
 158         if is_imp g_tm then
 159           if name = "_" then
 160             DISCH_THEN (fun th -> ALL_TAC)
 161           else
 162             DISCH_THEN (LABEL_TAC name)
 163         else
 164           failwith "move: not (!) or (==>)" in
 165       tac g in
 166     fun g ->
 167       let tac = itlist
 168         (fun name tac -> move_eq THEN move1 name THEN tac) labels ALL_TAC in
 169         tac g;;
 170
 171
 172 (* Localization tactical *)
 173 let in_tac a_list in_goal tac (g:goal) =
 174   let goal_tm = snd g in
 175   let tmp_goal_name = "$_goal_$" in
 176   let tmp_goal_var = mk_var (tmp_goal_name, bool_ty) in
 177   let tmp_goal = mk_eq (tmp_goal_var, goal_tm) in
 178   let tmp_goal_sym = mk_eq (goal_tm, tmp_goal_var) in
 179   let disch_tac =
 180     rev_itlist (fun name tac -> REMOVE_THEN name MP_TAC THEN tac) a_list ALL_TAC in
 181   let intro_tac = move a_list in
 182   let hide_goal, unfold_goal =
 183     if in_goal then
 184       ALL_TAC, ALL_TAC
 185     else
 186       ABBREV_TAC tmp_goal,
 187     EXPAND_TAC tmp_goal_name THEN
 188       UNDISCH_TAC tmp_goal_sym THEN DISCH_THEN (fun th -> ALL_TAC)
 189   in
 190     (hide_goal THEN disch_tac THEN tac THEN TRY intro_tac THEN unfold_goal) g;;
 191
 192
 193
 194 (* Finds a subterm in the given term which matches against the given
 195    pattern; local_consts is a list of variable which must be fixed in
 196    the pattern.
 197    This function returns the path to the first matched subterm *)
 198 let match_subterm local_consts pat tm =
 199   let rec find tm path =
 200     try
 201       let inst = term_match local_consts pat tm in
 202         if instantiate inst pat = tm then path else failwith "Bad instantiation"
 203     with x ->
 204       try
 205         match tm with
 206           | Abs(_, b_tm) -> find b_tm (path^"b")
 207           | Comb(l_tm, r_tm) ->
 208               try find l_tm (path^"l")
 209               with Failure _ -> find r_tm (path^"r")
 210           | _ -> failwith "match_subterm: no match"
 211       with x ->
 212         failwith ("match_subterm: no match: "^string_of_term pat) in
 213     find tm "";;
 214
 215
 216
 217 (* Returns paths to all subterms satisfying p *)
 218 let find_all_paths p tm =
 219   let rec find_path p tm path =
 220     let paths =
 221       match tm with
 222         | Abs(_, b_tm) ->
 223             find_path p b_tm (path ^ "b")
 224         | Comb(l_tm, r_tm) ->
 225             (find_path p l_tm (path ^ "l")) @ (find_path p r_tm (path ^ "r"))
 226         | _ -> [] in
 227       if p tm then path :: paths else paths in
 228     find_path p tm "";;
 229
 230
 231 (* Instantiates types of the given context variables in the given term.*)
 232 let inst_context_vars vars tm_vars tm =
 233   let find_type var =
 234     let name, ty = dest_var var in
 235       try
 236         (ty, type_of (assoc name vars))
 237       with Failure _ ->
 238         failwith (name^" is free in the term `"^(string_of_term tm)^"` and in the context") in
 239   let ty_src, ty_dst = unzip (map find_type tm_vars) in
 240   let ty_inst = itlist2 type_match ty_src ty_dst [] in
 241     inst ty_inst tm;;
 242
 243
 244 (* Instantiates types of all free variables in the term using the context *)
 245 let inst_all_free_vars tm (g : goal) =
 246   let context_vars = get_context_vars g in
 247   let f_vars = frees tm in
 248     inst_context_vars context_vars f_vars tm;;
 249
 250
 251 (* Finds a subterm corresponding to the given pattern.
 252    Before matching, the term types are instantiated in the given context. *)
 253 let match_subterm_in_context pat tm (g : goal) =
 254   let context_vars = get_context_vars g in
 255   let f0_vars = filter (fun tm -> ((fst o dest_var) tm).[0] <> '_') (frees pat) in
 256   let pattern = inst_context_vars context_vars f0_vars pat in
 257   let f1_vars = filter (fun tm -> ((fst o dest_var) tm).[0] <> '_') (frees pattern) in
 258     match_subterm f1_vars pattern tm;;
 259
 260
 261 (*************************)
 262 (*       Rewriting       *)
 263 (*************************)
 264
 265 (* Breaks conjunctions and does other misc stuff *)
 266 let rec break_conjuncts th : thm list =
 267   (* Convert P ==> (!x. Q x) to !x. P ==> Q x and P ==> Q ==> R to P /\ Q ==> R *)
 268   let th0 = PURE_REWRITE_RULE[GSYM RIGHT_FORALL_IMP_THM; IMP_IMP] th in
 269   let th1 = SPEC_ALL th0 in
 270   (* Break top level conjunctions *)
 271   let th_list = CONJUNCTS th1 in
 272     if length th_list > 1 then
 273       List.concat (map break_conjuncts th_list)
 274     else
 275       let th_tm = concl th1 in
 276         (* Deal with assumptions *)
 277         if is_imp th_tm then
 278           let a_tm = lhand th_tm in
 279           let th_list = break_conjuncts (UNDISCH th1) in
 280             map (DISCH a_tm) th_list
 281         else
 282           if is_eq th_tm then [th1]
 283           else
 284             if is_neg th_tm then
 285               [PURE_ONCE_REWRITE_RULE[TAUT `~P <=> (P <=> F)`] th1]
 286             else
 287               [EQT_INTRO th1];;
 288
 289
 290 (* Finds an instantination for the given term inside another term *)
 291 let rec find_term_inst local_consts tm src_tm path =
 292   try (term_match local_consts tm src_tm, true, path)
 293   with Failure _ ->
 294     match src_tm with
 295       | Comb(l_tm, r_tm) ->
 296           let r_inst, flag, s = find_term_inst local_consts tm l_tm (path ^ "l") in
 297             if flag then (r_inst, flag, s)
 298             else
 299               find_term_inst local_consts tm r_tm (path ^ "r")
 300       | Abs(_, b_tm) ->
 301           find_term_inst local_consts tm b_tm (path ^ "b")
 302       | _ -> (([],[],[]), false, path);;
 303
 304
 305
 306 (* Rewrites the subterm at the given path using the given equation theorem *)
 307 let path_rewrite path th tm =
 308   let rec build path tm =
 309     let n = String.length path in
 310       if n = 0 then
 311         th
 312       else
 313         let ch = path.[0] in
 314         let path' = String.sub path 1 (n - 1) in
 315           if ch = 'l' then
 316             let lhs, rhs = dest_comb tm in
 317             let th0 = build path' lhs in
 318               AP_THM th0 rhs
 319           else if ch = 'r' then
 320             let lhs, rhs = dest_comb tm in
 321             let th0 = build path' rhs in
 322               AP_TERM lhs th0
 323           else if ch = 'b' then
 324             let var, body = dest_abs tm in
 325             let th0 = build path' body in
 326               try ABS var th0
 327               with Failure _ -> failwith ("ABS failed: (" ^ string_of_term var ^ ", " ^ string_of_thm th0)
 328           else
 329             failwith ("Bad path symbol: "^path) in
 330   let res = build path tm in
 331   let lhs = (lhand o concl) res in
 332     if not (aconv lhs tm) then failwith ("path_rewrite: incorrect result [required: "^
 333                                   (string_of_term tm)^"; obtained: "^
 334                                   (string_of_term lhs))
 335     else
 336       res;;
 337
 338
 339 let new_rewrite occ pat th g =
 340   let goal_tm = snd g in
 341   (* Free variables in the given theorem will not be matched *)
 342   let local_consts = frees (concl th) in
 343   (* Apply the pattern *)
 344   let goal_subterm_path =
 345     if pat = [] then "" else match_subterm_in_context (hd pat) goal_tm g in
 346   let goal_subterm = follow_path goal_subterm_path goal_tm in
 347
 348   (* Local rewrite function *)
 349   let rewrite th =
 350     let concl_th = concl th in
 351     let cond_flag = is_imp concl_th in
 352     let match_fun = lhs o (if cond_flag then rand else I) in
 353
 354     (* Match the theorem *)
 355     let lhs_tm = match_fun concl_th in
 356     let ii, flag, path = find_term_inst local_consts lhs_tm goal_subterm goal_subterm_path in
 357       if not flag then
 358         failwith (string_of_term lhs_tm ^ " does not match any subterm in the goal")
 359       else
 360         let matched_th = INSTANTIATE ii th in
 361         let matched_tm = (match_fun o concl) matched_th in
 362
 363         (* Find all matched subterms *)
 364         let paths = find_all_paths (fun x -> aconv x matched_tm) goal_tm in
 365         let paths = if occ = [] then paths else
 366           map (fun i -> List.nth paths (i - 1)) occ in
 367
 368         (* Find all free variables in the matched theorem which do not correspond to free variables in
 369            the matched subterm *)
 370         let tm_frees = frees matched_tm in
 371         let mth_frees = frees (concl matched_th) in
 372         let vars = subtract mth_frees (union local_consts tm_frees) in
 373           if vars = [] then
 374             (* Construct the tactic for rewriting *)
 375             let r_tac = fun th -> MAP_EVERY (fun path -> CONV_TAC (path_rewrite path th)) paths in
 376               if cond_flag then
 377                 MP_TAC matched_th THEN ANTS_TAC THENL [ALL_TAC; DISCH_THEN r_tac]
 378               else
 379                 r_tac matched_th
 380           else
 381             let rec gen_vars vars th =
 382               match vars with
 383                 | v :: vs -> gen_vars vs (GEN v th)
 384                 | [] -> th in
 385             let th2 = gen_vars vars matched_th in
 386               MP_TAC th2 THEN PURE_REWRITE_TAC[LEFT_IMP_FORALL_THM] in
 387
 388   (* Try to rewrite with all given theorems *)
 389   let th_list = break_conjuncts th in
 390   let rec my_first th_list =
 391     if length th_list = 1 then
 392       rewrite (hd th_list) g
 393     else
 394       try rewrite (hd th_list) g
 395       with Failure _ -> my_first (tl th_list) in
 396     my_first th_list;;
 397
 398
 399 (*
 400 let th = ARITH_RULE `!n. n * 0 <= 1`;;
 401 let tm = `m * 0 <= 1 <=> T`;;
 402 g tm;;
 403 e(new_rewrite [] [] th);;
 404
 405 let th = CONJ REAL_MUL_RINV REAL_MUL_LINV;;
 406 let tm = `inv (x - y) * (x - y) + &1 = &1 + inv (x - y) * (x - y) + x * inv x`;;
 407 let tm0 = `!x. inv (x - y) * (x - y) = &1`;;
 408
 409
 410 g tm0;;
 411 e(new_rewrite [] [] (th));;
 412 e(new_rewrite [] [] (GSYM th));;
 413 e(new_rewrite [] [`_ + &1`] th);;
 414
 415 g(`x < 2`);;
 416 e(new_rewrite [] [] (ARITH_RULE `!x. x > 2 ==> (!n. n = 2 ==> ~(x < n))`));;
 417
 418 *)
 419
 420
 421 (* Rewrite tactic for usual and conditional theorems *)
 422 let rewrite occ pat th g =
 423   let rec match_theorem ffun th tm str =
 424     try (PART_MATCH ffun th tm, true, str)
 425     with Failure _ ->
 426       match tm with
 427         | Comb(l_tm, r_tm) ->
 428             let r_th, flag, s = match_theorem ffun th l_tm (str ^ "l") in
 429               if flag then (r_th, flag, s)
 430               else
 431                 match_theorem ffun th r_tm (str ^ "r")
 432         | Abs(_, b_tm) ->
 433             match_theorem ffun th b_tm (str ^ "b")
 434         | _ -> (th, false, str) in
 435   (* Initialize auxiliary variables *)
 436   let goal_tm = snd g in
 437   let th0 = PURE_REWRITE_RULE[IMP_IMP] th in
 438   let concl_th = concl (SPEC_ALL th0) in
 439   let cond_flag = is_imp concl_th in
 440   let eq_tm = if cond_flag then rand concl_th else concl_th in
 441   let match_fun = (if is_eq eq_tm then lhand else I) o (if cond_flag then rand else I) in
 442
 443   (* Apply the pattern *)
 444   let goal_subterm_path =
 445     if pat = [] then "" else match_subterm_in_context (hd pat) goal_tm g in
 446   let goal_subterm = follow_path goal_subterm_path goal_tm in
 447
 448   (* Match the theorem *)
 449   let matched_th, flag, path = match_theorem match_fun th0 goal_subterm goal_subterm_path in
 450   if not flag then
 451     failwith "lhs does not match any term in the goal"
 452   else
 453     let matched_tm = (match_fun o concl) matched_th in
 454     (* Find all matched subterms *)
 455     let paths = find_all_paths (fun x -> x = matched_tm) goal_tm in
 456     let paths = if occ = [] then paths else
 457       map (fun i -> List.nth paths (i - 1)) occ in
 458     (* Find all free variables in the matched theorem which do not correspond to free variables in
 459        the matched subterm *)
 460     let tm_frees = frees matched_tm in
 461     let th_frees = frees (concl th0) in
 462     let mth_frees = frees (concl matched_th) in
 463     let vars = subtract mth_frees (union th_frees tm_frees) in
 464       if vars = [] then
 465         let r_tac = fun th -> MAP_EVERY (fun path -> GEN_REWRITE_TAC (PATH_CONV path) [th]) paths in
 466           if cond_flag then
 467             (MP_TAC matched_th THEN ANTS_TAC THENL [ALL_TAC; DISCH_THEN r_tac]) g
 468           else
 469             (r_tac matched_th) g
 470       else
 471         let rec gen_vars vars th =
 472           match vars with
 473             | v :: vs -> gen_vars vs (GEN v th)
 474             | [] -> th in
 475         let th2 = gen_vars vars matched_th in
 476           (MP_TAC th2 THEN REWRITE_TAC[LEFT_IMP_FORALL_THM]) g;;
 477
 478
 479
 480
 481 (* Analogue of the "done" tactic in SSReflect *)
 482 let done_tac = ASM_REWRITE_TAC[] THEN FAIL_TAC "done: not all subgoals are proved";;
 483
 484 (* Simplification: /= *)
 485 let simp_tac = SIMP_TAC[];;
 486
 487
 488 (* Linear arithmetic simplification *)
 489 let arith_tac = FIRST [ARITH_TAC; REAL_ARITH_TAC; INT_ARITH_TAC];;
 490
 491
 492 (* split *)
 493 let split_tac = FIRST [CONJ_TAC; EQ_TAC];;
 494
 495
 496
 497 (* Creates an abbreviation for the given term with the given name *)
 498 let set_tac name tm (g : goal) =
 499   let goal_tm = snd g in
 500   let tm0 =
 501     try
 502       follow_path (match_subterm_in_context tm goal_tm g) goal_tm
 503     with Failure _ -> tm in
 504   let tm1 = inst_all_free_vars tm0 g in
 505   let abbrev_tm = mk_eq (mk_var (name, type_of tm1), tm1) in
 506     (ABBREV_TAC abbrev_tm THEN POP_ASSUM (LABEL_TAC (name ^ "_def"))) g;;
 507
 508 (* Generates a fresh name for the given term *)
 509 (* taking into account names of the provided variables *)
 510 let generate_fresh_name names tm =
 511   let rec find_name prefix n =
 512     let name = prefix ^ (if n = 0 then "" else string_of_int n) in
 513     if can (find (fun str -> str = name)) names then
 514       find_name prefix (n + 1)
 515     else
 516       name in
 517   let prefix = if is_var tm then (fst o dest_var) tm else "x" in
 518     find_name prefix 0;;
 519
 520
 521 (* Returns a variable which name does not conflict with names of given vars *)
 522 let get_fresh_var var vars =
 523   let names = map (fst o dest_var) vars in
 524     mk_var (generate_fresh_name names var, type_of var);;
 525
 526
 527 (* Matches all wild cards in the term and *)
 528 (* instantinates all type variables in the given context *)
 529 let prepare_term tm (g : goal) =
 530   let goal_tm = snd g in
 531   let tm0 =
 532     try follow_path (match_subterm_in_context tm goal_tm g) goal_tm
 533     with Failure _ -> tm in
 534     inst_all_free_vars tm0 g;;
 535
 536 (* Discharges a term by generalizing all occurences of this term first *)
 537 let disch_tm_tac occs tm (g : goal) =
 538   let tm0 = prepare_term tm g in
 539   let name = generate_fresh_name ((fst o unzip) (get_context_vars g)) tm in
 540   let new_tm = mk_var (name, type_of tm0) in
 541   let new_tm1 =
 542     if occs = [] && is_var tm then
 543       mk_var ((fst o dest_var) tm, type_of tm0)
 544     else new_tm in
 545   let abbrev_tm = mk_eq (new_tm, tm0) in
 546     (ABBREV_TAC abbrev_tm THEN
 547        EXPAND_TAC name THEN
 548        POP_ASSUM (fun th -> TRY (new_rewrite occs [] th)) THEN
 549        SPEC_TAC (new_tm, new_tm1)) g;;
 550
 551
 552 (* Discharges a theorem or a term *)
 553 let disch_tac occs arg =
 554   match arg with
 555     | Arg_theorem th -> MP_TAC th
 556     | Arg_term tm -> disch_tm_tac occs tm
 557     | _ -> failwith "disch_tac: a type cannot be discharged";;
 558
 559
 560
 561 (* process_thm *)
 562 let process_thm =
 563   let conj_imp = TAUT `(A /\ B ==> C) ==> (A ==> B ==> C)` in
 564   let dummy_tm = `F` in
 565     fun local_consts ->
 566       let rec process th =
 567         let ctm = concl th in
 568           (* forall *)
 569           if is_forall ctm then
 570             let (var_tm, _) = dest_forall ctm in
 571             let var = get_fresh_var var_tm (thm_frees th @ local_consts) in
 572             let th1 = SPEC var th in
 573             let list, th0 = process th1 in
 574               ("spec", var) :: list, th0
 575                 (* P ==> Q *)
 576           else if is_imp ctm then
 577             let ant_tm, _ = dest_imp ctm in
 578               (* P /\ R ==> Q *)
 579               if is_conj ant_tm then
 580                 let th1 = MATCH_MP conj_imp th in
 581                 let list, th0 = process th1 in
 582                   ("conj", dummy_tm) :: list, th0
 583                     (* P ==> Q *)
 584               else
 585                 let th1 = UNDISCH th in
 586                 let list, th0 = process th1 in
 587                   ("undisch", ant_tm) :: list, th0
 588           else
 589             [], th in
 590         process;;
 591
 592
 593
 594 (* reconstruct_thm *)
 595 let reconstruct_thm =
 596   let imp_conj = TAUT `(A ==> B ==> C) ==> (A /\ B ==> C)` in
 597   let triv_ths = TAUT `((T ==> A) <=> A) /\ ((T /\ A) = A) /\ ((A /\ T) = A)` in
 598   let rec reconstruct list th =
 599     match list with
 600       | [] -> th
 601       | cmd :: t ->
 602           let th1 =
 603             match cmd with
 604               | ("spec", (_ as tm)) -> GEN tm th
 605               | ("conj", _) -> MATCH_MP imp_conj th
 606               | ("undisch", (_ as tm)) -> DISCH tm th
 607               | _ -> failwith ("Unknown command: " ^ fst cmd) in
 608             reconstruct t th1 in
 609
 610     fun (cmd_list, th) ->
 611       let th1 = reconstruct (rev cmd_list) th in
 612         PURE_REWRITE_RULE[triv_ths] th1;;
 613
 614
 615 (* spec_var_th *)
 616 let spec_var_th th n tm =
 617   let cmd, th0 = process_thm (frees tm) th in
 618   let ty = type_of tm in
 619   let rec spec n list head =
 620     match list with
 621       | ("spec", (_ as var_tm)) :: t ->
 622           (try
 623              let ty_ii = type_match (type_of var_tm) ty [] in
 624                if n <= 1 then
 625                  let th1 = reconstruct_thm (list, th0) in
 626                  let th2 = ISPEC tm th1 in
 627                  let tail, th0 = process_thm [] th2 in
 628                  let head1 = map (fun s, tm -> s, inst ty_ii tm) head in
 629                    head1 @ tail, th0
 630                else
 631                  spec (n - 1) t (head @ [hd list])
 632            with Failure _ ->
 633              spec n t (head @ [hd list]))
 634       | h :: t -> spec n t (head @ [h])
 635       | [] -> failwith ("spec_var_th") in
 636     reconstruct_thm (spec n cmd []);;
 637
 638
 639 (* match_mp_th *)
 640 let match_mp_th ith n th =
 641   let lconsts = thm_frees ith in
 642   let cmd, th0 = process_thm (thm_frees th) ith in
 643   let tm = concl th in
 644   let rec rec_match n list head =
 645     match list with
 646       | ("undisch", (_ as tm0)) :: t ->
 647           (try
 648              let ii = term_match lconsts tm0 tm in
 649                if n <= 1 then
 650                  let th1 = INSTANTIATE_ALL ii th0 in
 651                  let th2 = PROVE_HYP th th1 in
 652                  let list0 = head @ (("undisch", `T`) :: t) in
 653                  let f_vars = frees tm0 in
 654                  let list1 = filter
 655                    (fun s, tm -> not (s = "spec" && mem tm f_vars)) list0 in
 656                  let list = map (fun s, tm -> s, instantiate ii tm) list1 in
 657                    list, th2
 658                else
 659                  rec_match (n - 1) t (head @ [hd list])
 660            with Failure _ ->
 661              rec_match n t (head @ [hd list]))
 662       | h :: t -> rec_match n t (head @ [h])
 663       | [] -> failwith "match_mp_th: no match" in
 664   let r = rec_match n cmd [] in
 665     reconstruct_thm r;;
 666
 667 (* Introduces a subgoal *)
 668 let have_gen_tac binders then_tac tm (g : goal) =
 669 (*  let tm0 = inst_all_free_vars tm g in *)
 670   let tm1 = gen_variables binders tm in
 671   let tm2 = prepare_term tm1 g in
 672     (THENL_FIRST (SUBGOAL_THEN tm2 (fun th -> MP_TAC th THEN then_tac))
 673        (move binders)) g;;
 674
 675
 676 let have_tac then_tac tm (g : goal) =
 677 (*  let tm0 = inst_all_free_vars tm g in *)
 678   let tm0 = prepare_term tm g in
 679     (SUBGOAL_THEN tm0 (fun th -> MP_TAC th THEN then_tac)) g;;
 680
 681
 682
 683 (* 'wlog' tactic *)
 684 let wlog_tac then_tac vars tm (g : goal) =
 685 (*  let tm0 = inst_all_free_vars tm g in *)
 686   let tm0 = prepare_term tm g in
 687   let vars0 = map (fun tm -> inst_all_free_vars tm g) vars in
 688   let g_tm = snd g in
 689   let imp = list_mk_forall (vars0, mk_imp (tm0, g_tm)) in
 690     (THENL_ROT 1 (SUBGOAL_THEN imp (fun th -> MP_TAC th THEN then_tac) THENL
 691        [REPLICATE_TAC (length vars) GEN_TAC; ALL_TAC])) g;;
 692
 693
 694 (* Provides a witness for an existential goal *)
 695 let exists_tac tm (g : goal) =
 696   let tm0 = inst_all_free_vars tm g in
 697   let target_ty = (type_of o fst o dest_exists o snd) g in
 698   let inst_ty = type_match (type_of tm0) target_ty [] in
 699   let tm1 = inst inst_ty tm0 in
 700     (EXISTS_TAC tm1) g;;
 701
 702 (* Instantiates the first type variable in the given theorem *)
 703 let inst_first_type th ty =
 704   let ty_vars = type_vars_in_term (concl th) in
 705   if ty_vars = [] then
 706     failwith "inst_first_type: no type variables in the theorem"
 707   else
 708     INST_TYPE [(ty, hd ty_vars)] th;;
 709
 710
 711 (* The first argument must be a theorem, the second argument is arbitrary *)
 712 let combine_args arg1 arg2 =
 713   let th1 = get_arg_thm arg1 in
 714   let th0 =
 715     match arg2 with
 716       | Arg_theorem th2 ->
 717           (try MATCH_MP th1 th2 with Failure _ -> match_mp_th th1 1 th2)
 718       | Arg_term tm2 ->
 719           (try ISPEC tm2 th1 with Failure _ -> spec_var_th th1 1 tm2)
 720       | Arg_type ty2 -> inst_first_type th1 ty2 in
 721     Arg_theorem th0;;
 722
 723
 724 let use_arg_then_result = ref TRUTH;;
 725
 726 let use_arg_then id (arg_tac:arg_type->tactic) (g:goal) =
 727   let list = fst g in
 728   let arg =
 729     try
 730       let assumption = assoc id list in
 731         Arg_theorem assumption
 732     with Failure _ ->
 733       try
 734         let vars = get_context_vars g in
 735         let var = assoc id vars in
 736           Arg_term var
 737       with Failure _ ->
 738         let lexbuf =
 739           Lexing.from_string ("use_arg_then_result := " ^ id ^ ";;") in
 740         let ast = (!Toploop.parse_toplevel_phrase) lexbuf in
 741         let _ =
 742           try
 743             Toploop.execute_phrase false Format.std_formatter ast
 744           with _ -> failwith ("Bad identifier: " ^ id) in
 745           Arg_theorem !use_arg_then_result in
 746     arg_tac arg g;;
 747
 748
 749 let combine_args_then (tac:arg_type->tactic) arg1 arg2 (g:goal) =
 750   let th1 = get_arg_thm arg1 in
 751   let th0 =
 752     match arg2 with
 753       | Arg_theorem th2 ->
 754           (try MATCH_MP th1 th2 with Failure _ -> match_mp_th th1 1 th2)
 755       | Arg_term tm2 ->
 756           let tm0 = prepare_term tm2 g in
 757             (try ISPEC tm0 th1 with Failure _ -> spec_var_th th1 1 tm0)
 758       | Arg_type ty2 -> inst_first_type th1 ty2 in
 759     tac (Arg_theorem th0) g;;
 760
 761
 762
 763
 764 (* Specializes a variable and applies the next tactic *)
 765 let ispec_then tm (tac : thm_tactic) th (g : goal) =
 766   let tm0 = prepare_term tm g in
 767   let th0 = try ISPEC tm0 th with Failure _ -> spec_var_th th 1 tm0 in
 768     tac th0 g;;
 769
 770
 771 let ISPEC_THEN tm (tac : thm_tactic) th (g : goal) =
 772   let tm0 = inst_all_free_vars tm g in
 773     tac (ISPEC tm0 th) g;;
 774
 775
 776
 777 let USE_THM_THEN th (tac : thm_tactic) =
 778   tac th;;
 779
 780
 781 let MATCH_MP_THEN th2 (tac : thm_tactic) th1 =
 782   tac (MATCH_MP th1 th2);;
 783
 784 let match_mp_then th2 (tac : thm_tactic) th1 =
 785   let th0 = try MATCH_MP th1 th2 with Failure _ -> match_mp_th th1 1 th2 in
 786     tac th0;;
 787
 788
 789 let GSYM_THEN (tac : thm -> tactic) th =
 790   tac (GSYM th);;
 791
 792
 793 let gsym_then (tac:arg_type->tactic) arg =
 794   tac (Arg_theorem (GSYM (get_arg_thm arg)));;
 795
 796
 797 (* The 'apply' tactic *)
 798 let apply_tac th g =
 799   let rec try_match th =
 800     try MATCH_MP_TAC th g with Failure _ ->
 801       let th0 = PURE_ONCE_REWRITE_RULE[IMP_IMP] th in
 802       if th = th0 then failwith "apply_tac: no match"
 803       else
 804         try_match th0 in
 805
 806       try MATCH_ACCEPT_TAC th g with Failure _ ->
 807         try_match th;;
 808
 809 (*let apply_tac th =
 810   FIRST [MATCH_ACCEPT_TAC th; MATCH_MP_TAC th];; *)
 811
 812
 813 (* The 'exact' tactic *)
 814 (* TODO: do [done | by move => top; apply top], here apply top
 815    works as ACCEPT_TAC with matching (rewriting) in some cases *)
 816 let exact_tac = FIRST [done_tac; DISCH_THEN (fun th -> apply_tac th) THEN done_tac];;
 817
 818
 819
 820 (* Specializes the theorem using the given set of variables *)
 821 let spec0 names vars =
 822   let find name =
 823     try (assoc name vars, true)
 824     with Failure _ -> (parse_term name, false) in
 825   let find_type var =
 826     let name, ty = dest_var var in
 827     let t, flag = find name in
 828       if flag then
 829         (ty, type_of t)
 830       else
 831         (`:bool`, `:bool`) in
 832   let inst_term tm =
 833     let ty_src, ty_dst = unzip (map find_type (frees tm)) in
 834     let ty_inst = itlist2 type_match ty_src ty_dst [] in
 835       inst ty_inst tm in
 836   let list = map find names in
 837   let tm_list = map (fun tm, flag -> if flag then tm else inst_term tm) list in
 838     ISPECL tm_list;;
 839
 840
 841 let spec names = spec0 names (get_context_vars (top_realgoal()));;
 842
 843
 844 let spec_mp names th g = MP_TAC (spec0 names (get_context_vars g) th) g;;
 845
 846
 847 (* Case theorems *)
 848 let bool_cases = ONCE_REWRITE_RULE[CONJ_ACI] bool_INDUCT;;
 849 let list_cases = prove(`!P. P [] /\ (!(h:A) t. P (CONS h t)) ==> (!l. P l)`,
 850   REPEAT STRIP_TAC THEN
 851     MP_TAC (SPEC `l:(A)list` list_CASES) THEN DISCH_THEN DISJ_CASES_TAC THEN ASM_REWRITE_TAC[] THEN
 852     FIRST_X_ASSUM (CHOOSE_THEN MP_TAC) THEN DISCH_THEN (CHOOSE_THEN MP_TAC) THEN
 853     DISCH_THEN (fun th -> ASM_REWRITE_TAC[th]));;
 854 let pair_cases = pair_INDUCT;;
 855 let num_cases = prove(`!P. P 0 /\ (!n. P (SUC n)) ==> (!m. P m)`,
 856   REPEAT STRIP_TAC THEN
 857     MP_TAC (SPEC `m:num` num_CASES) THEN DISCH_THEN DISJ_CASES_TAC THEN ASM_REWRITE_TAC[] THEN
 858     FIRST_X_ASSUM (CHOOSE_THEN (fun th -> ASM_REWRITE_TAC[th])));;
 859 let option_cases = option_INDUCT;;
 860
 861
 862 let cases_table = Hashtbl.create 10;;
 863 Hashtbl.add cases_table "bool" bool_cases;;
 864 Hashtbl.add cases_table "list" list_cases;;
 865 Hashtbl.add cases_table "prod" pair_cases;;
 866 Hashtbl.add cases_table "num" num_cases;;
 867 Hashtbl.add cases_table "option" option_cases;;
 868
 869
 870 (* Induction theorems *)
 871 let bool_elim = bool_cases;;
 872 let list_elim = list_INDUCT;;
 873 let pair_elim = pair_INDUCT;;
 874 let num_elim = num_INDUCTION;;
 875 let option_elim = option_INDUCT;;
 876
 877 let elim_table = Hashtbl.create 10;;
 878 Hashtbl.add elim_table "bool" bool_elim;;
 879 Hashtbl.add elim_table "list" list_elim;;
 880 Hashtbl.add elim_table "prod" pair_elim;;
 881 Hashtbl.add elim_table "num" num_elim;;
 882 Hashtbl.add elim_table "option" option_elim;;
 883
 884
 885
 886 (* case: works only for (A /\ B) -> C; (A \/ B) -> C; (?x. P) -> Q; !(n:num). P; !(l:list(A)). P *)
 887 let case (g:goal) =
 888   let goal_tm = snd g in
 889     if not (is_imp goal_tm) then
 890       (* !a. P *)
 891       if is_forall goal_tm then
 892         let var, _ = dest_forall goal_tm in
 893         let ty_name = (fst o dest_type o type_of) var in
 894         let case_th = Hashtbl.find cases_table ty_name in
 895           (MATCH_MP_TAC case_th THEN REPEAT CONJ_TAC) g
 896       else
 897         failwith "case: not imp or forall"
 898     else
 899       let tm = lhand goal_tm in
 900         (* A /\ B *)
 901         if is_conj tm then
 902           (DISCH_THEN (CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN POP_ASSUM MP_TAC) g
 903         (* A \/ B *)
 904         else if is_disj tm then
 905           (DISCH_THEN DISJ_CASES_TAC THEN POP_ASSUM MP_TAC) g
 906         (* ?x. P *)
 907         else if is_exists tm then
 908           (ONCE_REWRITE_TAC[GSYM LEFT_FORALL_IMP_THM]) g
 909         else
 910           failwith "case: not implemented";;
 911
 912
 913
 914 (* elim: works only for num and list *)
 915 let elim (g:goal) =
 916   let goal_tm = snd g in
 917     (* !a. P *)
 918     if is_forall goal_tm then
 919       let var, _ = dest_forall goal_tm in
 920       let ty_name = (fst o dest_type o type_of) var in
 921       let induct_th = Hashtbl.find elim_table ty_name in
 922         (MATCH_MP_TAC induct_th THEN REPEAT CONJ_TAC) g
 923     else
 924       failwith "elim: not forall";;
 925
 926
 927
 928 (* Instantiates the first type variable in the given theorem *)
 929 let INST_FIRST_TYPE_THEN ty (then_tac:thm_tactic) th =
 930   let ty_vars = type_vars_in_term (concl th) in
 931   if ty_vars = [] then
 932     failwith "inst_first_type: no type variables in the theorem"
 933   else
 934     then_tac (INST_TYPE [(ty, hd ty_vars)] th);;
 935
 936
 937 (* Replaces all occurrences of distinct '_' with unique variables *)
 938 let transform_pattern pat_tm =
 939   let names = ref (map (fst o dest_var) (frees pat_tm)) in
 940   let rec transform tm =
 941     match tm with
 942       | Abs(x_tm, b_tm) ->
 943           let _ = names := (fst o dest_var) x_tm :: !names in
 944             mk_abs (x_tm, transform b_tm)
 945       | Comb(l_tm, r_tm) ->
 946           mk_comb (transform l_tm, transform r_tm)
 947       | Var ("_", ty) ->
 948           let name = generate_fresh_name !names tm in
 949           let _ = names := name :: !names in
 950             mk_var (name, ty)
 951       | _ -> tm in
 952     transform pat_tm;;
 953
 954
 955 let wild_frees tm =
 956   filter (fun tm -> ((fst o dest_var) tm).[0] = '_') (frees tm);;
 957
 958 let nwild_frees tm =
 959   filter (fun tm -> ((fst o dest_var) tm).[0] <> '_') (frees tm);;
 960
 961
 962 (* congr_tac *)
 963 let congr_tac pat_tm goal =
 964   let goal_tm = snd goal in
 965   let context_vars = get_context_vars goal in
 966   let pat = transform_pattern pat_tm in
 967   let f0_vars = nwild_frees pat in
 968   let pattern = inst_context_vars context_vars f0_vars pat in
 969   let const_pat = nwild_frees pattern in
 970   let wild_pat = wild_frees pattern in
 971
 972   let lhs, rhs = dest_eq goal_tm in
 973   let lm, rm =
 974     term_match const_pat pattern lhs, term_match const_pat pattern rhs in
 975   let eq_tms = map
 976     (fun tm -> mk_eq (instantiate lm tm, instantiate rm tm)) wild_pat in
 977   let eq_tm = itlist (curry mk_imp) eq_tms goal_tm in
 978   let eq_thm = EQT_ELIM (SIMP_CONV[] eq_tm) in
 979     (apply_tac eq_thm THEN REPEAT CONJ_TAC) goal;;
 980
 981
 982 (* Eliminates the first antecedent of a goal *)
 983 let elim_fst_ants_tac =
 984   let gen_elim_thm tm =
 985     let vars, tm1 = strip_forall tm in
 986     let ants_tm, concl_tm = dest_imp tm1 in
 987     let th1 = ASSUME (itlist (curry mk_forall) vars concl_tm) in
 988     let th2 = DISCH ants_tm (SPECL vars th1) in
 989       DISCH_ALL (itlist GEN vars th2) in
 990     fun (g:goal) ->
 991       let goal_tm = snd g in
 992       let elim_th = gen_elim_thm goal_tm in
 993         MATCH_MP_TAC elim_th g;;
 994
 995
 996 (* If a goal has the form ssreflect_eq ==> P then the equality is introduced as
 997    an assumption.
 998    If a goal has the form !x. ssreflect_eq ==> P then the equality is eliminated *)
 999 let process_fst_eq_tac (g:goal) =
1000   let vars, g_tm = strip_forall (snd g) in
1001   let tac =
1002     try
1003       let eq_tm = (rator o fst o dest_imp) g_tm in
1004       let label = (fst o dest_var o rand) eq_tm in
1005         if (fst o dest_const o rator) eq_tm = "ssreflect_eq" then
1006           if length vars = 0 then
1007             DISCH_THEN (LABEL_TAC label o PURE_ONCE_REWRITE_RULE[ssreflect_eq_def])
1008           else
1009             elim_fst_ants_tac
1010       else
1011         ALL_TAC
1012     with Failure _ -> ALL_TAC in
1013     tac g;;
1014
1015
1016 (* Discharges a term by generalizing all occurences of this term first *)
1017 let disch_tm_eq_tac eq_name occs tm (g : goal) =
1018   let tm0 = prepare_term tm g in
1019   let name = generate_fresh_name ((fst o unzip) (get_context_vars g)) tm in
1020   let eq_var = mk_var (eq_name, aty) in
1021   let new_tm = mk_var (name, type_of tm0) in
1022   let abbrev_tm = mk_eq (new_tm, tm0) in
1023     (ABBREV_TAC abbrev_tm THEN
1024        EXPAND_TAC name THEN
1025        FIRST_ASSUM (fun th -> TRY (new_rewrite occs [] th)) THEN
1026        POP_ASSUM (MP_TAC o PURE_ONCE_REWRITE_RULE[GSYM (SPEC eq_var ssreflect_eq_def)]) THEN
1027        SPEC_TAC (new_tm, new_tm)) g;;
1028
1029
1030 (* Discharges a term and generates an equality *)
1031 let disch_eq_tac eq_name occs arg =
1032   disch_tm_eq_tac eq_name occs (get_arg_term arg);;