From 6b649aba925b6f7462da07599fe67ebb12a3460e Mon Sep 17 00:00:00 2001 From: Samuel Mimram Date: Wed, 28 Jul 2004 21:54:47 +0000 Subject: Imported Upstream version 8.0pl1 --- tactics/auto.ml | 939 +++++++++++++++++++ tactics/auto.mli | 197 ++++ tactics/autorewrite.ml | 105 +++ tactics/autorewrite.mli | 22 + tactics/btermdn.ml | 51 + tactics/btermdn.mli | 28 + tactics/contradiction.ml | 88 ++ tactics/contradiction.mli | 19 + tactics/dhyp.ml | 373 ++++++++ tactics/dhyp.mli | 32 + tactics/dn.ml | 80 ++ tactics/dn.mli | 40 + tactics/doc.tex | 11 + tactics/eauto.ml4 | 448 +++++++++ tactics/eauto.mli | 25 + tactics/elim.ml | 195 ++++ tactics/elim.mli | 38 + tactics/eqdecide.ml4 | 188 ++++ tactics/equality.ml | 1213 ++++++++++++++++++++++++ tactics/equality.mli | 83 ++ tactics/extraargs.ml4 | 31 + tactics/extraargs.mli | 18 + tactics/extratactics.ml4 | 329 +++++++ tactics/extratactics.mli | 20 + tactics/hiddentac.ml | 103 ++ tactics/hiddentac.mli | 108 +++ tactics/hipattern.ml | 366 ++++++++ tactics/hipattern.mli | 129 +++ tactics/inv.ml | 564 +++++++++++ tactics/inv.mli | 44 + tactics/leminv.ml | 318 +++++++ tactics/leminv.mli | 19 + tactics/nbtermdn.ml | 83 ++ tactics/nbtermdn.mli | 37 + tactics/refine.ml | 346 +++++++ tactics/refine.mli | 14 + tactics/setoid_replace.ml | 686 ++++++++++++++ tactics/setoid_replace.mli | 27 + tactics/tacinterp.ml | 2236 ++++++++++++++++++++++++++++++++++++++++++++ tactics/tacinterp.mli | 126 +++ tactics/tacticals.ml | 457 +++++++++ tactics/tacticals.mli | 162 ++++ tactics/tactics.ml | 1922 +++++++++++++++++++++++++++++++++++++ tactics/tactics.mli | 245 +++++ tactics/tauto.ml4 | 209 +++++ tactics/termdn.ml | 84 ++ tactics/termdn.mli | 51 + 47 files changed, 12909 insertions(+) create mode 100644 tactics/auto.ml create mode 100644 tactics/auto.mli create mode 100644 tactics/autorewrite.ml create mode 100644 tactics/autorewrite.mli create mode 100644 tactics/btermdn.ml create mode 100644 tactics/btermdn.mli create mode 100644 tactics/contradiction.ml create mode 100644 tactics/contradiction.mli create mode 100644 tactics/dhyp.ml create mode 100644 tactics/dhyp.mli create mode 100644 tactics/dn.ml create mode 100644 tactics/dn.mli create mode 100644 tactics/doc.tex create mode 100644 tactics/eauto.ml4 create mode 100644 tactics/eauto.mli create mode 100644 tactics/elim.ml create mode 100644 tactics/elim.mli create mode 100644 tactics/eqdecide.ml4 create mode 100644 tactics/equality.ml create mode 100644 tactics/equality.mli create mode 100644 tactics/extraargs.ml4 create mode 100644 tactics/extraargs.mli create mode 100644 tactics/extratactics.ml4 create mode 100644 tactics/extratactics.mli create mode 100644 tactics/hiddentac.ml create mode 100644 tactics/hiddentac.mli create mode 100644 tactics/hipattern.ml create mode 100644 tactics/hipattern.mli create mode 100644 tactics/inv.ml create mode 100644 tactics/inv.mli create mode 100644 tactics/leminv.ml create mode 100644 tactics/leminv.mli create mode 100644 tactics/nbtermdn.ml create mode 100644 tactics/nbtermdn.mli create mode 100644 tactics/refine.ml create mode 100644 tactics/refine.mli create mode 100644 tactics/setoid_replace.ml create mode 100644 tactics/setoid_replace.mli create mode 100644 tactics/tacinterp.ml create mode 100644 tactics/tacinterp.mli create mode 100644 tactics/tacticals.ml create mode 100644 tactics/tacticals.mli create mode 100644 tactics/tactics.ml create mode 100644 tactics/tactics.mli create mode 100644 tactics/tauto.ml4 create mode 100644 tactics/termdn.ml create mode 100644 tactics/termdn.mli (limited to 'tactics') diff --git a/tactics/auto.ml b/tactics/auto.ml new file mode 100644 index 00000000..d087420a --- /dev/null +++ b/tactics/auto.ml @@ -0,0 +1,939 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* [v] + | h::tl -> if pri_order v h then v::h::tl else h::(insrec tl) + in + insrec l + +(* Nov 98 -- Papageno *) +(* Les Hints sont ré-organisés en plusieurs databases. + + La table impérative "searchtable", de type "hint_db_table", + associe une database (hint_db) à chaque nom. + + Une hint_db est une table d'association fonctionelle constr -> search_entry + Le constr correspond à la constante de tête de la conclusion. + + Une search_entry est un triplet comprenant : + - la liste des tactiques qui n'ont pas de pattern associé + - la liste des tactiques qui ont un pattern + - un discrimination net borné (Btermdn.t) constitué de tous les + patterns de la seconde liste de tactiques *) + +type stored_data = pri_auto_tactic + +type search_entry = stored_data list * stored_data list * stored_data Btermdn.t + +let empty_se = ([],[],Btermdn.create ()) + +let add_tac t (l,l',dn) = + match t.pat with + None -> (insert t l, l', dn) + | Some pat -> (l, insert t l', Btermdn.add dn (pat,t)) + + +let lookup_tacs (hdc,c) (l,l',dn) = + let l' = List.map snd (Btermdn.lookup dn c) in + let sl' = Sort.list pri_order l' in + Sort.merge pri_order l sl' + + +module Constr_map = Map.Make(struct + type t = constr_label + let compare = Pervasives.compare + end) + +module Hint_db = struct + + type t = search_entry Constr_map.t + + let empty = Constr_map.empty + + let find key db = + try Constr_map.find key db + with Not_found -> empty_se + + let map_all k db = + let (l,l',_) = find k db in + Sort.merge pri_order l l' + + let map_auto (k,c) db = + lookup_tacs (k,c) (find k db) + + let add_one (k,v) db = + let oval = find k db in + Constr_map.add k (add_tac v oval) db + + let add_list l db = List.fold_right add_one l db + + let iter f db = Constr_map.iter (fun k (l,l',_) -> f k (l@l')) db + +end + +type frozen_hint_db_table = Hint_db.t Stringmap.t + +type hint_db_table = Hint_db.t Stringmap.t ref + +type hint_db_name = string + +let searchtable = (ref Stringmap.empty : hint_db_table) + +let searchtable_map name = + Stringmap.find name !searchtable +let searchtable_add (name,db) = + searchtable := Stringmap.add name db !searchtable + +(**************************************************************************) +(* Definition of the summary *) +(**************************************************************************) + +let init () = searchtable := Stringmap.empty +let freeze () = !searchtable +let unfreeze fs = searchtable := fs + +let _ = Summary.declare_summary "search" + { Summary.freeze_function = freeze; + Summary.unfreeze_function = unfreeze; + Summary.init_function = init; + Summary.survive_module = false; + Summary.survive_section = false } + + +(**************************************************************************) +(* Auxiliary functions to prepare AUTOHINT objects *) +(**************************************************************************) + +let rec nb_hyp c = match kind_of_term c with + | Prod(_,_,c2) -> if noccurn 1 c2 then 1+(nb_hyp c2) else nb_hyp c2 + | _ -> 0 + +(* adding and removing tactics in the search table *) + +let try_head_pattern c = + try head_pattern_bound c + with BoundPattern -> error "Bound head variable" + +let make_exact_entry name (c,cty) = + let cty = strip_outer_cast cty in + match kind_of_term cty with + | Prod (_,_,_) -> + failwith "make_exact_entry" + | _ -> + (head_of_constr_reference (List.hd (head_constr cty)), + { hname=name; pri=0; pat=None; code=Give_exact c }) + +let make_apply_entry env sigma (eapply,verbose) name (c,cty) = + let cty = hnf_constr env sigma cty in + match kind_of_term cty with + | Prod _ -> + let ce = mk_clenv_from () (c,cty) in + let c' = (clenv_template_type ce).rebus in + let pat = Pattern.pattern_of_constr c' in + let hd = (try head_pattern_bound pat + with BoundPattern -> failwith "make_apply_entry") in + let nmiss = List.length (clenv_missing ce) + in + if eapply & (nmiss <> 0) then begin + if verbose then + warn (str "the hint: EApply " ++ prterm c ++ + str " will only be used by EAuto"); + (hd, + { hname = name; + pri = nb_hyp cty + nmiss; + pat = Some pat; + code = ERes_pf(c,ce) }) + end else + (hd, + { hname = name; + pri = nb_hyp cty; + pat = Some pat; + code = Res_pf(c,ce) }) + | _ -> failwith "make_apply_entry" + +(* eap is (e,v) with e=true if eapply and v=true if verbose + c is a constr + cty is the type of constr *) + +let make_resolves env sigma name eap (c,cty) = + let ents = + map_succeed + (fun f -> f name (c,cty)) + [make_exact_entry; make_apply_entry env sigma eap] + in + if ents = [] then + errorlabstrm "Hint" (prterm c ++ spc () ++ str "cannot be used as a hint"); + ents + +(* used to add an hypothesis to the local hint database *) +let make_resolve_hyp env sigma (hname,_,htyp) = + try + [make_apply_entry env sigma (true, false) hname + (mkVar hname, htyp)] + with + | Failure _ -> [] + | e when Logic.catchable_exception e -> anomaly "make_resolve_hyp" + +(* REM : in most cases hintname = id *) +let make_unfold (hintname, ref) = + (Pattern.label_of_ref ref, + { hname = hintname; + pri = 4; + pat = None; + code = Unfold_nth ref }) + +let make_extern name pri pat tacast = + let hdconstr = try_head_pattern pat in + (hdconstr, + { hname = name; + pri=pri; + pat = Some pat; + code= Extern tacast }) + +let make_trivial env sigma (name,c) = + let t = hnf_constr env sigma (type_of env sigma c) in + let hd = head_of_constr_reference (List.hd (head_constr t)) in + let ce = mk_clenv_from () (c,t) in + (hd, { hname = name; + pri=1; + pat = Some (Pattern.pattern_of_constr (clenv_template_type ce).rebus); + code=Res_pf_THEN_trivial_fail(c,ce) }) + +open Vernacexpr + +(**************************************************************************) +(* declaration of the AUTOHINT library object *) +(**************************************************************************) + +(* If the database does not exist, it is created *) +(* TODO: should a warning be printed in this case ?? *) +let add_hint dbname hintlist = + try + let db = searchtable_map dbname in + let db' = Hint_db.add_list hintlist db in + searchtable_add (dbname,db') + with Not_found -> + let db = Hint_db.add_list hintlist Hint_db.empty in + searchtable_add (dbname,db) + +let cache_autohint (_,(local,name,hintlist)) = add_hint name hintlist + +(* let recalc_hints hintlist = + let env = Global.env() and sigma = Evd.empty in + let recalc_hint ((_,data) as hint) = + match data.code with + | Res_pf (c,_) -> + let c' = Term.subst_mps subst c in + if c==c' then hint else + make_apply_entry env sigma (false,false) + data.hname (c', type_of env sigma c') + | ERes_pf (c,_) -> + let c' = Term.subst_mps subst c in + if c==c' then hint else + make_apply_entry env sigma (true,false) + data.hname (c', type_of env sigma c') + | Give_exact c -> + let c' = Term.subst_mps subst c in + if c==c' then hint else + make_exact_entry data.hname (c',type_of env sigma c') + | Res_pf_THEN_trivial_fail (c,_) -> + let c' = Term.subst_mps subst c in + if c==c' then hint else + make_trivial env sigma (data.hname,c') + | Unfold_nth ref -> + let ref' = subst_global subst ref in + if ref==ref' then hint else + make_unfold (data.hname,ref') + | Extern _ -> + anomaly "Extern hints cannot be substituted!!!" + in + list_smartmap recalc_hint hintlist +*) + +let forward_subst_tactic = + ref (fun _ -> failwith "subst_tactic is not installed for Auto") + +let set_extern_subst_tactic f = forward_subst_tactic := f + +let subst_autohint (_,subst,(local,name,hintlist as obj)) = + let trans_clenv clenv = Clenv.subst_clenv (fun _ a -> a) subst clenv in + let trans_data data code = + { data with + pat = option_smartmap (subst_pattern subst) data.pat ; + code = code ; + } + in + let subst_hint (lab,data as hint) = + let lab' = subst_label subst lab in + let data' = match data.code with + | Res_pf (c, clenv) -> + let c' = Term.subst_mps subst c in + if c==c' then data else + trans_data data (Res_pf (c', trans_clenv clenv)) + | ERes_pf (c, clenv) -> + let c' = Term.subst_mps subst c in + if c==c' then data else + trans_data data (ERes_pf (c', trans_clenv clenv)) + | Give_exact c -> + let c' = Term.subst_mps subst c in + if c==c' then data else + trans_data data (Give_exact c') + | Res_pf_THEN_trivial_fail (c, clenv) -> + let c' = Term.subst_mps subst c in + if c==c' then data else + let code' = Res_pf_THEN_trivial_fail (c', trans_clenv clenv) in + trans_data data code' + | Unfold_nth ref -> + let ref' = subst_global subst ref in + if ref==ref' then data else + trans_data data (Unfold_nth ref') + | Extern tac -> + let tac' = !forward_subst_tactic subst tac in + if tac==tac' then data else + trans_data data (Extern tac') + in + if lab' == lab && data' == data then hint else + (lab',data') + in + let hintlist' = list_smartmap subst_hint hintlist in + if hintlist' == hintlist then obj else + (local,name,hintlist') + +let classify_autohint (_,((local,name,hintlist) as obj)) = + if local or hintlist = [] then Dispose else Substitute obj + +let export_autohint ((local,name,hintlist) as obj) = + if local then None else Some obj + +let (inAutoHint,outAutoHint) = + declare_object {(default_object "AUTOHINT") with + cache_function = cache_autohint; + load_function = (fun _ -> cache_autohint); + subst_function = subst_autohint; + classify_function = classify_autohint; + export_function = export_autohint } + + +(**************************************************************************) +(* The "Hint" vernacular command *) +(**************************************************************************) +let add_resolves env sigma clist local dbnames = + List.iter + (fun dbname -> + Lib.add_anonymous_leaf + (inAutoHint + (local,dbname, + List.flatten + (List.map + (fun (name,c) -> + let ty = type_of env sigma c in + let verbose = Options.is_verbose() in + make_resolves env sigma name (true,verbose) (c,ty)) clist + ) + ))) + dbnames + + +let add_unfolds l local dbnames = + List.iter + (fun dbname -> Lib.add_anonymous_leaf + (inAutoHint (local,dbname, List.map make_unfold l))) + dbnames + + +let add_extern name pri (patmetas,pat) tacast local dbname = + (* We check that all metas that appear in tacast have at least + one occurence in the left pattern pat *) +(* TODO + let tacmetas = Coqast.collect_metas tacast in +*) + let tacmetas = [] in + match (list_subtract tacmetas patmetas) with + | i::_ -> + errorlabstrm "add_extern" + (str "The meta-variable ?" ++ pr_patvar i ++ str" is not bound") + | [] -> + Lib.add_anonymous_leaf + (inAutoHint(local,dbname, [make_extern name pri pat tacast])) + +let add_externs name pri pat tacast local dbnames = + List.iter (add_extern name pri pat tacast local) dbnames + +let add_trivials env sigma l local dbnames = + List.iter + (fun dbname -> + Lib.add_anonymous_leaf ( + inAutoHint(local,dbname, List.map (make_trivial env sigma) l))) + dbnames + +let forward_intern_tac = + ref (fun _ -> failwith "intern_tac is not installed for Auto") + +let set_extern_intern_tac f = forward_intern_tac := f + +let add_hints local dbnames0 h = + let dbnames = if dbnames0 = [] then ["core"] else dbnames0 in + match h with + | HintsResolve lhints -> + let env = Global.env() and sigma = Evd.empty in + let f (n,c) = + let c = Constrintern.interp_constr sigma env c in + let n = match n with + | None -> (*id_of_global (reference_of_constr c)*) + id_of_string "" + | Some n -> n in + (n,c) in + add_resolves env sigma (List.map f lhints) local dbnames + | HintsImmediate lhints -> + let env = Global.env() and sigma = Evd.empty in + let f (n,c) = + let c = Constrintern.interp_constr sigma env c in + let n = match n with + | None -> (*id_of_global (reference_of_constr c)*) + id_of_string "" + | Some n -> n in + (n,c) in + add_trivials env sigma (List.map f lhints) local dbnames + | HintsUnfold lhints -> + let f (n,locqid) = + let r = Nametab.global locqid in + let n = match n with + | None -> id_of_global r + | Some n -> n in + (n,r) in + add_unfolds (List.map f lhints) local dbnames + | HintsConstructors (hintname, lqid) -> + let add_one qid = + let env = Global.env() and sigma = Evd.empty in + let isp = global_inductive qid in + let consnames = (snd (Global.lookup_inductive isp)).mind_consnames in + let lcons = list_tabulate + (fun i -> mkConstruct (isp,i+1)) (Array.length consnames) in + let lcons = List.map2 + (fun id c -> (id,c)) (Array.to_list consnames) lcons in + add_resolves env sigma lcons local dbnames in + List.iter add_one lqid + | HintsExtern (hintname, pri, patcom, tacexp) -> + let hintname = match hintname with + Some h -> h + | _ -> id_of_string "" in + let pat = Constrintern.interp_constrpattern Evd.empty (Global.env()) patcom in + let tacexp = !forward_intern_tac (fst pat) tacexp in + add_externs hintname pri pat tacexp local dbnames + | HintsDestruct(na,pri,loc,pat,code) -> + if dbnames0<>[] then + warn (str"Database selection not implemented for destruct hints"); + Dhyp.add_destructor_hint local na loc pat pri code + +(**************************************************************************) +(* Functions for printing the hints *) +(**************************************************************************) + +let fmt_autotactic = function + | Res_pf (c,clenv) -> (str"Apply " ++ prterm c) + | ERes_pf (c,clenv) -> (str"EApply " ++ prterm c) + | Give_exact c -> (str"Exact " ++ prterm c) + | Res_pf_THEN_trivial_fail (c,clenv) -> + (str"Apply " ++ prterm c ++ str" ; Trivial") + | Unfold_nth c -> (str"Unfold " ++ pr_global c) + | Extern tac -> (str "Extern " ++ Pptactic.pr_glob_tactic tac) + +let fmt_hint v = + (fmt_autotactic v.code ++ str"(" ++ int v.pri ++ str")" ++ spc ()) + +let fmt_hint_list hintlist = + (str " " ++ hov 0 (prlist fmt_hint hintlist) ++ fnl ()) + +let fmt_hints_db (name,db,hintlist) = + (str "In the database " ++ str name ++ str ":" ++ + if hintlist = [] then (str " nothing" ++ fnl ()) + else (fnl () ++ fmt_hint_list hintlist)) + +(* Print all hints associated to head c in any database *) +let fmt_hint_list_for_head c = + let dbs = stringmap_to_list !searchtable in + let valid_dbs = + map_succeed + (fun (name,db) -> (name,db,Hint_db.map_all c db)) + dbs + in + if valid_dbs = [] then + (str "No hint declared for :" ++ pr_ref_label c) + else + hov 0 + (str"For " ++ pr_ref_label c ++ str" -> " ++ fnl () ++ + hov 0 (prlist fmt_hints_db valid_dbs)) + +let fmt_hint_ref ref = fmt_hint_list_for_head (label_of_ref ref) + +(* Print all hints associated to head id in any database *) +let print_hint_ref ref = ppnl(fmt_hint_ref ref) + +let fmt_hint_term cl = + try + let (hdc,args) = match head_constr_bound cl [] with + | hdc::args -> (hdc,args) + | [] -> assert false + in + let hd = head_of_constr_reference hdc in + let dbs = stringmap_to_list !searchtable in + let valid_dbs = + if occur_existential cl then + map_succeed + (fun (name, db) -> (name, db, Hint_db.map_all hd db)) + dbs + else + map_succeed + (fun (name, db) -> + (name, db, Hint_db.map_auto (hd,applist(hdc,args)) db)) + dbs + in + if valid_dbs = [] then + (str "No hint applicable for current goal") + else + (str "Applicable Hints :" ++ fnl () ++ + hov 0 (prlist fmt_hints_db valid_dbs)) + with Bound | Match_failure _ | Failure _ -> + (str "No hint applicable for current goal") + +let print_hint_term cl = ppnl (fmt_hint_term cl) + +(* print all hints that apply to the concl of the current goal *) +let print_applicable_hint () = + let pts = get_pftreestate () in + let gl = nth_goal_of_pftreestate 1 pts in + print_hint_term (pf_concl gl) + +(* displays the whole hint database db *) +let print_hint_db db = + Hint_db.iter + (fun head hintlist -> + msg (hov 0 + (str "For " ++ pr_ref_label head ++ str " -> " ++ + fmt_hint_list hintlist))) + db + +let print_hint_db_by_name dbname = + try + let db = searchtable_map dbname in print_hint_db db + with Not_found -> + error (dbname^" : No such Hint database") + +(* displays all the hints of all databases *) +let print_searchtable () = + Stringmap.iter + (fun name db -> + msg (str "In the database " ++ str name ++ fnl ()); + print_hint_db db) + !searchtable + +(**************************************************************************) +(* Automatic tactics *) +(**************************************************************************) + +(**************************************************************************) +(* tactics with a trace mechanism for automatic search *) +(**************************************************************************) + +let priority l = List.map snd (List.filter (fun (pr,_) -> pr = 0) l) + + +(* Try unification with the precompiled clause, then use registered Apply *) + +let unify_resolve (c,clenv) gls = + let (wc,kONT) = startWalk gls in + let clenv' = connect_clenv wc clenv in + let _ = clenv_unique_resolver false clenv' gls in + h_simplest_apply c gls + +(* builds a hint database from a constr signature *) +(* typically used with (lid, ltyp) = pf_hyps_types *) + +let make_local_hint_db g = + let sign = pf_hyps g in + let hintlist = list_map_append (make_resolve_hyp (pf_env g) (project g)) sign + in Hint_db.add_list hintlist Hint_db.empty + + +(* Serait-ce possible de compiler d'abord la tactique puis de faire la + substitution sans passer par bdize dont l'objectif est de préparer un + terme pour l'affichage ? (HH) *) + +(* Si on enlève le dernier argument (gl) conclPattern est calculé une +fois pour toutes : en particulier si Pattern.somatch produit une UserError +Ce qui fait que si la conclusion ne matche pas le pattern, Auto échoue, même +si après Intros la conclusion matche le pattern. +*) + +(* conclPattern doit échouer avec error car il est rattraper par tclFIRST *) + +let forward_interp_tactic = + ref (fun _ -> failwith "interp_tactic is not installed for Auto") + +let set_extern_interp f = forward_interp_tactic := f + +let conclPattern concl pat tac gl = + let constr_bindings = + try matches pat concl + with PatternMatchingFailure -> error "conclPattern" in + !forward_interp_tactic constr_bindings tac gl + +(**************************************************************************) +(* The Trivial tactic *) +(**************************************************************************) + +(* local_db is a Hint database containing the hypotheses of current goal *) +(* Papageno : cette fonction a été pas mal simplifiée depuis que la base + de Hint impérative a été remplacée par plusieurs bases fonctionnelles *) + +let rec trivial_fail_db db_list local_db gl = + let intro_tac = + tclTHEN intro + (fun g'-> + let hintl = make_resolve_hyp (pf_env g') (project g') (pf_last_hyp g') + in trivial_fail_db db_list (Hint_db.add_list hintl local_db) g') + in + tclFIRST + (assumption::intro_tac:: + (List.map tclCOMPLETE + (trivial_resolve db_list local_db (pf_concl gl)))) gl + +and my_find_search db_list local_db hdc concl = + let tacl = + if occur_existential concl then + list_map_append (fun db -> Hint_db.map_all hdc db) (local_db::db_list) + else + list_map_append (fun db -> Hint_db.map_auto (hdc,concl) db) + (local_db::db_list) + in + List.map + (fun ({pri=b; pat=p; code=t} as patac) -> + (b, + match t with + | Res_pf (term,cl) -> unify_resolve (term,cl) + | ERes_pf (_,c) -> (fun gl -> error "eres_pf") + | Give_exact c -> exact_check c + | Res_pf_THEN_trivial_fail (term,cl) -> + tclTHEN + (unify_resolve (term,cl)) + (trivial_fail_db db_list local_db) + | Unfold_nth c -> unfold_constr c + | Extern tacast -> + conclPattern concl (out_some p) tacast)) + tacl + +and trivial_resolve db_list local_db cl = + try + let hdconstr = List.hd (head_constr_bound cl []) in + priority + (my_find_search db_list local_db (head_of_constr_reference hdconstr) cl) + with Bound | Not_found -> + [] + +let trivial dbnames gl = + let db_list = + List.map + (fun x -> + try + searchtable_map x + with Not_found -> + error ("Trivial: "^x^": No such Hint database")) + ("core"::dbnames) + in + tclTRY (trivial_fail_db db_list (make_local_hint_db gl)) gl + +let full_trivial gl = + let dbnames = stringmap_dom !searchtable in + let dbnames = list_subtract dbnames ["v62"] in + let db_list = List.map (fun x -> searchtable_map x) dbnames in + tclTRY (trivial_fail_db db_list (make_local_hint_db gl)) gl + +let gen_trivial = function + | None -> full_trivial + | Some l -> trivial l + +let h_trivial l = Refiner.abstract_tactic (TacTrivial l) (gen_trivial l) + +(**************************************************************************) +(* The classical Auto tactic *) +(**************************************************************************) + +let possible_resolve db_list local_db cl = + try + let hdconstr = List.hd (head_constr_bound cl []) in + List.map snd + (my_find_search db_list local_db (head_of_constr_reference hdconstr) cl) + with Bound | Not_found -> + [] + +let decomp_unary_term c gls = + let typc = pf_type_of gls c in + let hd = List.hd (head_constr typc) in + if Hipattern.is_conjunction hd then + simplest_case c gls + else + errorlabstrm "Auto.decomp_unary_term" (str "not a unary type") + +let decomp_empty_term c gls = + let typc = pf_type_of gls c in + let (hd,_) = decompose_app typc in + if Hipattern.is_empty_type hd then + simplest_case c gls + else + errorlabstrm "Auto.decomp_empty_term" (str "not an empty type") + + +(* decomp is an natural number giving an indication on decomposition + of conjunction in hypotheses, 0 corresponds to no decomposition *) +(* n is the max depth of search *) +(* local_db contains the local Hypotheses *) + +let rec search_gen decomp n db_list local_db extra_sign goal = + if n=0 then error "BOUND 2"; + let decomp_tacs = match decomp with + | 0 -> [] + | p -> + (tclTRY_sign decomp_empty_term extra_sign) + :: + (List.map + (fun id -> tclTHENSEQ + [decomp_unary_term (mkVar id); + clear [id]; + search_gen decomp p db_list local_db []]) + (pf_ids_of_hyps goal)) + in + let intro_tac = + tclTHEN intro + (fun g' -> + let (hid,_,htyp as d) = pf_last_hyp g' in + let hintl = + try + [make_apply_entry (pf_env g') (project g') + (true,false) + hid (mkVar hid, htyp)] + with Failure _ -> [] + in + search_gen decomp n db_list (Hint_db.add_list hintl local_db) [d] g') + in + let rec_tacs = + List.map + (fun ntac -> + tclTHEN ntac + (search_gen decomp (n-1) db_list local_db empty_named_context)) + (possible_resolve db_list local_db (pf_concl goal)) + in + tclFIRST (assumption::(decomp_tacs@(intro_tac::rec_tacs))) goal + + +let search = search_gen 0 + +let default_search_depth = ref 5 + +let auto n dbnames gl = + let db_list = + List.map + (fun x -> + try + searchtable_map x + with Not_found -> + error ("Auto: "^x^": No such Hint database")) + ("core"::dbnames) + in + let hyps = pf_hyps gl in + tclTRY (search n db_list (make_local_hint_db gl) hyps) gl + +let default_auto = auto !default_search_depth [] + +let full_auto n gl = + let dbnames = stringmap_dom !searchtable in + let dbnames = list_subtract dbnames ["v62"] in + let db_list = List.map (fun x -> searchtable_map x) dbnames in + let hyps = pf_hyps gl in + tclTRY (search n db_list (make_local_hint_db gl) hyps) gl + +let default_full_auto gl = full_auto !default_search_depth gl + +let gen_auto n dbnames = + let n = match n with None -> !default_search_depth | Some n -> n in + match dbnames with + | None -> full_auto n + | Some l -> auto n l + +let h_auto n l = Refiner.abstract_tactic (TacAuto (n,l)) (gen_auto n l) + +(**************************************************************************) +(* The "destructing Auto" from Eduardo *) +(**************************************************************************) + +(* Depth of search after decomposition of hypothesis, by default + one look for an immediate solution *) +(* Papageno : de toute façon un paramète > 1 est traité comme 1 pour + l'instant *) +let default_search_decomp = ref 1 + +let destruct_auto des_opt n gl = + let hyps = pf_hyps gl in + search_gen des_opt n [searchtable_map "core"] + (make_local_hint_db gl) hyps gl + +let dautomatic des_opt n = tclTRY (destruct_auto des_opt n) + +let default_dauto = dautomatic !default_search_decomp !default_search_depth + +let dauto = function + | None, None -> default_dauto + | Some n, None -> dautomatic !default_search_decomp n + | Some n, Some p -> dautomatic p n + | None, Some p -> dautomatic p !default_search_depth + +let h_dauto (n,p) = Refiner.abstract_tactic (TacDAuto (n,p)) (dauto (n,p)) + +(***************************************) +(*** A new formulation of Auto *********) +(***************************************) + +type autoArguments = + | UsingTDB + | Destructing + +let keepAfter tac1 tac2 = + (tclTHEN tac1 + (function g -> tac2 [pf_last_hyp g] g)) + +let compileAutoArg contac = function + | Destructing -> + (function g -> + let ctx = pf_hyps g in + tclFIRST + (List.map + (fun (id,_,typ) -> + let cl = snd (decompose_prod typ) in + if Hipattern.is_conjunction cl + then + tclTHENSEQ [simplest_elim (mkVar id); clear [id]; contac] + else + tclFAIL 0 ((string_of_id id)^"is not a conjunction")) + ctx) g) + | UsingTDB -> + (tclTHEN + (Tacticals.tryAllClauses + (function + | Some (id,_,_) -> Dhyp.h_destructHyp false id + | None -> Dhyp.h_destructConcl)) + contac) + +let compileAutoArgList contac = List.map (compileAutoArg contac) + +let rec super_search n db_list local_db argl goal = + if n = 0 then error "BOUND 2"; + tclFIRST + (assumption + :: + (tclTHEN intro + (fun g -> + let (hid,_,htyp) = pf_last_hyp g in + let hintl = + make_resolves (pf_env g) (project g) + hid (true,false) (mkVar hid, htyp) in + super_search n db_list (Hint_db.add_list hintl local_db) + argl g)) + :: + ((List.map + (fun ntac -> + tclTHEN ntac + (super_search (n-1) db_list local_db argl)) + (possible_resolve db_list local_db (pf_concl goal))) + @ + (compileAutoArgList + (super_search (n-1) db_list local_db argl) argl))) goal + +let search_superauto n to_add argl g = + let sigma = + List.fold_right + (fun (id,c) -> add_named_decl (id, None, pf_type_of g c)) + to_add empty_named_context in + let db0 = list_map_append (make_resolve_hyp (pf_env g) (project g)) sigma in + let db = Hint_db.add_list db0 (make_local_hint_db g) in + super_search n [Stringmap.find "core" !searchtable] db argl g + +let superauto n to_add argl = + tclTRY (tclCOMPLETE (search_superauto n to_add argl)) + +let default_superauto g = superauto !default_search_depth [] [] g + +let interp_to_add gl locqid = + let r = Nametab.global locqid in + let id = id_of_global r in + (next_ident_away id (pf_ids_of_hyps gl), constr_of_reference r) + +let gen_superauto nopt l a b gl = + let n = match nopt with Some n -> n | None -> !default_search_depth in + let al = (if a then [Destructing] else [])@(if b then [UsingTDB] else []) in + superauto n (List.map (interp_to_add gl) l) al gl + +let h_superauto no l a b = + Refiner.abstract_tactic (TacSuperAuto (no,l,a,b)) (gen_superauto no l a b) + diff --git a/tactics/auto.mli b/tactics/auto.mli new file mode 100644 index 00000000..ef6b85ea --- /dev/null +++ b/tactics/auto.mli @@ -0,0 +1,197 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* t -> search_entry + val map_all : constr_label -> t -> pri_auto_tactic list + val map_auto : constr_label * constr -> t -> pri_auto_tactic list + val add_one : constr_label * pri_auto_tactic -> t -> t + val add_list : (constr_label * pri_auto_tactic) list -> t -> t + val iter : (constr_label -> stored_data list -> unit) -> t -> unit + end + +type frozen_hint_db_table = Hint_db.t Stringmap.t + +type hint_db_table = Hint_db.t Stringmap.t ref + +type hint_db_name = string + +val add_hints : locality_flag -> hint_db_name list -> hints -> unit + +val print_searchtable : unit -> unit + +val print_applicable_hint : unit -> unit + +val print_hint_ref : global_reference -> unit + +val print_hint_db_by_name : hint_db_name -> unit + +val searchtable : hint_db_table + +(* [make_exact_entry hint_name (c, ctyp)]. + [hint_name] is the name of then hint; + [c] is the term given as an exact proof to solve the goal; + [ctyp] is the type of [hc]. *) + +val make_exact_entry : + identifier -> constr * constr -> constr_label * pri_auto_tactic + +(* [make_apply_entry (eapply,verbose) name (c,cty)]. + [eapply] is true if this hint will be used only with EApply; + [name] is the name of then hint; + [c] is the term given as an exact proof to solve the goal; + [cty] is the type of [hc]. *) + +val make_apply_entry : + env -> evar_map -> bool * bool -> identifier -> constr * constr + -> constr_label * pri_auto_tactic + +(* A constr which is Hint'ed will be: + (1) used as an Exact, if it does not start with a product + (2) used as an Apply, if its HNF starts with a product, and + has no missing arguments. + (3) used as an EApply, if its HNF starts with a product, and + has missing arguments. *) + +val make_resolves : + env -> evar_map -> identifier -> bool * bool -> constr * constr -> + (constr_label * pri_auto_tactic) list + +(* [make_resolve_hyp hname htyp]. + used to add an hypothesis to the local hint database; + Never raises an User_exception; + If the hyp cannot be used as a Hint, the empty list is returned. *) + +val make_resolve_hyp : + env -> evar_map -> named_declaration -> + (constr_label * pri_auto_tactic) list + +(* [make_extern name pri pattern tactic_expr] *) + +val make_extern : + identifier -> int -> constr_pattern -> Tacexpr.glob_tactic_expr + -> constr_label * pri_auto_tactic + +val set_extern_interp : + (patvar_map -> Tacexpr.glob_tactic_expr -> tactic) -> unit + +val set_extern_intern_tac : + (patvar list -> Tacexpr.raw_tactic_expr -> Tacexpr.glob_tactic_expr) + -> unit + +val set_extern_subst_tactic : + (Names.substitution -> Tacexpr.glob_tactic_expr -> Tacexpr.glob_tactic_expr) + -> unit + +(* Create a Hint database from the pairs (name, constr). + Useful to take the current goal hypotheses as hints *) + +val make_local_hint_db : goal sigma -> Hint_db.t + +val priority : (int * 'a) list -> 'a list + +val default_search_depth : int ref + +(* Try unification with the precompiled clause, then use registered Apply *) +val unify_resolve : (constr * unit clausenv) -> tactic + +(* [ConclPattern concl pat tacast]: + if the term concl matches the pattern pat, (in sense of + [Pattern.somatches], then replace [?1] [?2] metavars in tacast by the + right values to build a tactic *) + +val conclPattern : constr -> constr_pattern -> Tacexpr.glob_tactic_expr -> tactic + +(* The Auto tactic *) + +val auto : int -> hint_db_name list -> tactic + +(* auto with default search depth and with the hint database "core" *) +val default_auto : tactic + +(* auto with all hint databases except the "v62" compatibility database *) +val full_auto : int -> tactic + +(* auto with default search depth and with all hint databases + except the "v62" compatibility database *) +val default_full_auto : tactic + +(* The generic form of auto (second arg [None] means all bases) *) +val gen_auto : int option -> hint_db_name list option -> tactic + +(* The hidden version of auto *) +val h_auto : int option -> hint_db_name list option -> tactic + +(* Trivial *) +val trivial : hint_db_name list -> tactic +val gen_trivial : hint_db_name list option -> tactic +val full_trivial : tactic +val h_trivial : hint_db_name list option -> tactic + +val fmt_autotactic : auto_tactic -> Pp.std_ppcmds + +(*s The following is not yet up to date -- Papageno. *) + +(* DAuto *) +val dauto : int option * int option -> tactic +val default_search_decomp : int ref +val default_dauto : tactic + +val h_dauto : int option * int option -> tactic +(* SuperAuto *) + +type autoArguments = + | UsingTDB + | Destructing + +(* +val superauto : int -> (identifier * constr) list -> autoArguments list -> tactic +*) + +val h_superauto : int option -> reference list -> bool -> bool -> tactic diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml new file mode 100644 index 00000000..7c134b89 --- /dev/null +++ b/tactics/autorewrite.ml @@ -0,0 +1,105 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* + errorlabstrm "AutoRewrite" + (str ("Rewriting base "^(bas)^" does not exist")) + in + tclREPEAT_MAIN (tclPROGRESS (List.fold_left (fun tac (csr,dir,tc) -> + tclTHEN tac + (tclREPEAT_MAIN + (tclTHENSFIRSTn (general_rewrite dir csr) [|tac_main|] tc))) + tclIDTAC lrul)) + +(* The AutoRewrite tactic *) +let autorewrite tac_main lbas = + tclREPEAT_MAIN (tclPROGRESS + (List.fold_left (fun tac bas -> + tclTHEN tac (one_base tac_main bas)) tclIDTAC lbas)) + +(* Functions necessary to the library object declaration *) +let cache_hintrewrite (_,(rbase,lrl)) = + let l = List.rev_map (fun (c,b,t) -> (c,b,Tacinterp.eval_tactic t)) lrl in + let l = + try + List.rev_append l (Stringmap.find rbase !rewtab) + with + | Not_found -> List.rev l + in + rewtab:=Stringmap.add rbase l !rewtab + +let export_hintrewrite x = Some x + +let subst_hintrewrite (_,subst,(rbase,list as node)) = + let subst_first (cst,b,t as pair) = + let cst' = Term.subst_mps subst cst in + let t' = Tacinterp.subst_tactic subst t in + if cst == cst' & t == t' then pair else + (cst',b,t) + in + let list' = list_smartmap subst_first list in + if list' == list then node else + (rbase,list') + +let classify_hintrewrite (_,x) = Libobject.Substitute x + + +(* Declaration of the Hint Rewrite library object *) +let (in_hintrewrite,out_hintrewrite)= + Libobject.declare_object {(Libobject.default_object "HINT_REWRITE") with + Libobject.open_function = (fun i o -> if i=1 then cache_hintrewrite o); + Libobject.cache_function = cache_hintrewrite; + Libobject.subst_function = subst_hintrewrite; + Libobject.classify_function = classify_hintrewrite; + Libobject.export_function = export_hintrewrite } + +(* To add rewriting rules to a base *) +let add_rew_rules base lrul = + let lrul = List.rev_map (fun (c,b,t) -> (c,b,Tacinterp.glob_tactic t)) lrul in + Lib.add_anonymous_leaf (in_hintrewrite (base,lrul)) diff --git a/tactics/autorewrite.mli b/tactics/autorewrite.mli new file mode 100644 index 00000000..e97cde83 --- /dev/null +++ b/tactics/autorewrite.mli @@ -0,0 +1,22 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* raw_rew_rule list -> unit + +(* The AutoRewrite tactic *) +val autorewrite : tactic -> string list -> tactic diff --git a/tactics/btermdn.ml b/tactics/btermdn.ml new file mode 100644 index 00000000..c5cdd540 --- /dev/null +++ b/tactics/btermdn.ml @@ -0,0 +1,51 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* None + | Some (c,l) -> Some(c,List.map (fun c -> (c,depth-1)) l) + +let bounded_constr_val_discr (t,depth) = + if depth = 0 then + None + else + match constr_val_discr t with + | None -> None + | Some (c,l) -> Some(c,List.map (fun c -> (c,depth-1)) l) + +type 'a t = (constr_label,constr_pattern * int,'a) Dn.t + +let create = Dn.create + +let add dn (c,v) = Dn.add dn bounded_constr_pat_discr ((c,!dnet_depth),v) + +let rmv dn (c,v) = Dn.rmv dn bounded_constr_pat_discr ((c,!dnet_depth),v) + +let lookup dn t = + List.map + (fun ((c,_),v) -> (c,v)) + (Dn.lookup dn bounded_constr_val_discr (t,!dnet_depth)) + +let app f dn = Dn.app (fun ((c,_),v) -> f(c,v)) dn + diff --git a/tactics/btermdn.mli b/tactics/btermdn.mli new file mode 100644 index 00000000..fe247495 --- /dev/null +++ b/tactics/btermdn.mli @@ -0,0 +1,28 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* 'a t + +val add : 'a t -> (constr_pattern * 'a) -> 'a t +val rmv : 'a t -> (constr_pattern * 'a) -> 'a t + +val lookup : 'a t -> constr -> (constr_pattern * 'a) list +val app : ((constr_pattern * 'a) -> unit) -> 'a t -> unit + +val dnet_depth : int ref diff --git a/tactics/contradiction.ml b/tactics/contradiction.ml new file mode 100644 index 00000000..c9d0ead5 --- /dev/null +++ b/tactics/contradiction.ml @@ -0,0 +1,88 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* + let ida = pf_nth_hyp_id gl 1 + and idna = pf_nth_hyp_id gl 2 in + exact_no_check (applist(mkVar idna,[mkVar ida])) gl))); + tclIDTAC])); + tclIDTAC])) gls + +(* Contradiction *) + +let filter_hyp f tac gl = + let rec seek = function + | [] -> raise Not_found + | (id,_,t)::rest when f t -> tac id gl + | _::rest -> seek rest in + seek (pf_hyps gl) + +let contradiction_context gl = + let env = pf_env gl in + let sigma = project gl in + let rec seek_neg l gl = match l with + | [] -> error "No such contradiction" + | (id,_,typ)::rest -> + let typ = whd_betadeltaiota env sigma typ in + if is_empty_type typ then + simplest_elim (mkVar id) gl + else match kind_of_term typ with + | Prod (na,t,u) when is_empty_type u -> + (try + filter_hyp (fun typ -> pf_conv_x_leq gl typ t) + (fun id' -> simplest_elim (mkApp (mkVar id,[|mkVar id'|]))) + gl + with Not_found -> seek_neg rest gl) + | _ -> seek_neg rest gl in + seek_neg (pf_hyps gl) gl + +let is_negation_of env sigma typ t = + match kind_of_term (whd_betadeltaiota env sigma t) with + | Prod (na,t,u) -> is_empty_type u & is_conv_leq env sigma typ t + | _ -> false + +let contradiction_term (c,lbind as cl) gl = + let env = pf_env gl in + let sigma = project gl in + let typ = pf_type_of gl c in + let _, ccl = splay_prod env sigma typ in + if is_empty_type ccl then + tclTHEN (elim cl None) (tclTRY assumption) gl + else + try + if lbind = NoBindings then + filter_hyp (is_negation_of env sigma typ) + (fun id -> simplest_elim (mkApp (mkVar id,[|c|]))) gl + else + raise Not_found + with Not_found -> error "Not a contradiction" + +let contradiction = function + | None -> tclTHEN intros contradiction_context + | Some c -> contradiction_term c diff --git a/tactics/contradiction.mli b/tactics/contradiction.mli new file mode 100644 index 00000000..90ec101c --- /dev/null +++ b/tactics/contradiction.mli @@ -0,0 +1,19 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* tactic +val contradiction : constr with_bindings option -> tactic diff --git a/tactics/dhyp.ml b/tactics/dhyp.ml new file mode 100644 index 00000000..fb672d0b --- /dev/null +++ b/tactics/dhyp.ml @@ -0,0 +1,373 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* + SORT= + + and from these patterns, we will be able to decide which tactic to + execute. + + For hypotheses, we have a vector of 4 patterns: + + HYP[TYP] HYP[SORT] CONCL[TYP] CONCL[SORT] + + and for conclusions, we have 2: + + CONCL[TYP] CONCL[SORT] + + If the user doesn't supply some of these, they are just replaced + with empties. + + The process of matching goes like this: + + We use a discrimination net to look for matches between the pattern + for HYP[TOP] (CONCL[TOP]) and the type of the chosen hypothesis. + Then, we use this to look for the right tactic to apply, by + matching the rest of the slots. Each match is tried, and if there + is more than one, this fact is reported, and the one with the + lowest priority is taken. The priority is a parameter of the + tactic input. + + The tactic input is an expression to hand to the + tactic-interpreter, and its priority. + + For most tactics, the priority should be the number of subgoals + generated. + + Matching is compatible with second-order matching of sopattern. + + SYNTAX: + + Hint DHyp pri . + + and + + Hint DConcl pri . + + The bindings at the end allow us to transfer information from the + patterns on terms into the patterns on tactics in a safe way - we + will perform second-order normalization and conversion to an AST + before substitution into the tactic-expression. + + WARNING: The binding mechanism is NOT intended to facilitate the + transfer of large amounts of information from the terms to the + tactic. This should be done in a special-purpose tactic. + + *) + +(* + +Example : The tactic "if there is a hypothesis saying that the +successor of some number is smaller than zero, then invert such +hypothesis" is defined in this way: + +Require DHyp. +Hint Destruct Hypothesis less_than_zero (le (S ?) O) 1 + (:tactic:). + +Then, the tactic is used like this: + +Goal (le (S O) O) -> False. +Intro H. +DHyp H. +Qed. + +The name "$0" refers to the matching hypothesis --in this case the +hypothesis H. + +Similarly for the conclusion : + +Hint Destruct Conclusion equal_zero (? = ?) 1 (:tactic:). + +Goal (plus O O)=O. +DConcl. +Qed. + +The "Discardable" option clears the hypothesis after using it. + +Require DHyp. +Hint Destruct Discardable Hypothesis less_than_zero (le (S ?) O) 1 + (:tactic:). + +Goal (n:nat)(le (S n) O) -> False. +Intros n H. +DHyp H. +Qed. +-- Eduardo (9/3/97 ) + +*) + +open Pp +open Util +open Names +open Term +open Environ +open Reduction +open Proof_type +open Rawterm +open Tacmach +open Refiner +open Tactics +open Clenv +open Tactics +open Tacticals +open Libobject +open Library +open Pattern +open Matching +open Ast +open Pcoq +open Tacexpr +open Libnames + +(* two patterns - one for the type, and one for the type of the type *) +type destructor_pattern = { + d_typ: constr_pattern; + d_sort: constr_pattern } + +let subst_destructor_pattern subst { d_typ = t; d_sort = s } = + { d_typ = subst_pattern subst t; d_sort = subst_pattern subst s } + +(* hypothesis patterns might need to do matching on the conclusion, too. + * conclusion-patterns only need to do matching on the hypothesis *) +type located_destructor_pattern = + (* discardable, pattern for hyp, pattern for concl *) + (bool * destructor_pattern * destructor_pattern, + (* pattern for concl *) + destructor_pattern) location + +let subst_located_destructor_pattern subst = function + | HypLocation (b,d,d') -> + HypLocation + (b,subst_destructor_pattern subst d, subst_destructor_pattern subst d') + | ConclLocation d -> + ConclLocation (subst_destructor_pattern subst d) + +type destructor_data = { + d_pat : located_destructor_pattern; + d_pri : int; + d_code : identifier option * glob_tactic_expr (* should be of phylum tactic *) +} + +type t = (identifier,destructor_data) Nbtermdn.t +type frozen_t = (identifier,destructor_data) Nbtermdn.frozen_t + +let tactab = (Nbtermdn.create () : t) + +let lookup pat = Nbtermdn.lookup tactab pat + +let init () = Nbtermdn.empty tactab + +let freeze () = Nbtermdn.freeze tactab +let unfreeze fs = Nbtermdn.unfreeze fs tactab + +let rollback f x = + let fs = freeze() in + try f x with e -> (unfreeze fs; raise e) + +let add (na,dd) = + let pat = match dd.d_pat with + | HypLocation(_,p,_) -> p.d_typ + | ConclLocation p -> p.d_typ + in + if Nbtermdn.in_dn tactab na then begin + msgnl (str "Warning [Overriding Destructor Entry " ++ + str (string_of_id na) ++ str"]"); + Nbtermdn.remap tactab na (pat,dd) + end else + Nbtermdn.add tactab (na,(pat,dd)) + +let _ = + Summary.declare_summary "destruct-hyp-concl" + { Summary.freeze_function = freeze; + Summary.unfreeze_function = unfreeze; + Summary.init_function = init; + Summary.survive_module = false; + Summary.survive_section = false } + +let forward_subst_tactic = + ref (fun _ -> failwith "subst_tactic is not installed for DHyp") + +let set_extern_subst_tactic f = forward_subst_tactic := f + +let cache_dd (_,(_,na,dd)) = + try + add (na,dd) + with _ -> + anomalylabstrm "Dhyp.add" + (str"The code which adds destructor hints broke;" ++ spc () ++ + str"this is not supposed to happen") + +let classify_dd (_,(local,_,_ as o)) = + if local then Dispose else Substitute o + +let export_dd (local,_,_ as x) = if local then None else Some x + +let subst_dd (_,subst,(local,na,dd)) = + (local,na, + { d_pat = subst_located_destructor_pattern subst dd.d_pat; + d_pri = dd.d_pri; + d_code = !forward_subst_tactic subst dd.d_code }) + +let (inDD,outDD) = + declare_object {(default_object "DESTRUCT-HYP-CONCL-DATA") with + cache_function = cache_dd; + open_function = (fun i o -> if i=1 then cache_dd o); + subst_function = subst_dd; + classify_function = classify_dd; + export_function = export_dd } + +let forward_intern_tac = + ref (fun _ -> failwith "intern_tac is not installed for DHyp") + +let set_extern_intern_tac f = forward_intern_tac := f + +let catch_all_sort_pattern = PMeta(Some (id_of_string "SORT")) +let catch_all_type_pattern = PMeta(Some (id_of_string "TYPE")) + +let add_destructor_hint local na loc pat pri code = + let code = !forward_intern_tac code in + let code = + begin match loc, code with + | HypLocation _, TacFun ([id],body) -> (id,body) + | ConclLocation _, _ -> (None, code) + | _ -> + errorlabstrm "add_destructor_hint" + (str "The tactic should be a function of the hypothesis name") end + in + let (_,pat) = Constrintern.interp_constrpattern Evd.empty (Global.env()) pat + in + let pat = match loc with + | HypLocation b -> + HypLocation + (b,{d_typ=pat;d_sort=catch_all_sort_pattern}, + {d_typ=catch_all_type_pattern;d_sort=catch_all_sort_pattern}) + | ConclLocation () -> + ConclLocation({d_typ=pat;d_sort=catch_all_sort_pattern}) in + Lib.add_anonymous_leaf + (inDD (local,na,{ d_pat = pat; d_pri=pri; d_code=code })) + +let match_dpat dp cls gls = + match (cls,dp) with + | ({onhyps=lo;onconcl=false},HypLocation(_,hypd,concld)) -> + let hl = match lo with + Some l -> l + | None -> List.map (fun id -> (id,[],(InHyp,ref None))) + (pf_ids_of_hyps gls) in + if not + (List.for_all + (fun (id,_,(hl,_)) -> + let cltyp = pf_get_hyp_typ gls id in + let cl = pf_concl gls in + (hl=InHyp) & + (is_matching hypd.d_typ cltyp) & + (is_matching hypd.d_sort (pf_type_of gls cltyp)) & + (is_matching concld.d_typ cl) & + (is_matching concld.d_sort (pf_type_of gls cl))) + hl) + then error "No match" + | ({onhyps=Some[];onconcl=true},ConclLocation concld) -> + let cl = pf_concl gls in + if not + ((is_matching concld.d_typ cl) & + (is_matching concld.d_sort (pf_type_of gls cl))) + then error "No match" + | _ -> error "ApplyDestructor" + +let forward_interp_tactic = + ref (fun _ -> failwith "interp_tactic is not installed for DHyp") + +let set_extern_interp f = forward_interp_tactic := f + +let applyDestructor cls discard dd gls = + match_dpat dd.d_pat cls gls; + let cll = simple_clause_list_of cls gls in + let tacl = + List.map (fun cl -> + match cl, dd.d_code with + | Some (id,_,_), (Some x, tac) -> + let arg = + ConstrMayEval(ConstrTerm (RRef(dummy_loc,VarRef id),None)) in + TacLetIn ([(dummy_loc, x), None, arg], tac) + | None, (None, tac) -> tac + | _, (Some _,_) -> error "Destructor expects an hypothesis" + | _, (None,_) -> error "Destructor is for conclusion") + cll in + let discard_0 = + List.map (fun cl -> + match (cl,dd.d_pat) with + | (Some (id,_,_),HypLocation(discardable,_,_)) -> + if discard & discardable then thin [id] else tclIDTAC + | (None,ConclLocation _) -> tclIDTAC + | _ -> error "ApplyDestructor" ) cll in + tclTHEN (tclMAP !forward_interp_tactic tacl) (tclTHENLIST discard_0) gls + + +(* [DHyp id gls] + + will take an identifier, get its type, look it up in the + discrimination net, get the destructors stored there, and then try + them in order of priority. *) + +let destructHyp discard id gls = + let hyptyp = pf_get_hyp_typ gls id in + let ddl = List.map snd (lookup hyptyp) in + let sorted_ddl = Sort.list (fun dd1 dd2 -> dd1.d_pri > dd2.d_pri) ddl in + tclFIRST (List.map (applyDestructor (onHyp id) discard) sorted_ddl) gls + +let cDHyp id gls = destructHyp true id gls +let dHyp id gls = destructHyp false id gls + +let h_destructHyp b id = + abstract_tactic (TacDestructHyp (b,(dummy_loc,id))) (destructHyp b id) + +(* [DConcl gls] + + will take a goal, get its concl, look it up in the + discrimination net, get the destructors stored there, and then try + them in order of priority. *) + +let dConcl gls = + let ddl = List.map snd (lookup (pf_concl gls)) in + let sorted_ddl = Sort.list (fun dd1 dd2 -> dd1.d_pri > dd2.d_pri) ddl in + tclFIRST (List.map (applyDestructor onConcl false) sorted_ddl) gls + +let h_destructConcl = abstract_tactic TacDestructConcl dConcl + +let to2Lists (table : t) = Nbtermdn.to2lists table + +let rec search n = + if n=0 then error "Search has reached zero."; + tclFIRST + [intros; + assumption; + (tclTHEN + (Tacticals.tryAllClauses + (function + | Some (id,_,_) -> (dHyp id) + | None -> dConcl )) + (search (n-1)))] + +let auto_tdb n = tclTRY (tclCOMPLETE (search n)) + +let search_depth_tdb = ref(5) + +let depth_tdb = function + | None -> !search_depth_tdb + | Some n -> n + +let h_auto_tdb n = abstract_tactic (TacAutoTDB n) (auto_tdb (depth_tdb n)) diff --git a/tactics/dhyp.mli b/tactics/dhyp.mli new file mode 100644 index 00000000..a0cef679 --- /dev/null +++ b/tactics/dhyp.mli @@ -0,0 +1,32 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* tactic) -> unit +val set_extern_intern_tac : (raw_tactic_expr -> glob_tactic_expr) -> unit + +(* +val dHyp : identifier -> tactic +val dConcl : tactic +*) +val h_destructHyp : bool -> identifier -> tactic +val h_destructConcl : tactic +val h_auto_tdb : int option -> tactic + +val add_destructor_hint : + Vernacexpr.locality_flag -> identifier -> (bool,unit) Tacexpr.location -> + Topconstr.constr_expr -> int -> raw_tactic_expr -> unit diff --git a/tactics/dn.ml b/tactics/dn.ml new file mode 100644 index 00000000..55116831 --- /dev/null +++ b/tactics/dn.ml @@ -0,0 +1,80 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* [] + | h::tl -> pathrec tl h + + and pathrec deferred t = + match dna t with + | None -> + None :: (path_of_deferred deferred) + | Some (lbl,[]) -> + (Some (lbl,0))::(path_of_deferred deferred) + | Some (lbl,(h::def_subl as v)) -> + (Some (lbl,List.length v))::(pathrec (def_subl@deferred) h) + in + pathrec [] + +let tm_of tm lbl = + try [Tlm.map tm lbl] with Not_found -> [] + +let lookup tm dna t = + let rec lookrec t tm = + (tm_of tm None)@ + (match dna t with + | None -> [] + | Some(lbl,v) -> + List.fold_left + (fun l c -> List.flatten(List.map (lookrec c) l)) + (tm_of tm (Some(lbl,List.length v))) v) + in + List.flatten(List.map Tlm.xtract (lookrec t tm)) + +let add tm dna (pat,inf) = + let p = path_of dna pat in Tlm.add tm (p,(pat,inf)) + +let rmv tm dna (pat,inf) = + let p = path_of dna pat in Tlm.rmv tm (p,(pat,inf)) + +let app f tm = Tlm.app (fun (_,p) -> f p) tm + diff --git a/tactics/dn.mli b/tactics/dn.mli new file mode 100644 index 00000000..a54007d8 --- /dev/null +++ b/tactics/dn.mli @@ -0,0 +1,40 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* ('lbl,'pat,'inf) t + +(* [add t f (tree,inf)] adds a structured object [tree] together with + the associated information [inf] to the table [t]; the function + [f] is used to translated [tree] into its prefix decomposition: [f] + must decompose any tree into a label characterizing its root node and + the list of its subtree *) + +val add : ('lbl,'pat,'inf) t -> ('lbl,'pat) decompose_fun -> 'pat * 'inf + -> ('lbl,'pat,'inf) t + +val rmv : ('lbl,'pat,'inf) t -> ('lbl,'pat) decompose_fun -> 'pat * 'inf + -> ('lbl,'pat,'inf) t + +(* [lookup t f tree] looks for trees (and their associated + information) in table [t] such that the structured object [tree] + matches against them; [f] is used to translated [tree] into its + prefix decomposition: [f] must decompose any tree into a label + characterizing its root node and the list of its subtree *) + +val lookup : ('lbl,'pat,'inf) t -> ('lbl,'term) decompose_fun -> 'term + -> ('pat * 'inf) list + +val app : (('pat * 'inf) -> unit) -> ('lbl,'pat,'inf) t -> unit diff --git a/tactics/doc.tex b/tactics/doc.tex new file mode 100644 index 00000000..d44cc14a --- /dev/null +++ b/tactics/doc.tex @@ -0,0 +1,11 @@ + +\newpage +\section*{The Tactics} + +\ocwsection \label{tactics} +This chapter describes the \Coq\ main tactics. +The modules of that chapter are organized as follows. + +\bigskip +\begin{center}\epsfig{file=tactics.dep.ps,width=\linewidth}\end{center} + diff --git a/tactics/eauto.ml4 b/tactics/eauto.ml4 new file mode 100644 index 00000000..31d79948 --- /dev/null +++ b/tactics/eauto.ml4 @@ -0,0 +1,448 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* [ e_give_exact c ] +END*) +TACTIC EXTEND Eexact +| [ "EExact" constr(c) ] -> [ e_give_exact c ] +END + +let e_give_exact_constr = h_eexact + +let registered_e_assumption gl = + tclFIRST (List.map (fun id gl -> e_give_exact_constr (mkVar id) gl) + (pf_ids_of_hyps gl)) gl + +(* This automatically define h_eApply (among other things) *) +(*V8 TACTIC EXTEND eapply + [ "eapply" constr_with_bindings(c) ] -> [ e_resolve_with_bindings_tac c ] +END*) +TACTIC EXTEND eapply + [ "EApply" constr_with_bindings(c) ] -> [ e_resolve_with_bindings_tac c ] +END + +let vernac_e_resolve_constr c = h_eapply (c,NoBindings) + +let e_constructor_tac boundopt i lbind gl = + let cl = pf_concl gl in + let (mind,redcl) = pf_reduce_to_quantified_ind gl cl in + let nconstr = + Array.length (snd (Global.lookup_inductive mind)).mind_consnames + and sigma = project gl in + if i=0 then error "The constructors are numbered starting from 1"; + if i > nconstr then error "Not enough constructors"; + begin match boundopt with + | Some expctdnum -> + if expctdnum <> nconstr then + error "Not the expected number of constructors" + | None -> () + end; + let cons = mkConstruct (ith_constructor_of_inductive mind i) in + let apply_tac = e_resolve_with_bindings_tac (cons,lbind) in + (tclTHENLIST [convert_concl_no_check redcl; intros; apply_tac]) gl + +let e_one_constructor i = e_constructor_tac None i + +let e_any_constructor tacopt gl = + let t = match tacopt with None -> tclIDTAC | Some t -> t in + let mind = fst (pf_reduce_to_quantified_ind gl (pf_concl gl)) in + let nconstr = + Array.length (snd (Global.lookup_inductive mind)).mind_consnames in + if nconstr = 0 then error "The type has no constructors"; + tclFIRST (List.map (fun i -> tclTHEN (e_one_constructor i NoBindings) t) + (interval 1 nconstr)) gl + +let e_left = e_constructor_tac (Some 2) 1 + +let e_right = e_constructor_tac (Some 2) 2 + +let e_split = e_constructor_tac (Some 1) 1 + +(* This automatically define h_econstructor (among other things) *) +(*V8 TACTIC EXTEND eapply + [ "econstructor" integer(n) with_bindings(c) ] -> [ e_constructor_tac None n c ] +END*) +TACTIC EXTEND econstructor + [ "EConstructor" integer(n) "with" bindings(c) ] -> [ e_constructor_tac None n c ] + | [ "EConstructor" integer(n) ] -> [ e_constructor_tac None n NoBindings ] + | [ "EConstructor" tactic_opt(t) ] -> [ e_any_constructor (option_app Tacinterp.eval_tactic t) ] + END + +TACTIC EXTEND eleft + [ "ELeft" "with" bindings(l) ] -> [e_left l] + | [ "ELeft"] -> [e_left NoBindings] +END + +TACTIC EXTEND eright + [ "ERight" "with" bindings(l) ] -> [e_right l] + | [ "ERight" ] -> [e_right NoBindings] +END + +TACTIC EXTEND esplit + [ "ESplit" "with" bindings(l) ] -> [e_split l] + | [ "ESplit"] -> [e_split NoBindings] +END + + +TACTIC EXTEND eexists + [ "EExists" bindings(l) ] -> [e_split l] +END + + +(************************************************************************) +(* PROLOG tactic *) +(************************************************************************) + +let one_step l gl = + [Tactics.intro] + @ (List.map e_resolve_constr (List.map mkVar (pf_ids_of_hyps gl))) + @ (List.map e_resolve_constr l) + @ (List.map assumption (pf_ids_of_hyps gl)) + +let rec prolog l n gl = + if n <= 0 then error "prolog - failure"; + let prol = (prolog l (n-1)) in + (tclFIRST (List.map (fun t -> (tclTHEN t prol)) (one_step l gl))) gl + +let prolog_tac l n gl = + let n = + match n with + | Genarg.ArgArg n -> n + | _ -> error "Prolog called with a non closed argument" + in + try (prolog l n gl) + with UserError ("Refiner.tclFIRST",_) -> + errorlabstrm "Prolog.prolog" (str "Prolog failed") + +(* V8 TACTIC EXTEND prolog +| [ "prolog" "[" constr_list(l) "]" int_or_var(n) ] -> [ prolog_tac l n ] +END*) +TACTIC EXTEND Prolog +| [ "Prolog" "[" constr_list(l) "]" int_or_var(n) ] -> [ prolog_tac l n ] +END + +(* +let vernac_prolog = + let uncom = function + | Constr c -> c + | _ -> assert false + in + let gentac = + hide_tactic "Prolog" + (function + | (Integer n) :: al -> prolog_tac (List.map uncom al) n + | _ -> assert false) + in + fun coms n -> + gentac ((Integer n) :: (List.map (fun com -> (Constr com)) coms)) +*) + +open Auto + +(***************************************************************************) +(* A tactic similar to Auto, but using EApply, Assumption and e_give_exact *) +(***************************************************************************) + +let unify_e_resolve (c,clenv) gls = + let (wc,kONT) = startWalk gls in + let clenv' = connect_clenv wc clenv in + let _ = clenv_unique_resolver false clenv' gls in + vernac_e_resolve_constr c gls + +let rec e_trivial_fail_db db_list local_db goal = + let tacl = + registered_e_assumption :: + (tclTHEN Tactics.intro + (function g'-> + let d = pf_last_hyp g' in + let hintl = make_resolve_hyp (pf_env g') (project g') d in + (e_trivial_fail_db db_list + (Hint_db.add_list hintl local_db) g'))) :: + (List.map fst (e_trivial_resolve db_list local_db (pf_concl goal)) ) + in + tclFIRST (List.map tclCOMPLETE tacl) goal + +and e_my_find_search db_list local_db hdc concl = + let hdc = head_of_constr_reference hdc in + let hintl = + if occur_existential concl then + list_map_append (Hint_db.map_all hdc) (local_db::db_list) + else + list_map_append (Hint_db.map_auto (hdc,concl)) (local_db::db_list) + in + let tac_of_hint = + fun ({pri=b; pat = p; code=t} as patac) -> + (b, + let tac = + match t with + | Res_pf (term,cl) -> unify_resolve (term,cl) + | ERes_pf (term,cl) -> unify_e_resolve (term,cl) + | Give_exact (c) -> e_give_exact_constr c + | Res_pf_THEN_trivial_fail (term,cl) -> + tclTHEN (unify_e_resolve (term,cl)) + (e_trivial_fail_db db_list local_db) + | Unfold_nth c -> unfold_constr c + | Extern tacast -> conclPattern concl + (out_some p) tacast + in + (tac,fmt_autotactic t)) + (*i + fun gls -> pPNL (fmt_autotactic t); Format.print_flush (); + try tac gls + with e when Logic.catchable_exception(e) -> + (Format.print_string "Fail\n"; + Format.print_flush (); + raise e) + i*) + in + List.map tac_of_hint hintl + +and e_trivial_resolve db_list local_db gl = + try + Auto.priority + (e_my_find_search db_list local_db + (List.hd (head_constr_bound gl [])) gl) + with Bound | Not_found -> [] + +let e_possible_resolve db_list local_db gl = + try List.map snd (e_my_find_search db_list local_db + (List.hd (head_constr_bound gl [])) gl) + with Bound | Not_found -> [] + +let assumption_tac_list id = apply_tac_list (e_give_exact_constr (mkVar id)) + +let find_first_goal gls = + try first_goal gls with UserError _ -> assert false + +(*s The following module [SearchProblem] is used to instantiate the generic + exploration functor [Explore.Make]. *) + +module SearchProblem = struct + + type state = { + depth : int; (*r depth of search before failing *) + tacres : goal list sigma * validation; + last_tactic : std_ppcmds; + dblist : Auto.Hint_db.t list; + localdb : Auto.Hint_db.t list } + + let success s = (sig_it (fst s.tacres)) = [] + + let rec filter_tactics (glls,v) = function + | [] -> [] + | (tac,pptac) :: tacl -> + try + let (lgls,ptl) = apply_tac_list tac glls in + let v' p = v (ptl p) in + ((lgls,v'),pptac) :: filter_tactics (glls,v) tacl + with e when Logic.catchable_exception e -> + filter_tactics (glls,v) tacl + + let rec list_addn n x l = + if n = 0 then l else x :: (list_addn (pred n) x l) + + (* Ordering of states is lexicographic on depth (greatest first) then + number of remaining goals. *) + let compare s s' = + let d = s'.depth - s.depth in + let nbgoals s = List.length (sig_it (fst s.tacres)) in + if d <> 0 then d else nbgoals s - nbgoals s' + + let branching s = + if s.depth = 0 then + [] + else + let lg = fst s.tacres in + let nbgl = List.length (sig_it lg) in + assert (nbgl > 0); + let g = find_first_goal lg in + let assumption_tacs = + let l = + filter_tactics s.tacres + (List.map + (fun id -> (e_give_exact_constr (mkVar id), + (str "Exact" ++ spc () ++ pr_id id))) + (pf_ids_of_hyps g)) + in + List.map (fun (res,pp) -> { depth = s.depth; tacres = res; + last_tactic = pp; dblist = s.dblist; + localdb = List.tl s.localdb }) l + in + let intro_tac = + List.map + (fun ((lgls,_) as res,pp) -> + let g' = first_goal lgls in + let hintl = + make_resolve_hyp (pf_env g') (project g') (pf_last_hyp g') + in + let ldb = Hint_db.add_list hintl (List.hd s.localdb) in + { depth = s.depth; tacres = res; + last_tactic = pp; dblist = s.dblist; + localdb = ldb :: List.tl s.localdb }) + (filter_tactics s.tacres [Tactics.intro,(str "Intro")]) + in + let rec_tacs = + let l = + filter_tactics s.tacres + (e_possible_resolve s.dblist (List.hd s.localdb) (pf_concl g)) + in + List.map + (fun ((lgls,_) as res, pp) -> + let nbgl' = List.length (sig_it lgls) in + if nbgl' < nbgl then + { depth = s.depth; tacres = res; last_tactic = pp; + dblist = s.dblist; localdb = List.tl s.localdb } + else + { depth = pred s.depth; tacres = res; + dblist = s.dblist; last_tactic = pp; + localdb = + list_addn (nbgl'-nbgl) (List.hd s.localdb) s.localdb }) + l + in + List.sort compare (assumption_tacs @ intro_tac @ rec_tacs) + + let pp s = + msg (hov 0 (str " depth=" ++ int s.depth ++ spc () ++ + s.last_tactic ++ str "\n")) + +end + +module Search = Explore.Make(SearchProblem) + +let make_initial_state n gl dblist localdb = + { SearchProblem.depth = n; + SearchProblem.tacres = tclIDTAC gl; + SearchProblem.last_tactic = (mt ()); + SearchProblem.dblist = dblist; + SearchProblem.localdb = [localdb] } + +let e_depth_search debug p db_list local_db gl = + try + let tac = if debug then Search.debug_depth_first else Search.depth_first in + let s = tac (make_initial_state p gl db_list local_db) in + s.SearchProblem.tacres + with Not_found -> error "EAuto: depth first search failed" + +let e_breadth_search debug n db_list local_db gl = + try + let tac = + if debug then Search.debug_breadth_first else Search.breadth_first + in + let s = tac (make_initial_state n gl db_list local_db) in + s.SearchProblem.tacres + with Not_found -> error "EAuto: breadth first search failed" + +let e_search_auto debug (in_depth,p) db_list gl = + let local_db = make_local_hint_db gl in + if in_depth then + e_depth_search debug p db_list local_db gl + else + e_breadth_search debug p db_list local_db gl + +let eauto debug np dbnames = + let db_list = + List.map + (fun x -> + try Stringmap.find x !searchtable + with Not_found -> error ("EAuto: "^x^": No such Hint database")) + ("core"::dbnames) + in + tclTRY (e_search_auto debug np db_list) + +let full_eauto debug n gl = + let dbnames = stringmap_dom !searchtable in + let dbnames = list_subtract dbnames ["v62"] in + let db_list = List.map (fun x -> Stringmap.find x !searchtable) dbnames in + let local_db = make_local_hint_db gl in + tclTRY (e_search_auto debug n db_list) gl + +let gen_eauto d np = function + | None -> full_eauto d np + | Some l -> eauto d np l + +let make_depth = function + | None -> !default_search_depth + | Some (Genarg.ArgArg d) -> d + | _ -> error "EAuto called with a non closed argument" + +let make_dimension n = function + | None -> (true,make_depth n) + | Some (Genarg.ArgArg d) -> (false,d) + | _ -> error "EAuto called with a non closed argument" + +open Genarg + +(* Hint bases *) + +let pr_hintbases _prc _prt = function + | None -> str " with *" + | Some [] -> mt () + | Some l -> str " with " ++ Util.prlist_with_sep spc str l + +ARGUMENT EXTEND hintbases + TYPED AS preident_list_opt + PRINTED BY pr_hintbases +| [ "with" "*" ] -> [ None ] +| [ "with" ne_preident_list(l) ] -> [ Some l ] +| [ ] -> [ Some [] ] +END + +TACTIC EXTEND EAuto +| [ "EAuto" int_or_var_opt(n) int_or_var_opt(p) hintbases(db) ] -> + [ gen_eauto false (make_dimension n p) db ] +END + +V7 TACTIC EXTEND EAutodebug +| [ "EAutod" int_or_var_opt(n) int_or_var_opt(p) hintbases(db) ] -> + [ gen_eauto true (make_dimension n p) db ] +END + + diff --git a/tactics/eauto.mli b/tactics/eauto.mli new file mode 100644 index 00000000..c3084e65 --- /dev/null +++ b/tactics/eauto.mli @@ -0,0 +1,25 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* tactic + +val vernac_e_resolve_constr : constr -> tactic + +val e_give_exact_constr : constr -> tactic diff --git a/tactics/elim.ml b/tactics/elim.ml new file mode 100644 index 00000000..5573f9ea --- /dev/null +++ b/tactics/elim.ml @@ -0,0 +1,195 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* if b then acc+2 else acc+1) + 0 ba.branchsign + in + let introElimAssums = tclDO nassums intro in + (tclTHEN introElimAssums (elim_on_ba tac ba)) + +let introCaseAssumsThen tac ba = + let case_thin_sign = + List.flatten + (List.map (function b -> if b then [false;true] else [false]) + ba.branchsign) + in + let n1 = List.length case_thin_sign in + let n2 = List.length ba.branchnames in + let (l1,l2),l3 = + if n1 < n2 then list_chop n1 ba.branchnames, [] + else + (ba.branchnames, []), + if n1 > n2 then snd (list_chop n2 case_thin_sign) else [] in + let introCaseAssums = tclTHEN (intros_pattern None l1) (intros_clearing l3) + in + (tclTHEN introCaseAssums (case_on_ba (tac l2) ba)) + +(* The following tactic Decompose repeatedly applies the + elimination(s) rule(s) of the types satisfying the predicate + ``recognizer'' onto a certain hypothesis. For example : + +Require Elim. +Require Le. + Goal (y:nat){x:nat | (le O x)/\(le x y)}->{x:nat | (le O x)}. + Intros y H. + Decompose [sig and] H;EAuto. + Qed. + +Another example : + + Goal (A,B,C:Prop)(A/\B/\C \/ B/\C \/ C/\A) -> C. + Intros A B C H; Decompose [and or] H; Assumption. + Qed. +*) + +let elimHypThen tac id gl = + elimination_then tac ([],[]) (mkVar id) gl + +let rec general_decompose_on_hyp recognizer = + ifOnHyp recognizer (general_decompose recognizer) (fun _ -> tclIDTAC) + +and general_decompose recognizer id = + elimHypThen + (introElimAssumsThen + (fun bas -> + tclTHEN (clear [id]) + (tclMAP (general_decompose_on_hyp recognizer) + (ids_of_named_context bas.assums)))) + id + +(* Faudrait ajouter un COMPLETE pour que l'hypothèse créée ne reste + pas si aucune élimination n'est possible *) + +(* Meilleures stratégies mais perte de compatibilité *) +let tmphyp_name = id_of_string "_TmpHyp" +let up_to_delta = ref false (* true *) + +let general_decompose recognizer c gl = + let typc = pf_type_of gl c in + tclTHENSV (cut typc) + [| tclTHEN (intro_using tmphyp_name) + (onLastHyp + (ifOnHyp recognizer (general_decompose recognizer) + (fun id -> clear [id]))); + exact_no_check c |] gl + +let head_in gls indl t = + try + let ity,_ = + if !up_to_delta + then find_mrectype (pf_env gls) (project gls) t + else extract_mrectype t + in List.mem ity indl + with Not_found -> false + +let inductive_of = function + | IndRef ity -> ity + | r -> + errorlabstrm "Decompose" + (Printer.pr_global r ++ str " is not an inductive type") + +let decompose_these c l gls = + let indl = (*List.map inductive_of*) l in + general_decompose (fun (_,t) -> head_in gls indl t) c gls + +let decompose_nonrec c gls = + general_decompose + (fun (_,t) -> is_non_recursive_type t) + c gls + +let decompose_and c gls = + general_decompose + (fun (_,t) -> is_conjunction t) + c gls + +let decompose_or c gls = + general_decompose + (fun (_,t) -> is_disjunction t) + c gls + +let h_decompose l c = + Refiner.abstract_tactic (TacDecompose (l,c)) (decompose_these c l) + +let h_decompose_or c = + Refiner.abstract_tactic (TacDecomposeOr c) (decompose_or c) + +let h_decompose_and c = + Refiner.abstract_tactic (TacDecomposeAnd c) (decompose_and c) + +(* The tactic Double performs a double induction *) + +let simple_elimination c gls = + simple_elimination_then (fun _ -> tclIDTAC) c gls + +let induction_trailer abs_i abs_j bargs = + tclTHEN + (tclDO (abs_j - abs_i) intro) + (onLastHyp + (fun id gls -> + let idty = pf_type_of gls (mkVar id) in + let fvty = global_vars (pf_env gls) idty in + let possible_bring_hyps = + (List.tl (nLastHyps (abs_j - abs_i) gls)) @ bargs.assums + in + let (hyps,_) = + List.fold_left + (fun (bring_ids,leave_ids) (cid,_,cidty as d) -> + if not (List.mem cid leave_ids) + then (d::bring_ids,leave_ids) + else (bring_ids,cid::leave_ids)) + ([],fvty) possible_bring_hyps + in + let ids = List.rev (ids_of_named_context hyps) in + (tclTHENSEQ + [bring_hyps hyps; tclTRY (clear ids); + simple_elimination (mkVar id)]) + gls)) + +let double_ind h1 h2 gls = + let abs_i = depth_of_quantified_hypothesis true h1 gls in + let abs_j = depth_of_quantified_hypothesis true h2 gls in + let (abs_i,abs_j) = + if abs_i < abs_j then (abs_i,abs_j) else + if abs_i > abs_j then (abs_j,abs_i) else + error "Both hypotheses are the same" in + let cl = pf_concl gls in + (tclTHEN (tclDO abs_i intro) + (onLastHyp + (fun id -> + elimination_then + (introElimAssumsThen (induction_trailer abs_i abs_j)) + ([],[]) (mkVar id)))) gls + +let h_double_induction h1 h2 = + Refiner.abstract_tactic (TacDoubleInduction (h1,h2)) (double_ind h1 h2) + + diff --git a/tactics/elim.mli b/tactics/elim.mli new file mode 100644 index 00000000..a891cd9d --- /dev/null +++ b/tactics/elim.mli @@ -0,0 +1,38 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* tactic) -> branch_args -> tactic + +val introCaseAssumsThen : + (intro_pattern_expr list -> branch_assumptions -> tactic) -> + branch_args -> tactic + +val general_decompose : (identifier * constr -> bool) -> constr -> tactic +val decompose_nonrec : constr -> tactic +val decompose_and : constr -> tactic +val decompose_or : constr -> tactic +val h_decompose : inductive list -> constr -> tactic +val h_decompose_or : constr -> tactic +val h_decompose_and : constr -> tactic + +val double_ind : Rawterm.quantified_hypothesis -> Rawterm.quantified_hypothesis -> tactic +val h_double_induction : Rawterm.quantified_hypothesis -> Rawterm.quantified_hypothesis->tactic diff --git a/tactics/eqdecide.ml4 b/tactics/eqdecide.ml4 new file mode 100644 index 00000000..8edfcb3e --- /dev/null +++ b/tactics/eqdecide.ml4 @@ -0,0 +1,188 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* (clear [destVar c]))) + +let mkBranches = + tclTHENSEQ + [intro; + tclLAST_HYP h_simplest_elim; + clear_last; + intros ; + tclLAST_HYP h_simplest_case; + clear_last; + intros] + +let solveRightBranch = + tclTHEN h_simplest_right + (tclTHEN (intro_force true) + (onLastHyp (fun id -> Extratactics.h_discrHyp (Rawterm.NamedHyp id)))) + +let h_solveRightBranch = + Refiner.abstract_extended_tactic "solveRightBranch" [] solveRightBranch + +(* +let h_solveRightBranch = + hide_atomic_tactic "solveRightBranch" solveRightBranch +*) + +(* Constructs the type {c1=c2}+{~c1=c2} *) + +let mkDecideEqGoal rectype c1 c2 g = + let equality = mkApp(build_coq_eq(), [|rectype; c1; c2|]) in + let disequality = mkApp(build_coq_not (), [|equality|]) in + mkApp(build_coq_sumbool (), [|equality; disequality |]) + + +(* Constructs the type (x1,x2:R){x1=x2}+{~x1=x2} *) + +let mkGenDecideEqGoal rectype g = + let hypnames = pf_ids_of_hyps g in + let xname = next_ident_away (id_of_string "x") hypnames + and yname = next_ident_away (id_of_string "y") hypnames in + (mkNamedProd xname rectype + (mkNamedProd yname rectype + (mkDecideEqGoal rectype (mkVar xname) (mkVar yname) g))) + +let eqCase tac = + (tclTHEN intro + (tclTHEN (tclLAST_HYP Extratactics.h_rewriteLR) + (tclTHEN clear_last + tac))) + +let diseqCase = + let diseq = id_of_string "diseq" in + let absurd = id_of_string "absurd" in + (tclTHEN (intro_using diseq) + (tclTHEN h_simplest_right + (tclTHEN red_in_concl + (tclTHEN (intro_using absurd) + (tclTHEN (h_simplest_apply (mkVar diseq)) + (tclTHEN (Extratactics.h_injHyp (Rawterm.NamedHyp absurd)) + full_trivial)))))) + +let solveArg a1 a2 tac g = + let rectype = pf_type_of g a1 in + let decide = mkDecideEqGoal rectype a1 a2 g in + (tclTHENS + (h_elim_type decide) + [(eqCase tac);diseqCase;default_auto]) g + +let solveLeftBranch rectype g = + try + let (lhs,rhs) = match_eqdec_partial (pf_concl g) in + let (mib,mip) = Global.lookup_inductive rectype in + let nparams = mip.mind_nparams in + let getargs l = list_skipn nparams (snd (decompose_app l)) in + let rargs = getargs rhs + and largs = getargs lhs in + List.fold_right2 + solveArg largs rargs (tclTHEN h_simplest_left h_reflexivity) g + with PatternMatchingFailure -> error "Unexpected conclusion!" + +(* The tactic Decide Equality *) + +let hd_app c = match kind_of_term c with + | App (h,_) -> h + | _ -> c + +let decideGralEquality g = + try + let typ = match_eqdec (pf_concl g) in + let headtyp = hd_app (pf_compute g typ) in + let rectype = + match kind_of_term headtyp with + | Ind mi -> mi + | _ -> error "This decision procedure only works for inductive objects" + in + (tclTHEN + mkBranches + (tclORELSE h_solveRightBranch (solveLeftBranch rectype))) g + with PatternMatchingFailure -> + error "The goal does not have the expected form" + + +let decideEquality c1 c2 g = + let rectype = (pf_type_of g c1) in + let decide = mkGenDecideEqGoal rectype g in + (tclTHENS (cut decide) [default_auto;decideGralEquality]) g + + +(* The tactic Compare *) + +let compare c1 c2 g = + let rectype = pf_type_of g c1 in + let decide = mkDecideEqGoal rectype c1 c2 g in + (tclTHENS (cut decide) + [(tclTHEN intro + (tclTHEN (tclLAST_HYP simplest_case) + clear_last)); + decideEquality c1 c2]) g + + +(* User syntax *) + +TACTIC EXTEND DecideEquality + [ "Decide" "Equality" constr(c1) constr(c2) ] -> [ decideEquality c1 c2 ] +| [ "Decide" "Equality" ] -> [ decideGralEquality ] +END + +TACTIC EXTEND Compare +| [ "Compare" constr(c1) constr(c2) ] -> [ compare c1 c2 ] +END + diff --git a/tactics/equality.ml b/tactics/equality.ml new file mode 100644 index 00000000..dd9054f5 --- /dev/null +++ b/tactics/equality.ml @@ -0,0 +1,1213 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* __r + with type (A:)(x:A)(P:A->Prop)(P x)->(y:A)(eqname A y x)->(P y). + If another equality myeq is introduced, then corresponding theorems + myeq_ind_r, myeq_rec_r and myeq_rect_r have to be proven. See below. + -- Eduardo (19/8/97 +*) + +let general_rewrite_bindings lft2rgt (c,l) gl = + let ctype = pf_type_of gl c in + let env = pf_env gl in + let sigma = project gl in + let _,t = splay_prod env sigma ctype in + match match_with_equation t with + | None -> + if l = NoBindings + then general_s_rewrite lft2rgt c gl + else error "The term provided does not end with an equation" + | Some (hdcncl,_) -> + let hdcncls = string_of_inductive hdcncl in + let suffix = Indrec.elimination_suffix (elimination_sort_of_goal gl)in + let elim = + if lft2rgt then + pf_global gl (id_of_string (hdcncls^suffix^"_r")) + else + pf_global gl (id_of_string (hdcncls^suffix)) + in + tclNOTSAMEGOAL (general_elim (c,l) (elim,NoBindings) ~allow_K:false) gl + (* was tclWEAK_PROGRESS which only fails for tactics generating one subgoal + and did not fail for useless conditional rewritings generating an + extra condition *) + +(* Conditional rewriting, the success of a rewriting is related + to the resolution of the conditions by a given tactic *) + +let conditional_rewrite lft2rgt tac (c,bl) = + tclTHENSFIRSTn (general_rewrite_bindings lft2rgt (c,bl)) + [|tclIDTAC|] (tclCOMPLETE tac) + +let general_rewrite lft2rgt c = general_rewrite_bindings lft2rgt (c,NoBindings) + +let rewriteLR_bindings = general_rewrite_bindings true +let rewriteRL_bindings = general_rewrite_bindings false + +let rewriteLR = general_rewrite true +let rewriteRL = general_rewrite false + +(* The Rewrite in tactic *) +let general_rewrite_in lft2rgt id (c,l) gl = + let ctype = pf_type_of gl c in + let env = pf_env gl in + let sigma = project gl in + let _,t = splay_prod env sigma ctype in + match match_with_equation t with + | None -> (* Do not deal with setoids yet *) + error "The term provided does not end with an equation" + | Some (hdcncl,_) -> + let hdcncls = string_of_inductive hdcncl in + let suffix = + Indrec.elimination_suffix (elimination_sort_of_hyp id gl) in + let rwr_thm = + if lft2rgt then hdcncls^suffix else hdcncls^suffix^"_r" in + let elim = + try pf_global gl (id_of_string rwr_thm) + with Not_found -> + error ("Cannot find rewrite principle "^rwr_thm) in + general_elim_in id (c,l) (elim,NoBindings) gl + +let rewriteLRin = general_rewrite_in true +let rewriteRLin = general_rewrite_in false + +let conditional_rewrite_in lft2rgt id tac (c,bl) = + tclTHENSFIRSTn (general_rewrite_in lft2rgt id (c,bl)) + [|tclIDTAC|] (tclCOMPLETE tac) + +let rewriteRL_clause = function + | None -> rewriteRL_bindings + | Some id -> rewriteRLin id + +(* Replacing tactics *) + +(* eqt,sym_eqt : equality on Type and its symmetry theorem + c2 c1 : c1 is to be replaced by c2 + unsafe : If true, do not check that c1 and c2 are convertible + gl : goal *) + +let abstract_replace clause c2 c1 unsafe gl = + let t1 = pf_type_of gl c1 + and t2 = pf_type_of gl c2 in + if unsafe or (pf_conv_x gl t1 t2) then + let e = (build_coq_eqT_data ()).eq in + let sym = (build_coq_eqT_data ()).sym in + let eq = applist (e, [t1;c1;c2]) in + tclTHENS (assert_tac false Anonymous eq) + [onLastHyp (fun id -> + tclTHEN + (tclTRY (rewriteRL_clause clause (mkVar id,NoBindings))) + (clear [id])); + tclORELSE assumption + (tclTRY (tclTHEN (apply sym) assumption))] gl + else + error "terms does not have convertible types" + +let replace c2 c1 gl = abstract_replace None c2 c1 false gl + +let replace_in id c2 c1 gl = abstract_replace (Some id) c2 c1 false gl + +(* End of Eduardo's code. The rest of this file could be improved + using the functions match_with_equation, etc that I defined + in Pattern.ml. + -- Eduardo (19/8/97) +*) + +(* Tactics for equality reasoning with the "eq" or "eqT" + relation This code will work with any equivalence relation which + is substitutive *) + +(* Patterns *) + +let build_coq_eq eq = eq.eq +let build_ind eq = eq.ind +let build_rect eq = + match eq.rect with + | None -> assert false + | Some c -> c + +(*********** List of constructions depending of the initial state *) + +let find_eq_pattern aritysort sort = + (* "eq" now accept arguments in Type and elimination to Type *) + Coqlib.build_coq_eq () + +(* [find_positions t1 t2] + + will find the positions in the two terms which are suitable for + discrimination, or for injection. Obviously, if there is a + position which is suitable for discrimination, then we want to + exploit it, and not bother with injection. So when we find a + position which is suitable for discrimination, we will just raise + an exception with that position. + + So the algorithm goes like this: + + if [t1] and [t2] start with the same constructor, then we can + continue to try to find positions in the arguments of [t1] and + [t2]. + + if [t1] and [t2] do not start with the same constructor, then we + have found a discrimination position + + if one [t1] or [t2] do not start with a constructor and the two + terms are not already convertible, then we have found an injection + position. + + A discriminating position consists of a constructor-path and a pair + of operators. The constructor-path tells us how to get down to the + place where the two operators, which must differ, can be found. + + An injecting position has two terms instead of the two operators, + since these terms are different, but not manifestly so. + + A constructor-path is a list of pairs of (operator * int), where + the int (based at 0) tells us which argument of the operator we + descended into. + + *) + +exception DiscrFound of + (constructor * int) list * constructor * constructor + +let find_positions env sigma t1 t2 = + let rec findrec posn t1 t2 = + let hd1,args1 = whd_betadeltaiota_stack env sigma t1 in + let hd2,args2 = whd_betadeltaiota_stack env sigma t2 in + match (kind_of_term hd1, kind_of_term hd2) with + + | Construct sp1, Construct sp2 + when List.length args1 = mis_constructor_nargs_env env sp1 + -> + (* both sides are fully applied constructors, so either we descend, + or we can discriminate here. *) + if sp1 = sp2 then + List.flatten + (list_map2_i + (fun i arg1 arg2 -> + findrec ((sp1,i)::posn) arg1 arg2) + 0 args1 args2) + else + raise (DiscrFound(List.rev posn,sp1,sp2)) + + | _ -> + let t1_0 = applist (hd1,args1) + and t2_0 = applist (hd2,args2) in + if is_conv env sigma t1_0 t2_0 then + [] + else + let ty1_0 = get_type_of env sigma t1_0 in + match get_sort_family_of env sigma ty1_0 with + | InSet | InType -> [(List.rev posn,t1_0,t2_0)] + | InProp -> [] + in + (try + Inr(findrec [] t1 t2) + with DiscrFound (path,c1,c2) -> + Inl (path,c1,c2)) + +let discriminable env sigma t1 t2 = + match find_positions env sigma t1 t2 with + | Inl _ -> true + | _ -> false + +(* Once we have found a position, we need to project down to it. If + we are discriminating, then we need to produce False on one of the + branches of the discriminator, and True on the other one. So the + result type of the case-expressions is always Prop. + + If we are injecting, then we need to discover the result-type. + This can be difficult, since the type of the two terms at the + injection-position can be different, and we need to find a + dependent sigma-type which generalizes them both. + + We can get an approximation to the right type to choose by: + + (0) Before beginning, we reserve a patvar for the default + value of the match, to be used in all the bogus branches. + + (1) perform the case-splits, down to the site of the injection. At + each step, we have a term which is the "head" of the next + case-split. At the point when we actually reach the end of our + path, the "head" is the term to return. We compute its type, and + then, backwards, make a sigma-type with every free debruijn + reference in that type. We can be finer, and first do a S(TRONG)NF + on the type, so that we get the fewest number of references + possible. + + (2) This gives us a closed type for the head, which we use for the + types of all the case-splits. + + (3) Now, we can compute the type of one of T1, T2, and then unify + it with the type of the last component of the result-type, and this + will give us the bindings for the other arguments of the tuple. + + *) + +(* The algorithm, then is to perform successive case-splits. We have + the result-type of the case-split, and also the type of that + result-type. We have a "direction" we want to follow, i.e. a + constructor-number, and in all other "directions", we want to juse + use the default-value. + + After doing the case-split, we call the afterfun, with the updated + environment, to produce the term for the desired "direction". + + The assumption is made here that the result-type is not manifestly + functional, so we can just use the length of the branch-type to + know how many lambda's to stick in. + + *) + +(* [descend_then sigma env head dirn] + + returns the number of products introduced, and the environment + which is active, in the body of the case-branch given by [dirn], + along with a continuation, which expects to be fed: + + (1) the value of the body of the branch given by [dirn] + (2) the default-value + + (3) the type of the default-value, which must also be the type of + the body of the [dirn] branch + + the continuation then constructs the case-split. + *) +let descend_then sigma env head dirn = + let IndType (indf,_) as indt = + try find_rectype env sigma (get_type_of env sigma head) + with Not_found -> assert false in + let ind,_ = dest_ind_family indf in + let (mib,mip) = lookup_mind_specif env ind in + let cstr = get_constructors env indf in + let dirn_nlams = cstr.(dirn-1).cs_nargs in + let dirn_env = push_rel_context cstr.(dirn-1).cs_args env in + (dirn_nlams, + dirn_env, + (fun dirnval (dfltval,resty) -> + let arign,_ = get_arity env indf in + let p = it_mkLambda_or_LetIn (lift mip.mind_nrealargs resty) arign in + let build_branch i = + let result = if i = dirn then dirnval else dfltval in + it_mkLambda_or_LetIn_name env result cstr.(i-1).cs_args in + let brl = + List.map build_branch + (interval 1 (Array.length mip.mind_consnames)) in + let ci = make_default_case_info env RegularStyle ind in + mkCase (ci, p, head, Array.of_list brl))) + +(* Now we need to construct the discriminator, given a discriminable + position. This boils down to: + + (1) If the position is directly beneath us, then we need to do a + case-split, with result-type Prop, and stick True and False into + the branches, as is convenient. + + (2) If the position is not directly beneath us, then we need to + call descend_then, to descend one step, and then recursively + construct the discriminator. + + *) + +(* [construct_discriminator env dirn headval] + constructs a case-split on [headval], with the [dirn]-th branch + giving [True], and all the rest giving False. *) + +let construct_discriminator sigma env dirn c sort = + let (IndType(indf,_) as indt) = + try find_rectype env sigma (type_of env sigma c) + with Not_found -> + (* one can find Rel(k) in case of dependent constructors + like T := c : (A:Set)A->T and a discrimination + on (c bool true) = (c bool false) + CP : changed assert false in a more informative error + *) + errorlabstrm "Equality.construct_discriminator" + (str "Cannot discriminate on inductive constructors with + dependent types") in + let (ind,_) = dest_ind_family indf in + let (mib,mip) = lookup_mind_specif env ind in + let arsign,arsort = get_arity env indf in + let (true_0,false_0,sort_0) = build_coq_True(),build_coq_False(),Prop Null in + let p = it_mkLambda_or_LetIn (mkSort sort_0) arsign in + let cstrs = get_constructors env indf in + let build_branch i = + let endpt = if i = dirn then true_0 else false_0 in + it_mkLambda_or_LetIn endpt cstrs.(i-1).cs_args in + let brl = + List.map build_branch(interval 1 (Array.length mip.mind_consnames)) in + let ci = make_default_case_info env RegularStyle ind in + mkCase (ci, p, c, Array.of_list brl) + +let rec build_discriminator sigma env dirn c sort = function + | [] -> construct_discriminator sigma env dirn c sort + | ((sp,cnum),argnum)::l -> + let cty = type_of env sigma c in + let IndType (indf,_) = + try find_rectype env sigma cty with Not_found -> assert false in + let (ind,_) = dest_ind_family indf in + let (mib,mip) = lookup_mind_specif env ind in + let _,arsort = get_arity env indf in + let nparams = mip.mind_nparams in + let (cnum_nlams,cnum_env,kont) = descend_then sigma env c cnum in + let newc = mkRel(cnum_nlams-(argnum-nparams)) in + let subval = build_discriminator sigma cnum_env dirn newc sort l in + kont subval (build_coq_False (),mkSort (Prop Null)) + +let gen_absurdity id gl = + if is_empty_type (clause_type (onHyp id) gl) + then + simplest_elim (mkVar id) gl + else + errorlabstrm "Equality.gen_absurdity" + (str "Not the negation of an equality") + +(* Precondition: eq is leibniz equality + + returns ((eq_elim t t1 P i t2), absurd_term) + where P=[e:t]discriminator + absurd_term=False +*) + +let discrimination_pf e (t,t1,t2) discriminator lbeq gls = + let i = build_coq_I () in + let absurd_term = build_coq_False () in + let eq_elim = build_ind lbeq in + (applist (eq_elim, [t;t1;mkNamedLambda e t discriminator;i;t2]), absurd_term) + +exception NotDiscriminable + +let discr id gls = + let eqn = pf_whd_betadeltaiota gls (pf_get_hyp_typ gls id) in + let sort = pf_type_of gls (pf_concl gls) in + let (lbeq,(t,t1,t2)) = + try find_eq_data_decompose eqn + with PatternMatchingFailure -> + errorlabstrm "discr" (pr_id id ++ str": not a primitive equality here") + in + let sigma = project gls in + let env = pf_env gls in + (match find_positions env sigma t1 t2 with + | Inr _ -> + errorlabstrm "discr" (str" Not a discriminable equality") + | Inl (cpath, (_,dirn), _) -> + let e = pf_get_new_id (id_of_string "ee") gls in + let e_env = push_named (e,None,t) env in + let discriminator = + build_discriminator sigma e_env dirn (mkVar e) sort cpath in + let (indt,_) = find_mrectype env sigma t in + let (pf, absurd_term) = + discrimination_pf e (t,t1,t2) discriminator lbeq gls + in + tclCOMPLETE((tclTHENS (cut_intro absurd_term) + ([onLastHyp gen_absurdity; + refine (mkApp (pf, [| mkVar id |]))]))) gls) + + +let not_found_message id = + (str "The variable" ++ spc () ++ str (string_of_id id) ++ spc () ++ + str" was not found in the current environment") + +let onNegatedEquality tac gls = + if is_matching_not (pf_concl gls) then + (tclTHEN (tclTHEN hnf_in_concl intro) (onLastHyp tac)) gls + else if is_matching_imp_False (pf_concl gls)then + (tclTHEN intro (onLastHyp tac)) gls + else + errorlabstrm "extract_negated_equality_then" + (str"The goal should negate an equality") + + +let discrSimpleClause = function + | None -> onNegatedEquality discr + | Some (id,_,_) -> discr id + +let discrClause = onClauses discrSimpleClause + +let discrEverywhere = + tclORELSE + (Tacticals.tryAllClauses discrSimpleClause) + (fun gls -> + errorlabstrm "DiscrEverywhere" (str" No discriminable equalities")) + +let discr_tac = function + | None -> discrEverywhere + | Some id -> try_intros_until discr id + +let discrConcl gls = discrClause onConcl gls +let discrHyp id gls = discrClause (onHyp id) gls + +(* returns the sigma type (sigS, sigT) with the respective + constructor depending on the sort *) + +let find_sigma_data s = + match s with + | Prop Pos -> build_sigma_set () (* Set *) + | Type _ -> build_sigma_type () (* Type *) + | Prop Null -> error "find_sigma_data" + +(* [make_tuple env sigma (rterm,rty) lind] assumes [lind] is the lesser + index bound in [rty] + + Then we build the term + + [(existS A P (mkRel lind) rterm)] of type [(sigS A P)] + + where [A] is the type of [mkRel lind] and [P] is [\na:A.rty{1/lind}] + *) + +let make_tuple env sigma (rterm,rty) lind = + assert (dependent (mkRel lind) rty); + let {intro = exist_term; typ = sig_term} = + find_sigma_data (get_sort_of env sigma rty) in + let a = type_of env sigma (mkRel lind) in + let (na,_,_) = lookup_rel lind env in + (* We move [lind] to [1] and lift other rels > [lind] by 1 *) + let rty = lift (1-lind) (liftn lind (lind+1) rty) in + (* Now [lind] is [mkRel 1] and we abstract on (na:a) *) + let p = mkLambda (na, a, rty) in + (applist(exist_term,[a;p;(mkRel lind);rterm]), + applist(sig_term,[a;p])) + +(* check that the free-references of the type of [c] are contained in + the free-references of the normal-form of that type. If the normal + form of the type contains fewer references, we want to return that + instead. *) + +let minimal_free_rels env sigma (c,cty) = + let cty_rels = free_rels cty in + let nf_cty = nf_betadeltaiota env sigma cty in + let nf_rels = free_rels nf_cty in + if Intset.subset cty_rels nf_rels then + (cty,cty_rels) + else + (nf_cty,nf_rels) + +(* [sig_clausal_form siglen ty] + + Will explode [siglen] [sigS,sigT ]'s on [ty] (depending on the + type of ty), and return: + + (1) a pattern, with meta-variables in it for various arguments, + which, when the metavariables are replaced with appropriate + terms, will have type [ty] + + (2) an integer, which is the last argument - the one which we just + returned. + + (3) a pattern, for the type of that last meta + + (4) a typing for each patvar + + WARNING: No checking is done to make sure that the + sigS(or sigT)'s are actually there. + - Only homogenious pairs are built i.e. pairs where all the + dependencies are of the same sort + + [sig_clausal_form] proceed as follows: the default tuple is + constructed by taking the tuple-type, exploding the first [tuplen] + [sigS]'s, and replacing at each step the binder in the + right-hand-type by a fresh metavariable. In addition, on the way + back out, we will construct the pattern for the tuple which uses + these meta-vars. + + This gives us a pattern, which we use to match against the type of + [dflt]; if that fails, then against the S(TRONG)NF of that type. If + both fail, then we just cannot construct our tuple. If one of + those succeed, then we can construct our value easily - we just use + the tuple-pattern. + + *) + +let sig_clausal_form env sigma sort_of_ty siglen ty (dFLT,dFLTty) = + let { intro = exist_term } = find_sigma_data sort_of_ty in + let isevars = Evarutil.create_evar_defs sigma in + let rec sigrec_clausal_form siglen p_i = + if siglen = 0 then + if Evarconv.the_conv_x env isevars p_i dFLTty then + (* the_conv_x had a side-effect on isevars *) + dFLT + else + error "Cannot solve an unification problem" + else + let (a,p_i_minus_1) = match whd_beta_stack p_i with + | (_sigS,[a;p]) -> (a,p) + | _ -> anomaly "sig_clausal_form: should be a sigma type" in + let ev = Evarutil.new_isevar isevars env (dummy_loc,InternalHole) + (Evarutil.new_Type ()) in + let rty = beta_applist(p_i_minus_1,[ev]) in + let tuple_tail = sigrec_clausal_form (siglen-1) rty in + match + Instantiate.existential_opt_value (Evarutil.evars_of isevars) + (destEvar ev) + with + | Some w -> applist(exist_term,[a;p_i_minus_1;w;tuple_tail]) + | None -> anomaly "Not enough components to build the dependent tuple" + in + let scf = sigrec_clausal_form siglen ty in + Evarutil.nf_evar (Evarutil.evars_of isevars) scf + +(* The problem is to build a destructor (a generalization of the + predecessor) which, when applied to a term made of constructors + (say [Ci(e1,Cj(e2,Ck(...,term,...),...),...)]), returns a given + subterm of the term (say [term]). + + Let [typ] be the type of [term]. If [term] has no dependencies in + the [e1], [e2], etc, then all is simple. If not, then we need to + encapsulated the dependencies into a dependent tuple in such a way + that the destructor has not a dependent type and rewriting can then + be applied. The destructor has the form + + [e]Cases e of + | ... + | Ci (x1,x2,...) => + Cases x2 of + | ... + | Cj (y1,y2,...) => + Cases y2 of + | ... + | Ck (...,z,...) => z + | ... end + | ... end + | ... end + + and the dependencies is expressed by the fact that [z] has a type + dependent in the x1, y1, ... + + Assume [z] is typed as follows: env |- z:zty + + If [zty] has no dependencies, this is simple. Otherwise, assume + [zty] has free (de Bruijn) variables in,...i1 then the role of + [make_iterated_tuple sigma env (term,typ) (z,zty)] is to build the + tuple + + [existS [xn]Pn Rel(in) .. (existS [x2]P2 Rel(i2) (existS [x1]P1 Rel(i1) z))] + + where P1 is zty[i1/x1], P2 is {x1 | P1[i2/x2]} etc. + + To do this, we find the free (relative) references of the strong NF + of [z]'s type, gather them together in left-to-right order + (i.e. highest-numbered is farthest-left), and construct a big + iterated pair out of it. This only works when the references are + all themselves to members of [Set]s, because we use [sigS] to + construct the tuple. + + Suppose now that our constructed tuple is of length [tuplen]. We + need also to construct a default value for the other branches of + the destructor. As default value, we take a tuple of the form + + [existS [xn]Pn ?n (... existS [x2]P2 ?2 (existS [x1]P1 ?1 term))] + + but for this we have to solve the following unification problem: + + typ = zty[i1/?1;...;in/?n] + + This is done by [sig_clausal_form]. + *) + +let make_iterated_tuple env sigma dflt (z,zty) = + let (zty,rels) = minimal_free_rels env sigma (z,zty) in + let sort_of_zty = get_sort_of env sigma zty in + let sorted_rels = Sort.list (<) (Intset.elements rels) in + let (tuple,tuplety) = + List.fold_left (make_tuple env sigma) (z,zty) sorted_rels + in + assert (closed0 tuplety); + let n = List.length sorted_rels in + let dfltval = sig_clausal_form env sigma sort_of_zty n tuplety dflt in + (tuple,tuplety,dfltval) + +let rec build_injrec sigma env (t1,t2) c = function + | [] -> + make_iterated_tuple env sigma (t1,type_of env sigma t1) + (c,type_of env sigma c) + | ((sp,cnum),argnum)::l -> + let cty = type_of env sigma c in + let (ity,_) = find_mrectype env sigma cty in + let (mib,mip) = lookup_mind_specif env ity in + let nparams = mip.mind_nparams in + let (cnum_nlams,cnum_env,kont) = descend_then sigma env c cnum in + let newc = mkRel(cnum_nlams-(argnum-nparams)) in + let (subval,tuplety,dfltval) = + build_injrec sigma cnum_env (t1,t2) newc l + in + (kont subval (dfltval,tuplety), + tuplety,dfltval) + +let build_injector sigma env (t1,t2) c cpath = + let (injcode,resty,_) = build_injrec sigma env (t1,t2) c cpath in + (injcode,resty) + +let try_delta_expand env sigma t = + let whdt = whd_betadeltaiota env sigma t in + let rec hd_rec c = + match kind_of_term c with + | Construct _ -> whdt + | App (f,_) -> hd_rec f + | Cast (c,_) -> hd_rec c + | _ -> t + in + hd_rec whdt + +(* Given t1=t2 Inj calculates the whd normal forms of t1 and t2 and it + expands then only when the whdnf has a constructor of an inductive type + in hd position, otherwise delta expansion is not done *) + +let inj id gls = + let eqn = pf_whd_betadeltaiota gls (pf_get_hyp_typ gls id) in + let (eq,(t,t1,t2))= + try find_eq_data_decompose eqn + with PatternMatchingFailure -> + errorlabstrm "Inj" (pr_id id ++ str": not a primitive equality here") + in + let sigma = project gls in + let env = pf_env gls in + match find_positions env sigma t1 t2 with + | Inl _ -> + errorlabstrm "Inj" + (str (string_of_id id) ++ + str" is not a projectable equality but a discriminable one") + | Inr [] -> + errorlabstrm "Equality.inj" + (str"Nothing to do, it is an equality between convertible terms") + | Inr posns -> + let e = pf_get_new_id (id_of_string "e") gls in + let e_env = push_named (e,None,t) env in + let injectors = + map_succeed + (fun (cpath,t1_0,t2_0) -> + try + let (injbody,resty) = + build_injector sigma e_env (t1_0,t2_0) (mkVar e) cpath in + let injfun = mkNamedLambda e t injbody in + let _ = type_of env sigma injfun in (injfun,resty) + with e when catchable_exception e -> + (* may fail because ill-typed or because of a Prop argument *) + (* error "find_sigma_data" *) + failwith "caught") + posns + in + if injectors = [] then + errorlabstrm "Equality.inj" + (str "Failed to decompose the equality"); + tclMAP + (fun (injfun,resty) -> + let pf = applist(eq.congr, + [t;resty;injfun; + try_delta_expand env sigma t1; + try_delta_expand env sigma t2; + mkVar id]) + in + let ty = + try pf_nf gls (pf_type_of gls pf) + with + | UserError("refiner__fail",_) -> + errorlabstrm "InjClause" + (str (string_of_id id) ++ str" Not a projectable equality") + in ((tclTHENS (cut ty) ([tclIDTAC;refine pf])))) + injectors + gls + +let injClause = function + | None -> onNegatedEquality inj + | Some id -> try_intros_until inj id + +let injConcl gls = injClause None gls +let injHyp id gls = injClause (Some id) gls + +let decompEqThen ntac id gls = + let eqn = pf_whd_betadeltaiota gls (pf_get_hyp_typ gls id) in + let (lbeq,(t,t1,t2))= find_eq_data_decompose eqn in + let sort = pf_type_of gls (pf_concl gls) in + let sigma = project gls in + let env = pf_env gls in + (match find_positions env sigma t1 t2 with + | Inl (cpath, (_,dirn), _) -> + let e = pf_get_new_id (id_of_string "e") gls in + let e_env = push_named (e,None,t) env in + let discriminator = + build_discriminator sigma e_env dirn (mkVar e) sort cpath in + let (pf, absurd_term) = + discrimination_pf e (t,t1,t2) discriminator lbeq gls in + tclCOMPLETE + ((tclTHENS (cut_intro absurd_term) + ([onLastHyp gen_absurdity; + refine (mkApp (pf, [| mkVar id |]))]))) gls + | Inr [] -> (* Change: do not fail, simplify clear this trivial hyp *) + ntac 0 gls + | Inr posns -> + (let e = pf_get_new_id (id_of_string "e") gls in + let e_env = push_named (e,None,t) env in + let injectors = + map_succeed + (fun (cpath,t1_0,t2_0) -> + let (injbody,resty) = + build_injector sigma e_env (t1_0,t2_0) (mkVar e) cpath in + let injfun = mkNamedLambda e t injbody in + try + let _ = type_of env sigma injfun in (injfun,resty) + with e when catchable_exception e -> failwith "caught") + posns + in + if injectors = [] then + errorlabstrm "Equality.decompEqThen" + (str "Discriminate failed to decompose the equality"); + (tclTHEN + (tclMAP (fun (injfun,resty) -> + let pf = applist(lbeq.congr, + [t;resty;injfun;t1;t2; + mkVar id]) in + let ty = pf_nf gls (pf_type_of gls pf) in + ((tclTHENS (cut ty) + ([tclIDTAC;refine pf])))) + (List.rev injectors)) + (ntac (List.length injectors))) + gls)) + +let decompEq = decompEqThen (fun x -> tclIDTAC) + +let dEqThen ntac = function + | None -> onNegatedEquality (decompEqThen ntac) + | Some id -> try_intros_until (decompEqThen ntac) id + +let dEq = dEqThen (fun x -> tclIDTAC) + +let dEqConcl gls = dEq None gls +let dEqHyp id gls = dEq (Some id) gls + +let rewrite_msg = function + | None -> str "passed term is not a primitive equality" + | Some id -> pr_id id ++ str "does not satisfy preconditions " + +let swap_equands gls eqn = + let (lbeq,(t,e1,e2)) = find_eq_data_decompose eqn in + applist(lbeq.eq,[t;e2;e1]) + +let swapEquandsInConcl gls = + let (lbeq,(t,e1,e2)) = find_eq_data_decompose (pf_concl gls) in + let sym_equal = lbeq.sym in + refine (applist(sym_equal,[t;e2;e1;mkMeta (Clenv.new_meta())])) gls + +let swapEquandsInHyp id gls = + ((tclTHENS (cut_replacing id (swap_equands gls (pf_get_hyp_typ gls id))) + ([tclIDTAC; + (tclTHEN (swapEquandsInConcl) (exact_no_check (mkVar id)))]))) gls + +(* find_elim determines which elimination principle is necessary to + eliminate lbeq on sort_of_gl. It yields the boolean true wether + it is a dependent elimination principle (as idT.rect) and false + otherwise *) + +let find_elim sort_of_gl lbeq = + match kind_of_term sort_of_gl with + | Sort(Prop Null) (* Prop *) -> (lbeq.ind, false) + | Sort(Prop Pos) (* Set *) -> + (match lbeq.rrec with + | Some eq_rec -> (eq_rec, false) + | None -> errorlabstrm "find_elim" + (str "this type of elimination is not allowed")) + | _ (* Type *) -> + (match lbeq.rect with + | Some eq_rect -> (eq_rect, true) + | None -> errorlabstrm "find_elim" + (str "this type of elimination is not allowed")) + +(* builds a predicate [e:t][H:(lbeq t e t1)](body e) + to be used as an argument for equality dependent elimination principle: + Preconditon: dependent body (mkRel 1) *) + +let build_dependent_rewrite_predicate (t,t1,t2) body lbeq gls = + let e = pf_get_new_id (id_of_string "e") gls in + let h = pf_get_new_id (id_of_string "HH") gls in + let eq_term = lbeq.eq in + (mkNamedLambda e t + (mkNamedLambda h (applist (eq_term, [t;t1;(mkRel 1)])) + (lift 1 body))) + +(* builds a predicate [e:t](body e) ??? + to be used as an argument for equality non-dependent elimination principle: + Preconditon: dependent body (mkRel 1) *) + +let build_non_dependent_rewrite_predicate (t,t1,t2) body gls = + lambda_create (pf_env gls) (t,body) + +let bareRevSubstInConcl lbeq body (t,e1,e2) gls = + let (eq_elim,dep) = + try + find_elim (pf_type_of gls (pf_concl gls)) lbeq + with e when catchable_exception e -> + errorlabstrm "RevSubstIncConcl" + (str "this type of substitution is not allowed") + in + let p = + if dep then + (build_dependent_rewrite_predicate (t,e1,e2) body lbeq gls) + else + (build_non_dependent_rewrite_predicate (t,e1,e2) body gls) + in + refine (applist(eq_elim,[t;e1;p;mkMeta(Clenv.new_meta()); + e2;mkMeta(Clenv.new_meta())])) gls + +(* [subst_tuple_term dep_pair B] + + Given that dep_pair looks like: + + (existS e1 (existS e2 ... (existS en en+1) ... )) + + and B might contain instances of the ei, we will return the term: + + ([x1:ty(e1)]...[xn:ty(en)]B + (projS1 (mkRel 1)) + (projS1 (projS2 (mkRel 1))) + ... etc ...) + + That is, we will abstract out the terms e1...en+1 as usual, but + will then produce a term in which the abstraction is on a single + term - the debruijn index [mkRel 1], which will be of the same type + as dep_pair. + + ALGORITHM for abstraction: + + We have a list of terms, [e1]...[en+1], which we want to abstract + out of [B]. For each term [ei], going backwards from [n+1], we + just do a [subst_term], and then do a lambda-abstraction to the + type of the [ei]. + + *) + +let decomp_tuple_term env c t = + let rec decomprec inner_code ex exty = + try + let {proj1 = p1; proj2 = p2 },(a,p,car,cdr) = + find_sigma_data_decompose ex in + let car_code = applist (p1,[a;p;inner_code]) + and cdr_code = applist (p2,[a;p;inner_code]) in + let cdrtyp = beta_applist (p,[car]) in + ((car,a),car_code)::(decomprec cdr_code cdr cdrtyp) + with PatternMatchingFailure -> + [((ex,exty),inner_code)] + in + List.split (decomprec (mkRel 1) c t) + +let subst_tuple_term env sigma dep_pair b = + let typ = get_type_of env sigma dep_pair in + let e_list,proj_list = decomp_tuple_term env dep_pair typ in + let abst_B = + List.fold_right + (fun (e,t) body -> lambda_create env (t,subst_term e body)) e_list b in + let app_B = applist(abst_B,proj_list) in app_B + +(* |- (P e2) + BY RevSubstInConcl (eq T e1 e2) + |- (P e1) + |- (eq T e1 e2) + *) +(* Redondant avec Replace ! *) + +let substInConcl_RL eqn gls = + let (lbeq,(t,e1,e2)) = find_eq_data_decompose eqn in + let body = subst_tuple_term (pf_env gls) (project gls) e2 (pf_concl gls) in + assert (dependent (mkRel 1) body); + bareRevSubstInConcl lbeq body (t,e1,e2) gls + +(* |- (P e1) + BY SubstInConcl (eq T e1 e2) + |- (P e2) + |- (eq T e1 e2) + *) +let substInConcl_LR eqn gls = + (tclTHENS (substInConcl_RL (swap_equands gls eqn)) + ([tclIDTAC; + swapEquandsInConcl])) gls + +let substInConcl l2r = if l2r then substInConcl_LR else substInConcl_RL + +let substInHyp_LR eqn id gls = + let (lbeq,(t,e1,e2)) = find_eq_data_decompose eqn in + let body = subst_term e1 (pf_get_hyp_typ gls id) in + if not (dependent (mkRel 1) body) then errorlabstrm "SubstInHyp" (mt ()); + (tclTHENS (cut_replacing id (subst1 e2 body)) + ([tclIDTAC; + (tclTHENS (bareRevSubstInConcl lbeq body (t,e1,e2)) + ([exact_no_check (mkVar id);tclIDTAC]))])) gls + +let substInHyp_RL eqn id gls = + (tclTHENS (substInHyp_LR (swap_equands gls eqn) id) + ([tclIDTAC; + swapEquandsInConcl])) gls + +let substInHyp l2r = if l2r then substInHyp_LR else substInHyp_RL + +let try_rewrite tac gls = + try + tac gls + with + | PatternMatchingFailure -> + errorlabstrm "try_rewrite" (str "Not a primitive equality here") + | e when catchable_exception e -> + errorlabstrm "try_rewrite" + (str "Cannot find a well-typed generalization of the goal that" ++ + str " makes the proof progress") + +let subst l2r eqn cls gls = + match cls with + | None -> substInConcl l2r eqn gls + | Some id -> substInHyp l2r eqn id gls + +(* |- (P a) + * SubstConcl_LR a=b + * |- (P b) + * |- a=b + *) + +let substConcl l2r eqn gls = try_rewrite (subst l2r eqn None) gls +let substConcl_LR = substConcl true + +(* id:(P a) |- G + * SubstHyp a=b id + * id:(P b) |- G + * id:(P a) |-a=b +*) + +let hypSubst l2r id cls gls = + onClauses (function + | None -> + (tclTHENS (substInConcl l2r (pf_get_hyp_typ gls id)) + ([tclIDTAC; exact_no_check (mkVar id)])) + | Some (hypid,_,_) -> + (tclTHENS (substInHyp l2r (pf_get_hyp_typ gls id) hypid) + ([tclIDTAC;exact_no_check (mkVar id)]))) + cls gls + +let hypSubst_LR = hypSubst true + +(* id:a=b |- (P a) + * HypSubst id. + * id:a=b |- (P b) + *) +let substHypInConcl l2r id gls = try_rewrite (hypSubst l2r id onConcl) gls +let substHypInConcl_LR = substHypInConcl true + +(* id:a=b H:(P a) |- G + SubstHypInHyp id H. + id:a=b H:(P b) |- G +*) +(* |- (P b) + SubstConcl_RL a=b + |- (P a) + |- a=b +*) +let substConcl_RL = substConcl false + +(* id:(P b) |-G + SubstHyp_RL a=b id + id:(P a) |- G + |- a=b +*) +let substHyp l2r eqn id gls = try_rewrite (subst l2r eqn (Some id)) gls +let substHyp_RL = substHyp false + +let hypSubst_RL = hypSubst false + +(* id:a=b |- (P b) + * HypSubst id. + * id:a=b |- (P a) + *) +let substHypInConcl_RL = substHypInConcl false + +(* id:a=b H:(P b) |- G + SubstHypInHyp id H. + id:a=b H:(P a) |- G +*) + +(* Substitutions tactics (JCF) *) + +let unfold_body x gl = + let hyps = pf_hyps gl in + let xval = + match Sign.lookup_named x hyps with + (_,Some xval,_) -> xval + | _ -> errorlabstrm "unfold_body" + (pr_id x ++ str" is not a defined hypothesis") in + let aft = afterHyp x gl in + let hl = List.fold_right + (fun (y,yval,_) cl -> (y,[],(InHyp,ref None)) :: cl) aft [] in + let xvar = mkVar x in + let rfun _ _ c = replace_term xvar xval c in + tclTHENLIST + [tclMAP (fun h -> reduct_in_hyp rfun h) hl; + reduct_in_concl rfun] gl + + + + +exception FoundHyp of (identifier * constr * bool) + +(* tests whether hyp [c] is [x = t] or [t = x], [x] not occuring in [t] *) +let is_eq_x x (id,_,c) = + try + let (_,lhs,rhs) = snd (find_eq_data_decompose c) in + if (x = lhs) && not (occur_term x rhs) then raise (FoundHyp (id,rhs,true)); + if (x = rhs) && not (occur_term x lhs) then raise (FoundHyp (id,lhs,false)) + with PatternMatchingFailure -> + () + +let subst_one x gl = + let hyps = pf_hyps gl in + let (_,xval,_) = pf_get_hyp gl x in + (* If x has a body, simply replace x with body and clear x *) + if xval <> None then tclTHEN (unfold_body x) (clear [x]) gl else + (* x is a variable: *) + let varx = mkVar x in + (* Find a non-recursive definition for x *) + let (hyp,rhs,dir) = + try + let test hyp _ = is_eq_x varx hyp in + Sign.fold_named_context test ~init:() hyps; + errorlabstrm "Subst" + (str "cannot find any non-recursive equality over " ++ pr_id x) + with FoundHyp res -> res + in + (* The set of hypotheses using x *) + let depdecls = + let test (id,_,c as dcl) = + if id <> hyp && occur_var_in_decl (pf_env gl) x dcl then dcl + else failwith "caught" in + List.rev (map_succeed test hyps) in + let dephyps = List.map (fun (id,_,_) -> id) depdecls in + (* Decides if x appears in conclusion *) + let depconcl = occur_var (pf_env gl) x (pf_concl gl) in + (* The set of non-defined hypothesis: they must be abstracted, + rewritten and reintroduced *) + let abshyps = + map_succeed + (fun (id,v,_) -> if v=None then mkVar id else failwith "caught") + depdecls in + (* a tactic that either introduce an abstracted and rewritten hyp, + or introduce a definition where x was replaced *) + let introtac = function + (id,None,_) -> intro_using id + | (id,Some hval,htyp) -> + forward true (Name id) (mkCast(replace_term varx rhs hval, + replace_term varx rhs htyp)) in + let need_rewrite = dephyps <> [] || depconcl in + tclTHENLIST + ((if need_rewrite then + [generalize abshyps; + (if dir then rewriteLR else rewriteRL) (mkVar hyp); + thin dephyps; + tclMAP introtac depdecls] + else + [thin dephyps; + tclMAP introtac depdecls]) @ + [tclTRY (clear [x;hyp])]) gl + +let subst = tclMAP subst_one + +let subst_all gl = + let test (_,c) = + try + let (_,x,y) = snd (find_eq_data_decompose c) in + match kind_of_term x with Var x -> x | _ -> + match kind_of_term y with Var y -> y | _ -> failwith "caught" + with PatternMatchingFailure -> failwith "caught" + in + let ids = map_succeed test (pf_hyps_types gl) in + let ids = list_uniquize ids in + subst ids gl + +(* Rewrite the first assumption for which the condition faildir does not fail + and gives the direction of the rewrite *) + +let rewrite_assumption_cond faildir gl = + let rec arec = function + | [] -> error "No such assumption" + | (id,_,t)::rest -> + (try let dir = faildir t gl in + general_rewrite dir (mkVar id) gl + with Failure _ | UserError _ -> arec rest) + in arec (pf_hyps gl) + + +let rewrite_assumption_cond_in faildir hyp gl = + let rec arec = function + | [] -> error "No such assumption" + | (id,_,t)::rest -> + (try let dir = faildir t gl in + general_rewrite_in dir hyp ((mkVar id),NoBindings) gl + with Failure _ | UserError _ -> arec rest) + in arec (pf_hyps gl) + +let cond_eq_term_left c t gl = + try + let (_,x,_) = snd (find_eq_data_decompose t) in + if pf_conv_x gl c x then true else failwith "not convertible" + with PatternMatchingFailure -> failwith "not an equality" + +let cond_eq_term_right c t gl = + try + let (_,_,x) = snd (find_eq_data_decompose t) in + if pf_conv_x gl c x then false else failwith "not convertible" + with PatternMatchingFailure -> failwith "not an equality" + +let cond_eq_term c t gl = + try + let (_,x,y) = snd (find_eq_data_decompose t) in + if pf_conv_x gl c x then true + else if pf_conv_x gl c y then false + else failwith "not convertible" + with PatternMatchingFailure -> failwith "not an equality" + +let replace_term_left t = rewrite_assumption_cond (cond_eq_term_left t) + +let replace_term_right t = rewrite_assumption_cond (cond_eq_term_right t) + +let replace_term t = rewrite_assumption_cond (cond_eq_term t) + +let replace_term_in_left t = rewrite_assumption_cond_in (cond_eq_term_left t) + +let replace_term_in_right t = rewrite_assumption_cond_in (cond_eq_term_right t) + +let replace_term_in t = rewrite_assumption_cond_in (cond_eq_term t) diff --git a/tactics/equality.mli b/tactics/equality.mli new file mode 100644 index 00000000..ab439c39 --- /dev/null +++ b/tactics/equality.mli @@ -0,0 +1,83 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* sorts -> constr + +val general_rewrite_bindings : bool -> constr with_bindings -> tactic +val general_rewrite : bool -> constr -> tactic +val rewriteLR_bindings : constr with_bindings -> tactic +val rewriteRL_bindings : constr with_bindings -> tactic + +val rewriteLR : constr -> tactic +val rewriteRL : constr -> tactic + +val conditional_rewrite : bool -> tactic -> constr with_bindings -> tactic +val general_rewrite_in : bool -> identifier -> constr with_bindings -> tactic +val conditional_rewrite_in : + bool -> identifier -> tactic -> constr with_bindings -> tactic + +val replace : constr -> constr -> tactic +val replace_in : identifier -> constr -> constr -> tactic + +val discr : identifier -> tactic +val discrConcl : tactic +val discrClause : clause -> tactic +val discrHyp : identifier -> tactic +val discrEverywhere : tactic +val discr_tac : quantified_hypothesis option -> tactic +val inj : identifier -> tactic +val injClause : quantified_hypothesis option -> tactic + +val dEq : quantified_hypothesis option -> tactic +val dEqThen : (int -> tactic) -> quantified_hypothesis option -> tactic + +val make_iterated_tuple : + env -> evar_map -> (constr * constr) -> (constr * constr) + -> constr * constr * constr + +val substHypInConcl : bool -> identifier -> tactic +val substConcl : bool -> constr -> tactic +val substHyp : bool -> constr -> identifier -> tactic + +val hypSubst_LR : identifier -> clause -> tactic +val hypSubst_RL : identifier -> clause -> tactic + +val discriminable : env -> evar_map -> constr -> constr -> bool + +(* Subst *) + +val unfold_body : identifier -> tactic + +val subst : identifier list -> tactic +val subst_all : tactic + +(* Replace term *) +val replace_term_left : constr -> tactic +val replace_term_right : constr -> tactic +val replace_term : constr -> tactic +val replace_term_in_left : constr -> identifier -> tactic +val replace_term_in_right : constr -> identifier -> tactic +val replace_term_in : constr -> identifier -> tactic diff --git a/tactics/extraargs.ml4 b/tactics/extraargs.ml4 new file mode 100644 index 00000000..34348834 --- /dev/null +++ b/tactics/extraargs.ml4 @@ -0,0 +1,31 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* " + +let pr_orient _prc _prt = function + | true -> Pp.mt () + | false -> Pp.str " <-" + +ARGUMENT EXTEND orient TYPED AS bool PRINTED BY pr_orient +| [ "->" ] -> [ true ] +| [ "<-" ] -> [ false ] +| [ ] -> [ true ] +END + diff --git a/tactics/extraargs.mli b/tactics/extraargs.mli new file mode 100644 index 00000000..60a1ddc5 --- /dev/null +++ b/tactics/extraargs.mli @@ -0,0 +1,18 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* [general_rewrite_bindings b c] +END + +TACTIC EXTEND RewriteIn + [ "Rewrite" orient(b) constr_with_bindings(c) "in" hyp(h) ] -> + [general_rewrite_in b h c] +END + +let h_rewriteLR x = h_rewrite true (x,Rawterm.NoBindings) + +TACTIC EXTEND Replace + [ "Replace" constr(c1) "with" constr(c2) ] -> [ replace c1 c2 ] +END + +TACTIC EXTEND ReplaceIn + [ "Replace" constr(c1) "with" constr(c2) "in" hyp(h) ] -> + [ replace_in h c1 c2 ] +END + +TACTIC EXTEND Replacetermleft + [ "Replace" "->" constr(c) ] -> [ replace_term_left c ] +END + +TACTIC EXTEND Replacetermright + [ "Replace" "<-" constr(c) ] -> [ replace_term_right c ] +END + +TACTIC EXTEND Replaceterm + [ "Replace" constr(c) ] -> [ replace_term c ] +END + +TACTIC EXTEND ReplacetermInleft + [ "Replace" "->" constr(c) "in" hyp(h) ] + -> [ replace_term_in_left c h ] +END + +TACTIC EXTEND ReplacetermInright + [ "Replace" "<-" constr(c) "in" hyp(h) ] + -> [ replace_term_in_right c h ] +END + +TACTIC EXTEND ReplacetermIn + [ "Replace" constr(c) "in" hyp(h) ] + -> [ replace_term_in c h ] +END + +TACTIC EXTEND DEq + [ "Simplify_eq" quantified_hypothesis_opt(h) ] -> [ dEq h ] +END + +TACTIC EXTEND Discriminate + [ "Discriminate" quantified_hypothesis_opt(h) ] -> [ discr_tac h ] +END + +let h_discrHyp id = h_discriminate (Some id) + +TACTIC EXTEND Injection + [ "Injection" quantified_hypothesis_opt(h) ] -> [ injClause h ] +END + +let h_injHyp id = h_injection (Some id) + +TACTIC EXTEND ConditionalRewrite + [ "Conditional" tactic(tac) "Rewrite" orient(b) constr_with_bindings(c) ] + -> [ conditional_rewrite b (snd tac) c ] +END + +TACTIC EXTEND ConditionalRewriteIn + [ "Conditional" tactic(tac) "Rewrite" orient(b) constr_with_bindings(c) + "in" hyp(h) ] + -> [ conditional_rewrite_in b h (snd tac) c ] +END + +TACTIC EXTEND DependentRewrite +| [ "Dependent" "Rewrite" orient(b) hyp(id) ] -> [ substHypInConcl b id ] +| [ "CutRewrite" orient(b) constr(eqn) ] -> [ substConcl b eqn ] +| [ "CutRewrite" orient(b) constr(eqn) "in" hyp(id) ] + -> [ substHyp b eqn id ] +END + +(* Contradiction *) +open Contradiction + +TACTIC EXTEND Absurd + [ "Absurd" constr(c) ] -> [ absurd c ] +END + +TACTIC EXTEND Contradiction + [ "Contradiction" constr_with_bindings_opt(c) ] -> [ contradiction c ] +END + +(* AutoRewrite *) + +open Autorewrite +TACTIC EXTEND AutorewriteV7 + [ "AutoRewrite" "[" ne_preident_list(l) "]" ] -> + [ autorewrite Refiner.tclIDTAC l ] +| [ "AutoRewrite" "[" ne_preident_list(l) "]" "using" tactic(t) ] -> + [ autorewrite (snd t) l ] +END +TACTIC EXTEND AutorewriteV8 + [ "AutoRewrite" "with" ne_preident_list(l) ] -> + [ autorewrite Refiner.tclIDTAC l ] +| [ "AutoRewrite" "with" ne_preident_list(l) "using" tactic(t) ] -> + [ autorewrite (snd t) l ] +END + +let add_rewrite_hint name ort t lcsr = + let env = Global.env() and sigma = Evd.empty in + let f c = Constrintern.interp_constr sigma env c, ort, t in + add_rew_rules name (List.map f lcsr) + +(* V7 *) +VERNAC COMMAND EXTEND HintRewriteV7 + [ "Hint" "Rewrite" orient(o) "[" ne_constr_list(l) "]" "in" preident(b) ] -> + [ add_rewrite_hint b o (Tacexpr.TacId "") l ] +| [ "Hint" "Rewrite" orient(o) "[" ne_constr_list(l) "]" "in" preident(b) + "using" tactic(t) ] -> + [ add_rewrite_hint b o t l ] +END + +(* V8 *) +VERNAC COMMAND EXTEND HintRewriteV8 + [ "Hint" "Rewrite" orient(o) ne_constr_list(l) ":" preident(b) ] -> + [ add_rewrite_hint b o (Tacexpr.TacId "") l ] +| [ "Hint" "Rewrite" orient(o) ne_constr_list(l) "using" tactic(t) + ":" preident(b) ] -> + [ add_rewrite_hint b o t l ] +END + + +(* Refine *) + +open Refine + +TACTIC EXTEND Refine + [ "Refine" castedopenconstr(c) ] -> [ refine c ] +END + +let refine_tac = h_refine + +(* Setoid_replace *) + +open Setoid_replace + +TACTIC EXTEND SetoidReplace + [ "Setoid_replace" constr(c1) "with" constr(c2) ] + -> [ setoid_replace c1 c2 None] +END + +TACTIC EXTEND SetoidRewrite + [ "Setoid_rewrite" orient(b) constr(c) ] -> [ general_s_rewrite b c ] +END + +VERNAC COMMAND EXTEND AddSetoid +| [ "Add" "Setoid" constr(a) constr(aeq) constr(t) ] -> [ add_setoid a aeq t ] +| [ "Add" "Morphism" constr(m) ":" ident(s) ] -> [ new_named_morphism s m ] +END + +(* Inversion lemmas (Leminv) *) + +open Inv +open Leminv + +VERNAC COMMAND EXTEND DeriveInversionClear + [ "Derive" "Inversion_clear" ident(na) hyp(id) ] + -> [ inversion_lemma_from_goal 1 na id Term.mk_Prop false inv_clear_tac ] + +| [ "Derive" "Inversion_clear" natural(n) ident(na) hyp(id) ] + -> [ inversion_lemma_from_goal n na id Term.mk_Prop false inv_clear_tac ] + +| [ "Derive" "Inversion_clear" ident(na) "with" constr(c) "Sort" sort(s) ] + -> [ add_inversion_lemma_exn na c s false inv_clear_tac ] + +| [ "Derive" "Inversion_clear" ident(na) "with" constr(c) ] + -> [ add_inversion_lemma_exn na c (Rawterm.RProp Term.Null) false inv_clear_tac ] +END + +open Term +open Rawterm + +VERNAC COMMAND EXTEND DeriveInversion +| [ "Derive" "Inversion" ident(na) "with" constr(c) "Sort" sort(s) ] + -> [ add_inversion_lemma_exn na c s false half_inv_tac ] + +| [ "Derive" "Inversion" ident(na) "with" constr(c) ] + -> [ add_inversion_lemma_exn na c (RProp Null) false half_inv_tac ] + +| [ "Derive" "Inversion" ident(na) hyp(id) ] + -> [ inversion_lemma_from_goal 1 na id Term.mk_Prop false half_inv_tac ] + +| [ "Derive" "Inversion" natural(n) ident(na) hyp(id) ] + -> [ inversion_lemma_from_goal n na id Term.mk_Prop false half_inv_tac ] +END + +VERNAC COMMAND EXTEND DeriveDependentInversion +| [ "Derive" "Dependent" "Inversion" ident(na) "with" constr(c) "Sort" sort(s) ] + -> [ add_inversion_lemma_exn na c s true half_dinv_tac ] + END + +VERNAC COMMAND EXTEND DeriveDependentInversionClear +| [ "Derive" "Dependent" "Inversion_clear" ident(na) "with" constr(c) "Sort" sort(s) ] + -> [ add_inversion_lemma_exn na c s true dinv_clear_tac ] +END + +(* Subst *) + +TACTIC EXTEND Subst +| [ "Subst" ne_var_list(l) ] -> [ subst l ] +| [ "Subst" ] -> [ subst_all ] +END + +(** Nijmegen "step" tactic for setoid rewriting *) + +open Tacticals +open Tactics +open Tactics +open Libnames +open Rawterm +open Summary +open Libobject +open Lib + +(* Registered lemmas are expected to be of the form + x R y -> y == z -> x R z (in the right table) + x R y -> x == z -> z R y (in the left table) +*) + +let transitivity_right_table = ref [] +let transitivity_left_table = ref [] + +(* [step] tries to apply a rewriting lemma; then apply [tac] intended to + complete to proof of the last hypothesis (assumed to state an equality) *) + +let step left x tac = + let l = + List.map (fun lem -> + tclTHENLAST + (apply_with_bindings (constr_of_reference lem, ImplicitBindings [x])) + tac) + !(if left then transitivity_left_table else transitivity_right_table) + in + tclFIRST l + +(* Main function to push lemmas in persistent environment *) + +let cache_transitivity_lemma (_,(left,lem)) = + if left then + transitivity_left_table := lem :: !transitivity_left_table + else + transitivity_right_table := lem :: !transitivity_right_table + +let subst_transitivity_lemma (_,subst,(b,ref)) = (b,subst_global subst ref) + +let (inTransitivity,_) = + declare_object {(default_object "TRANSITIVITY-STEPS") with + cache_function = cache_transitivity_lemma; + open_function = (fun i o -> if i=1 then cache_transitivity_lemma o); + subst_function = subst_transitivity_lemma; + classify_function = (fun (_,o) -> Substitute o); + export_function = (fun x -> Some x) } + +(* Synchronisation with reset *) + +let freeze () = !transitivity_left_table, !transitivity_right_table + +let unfreeze (l,r) = + transitivity_left_table := l; + transitivity_right_table := r + +let init () = + transitivity_left_table := []; + transitivity_right_table := [] + +let _ = + declare_summary "transitivity-steps" + { freeze_function = freeze; + unfreeze_function = unfreeze; + init_function = init; + survive_module = false; + survive_section = false } + +(* Main entry points *) + +let add_transitivity_lemma left ref = + add_anonymous_leaf (inTransitivity (left,Nametab.global ref)) + +(* Vernacular syntax *) + +TACTIC EXTEND Stepl +| ["Stepl" constr(c) "by" tactic(tac) ] -> [ step true c (snd tac) ] +| ["Stepl" constr(c) ] -> [ step true c tclIDTAC ] +END + +TACTIC EXTEND Stepr +| ["Stepr" constr(c) "by" tactic(tac) ] -> [ step false c (snd tac) ] +| ["Stepr" constr(c) ] -> [ step false c tclIDTAC ] +END + +VERNAC COMMAND EXTEND AddStepl +| [ "Declare" "Left" "Step" global(id) ] -> + [ add_transitivity_lemma true id ] +END + +VERNAC COMMAND EXTEND AddStepr +| [ "Declare" "Right" "Step" global(id) ] -> + [ add_transitivity_lemma false id ] +END diff --git a/tactics/extratactics.mli b/tactics/extratactics.mli new file mode 100644 index 00000000..a714c8dd --- /dev/null +++ b/tactics/extratactics.mli @@ -0,0 +1,20 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* tactic +val h_injHyp : quantified_hypothesis -> tactic +val h_rewriteLR : constr -> tactic + +val refine_tac : Genarg.open_constr -> tactic diff --git a/tactics/hiddentac.ml b/tactics/hiddentac.ml new file mode 100644 index 00000000..f35c624b --- /dev/null +++ b/tactics/hiddentac.ml @@ -0,0 +1,103 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* identifier option -> tactic +val h_intro : identifier -> tactic +val h_intros_until : quantified_hypothesis -> tactic + +val h_assumption : tactic +val h_exact : constr -> tactic + +val h_apply : constr with_bindings -> tactic + +val h_elim : constr with_bindings -> + constr with_bindings option -> tactic +val h_elim_type : constr -> tactic +val h_case : constr with_bindings -> tactic +val h_case_type : constr -> tactic + +val h_mutual_fix : identifier -> int -> + (identifier * int * constr) list -> tactic +val h_fix : identifier option -> int -> tactic +val h_mutual_cofix : identifier -> (identifier * constr) list -> tactic +val h_cofix : identifier option -> tactic + +val h_cut : constr -> tactic +val h_true_cut : name -> constr -> tactic +val h_generalize : constr list -> tactic +val h_generalize_dep : constr -> tactic +val h_forward : bool -> name -> constr -> tactic +val h_let_tac : name -> constr -> Tacticals.clause -> tactic +val h_instantiate : int -> constr -> Tacticals.clause -> tactic + +(* Derived basic tactics *) + +val h_simple_induction : quantified_hypothesis * (bool ref * intro_pattern_expr list ref list) list ref -> tactic +val h_simple_destruct : quantified_hypothesis -> tactic +val h_new_induction : + constr induction_arg -> constr with_bindings option -> + intro_pattern_expr option * (bool ref * intro_pattern_expr list ref list) list ref + -> tactic +val h_new_destruct : + constr induction_arg -> constr with_bindings option -> + intro_pattern_expr option * (bool ref * intro_pattern_expr list ref list) list ref + -> tactic +val h_specialize : int option -> constr with_bindings -> tactic +val h_lapply : constr -> tactic + +(* Automation tactic : see Auto *) + + +(* Context management *) +val h_clear : identifier list -> tactic +val h_clear_body : identifier list -> tactic +val h_move : bool -> identifier -> identifier -> tactic +val h_rename : identifier -> identifier -> tactic + + +(* Constructors *) +(* +val h_any_constructor : tactic -> tactic +*) +val h_constructor : int -> constr bindings -> tactic +val h_left : constr bindings -> tactic +val h_right : constr bindings -> tactic +val h_split : constr bindings -> tactic + +val h_one_constructor : int -> tactic +val h_simplest_left : tactic +val h_simplest_right : tactic + + +(* Conversion *) +val h_reduce : Tacred.red_expr -> Tacticals.clause -> tactic +val h_change : + constr occurrences option -> constr -> Tacticals.clause -> tactic + +(* Equivalence relations *) +val h_reflexivity : tactic +val h_symmetry : Tacticals.clause -> tactic +val h_transitivity : constr -> tactic + +val h_simplest_apply : constr -> tactic +val h_simplest_elim : constr -> tactic +val h_simplest_case : constr -> tactic + +val h_intro_patterns : intro_pattern_expr list -> tactic diff --git a/tactics/hipattern.ml b/tactics/hipattern.ml new file mode 100644 index 00000000..0ada5a06 --- /dev/null +++ b/tactics/hipattern.ml @@ -0,0 +1,366 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* 'a option + +type testing_function = constr -> bool + +let mkmeta n = Nameops.make_ident "X" (Some n) +let mkPMeta n = PMeta (Some (mkmeta n)) +let meta1 = mkmeta 1 +let meta2 = mkmeta 2 +let meta3 = mkmeta 3 +let meta4 = mkmeta 4 + +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 (mkPMeta 1) (mkPMeta 2) +let match_arrow_pattern t = + match matches coq_arrow_pattern t with + | [(m1,arg);(m2,mind)] -> assert (m1=meta1 & m2=meta2); (arg, mind) + | _ -> anomaly "Incorrect pattern matching" + +let match_with_nottype t = + try + let (arg,mind) = match_arrow_pattern t in + if is_empty_type mind then Some (mind,arg) else None + with PatternMatchingFailure -> None + +let is_nottype t = op2bool (match_with_nottype t) + +let match_with_forall_term c= + match kind_of_term c with + | Prod (nam,a,b) -> Some (nam,a,b) + | _ -> None + +let is_forall_term c = op2bool (match_with_forall_term c) + +let match_with_imp_term c= + match kind_of_term c with + | Prod (_,a,b) when not (dependent (mkRel 1) b) ->Some (a,b) + | _ -> None + +let is_imp_term c = op2bool (match_with_imp_term c) + +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 + if Array.length (mib.mind_packets)>1 then None else + let nodep_constr = has_nodep_prod_after mip.mind_nparams in + if array_for_all nodep_constr mip.mind_nf_lc then + let params= + if mip.mind_nrealargs=0 then args else + fst (list_chop mip.mind_nparams args) in + Some (hdapp,params,mip.mind_nrealargs) + else + None + | _ -> None + +let is_nodep_ind t=op2bool (match_with_nodep_ind t) + +let match_with_sigma_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 + if (Array.length (mib.mind_packets)=1) && + (mip.mind_nrealargs=0) && + (Array.length mip.mind_consnames=1) && + has_nodep_prod_after (mip.mind_nparams+1) mip.mind_nf_lc.(0) then + (*allowing only 1 existential*) + Some (hdapp,args) + else + None + | _ -> None + +let is_sigma_type t=op2bool (match_with_sigma_type t) + +(***** Destructing patterns bound to some theory *) + +let rec first_match matcher = function + | [] -> raise PatternMatchingFailure + | (pat,build_set)::l -> + try (build_set (),matcher pat) + with PatternMatchingFailure -> first_match matcher l + +(*** Equality *) + +(* Patterns "(eq ?1 ?2 ?3)", "(eqT ?1 ?2 ?3)" and "(idT ?1 ?2 ?3)" *) +let coq_eq_pattern_gen eq = + lazy (PApp(PRef (Lazy.force eq), [|mkPMeta 1;mkPMeta 2;mkPMeta 3|])) +let coq_eq_pattern = coq_eq_pattern_gen coq_eq_ref +(*let coq_eqT_pattern = coq_eq_pattern_gen coq_eqT_ref*) +let coq_idT_pattern = coq_eq_pattern_gen coq_idT_ref + +let match_eq eqn eq_pat = + match matches (Lazy.force eq_pat) eqn with + | [(m1,t);(m2,x);(m3,y)] -> + assert (m1 = meta1 & m2 = meta2 & m3 = meta3); + (t,x,y) + | _ -> anomaly "match_eq: an eq pattern should match 3 terms" + +let equalities = + [coq_eq_pattern, build_coq_eq_data; +(* coq_eqT_pattern, build_coq_eqT_data;*) + coq_idT_pattern, build_coq_idT_data] + +let find_eq_data_decompose eqn = (* fails with PatternMatchingFailure *) + first_match (match_eq eqn) equalities + +open Tacmach +open Tacticals + +let match_eq_nf gls eqn eq_pat = + match pf_matches gls (Lazy.force eq_pat) eqn with + | [(m1,t);(m2,x);(m3,y)] -> + assert (m1 = meta1 & m2 = meta2 & m3 = meta3); + (t,pf_whd_betadeltaiota gls x,pf_whd_betadeltaiota gls y) + | _ -> anomaly "match_eq: an eq pattern should match 3 terms" + +let dest_nf_eq gls eqn = + try + snd (first_match (match_eq_nf gls eqn) equalities) + with PatternMatchingFailure -> + error "Not an equality" + +(*** Sigma-types *) + +(* Patterns "(existS ?1 ?2 ?3 ?4)" and "(existT ?1 ?2 ?3 ?4)" *) +let coq_ex_pattern_gen ex = + lazy(PApp(PRef (Lazy.force ex), [|mkPMeta 1;mkPMeta 2;mkPMeta 3;mkPMeta 4|])) +let coq_existS_pattern = coq_ex_pattern_gen coq_existS_ref +let coq_existT_pattern = coq_ex_pattern_gen coq_existT_ref + +let match_sigma ex ex_pat = + match matches (Lazy.force ex_pat) ex with + | [(m1,a);(m2,p);(m3,car);(m4,cdr)] as l -> + assert (m1=meta1 & m2=meta2 & m3=meta3 & m4=meta4); + (a,p,car,cdr) + | _ -> + anomaly "match_sigma: a successful sigma pattern should match 4 terms" + +let find_sigma_data_decompose ex = (* fails with PatternMatchingFailure *) + first_match (match_sigma ex) + [coq_existS_pattern, build_sigma_set; + coq_existT_pattern, build_sigma_type] + +(* Pattern "(sig ?1 ?2)" *) +let coq_sig_pattern = + lazy (PApp (PRef (Lazy.force coq_sig_ref), [| (mkPMeta 1); (mkPMeta 2) |])) + +let match_sigma t = + match matches (Lazy.force coq_sig_pattern) t with + | [(_,a); (_,p)] -> (a,p) + | _ -> anomaly "Unexpected pattern" + +let is_matching_sigma t = is_matching (Lazy.force coq_sig_pattern) t + +(*** Decidable equalities *) + +(* Pattern "(sumbool (eq ?1 ?2 ?3) ?4)" *) +let coq_eqdec_partial_pattern = + lazy + (PApp + (PRef (Lazy.force coq_sumbool_ref), + [| Lazy.force coq_eq_pattern; (mkPMeta 4) |])) + +let match_eqdec_partial t = + match matches (Lazy.force coq_eqdec_partial_pattern) t with + | [_; (_,lhs); (_,rhs); _] -> (lhs,rhs) + | _ -> anomaly "Unexpected pattern" + +(* The expected form of the goal for the tactic Decide Equality *) + +(* Pattern "(x,y:?1){x=y}+{~(x=y)}" *) +(* i.e. "(x,y:?1)(sumbool (eq ?1 x y) ~(eq ?1 x y))" *) +let x = Name (id_of_string "x") +let y = Name (id_of_string "y") +let coq_eqdec_pattern = + lazy + (PProd (x, (mkPMeta 1), PProd (y, (mkPMeta 1), + PApp (PRef (Lazy.force coq_sumbool_ref), + [| PApp (PRef (Lazy.force coq_eq_ref), + [| (mkPMeta 1); PRel 2; PRel 1 |]); + PApp (PRef (Lazy.force coq_not_ref), + [|PApp (PRef (Lazy.force coq_eq_ref), + [| (mkPMeta 1); PRel 2; PRel 1 |])|]) |])))) + +let match_eqdec t = + match matches (Lazy.force coq_eqdec_pattern) t with + | [(_,typ)] -> typ + | _ -> anomaly "Unexpected pattern" + +(* Patterns "~ ?" and "? -> False" *) +let coq_not_pattern = lazy(PApp(PRef (Lazy.force coq_not_ref), [|PMeta None|])) +let coq_imp_False_pattern = + lazy (imp (PMeta None) (PRef (Lazy.force coq_False_ref))) + +let is_matching_not t = is_matching (Lazy.force coq_not_pattern) t +let is_matching_imp_False t = is_matching (Lazy.force coq_imp_False_pattern) t diff --git a/tactics/hipattern.mli b/tactics/hipattern.mli new file mode 100644 index 00000000..7e2aa8f2 --- /dev/null +++ b/tactics/hipattern.mli @@ -0,0 +1,129 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* bool + +(*s 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 + +val match_with_non_recursive_type : (constr * constr list) matching_function +val is_non_recursive_type : testing_function + +val match_with_disjunction : (constr * constr list) matching_function +val is_disjunction : testing_function + +val match_with_conjunction : (constr * constr list) matching_function +val is_conjunction : testing_function + +val match_with_empty_type : constr matching_function +val is_empty_type : testing_function + +val match_with_unit_type : constr matching_function + +(* type with only one constructor and no arguments *) +val is_unit_type : testing_function + +val match_with_equation : (constr * constr list) matching_function +val is_equation : testing_function + +val match_with_nottype : (constr * constr) matching_function +val is_nottype : testing_function + +val match_with_forall_term : (name * constr * constr) matching_function +val is_forall_term : testing_function + +val match_with_imp_term : (constr * constr) matching_function +val is_imp_term : testing_function + +(* I added these functions to test whether a type contains dependent + products or not, and if an inductive has constructors with dependent types + (excluding parameters). this is useful to check whether a conjunction is a + real conjunction and not a dependent tuple. (Pierre Corbineau, 13/5/2002) *) + +val has_nodep_prod_after : int -> testing_function +val has_nodep_prod : testing_function + +val match_with_nodep_ind : (constr * constr list * int) matching_function +val is_nodep_ind : testing_function + +val match_with_sigma_type : (constr * constr list) matching_function +val is_sigma_type : testing_function + +(***** Destructing patterns bound to some theory *) + +open Coqlib + +(* Match terms [(eq A t u)], [(eqT A t u)] or [(identityT A t u)] *) +(* Returns associated lemmas and [A,t,u] *) +val find_eq_data_decompose : constr -> + coq_leibniz_eq_data * (constr * constr * constr) + +(* Match a term of the form [(existS A P t p)] or [(existT A P t p)] *) +(* Returns associated lemmas and [A,P,t,p] *) +val find_sigma_data_decompose : constr -> + coq_sigma_data * (constr * constr * constr * constr) + +(* Match a term of the form [{x:A|P}], returns [A] and [P] *) +val match_sigma : constr -> constr * constr + +val is_matching_sigma : constr -> bool + +(* Match a term of the form [{x=y}+{_}], returns [x] and [y] *) +val match_eqdec_partial : constr -> constr * constr + +(* Match a term of the form [(x,y:t){x=y}+{~x=y}], returns [t] *) +val match_eqdec : constr -> constr + +(* Match an equality up to conversion; returns [(eq,t1,t2)] in normal form *) +open Proof_type +open Tacmach +val dest_nf_eq : goal sigma -> constr -> (constr * constr * constr) + +(* Match a negation *) +val is_matching_not : constr -> bool +val is_matching_imp_False : constr -> bool diff --git a/tactics/inv.ml b/tactics/inv.ml new file mode 100644 index 00000000..54ce467c --- /dev/null +++ b/tactics/inv.ml @@ -0,0 +1,564 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* mv::acc + | _ -> fold_constr collrec acc c + in + collrec [] c + +let check_no_metas clenv ccl = + if occur_meta ccl then + let metas = List.map (fun n -> Metamap.find n clenv.namenv) + (collect_meta_variables ccl) in + errorlabstrm "inversion" + (str ("Cannot find an instantiation for variable"^ + (if List.length metas = 1 then " " else "s ")) ++ + prlist_with_sep pr_coma pr_id metas + (* ajouter "in " ++ prterm ccl mais il faut le bon contexte *)) + +let var_occurs_in_pf gl id = + let env = pf_env gl in + occur_var env id (pf_concl gl) or + List.exists (occur_var_in_decl env id) (pf_hyps gl) + +(* [make_inv_predicate (ity,args) C] + + is given the inductive type, its arguments, both the global + parameters and its local arguments, and is expected to produce a + predicate P such that if largs is the "local" part of the + arguments, then (P largs) will be convertible with a conclusion of + the form: + + a1=a1->a2=a2 ... -> C + + Algorithm: suppose length(largs)=n + + (1) Push the entire arity, [xbar:Abar], carrying along largs and + the conclusion + + (2) Pair up each ai with its respective Rel version: a1==(Rel n), + a2==(Rel n-1), etc. + + (3) For each pair, ai,Rel j, if the Ai is dependent - that is, the + type of [Rel j] is an open term, then we construct the iterated + tuple, [make_iterated_tuple] does it, and use that for our equation + + Otherwise, we just use ai=Rel j + + *) + +type inversion_status = Dep of constr option | NoDep + +let compute_eqn env sigma n i ai = + (ai,get_type_of env sigma ai), + (mkRel (n-i),get_type_of env sigma (mkRel (n-i))) + +let make_inv_predicate env sigma indf realargs id status concl = + let nrealargs = List.length realargs in + let (hyps,concl) = + match status with + | NoDep -> + (* We push the arity and leave concl unchanged *) + let hyps_arity,_ = get_arity env indf in + (hyps_arity,concl) + | Dep dflt_concl -> + if not (occur_var env id concl) then + errorlabstrm "make_inv_predicate" + (str "Current goal does not depend on " ++ pr_id id); + (* We abstract the conclusion of goal with respect to + realargs and c to * be concl in order to rewrite and have + c also rewritten when the case * will be done *) + let pred = + match dflt_concl with + | Some concl -> concl (*assumed it's some [x1..xn,H:I(x1..xn)]C*) + | None -> + let sort = get_sort_of env sigma concl in + let p = make_arity env true indf sort in + abstract_list_all env sigma p concl (realargs@[mkVar id]) in + let hyps,bodypred = decompose_lam_n_assum (nrealargs+1) pred in + (* We lift to make room for the equations *) + (hyps,lift nrealargs bodypred) + in + let nhyps = List.length hyps in + let env' = push_rel_context hyps env in + let realargs' = List.map (lift nhyps) realargs in + let pairs = list_map_i (compute_eqn env' sigma nhyps) 0 realargs' in + (* Now the arity is pushed, and we need to construct the pairs + * ai,mkRel(n-i+1) *) + (* Now, we can recurse down this list, for each ai,(mkRel k) whether to + push (mkRel k)=ai (when Ai is closed). + In any case, we carry along the rest of pairs *) + let rec build_concl eqns n = function + | [] -> (prod_it concl eqns,n) + | ((ai,ati),(xi,ti))::restlist -> + let (lhs,eqnty,rhs) = + if closed0 ti then + (xi,ti,ai) + else + make_iterated_tuple env' sigma (ai,ati) (xi,ti) + in + let type_type_rhs = get_sort_of env sigma (type_of env sigma rhs) in + let sort = get_sort_of env sigma concl in + let eq_term = find_eq_pattern type_type_rhs sort in + let eqn = applist (eq_term ,[eqnty;lhs;rhs]) in + build_concl ((Anonymous,lift n eqn)::eqns) (n+1) restlist + in + let (newconcl,neqns) = build_concl [] 0 pairs in + let predicate = it_mkLambda_or_LetIn_name env newconcl hyps in + (* OK - this predicate should now be usable by res_elimination_then to + do elimination on the conclusion. *) + (predicate,neqns) + +(* The result of the elimination is a bunch of goals like: + + |- (cibar:Cibar)Equands->C + + where the cibar are either dependent or not. We are fed a + signature, with "true" for every recursive argument, and false for + every non-recursive one. So we need to do the + sign_branch_len(sign) intros, thinning out all recursive + assumptions. This leaves us with exactly length(sign) assumptions. + + We save their names, and then do introductions for all the equands + (there are some number of them, which is the other argument of the + tactic) + + This gives us the #neqns equations, whose names we get also, and + the #length(sign) arguments. + + Suppose that #nodep of these arguments are non-dependent. + Generalize and thin them. + + This gives us #dep = #length(sign)-#nodep arguments which are + dependent. + + Now, we want to take each of the equations, and do all possible + injections to get the left-hand-side to be a variable. At the same + time, if we find a lhs/rhs pair which are different, we can + discriminate them to prove false and finish the branch. + + Then, we thin away the equations, and do the introductions for the + #nodep arguments which we generalized before. + *) + +(* Called after the case-assumptions have been killed off, and all the + intros have been done. Given that the clause in question is an + equality (if it isn't we fail), we are responsible for projecting + the equality, using Injection and Discriminate, and applying it to + the concusion *) + +(* Computes the subset of hypothesis in the local context whose + type depends on t (should be of the form (mkVar id)), then + it generalizes them, applies tac to rewrite all occurrencies of t, + and introduces generalized hypotheis. + Precondition: t=(mkVar id) *) + +let rec dependent_hyps id idlist sign = + let rec dep_rec =function + | [] -> [] + | (id1,_,id1ty as d1)::l -> + if occur_var (Global.env()) id id1ty + then d1 :: dep_rec l + else dep_rec l + in + dep_rec idlist + +let split_dep_and_nodep hyps gl = + List.fold_right + (fun (id,_,_ as d) (l1,l2) -> + if var_occurs_in_pf gl id then (d::l1,l2) else (l1,d::l2)) + hyps ([],[]) + +open Coqlib + +(* Computation of dids is late; must have been done in rewrite_equations*) +(* Will keep generalizing and introducing back and forth... *) +(* Moreover, others hyps depending of dids should have been *) +(* generalized; in such a way that [dids] can endly be cleared *) +(* Consider for instance this case extracted from Well_Ordering.v + + A : Set + B : A ->Set + a0 : A + f : (B a0) ->WO + y : WO + H0 : (le_WO y (sup a0 f)) + ============================ + (Acc WO le_WO y) + + Inversion H0 gives + + A : Set + B : A ->Set + a0 : A + f : (B a0) ->WO + y : WO + H0 : (le_WO y (sup a0 f)) + a1 : A + f0 : (B a1) ->WO + v : (B a1) + H1 : (f0 v)=y + H3 : a1=a0 + f1 : (B a0) ->WO + v0 : (B a0) + H4 : (existS A [a:A](B a) ->WO a0 f1)=(existS A [a:A](B a) ->WO a0 f) + ============================ + (Acc WO le_WO (f1 v0)) + +while, ideally, we would have expected + + A : Set + B : A ->Set + a0 : A + f0 : (B a0)->WO + v : (B a0) + ============================ + (Acc WO le_WO (f0 v)) + +obtained from destruction with equalities + + A : Set + B : A ->Set + a0 : A + f : (B a0) ->WO + y : WO + H0 : (le_WO y (sup a0 f)) + a1 : A + f0 : (B a1)->WO + v : (B a1) + H1 : (f0 v)=y + H2 : (sup a1 f0)=(sup a0 f) + ============================ + (Acc WO le_WO (f0 v)) + +by clearing initial hypothesis H0 and its dependency y, clearing H1 +(in fact H1 can be avoided using the same trick as for newdestruct), +decomposing H2 to get a1=a0 and (a1,f0)=(a0,f), replacing a1 by a0 +everywhere and removing a1 and a1=a0 (in fact it would have been more +regular to replace a0 by a1, avoiding f1 and v0 cannot replace f0 and v), +finally removing H4 (here because f is not used, more generally after using +eq_dep and replacing f by f0) [and finally rename a0, f0 into a,f]. +Summary: nine useless hypotheses! +Nota: with Inversion_clear, only four useless hypotheses +*) + +let generalizeRewriteIntros tac depids id gls = + let dids = dependent_hyps id depids (pf_env gls) in + (tclTHENSEQ + [bring_hyps dids; tac; + (* may actually fail to replace if dependent in a previous eq *) + intros_replacing (ids_of_named_context dids)]) + gls + +let rec tclMAP_i n tacfun = function + | [] -> tclDO n (tacfun None) + | a::l -> + if n=0 then error "Too much names" + else tclTHEN (tacfun (Some a)) (tclMAP_i (n-1) tacfun l) + +let remember_first_eq id x = if !x = None then x := Some id + +(* invariant: ProjectAndApply is responsible for erasing the clause + which it is given as input + It simplifies the clause (an equality) to use it as a rewrite rule and then + erases the result of the simplification. *) +(* invariant: ProjectAndApplyNoThining simplifies the clause (an equality) . + If it can discriminate then the goal is proved, if not tries to use it as + a rewrite rule. It erases the clause which is given as input *) + +let projectAndApply thin id eqname names depids gls = + let env = pf_env gls in + let clearer id = + if thin then clear [id] else (remember_first_eq id eqname; tclIDTAC) in + let subst_hyp_LR id = tclTHEN (tclTRY(hypSubst_LR id onConcl)) (clearer id) in + let subst_hyp_RL id = tclTHEN (tclTRY(hypSubst_RL id onConcl)) (clearer id) in + let substHypIfVariable tac id gls = + let (t,t1,t2) = Hipattern.dest_nf_eq gls (pf_get_hyp_typ gls id) in + match (kind_of_term t1, kind_of_term t2) with + | Var id1, _ -> generalizeRewriteIntros (subst_hyp_LR id) depids id1 gls + | _, Var id2 -> generalizeRewriteIntros (subst_hyp_RL id) depids id2 gls + | _ -> tac id gls + in + let deq_trailer id neqns = + tclTHENSEQ + [(if names <> [] then clear [id] else tclIDTAC); + (tclMAP_i neqns (fun idopt -> + tclTHEN + (intro_move idopt None) + (* try again to substitute and if still not a variable after *) + (* decomposition, arbitrarily try to rewrite RL !? *) + (tclTRY (onLastHyp (substHypIfVariable subst_hyp_RL)))) + names); + (if names = [] then clear [id] else tclIDTAC)] + in + substHypIfVariable + (* If no immediate variable in the equation, try to decompose it *) + (* and apply a trailer which again try to substitute *) + (fun id -> dEqThen (deq_trailer id) (Some (NamedHyp id))) + id + gls + +(* Inversion qui n'introduit pas les hypotheses, afin de pouvoir les nommer + soi-meme (proposition de Valerie). *) +let rewrite_equations_gene othin neqns ba gl = + let (depids,nodepids) = split_dep_and_nodep ba.assums gl in + let rewrite_eqns = + match othin with + | Some thin -> + onLastHyp + (fun last -> + tclTHENSEQ + [tclDO neqns + (tclTHEN intro + (onLastHyp + (fun id -> + tclTRY + (projectAndApply thin id (ref None) + [] depids)))); + onHyps (compose List.rev (afterHyp last)) bring_hyps; + onHyps (afterHyp last) + (compose clear ids_of_named_context)]) + | None -> tclIDTAC + in + (tclTHENSEQ + [tclDO neqns intro; + bring_hyps nodepids; + clear (ids_of_named_context nodepids); + onHyps (compose List.rev (nLastHyps neqns)) bring_hyps; + onHyps (nLastHyps neqns) (compose clear ids_of_named_context); + rewrite_eqns; + tclMAP (fun (id,_,_ as d) -> + (tclORELSE (clear [id]) + (tclTHEN (bring_hyps [d]) (clear [id])))) + depids]) + gl + +(* Introduction of the equations on arguments + othin: discriminates Simple Inversion, Inversion and Inversion_clear + None: the equations are introduced, but not rewritten + Some thin: the equations are rewritten, and cleared if thin is true *) + +let rec get_names allow_conj = function + | IntroWildcard -> + error "Discarding pattern not allowed for inversion equations" + | IntroOrAndPattern [l] -> + if allow_conj then + if l = [] then (None,[]) else + let l = List.map (fun id -> out_some (fst (get_names false id))) l in + (Some (List.hd l), l) + else + error "Nested conjunctive patterns not allowed for inversion equations" + | IntroOrAndPattern l -> + error "Disjunctive patterns not allowed for inversion equations" + | IntroIdentifier id -> + (Some id,[id]) + +let extract_eqn_names = function + | None -> None,[] + | Some x -> x + +let rewrite_equations othin neqns names ba gl = + let names = List.map (get_names true) names in + let (depids,nodepids) = split_dep_and_nodep ba.assums gl in + let rewrite_eqns = + let first_eq = ref None in + let update id = if !first_eq = None then first_eq := Some id in + match othin with + | Some thin -> + tclTHENSEQ + [onHyps (compose List.rev (nLastHyps neqns)) bring_hyps; + onHyps (nLastHyps neqns) (compose clear ids_of_named_context); + tclMAP_i neqns (fun o -> + let idopt,names = extract_eqn_names o in + (tclTHEN + (intro_move idopt None) + (onLastHyp (fun id -> + tclTRY (projectAndApply thin id first_eq names depids))))) + names; + tclMAP (fun (id,_,_) gl -> + intro_move None (if thin then None else !first_eq) gl) + nodepids; + tclMAP (fun (id,_,_) -> tclTRY (clear [id])) depids] + | None -> tclIDTAC + in + (tclTHENSEQ + [tclDO neqns intro; + bring_hyps nodepids; + clear (ids_of_named_context nodepids); + rewrite_eqns]) + gl + +let interp_inversion_kind = function + | SimpleInversion -> None + | FullInversion -> Some false + | FullInversionClear -> Some true + +let rewrite_equations_tac (gene, othin) id neqns names ba = + let othin = interp_inversion_kind othin in + let tac = + if gene then rewrite_equations_gene othin neqns ba + else rewrite_equations othin neqns names ba in + if othin = Some true (* if Inversion_clear, clear the hypothesis *) then + tclTHEN tac (tclTRY (clear [id])) + else + tac + + +let raw_inversion inv_kind indbinding id status names gl = + let env = pf_env gl and sigma = project gl in + let c = mkVar id in + let (wc,kONT) = startWalk gl in + let t = strong_prodspine (pf_whd_betadeltaiota gl) (pf_type_of gl c) in + let indclause = mk_clenv_from wc (c,t) in + let indclause' = clenv_constrain_with_bindings indbinding indclause in + let newc = clenv_instance_template indclause' in + let ccl = clenv_instance_template_type indclause' in + check_no_metas indclause' ccl; + let IndType (indf,realargs) = + try find_rectype env sigma ccl + with Not_found -> + errorlabstrm "raw_inversion" + (str ("The type of "^(string_of_id id)^" is not inductive")) in + let (elim_predicate,neqns) = + make_inv_predicate env sigma indf realargs id status (pf_concl gl) in + let (cut_concl,case_tac) = + if status <> NoDep & (dependent c (pf_concl gl)) then + Reduction.beta_appvect elim_predicate (Array.of_list (realargs@[c])), + case_then_using + else + Reduction.beta_appvect elim_predicate (Array.of_list realargs), + case_nodep_then_using + in + (tclTHENS + (true_cut Anonymous cut_concl) + [case_tac names + (introCaseAssumsThen (rewrite_equations_tac inv_kind id neqns)) + (Some elim_predicate) ([],[]) newc; + onLastHyp + (fun id -> + (tclTHEN + (apply_term (mkVar id) + (list_tabulate (fun _ -> mkMeta(Clenv.new_meta())) neqns)) + reflexivity))]) + gl + +(* Error messages of the inversion tactics *) +let not_found_message ids = + if List.length ids = 1 then + (str "the variable" ++ spc () ++ str (string_of_id (List.hd ids)) ++ spc () ++ + str" was not found in the current environment") + else + (str "the variables [" ++ + spc () ++ prlist (fun id -> (str (string_of_id id) ++ spc ())) ids ++ + str" ] were not found in the current environment") + +let dep_prop_prop_message id = + errorlabstrm "Inv" + (str "Inversion on " ++ pr_id id ++ + str " would needs dependent elimination Prop-Prop") + +let not_inductive_here id = + errorlabstrm "mind_specif_of_mind" + (str "Cannot recognize an inductive predicate in " ++ pr_id id ++ + str ". If there is one, may be the structure of the arity or of the type of constructors is hidden by constant definitions.") + +(* Noms d'errreurs obsolètes ?? *) +let wrap_inv_error id = function + | UserError ("Case analysis",s) -> errorlabstrm "Inv needs Nodep Prop Set" s + | UserError("mind_specif_of_mind",_) -> not_inductive_here id + | UserError (a,b) -> errorlabstrm "Inv" b + | Invalid_argument (*"it_list2"*) "List.fold_left2" -> dep_prop_prop_message id + | Not_found -> errorlabstrm "Inv" (not_found_message [id]) + | e -> raise e + +(* The most general inversion tactic *) +let inversion inv_kind status names id gls = + try (raw_inversion inv_kind [] id status names) gls + with e -> wrap_inv_error id e + +(* Specializing it... *) + +let inv_gen gene thin status names = + try_intros_until (inversion (gene,thin) status names) + +open Tacexpr + +let inv k = inv_gen false k NoDep + +let half_inv_tac id = inv SimpleInversion None (NamedHyp id) +let inv_tac id = inv FullInversion None (NamedHyp id) +let inv_clear_tac id = inv FullInversionClear None (NamedHyp id) + +let dinv k c = inv_gen false k (Dep c) + +let half_dinv_tac id = dinv SimpleInversion None None (NamedHyp id) +let dinv_tac id = dinv FullInversion None None (NamedHyp id) +let dinv_clear_tac id = dinv FullInversionClear None None (NamedHyp id) + +(* InvIn will bring the specified clauses into the conclusion, and then + * perform inversion on the named hypothesis. After, it will intro them + * back to their places in the hyp-list. *) + +let invIn k names ids id gls = + let hyps = List.map (pf_get_hyp gls) ids in + let nb_prod_init = nb_prod (pf_concl gls) in + let intros_replace_ids gls = + let nb_of_new_hyp = + nb_prod (pf_concl gls) - (List.length hyps + nb_prod_init) + in + if nb_of_new_hyp < 1 then + intros_replacing ids gls + else + tclTHEN (tclDO nb_of_new_hyp intro) (intros_replacing ids) gls + in + try + (tclTHENSEQ + [bring_hyps hyps; + inversion (false,k) NoDep names id; + intros_replace_ids]) + gls + with e -> wrap_inv_error id e + +let invIn_gen k names idl = try_intros_until (invIn k names idl) + +let inv_clause k names = function + | [] -> inv k names + | idl -> invIn_gen k names idl diff --git a/tactics/inv.mli b/tactics/inv.mli new file mode 100644 index 00000000..e19d8232 --- /dev/null +++ b/tactics/inv.mli @@ -0,0 +1,44 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* inversion_kind -> inversion_status -> + intro_pattern_expr option -> quantified_hypothesis -> tactic +val invIn_gen : + inversion_kind -> intro_pattern_expr option -> identifier list -> + quantified_hypothesis -> tactic + +val inv_clause : + inversion_kind -> intro_pattern_expr option -> identifier list -> + quantified_hypothesis -> tactic + +val inv : inversion_kind -> intro_pattern_expr option -> + quantified_hypothesis -> tactic + +val dinv : inversion_kind -> constr option -> intro_pattern_expr option -> + quantified_hypothesis -> tactic + +val half_inv_tac : identifier -> tactic +val inv_tac : identifier -> tactic +val inv_clear_tac : identifier -> tactic +val half_dinv_tac : identifier -> tactic +val dinv_tac : identifier -> tactic +val dinv_clear_tac : identifier -> tactic diff --git a/tactics/leminv.ml b/tactics/leminv.ml new file mode 100644 index 00000000..1be465f5 --- /dev/null +++ b/tactics/leminv.ml @@ -0,0 +1,318 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(*