package coq-core

  1. Overview
  2. Docs
package coq-core
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Source file elim.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
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
(************************************************************************)
(*         *   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 Names
open Constr
open Termops
open EConstr
open Inductiveops
open Hipattern
open Tacmach
open Tacticals
open Clenv
open Tactics

type branch_args = {
  branchnum  : int;         (* the branch number *)
  nassums    : int;         (* number of assumptions/letin to be introduced *)
  branchsign : bool list;   (* the signature of the branch.
                               true=assumption, false=let-in *)
  branchnames : Tactypes.intro_patterns}

type elim_kind = Case of bool | Elim

(* Find the right elimination suffix corresponding to the sort of the goal *)
(* c should be of type A1->.. An->B with B an inductive definition *)
let general_elim_then_using mk_elim
    rec_flag allnames tac predicate (ind, u, args) id =
  let open Pp in
  Proofview.Goal.enter begin fun gl ->
    let env = Proofview.Goal.env gl in
    let sigma = Proofview.Goal.sigma gl in
    let sort = Retyping.get_sort_family_of env sigma (Proofview.Goal.concl gl) in
    let sigma, elim, elimt = match mk_elim with
    | Case dep ->
      let u = EInstance.kind sigma u in
      let (sigma, r, t) = Indrec.build_case_analysis_scheme env sigma (ind, u) dep sort in
      (sigma, EConstr.of_constr r, EConstr.of_constr t)
    | Elim ->
      let gr = Indrec.lookup_eliminator env ind sort in
      let sigma, r = Evd.fresh_global env sigma gr in
      (sigma, r, Retyping.get_type_of env sigma r)
    in
    (* applying elimination_scheme just a little modified *)
    let elimclause = mk_clenv_from env sigma (elim, elimt) in
    let indmv =
      match EConstr.kind elimclause.evd (last_arg elimclause.evd elimclause.templval.Evd.rebus) with
      | Meta mv -> mv
      | _         -> CErrors.anomaly (str"elimination.")
    in
    let pmv =
      let p, _ = decompose_app elimclause.evd elimclause.templtyp.Evd.rebus in
      match EConstr.kind elimclause.evd p with
      | Meta p -> p
      | _ ->
          let name_elim =
            match EConstr.kind sigma elim with
            | Const _ | Var _ -> str " " ++ Printer.pr_econstr_env env sigma elim
            | _ -> mt ()
          in
          CErrors.user_err
            (str "The elimination combinator " ++ name_elim ++ str " is unknown.")
    in
    let elimclause' = clenv_instantiate indmv elimclause (mkVar id, mkApp (mkIndU (ind, u), args)) in
    let branchsigns = Tacticals.compute_constructor_signatures env ~rec_flag (ind, u) in
    let brnames = Tacticals.compute_induction_names false branchsigns allnames in
    let flags = Unification.elim_flags () in
    let elimclause' =
      match predicate with
      | None   -> elimclause'
      | Some p -> clenv_unify ~flags Reduction.CONV (mkMeta pmv) p elimclause'
    in
    let after_tac i =
      let ba = { branchsign = branchsigns.(i);
                  branchnames = brnames.(i);
                  nassums = List.length branchsigns.(i);
                  branchnum = i+1; }
      in
      tac ba
    in
    let branchtacs = List.init (Array.length branchsigns) after_tac in
    Proofview.tclTHEN
      (Clenv.res_pf ~flags elimclause')
      (Proofview.tclEXTEND [] tclIDTAC branchtacs)
  end

(* computing the case/elim combinators *)

let make_elim_branch_assumptions ba hyps =
  let assums =
    try List.rev (List.firstn ba.nassums hyps)
    with Failure _ -> CErrors.anomaly (Pp.str "make_elim_branch_assumptions.") in
  assums

let elim_on_ba tac ba =
  Proofview.Goal.enter begin fun gl ->
  let branches = make_elim_branch_assumptions ba (Proofview.Goal.hyps gl) in
  tac branches
  end

let elimination_then tac id =
  let open Declarations in
  Proofview.Goal.enter begin fun gl ->
  let env = Proofview.Goal.env gl in
  let ((ind, u), t) = pf_apply Tacred.reduce_to_atomic_ind gl (pf_get_type_of gl (mkVar id)) in
  let _, args = decompose_app_vect (Proofview.Goal.sigma gl) t in
  let isrec,mkelim =
    match (Environ.lookup_mind (fst ind) env).mind_record with
    | NotRecord -> true, Elim
    | FakeRecord | PrimRecord _ -> false, Case true
  in
  general_elim_then_using mkelim isrec None tac None (ind, u, args) id
  end

(* Supposed to be called without as clause *)
let introElimAssumsThen tac ba =
  assert (ba.branchnames == []);
  let introElimAssums = tclDO ba.nassums intro in
  (tclTHEN introElimAssums (elim_on_ba tac ba))

(* Supposed to be called with a non-recursive scheme *)
let introCaseAssumsThen with_evars tac ba =
  let n1 = List.length ba.branchsign in
  let n2 = List.length ba.branchnames in
  let (l1,l2),l3 =
    if n1 < n2 then List.chop n1 ba.branchnames, []
    else (ba.branchnames, []), List.make (n1-n2) false in
  let introCaseAssums =
    tclTHEN (intro_patterns with_evars l1) (intros_clearing l3) in
  (tclTHEN introCaseAssums (elim_on_ba (tac l2) ba))

let case_tac dep names tac elim ind c =
  let tac = introCaseAssumsThen false (* ApplyOn not supported by inversion *) tac in
  general_elim_then_using (Case dep) false names tac (Some elim) ind c

(* The following tactic Decompose repeatedly applies the
   elimination(s) rule(s) of the types satisfying the predicate
   ``recognizer'' onto a certain hypothesis. For example :

Require Elim.
Require Le.
   Goal (y:nat){x:nat | (le O x)/\(le x y)}->{x:nat | (le O x)}.
   Intros y H.
   Decompose [sig and] H;EAuto.
   Qed.

Another example :

   Goal (A,B,C:Prop)(A/\B/\C \/ B/\C \/ C/\A) -> C.
   Intros A B C H; Decompose [and or] H; Assumption.
   Qed.
*)

let rec general_decompose_on_hyp recognizer =
  ifOnHyp recognizer (general_decompose_aux recognizer) (fun _ -> Proofview.tclUNIT())

and general_decompose_aux recognizer id =
  elimination_then
    (introElimAssumsThen
       (fun bas ->
          tclTHEN (clear [id])
            (tclMAP (general_decompose_on_hyp recognizer)
               (ids_of_named_context bas))))
    id

(* We should add a COMPLETE to be sure that the created hypothesis
   doesn't stay if no elimination is possible *)

(* Best strategies but loss of compatibility *)
let tmphyp_name = Id.of_string "_TmpHyp"

let general_decompose recognizer c =
  Proofview.Goal.enter begin fun gl ->
  let typc = pf_get_type_of gl c in
  tclTHENS (cut typc)
    [ intro_using_then tmphyp_name (fun id ->
          ifOnHyp recognizer (general_decompose_aux recognizer)
            (fun id -> clear [id])
            id);
       exact_no_check c ]
  end

let head_in indl t gl =
  let sigma = Tacmach.project gl in
  try
    let ity,_ = extract_mrectype sigma t in
    List.exists (fun i -> Ind.CanOrd.equal (fst i) (fst ity)) indl
  with Not_found -> false

let decompose_these c l =
  Proofview.Goal.enter begin fun gl ->
  let indl = List.map (fun x -> x, Univ.Instance.empty) l in
  general_decompose (fun env sigma (_,t) -> head_in indl t gl) c
  end

let decompose_and c =
  general_decompose
    (fun env sigma (_,t) -> is_record env sigma t)
    c

let decompose_or c =
  general_decompose
    (fun env sigma (_,t) -> is_disjunction env sigma t)
    c

let h_decompose l c = decompose_these c l

let h_decompose_or = decompose_or

let h_decompose_and = decompose_and
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct