jHOLLight/caml/ssreflect.hl

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