diff options
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/eqdecide.ml4 | 4 | ||||
| -rw-r--r-- | tactics/equality.ml | 148 | ||||
| -rw-r--r-- | tactics/equality.mli | 24 | ||||
| -rw-r--r-- | tactics/extratactics.ml4 | 84 | ||||
| -rw-r--r-- | tactics/extratactics.mli | 5 | ||||
| -rw-r--r-- | tactics/inv.ml | 2 | ||||
| -rw-r--r-- | tactics/tacinterp.ml | 2 | ||||
| -rw-r--r-- | tactics/tacticals.ml | 4 | ||||
| -rw-r--r-- | tactics/tactics.ml | 33 | ||||
| -rw-r--r-- | tactics/tactics.mli | 7 |
10 files changed, 208 insertions, 105 deletions
diff --git a/tactics/eqdecide.ml4 b/tactics/eqdecide.ml4 index 8aef9c50b..61100f0a5 100644 --- a/tactics/eqdecide.ml4 +++ b/tactics/eqdecide.ml4 @@ -75,7 +75,7 @@ let mkBranches c1 c2 = let solveNoteqBranch side = tclTHEN (choose_noteq side) (tclTHEN (intro_force true) - (onLastHyp (fun id -> Extratactics.h_discrHyp (Rawterm.NamedHyp id)))) + (onLastHyp (fun id -> Extratactics.h_discrHyp id))) let h_solveNoteqBranch side = Refiner.abstract_extended_tactic "solveNoteqBranch" [] @@ -115,7 +115,7 @@ let diseqCase eqonleft = (tclTHEN red_in_concl (tclTHEN (intro_using absurd) (tclTHEN (h_simplest_apply (mkVar diseq)) - (tclTHEN (Extratactics.h_injHyp (Rawterm.NamedHyp absurd)) + (tclTHEN (Extratactics.h_injHyp absurd) (full_trivial []))))))) let solveArg eqonleft op a1 a2 tac g = diff --git a/tactics/equality.ml b/tactics/equality.ml index f907b1fd7..3bfc719e2 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -40,6 +40,9 @@ open Vernacexpr open Setoid_replace open Declarations open Indrec +open Printer +open Clenv +open Clenvtac (* Rewriting tactics *) @@ -550,66 +553,84 @@ exception NotDiscriminable let eq_baseid = id_of_string "e" -let discr_positions env sigma (lbeq,(t,t1,t2)) id cpath dirn sort = +let apply_on_clause (f,t) clause = + let sigma = Evd.evars_of clause.evd in + let f_clause = mk_clenv_from_env clause.env sigma None (f,t) in + let argmv = + (match kind_of_term (last_arg f_clause.templval.Evd.rebus) with + | Meta mv -> mv + | _ -> errorlabstrm "" (str "Ill-formed clause applicator")) in + clenv_fchain argmv f_clause clause + +let discr_positions env sigma (lbeq,(t,t1,t2)) eq_clause cpath dirn sort = let e = next_ident_away eq_baseid (ids_of_context env) in let e_env = push_named (e,None,t) env in + let eqn = mkApp(lbeq.eq,[|t;t1;t2|]) 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 in - tclCOMPLETE - ((tclTHENS (cut_intro absurd_term) - [onLastHyp gen_absurdity; - refine (mkApp (pf,[|mkVar id|]))])) + let pf_ty = mkArrow eqn absurd_term in + let absurd_clause = apply_on_clause (pf,pf_ty) eq_clause in + tclTHENS (cut_intro absurd_term) + [onLastHyp gen_absurdity; res_pf absurd_clause] -let discrEq (lbeq,(t,t1,t2) as u) id gls = - let sigma = project gls in +let discrEq (lbeq,(t,t1,t2) as u) eq_clause gls = + let sigma = Evd.evars_of eq_clause.evd in let env = pf_env gls in match find_positions env sigma t1 t2 with | Inr _ -> - errorlabstrm "discr" (str" Not a discriminable equality") + errorlabstrm "discr" (str"Not a discriminable equality") | Inl (cpath, (_,dirn), _) -> let sort = pf_apply get_type_of gls (pf_concl gls) in - discr_positions env sigma u id cpath dirn sort gls - -let onEquality tac id gls = - let eqn = pf_whd_betadeltaiota gls (pf_get_hyp_typ gls id) in + discr_positions env sigma u eq_clause cpath dirn sort gls + +let onEquality with_evars tac (c,lbindc) gls = + let t = pf_type_of gls c in + let t' = try snd (pf_reduce_to_quantified_ind gls t) with UserError _ -> t in + let eq_clause = make_clenv_binding gls (c,t') lbindc in + let eq_clause' = clenv_pose_dependent_evars with_evars eq_clause in + let eqn = clenv_type eq_clause' in let eq = try find_eq_data_decompose eqn with PatternMatchingFailure -> - errorlabstrm "" (pr_id id ++ str": not a primitive equality") - in tac eq id gls + errorlabstrm "" (str"No primitive equality found") in + tclTHEN + (Refiner.tclEVARS (Evd.evars_of eq_clause'.evd)) + (tac eq eq_clause') gls -let onNegatedEquality tac gls = +let onNegatedEquality with_evars tac gls = let ccl = pf_concl gls in - let eq = - try match kind_of_term (hnf_constr (pf_env gls) (project gls) ccl) with - | Prod (_,t,u) when is_empty_type u -> - find_eq_data_decompose (pf_whd_betadeltaiota gls t) - | _ -> raise PatternMatchingFailure - with PatternMatchingFailure -> + match kind_of_term (hnf_constr (pf_env gls) (project gls) ccl) with + | Prod (_,t,u) when is_empty_type u -> + tclTHEN introf + (onLastHyp (fun id -> + onEquality with_evars tac (mkVar id,NoBindings))) gls + | _ -> errorlabstrm "" (str "Not a negated primitive equality") - in tclTHEN introf (onLastHyp (tac eq)) gls -let discrSimpleClause = function - | None -> onNegatedEquality discrEq - | Some ((_,id),_) -> onEquality discrEq id +let discrSimpleClause with_evars = function + | None -> onNegatedEquality with_evars discrEq + | Some ((_,id),_) -> onEquality with_evars discrEq (mkVar id,NoBindings) -let discr = onEquality discrEq +let discr with_evars = onEquality with_evars discrEq -let discrClause = onClauses discrSimpleClause +let discrClause with_evars = onClauses (discrSimpleClause with_evars) -let discrEverywhere = +let discrEverywhere with_evars = tclORELSE - (Tacticals.tryAllClauses discrSimpleClause) + (tclTHEN + (tclREPEAT introf) + (Tacticals.tryAllHyps + (fun id -> tclCOMPLETE (discr with_evars (mkVar id,NoBindings))))) (fun gls -> errorlabstrm "DiscrEverywhere" (str"No discriminable equalities")) -let discr_tac = function - | None -> discrEverywhere - | Some id -> try_intros_until discr id +let discr_tac with_evars = function + | None -> discrEverywhere with_evars + | Some c -> onInductionArg (discr with_evars) c -let discrConcl gls = discrClause onConcl gls -let discrHyp id gls = discrClause (onHyp id) gls +let discrConcl gls = discrClause false onConcl gls +let discrHyp id gls = discrClause false (onHyp id) gls (* returns the sigma type (sigS, sigT) with the respective constructor depending on the sort *) @@ -828,7 +849,7 @@ let simplify_args env sigma t = | eq, [t1;c1;t2;c2] -> applist (eq,[t1;nf env sigma c1;t2;nf env sigma c2]) | _ -> t -let inject_at_positions env sigma (eq,(t,t1,t2)) id posns = +let inject_at_positions env sigma (eq,(t,t1,t2)) eq_clause posns = let e = next_ident_away eq_baseid (ids_of_context env) in let e_env = push_named (e,None,t) env in let injectors = @@ -837,9 +858,12 @@ let inject_at_positions env sigma (eq,(t,t1,t2)) id posns = (* arbitrarily take t1' as the injector default value *) let (injbody,resty) = build_injector sigma e_env t1' (mkVar e) cpath in let injfun = mkNamedLambda e t injbody in - let pf = applist(eq.congr,[t;resty;injfun;t1;t2;mkVar id]) in - let ty = simplify_args env sigma (get_type_of env sigma pf) in - (pf,ty)) + let pf = applist(eq.congr,[t;resty;injfun;t1;t2]) in + let pf_typ = get_type_of env sigma pf in + let inj_clause = apply_on_clause (pf,pf_typ) eq_clause in + let pf = clenv_value_cast_meta inj_clause in + let ty = simplify_args env sigma (clenv_type inj_clause) in + (pf,ty)) posns in if injectors = [] then errorlabstrm "Equality.inj" (str "Failed to decompose the equality"); @@ -850,14 +874,13 @@ let inject_at_positions env sigma (eq,(t,t1,t2)) id posns = exception Not_dep_pair -let injEq ipats (eq,(t,t1,t2)) id gls = - let sigma = project gls in - let env = pf_env gls in +let injEq ipats (eq,(t,t1,t2)) eq_clause = + let sigma = Evd.evars_of eq_clause.evd in + let env = eq_clause.env 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") + (str"Not a projectable equality but a discriminable one") | Inr [] -> errorlabstrm "Equality.inj" (str"Nothing to do, it is an equality between convertible terms") @@ -895,45 +918,44 @@ let injEq ipats (eq,(t,t1,t2)) id gls = [|ar1.(0);Ind_tables.find_eq_dec_proof ind; ar1.(1);ar1.(2);ar1.(3);ar2.(3)|]) )) (Auto.trivial [] []) - ] gls + ] (* not a dep eq or no decidable type found *) ) else (raise Not_dep_pair) - ) with _ -> ( - tclTHEN - (inject_at_positions env sigma (eq,(t,t1,t2)) id posns) + ) with _ -> + tclTHEN + (inject_at_positions env sigma (eq,(t,t1,t2)) eq_clause posns) (intros_pattern None ipats) - gls - ) -let inj ipats = onEquality (injEq ipats) +let inj ipats with_evars = onEquality with_evars (injEq ipats) -let injClause ipats = function - | None -> onNegatedEquality (injEq ipats) - | Some id -> try_intros_until (inj ipats) id +let injClause ipats with_evars = function + | None -> onNegatedEquality with_evars (injEq ipats) + | Some c -> onInductionArg (inj ipats with_evars) c -let injConcl gls = injClause [] None gls -let injHyp id gls = injClause [] (Some id) gls +let injConcl gls = injClause [] false None gls +let injHyp id gls = injClause [] false (Some (ElimOnIdent (dummy_loc,id))) gls -let decompEqThen ntac (lbeq,(t,t1,t2) as u) id gls = +let decompEqThen ntac (lbeq,(t,t1,t2) as u) clause gls = let sort = pf_apply get_type_of gls (pf_concl gls) in - let sigma = project gls in + let sigma = Evd.evars_of clause.evd in let env = pf_env gls in match find_positions env sigma t1 t2 with | Inl (cpath, (_,dirn), _) -> - discr_positions env sigma u id cpath dirn sort gls + discr_positions env sigma u clause cpath dirn sort gls | Inr [] -> (* Change: do not fail, simplify clear this trivial hyp *) ntac 0 gls | Inr posns -> tclTHEN - (inject_at_positions env sigma (lbeq,(t,t1,t2)) id (List.rev posns)) + (inject_at_positions env sigma (lbeq,(t,t1,t2)) clause + (List.rev posns)) (ntac (List.length posns)) gls -let dEqThen ntac = function - | None -> onNegatedEquality (decompEqThen ntac) - | Some id -> try_intros_until (onEquality (decompEqThen ntac)) id +let dEqThen with_evars ntac = function + | None -> onNegatedEquality with_evars (decompEqThen ntac) + | Some c -> onInductionArg (onEquality with_evars (decompEqThen ntac)) c -let dEq = dEqThen (fun x -> tclIDTAC) +let dEq with_evars = dEqThen with_evars (fun x -> tclIDTAC) let rewrite_msg = function | None -> str "passed term is not a primitive equality" diff --git a/tactics/equality.mli b/tactics/equality.mli index acbaca235..3c7f9c6b0 100644 --- a/tactics/equality.mli +++ b/tactics/equality.mli @@ -67,18 +67,22 @@ val replace_in : identifier -> constr -> constr -> tactic val replace_by : constr -> constr -> tactic -> tactic val replace_in_by : identifier -> constr -> constr -> tactic -> tactic -val discr : identifier -> tactic +val discr : evars_flag -> constr with_ebindings -> tactic val discrConcl : tactic -val discrClause : clause -> tactic +val discrClause : evars_flag -> clause -> tactic val discrHyp : identifier -> tactic -val discrEverywhere : tactic -val discr_tac : quantified_hypothesis option -> tactic -val inj : intro_pattern_expr list -> identifier -> tactic -val injClause : intro_pattern_expr list -> quantified_hypothesis option -> - tactic - -val dEq : quantified_hypothesis option -> tactic -val dEqThen : (int -> tactic) -> quantified_hypothesis option -> tactic +val discrEverywhere : evars_flag -> tactic +val discr_tac : evars_flag -> + constr with_ebindings induction_arg option -> tactic +val inj : intro_pattern_expr list -> evars_flag -> + constr with_ebindings -> tactic +val injClause : intro_pattern_expr list -> evars_flag -> + constr with_ebindings induction_arg option -> tactic +val injHyp : identifier -> tactic +val injConcl : tactic + +val dEq : evars_flag -> constr with_ebindings induction_arg option -> tactic +val dEqThen : evars_flag -> (int -> tactic) -> constr with_ebindings induction_arg option -> tactic val make_iterated_tuple : env -> evar_map -> constr -> (constr * types) -> constr * constr * constr diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4 index dd716024d..5d374215d 100644 --- a/tactics/extratactics.ml4 +++ b/tactics/extratactics.ml4 @@ -16,6 +16,8 @@ open Genarg open Extraargs open Mod_subst open Names +open Tacexpr +open Rawterm (* Equality *) open Equality @@ -41,25 +43,93 @@ TACTIC EXTEND replace_term -> [ replace_multi_term None c (glob_in_arg_hyp_to_clause in_hyp) ] END +let induction_arg_of_quantified_hyp = function + | AnonHyp n -> ElimOnAnonHyp n + | NamedHyp id -> ElimOnIdent (Util.dummy_loc,id) + +(* Versions *_main must come first!! so that "1" is interpreted as a + ElimOnAnonHyp and not as a "constr", and "id" is interpreted as a + ElimOnIdent and not as "constr" *) + +TACTIC EXTEND simplify_eq_main +| [ "simplify_eq" constr_with_bindings(c) ] -> + [ dEq false (Some (ElimOnConstr c)) ] +END TACTIC EXTEND simplify_eq - [ "simplify_eq" quantified_hypothesis_opt(h) ] -> [ dEq h ] + [ "simplify_eq" ] -> [ dEq false None ] +| [ "simplify_eq" quantified_hypothesis(h) ] -> + [ dEq false (Some (induction_arg_of_quantified_hyp h)) ] +END +TACTIC EXTEND esimplify_eq_main +| [ "esimplify_eq" constr_with_bindings(c) ] -> + [ dEq true (Some (ElimOnConstr c)) ] +END +TACTIC EXTEND esimplify_eq +| [ "esimplify_eq" ] -> [ dEq true None ] +| [ "esimplify_eq" quantified_hypothesis(h) ] -> + [ dEq true (Some (induction_arg_of_quantified_hyp h)) ] END +TACTIC EXTEND discriminate_main +| [ "discriminate" constr_with_bindings(c) ] -> + [ discr_tac false (Some (ElimOnConstr c)) ] +END TACTIC EXTEND discriminate - [ "discriminate" quantified_hypothesis_opt(h) ] -> [ discr_tac h ] +| [ "discriminate" ] -> [ discr_tac false None ] +| [ "discriminate" quantified_hypothesis(h) ] -> + [ discr_tac false (Some (induction_arg_of_quantified_hyp h)) ] +END +TACTIC EXTEND ediscriminate_main +| [ "ediscriminate" constr_with_bindings(c) ] -> + [ discr_tac true (Some (ElimOnConstr c)) ] +END +TACTIC EXTEND ediscriminate +| [ "ediscriminate" ] -> [ discr_tac true None ] +| [ "ediscriminate" quantified_hypothesis(h) ] -> + [ discr_tac true (Some (induction_arg_of_quantified_hyp h)) ] END -let h_discrHyp id = h_discriminate (Some id) +let h_discrHyp id = h_discriminate_main (Term.mkVar id,NoBindings) +TACTIC EXTEND injection_main +| [ "injection" constr_with_bindings(c) ] -> + [ injClause [] false (Some (ElimOnConstr c)) ] +END TACTIC EXTEND injection - [ "injection" quantified_hypothesis_opt(h) ] -> [ injClause [] h ] +| [ "injection" ] -> [ injClause [] false None ] +| [ "injection" quantified_hypothesis(h) ] -> + [ injClause [] false (Some (induction_arg_of_quantified_hyp h)) ] +END +TACTIC EXTEND einjection_main +| [ "einjection" constr_with_bindings(c) ] -> + [ injClause [] true (Some (ElimOnConstr c)) ] +END +TACTIC EXTEND einjection +| [ "einjection" ] -> [ injClause [] true None ] +| [ "einjection" quantified_hypothesis(h) ] -> [ injClause [] true (Some (induction_arg_of_quantified_hyp h)) ] +END +TACTIC EXTEND injection_as_main +| [ "injection" constr_with_bindings(c) "as" simple_intropattern_list(ipat)] -> + [ injClause ipat false (Some (ElimOnConstr c)) ] END TACTIC EXTEND injection_as - [ "injection" quantified_hypothesis_opt(h) - "as" simple_intropattern_list(ipat)] -> [ injClause ipat h ] +| [ "injection" "as" simple_intropattern_list(ipat)] -> + [ injClause ipat false None ] +| [ "injection" quantified_hypothesis(h) "as" simple_intropattern_list(ipat) ] -> + [ injClause ipat false (Some (induction_arg_of_quantified_hyp h)) ] +END +TACTIC EXTEND einjection_as_main +| [ "einjection" constr_with_bindings(c) "as" simple_intropattern_list(ipat)] -> + [ injClause ipat true (Some (ElimOnConstr c)) ] +END +TACTIC EXTEND einjection_as +| [ "einjection" "as" simple_intropattern_list(ipat)] -> + [ injClause ipat true None ] +| [ "einjection" quantified_hypothesis(h) "as" simple_intropattern_list(ipat) ] -> + [ injClause ipat true (Some (induction_arg_of_quantified_hyp h)) ] END -let h_injHyp id = h_injection (Some id) +let h_injHyp id = h_injection_main (Term.mkVar id,NoBindings) TACTIC EXTEND conditional_rewrite | [ "conditional" tactic(tac) "rewrite" orient(b) constr_with_bindings(c) ] diff --git a/tactics/extratactics.mli b/tactics/extratactics.mli index 341716c01..7a5314c36 100644 --- a/tactics/extratactics.mli +++ b/tactics/extratactics.mli @@ -9,10 +9,9 @@ (*i $Id$ i*) open Proof_type -open Rawterm -val h_discrHyp : quantified_hypothesis -> tactic -val h_injHyp : quantified_hypothesis -> tactic +val h_discrHyp : Names.identifier -> tactic +val h_injHyp : Names.identifier -> tactic val refine_tac : Evd.open_constr -> tactic diff --git a/tactics/inv.ml b/tactics/inv.ml index a77a97906..a25fa285b 100644 --- a/tactics/inv.ml +++ b/tactics/inv.ml @@ -331,7 +331,7 @@ let projectAndApply thin id eqname names depids gls = 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))) + (fun id -> dEqThen false (deq_trailer id) (Some (ElimOnIdent (dummy_loc,id)))) id gls diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index 876f13c33..897c8fd98 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -1150,7 +1150,7 @@ let debugging_exception_step ist signal_anomaly e pp = let error_ltac_variable loc id env v s = user_err_loc (loc, "", str "Ltac variable " ++ pr_id id ++ str " is bound to" ++ spc () ++ pr_value env v ++ spc () ++ - str "which cannot be coerced to " ++ str s) + strbrk "which cannot be coerced to " ++ str s) exception CannotCoerceTo of string diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml index 577ef0c6f..3d5fd753e 100644 --- a/tactics/tacticals.ml +++ b/tactics/tacticals.ml @@ -325,10 +325,6 @@ let elimination_sort_of_hyp id gl = (* Find the right elimination suffix corresponding to the sort of the goal *) (* c should be of type A1->.. An->B with B an inductive definition *) -let last_arg c = match kind_of_term c with - | App (f,cl) -> array_last cl - | _ -> anomaly "last_arg" - let general_elim_then_using mk_elim isrec allnames tac predicate (indbindings,elimbindings) ind indclause gl = diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 25e920976..c8f92b60f 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -469,6 +469,21 @@ let rec intros_rmove = function move_to_rhyp destopt; intros_rmove rest ] +(* Apply a tactic on a quantified hypothesis, an hypothesis in context + or a term with bindings *) + +let onInductionArg tac = function + | ElimOnConstr (c,lbindc as cbl) -> + if isVar c & lbindc = NoBindings then + tclTHEN (tclTRY (intros_until_id (destVar c))) (tac cbl) + else + tac cbl + | ElimOnAnonHyp n -> + tclTHEN (intros_until_n n) (tclLAST_HYP (fun c -> tac (c,NoBindings))) + | ElimOnIdent (_,id) -> + (*Identifier apart because id can be quantified in goal and not typable*) + tclTHEN (tclTRY (intros_until_id id)) (tac (mkVar id,NoBindings)) + (**************************) (* Refinement tactics *) (**************************) @@ -2531,7 +2546,6 @@ let induct_destruct_l isrec with_evars lc elim names cls = "'in' clause not supported when several induction hypothesis are given"; new_induct_gen_l isrec with_evars elim names newlc - (* Induction either over a term, over a quantified premisse, or over several quantified premisses (like with functional induction principles). @@ -2540,19 +2554,10 @@ let induct_destruct_l isrec with_evars lc elim names cls = let induct_destruct isrec with_evars lc elim names cls = assert (List.length lc > 0); (* ensured by syntax, but if called inside caml? *) if List.length lc = 1 then (* induction on one arg: use old mechanism *) - try - let c = List.hd lc in - match c with - | ElimOnConstr c -> new_induct_gen isrec with_evars elim names c cls - | ElimOnAnonHyp n -> - tclTHEN (intros_until_n n) - (tclLAST_HYP (fun c -> - new_induct_gen isrec with_evars elim names (c,NoBindings) cls)) - (* Identifier apart because id can be quantified in goal and not typable *) - | ElimOnIdent (_,id) -> - tclTHEN (tclTRY (intros_until_id id)) - (new_induct_gen isrec with_evars elim names - (mkVar id,NoBindings) cls) + try + onInductionArg + (fun c -> new_induct_gen isrec with_evars elim names c cls) + (List.hd lc) with (* If this fails, try with new mechanism but if it fails too, then the exception is the first one. *) | x -> diff --git a/tactics/tactics.mli b/tactics/tactics.mli index 0492e296f..700c25f6e 100644 --- a/tactics/tactics.mli +++ b/tactics/tactics.mli @@ -101,6 +101,13 @@ val intros_clearing : bool list -> tactic val try_intros_until : (identifier -> tactic) -> quantified_hypothesis -> tactic +(* Apply a tactic on a quantified hypothesis, an hypothesis in context + or a term with bindings *) + +val onInductionArg : + (constr with_ebindings -> tactic) -> + constr with_ebindings induction_arg -> tactic + (*s Introduction tactics with eliminations. *) val intro_pattern : identifier option -> intro_pattern_expr -> tactic |