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
|
(***********************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
(* \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 Nameops
open Term
open Termops
open Reductionops
open Inductiveops
open Evd
open Environ
open Proof_trees
open Clenv
open Pattern
open Coqlib
open Declarations
(* I implemented the following functions which test whether a term t
is an inductive but non-recursive type, a general conjuction, a
general disjunction, or a type with no constructors.
They are more general than matching with or_term, and_term, etc,
since they do not depend on the name of the type. Hence, they
also work on ad-hoc disjunctions introduced by the user.
-- Eduardo (6/8/97). *)
type 'a matching_function = constr -> 'a option
type testing_function = constr -> bool
let op2bool = function Some _ -> true | None -> false
let match_with_non_recursive_type t =
match kind_of_term t with
| App _ ->
let (hdapp,args) = decompose_app t in
(match kind_of_term hdapp with
| Ind ind ->
if not (Global.lookup_mind (fst ind)).mind_finite then
Some (hdapp,args)
else
None
| _ -> None)
| _ -> None
let is_non_recursive_type t = op2bool (match_with_non_recursive_type t)
(* A general conjunction type is a non-recursive inductive type with
only one constructor. *)
let match_with_conjunction t =
let (hdapp,args) = decompose_app t in
match kind_of_term hdapp with
| Ind ind ->
let (mib,mip) = Global.lookup_inductive ind in
if (Array.length mip.mind_consnames = 1)
&& (not (mis_is_recursive (ind,mib,mip)))
&& (mip.mind_nrealargs = 0)
then
Some (hdapp,args)
else
None
| _ -> None
let is_conjunction t = op2bool (match_with_conjunction t)
(* A general disjunction type is a non-recursive inductive type all
whose constructors have a single argument. *)
let match_with_disjunction t =
let (hdapp,args) = decompose_app t in
match kind_of_term hdapp with
| Ind ind ->
let car = mis_constr_nargs ind in
if array_for_all (fun ar -> ar = 1) car &&
(let (mib,mip) = Global.lookup_inductive ind in
not (mis_is_recursive (ind,mib,mip)))
then
Some (hdapp,args)
else
None
| _ -> None
let is_disjunction t = op2bool (match_with_disjunction t)
let match_with_empty_type t =
let (hdapp,args) = decompose_app t in
match (kind_of_term hdapp) with
| Ind ind ->
let (mib,mip) = Global.lookup_inductive ind in
let nconstr = Array.length mip.mind_consnames in
if nconstr = 0 then Some hdapp else None
| _ -> None
let is_empty_type t = op2bool (match_with_empty_type t)
let match_with_unit_type t =
let (hdapp,args) = decompose_app t in
match (kind_of_term hdapp) with
| Ind ind ->
let (mib,mip) = Global.lookup_inductive ind in
let constr_types = mip.mind_nf_lc in
let nconstr = Array.length mip.mind_consnames in
let zero_args c =
nb_prod c = mip.mind_nparams in
if nconstr = 1 && array_for_all zero_args constr_types then
Some hdapp
else
None
| _ -> None
let is_unit_type t = op2bool (match_with_unit_type t)
(* Checks if a given term is an application of an
inductive binary relation R, so that R has only one constructor
establishing its reflexivity. *)
(* ["(A : ?)(x:A)(? A x x)"] and ["(x : ?)(? x x)"] *)
let x = Name (id_of_string "x")
let y = Name (id_of_string "y")
let name_A = Name (id_of_string "A")
let coq_refl_rel1_pattern =
PProd
(name_A, PMeta None,
PProd (x, PRel 1, PApp (PMeta None, [|PRel 2; PRel 1; PRel 1|])))
let coq_refl_rel2_pattern =
PProd (x, PMeta None, PApp (PMeta None, [|PRel 1; PRel 1|]))
let coq_refl_reljm_pattern =
PProd
(name_A, PMeta None,
PProd (x, PRel 1, PApp (PMeta None, [|PRel 2; PRel 1; PRel 2;PRel 1|])))
let match_with_equation t =
let (hdapp,args) = decompose_app t in
match (kind_of_term hdapp) with
| Ind ind ->
let (mib,mip) = Global.lookup_inductive ind in
let constr_types = mip.mind_nf_lc in
let nconstr = Array.length mip.mind_consnames in
if nconstr = 1 &&
(is_matching coq_refl_rel1_pattern constr_types.(0) ||
is_matching coq_refl_rel2_pattern constr_types.(0) ||
is_matching coq_refl_reljm_pattern constr_types.(0))
then
Some (hdapp,args)
else
None
| _ -> None
let is_equation t = op2bool (match_with_equation t)
(* ["(?1 -> ?2)"] *)
let imp a b = PProd (Anonymous, a, b)
let coq_arrow_pattern = imp (PMeta (Some 1)) (PMeta (Some 2))
let match_with_nottype t =
try
match matches coq_arrow_pattern t with
| [(1,arg);(2,mind)] ->
if is_empty_type mind then Some (mind,arg) else None
| _ -> anomaly "Incorrect pattern matching"
with PatternMatchingFailure -> None
let is_nottype t = op2bool (match_with_nottype t)
let is_imp_term c =
match kind_of_term c with
| Prod (_,_,b) -> not (dependent (mkRel 1) b)
| _ -> false
let rec has_nodep_prod_after n c =
match kind_of_term c with
| Prod (_,_,b) ->
( n>0 || not (dependent (mkRel 1) b))
&& (has_nodep_prod_after (n-1) b)
| _ -> true
let has_nodep_prod = has_nodep_prod_after 0
let match_with_nodep_ind t =
let (hdapp,args) = decompose_app t in
match (kind_of_term hdapp) with
| Ind ind ->
let (mib,mip) = Global.lookup_inductive ind in
let constr_types = mip.mind_nf_lc in
let nodep_constr = has_nodep_prod_after mip.mind_nparams in
if array_for_all nodep_constr constr_types then
Some (hdapp,args)
else
None
| _ -> None
let is_nodep_ind t=op2bool (match_with_nodep_ind t)
|
