Source file `recLemmas.ml`

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
(************************************************************************)
(*         *   The Coq Proof Assistant / The Coq Development Team       *)
(*  v      *         Copyright INRIA, CNRS and contributors             *)
(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(*   \VV/  **************************************************************)
(*    //   *    This file is distributed under the terms of the         *)
(*         *     GNU Lesser General Public License Version 2.1          *)
(*         *     (see LICENSE file for the text of the license)         *)
(************************************************************************)

open Util
open Constr
open Declarations

module RelDecl = Context.Rel.Declaration

let find_mutually_recursive_statements sigma thms =
    let inds = List.map (fun x ->
      let typ = Declare.CInfo.get_typ x in
      let (hyps,ccl) = EConstr.decompose_prod_decls sigma typ in
      let whnf_hyp_hds = EConstr.map_rel_context_in_env
        (fun env c -> fst (Reductionops.whd_all_stack env sigma c))
        (Global.env()) hyps in
      let ind_hyps =
        List.flatten (List.map_i (fun i decl ->
          let t = RelDecl.get_type decl in
          match EConstr.kind sigma t with
          | Ind ((kn,_ as ind),u) when
                let mind = Global.lookup_mind kn in
                mind.mind_finite <> Declarations.CoFinite ->
              [ind,x,i]
          | _ ->
              []) 0 (List.rev (List.filter Context.Rel.Declaration.is_local_assum whnf_hyp_hds))) in
      let ind_ccl =
        let cclenv = EConstr.push_rel_context hyps (Global.env()) in
        let whnf_ccl,_ = Reductionops.whd_all_stack cclenv sigma ccl in
        match EConstr.kind sigma whnf_ccl with
        | Ind ((kn,_ as ind),u) when (Global.lookup_mind kn).mind_finite == Declarations.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',_),_,_) -> Environ.QMutInd.equal (Global.env ()) 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 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 possibly_cofix = not (List.is_empty same_indccl) in (* all conclusions are coinductive *)
    let possible_fix_indices =
      match common_same_indhyp with
      | [] -> []
      | _::_ ->
        (* assume the largest indices as possible *)
        List.map (List.map pi3) inds_hyps in
    if not possibly_cofix && List.is_empty possible_fix_indices then
      CErrors.user_err Pp.(str
         ("Cannot find common (mutual) inductive premises or coinductive" ^
          " conclusions in the statements."));
    Pretyping.{possibly_cofix; possible_fix_indices}

type mutual_info =
  | NonMutual of EConstr.t Declare.CInfo.t
  | Mutual of Pretyping.possible_guard

let look_for_possibly_mutual_statements sigma thms : mutual_info =
  match thms with
  | [thm] ->
      (* One non recursively proved theorem *)
    NonMutual thm
  | _::_ as thms ->
    (* More than one statement and/or an explicit decreasing mark: *)
    Mutual (find_mutually_recursive_statements sigma thms)
  | [] -> CErrors.anomaly (Pp.str "Empty list of theorems.")