summaryrefslogtreecommitdiff
path: root/toplevel/lemmas.ml
blob: 7704449f528acf9ecabb235eb3f7cdcd9b4cf677 (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
(************************************************************************)
(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
(*   \VV/  **************************************************************)
(*    //   *      This file is distributed under the terms of the       *)
(*         *       GNU Lesser General Public License Version 2.1        *)
(************************************************************************)

(* Created by Hugo Herbelin from contents related to lemma proofs in
   file command.ml, Aug 2009 *)

open Util
open Flags
open Pp
open Names
open Term
open Declarations
open Entries
open Environ
open Nameops
open Libnames
open Decls
open Decl_kinds
open Declare
open Pretyping
open Termops
open Namegen
open Evd
open Evarutil
open Reductionops
open Topconstr
open Constrintern
open Impargs
open Tacticals

(* Support for mutually proved theorems *)

let retrieve_first_recthm = function
  | VarRef id ->
      (pi2 (Global.lookup_named id),variable_opacity id)
  | ConstRef cst ->
      let cb = Global.lookup_constant cst in
      (Option.map Declarations.force (body_of_constant cb), is_opaque cb)
  | _ -> assert false

let adjust_guardness_conditions const = function
  | [] -> const (* Not a recursive statement *)
  | possible_indexes ->
  (* Try all combinations... not optimal *)
  match kind_of_term const.const_entry_body with
  | Fix ((nv,0),(_,_,fixdefs as fixdecls)) ->
(*      let possible_indexes =
	List.map2 (fun i c -> match i with Some i -> i | None ->
	  interval 0 (List.length ((lam_assum c))))
	  lemma_guard (Array.to_list fixdefs) in
*)
      let indexes =
	search_guard dummy_loc (Global.env()) possible_indexes fixdecls in
      { const with const_entry_body = mkFix ((indexes,0),fixdecls) }
  | c -> const

let find_mutually_recursive_statements thms =
    let n = List.length thms in
    let inds = List.map (fun (id,(t,impls,annot)) ->
      let (hyps,ccl) = decompose_prod_assum t in
      let x = (id,(t,impls)) in
      match annot with
      (* Explicit fixpoint decreasing argument is given *)
      | Some (Some (_,id),CStructRec) ->
          let i,b,typ = lookup_rel_id id hyps in
          (match kind_of_term t with
          | Ind (kn,_ as ind) when
              let mind = Global.lookup_mind kn in
              mind.mind_finite & b = None ->
              [ind,x,i],[]
          | _ ->
              error "Decreasing argument is not an inductive assumption.")
      (* Unsupported cases *)
      | Some (_,(CWfRec _|CMeasureRec _)) ->
          error "Only structural decreasing is supported for mutual statements."
      (* Cofixpoint or fixpoint w/o explicit decreasing argument *)
      | None | Some (None, CStructRec) ->
      let whnf_hyp_hds = map_rel_context_in_env
        (fun env c -> fst (whd_betadeltaiota_stack env Evd.empty c))
        (Global.env()) hyps in
      let ind_hyps =
        List.flatten (list_map_i (fun i (_,b,t) ->
          match kind_of_term t with
          | Ind (kn,_ as ind) when
                let mind = Global.lookup_mind kn in
                mind.mind_finite & b = None ->
              [ind,x,i]
          | _ ->
              []) 0 (List.rev whnf_hyp_hds)) in
      let ind_ccl =
        let cclenv = push_rel_context hyps (Global.env()) in
        let whnf_ccl,_ = whd_betadeltaiota_stack cclenv Evd.empty ccl in
        match kind_of_term whnf_ccl with
        | Ind (kn,_ as ind) when
              let mind = Global.lookup_mind kn in
              mind.mind_ntypes = n & not mind.mind_finite ->
            [ind,x,0]
        | _ ->
            [] in
      ind_hyps,ind_ccl) thms in
    let inds_hyps,ind_ccls = List.split inds in
    let of_same_mutind ((kn,_),_,_) = function ((kn',_),_,_) -> kn = kn' in
    (* Check if all conclusions are coinductive in the same type *)
    (* (degenerated cartesian product since there is at most one coind ccl) *)
    let same_indccl =
      list_cartesians_filter (fun hyp oks ->
	if List.for_all (of_same_mutind hyp) oks
	then Some (hyp::oks) else None) [] ind_ccls in
    let ordered_same_indccl =
      List.filter (list_for_all_i (fun i ((kn,j),_,_) -> i=j) 0) same_indccl in
    (* Check if some hypotheses are inductive in the same type *)
    let common_same_indhyp =
      list_cartesians_filter (fun hyp oks ->
	if List.for_all (of_same_mutind hyp) oks
	then Some (hyp::oks) else None) [] inds_hyps in
    let ordered_inds,finite,guard =
      match ordered_same_indccl, common_same_indhyp with
      | indccl::rest, _ ->
	  assert (rest=[]);
          (* One occ. of common coind ccls and no common inductive hyps *)
	  if common_same_indhyp <> [] then
	    if_verbose msgnl (str "Assuming mutual coinductive statements.");
	  flush_all ();
          indccl, true, []
      | [], _::_ ->
	  if same_indccl <> [] &&
	     list_distinct (List.map pi1 (List.hd same_indccl)) then
	    if_verbose msgnl (strbrk "Coinductive statements do not follow the order of definition, assuming the proof to be by induction."); flush_all ();
          let possible_guards = List.map (List.map pi3) inds_hyps in
	  (* assume the largest indices as possible *)
	  list_last common_same_indhyp, false, possible_guards
      | _, [] ->
	  error
            ("Cannot find common (mutual) inductive premises or coinductive" ^
             " conclusions in the statements.")
    in
    (finite,guard,None), ordered_inds

let look_for_possibly_mutual_statements = function
  | [id,(t,impls,None)] ->
      (* One non recursively proved theorem *)
      None,[id,(t,impls)],None
  | _::_ as thms ->
    (* More than one statement and/or an explicit decreasing mark: *)
    (* we look for a common inductive hyp or a common coinductive conclusion *)
    let recguard,ordered_inds = find_mutually_recursive_statements thms in
    let thms = List.map pi2 ordered_inds in
    Some recguard,thms, Some (List.map (fun (_,_,i) -> succ i) ordered_inds)
  | [] -> anomaly "Empty list of theorems."

(* Saving a goal *)

let save id const do_guard (locality,kind) hook =
  let const = adjust_guardness_conditions const do_guard in
  let {const_entry_body = pft;
       const_entry_type = tpo;
       const_entry_opaque = opacity } = const in
  let k = logical_kind_of_goal_kind kind in
  let l,r = match locality with
    | Local when Lib.sections_are_opened () ->
	let c = SectionLocalDef (pft, tpo, opacity) in
	let _ = declare_variable id (Lib.cwd(), c, k) in
	(Local, VarRef id)
    | Local | Global ->
        let kn = declare_constant id (DefinitionEntry const, k) in
	Autoinstance.search_declaration (ConstRef kn);
	(Global, ConstRef kn) in
  Pfedit.delete_current_proof ();
  definition_message id;
  hook l r

let default_thm_id = id_of_string "Unnamed_thm"

let compute_proof_name locality = function
  | Some (loc,id) ->
      (* We check existence here: it's a bit late at Qed time *)
      if Nametab.exists_cci (Lib.make_path id) || is_section_variable id ||
	 locality=Global && Nametab.exists_cci (Lib.make_path_except_section id)
      then
        user_err_loc (loc,"",pr_id id ++ str " already exists.");
      id
  | None ->
      next_global_ident_away default_thm_id (Pfedit.get_all_proof_names ()) 

let save_remaining_recthms (local,kind) body opaq i (id,(t_i,(_,imps))) =
  match body with
  | None ->
      (match local with
      | Local ->
          let impl=false in (* copy values from Vernacentries *)
          let k = IsAssumption Conjectural in
          let c = SectionLocalAssum (t_i,impl) in
	  let _ = declare_variable id (Lib.cwd(),c,k) in
          (Local,VarRef id,imps)
      | Global ->
          let k = IsAssumption Conjectural in
          let kn = declare_constant id (ParameterEntry (None,t_i,None), k) in
          (Global,ConstRef kn,imps))
  | Some body ->
      let k = logical_kind_of_goal_kind kind in
      let body_i = match kind_of_term body with
        | Fix ((nv,0),decls) -> mkFix ((nv,i),decls)
        | CoFix (0,decls) -> mkCoFix (i,decls)
        | _ -> anomaly "Not a proof by induction" in
      match local with
      | Local ->
	  let c = SectionLocalDef (body_i, Some t_i, opaq) in
	  let _ = declare_variable id (Lib.cwd(), c, k) in
          (Local,VarRef id,imps)
      | Global ->
          let const =
            { const_entry_body = body_i;
              const_entry_secctx = None;
              const_entry_type = Some t_i;
              const_entry_opaque = opaq } in
          let kn = declare_constant id (DefinitionEntry const, k) in
          (Global,ConstRef kn,imps)

let save_hook = ref ignore
let set_save_hook f = save_hook := f

let get_proof opacity =
  let id,(const,do_guard,persistence,hook) = Pfedit.cook_proof !save_hook in
  id,{const with const_entry_opaque = opacity},do_guard,persistence,hook

let save_named opacity =
  let id,const,do_guard,persistence,hook = get_proof opacity in
  save id const do_guard persistence hook

let check_anonymity id save_ident =
  if atompart_of_id id <> string_of_id (default_thm_id) then
    error "This command can only be used for unnamed theorem."

let save_anonymous opacity save_ident =
  let id,const,do_guard,persistence,hook = get_proof opacity in
  check_anonymity id save_ident;
  save save_ident const do_guard persistence hook

let save_anonymous_with_strength kind opacity save_ident =
  let id,const,do_guard,_,hook = get_proof opacity in
  check_anonymity id save_ident;
  (* we consider that non opaque behaves as local for discharge *)
  save save_ident const do_guard (Global, Proof kind) hook

(* Starting a goal *)

let start_hook = ref ignore
let set_start_hook = (:=) start_hook

let start_proof id kind c ?init_tac ?(compute_guard=[]) hook =
  let sign = initialize_named_context_for_proof () in
  !start_hook c;
  Pfedit.start_proof id kind sign c ?init_tac ~compute_guard hook

let rec_tac_initializer finite guard thms snl =
  if finite then
    match List.map (fun (id,(t,_)) -> (id,t)) thms with
    | (id,_)::l -> Hiddentac.h_mutual_cofix true id l
    | _ -> assert false
  else
    (* nl is dummy: it will be recomputed at Qed-time *)
    let nl = match snl with 
     | None -> List.map succ (List.map list_last guard)
     | Some nl -> nl
    in match List.map2 (fun (id,(t,_)) n -> (id,n,t)) thms nl with
       | (id,n,_)::l -> Hiddentac.h_mutual_fix true id n l
       | _ -> assert false

let start_proof_with_initialization kind recguard thms snl hook =
  let intro_tac (_, (_, (ids, _))) =
    Refiner.tclMAP (function
    | Name id -> Tactics.intro_mustbe_force id
    | Anonymous -> Tactics.intro) (List.rev ids) in
  let init_tac,guard = match recguard with
  | Some (finite,guard,init_tac) ->
      let rec_tac = rec_tac_initializer finite guard thms snl in
      Some (match init_tac with
        | None -> 
            if Flags.is_auto_intros () then 
              tclTHENS rec_tac (List.map intro_tac thms)
            else
              rec_tac
        | Some tacl ->
            tclTHENS rec_tac
            (if Flags.is_auto_intros () then
              List.map2 (fun tac thm -> tclTHEN tac (intro_tac thm)) tacl thms
            else
              tacl)),guard
  | None ->
      assert (List.length thms = 1);
      (if Flags.is_auto_intros () then Some (intro_tac (List.hd thms)) else None), [] in
  match thms with
  | [] -> anomaly "No proof to start"
  | (id,(t,(_,imps)))::other_thms ->
      let hook strength ref =
        let other_thms_data =
          if other_thms = [] then [] else
            (* there are several theorems defined mutually *)
            let body,opaq = retrieve_first_recthm ref in
            list_map_i (save_remaining_recthms kind body opaq) 1 other_thms in
        let thms_data = (strength,ref,imps)::other_thms_data in
        List.iter (fun (strength,ref,imps) ->
	  maybe_declare_manual_implicits false ref imps;
	  hook strength ref) thms_data in
      start_proof id kind t ?init_tac hook ~compute_guard:guard

let start_proof_com kind thms hook =
  let evdref = ref Evd.empty in
  let env0 = Global.env () in
  let thms = List.map (fun (sopt,(bl,t,guard)) ->
    let impls, ((env, ctx), imps) = interp_context_evars evdref env0 bl in
    let t', imps' = interp_type_evars_impls ~impls ~evdref env t in
    Sign.iter_rel_context (check_evars env Evd.empty !evdref) ctx;
    let ids = List.map pi1 ctx in
      (compute_proof_name (fst kind) sopt,
      (nf_evar !evdref (it_mkProd_or_LetIn t' ctx),
       (ids, imps @ lift_implicits (List.length ids) imps'),
       guard)))
    thms in
  let recguard,thms,snl = look_for_possibly_mutual_statements thms in
  start_proof_with_initialization kind recguard thms snl hook

(* Admitted *)

let admit () =
  let (id,k,typ,hook) = Pfedit.current_proof_statement () in
  let e = Pfedit.get_used_variables(), typ, None in
  let kn =
    declare_constant id (ParameterEntry e,IsAssumption Conjectural) in
  Pfedit.delete_current_proof ();
  assumption_message id;
  hook Global (ConstRef kn)

(* Miscellaneous *)

let get_current_context () =
  try Pfedit.get_current_goal_context ()
  with e when Logic.catchable_exception e ->
    (Evd.empty, Global.env())