← Back to branch summary

~ubuntu-branches/ubuntu/wily/coq-doc/wily

« back to all changes in this revision

Viewing changes to tactics/elim.ml

  • Committer: Bazaar Package Importer
  • Author(s): Stéphane Glondu, Stéphane Glondu, Samuel Mimram
  • Date: 2010-01-07 22:50:39 UTC
  • mfrom: (1.2.2 upstream)
  • Revision ID: james.westby@ubuntu.com-20100107225039-n3cq82589u0qt0s2
Tags: 8.2pl1-1
http://bugs.debian.org/563669
http://bugs.debian.org/543545
[ Stéphane Glondu ]
* New upstream release (Closes: #563669)
  - remove patches
* Packaging overhaul:
  - use git, advertise it in Vcs-* fields of debian/control
  - use debhelper 7 and dh with override
  - use source format 3.0 (quilt)
* debian/control:
  - set Maintainer to d-o-m, set Uploaders to Sam and myself
  - add Homepage field
  - bump Standards-Version to 3.8.3
* Register PDF documentation into doc-base
* Add debian/watch
* Update debian/copyright

[ Samuel Mimram ]
* Change coq-doc's description to mention that it provides documentation in
  pdf format, not postscript, closes: #543545.

Show diffs side-by-side

added added

removed removed

Lines of Context:
tactics/elim.ml
 
1
(************************************************************************)
 
2
(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
 
3
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
 
4
(*   \VV/  **************************************************************)
 
5
(*    //   *      This file is distributed under the terms of the       *)
 
6
(*         *       GNU Lesser General Public License Version 2.1        *)
 
7
(************************************************************************)
 
8
 
 
9
(* $Id: elim.ml 11739 2009-01-02 19:33:19Z herbelin $ *)
 
10
 
 
11
open Pp
 
12
open Util
 
13
open Names
 
14
open Term
 
15
open Termops
 
16
open Environ
 
17
open Libnames
 
18
open Reduction
 
19
open Inductiveops
 
20
open Proof_type
 
21
open Clenv
 
22
open Hipattern
 
23
open Tacmach
 
24
open Tacticals
 
25
open Tactics
 
26
open Hiddentac
 
27
open Genarg
 
28
open Tacexpr
 
29
 
 
30
let introElimAssumsThen tac ba =
 
31
  let nassums = 
 
32
    List.fold_left 
 
33
      (fun acc b -> if b then acc+2 else acc+1) 
 
34
      0 ba.branchsign 
 
35
  in 
 
36
  let introElimAssums = tclDO nassums intro in 
 
37
  (tclTHEN introElimAssums (elim_on_ba tac ba))
 
38
 
 
39
let introCaseAssumsThen tac ba =
 
40
  let case_thin_sign =
 
41
    List.flatten
 
42
      (List.map (function b -> if b then [false;true] else [false])
 
43
        ba.branchsign)
 
44
  in 
 
45
  let n1 = List.length case_thin_sign in
 
46
  let n2 = List.length ba.branchnames in
 
47
  let (l1,l2),l3 =
 
48
    if n1 < n2 then list_chop n1 ba.branchnames, []
 
49
    else 
 
50
      (ba.branchnames, []),
 
51
       if n1 > n2 then snd (list_chop n2 case_thin_sign) else [] in
 
52
  let introCaseAssums =
 
53
    tclTHEN (intros_pattern no_move l1) (intros_clearing l3) in
 
54
  (tclTHEN introCaseAssums (case_on_ba (tac l2) ba))
 
55
 
 
56
(* The following tactic Decompose repeatedly applies the
 
57
   elimination(s) rule(s) of the types satisfying the predicate
 
58
   ``recognizer'' onto a certain hypothesis. For example :
 
59
 
 
60
Require Elim.
 
61
Require Le.
 
62
   Goal (y:nat){x:nat | (le O x)/\(le x y)}->{x:nat | (le O x)}.
 
63
   Intros y H.
 
64
   Decompose [sig and] H;EAuto.
 
65
   Qed.
 
66
 
 
67
Another example :
 
68
 
 
69
   Goal (A,B,C:Prop)(A/\B/\C \/ B/\C \/ C/\A) -> C.
 
70
   Intros A B C H; Decompose [and or] H; Assumption.
 
71
   Qed.
 
72
*)
 
73
 
 
74
let elimHypThen tac id gl =
 
75
  elimination_then tac ([],[]) (mkVar id) gl
 
76
 
 
77
let rec general_decompose_on_hyp recognizer =
 
78
  ifOnHyp recognizer (general_decompose recognizer) (fun _ -> tclIDTAC)
 
79
 
 
80
and general_decompose recognizer id =
 
81
  elimHypThen
 
82
    (introElimAssumsThen
 
83
       (fun bas ->
 
84
          tclTHEN (clear [id])
 
85
            (tclMAP (general_decompose_on_hyp recognizer)
 
86
               (ids_of_named_context bas.assums))))
 
87
    id
 
88
 
 
89
(* Faudrait ajouter un COMPLETE pour que l'hypoth�se cr��e ne reste
 
90
   pas si aucune �limination n'est possible *)
 
91
 
 
92
(* Meilleures strat�gies mais perte de compatibilit� *)
 
93
let tmphyp_name = id_of_string "_TmpHyp"
 
94
let up_to_delta = ref false (* true *)
 
95
 
 
96
let general_decompose recognizer c gl = 
 
97
  let typc = pf_type_of gl c in  
 
98
  tclTHENSV (cut typc) 
 
99
    [| tclTHEN (intro_using tmphyp_name)
 
100
         (onLastHyp
 
101
            (ifOnHyp recognizer (general_decompose recognizer)
 
102
              (fun id -> clear [id])));
 
103
       exact_no_check c |] gl
 
104
 
 
105
let head_in gls indl t =
 
106
  try
 
107
    let ity,_ =
 
108
      if !up_to_delta
 
109
      then find_mrectype (pf_env gls) (project gls) t
 
110
      else extract_mrectype t
 
111
    in List.mem ity indl
 
112
  with Not_found -> false
 
113
       
 
114
let inductive_of = function
 
115
  | IndRef ity -> ity
 
116
  | r ->
 
117
      errorlabstrm "Decompose"
 
118
        (Printer.pr_global r ++ str " is not an inductive type.")
 
119
 
 
120
let decompose_these c l gls =
 
121
  let indl = (*List.map inductive_of*) l in 
 
122
  general_decompose (fun (_,t) -> head_in gls indl t) c gls
 
123
 
 
124
let decompose_nonrec c gls =
 
125
  general_decompose 
 
126
    (fun (_,t) -> is_non_recursive_type t)
 
127
    c gls
 
128
 
 
129
let decompose_and c gls = 
 
130
  general_decompose 
 
131
    (fun (_,t) -> is_record t)
 
132
    c gls
 
133
 
 
134
let decompose_or c gls = 
 
135
  general_decompose 
 
136
    (fun (_,t) -> is_disjunction t)
 
137
    c gls
 
138
 
 
139
let inj_open c = (Evd.empty,c)
 
140
 
 
141
let h_decompose l c =
 
142
  Refiner.abstract_tactic (TacDecompose (l,inj_open c)) (decompose_these c l)
 
143
 
 
144
let h_decompose_or c =
 
145
  Refiner.abstract_tactic (TacDecomposeOr (inj_open c)) (decompose_or c)
 
146
 
 
147
let h_decompose_and c =
 
148
  Refiner.abstract_tactic (TacDecomposeAnd (inj_open c)) (decompose_and c)
 
149
 
 
150
(* The tactic Double performs a double induction *)
 
151
 
 
152
let simple_elimination c gls =
 
153
  simple_elimination_then (fun _ -> tclIDTAC) c gls
 
154
 
 
155
let induction_trailer abs_i abs_j bargs =
 
156
  tclTHEN 
 
157
    (tclDO (abs_j - abs_i) intro)
 
158
    (onLastHyp
 
159
       (fun id gls ->
 
160
          let idty = pf_type_of gls (mkVar id) in
 
161
          let fvty = global_vars (pf_env gls) idty in
 
162
          let possible_bring_hyps =
 
163
            (List.tl (nLastHyps (abs_j - abs_i) gls)) @ bargs.assums
 
164
          in
 
165
          let (hyps,_) =
 
166
            List.fold_left 
 
167
              (fun (bring_ids,leave_ids) (cid,_,cidty as d) ->
 
168
                 if not (List.mem cid leave_ids)
 
169
                 then (d::bring_ids,leave_ids)
 
170
                 else (bring_ids,cid::leave_ids))
 
171
              ([],fvty) possible_bring_hyps
 
172
          in
 
173
          let ids = List.rev (ids_of_named_context hyps) in
 
174
          (tclTHENSEQ
 
175
            [bring_hyps hyps; tclTRY (clear ids); 
 
176
             simple_elimination (mkVar id)])
 
177
          gls))
 
178
 
 
179
let double_ind h1 h2 gls =
 
180
  let abs_i = depth_of_quantified_hypothesis true h1 gls in
 
181
  let abs_j = depth_of_quantified_hypothesis true h2 gls in
 
182
  let (abs_i,abs_j) =
 
183
    if abs_i < abs_j then (abs_i,abs_j) else
 
184
    if abs_i > abs_j then (abs_j,abs_i) else
 
185
      error "Both hypotheses are the same." in
 
186
  (tclTHEN (tclDO abs_i intro)
 
187
     (onLastHyp
 
188
        (fun id ->
 
189
           elimination_then
 
190
             (introElimAssumsThen (induction_trailer abs_i abs_j))
 
191
             ([],[]) (mkVar id)))) gls
 
192
 
 
193
let h_double_induction h1 h2 =
 
194
  Refiner.abstract_tactic (TacDoubleInduction (h1,h2)) (double_ind h1 h2)
 
195
 
 
196