formal_ineqs/lib/ssreflect/sections.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 (* Basic commands for working with the goal stack *)
   9 let revert_proof_step = b;;
  10 let begin_goal = g;;
  11
  12 (* A flag for fast proof loading (using mk_thm) *)
  13 let fast_load_flag = ref false;;
  14
  15 (* Section variables, hypotheses (with labels), and implicit types *)
  16 type section_info = term list * (string * term) list * (string * hol_type) list;;
  17
  18 let empty_section : section_info = ([], [], []);;
  19
  20 let section_stack = ref ([] : (string * section_info) list);;
  21
  22
  23 (* Begins a new section *)
  24 let begin_section name =
  25   let sections = !section_stack in
  26     if can (C assoc sections) name then
  27       failwith ("Section " ^ name ^ " is already active")
  28     else
  29       let sections = (name, empty_section) :: sections in
  30       section_stack := sections;;
  31
  32
  33 (* Ends the active section *)
  34 let end_section name =
  35   let sections = !section_stack in
  36     if sections = [] then
  37       failwith "end_section: No open sections"
  38     else
  39       let last_name, _ = hd sections in
  40         if Pervasives.compare last_name name <> 0 then
  41           failwith ("The last open section is " ^ last_name)
  42         else
  43           section_stack := tl sections;;
  44
  45 (* Returns all section variables in the current section *)
  46 let current_section_vars () =
  47   if !section_stack = [] then []
  48   else
  49     let (_, (vars, _, _)) = hd !section_stack in
  50       vars;;
  51
  52 (* Returns all hypotheses in the current section *)
  53 let current_section_hyps () =
  54   if !section_stack = [] then []
  55   else
  56     let (_, (_, hyps, _)) = hd !section_stack in
  57       hyps;;
  58
  59
  60 (* Returns all section variables from all sections *)
  61 let section_vars () : term list =
  62   let vars = map (fun (_, (v, _, _)) -> v) !section_stack in
  63     List.concat vars;;
  64
  65
  66 (* Returns all implicit types from all sections *)
  67 let section_types () : (string * hol_type) list =
  68   let types = map (fun (_, (_, _, t)) -> t) !section_stack in
  69     List.concat types;;
  70
  71
  72
  73 (* Returns all hypotheses from all sections *)
  74 let section_hyps () : (string * term) list =
  75   let hyps = map (fun (_, (_, h, _)) -> h) !section_stack in
  76     List.concat hyps;;
  77
  78
  79 (* Adds the given variable to the active section *)
  80 let add_section_var var =
  81   let sections = !section_stack in
  82     if sections = [] then
  83       failwith "add_section_var: No open sections"
  84     else
  85       let name, (vars, hyps, types) = hd sections in
  86       let s_var = section_vars() in
  87       let var_name, _ = dest_var var in
  88         if can (C assoc (map dest_var s_var)) var_name then
  89           failwith ("A variable with the name "^var_name^" is already defined")
  90         else
  91           section_stack := (name, (var :: vars, hyps, types)) :: tl sections;;
  92
  93 (* Adds the given implicit type to the active section *)
  94 let add_section_type tm =
  95   let sections = !section_stack in
  96     if sections = [] then
  97       failwith "add_section_type: No open sections"
  98     else
  99       let name, (vars, hyps, types) = hd sections in
 100       let s_types = section_types() in
 101       let var_name, ty = dest_var tm in
 102         if can (C assoc s_types) var_name then
 103           failwith ("An implicit type for the variable "^var_name^" is already defined")
 104         else
 105           section_stack := (name, (vars, hyps, (var_name, ty) :: types)) :: tl sections;;
 106
 107
 108
 109 (* Removes the given variable from the active section *)
 110 let remove_section_var var_name =
 111   let sections = !section_stack in
 112   let name, (vars, hyps, types) = hd sections in
 113   let ty = assoc var_name (map dest_var vars) in
 114   let var = mk_var (var_name, ty) in
 115   let new_vars = subtract vars [var] in
 116     section_stack := (name, (new_vars, hyps, types)) :: tl sections;;
 117
 118
 119 (* Removes the given implicit type from the active section *)
 120 let remove_section_type type_name =
 121   let sections = !section_stack in
 122   let name, (vars, hyps, types) = hd sections in
 123   let ty = assoc type_name types in
 124   let new_types = subtract types [type_name, ty] in
 125     section_stack := (name, (vars, hyps, new_types)) :: tl sections;;
 126
 127
 128
 129
 130 (* Instantiates types of section variables in the term *)
 131 let inst_section_vars tm =
 132   let s_vars = map dest_var (section_vars()) in
 133   let find_var (name, ty) =
 134     try (assoc name s_vars, ty)
 135     with Failure _ -> (bool_ty, bool_ty) in
 136   let inst_var (name, ty) tm =
 137     let ty_dst, ty_src = find_var (name, ty) in
 138       try (inst (type_match ty_src ty_dst []) tm)
 139       with Failure _ ->
 140         failwith ("Section variable " ^ name ^
 141                     " has type " ^ string_of_type ty_dst) in
 142   let f_vars = map dest_var (frees tm) in
 143     itlist inst_var f_vars tm;;
 144
 145
 146 (* Instantiates implicit types in the given term *)
 147 (* (free variables and top generalized variables are considered in the term) *)
 148 let inst_section_types tm =
 149   let s_types = section_types() in
 150   let find_type tm =
 151     let name, ty = dest_var tm in
 152     try (assoc name s_types, ty) with Failure _ -> (bool_ty, bool_ty) in
 153   let f_vars = frees tm in
 154   let g_vars, _ = strip_forall tm in
 155   let ty_dst, ty_src = unzip (map find_type (g_vars @ f_vars)) in
 156   let ty_inst = itlist2 type_match ty_src ty_dst [] in
 157     inst ty_inst tm;;
 158
 159
 160 (* Checks if the term contains any free variables
 161    which are not section variables *)
 162 let check_section_term tm =
 163   let f_vars = frees tm in
 164   if !section_stack = [] then
 165     if f_vars <> [] then
 166       let str = String.concat ", " (map string_of_term f_vars) in
 167         failwith ("Free variables: " ^ str)
 168     else ()
 169   else
 170     let s_vars = section_vars() in
 171     let vars = subtract f_vars s_vars in
 172       if vars <> [] then
 173         let str = String.concat ", " (map string_of_term vars) in
 174           failwith ("Free variables: " ^ str)
 175       else ();;
 176
 177
 178
 179
 180 (* Adds the given hypothesis (term) to the active section *)
 181 let add_section_hyp label hyp =
 182   let sections = !section_stack in
 183     if sections = [] then
 184       failwith "add_section_hyp: No open sections"
 185     else
 186       let hyp0 = inst_section_vars hyp in
 187       let hyp1 = inst_section_types hyp0 in
 188       let name, (vars, hyps, types) = hd sections in
 189       let hyp_names = map fst (section_hyps()) in
 190         if can (find (fun x -> Pervasives.compare label x = 0)) hyp_names then
 191           failwith ("A hypothesis with the name "^label^" is already defined")
 192         else
 193           check_section_term hyp1;
 194           section_stack := (name, (vars, (label, hyp1) :: hyps, types)) :: tl sections;;
 195
 196
 197 (* Removes the given assumption from the active section *)
 198 let remove_section_hyp label =
 199   let sections = !section_stack in
 200   let name, (vars, hyps, types) = hd sections in
 201   let hyp = assoc label hyps in
 202   let new_hyps = subtract hyps [(label, hyp)] in
 203     section_stack := (name, (vars, new_hyps, types)) :: tl sections;;
 204
 205
 206
 207 (* Prepares a goal term *)
 208 let prepare_goal_term tm =
 209   if !section_stack = [] then (check_section_term tm; tm)
 210   else
 211     let tm0 = inst_section_vars tm in
 212     let tm1 = inst_section_types tm0 in
 213     let s_hyps = map snd (section_hyps()) in
 214     let r = itlist (curry mk_imp) s_hyps tm1 in
 215       check_section_term r; r;;
 216
 217
 218 (* Prepares a goal term and an initial tactic *)
 219 let prepare_section_proof names tm =
 220   let f_vars = map dest_var (frees tm) in
 221   let find var_name =
 222     try assoc var_name f_vars with Failure _ -> failwith ("Unused variable: "^var_name) in
 223   let g_vars = map (fun name -> mk_var (name, find name)) names in
 224   let g_tm = list_mk_forall (g_vars, tm) in
 225   let tm0 = prepare_goal_term g_tm in
 226   let n_hyps = map fst (section_hyps()) in
 227   let gen_tac = REPLICATE_TAC (length g_vars) GEN_TAC in
 228   let disch_tac = itlist (fun name tac -> DISCH_THEN (LABEL_TAC name) THEN tac) n_hyps ALL_TAC in
 229     tm0, disch_tac THEN gen_tac;;
 230
 231
 232 (* Starts a proof of the goal using section hypotheses *)
 233 let start_section_proof names tm =
 234   let tm0, tac0 = prepare_section_proof names tm in
 235   let _ = set_goal([], tm0) in
 236     refine (by (VALID tac0));;
 237
 238
 239 (* Returns the final theorem *)
 240 let end_section_proof () =
 241   let th = top_thm() in
 242   let hyps = section_hyps() in
 243     itlist (fun _ th -> UNDISCH th) hyps th;;
 244
 245 (* Proofs a lemma using section hypotheses and variables *)
 246 let section_proof names tm tac_list =
 247   let tm0, tac0 = prepare_section_proof names tm in
 248   let gstate = mk_goalstate ([], tm0) in
 249   let tac_list1 =
 250     if !fast_load_flag then
 251       [fun g -> ACCEPT_TAC(mk_thm([], snd g)) g]
 252     else
 253       tac_list in
 254   let _, sgs, just = rev_itlist by (tac0 :: tac_list1) gstate in
 255   let th0 =
 256     if sgs = [] then just null_inst []
 257     else failwith "section_proof: unsolved goals" in
 258   let hyps = section_hyps() in
 259     itlist (fun _ th -> UNDISCH th) hyps th0;;
 260
 261
 262
 263 (* Discharges all assumptions and generalize all section variables *)
 264 let finalize_theorem th =
 265   let hyps = map snd (current_section_hyps()) in
 266   let th_hyps = hyp th in
 267   let hyps0 = intersect hyps th_hyps in
 268   let s_vars = current_section_vars() in
 269   let th1 = rev_itlist (fun hyp th -> DISCH hyp th) hyps0 th in
 270   let f_vars = frees (concl th1) in
 271   let vars = intersect f_vars s_vars in
 272     itlist (fun var th -> GEN var th) vars th1;;
 273