diff options
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/equality.ml | 79 | ||||
| -rw-r--r-- | tactics/hiddentac.ml | 3 | ||||
| -rw-r--r-- | tactics/hiddentac.mli | 2 | ||||
| -rw-r--r-- | tactics/hipattern.ml4 | 67 | ||||
| -rw-r--r-- | tactics/hipattern.mli | 22 | ||||
| -rw-r--r-- | tactics/rewrite.ml4 | 16 | ||||
| -rw-r--r-- | tactics/tacinterp.ml | 6 | ||||
| -rw-r--r-- | tactics/tactics.ml | 176 | ||||
| -rw-r--r-- | tactics/tactics.mli | 34 |
9 files changed, 227 insertions, 178 deletions
diff --git a/tactics/equality.ml b/tactics/equality.ml index ce0677caef..101e7ef8c2 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -632,10 +632,9 @@ let apply_on_clause (f,t) clause = | _ -> 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 discr_positions env sigma (lbeq,eqn,(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 @@ -645,8 +644,8 @@ let discr_positions env sigma (lbeq,(t,t1,t2)) eq_clause cpath dirn sort = tclTHENS (cut_intro absurd_term) [onLastHypId gen_absurdity; refine pf] -let discrEq (lbeq,(t,t1,t2) as u) eq_clause gls = - let sigma = eq_clause.evd in +let discrEq (lbeq,_,(t,t1,t2) as u) eq_clause gls = + let sigma = eq_clause.evd in let env = pf_env gls in match find_positions env sigma t1 t2 with | Inr _ -> @@ -655,19 +654,26 @@ let discrEq (lbeq,(t,t1,t2) as u) eq_clause gls = let sort = pf_apply get_type_of gls (pf_concl gls) in discr_positions env sigma u eq_clause cpath dirn sort gls +let extract_main_eq_args gl = function + | MonomorphicLeibnizEq (e1,e2) -> let t = pf_type_of gl e1 in (t,e1,e2) + | PolymorphicLeibnizEq (t,e1,e2) -> (t,e1,e2) + | HeterogenousEq (t1,e1,t2,e2) -> + if pf_conv_x gl t1 t2 then (t1,e1,e2) + else error"Don't know what to do with JMeq on arguments not of same type." + 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 = + let eq,eq_args = try find_eq_data_decompose eqn with PatternMatchingFailure -> errorlabstrm "" (str"No primitive equality found.") in tclTHEN (Refiner.tclEVARS eq_clause'.evd) - (tac eq eq_clause') gls + (tac (eq,eqn,extract_main_eq_args gls eq_args) eq_clause') gls let onNegatedEquality with_evars tac gls = let ccl = pf_concl gls in @@ -688,7 +694,9 @@ let discr with_evars = onEquality with_evars discrEq let discrClause with_evars = onClause (discrSimpleClause with_evars) let discrEverywhere with_evars = +(* tclORELSE +*) (if !discr_do_intro then (tclTHEN (tclREPEAT introf) @@ -696,9 +704,9 @@ let discrEverywhere with_evars = (fun id -> tclCOMPLETE (discr with_evars (mkVar id,NoBindings))))) else (* <= 8.2 compat *) Tacticals.tryAllHypsAndConcl (discrSimpleClause with_evars)) - (fun gls -> +(* (fun gls -> errorlabstrm "DiscrEverywhere" (str"No discriminable equalities.")) - +*) let discr_tac with_evars = function | None -> discrEverywhere with_evars | Some c -> onInductionArg (discr with_evars) c @@ -926,7 +934,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)) eq_clause 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 = @@ -951,8 +959,8 @@ let inject_at_positions env sigma (eq,(t,t1,t2)) eq_clause posns = exception Not_dep_pair -let injEq ipats (eq,(t,t1,t2)) eq_clause = - let sigma = eq_clause.evd in +let injEq ipats (eq,_,(t,t1,t2) as u) eq_clause = + let sigma = eq_clause.evd in let env = eq_clause.env in match find_positions env sigma t1 t2 with | Inl _ -> @@ -1000,7 +1008,7 @@ let injEq ipats (eq,(t,t1,t2)) eq_clause = ) else (raise Not_dep_pair) ) with _ -> tclTHEN - (inject_at_positions env sigma (eq,(t,t1,t2)) eq_clause posns) + (inject_at_positions env sigma u eq_clause posns) (intros_pattern no_move ipats) let inj ipats with_evars = onEquality with_evars (injEq ipats) @@ -1012,7 +1020,7 @@ let injClause ipats with_evars = function 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) clause 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 = clause.evd in let env = pf_env gls in @@ -1023,8 +1031,7 @@ let decompEqThen ntac (lbeq,(t,t1,t2) as u) clause gls = ntac 0 gls | Inr posns -> tclTHEN - (inject_at_positions env sigma (lbeq,(t,t1,t2)) clause - (List.rev posns)) + (inject_at_positions env sigma u clause (List.rev posns)) (ntac (List.length posns)) gls @@ -1034,14 +1041,26 @@ let dEqThen with_evars ntac = function let dEq with_evars = dEqThen with_evars (fun x -> tclIDTAC) +let swap_equality_args = function + | MonomorphicLeibnizEq (e1,e2) -> [e2;e1] + | PolymorphicLeibnizEq (t,e1,e2) -> [t;e2;e1] + | HeterogenousEq (t1,e1,t2,e2) -> [t2;e2;t1;e1] + +let get_equality_args = function + | MonomorphicLeibnizEq (e1,e2) -> [e1;e2] + | PolymorphicLeibnizEq (t,e1,e2) -> [t;e1;e2] + | HeterogenousEq (t1,e1,t2,e2) -> [t1;e1;t2;e2] + let swap_equands gls eqn = - let (lbeq,(t,e1,e2)) = find_eq_data_decompose eqn in - applist(lbeq.eq,[t;e2;e1]) + let (lbeq,eq_args) = find_eq_data_decompose eqn in + applist(lbeq.eq,swap_equality_args eq_args) let swapEquandsInConcl gls = - let (lbeq,(t,e1,e2)) = find_eq_data_decompose (pf_concl gls) in + let (lbeq,eq_args) = find_eq_data_decompose (pf_concl gls) in let sym_equal = lbeq.sym in - refine (applist(sym_equal,[t;e2;e1;Evarutil.mk_new_meta()])) gls + refine + (applist(sym_equal,(swap_equality_args eq_args@[Evarutil.mk_new_meta()]))) + gls (* Refine from [|- P e2] to [|- P e1] and [|- e1=e2:>t] (body is P (Rel 1)) *) @@ -1102,12 +1121,13 @@ let subst_tuple_term env sigma dep_pair b = (fun (e,t) body -> lambda_create env (t,subst_term e body)) e_list b in beta_applist(abst_B,proj_list) -(* Comme "replace" mais decompose les egalites dependantes *) +(* Like "replace" but decompose dependent equalities *) exception NothingToRewrite let cutSubstInConcl_RL eqn gls = - let (lbeq,(t,e1,e2 as eq)) = find_eq_data_decompose eqn in + let (lbeq,eq_args) = find_eq_data_decompose eqn in + let (t,e1,e2 as eq) = extract_main_eq_args gls eq_args in let body = pf_apply subst_tuple_term gls e2 (pf_concl gls) in if not (dependent (mkRel 1) body) then raise NothingToRewrite; bareRevSubstInConcl lbeq body eq gls @@ -1125,7 +1145,8 @@ let cutSubstInConcl_LR eqn gls = let cutSubstInConcl l2r =if l2r then cutSubstInConcl_LR else cutSubstInConcl_RL let cutSubstInHyp_LR eqn id gls = - let (lbeq,(t,e1,e2 as eq)) = find_eq_data_decompose eqn in + let (lbeq,eq_args) = find_eq_data_decompose eqn in + let (t,e1,e2 as eq) = extract_main_eq_args gls eq_args in let body = pf_apply subst_tuple_term gls e1 (pf_get_hyp_typ gls id) in if not (dependent (mkRel 1) body) then raise NothingToRewrite; cut_replacing id (subst1 e2 body) @@ -1208,9 +1229,9 @@ let unfold_body x 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) = +let is_eq_x gl x (id,_,c) = try - let (_,lhs,rhs) = snd (find_eq_data_decompose c) in + let (_,lhs,rhs) = extract_main_eq_args gl (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 -> @@ -1226,7 +1247,7 @@ let subst_one x gl = (* Find a non-recursive definition for x *) let (hyp,rhs,dir) = try - let test hyp _ = is_eq_x varx hyp in + let test hyp _ = is_eq_x gl varx hyp in Sign.fold_named_context test ~init:() hyps; errorlabstrm "Subst" (str "Cannot find any non-recursive equality over " ++ pr_id x ++ @@ -1274,7 +1295,7 @@ let subst ids = tclTHEN tclNORMEVAR (tclMAP subst_one ids) let subst_all gl = let test (_,c) = try - let (_,x,y) = snd (find_eq_data_decompose c) in + let (_,x,y) = extract_main_eq_args gl (snd (find_eq_data_decompose c)) in (* J.F.: added to prevent failure on goal containing x=x as an hyp *) if eq_constr x y then failwith "caught"; match kind_of_term x with Var x -> x | _ -> @@ -1291,19 +1312,19 @@ let subst_all gl = let cond_eq_term_left c t gl = try - let (_,x,_) = snd (find_eq_data_decompose t) in + let (_,x,_) = extract_main_eq_args gl (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 + let (_,_,x) = extract_main_eq_args gl (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 + let (_,x,y) = extract_main_eq_args gl (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" diff --git a/tactics/hiddentac.ml b/tactics/hiddentac.ml index b85491c57d..65a56100bf 100644 --- a/tactics/hiddentac.ml +++ b/tactics/hiddentac.ml @@ -128,7 +128,8 @@ let h_change oc c cl = let h_reflexivity = abstract_tactic TacReflexivity intros_reflexivity let h_symmetry c = abstract_tactic (TacSymmetry c) (intros_symmetry c) let h_transitivity c = - abstract_tactic (TacTransitivity (inj_open c)) (intros_transitivity c) + abstract_tactic (TacTransitivity (Option.map inj_open c)) + (intros_transitivity c) let h_simplest_apply c = h_apply false false [inj_open c,NoBindings] let h_simplest_eapply c = h_apply false true [inj_open c,NoBindings] diff --git a/tactics/hiddentac.mli b/tactics/hiddentac.mli index 5aafb91a0d..f5b2dbb552 100644 --- a/tactics/hiddentac.mli +++ b/tactics/hiddentac.mli @@ -113,7 +113,7 @@ val h_change : (* Equivalence relations *) val h_reflexivity : tactic val h_symmetry : Tacticals.clause -> tactic -val h_transitivity : constr -> tactic +val h_transitivity : constr option -> tactic val h_simplest_apply : constr -> tactic val h_simplest_eapply : constr -> tactic diff --git a/tactics/hipattern.ml4 b/tactics/hipattern.ml4 index 7086e44219..0b81a492ac 100644 --- a/tactics/hipattern.ml4 +++ b/tactics/hipattern.ml4 @@ -219,28 +219,47 @@ let is_unit_type t = inductive binary relation R, so that R has only one constructor establishing its reflexivity. *) -let coq_refl_rel1_pattern = PATTERN [ forall A:_, forall x:A, _ A x x ] -let coq_refl_rel2_pattern = PATTERN [ forall x:_, _ x x ] -let coq_refl_reljm_pattern = PATTERN [ forall A:_, forall x:A, _ A x A x ] +type equation_kind = + | MonomorphicLeibnizEq of constr * constr + | PolymorphicLeibnizEq of constr * constr * constr + | HeterogenousEq of constr * constr * constr * constr + +exception NoEquationFound + +let coq_refl_leibniz1_pattern = PATTERN [ forall x:_, _ x x ] +let coq_refl_leibniz2_pattern = PATTERN [ forall A:_, forall x:A, _ A x x ] +let coq_refl_jm_pattern = PATTERN [ forall A:_, forall x:A, _ A x A x ] + +open Libnames let match_with_equation t = - let (hdapp,args) = decompose_app t in - match (kind_of_term hdapp) with - | Ind ind -> + if not (isApp t) then raise NoEquationFound; + let (hdapp,args) = destApp t in + match kind_of_term hdapp with + | Ind ind -> + if IndRef ind = glob_eq then + Some (build_coq_eq_data()),hdapp, + PolymorphicLeibnizEq(args.(0),args.(1),args.(2)) + else if IndRef ind = glob_identity then + Some (build_coq_identity_data()),hdapp, + PolymorphicLeibnizEq(args.(0),args.(1),args.(2)) + else if IndRef ind = glob_jmeq then + Some (build_coq_jmeq_data()),hdapp, + HeterogenousEq(args.(0),args.(1),args.(2),args.(3)) + else 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) + if nconstr = 1 then + if is_matching coq_refl_leibniz1_pattern constr_types.(0) then + None, hdapp, MonomorphicLeibnizEq(args.(0),args.(1)) + else if is_matching coq_refl_leibniz2_pattern constr_types.(0) then + None, hdapp, PolymorphicLeibnizEq(args.(0),args.(1),args.(2)) + else if is_matching coq_refl_jm_pattern constr_types.(0) then + None, hdapp, HeterogenousEq(args.(0),args.(1),args.(2),args.(3)) + else raise NoEquationFound + else raise NoEquationFound + | _ -> raise NoEquationFound let match_with_equality_type t = let (hdapp,args) = decompose_app t in @@ -255,6 +274,8 @@ let match_with_equality_type t = None | _ -> None +let is_equality_type t = op2bool (match_with_equality_type t) + let coq_arrow_pattern = PATTERN [ ?X1 -> ?X2 ] let match_arrow_pattern t = @@ -333,16 +354,22 @@ let rec first_match matcher = function let coq_eq_pattern_gen eq = lazy PATTERN [ %eq ?X1 ?X2 ?X3 ] let coq_eq_pattern = coq_eq_pattern_gen coq_eq_ref let coq_identity_pattern = coq_eq_pattern_gen coq_identity_ref +let coq_jmeq_pattern = lazy PATTERN [ %coq_jmeq_ref ?X1 ?X2 ?X3 ?X4 ] let match_eq eqn eq_pat = - match matches (Lazy.force eq_pat) eqn with + let pat = try Lazy.force eq_pat with _ -> raise PatternMatchingFailure in + match matches 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" + PolymorphicLeibnizEq (t,x,y) + | [(m1,t);(m2,x);(m3,t');(m4,x')] -> + assert (m1 = meta1 & m2 = meta2 & m3 = meta3 & m4 = meta4); + HeterogenousEq (t,x,t',x') + | _ -> anomaly "match_eq: an eq pattern should match 3 or 4 terms" let equalities = [coq_eq_pattern, build_coq_eq_data; + coq_jmeq_pattern, build_coq_jmeq_data; coq_identity_pattern, build_coq_identity_data] let find_eq_data_decompose eqn = (* fails with PatternMatchingFailure *) diff --git a/tactics/hipattern.mli b/tactics/hipattern.mli index 3418dd208e..5be8b20264 100644 --- a/tactics/hipattern.mli +++ b/tactics/hipattern.mli @@ -16,6 +16,7 @@ open Sign open Evd open Pattern open Proof_trees +open Coqlib (*i*) (*s Given a term with second-order variables in it, @@ -81,11 +82,9 @@ val is_unit_or_eq_type : testing_function (* type with only one constructor and no arguments, no indices *) val is_unit_type : testing_function -val match_with_equation : (constr * constr list) matching_function -val is_equation : testing_function - (* type with only one constructor, no arguments and at least one dependency *) val match_with_equality_type : (constr * constr list) matching_function +val is_equality_type : testing_function val match_with_nottype : (constr * constr) matching_function val is_nottype : testing_function @@ -110,14 +109,23 @@ 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 *) +(* Recongnize inductive relation defined by reflexivity *) -open Coqlib +type equation_kind = + | MonomorphicLeibnizEq of constr * constr + | PolymorphicLeibnizEq of constr * constr * constr + | HeterogenousEq of constr * constr * constr * constr + +exception NoEquationFound + +val match_with_equation: + constr -> coq_eq_data option * constr * equation_kind + +(***** Destructing patterns bound to some theory *) (* Match terms [(eq A t u)] or [(identity A t u)] *) (* Returns associated lemmas and [A,t,u] *) -val find_eq_data_decompose : constr -> - coq_leibniz_eq_data * (constr * constr * constr) +val find_eq_data_decompose : constr -> coq_eq_data * equation_kind (* Match a term of the form [(existT A P t p)] *) (* Returns associated lemmas and [A,P,t,p] *) diff --git a/tactics/rewrite.ml4 b/tactics/rewrite.ml4 index 52f10d46c6..43ae99203d 100644 --- a/tactics/rewrite.ml4 +++ b/tactics/rewrite.ml4 @@ -1390,9 +1390,8 @@ let setoid_proof gl ty fn fallback = let evm, car = project gl, pf_type_of gl args.(0) in fn env evm car rel gl with e -> - match fallback gl with - | Some tac -> tac gl - | None -> + try fallback gl + with Hipattern.NoEquationFound -> match e with | Not_found -> let rel, args = relation_of_constr env (pf_concl gl) in @@ -1412,9 +1411,11 @@ let setoid_symmetry gl = let setoid_transitivity c gl = setoid_proof gl "transitive" (fun env evm car rel -> - apply_with_bindings - ((get_transitive_proof env evm car rel), - Rawterm.ExplicitBindings [ dummy_loc, Rawterm.NamedHyp (id_of_string "y"), c ])) + let proof = get_transitive_proof env evm car rel in + match c with + | None -> eapply proof + | Some c -> + apply_with_bindings (proof,Rawterm.ExplicitBindings [ dummy_loc, Rawterm.NamedHyp (id_of_string "y"), c ])) (transitivity_red true c) let setoid_symmetry_in id gl = @@ -1450,7 +1451,8 @@ TACTIC EXTEND setoid_reflexivity END TACTIC EXTEND setoid_transitivity -[ "setoid_transitivity" constr(t) ] -> [ setoid_transitivity t ] + [ "setoid_transitivity" constr(t) ] -> [ setoid_transitivity (Some t) ] +| [ "setoid_etransitivity" ] -> [ setoid_transitivity None ] END let implify id gl = diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index 41ec5dc07b..e436fc90f5 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -798,7 +798,7 @@ let rec intern_atomic lf ist x = | TacReflexivity -> TacReflexivity | TacSymmetry idopt -> TacSymmetry (clause_app (intern_hyp_location ist) idopt) - | TacTransitivity c -> TacTransitivity (intern_constr ist c) + | TacTransitivity c -> TacTransitivity (Option.map (intern_constr ist) c) (* Equality and inversion *) | TacRewrite (ev,l,cl,by) -> @@ -2338,7 +2338,7 @@ and interp_atomic ist gl = function (* Equivalence relations *) | TacReflexivity -> h_reflexivity | TacSymmetry c -> h_symmetry (interp_clause ist gl c) - | TacTransitivity c -> h_transitivity (pf_interp_constr ist gl c) + | TacTransitivity c -> h_transitivity (Option.map (pf_interp_constr ist gl) c) (* Equality and inversion *) | TacRewrite (ev,l,cl,by) -> @@ -2652,7 +2652,7 @@ let rec subst_atomic subst (t:glob_atomic_tactic_expr) = match t with (* Equivalence relations *) | TacReflexivity | TacSymmetry _ as x -> x - | TacTransitivity c -> TacTransitivity (subst_rawconstr subst c) + | TacTransitivity c -> TacTransitivity (Option.map (subst_rawconstr subst) c) (* Equality and inversion *) | TacRewrite (ev,l,cl,by) -> diff --git a/tactics/tactics.ml b/tactics/tactics.ml index e96806de1c..0224da6c87 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -905,16 +905,13 @@ let eapply_with_bindings (c,bl) = let apply c = apply_with_ebindings (inj_open c,NoBindings) +let eapply c = + eapply_with_ebindings (inj_open c,NoBindings) + let apply_list = function | c::l -> apply_with_bindings (c,ImplicitBindings l) | _ -> assert false -(* Resolution with no reduction on the type (used ?) *) - -let apply_without_reduce c gl = - let clause = mk_clenv_type_of gl c in - res_pf clause gl - (* [apply_in hyp c] replaces hyp : forall y1, ti -> t hyp : rho(u) @@ -2116,9 +2113,6 @@ let mkHRefl t x = (* mkApp (coq_constant "mkHEq" ["Logic";"EqdepFacts"] "eq_dep_intro", *) (* [| ty; mkApp (Lazy.force id, [|ty|]); t; x |]) *) -let mkCoe a x p px y eq = - mkApp (Option.get (build_coq_eq_data ()).rect, [| a; x; p; px; y; eq |]) - let lift_togethern n l = let l', _ = List.fold_right @@ -3059,13 +3053,11 @@ let reflexivity_red allowred gl = else whd_betadeltaiota (pf_env gl) (project gl) (pf_concl gl) in match match_with_equality_type concl with - | None -> None - | Some _ -> Some (one_constructor 1 NoBindings) + | None -> raise NoEquationFound + | Some _ -> one_constructor 1 NoBindings gl -let reflexivity gl = - match reflexivity_red false gl with - | None -> !setoid_reflexivity gl - | Some tac -> tac gl +let reflexivity gl = + try reflexivity_red false gl with NoEquationFound -> !setoid_reflexivity gl let intros_reflexivity = (tclTHEN intros reflexivity) @@ -3079,41 +3071,35 @@ let intros_reflexivity = (tclTHEN intros reflexivity) let setoid_symmetry = ref (fun _ -> assert false) let register_setoid_symmetry f = setoid_symmetry := f +(* This is probably not very useful any longer *) +let prove_symmetry hdcncl eq_kind = + let symc = + match eq_kind with + | MonomorphicLeibnizEq (c1,c2) -> mkApp(hdcncl,[|c2;c1|]) + | PolymorphicLeibnizEq (typ,c1,c2) -> mkApp(hdcncl,[|typ;c2;c1|]) + | HeterogenousEq (t1,c1,t2,c2) -> mkApp(hdcncl,[|t2;c2;t1;c1|]) in + tclTHENFIRST (cut symc) + (tclTHENLIST + [ intro; + onLastHyp simplest_case; + one_constructor 1 NoBindings ]) + let symmetry_red allowred gl = (* PL: usual symmetry don't perform any reduction when searching for an equality, but we may need to do some when called back from inside setoid_reflexivity (see Optimize cases in setoid_replace.ml). *) - let concl = if not allowred then pf_concl gl - else whd_betadeltaiota (pf_env gl) (project gl) (pf_concl gl) + let concl = + if not allowred then pf_concl gl else pf_whd_betadeltaiota gl (pf_concl gl) in - match match_with_equation concl with - | None -> None - | Some (hdcncl,args) -> Some (fun gl -> - let hdcncls = string_of_inductive hdcncl in - begin - try - tclTHEN - (convert_concl_no_check concl DEFAULTcast) - (apply (pf_parse_const gl ("sym_"^hdcncls))) gl - with _ -> - let symc = match args with - | [t1; c1; t2; c2] -> mkApp (hdcncl, [| t2; c2; t1; c1 |]) - | [typ;c1;c2] -> mkApp (hdcncl, [| typ; c2; c1 |]) - | [c1;c2] -> mkApp (hdcncl, [| c2; c1 |]) - | _ -> assert false - in - tclTHENFIRST (cut symc) - (tclTHENLIST - [ intro; - onLastHyp simplest_case; - one_constructor 1 NoBindings ]) - gl - end) - -let symmetry gl = - match symmetry_red false gl with - | None -> !setoid_symmetry gl - | Some tac -> tac gl + match match_with_equation concl with + | Some eq_data,_,_ -> + tclTHEN + (convert_concl_no_check concl DEFAULTcast) + (apply eq_data.sym) gl + | None,eq,eq_kind -> prove_symmetry eq eq_kind gl + +let symmetry gl = + try symmetry_red false gl with NoEquationFound -> !setoid_symmetry gl let setoid_symmetry_in = ref (fun _ _ -> assert false) let register_setoid_symmetry_in f = setoid_symmetry_in := f @@ -3121,18 +3107,17 @@ let register_setoid_symmetry_in f = setoid_symmetry_in := f let symmetry_in id gl = let ctype = pf_type_of gl (mkVar id) in let sign,t = decompose_prod_assum ctype in - match match_with_equation t with - | None -> !setoid_symmetry_in id gl - | Some (hdcncl,args) -> - let symccl = match args with - | [t1; c1; t2; c2] -> mkApp (hdcncl, [| t2; c2; t1; c1 |]) - | [typ;c1;c2] -> mkApp (hdcncl, [| typ; c2; c1 |]) - | [c1;c2] -> mkApp (hdcncl, [| c2; c1 |]) - | _ -> assert false in - tclTHENS (cut (it_mkProd_or_LetIn symccl sign)) - [ intro_replacing id; - tclTHENLIST [ intros; symmetry; apply (mkVar id); assumption ] ] - gl + try + let _,hdcncl,eq = match_with_equation t in + let symccl = match eq with + | MonomorphicLeibnizEq (c1,c2) -> mkApp (hdcncl, [| c2; c1 |]) + | PolymorphicLeibnizEq (typ,c1,c2) -> mkApp (hdcncl, [| typ; c2; c1 |]) + | HeterogenousEq (t1,c1,t2,c2) -> mkApp (hdcncl, [| t2; c2; t1; c1 |]) in + tclTHENS (cut (it_mkProd_or_LetIn symccl sign)) + [ intro_replacing id; + tclTHENLIST [ intros; symmetry; apply (mkVar id); assumption ] ] + gl + with NoEquationFound -> !setoid_symmetry_in id gl let intros_symmetry = onClause @@ -3155,47 +3140,52 @@ let intros_symmetry = let setoid_transitivity = ref (fun _ _ -> assert false) let register_setoid_transitivity f = setoid_transitivity := f +(* This is probably not very useful any longer *) +let prove_transitivity hdcncl eq_kind t gl = + let eq1,eq2 = + match eq_kind with + | MonomorphicLeibnizEq (c1,c2) -> + (mkApp (hdcncl, [| c1; t|]), mkApp (hdcncl, [| t; c2 |])) + | PolymorphicLeibnizEq (typ,c1,c2) -> + (mkApp (hdcncl, [| typ; c1; t |]), mkApp (hdcncl, [| typ; t; c2 |])) + | HeterogenousEq (typ1,c1,typ2,c2) -> + let typt = pf_type_of gl t in + (mkApp(hdcncl, [| typ1; c1; typt ;t |]), + mkApp(hdcncl, [| typt; t; typ2; c2 |])) in + tclTHENFIRST (cut eq2) + (tclTHENFIRST (cut eq1) + (tclTHENLIST + [ tclDO 2 intro; + onLastHyp simplest_case; + assumption ])) gl + let transitivity_red allowred t gl = (* PL: usual transitivity don't perform any reduction when searching for an equality, but we may need to do some when called back from inside setoid_reflexivity (see Optimize cases in setoid_replace.ml). *) - let concl = if not allowred then pf_concl gl - else whd_betadeltaiota (pf_env gl) (project gl) (pf_concl gl) - in + let concl = + if not allowred then pf_concl gl else pf_whd_betadeltaiota gl (pf_concl gl) + in match match_with_equation concl with - | None -> None - | Some (hdcncl,args) -> Some (fun gl -> - let hdcncls = string_of_inductive hdcncl in - begin - try - apply_list [(pf_parse_const gl ("trans_"^hdcncls));t] gl - with _ -> - let eq1, eq2 = match args with - | [typ1;c1;typ2;c2] -> let typt = pf_type_of gl t in - ( mkApp(hdcncl, [| typ1; c1; typt ;t |]), - mkApp(hdcncl, [| typt; t; typ2; c2 |]) ) - | [typ;c1;c2] -> - ( mkApp (hdcncl, [| typ; c1; t |]), - mkApp (hdcncl, [| typ; t; c2 |]) ) - | [c1;c2] -> - ( mkApp (hdcncl, [| c1; t|]), - mkApp (hdcncl, [| t; c2 |]) ) - | _ -> assert false - in - tclTHENFIRST (cut eq2) - (tclTHENFIRST (cut eq1) - (tclTHENLIST - [ tclDO 2 intro; - onLastHyp simplest_case; - assumption ])) gl - end) - -let transitivity t gl = - match transitivity_red false t gl with - | None -> !setoid_transitivity t gl - | Some tac -> tac gl - -let intros_transitivity n = tclTHEN intros (transitivity n) + | Some eq_data,_,_ -> + tclTHEN + (convert_concl_no_check concl DEFAULTcast) + (match t with + | None -> eapply eq_data.trans + | Some t -> apply_list [eq_data.trans;t]) gl + | None,eq,eq_kind -> + match t with + | None -> error "etransitivity not supported for this relation." + | Some t -> prove_transitivity eq eq_kind t gl + +let transitivity_gen t gl = + try transitivity_red false t gl + with NoEquationFound -> !setoid_transitivity t gl + +let etransitivity = transitivity_gen None +let transitivity t = transitivity_gen (Some t) + +let intros_transitivity n = tclTHEN intros (transitivity_gen n) (* tactical to save as name a subproof such that the generalisation of the current goal, abstracted with respect to the local signature, diff --git a/tactics/tactics.mli b/tactics/tactics.mli index 355380a74c..40740c3a82 100644 --- a/tactics/tactics.mli +++ b/tactics/tactics.mli @@ -176,10 +176,9 @@ val apply_type : constr -> constr list -> tactic val apply_term : constr -> constr list -> tactic val bring_hyps : named_context -> tactic -val apply : constr -> tactic -val apply_without_reduce : constr -> tactic -val apply_list : constr list -> tactic - +val apply : constr -> tactic +val eapply : constr -> tactic + val apply_with_ebindings_gen : advanced_flag -> evars_flag -> open_constr with_ebindings list -> tactic @@ -271,8 +270,8 @@ val simple_induct : quantified_hypothesis -> tactic val new_induct : evars_flag -> constr with_ebindings induction_arg list -> constr with_ebindings option -> - intro_pattern_expr located option * intro_pattern_expr located option -> - clause option -> tactic + intro_pattern_expr located option * intro_pattern_expr located option -> + clause option -> tactic (*s Case analysis tactics. *) @@ -282,16 +281,16 @@ val simplest_case : constr -> tactic val simple_destruct : quantified_hypothesis -> tactic val new_destruct : evars_flag -> constr with_ebindings induction_arg list -> constr with_ebindings option -> - intro_pattern_expr located option * intro_pattern_expr located option -> - clause option -> tactic + intro_pattern_expr located option * intro_pattern_expr located option -> + clause option -> tactic (*s Generic case analysis / induction tactics. *) val induction_destruct : evars_flag -> rec_flag -> (constr with_ebindings induction_arg list * - constr with_ebindings option * - (intro_pattern_expr located option * intro_pattern_expr located option) * - clause option) list -> + constr with_ebindings option * + (intro_pattern_expr located option * intro_pattern_expr located option) * + clause option) list -> tactic (*s Eliminations giving the type instead of the proof. *) @@ -312,7 +311,7 @@ val dorE : bool -> clause ->tactic (*s Introduction tactics. *) val constructor_tac : evars_flag -> int option -> int -> - open_constr bindings -> tactic + open_constr bindings -> tactic val any_constructor : evars_flag -> tactic option -> tactic val one_constructor : int -> open_constr bindings -> tactic @@ -331,21 +330,22 @@ val simplest_split : tactic (*s Logical connective tactics. *) val register_setoid_reflexivity : tactic -> unit -val reflexivity_red : bool -> goal sigma -> tactic option +val reflexivity_red : bool -> tactic val reflexivity : tactic val intros_reflexivity : tactic val register_setoid_symmetry : tactic -> unit -val symmetry_red : bool -> goal sigma -> tactic option +val symmetry_red : bool -> tactic val symmetry : tactic val register_setoid_symmetry_in : (identifier -> tactic) -> unit val symmetry_in : identifier -> tactic val intros_symmetry : clause -> tactic -val register_setoid_transitivity : (constr -> tactic) -> unit -val transitivity_red : bool -> constr -> goal sigma -> tactic option +val register_setoid_transitivity : (constr option -> tactic) -> unit +val transitivity_red : bool -> constr option -> tactic val transitivity : constr -> tactic -val intros_transitivity : constr -> tactic +val etransitivity : tactic +val intros_transitivity : constr option -> tactic val cut : constr -> tactic val cut_intro : constr -> tactic |