aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics/elim.ml
blob: 2601cd4c5f65080b853dd3b9ed87f1ec2d8f9a69 (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
(************************************************************************)
(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
(*   \VV/  **************************************************************)
(*    //   *      This file is distributed under the terms of the       *)
(*         *       GNU Lesser General Public License Version 2.1        *)
(************************************************************************)

(* $Id$ *)

open Pp
open Util
open Names
open Term
open Termops
open Environ
open Libnames
open Reduction
open Inductiveops
open Proof_type
open Clenv
open Hipattern
open Tacmach
open Tacticals
open Tactics
open Hiddentac
open Genarg
open Tacexpr

let introElimAssumsThen tac ba =
  let nassums = 
    List.fold_left 
      (fun acc b -> if b then acc+2 else acc+1) 
      0 ba.branchsign 
  in 
  let introElimAssums = tclDO nassums intro in 
  (tclTHEN introElimAssums (elim_on_ba tac ba))

let introCaseAssumsThen tac ba =
  let case_thin_sign =
    List.flatten
      (List.map (function b -> if b then [false;true] else [false])
	ba.branchsign)
  in 
  let n1 = List.length case_thin_sign in
  let n2 = List.length ba.branchnames in
  let (l1,l2),l3 =
    if n1 < n2 then list_chop n1 ba.branchnames, []
    else 
      (ba.branchnames, []),
       if n1 > n2 then snd (list_chop n2 case_thin_sign) else [] in
  let introCaseAssums =
    tclTHEN (intros_pattern no_move l1) (intros_clearing l3) in
  (tclTHEN introCaseAssums (case_on_ba (tac l2) ba))

(* 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 elimHypThen tac id gl =
  elimination_then tac ([],[]) (mkVar id) gl

let rec general_decompose_on_hyp recognizer =
  ifOnHyp recognizer (general_decompose recognizer) (fun _ -> tclIDTAC)

and general_decompose recognizer id =
  elimHypThen
    (introElimAssumsThen
       (fun bas ->
	  tclTHEN (clear [id])
	    (tclMAP (general_decompose_on_hyp recognizer)
               (ids_of_named_context bas.assums))))
    id

(* Faudrait ajouter un COMPLETE pour que l'hypothèse créée ne reste
   pas si aucune élimination n'est possible *)

(* Meilleures stratégies mais perte de compatibilité *)
let tmphyp_name = id_of_string "_TmpHyp"
let up_to_delta = ref false (* true *)

let general_decompose recognizer c gl = 
  let typc = pf_type_of gl c in  
  tclTHENSV (cut typc) 
    [| tclTHEN (intro_using tmphyp_name)
         (onLastHyp
	    (ifOnHyp recognizer (general_decompose recognizer)
	      (fun id -> clear [id])));
       exact_no_check c |] gl

let head_in gls indl t =
  try
    let ity,_ =
      if !up_to_delta
      then find_mrectype (pf_env gls) (project gls) t
      else extract_mrectype t
    in List.mem ity indl
  with Not_found -> false
       
let inductive_of = function
  | IndRef ity -> ity
  | r ->
      errorlabstrm "Decompose"
        (Printer.pr_global r ++ str " is not an inductive type.")

let decompose_these c l gls =
  let indl = (*List.map inductive_of*) l in 
  general_decompose (fun (_,t) -> head_in gls indl t) c gls

let decompose_nonrec c gls =
  general_decompose 
    (fun (_,t) -> is_non_recursive_type t)
    c gls

let decompose_and c gls = 
  general_decompose 
    (fun (_,t) -> is_conjunction t)
    c gls

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

let inj_open c = (Evd.empty,c)

let h_decompose l c =
  Refiner.abstract_tactic (TacDecompose (l,inj_open c)) (decompose_these c l)

let h_decompose_or c =
  Refiner.abstract_tactic (TacDecomposeOr (inj_open c)) (decompose_or c)

let h_decompose_and c =
  Refiner.abstract_tactic (TacDecomposeAnd (inj_open c)) (decompose_and c)

(* The tactic Double performs a double induction *)

let simple_elimination c gls =
  simple_elimination_then (fun _ -> tclIDTAC) c gls

let induction_trailer abs_i abs_j bargs =
  tclTHEN 
    (tclDO (abs_j - abs_i) intro)
    (onLastHyp
       (fun id gls ->
	  let idty = pf_type_of gls (mkVar id) in
	  let fvty = global_vars (pf_env gls) idty in
	  let possible_bring_hyps =
	    (List.tl (nLastHyps (abs_j - abs_i) gls)) @ bargs.assums
          in
	  let (hyps,_) =
            List.fold_left 
	      (fun (bring_ids,leave_ids) (cid,_,cidty as d) ->
                 if not (List.mem cid leave_ids)
                 then (d::bring_ids,leave_ids)
                 else (bring_ids,cid::leave_ids))
	      ([],fvty) possible_bring_hyps
	  in
          let ids = List.rev (ids_of_named_context hyps) in
	  (tclTHENSEQ
            [bring_hyps hyps; tclTRY (clear ids); 
	     simple_elimination (mkVar id)])
          gls))

let double_ind h1 h2 gls =
  let abs_i = depth_of_quantified_hypothesis true h1 gls in
  let abs_j = depth_of_quantified_hypothesis true h2 gls in
  let (abs_i,abs_j) =
    if abs_i < abs_j then (abs_i,abs_j) else
    if abs_i > abs_j then (abs_j,abs_i) else
      error "Both hypotheses are the same." in
  (tclTHEN (tclDO abs_i intro)
     (onLastHyp
       	(fun id ->
           elimination_then
             (introElimAssumsThen (induction_trailer abs_i abs_j))
             ([],[]) (mkVar id)))) gls

let h_double_induction h1 h2 =
  Refiner.abstract_tactic (TacDoubleInduction (h1,h2)) (double_ind h1 h2)