aboutsummaryrefslogtreecommitdiffhomepage
path: root/stm/lemmas.ml
blob: fb2f0351d227ea444809720df08b89646f37956c (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
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
(************************************************************************)
(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
(*   \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 CErrors
open Util
open Flags
open Pp
open Names
open Term
open Declarations
open Declareops
open Entries
open Environ
open Nameops
open Globnames
open Decls
open Decl_kinds
open Declare
open Pretyping
open Termops
open Namegen
open Reductionops
open Constrexpr
open Constrintern
open Impargs
open Context.Rel.Declaration

type 'a declaration_hook = Decl_kinds.locality -> Globnames.global_reference -> 'a
let mk_hook hook = hook
let call_hook fix_exn hook l c =
  try hook l c
  with e when CErrors.noncritical e ->
    let e = CErrors.push e in
    iraise (fix_exn e)

(* Support for mutually proved theorems *)

let retrieve_first_recthm = function
  | VarRef id ->
      let open Context.Named.Declaration in
      (get_value (Global.lookup_named id),variable_opacity id)
  | ConstRef cst ->
      let cb = Global.lookup_constant cst in
      (Global.body_of_constant_body cb, is_opaque cb)
  | _ -> assert false

let adjust_guardness_conditions const = function
  | [] -> const (* Not a recursive statement *)
  | possible_indexes ->
  (* Try all combinations... not optimal *)
     let env = Global.env() in
     { const with const_entry_body =
        Future.chain ~greedy:true ~pure:true const.const_entry_body
        (fun ((body, ctx), eff) ->
          match kind_of_term body with
          | Fix ((nv,0),(_,_,fixdefs as fixdecls)) ->
(*      let possible_indexes =
	List.map2 (fun i c -> match i with Some i -> i | None ->
	  List.interval 0 (List.length ((lam_assum c))))
	  lemma_guard (Array.to_list fixdefs) in
*)
              let add c cb e =
                let exists c e =
                  try ignore(Environ.lookup_constant c e); true
                  with Not_found -> false in 
                if exists c e then e else Environ.add_constant c cb e in
              let env = List.fold_left (fun env { eff } ->
                match eff with
                | SEsubproof (c, cb,_) -> add c cb env
                | SEscheme (l,_) ->
                    List.fold_left (fun e (_,c,cb,_) -> add c cb e) env l)
                env (Safe_typing.side_effects_of_private_constants eff) in
              let indexes =
                search_guard Loc.ghost env
                  possible_indexes fixdecls in
		(mkFix ((indexes,0),fixdecls), ctx), eff
          | _ -> (body, ctx), eff) }

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), u) when
              let mind = Global.lookup_mind kn in
              mind.mind_finite == Decl_kinds.Finite && Option.is_empty b ->
              [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_all_stack env Evd.empty c))
        (Global.env()) hyps in
      let ind_hyps =
        List.flatten (List.map_i (fun i decl ->
          let t = get_type decl in
          match kind_of_term t with
          | Ind ((kn,_ as ind),u) when
                let mind = Global.lookup_mind kn in
                mind.mind_finite <> Decl_kinds.CoFinite && is_local_assum decl ->
              [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_all_stack cclenv Evd.empty ccl in
        match kind_of_term whnf_ccl with
        | Ind ((kn,_ as ind),u) when
              let mind = Global.lookup_mind kn in
              Int.equal mind.mind_ntypes n && mind.mind_finite == Decl_kinds.CoFinite ->
            [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',_),_,_) -> eq_mind 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),_,_) -> Int.equal 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 (List.is_empty rest);
          (* One occ. of common coind ccls and no common inductive hyps *)
	  if not (List.is_empty common_same_indhyp) then
	    if_verbose Feedback.msg_info (str "Assuming mutual coinductive statements.");
	  flush_all ();
          indccl, true, []
      | [], _::_ ->
          let () = match same_indccl with
          | ind :: _ ->
            if List.distinct_f ind_ord (List.map pi1 ind)
            then
              if_verbose Feedback.msg_info
                (strbrk
                   ("Coinductive statements do not follow the order of "^
                    "definition, assuming the proof to be by induction."));
            flush_all ()
          | _ -> ()
          in
          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 (Pp.str "Empty list of theorems.")

(* Saving a goal *)

let save ?export_seff id const cstrs pl do_guard (locality,poly,kind) hook =
  let fix_exn = Future.fix_exn_of const.Entries.const_entry_body in
  try
    let const = adjust_guardness_conditions const do_guard in
    let k = Kindops.logical_kind_of_goal_kind kind in
    let l,r = match locality with
      | Discharge when Lib.sections_are_opened () ->
          let c = SectionLocalDef const in
          let _ = declare_variable id (Lib.cwd(), c, k) in
          (Local, VarRef id)
      | Local | Global | Discharge ->
          let local = match locality with
          | Local | Discharge -> true
          | Global -> false
          in
          let kn =
           declare_constant ?export_seff id ~local (DefinitionEntry const, k) in
          (locality, ConstRef kn) in
    definition_message id;
    Option.iter (Universes.register_universe_binders r) pl;
    call_hook (fun exn -> exn) hook l r
  with e when CErrors.noncritical e ->
    let e = CErrors.push e in
    iraise (fix_exn e)

let default_thm_id = Id.of_string "Unnamed_thm"

let compute_proof_name locality = function
  | Some ((loc,id),pl) ->
      (* 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, pl
  | None ->
      next_global_ident_away default_thm_id (Pfedit.get_all_proof_names ()), None

let save_remaining_recthms (locality,p,kind) norm ctx body opaq i ((id,pl),(t_i,(_,imps))) =
  let t_i = norm t_i in
  match body with
  | None ->
      (match locality with
      | Discharge ->
          let impl = false in (* copy values from Vernacentries *)
          let k = IsAssumption Conjectural in
          let c = SectionLocalAssum ((t_i,ctx),p,impl) in
	  let _ = declare_variable id (Lib.cwd(),c,k) in
          (Discharge, VarRef id,imps)
      | Local | Global ->
          let k = IsAssumption Conjectural in
          let local = match locality with
          | Local -> true
          | Global -> false
          | Discharge -> assert false
          in
          let ctx = Univ.ContextSet.to_context ctx in
          let decl = (ParameterEntry (None,p,(t_i,ctx),None), k) in
          let kn = declare_constant id ~local decl in
          (locality,ConstRef kn,imps))
  | Some body ->
      let body = norm body in
      let k = Kindops.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 Pp.(str "Not a proof by induction: " ++ Printer.pr_constr body) in
      match locality with
      | Discharge ->
          let const = definition_entry ~types:t_i ~opaque:opaq ~poly:p 
	    ~univs:(Univ.ContextSet.to_context ctx) body_i in
	  let c = SectionLocalDef const in
	  let _ = declare_variable id (Lib.cwd(), c, k) in
          (Discharge,VarRef id,imps)
      | Local | Global ->
        let ctx = Univ.ContextSet.to_context ctx in
        let local = match locality with
        | Local -> true
        | Global -> false
        | Discharge -> assert false
        in
        let const =
	  Declare.definition_entry ~types:t_i ~poly:p ~univs:ctx ~opaque:opaq body_i
	in
        let kn = declare_constant id ~local (DefinitionEntry const, k) in
        (locality,ConstRef kn,imps)

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

let save_named ?export_seff proof =
  let id,const,(cstrs,pl),do_guard,persistence,hook = proof in
  save ?export_seff id const cstrs pl do_guard persistence hook

let check_anonymity id save_ident =
  if not (String.equal (atompart_of_id id) (Id.to_string (default_thm_id))) then
    error "This command can only be used for unnamed theorem."

let save_anonymous ?export_seff proof save_ident =
  let id,const,(cstrs,pl),do_guard,persistence,hook = proof in
  check_anonymity id save_ident;
  save ?export_seff save_ident const cstrs pl do_guard persistence hook

let save_anonymous_with_strength ?export_seff proof kind save_ident =
  let id,const,(cstrs,pl),do_guard,_,hook = proof in
  check_anonymity id save_ident;
  (* we consider that non opaque behaves as local for discharge *)
  save ?export_seff save_ident const cstrs pl do_guard
      (Global, const.const_entry_polymorphic, Proof kind) hook

(* Admitted *)

let warn_let_as_axiom =
  CWarnings.create ~name:"let-as-axiom" ~category:"vernacular"
                   (fun id -> strbrk "Let definition" ++ spc () ++ pr_id id ++
                                spc () ++ strbrk "declared as an axiom.")

let admit (id,k,e) pl hook () =
  let kn = declare_constant id (ParameterEntry e, IsAssumption Conjectural) in
  let () = match k with
  | Global, _, _ -> ()
  | Local, _, _ | Discharge, _, _ -> warn_let_as_axiom id
  in
  let () = assumption_message id in
  Option.iter (Universes.register_universe_binders (ConstRef kn)) pl;
  call_hook (fun exn -> exn) hook Global (ConstRef kn)

(* Starting a goal *)

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


let get_proof proof do_guard hook opacity =
  let (id,(const,univs,persistence)) =
    Pfedit.cook_this_proof proof
  in
  id,{const with const_entry_opaque = opacity},univs,do_guard,persistence,hook

let check_exist =
  List.iter (fun (loc,id) ->
    if not (Nametab.exists_cci (Lib.make_path id)) then
        user_err_loc (loc,"",pr_id id ++ str " does not exist.")
  )

let universe_proof_terminator compute_guard hook =
  let open Proof_global in
  make_terminator begin function
  | Admitted (id,k,pe,(ctx,pl)) ->
      admit (id,k,pe) pl (hook (Some ctx)) ();
      Feedback.feedback Feedback.AddedAxiom
  | Proved (opaque,idopt,proof) ->
      let is_opaque, export_seff, exports = match opaque with
        | Vernacexpr.Transparent -> false, true, []
        | Vernacexpr.Opaque None -> true, false, []
        | Vernacexpr.Opaque (Some l) -> true, true, l in
      let proof = get_proof proof compute_guard
	(hook (Some (fst proof.Proof_global.universes))) is_opaque in
      begin match idopt with
      | None -> save_named ~export_seff proof
      | Some ((_,id),None) -> save_anonymous ~export_seff proof id
      | Some ((_,id),Some kind) -> 
          save_anonymous_with_strength ~export_seff proof kind id
      end;
      check_exist exports
  end

let standard_proof_terminator compute_guard hook =
  universe_proof_terminator compute_guard (fun _ -> hook)

let start_proof id ?pl kind sigma ?terminator ?sign c ?init_tac ?(compute_guard=[]) hook =
  let terminator = match terminator with
  | None -> standard_proof_terminator compute_guard hook
  | Some terminator -> terminator compute_guard hook
  in
  let sign = 
    match sign with
    | Some sign -> sign
    | None -> initialize_named_context_for_proof ()
  in
  !start_hook c;
  Pfedit.start_proof id ?pl kind sigma sign c ?init_tac terminator

let start_proof_univs id ?pl kind sigma ?terminator ?sign c ?init_tac ?(compute_guard=[]) hook =
  let terminator = match terminator with
  | None -> universe_proof_terminator compute_guard hook
  | Some terminator -> terminator compute_guard hook
  in
  let sign = 
    match sign with
    | Some sign -> sign
    | None -> initialize_named_context_for_proof ()
  in
  !start_hook c;
  Pfedit.start_proof id ?pl kind sigma sign c ?init_tac terminator

let rec_tac_initializer finite guard thms snl =
  if finite then
    match List.map (fun ((id,_),(t,_)) -> (id,t)) thms with
    | (id,_)::l -> Tactics.mutual_cofix id l 0
    | _ -> 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 -> Tactics.mutual_fix id n l 0
       | _ -> assert false

let start_proof_with_initialization kind ctx recguard thms snl hook =
  let intro_tac (_, (_, (ids, _))) =
    Tacticals.New.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 
              Tacticals.New.tclTHENS rec_tac (List.map intro_tac thms)
            else
              rec_tac
        | Some tacl ->
            Tacticals.New.tclTHENS rec_tac
            (if Flags.is_auto_intros () then
              List.map2 (fun tac thm -> Tacticals.New.tclTHEN tac (intro_tac thm)) tacl thms
            else
              tacl)),guard
  | None ->
      let () = match thms with [_] -> () | _ -> assert false in
      (if Flags.is_auto_intros () then Some (intro_tac (List.hd thms)) else None), [] in
  match thms with
  | [] -> anomaly (Pp.str "No proof to start")
  | ((id,pl),(t,(_,imps)))::other_thms ->
      let hook ctx strength ref =
        let ctx = match ctx with
        | None -> Evd.empty_evar_universe_context
        | Some ctx -> ctx
        in
        let other_thms_data =
          if List.is_empty other_thms then [] else
            (* there are several theorems defined mutually *)
            let body,opaq = retrieve_first_recthm ref in
            let subst = Evd.evar_universe_context_subst ctx in
            let norm c = Universes.subst_opt_univs_constr subst c in
	    let ctx = UState.context_set (*FIXME*) ctx in
	    let body = Option.map norm body in
            List.map_i (save_remaining_recthms kind norm ctx 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;
	  call_hook (fun exn -> exn) hook strength ref) thms_data in
      start_proof_univs id ?pl kind ctx t ?init_tac (fun ctx -> mk_hook (hook ctx)) ~compute_guard:guard

let start_proof_com kind thms hook =
  let env0 = Global.env () in
  let levels = Option.map snd (fst (List.hd thms)) in 
  let evdref = ref (match levels with
		    | None -> Evd.from_env env0
		    | Some l -> Evd.from_ctx (Evd.make_evar_universe_context env0 l))
  in
  let thms = List.map (fun (sopt,(bl,t,guard)) ->
    let impls, ((env, ctx), imps) = interp_context_evars env0 evdref bl in
    let t', imps' = interp_type_evars_impls ~impls env evdref t in
    evdref := solve_remaining_evars all_and_fail_flags env !evdref (Evd.empty,!evdref);
    let ids = List.map get_name ctx in
      (compute_proof_name (pi1 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
  let evd, nf = Evarutil.nf_evars_and_universes !evdref in
  let thms = List.map (fun (n, (t, info)) -> (n, (nf t, info))) thms in
  let () =
    match levels with
    | None -> ()
    | Some l -> ignore (Evd.universe_context evd ?names:l)
  in
  let evd =
    if pi2 kind then evd
    else (* We fix the variables to ensure they won't be lowered to Set *)
      Evd.fix_undefined_variables evd
  in
    start_proof_with_initialization kind evd recguard thms snl hook


(* Saving a proof *)

let save_proof ?proof = function
  | Vernacexpr.Admitted ->
      let pe =
        let open Proof_global in
        match proof with
        | Some ({ id; entries; persistence = k; universes }, _) ->
            if List.length entries <> 1 then
              error "Admitted does not support multiple statements";
            let { const_entry_secctx; const_entry_type } = List.hd entries in
            if const_entry_type = None then
              error "Admitted requires an explicit statement";
            let typ = Option.get const_entry_type in
            let ctx = Evd.evar_context_universe_context (fst universes) in
            Admitted(id, k, (const_entry_secctx, pi2 k, (typ, ctx), None), universes)
        | None ->
            let pftree = Pfedit.get_pftreestate () in
            let id, k, typ = Pfedit.current_proof_statement () in
            let universes = Proof.initial_euctx pftree in
            (* This will warn if the proof is complete *)
            let pproofs, _univs =
              Proof_global.return_proof ~allow_partial:true () in
            let sec_vars =
              match  Pfedit.get_used_variables(), pproofs with
              | Some _ as x, _ -> x
              | None, (pproof, _) :: _ -> 
                  let env = Global.env () in
                  let ids_typ = Environ.global_vars_set env typ in
                  let ids_def = Environ.global_vars_set env pproof in
                  Some (Environ.keep_hyps env (Idset.union ids_typ ids_def))
              | _ -> None in
	    let names = Pfedit.get_universe_binders () in
            let evd = Evd.from_ctx universes in
            let binders, ctx = Evd.universe_context ?names evd in
            Admitted(id,k,(sec_vars, pi2 k, (typ, ctx), None),
		     (universes, Some binders))
      in
      Proof_global.apply_terminator (Proof_global.get_terminator ()) pe
  | Vernacexpr.Proved (is_opaque,idopt) ->
      let (proof_obj,terminator) =
        match proof with
        | None ->
            Proof_global.close_proof ~keep_body_ucst_separate:false (fun x -> x)
        | Some proof -> proof
      in
      (* if the proof is given explicitly, nothing has to be deleted *)
      if Option.is_empty proof then Pfedit.delete_current_proof ();
      Proof_global.(apply_terminator terminator (Proved (is_opaque,idopt,proof_obj)))

(* Miscellaneous *)

let get_current_context () =
  Pfedit.get_current_context ()