diff options
| -rw-r--r-- | tactics/tacticals.ml | 9 | ||||
| -rw-r--r-- | tactics/tactics.ml | 59 | ||||
| -rw-r--r-- | toplevel/indschemes.ml | 18 |
3 files changed, 55 insertions, 31 deletions
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml index c95486df61..4ba26dcebc 100644 --- a/tactics/tacticals.ml +++ b/tactics/tacticals.ml @@ -307,8 +307,13 @@ let gl_make_case_nodep ind gl = let elimination_then_using tac predicate bindings c gl = let (ind,t) = pf_reduce_to_quantified_ind gl (pf_type_of gl c) in let indclause = mk_clenv_from gl (c,t) in - general_elim_then_using gl_make_elim - true None tac predicate bindings ind indclause gl + let isrec,mkelim = + if (Global.lookup_mind (fst ind)).mind_record + then false,gl_make_case_dep + else true,gl_make_elim + in + general_elim_then_using mkelim isrec + None tac predicate bindings ind indclause gl let case_then_using = general_elim_then_using gl_make_case_dep false diff --git a/tactics/tactics.ml b/tactics/tactics.ml index bf93530762..2f386def1f 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -782,16 +782,48 @@ let general_elim_clause elimtac (c,lbindc) elim gl = let general_elim with_evars c e = general_elim_clause (elimination_clause_scheme with_evars) c e +(* Case analysis tactics *) + +let general_case_analysis_in_context with_evars (c,lbindc) gl = + let (mind,_) = pf_reduce_to_quantified_ind gl (pf_type_of gl c) in + let sort = elimination_sort_of_goal gl in + let elim = + if occur_term c (pf_concl gl) then + pf_apply build_case_analysis_scheme gl mind true sort + else + pf_apply build_case_analysis_scheme_default gl mind sort in + general_elim with_evars (c,lbindc) + {elimindex = None; elimbody = (elim,NoBindings)} gl + +let general_case_analysis with_evars (c,lbindc as cx) = + match kind_of_term c with + | Var id when lbindc = NoBindings -> + tclTHEN (try_intros_until_id_check id) + (general_case_analysis_in_context with_evars cx) + | _ -> + general_case_analysis_in_context with_evars cx + +let simplest_case c = general_case_analysis false (c,NoBindings) + (* Elimination tactic with bindings but using the default elimination * constant associated with the type. *) +exception IsRecord + +let is_record mind = (Global.lookup_mind (fst mind)).mind_record + let find_eliminator c gl = let (ind,t) = pf_reduce_to_quantified_ind gl (pf_type_of gl c) in + if is_record ind then raise IsRecord; let c = lookup_eliminator ind (elimination_sort_of_goal gl) in {elimindex = None; elimbody = (c,NoBindings)} let default_elim with_evars (c,_ as cx) gl = - general_elim with_evars cx (find_eliminator c gl) gl + try general_elim with_evars cx (find_eliminator c gl) gl + with IsRecord -> + (* For records, induction principles aren't there by default anymore. + Instead, we do a case analysis instead. *) + general_case_analysis with_evars cx gl let elim_in_context with_evars c = function | Some elim -> @@ -848,29 +880,6 @@ let elimination_in_clause_scheme with_evars ?(flags=elim_flags) id i elimclause let general_elim_in with_evars id = general_elim_clause (elimination_in_clause_scheme with_evars id) -(* Case analysis tactics *) - -let general_case_analysis_in_context with_evars (c,lbindc) gl = - let (mind,_) = pf_reduce_to_quantified_ind gl (pf_type_of gl c) in - let sort = elimination_sort_of_goal gl in - let elim = - if occur_term c (pf_concl gl) then - pf_apply build_case_analysis_scheme gl mind true sort - else - pf_apply build_case_analysis_scheme_default gl mind sort in - general_elim with_evars (c,lbindc) - {elimindex = None; elimbody = (elim,NoBindings)} gl - -let general_case_analysis with_evars (c,lbindc as cx) = - match kind_of_term c with - | Var id when lbindc = NoBindings -> - tclTHEN (try_intros_until_id_check id) - (general_case_analysis_in_context with_evars cx) - | _ -> - general_case_analysis_in_context with_evars cx - -let simplest_case c = general_case_analysis false (c,NoBindings) - (* Apply a tactic below the products of the conclusion of a lemma *) type conjunction_status = @@ -2803,7 +2812,7 @@ let guess_elim isrec hyp0 gl = let mind,_ = pf_reduce_to_quantified_ind gl tmptyp0 in let s = elimination_sort_of_goal gl in let elimc = - if isrec then lookup_eliminator mind s + if isrec && not (is_record mind) then lookup_eliminator mind s else if use_dependent_propositions_elimination () && dependent_no_evar (mkVar hyp0) (pf_concl gl) diff --git a/toplevel/indschemes.ml b/toplevel/indschemes.ml index 8804c60c82..6537ff10d7 100644 --- a/toplevel/indschemes.ml +++ b/toplevel/indschemes.ml @@ -55,6 +55,16 @@ let _ = optread = (fun () -> !elim_flag) ; optwrite = (fun b -> elim_flag := b) } +let record_elim_flag = ref false +let _ = + declare_bool_option + { optsync = true; + optdepr = false; + optname = "automatic declaration of induction schemes for records"; + optkey = ["Record";"Elimination";"Schemes"]; + optread = (fun () -> !record_elim_flag) ; + optwrite = (fun b -> record_elim_flag := b) } + let case_flag = ref false let _ = declare_bool_option @@ -448,11 +458,11 @@ let do_combined_scheme name schemes = let map_inductive_block f kn n = for i=0 to n-1 do f (kn,i) done -let mutual_inductive_size kn = Array.length (Global.lookup_mind kn).mind_packets - let declare_default_schemes kn = - let n = mutual_inductive_size kn in - if !elim_flag then declare_induction_schemes kn; + let mib = Global.lookup_mind kn in + let n = Array.length mib.mind_packets in + if !elim_flag && (not mib.mind_record || !record_elim_flag) then + declare_induction_schemes kn; if !case_flag then map_inductive_block declare_one_case_analysis_scheme kn n; if is_eq_flag() then try_declare_beq_scheme kn; if !eq_dec_flag then try_declare_eq_decidability kn; |