1 (* Copyright (C) 2002, HELM Team.
3 * This file is part of HELM, an Hypertextual, Electronic
4 * Library of Mathematics, developed at the Computer Science
5 * Department, University of Bologna, Italy.
7 * HELM is free software; you can redistribute it and/or
8 * modify it under the terms of the GNU General Public License
9 * as published by the Free Software Foundation; either version 2
10 * of the License, or (at your option) any later version.
12 * HELM is distributed in the hope that it will be useful,
13 * but WITHOUT ANY WARRANTY; without even the implied warranty of
14 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
15 * GNU General Public License for more details.
17 * You should have received a copy of the GNU General Public License
18 * along with HELM; if not, write to the Free Software
19 * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
22 * For details, see the HELM World-Wide-Web page,
23 * http://cs.unibo.it/helm/.
28 let debug_print = fun _ -> ()
30 (* term ha tipo t1=t2; funziona solo se t1 e t2 hanno in testa costruttori
33 let discriminate_tac ~term =
35 let module U = UriManager in
36 let module P = PrimitiveTactics in
37 let module T = Tacticals in
39 match LibraryObjects.true_URI () with
41 | None -> raise (ProofEngineTypes.Fail (lazy "You need to register the default \"true\" definition first. Please use the \"default\" command")) in
43 match LibraryObjects.false_URI () with
45 | None -> raise (ProofEngineTypes.Fail (lazy "You need to register the default \"false\" definition first. Please use the \"default\" command")) in
46 let fail msg = raise (ProofEngineTypes.Fail (lazy ("Discriminate: " ^ msg))) in
47 let find_discriminating_consno t1 t2 =
50 | C.MutConstruct _, C.MutConstruct _ when t1 = t2 -> None
51 | C.Appl ((C.MutConstruct _ as constr1) :: args1),
52 C.Appl ((C.MutConstruct _ as constr2) :: args2)
53 when constr1 = constr2 ->
54 let rec aux_list l1 l2 =
57 | hd1 :: tl1, hd2 :: tl2 ->
58 (match aux hd1 hd2 with
59 | None -> aux_list tl1 tl2
60 | Some _ as res -> res)
61 | _ -> (* same constructor applied to a different number of args *)
65 | ((C.MutConstruct (_,_,consno1,subst1)),
66 (C.MutConstruct (_,_,consno2,subst2)))
67 | ((C.MutConstruct (_,_,consno1,subst1)),
68 (C.Appl ((C.MutConstruct (_,_,consno2,subst2)) :: _)))
69 | ((C.Appl ((C.MutConstruct (_,_,consno1,subst1)) :: _)),
70 (C.MutConstruct (_,_,consno2,subst2)))
71 | ((C.Appl ((C.MutConstruct (_,_,consno1,subst1)) :: _)),
72 (C.Appl ((C.MutConstruct (_,_,consno2,subst2)) :: _)))
73 when (consno1 <> consno2) || (subst1 <> subst2) ->
75 | _ -> fail "not a discriminable equality"
79 let mk_branches_and_outtype turi typeno consno context args =
80 (* a list of "True" except for the element in position consno which
82 match fst (CicEnvironment.get_obj CicUniv.empty_ugraph turi) with
83 | C.InductiveDefinition (ind_type_list,_,paramsno,_) ->
84 let _,_,rty,constructor_list = List.nth ind_type_list typeno in
85 let false_constr_id,_ = List.nth constructor_list (consno - 1) in
89 (* dubbio: e' corretto ridurre in questo context ??? *)
90 let red_ty = CicReduction.whd context cty in
93 | C.Prod (_,_,target) when (k <= paramsno) ->
94 CicSubstitution.subst (List.nth args (k-1))
96 | C.Prod (binder,source,target) when (k > paramsno) ->
97 C.Lambda (binder, source, (aux target (k+1)))
99 if (id = false_constr_id)
100 then (C.MutInd(false_URI,0,[]))
101 else (C.MutInd(true_URI,0,[]))
103 (CicSubstitution.lift 1 (aux red_ty 1)))
107 let rec mk_lambdas rev_left_args =
109 0, args, C.Prod (_,so,ta) ->
111 (C.Name (incr seed; "x" ^ string_of_int !seed),
113 mk_lambdas rev_left_args (0,args,ta))
114 | 0, args, C.Sort _ ->
118 | n -> C.Rel n :: mk_rels (n - 1) in
119 let argsno = List.length args in
122 (if argsno + List.length rev_left_args > 0 then
124 (C.MutInd (turi, typeno, []) ::
126 (CicSubstitution.lift (argsno + 1))
127 (List.rev rev_left_args)) @
130 C.MutInd (turi,typeno,[])),
132 | 0, _, _ -> assert false (* seriously screwed up *)
133 | n, he::tl, C.Prod (_,_,ta) ->
134 mk_lambdas (he::rev_left_args)(n-1,tl,CicSubstitution.subst he ta)
136 assert false (* we should probably reduce in some context *)
138 mk_lambdas [] (paramsno, args, rty)
143 let discriminate'_tac ~term status =
144 let (proof, goal) = status in
145 let _,metasenv,_,_, _ = proof in
146 let _,context,_ = CicUtil.lookup_meta goal metasenv in
148 CicTypeChecker.type_of_aux' metasenv context term CicUniv.empty_ugraph
151 | C.Appl [(C.MutInd (equri, 0, [])) ; tty ; t1 ; t2]
152 when LibraryObjects.is_eq_URI equri ->
153 let turi,typeno,exp_named_subst,args =
155 | (C.MutInd (turi,typeno,exp_named_subst)) ->
156 turi,typeno,exp_named_subst,[]
157 | (C.Appl (C.MutInd (turi,typeno,exp_named_subst)::args)) ->
158 turi,typeno,exp_named_subst,args
159 | _ -> fail "not a discriminable equality"
162 match find_discriminating_consno t1 t2 with
163 | Some consno -> consno
164 | None -> fail "discriminating terms are structurally equal"
166 let branches,outtype =
167 mk_branches_and_outtype turi typeno consno context args
169 ProofEngineTypes.apply_tactic
171 ~start:(EliminationTactics.elim_type_tac (C.MutInd (false_URI, 0, [])))
175 (ReductionTactics.change_tac
176 ~pattern:(ProofEngineTypes.conclusion_pattern None)
179 C.Lambda ( C.Name "x", tty,
180 C.MutCase (turi, typeno, outtype, (C.Rel 1), branches));
186 (EqualityTactics.rewrite_simpl_tac
187 ~direction:`RightToLeft
188 ~pattern:(ProofEngineTypes.conclusion_pattern None)
191 (IntroductionTactics.constructor_tac ~n:1)))) status
192 | _ -> fail "not an equality"
194 ProofEngineTypes.mk_tactic (discriminate'_tac ~term)
198 ProofEngineTypes.Fail (lazy "Injection: not a projectable equality");;
200 ProofEngineTypes.Fail (lazy "Injection: not an equality");;
201 let exn_nothingtodo =
202 ProofEngineTypes.Fail (lazy "Nothing to do");;
203 let exn_discrnonind =
204 ProofEngineTypes.Fail (lazy "Discriminate: object is not an Inductive Definition: it's imposible");;
205 let exn_injwronggoal =
206 ProofEngineTypes.Fail (lazy "Injection: goal after cut is not correct");;
208 ProofEngineTypes.Fail (lazy "Injection: not an equality over elements of an inductive type");;
210 let rec injection_tac ~first_time ~term ~liftno ~continuation =
211 let module C = Cic in
212 let module CR = CicReduction in
213 let module U = UriManager in
214 let module P = PrimitiveTactics in
215 let module T = Tacticals in
216 let module PST = ProofEngineStructuralRules in
217 let module PET = ProofEngineTypes in
218 let prerr_endline s = prerr_endline (String.make liftno ' ' ^ s) in
219 let are_convertible hd1 hd2 metasenv context =
220 fst (CR.are_convertible ~metasenv context hd1 hd2 CicUniv.empty_ugraph)
222 let injection_tac ~term status =
223 let (proof, goal) = status in
224 let _,metasenv,_,_, _ = proof in
225 let _,context,_ = CicUtil.lookup_meta goal metasenv in
226 let term = CicSubstitution.lift liftno term in
228 CicTypeChecker.type_of_aux' metasenv context term CicUniv.empty_ugraph
230 prerr_endline ("injection su: " ^ CicPp.ppterm termty);
233 | C.Appl [(C.MutInd (equri, 0, [])) ; tty ; t1 ; t2]
234 when LibraryObjects.is_eq_URI equri -> begin
235 match (CicReduction.whd ~delta:true context tty) with
236 | C.MutInd (turi,typeno,ens)
237 | C.Appl (C.MutInd (turi,typeno,ens)::_) -> begin
239 | C.MutConstruct (uri1,typeno1,consno1,ens1),
240 C.MutConstruct (uri2,typeno2,consno2,ens2)
241 when (uri1 = uri2) && (typeno1 = typeno2) &&
242 (consno1 = consno2) && (ens1 = ens2) ->
243 if first_time then raise exn_nothingtodo
244 else continuation ~liftno
245 | C.Appl ((C.MutConstruct (uri1,typeno1,consno1,ens1))::applist1),
246 C.Appl ((C.MutConstruct (uri2,typeno2,consno2,ens2))::applist2)
247 when (uri1 = uri2) && (typeno1 = typeno2) &&
248 (consno1 = consno2) && (ens1 = ens2) ->
249 let rec traverse_list i l1 l2 =
251 | [],[] when first_time -> continuation
255 match List.nth context (n-1) with
256 | Some (C.Name id,_) ->
258 T.then_ ~start:(PST.clear ~hyps:[id])
259 ~continuation:(continuation ~liftno)
264 | hd1::tl1,hd2::tl2 ->
265 if are_convertible hd1 hd2 metasenv context then
266 traverse_list (i+1) tl1 tl2
268 injection1_tac ~i ~term
269 ~continuation:(traverse_list (i+1) tl1 tl2)
271 (* i 2 termini hanno in testa lo stesso costruttore,
272 * ma applicato a un numero diverso di termini *)
274 traverse_list 1 applist1 applist2 ~liftno
275 | C.MutConstruct (uri1,typeno1,consno1,ens1),
276 C.MutConstruct (uri2,typeno2,consno2,ens2)
277 | C.MutConstruct (uri1,typeno1,consno1,ens1),
278 C.Appl ((C.MutConstruct (uri2,typeno2,consno2,ens2))::_)
279 | C.Appl ((C.MutConstruct (uri1,typeno1,consno1,ens1))::_),
280 C.MutConstruct (uri2,typeno2,consno2,ens2)
281 | C.Appl ((C.MutConstruct (uri1,typeno1,consno1,ens1))::_),
282 C.Appl ((C.MutConstruct (uri2,typeno2,consno2,ens2))::_)
283 when (consno1 <> consno2) || (ens1 <> ens2) ->
284 discriminate_tac ~term
285 | _ when not first_time -> continuation ~liftno
286 | _ (* when first_time *) ->
290 match List.nth context (i-1) with
291 | Some (Cic.Name s, Cic.Def _) -> s
292 | Some (Cic.Name s, Cic.Decl _) -> s
296 ~start:(ReductionTactics.simpl_tac
297 ~pattern:(None,[name,Cic.Implicit (Some `Hole)],None))
298 ~continuation:(injection_tac ~first_time:false ~term ~liftno
300 | _ -> raise exn_nonproj
302 | _ when not first_time -> continuation ~liftno
303 | _ (* when first_time *) -> raise exn_nonproj
305 | _ -> raise exn_nonproj
307 PET.apply_tactic tac status
309 PET.mk_tactic (injection_tac ~term)
311 and injection1_tac ~term ~i ~liftno ~continuation =
312 let module C = Cic in
313 let module CTC = CicTypeChecker in
314 let module CU = CicUniv in
315 let module S = CicSubstitution in
316 let module U = UriManager in
317 let module P = PrimitiveTactics in
318 let module PET = ProofEngineTypes in
319 let module T = Tacticals in
320 let prerr_endline s = prerr_endline (String.make liftno ' ' ^ s) in
321 let give_name seed = function
322 | C.Name _ as name -> name
323 | C.Anonymous -> C.Name (incr seed; "y" ^ string_of_int !seed)
325 let rec mk_rels = function | 0 -> [] | n -> C.Rel n :: (mk_rels (n - 1)) in
326 let injection1_tac ~term ~i status =
327 let (proof, goal) = status in
328 (* precondizione: t1 e t2 hanno in testa lo stesso costruttore ma
329 * differiscono (o potrebbero differire?) nell'i-esimo parametro
331 let term = CicSubstitution.lift liftno term in
332 let _,metasenv,_,_, _ = proof in
333 let _,context,_ = CicUtil.lookup_meta goal metasenv in
335 CicTypeChecker.type_of_aux' metasenv context term CicUniv.empty_ugraph
337 prerr_endline ("injection1 su : " ^ CicPp.ppterm termty);
338 match termty with (* an equality *)
339 | C.Appl [(C.MutInd (equri, 0, [])) ; tty ; t1 ; t2]
340 when LibraryObjects.is_eq_URI equri ->
341 let turi,typeno,ens,params =
342 match tty with (* some inductive type *)
343 | C.MutInd (turi,typeno,ens) -> turi,typeno,ens,[]
344 | C.Appl (C.MutInd (turi,typeno,ens)::params) -> turi,typeno,ens,params
345 | _ -> raise exn_noneqind
347 let t1',t2',consno = (* sono i due sottotermini che differiscono *)
349 | C.Appl ((C.MutConstruct (uri1,typeno1,consno1,ens1))::applist1),
350 C.Appl ((C.MutConstruct (uri2,typeno2,consno2,ens2))::applist2)
351 when (uri1 = uri2) && (typeno1 = typeno2) &&
352 (consno1 = consno2) && (ens1 = ens2) ->
353 (* controllo ridondante *)
354 List.nth applist1 (i-1),List.nth applist2 (i-1),consno2
357 let tty',_ = CTC.type_of_aux' metasenv context t1' CU.empty_ugraph in
358 let patterns,outtype =
359 match fst (CicEnvironment.get_obj CicUniv.empty_ugraph turi) with
360 | C.InductiveDefinition (ind_type_list,_,paramsno,_)->
361 let left_params, right_params = HExtlib.split_nth paramsno params in
362 let _,_,_,constructor_list = List.nth ind_type_list typeno in
363 let i_constr_id,_ = List.nth constructor_list (consno - 1) in
367 (function (id,cty) ->
368 let reduced_cty = CicReduction.whd context cty in
369 let rec aux k = function
370 | C.Prod (_,_,tgt) when k <= paramsno ->
371 let left = List.nth left_params (k-1) in
372 aux (k+1) (CicSubstitution.subst left tgt)
373 | C.Prod (binder,source,target) when k > paramsno ->
374 let binder' = give_name seed binder in
375 C.Lambda (binder',source,(aux (k+1) target))
377 let nr_param_constr = k - paramsno in
378 if id = i_constr_id then C.Rel (k - i)
379 else S.lift nr_param_constr t1'
380 (* + 1 per liftare anche il lambda aggiunto
381 * esternamente al case *)
382 in aux 1 reduced_cty)
387 let rec to_lambdas te head =
388 match CicReduction.whd context te with
389 | C.Prod (binder,so,ta) ->
390 let binder' = give_name seed binder in
391 C.Lambda (binder',so,to_lambdas ta head)
394 let rec skip_prods params te =
395 match params, CicReduction.whd context te with
397 | left::tl, C.Prod (_,_,ta) ->
398 skip_prods tl (CicSubstitution.subst left ta)
399 | _, _ -> assert false
402 match CicSubstitution.lift (paramsno(* + 1*)) tty with
403 | C.MutInd _ as tty' -> tty'
405 let keep,abstract = HExtlib.split_nth (paramsno +1) l in
406 C.Appl (keep@mk_rels (List.length abstract))
409 match ind_type_list with
412 to_lambdas (skip_prods left_params ty)
414 (C.Name "x", abstracted_tty, S.lift 1 tty'))
417 | _ -> raise exn_discrnonind
419 let cutted = C.Appl [C.MutInd (equri,0,[]) ; tty' ; t1' ; t2'] in
420 prerr_endline ("CUT: " ^ CicPp.ppterm cutted);
422 (T.thens ~start: (P.cut_tac cutted)
424 [injection_tac ~first_time:false ~liftno:0 ~term:(C.Rel 1)
426 (fun ~liftno:x -> continuation ~liftno:(liftno+1+x))
427 (* here I need to lift all the continuations by 1;
428 since I am setting back liftno to 0, I actually
429 need to lift all the continuations by liftno + 1 *)
431 ~start:(PET.mk_tactic
433 prerr_endline "riempo il cut";
434 let (proof, goal) = status in
435 let _,metasenv,_,_, _ = proof in
436 let _,context,gty =CicUtil.lookup_meta goal metasenv in
437 let gty = Unshare.unshare gty in
440 | (C.Appl (C.MutInd (_,_,_)::_::t::_)) -> t
441 | _ -> raise exn_injwronggoal
445 C.Lambda (C.Name "x", tty,
446 C.MutCase (turi,typeno,outtype,C.Rel 1,patterns))
450 ("metto questo: " ^ CicPp.ppterm changed);
452 ("al posto di questo: " ^ CicPp.ppterm new_t1');
454 ("nel goal: " ^ CicPp.ppterm gty);
456 ("nel contesto:\n" ^ CicPp.ppcontext context);
459 (ReductionTactics.change_tac
461 Some (ProofEngineHelpers.pattern_of
462 ~term:gty [new_t1']))
463 (fun _ m u -> changed,m,u))
465 in prerr_endline "fine";rc
470 (EqualityTactics.rewrite_simpl_tac
471 ~direction:`LeftToRight
472 ~pattern:(PET.conclusion_pattern None)
474 ~continuation:EqualityTactics.reflexivity_tac)
477 | _ -> raise exn_noneq
479 PET.mk_tactic (injection1_tac ~term ~i)
482 (* destruct performs either injection or discriminate *)
483 (* equivalent to Coq's "analyze equality" *)
486 ~first_time:true ~liftno:0 ~continuation:(fun ~liftno -> Tacticals.id_tac)