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
218
219
220
221
222
223
224
225
226
227
228
229
|
(***********************************************************************)
(* 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 *)
(***********************************************************************)
(*i camlp4deps: "parsing/grammar.cma" i*)
(* $Id$ *)
(* This file is the interface between the c-c algorithm and Coq *)
open Evd
open Proof_type
open Names
open Libnames
open Nameops
open Inductiveops
open Declarations
open Term
open Termops
open Tacmach
open Tactics
open Tacticals
open Ccalgo
open Tacinterp
open Ccproof
open Pp
open Util
open Format
exception Not_an_eq
let fail()=raise Not_an_eq
let constant dir s = lazy (Coqlib.gen_constant "CC" dir s)
let f_equal_theo = constant ["Init";"Logic"] "f_equal"
let eq_rect_theo = constant ["Init";"Logic"] "eq_rect"
(* decompose member of equality in an applicative format *)
let rec decompose_term env t=
match kind_of_term t with
App (f,args)->
let tf=decompose_term env f in
let targs=Array.map (decompose_term env) args in
Array.fold_left (fun s t->Appli (s,t)) tf targs
| Construct c->
let (_,oib)=Global.lookup_inductive (fst c) in
let nargs=mis_constructor_nargs_env env c in
Constructor (c,nargs,nargs-oib.mind_nparams)
| _ ->(Symb t)
(* decompose equality in members and type *)
let eq_type_of_term term=
match kind_of_term term with
App (f,args)->
(try
let ref = reference_of_constr f in
if ref=Coqlib.glob_eq && (Array.length args)=3
then (args.(0),args.(1),args.(2))
else fail()
with
Not_found -> fail ())
| _ ->fail ()
(* read an equality *)
let read_eq env term=
let (_,t1,t2)=eq_type_of_term term in
(decompose_term env t1,decompose_term env t2)
(* rebuild a term from applicative format *)
let rec make_term=function
Symb s->s
| Constructor(c,_,_)->mkConstruct c
| Appli (s1,s2)->make_app [(make_term s2)] s1
and make_app l=function
Symb s->applistc s l
| Constructor(c,_,_)->applistc (mkConstruct c) l
| Appli (s1,s2)->make_app ((make_term s2)::l) s1
(* store all equalities from the context *)
let rec read_hyps env=function
[]->[]
| (id,_,e)::hyps->let q=(read_hyps env hyps) in
try (id,(read_eq env e))::q with Not_an_eq -> q
(* build a problem ( i.e. read the goal as an equality ) *)
let make_prb gl=
let env=pf_env gl in
let hyps=read_hyps env gl.it.evar_hyps in
try (hyps,Some (read_eq env gl.it.evar_concl)) with
Not_an_eq -> (hyps,None)
(* indhyps builds the array of arrays of constructor hyps for (ind largs) *)
let build_projection intype outtype (cstr:constructor) special default gls=
let (h,argv) =
try destApplication intype with
Invalid_argument _ -> (intype,[||]) in
let ind=destInd h in
let (mib,mip) = Global.lookup_inductive ind in
let n = mip.mind_nparams in
(* assert (n=(Array.length argv));*)
let lp=Array.length mip.mind_consnames in
let types=mip.mind_nf_lc in
let ci=(snd cstr)-1 in
let branch i=
let ti=Term.prod_appvect types.(i) argv in
let rc=fst (Sign.decompose_prod_assum ti) in
let head=
if i=ci then special else default in
Sign.it_mkLambda_or_LetIn head rc in
let branches=Array.init lp branch in
let casee=mkRel 1 in
let pred=mkLambda(Anonymous,intype,outtype) in
let env=pf_env gls in
let case_info=make_default_case_info (pf_env gls) RegularStyle ind in
let body= mkCase(case_info, pred, casee, branches) in
let id=pf_get_new_id (id_of_string "t") gls in
mkLambda(Name id,intype,body)
(* generate an adhoc tactic following the proof tree *)
let rec proof_tac axioms=function
Ax id->exact_check (mkVar id)
| SymAx id->tclTHEN symmetry (exact_check (mkVar id))
| Refl t->reflexivity
| Trans (p1,p2)->let t=(make_term (snd (type_proof axioms p1))) in
(tclTHENS (transitivity t)
[(proof_tac axioms p1);(proof_tac axioms p2)])
| Congr (p1,p2)->
fun gls->
let (f1,f2)=(type_proof axioms p1)
and (x1,x2)=(type_proof axioms p2) in
let tf1=make_term f1 and tx1=make_term x1
and tf2=make_term f2 and tx2=make_term x2 in
let typf=pf_type_of gls tf1 and typx=pf_type_of gls tx1
and typfx=pf_type_of gls (mkApp(tf1,[|tx1|])) in
let id=pf_get_new_id (id_of_string "f") gls in
let appx1=mkLambda(Name id,typf,mkApp(mkRel 1,[|tx1|])) in
let lemma1=
mkApp(Lazy.force f_equal_theo,[|typf;typfx;appx1;tf1;tf2|])
and lemma2=
mkApp(Lazy.force f_equal_theo,[|typx;typfx;tf2;tx1;tx2|]) in
(tclTHENS (transitivity (mkApp(tf2,[|tx1|])))
[tclTHEN (apply lemma1) (proof_tac axioms p1);
tclFIRST
[tclTHEN (apply lemma2) (proof_tac axioms p2);
reflexivity;
fun gls ->
errorlabstrm "Congruence"
(Pp.str
"I don't know how to handle dependent equality")]]
gls)
| Inject (prf,cstr,nargs,argind) as gprf->
(fun gls ->
let ti,tj=type_proof axioms prf in
let ai,aj=type_proof axioms gprf in
let cti=make_term ti in
let ctj=make_term tj in
let cai=make_term ai in
let intype=pf_type_of gls cti in
let outtype=pf_type_of gls cai in
let special=mkRel (1+nargs-argind) in
let default=make_term ai in
let proj=build_projection intype outtype cstr special default gls in
let injt=
mkApp (Lazy.force f_equal_theo,[|intype;outtype;proj;cti;ctj|]) in
tclTHEN (apply injt) (proof_tac axioms prf) gls)
(* wrap everything *)
let cc_tactic gls=
Library.check_required_library ["Coq";"Init";"Logic"];
let prb=make_prb gls in
match (cc_proof prb) with
Prove (p,axioms)-> proof_tac axioms p gls
| Refute (cstr,t1,t2,p,axioms) ->
let tt1=make_term t1 and tt2=make_term t2 in
let intype=pf_type_of gls tt1 in
let concl=pf_concl gls in
let outsort=mkType (new_univ ()) in
let xid=pf_get_new_id (id_of_string "X") gls in
let tid=pf_get_new_id (id_of_string "t") gls in
let identity=
mkLambda(Name xid,outsort,mkLambda(Name tid,mkRel 1,mkRel 1)) in
let trivial=pf_type_of gls identity in
let outtype=mkType (new_univ ()) in
let pred=mkLambda(Name xid,outtype,mkRel 1) in
let hid=pf_get_new_id (id_of_string "Heq") gls in
let proj=build_projection intype outtype cstr trivial concl gls in
let injt=
mkApp (Lazy.force f_equal_theo,
[|intype;outtype;proj;tt1;tt2;mkVar hid|]) in
let endt=
mkApp (Lazy.force eq_rect_theo,
[|outtype;trivial;pred;identity;concl;injt|]) in
let neweq=
mkApp(constr_of_reference Coqlib.glob_eq,[|intype;tt1;tt2|]) in
tclTHENS (true_cut (Name hid) neweq)
[proof_tac axioms p;exact_check endt] gls
(* Tactic registration *)
TACTIC EXTEND CC
[ "Congruence" ] -> [ cc_tactic ]
END
|
