summaryrefslogtreecommitdiff
path: root/plugins/cc/cctac.ml
blob: ca1a90854a8cbecda5f61c32db29283a400db766 (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
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
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
(************************************************************************)
(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
(*   \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: cctac.ml 13409 2010-09-13 07:53:13Z soubiran $ *)

(* 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 Typing
open Ccalgo
open Tacinterp
open Ccproof
open Pp
open Util
open Format

let constant dir s = lazy (Coqlib.gen_constant "CC" dir s)

let _f_equal = constant ["Init";"Logic"] "f_equal"

let _eq_rect = constant ["Init";"Logic"] "eq_rect"

let _refl_equal = constant ["Init";"Logic"] "refl_equal"

let _sym_eq = constant ["Init";"Logic"] "sym_eq"

let _trans_eq = constant ["Init";"Logic"] "trans_eq"

let _eq = constant ["Init";"Logic"] "eq"

let _False = constant ["Init";"Logic"] "False"

let whd env=
  let infos=Closure.create_clos_infos Closure.betaiotazeta env in
    (fun t -> Closure.whd_val infos (Closure.inject t))

let whd_delta env=
   let infos=Closure.create_clos_infos Closure.betadeltaiota env in
    (fun t -> Closure.whd_val infos (Closure.inject t))

(* decompose member of equality in an applicative format *)

let sf_of env sigma c = family_of_sort (sort_of env sigma c)

let rec decompose_term env sigma t=
    match kind_of_term (whd env t) with
      App (f,args)->
	let tf=decompose_term env sigma f in
	let targs=Array.map (decompose_term env sigma) args in
	  Array.fold_left (fun s t->Appli (s,t)) tf targs
    | Prod (_,a,_b) when not (dependent (mkRel 1) _b) ->
	let b = pop _b in
	let sort_b = sf_of env sigma b in
	let sort_a = sf_of env sigma a in
	Appli(Appli(Product (sort_a,sort_b) ,
		    decompose_term env sigma a),
	      decompose_term env sigma b)
    | Construct c->
	let (mind,i_ind),i_con = c in 
	let canon_mind = mind_of_kn (canonical_mind mind) in
	let canon_ind = canon_mind,i_ind in
	let (oib,_)=Global.lookup_inductive (canon_ind) in
	let nargs=mis_constructor_nargs_env env (canon_ind,i_con) in
	  Constructor {ci_constr= (canon_ind,i_con);
		       ci_arity=nargs;
		       ci_nhyps=nargs-oib.mind_nparams}
    | Ind c -> 
	let mind,i_ind = c in 
	let canon_mind = mind_of_kn (canonical_mind mind) in
	let canon_ind = canon_mind,i_ind in  (Symb (mkInd canon_ind))
    | Const c -> 
	let canon_const = constant_of_kn (canonical_con c) in 
	  (Symb (mkConst canon_const))
    | _ ->if closed0 t then (Symb t) else raise Not_found

(* decompose equality in members and type *)

let atom_of_constr env sigma term =
  let wh =  (whd_delta env term) in
  let kot = kind_of_term wh in
    match kot with
      App (f,args)->
	  if eq_constr f (Lazy.force _eq) && (Array.length args)=3
	  then `Eq (args.(0),
		   decompose_term env sigma args.(1),
		   decompose_term env sigma args.(2))
	  else `Other (decompose_term env sigma term)
    | _ -> `Other (decompose_term env sigma term)

let rec pattern_of_constr env sigma c =
  match kind_of_term (whd env c) with
      App (f,args)->
	let pf = decompose_term env sigma f in
	let pargs,lrels = List.split
	  (array_map_to_list (pattern_of_constr env sigma) args) in
	  PApp (pf,List.rev pargs),
	List.fold_left Intset.union Intset.empty lrels
    | Prod (_,a,_b) when not (dependent (mkRel 1) _b) ->
	let b =pop _b in
	let pa,sa = pattern_of_constr env sigma a in
	let pb,sb = pattern_of_constr env sigma b in
	let sort_b = sf_of env sigma b in
	let sort_a = sf_of env sigma a in
	  PApp(Product (sort_a,sort_b),
	       [pa;pb]),(Intset.union sa sb)
    | Rel i -> PVar i,Intset.singleton i
    | _ ->
	let pf = decompose_term env sigma c in
	  PApp (pf,[]),Intset.empty

let non_trivial = function
    PVar _ -> false
  | _ -> true

let patterns_of_constr env sigma nrels term=
  let f,args=
    try destApp (whd_delta env term) with _ -> raise Not_found in
	if eq_constr f (Lazy.force _eq) && (Array.length args)=3
	then
	  let patt1,rels1 = pattern_of_constr env sigma args.(1)
	  and patt2,rels2 = pattern_of_constr env sigma args.(2) in
	  let valid1 =
	    if Intset.cardinal rels1 <> nrels then Creates_variables
	    else if non_trivial patt1 then Normal
	    else Trivial args.(0)
	  and valid2 =
	    if Intset.cardinal rels2 <> nrels then Creates_variables
	    else if non_trivial patt2 then Normal
	    else Trivial args.(0) in
	    if valid1 <> Creates_variables
	      || valid2 <> Creates_variables  then
	      nrels,valid1,patt1,valid2,patt2
	    else raise Not_found
	else raise Not_found

let rec quantified_atom_of_constr env sigma nrels term =
  match kind_of_term (whd_delta env term) with
      Prod (id,atom,ff) -> 
	if eq_constr ff (Lazy.force _False) then
	  let patts=patterns_of_constr env sigma nrels atom in
	      `Nrule patts
	else 
	  quantified_atom_of_constr (Environ.push_rel (id,None,atom) env) sigma (succ nrels) ff
    | _ ->  
	let patts=patterns_of_constr env sigma nrels term in
	    `Rule patts

let litteral_of_constr env sigma term=
  match kind_of_term (whd_delta env term) with
    | Prod (id,atom,ff) -> 
	if eq_constr ff (Lazy.force _False) then
	  match (atom_of_constr env sigma atom) with
	      `Eq(t,a,b) -> `Neq(t,a,b)
	    | `Other(p) -> `Nother(p)
	else
	  begin
	    try 
	      quantified_atom_of_constr (Environ.push_rel (id,None,atom) env) sigma 1 ff  
	    with Not_found ->
	      `Other (decompose_term env sigma term)
	  end
    | _ ->
	atom_of_constr env sigma term


(* store all equalities from the context *)

let rec make_prb gls depth additionnal_terms =
  let env=pf_env gls in
  let sigma=sig_sig gls in
  let state = empty depth gls in
  let pos_hyps = ref [] in
  let neg_hyps =ref [] in
    List.iter
      (fun c ->
	 let t = decompose_term env sigma c in
	   ignore (add_term state t)) additionnal_terms;
    List.iter
      (fun (id,_,e) ->
	 begin
	   let cid=mkVar id in
	   match litteral_of_constr env sigma e with
	       `Eq (t,a,b) -> add_equality state cid a b
	     | `Neq (t,a,b) -> add_disequality state (Hyp cid) a b
	     | `Other ph ->
		 List.iter
		   (fun (cidn,nh) ->
		      add_disequality state (HeqnH (cid,cidn)) ph nh)
		   !neg_hyps;
		 pos_hyps:=(cid,ph):: !pos_hyps
	     | `Nother nh ->
		 List.iter
		   (fun (cidp,ph) ->
		      add_disequality state (HeqnH (cidp,cid)) ph nh)
		   !pos_hyps;
		 neg_hyps:=(cid,nh):: !neg_hyps
	     | `Rule patts -> add_quant state id true patts
	     | `Nrule patts -> add_quant state id false patts
	 end) (Environ.named_context_of_val gls.it.evar_hyps);
    begin
      match atom_of_constr env sigma gls.it.evar_concl with
	  `Eq (t,a,b) -> add_disequality state Goal a b
	|	`Other g ->
		  List.iter
	      (fun (idp,ph) ->
		 add_disequality state (HeqG idp) ph g) !pos_hyps
    end;
    state

(* indhyps builds the array of arrays of constructor hyps for (ind largs) *)

let build_projection intype outtype (cstr:constructor) special default gls=
  let env=pf_env gls in
  let (h,argv) =
    try destApp intype with
	Invalid_argument _ -> (intype,[||])  in
  let ind=destInd h in
  let types=Inductiveops.arities_of_constructors env ind in
  let lp=Array.length types in
  let ci=pred (snd cstr) in
  let branch i=
    let ti=Term.prod_appvect types.(i) argv in
    let rc=fst (decompose_prod_assum ti) in
    let head=
      if i=ci then special else default in
      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 case_info=make_case_info (pf_env gls) ind RegularStyle 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 _M =mkMeta

let rec proof_tac p gls =
  match p.p_rule with
      Ax c -> exact_check c gls
    | SymAx c ->
	let l=constr_of_term p.p_lhs and
	    r=constr_of_term p.p_rhs in
        let typ = refresh_universes (pf_type_of gls l) in
	  exact_check
	    (mkApp(Lazy.force _sym_eq,[|typ;r;l;c|])) gls
    | Refl t ->
	let lr = constr_of_term t in
	let typ = refresh_universes (pf_type_of gls lr) in
	exact_check
	   (mkApp(Lazy.force _refl_equal,[|typ;constr_of_term t|])) gls
    | Trans (p1,p2)->
	let t1 = constr_of_term p1.p_lhs and
	    t2 = constr_of_term p1.p_rhs and
	    t3 = constr_of_term p2.p_rhs in
	let typ = refresh_universes (pf_type_of gls t2) in
	let prf =
	  mkApp(Lazy.force _trans_eq,[|typ;t1;t2;t3;_M 1;_M 2|]) in
	  tclTHENS (refine prf) [(proof_tac p1);(proof_tac p2)] gls
    | Congr (p1,p2)->
	let tf1=constr_of_term p1.p_lhs
	and tx1=constr_of_term p2.p_lhs
	and tf2=constr_of_term p1.p_rhs
	and tx2=constr_of_term p2.p_rhs in
	let typf = refresh_universes (pf_type_of gls tf1) in
	let typx = refresh_universes (pf_type_of gls tx1) in
	let typfx = refresh_universes (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,
		[|typf;typfx;appx1;tf1;tf2;_M 1|]) in
	let lemma2=
	  mkApp(Lazy.force _f_equal,
		[|typx;typfx;tf2;tx1;tx2;_M 1|]) in
	let prf =
	  mkApp(Lazy.force _trans_eq,
		[|typfx;
		  mkApp(tf1,[|tx1|]);
		  mkApp(tf2,[|tx1|]);
		  mkApp(tf2,[|tx2|]);_M 2;_M 3|]) in
	  tclTHENS (refine prf)
	    [tclTHEN (refine lemma1) (proof_tac p1);
  	     tclFIRST
	       [tclTHEN (refine lemma2) (proof_tac p2);
		reflexivity;
		fun gls ->
		  errorlabstrm  "Congruence"
		    (Pp.str
		       "I don't know how to handle dependent equality")]] gls
  | Inject (prf,cstr,nargs,argind) ->
	 let ti=constr_of_term prf.p_lhs in
	 let tj=constr_of_term prf.p_rhs in
	 let default=constr_of_term p.p_lhs in
	 let intype=refresh_universes (pf_type_of gls ti) in
	 let outtype=refresh_universes (pf_type_of gls default) in
	 let special=mkRel (1+nargs-argind) in
	 let proj=build_projection intype outtype cstr special default gls in
	 let injt=
	   mkApp (Lazy.force _f_equal,[|intype;outtype;proj;ti;tj;_M 1|]) in
	   tclTHEN (refine injt) (proof_tac prf) gls

let refute_tac c t1 t2 p gls =
  let tt1=constr_of_term t1 and tt2=constr_of_term t2 in
  let intype=refresh_universes (pf_type_of gls tt1) in
  let neweq=
    mkApp(Lazy.force _eq,
	  [|intype;tt1;tt2|]) in
  let hid=pf_get_new_id (id_of_string "Heq") gls in
  let false_t=mkApp (c,[|mkVar hid|]) in
    tclTHENS (assert_tac (Name hid) neweq)
      [proof_tac p; simplest_elim false_t] gls

let convert_to_goal_tac c t1 t2 p gls =
  let tt1=constr_of_term t1 and tt2=constr_of_term t2 in
  let sort=refresh_universes (pf_type_of gls tt2) in
  let neweq=mkApp(Lazy.force _eq,[|sort;tt1;tt2|]) in
  let e=pf_get_new_id (id_of_string "e") gls in
  let x=pf_get_new_id (id_of_string "X") gls in
  let identity=mkLambda (Name x,sort,mkRel 1) in
  let endt=mkApp (Lazy.force _eq_rect,
		  [|sort;tt1;identity;c;tt2;mkVar e|]) in
    tclTHENS (assert_tac (Name e) neweq)
      [proof_tac p;exact_check endt] gls

let convert_to_hyp_tac c1 t1 c2 t2 p gls =
  let tt2=constr_of_term t2 in
  let h=pf_get_new_id (id_of_string "H") gls in
  let false_t=mkApp (c2,[|mkVar h|]) in
    tclTHENS (assert_tac (Name h) tt2)
      [convert_to_goal_tac c1 t1 t2 p;
       simplest_elim false_t] gls

let discriminate_tac cstr p gls =
  let t1=constr_of_term p.p_lhs and t2=constr_of_term p.p_rhs in
  let intype=refresh_universes (pf_type_of gls t1) 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,
		  [|intype;outtype;proj;t1;t2;mkVar hid|]) in
  let endt=mkApp (Lazy.force _eq_rect,
		  [|outtype;trivial;pred;identity;concl;injt|]) in
  let neweq=mkApp(Lazy.force _eq,[|intype;t1;t2|]) in
    tclTHENS (assert_tac (Name hid) neweq)
      [proof_tac p;exact_check endt] gls

(* wrap everything *)

let build_term_to_complete uf meta pac =
  let cinfo = get_constructor_info uf pac.cnode in
  let real_args = List.map (fun i -> constr_of_term (term uf i)) pac.args in
  let dummy_args = List.rev (list_tabulate meta pac.arity) in
  let all_args = List.rev_append real_args dummy_args in
    applistc (mkConstruct cinfo.ci_constr) all_args

let cc_tactic depth additionnal_terms gls=
  Coqlib.check_required_library ["Coq";"Init";"Logic"];
  let _ = debug Pp.msgnl (Pp.str "Reading subgoal ...") in
  let state = make_prb gls depth additionnal_terms in
  let _ = debug Pp.msgnl (Pp.str "Problem built, solving ...") in
  let sol = execute true state in
  let _ = debug Pp.msgnl (Pp.str "Computation completed.") in
  let uf=forest state in
    match sol with
	None -> tclFAIL 0 (str "congruence failed") gls
      | Some reason ->
	  debug Pp.msgnl (Pp.str "Goal solved, generating proof ...");
	  match reason with
	      Discrimination (i,ipac,j,jpac) ->
		let p=build_proof uf (`Discr (i,ipac,j,jpac)) in
		let cstr=(get_constructor_info uf ipac.cnode).ci_constr in
		  discriminate_tac cstr p gls
	    | Incomplete ->
		let metacnt = ref 0 in
		let newmeta _ = incr metacnt; _M !metacnt in
		let terms_to_complete =
		  List.map
		    (build_term_to_complete uf newmeta)
		    (epsilons uf) in
		  Pp.msgnl
		    (Pp.str "Goal is solvable by congruence but \
 some arguments are missing.");
		  Pp.msgnl
		    (Pp.str "  Try " ++
		     hov 8
		       begin
			 str "\"congruence with (" ++
			 prlist_with_sep
			   (fun () -> str ")" ++ pr_spc () ++ str "(")
			   (print_constr_env (pf_env gls))
			   terms_to_complete ++
			 str ")\","
		       end);
		  Pp.msgnl
		    (Pp.str "  replacing metavariables by arbitrary terms.");
		  tclFAIL 0 (str "Incomplete") gls
	    | Contradiction dis ->
		let p=build_proof uf (`Prove (dis.lhs,dis.rhs)) in
		let ta=term uf dis.lhs and tb=term uf dis.rhs in
		  match dis.rule with
		      Goal -> proof_tac p gls
		    | Hyp id -> refute_tac id ta tb p gls
		    | HeqG id ->
			convert_to_goal_tac id ta tb p gls
		    | HeqnH (ida,idb) ->
			convert_to_hyp_tac ida ta idb tb p gls


let cc_fail gls =
  errorlabstrm  "Congruence" (Pp.str "congruence failed.")

let congruence_tac depth l =
  tclORELSE
    (tclTHEN (tclREPEAT introf) (cc_tactic depth l))
    cc_fail

(* Beware: reflexivity = constructor 1 = apply refl_equal
   might be slow now, let's rather do something equivalent
   to a "simple apply refl_equal" *)

let simple_reflexivity () = apply (Lazy.force _refl_equal)

(* The [f_equal] tactic.

   It mimics the use of lemmas [f_equal], [f_equal2], etc.
   This isn't particularly related with congruence, apart from
   the fact that congruence is called internally.
*)

let f_equal gl =
  let cut_eq c1 c2 =
    let ty = refresh_universes (pf_type_of gl c1) in
    tclTHENTRY
      (Tactics.cut (mkApp (Lazy.force _eq, [|ty; c1; c2|])))
      (simple_reflexivity ())
  in
  try match kind_of_term (pf_concl gl) with
    | App (r,[|_;t;t'|]) when eq_constr r (Lazy.force _eq) ->
	begin match kind_of_term t, kind_of_term t' with
	  | App (f,v), App (f',v') when Array.length v = Array.length v' ->
	      let rec cuts i =
		if i < 0 then tclTRY (congruence_tac 1000 [])
		else tclTHENFIRST (cut_eq v.(i) v'.(i)) (cuts (i-1))
	      in cuts (Array.length v - 1) gl
	  | _ -> tclIDTAC gl
	end
    | _ -> tclIDTAC gl
  with Type_errors.TypeError _ -> tclIDTAC gl