diff options
| -rw-r--r-- | contrib/subtac/equations.ml4 | 433 | ||||
| -rw-r--r-- | proofs/logic.ml | 2 | ||||
| -rw-r--r-- | test-suite/success/Equations.v | 105 | ||||
| -rw-r--r-- | theories/Program/Equality.v | 170 | ||||
| -rw-r--r-- | theories/Program/Tactics.v | 35 |
5 files changed, 529 insertions, 216 deletions
diff --git a/contrib/subtac/equations.ml4 b/contrib/subtac/equations.ml4 index 14330e72e..f3f0e052b 100644 --- a/contrib/subtac/equations.ml4 +++ b/contrib/subtac/equations.ml4 @@ -37,21 +37,27 @@ open Libnames type pat = | PRel of int | PCstr of constructor * pat list - | PInnac of constr - -let rec constr_of_pat = function + | PInac of constr + +let coq_inacc = lazy (Coqlib.gen_constant "equations" ["Program";"Equality"] "inaccessible_pattern") + +let mkInac env c = + mkApp (Lazy.force coq_inacc, [| Typing.type_of env Evd.empty c ; c |]) + +let rec constr_of_pat ?(inacc=true) env = function | PRel i -> mkRel i | PCstr (c, p) -> let c' = mkConstruct c in - mkApp (c', Array.of_list (constrs_of_pats p)) - | PInnac r -> r + mkApp (c', Array.of_list (constrs_of_pats ~inacc env p)) + | PInac r -> + if inacc then try mkInac env r with _ -> r else r -and constrs_of_pats l = map constr_of_pat l +and constrs_of_pats ?(inacc=true) env l = map (constr_of_pat ~inacc env) l let rec pat_vars = function | PRel i -> Intset.singleton i | PCstr (c, p) -> pats_vars p - | PInnac _ -> Intset.empty + | PInac _ -> Intset.empty and pats_vars l = fold_left (fun vars p -> @@ -67,32 +73,51 @@ let rec pats_of_constrs l = map pat_of_constr l and pat_of_constr c = match kind_of_term c with | Rel i -> PRel i - | App (f, args) when isConstruct f -> + | App (f, [| a ; c |]) when eq_constr f (Lazy.force coq_inacc) -> + PInac c + | App (f, args) when isConstruct f -> PCstr (destConstruct f, pats_of_constrs (Array.to_list args)) | Construct f -> PCstr (f, []) - | _ -> PInnac c + | _ -> PInac c -let innacs_of_constrs l = map (fun x -> PInnac x) l +let inaccs_of_constrs l = map (fun x -> PInac x) l exception Conflict let rec pmatch p c = - match p, kind_of_term c with - | PRel i, t -> [i, c] - | PCstr (c, pl), App (c', l') when kind_of_term c' = Construct c -> - pmatches pl (Array.to_list l') - | PCstr (c, []), Construct c' when c' = c -> [] - | PInnac _, _ -> [] - | _, _ -> raise Conflict + match p, c with + | PRel i, t -> true +(* | _, PRel i -> true *) + | PCstr (c, pl), PCstr (c', pl') when c = c' -> pmatches pl pl' + | PInac _, _ -> true + | _, _ -> false and pmatches pl l = match pl, l with - | [], [] -> [] - | hd :: tl, hd' :: tl' -> pmatch hd hd' @ pmatches tl tl' - | _ -> raise Conflict + | [], [] -> true + | hd :: tl, hd' :: tl' -> pmatch hd hd' && pmatches tl tl' + | _ -> false let pattern_matches pl l = pmatches pl l +(* let rec pmatch p c = *) +(* match p, kind_of_term c with *) +(* | PRel i, t -> true *) +(* | t, Rel n -> true *) +(* | PCstr (c, pl), App (c', l') when kind_of_term c' = Construct c -> *) +(* pmatches pl (Array.to_list l') *) +(* | PCstr (c, []), Construct c' when c' = c -> true *) +(* | PInac _, _ -> true *) +(* | _, _ -> false *) + +(* and pmatches pl l = *) +(* match pl, l with *) +(* | [], [] -> true *) +(* | hd :: tl, hd' :: tl' -> pmatch hd hd' && pmatches tl tl' *) +(* | _ -> false *) + +(* let pattern_matches pl l = pmatches pl l *) + (** Specialize by a substitution. *) let subst_tele s = replace_vars (List.map (fun (id, _, t) -> id, t) s) @@ -129,30 +154,30 @@ let rec lift_pat n k p = if i >= k then PRel (i + n) else p | PCstr(c, pl) -> PCstr (c, lift_pats n k pl) - | PInnac r -> PInnac (liftn n k r) + | PInac r -> PInac (liftn n k r) and lift_pats n k = map (lift_pat n k) -let rec subst_pat k t p = +let rec subst_pat env k t p = match p with | PRel i -> if i = k then t else if i > k then PRel (pred i) else p | PCstr(c, pl) -> - PCstr (c, subst_pats k t pl) - | PInnac r -> PInnac (substnl [constr_of_pat t] k r) + PCstr (c, subst_pats env k t pl) + | PInac r -> PInac (substnl [constr_of_pat ~inacc:false env t] (pred k) r) -and subst_pats k t = map (subst_pat k t) +and subst_pats env k t = map (subst_pat env k t) let rec specialize s p = match p with | PRel i -> - if mem_assoc i s then PInnac (assoc i s) + if mem_assoc i s then PInac (assoc i s) else p | PCstr(c, pl) -> PCstr (c, specialize_pats s pl) - | PInnac r -> PInnac (specialize_constr s r) + | PInac r -> PInac (specialize_constr s r) and specialize_constr s c = subst_rel_subst 0 s c and specialize_pats s = map (specialize s) @@ -170,36 +195,34 @@ type program = and signature = identifier * rel_context * constr -and clause = rel_context * constr list * (constr, identifier located) rhs +and clause = lhs * (constr, int) rhs -and lhs = pat list +and lhs = rel_context * identifier * pat list and ('a, 'b) rhs = | Program of 'a | Empty of 'b type splitting = - | Compute of rel_context * lhs * (constr, int) rhs - | Split of rel_context * lhs * int * inductive_family * + | Compute of clause + | Split of lhs * int * inductive_family * unification_result array * splitting option array - + and unification_result = - rel_context * rel_context * constr * pat * substitution option + rel_context * int * constr * pat * substitution option and substitution = (int * constr) list -type problem = rel_context * identifier * pat list - -(* let vars_of_tele = map (fun (id, _, _) -> mkVar id) *) +type problem = identifier * lhs let rels_of_tele tele = rel_list 0 (List.length tele) let patvars_of_tele tele = map (fun c -> PRel (destRel c)) (rels_of_tele tele) -let split_solves split (delta, id, pats) = +let split_solves split prob = match split with - | Compute (ctx, lhs, rhs) -> delta = ctx && pats = lhs - | Split (ctx, lhs, id, indf, us, ls) -> delta = ctx && pats = lhs + | Compute (lhs, rhs) -> lhs = prob + | Split (lhs, id, indf, us, ls) -> lhs = prob let ids_of_constr c = let rec aux vars c = @@ -244,21 +267,26 @@ let split_tele n ctx = | _ -> raise (Invalid_argument "split_tele") in aux [] n ctx -let add_var_subst subst n c = - if mem_assoc n subst then - if eq_constr (assoc n subst) c then subst - else raise Conflict - else (n, c) :: subst +let rec add_var_subst env subst n c = + if mem_assoc n subst then + let t = assoc n subst in + if eq_constr t c then subst + else unify env subst t c + else + let rel = mkRel n in + if rel = c then subst + else if dependent rel c then raise Conflict + else (n, c) :: subst -let rec unify env subst x y = +and unify env subst x y = match kind_of_term x, kind_of_term y with - | Rel n, _ -> add_var_subst subst n y - | _, Rel n -> add_var_subst subst n x + | Rel n, _ -> add_var_subst env subst n y + | _, Rel n -> add_var_subst env subst n x | App (c, l), App (c', l') when eq_constr c c' -> unify_constrs env subst (Array.to_list l) (Array.to_list l') | _, _ -> if eq_constr x y then subst else raise Conflict -and unify_constrs env subst l l' = +and unify_constrs (env : env) subst l l' = if List.length l = List.length l' then fold_left2 (unify env) subst l l' else raise Conflict @@ -266,7 +294,7 @@ and unify_constrs env subst l l' = let substituted_context subst ctx = let substitute_in_ctx n c ctx = let rec aux k after = function - | [] -> assert false + | [] -> [] | decl :: before -> if k = n then subst_rel_context 0 c (rev after) @ before else aux (succ k) (decl :: after) before @@ -292,7 +320,7 @@ let substituted_context subst ctx = let t' = lift (-k) t in (* caution, not always well defined *) let ctx' = substitute_in_ctx k t' ctx' in let rest' = substitute_in_subst k t' rest in - record_subst (pred k) (lift (-1) t); + record_subst (pred k) (liftn (-1) k t); aux ctx' rest' in let ctx' = aux ctx subst in @@ -304,65 +332,79 @@ let unify_type before ty = let envb = push_rel_context before (Global.env()) in let IndType (indf, args) = find_rectype envb Evd.empty ty in let ind, params = dest_ind_family indf in -(* let vs = params @ args in *) - let vs = args in + let vs = map (Reduction.whd_betadeltaiota envb) args in let cstrs = Inductiveops.arities_of_constructors envb ind in let cstrs = Array.mapi (fun i ty -> let ty = prod_applist ty params in let ctx, ty = decompose_prod_assum ty in + let ctx, ids = + let ids = ids_of_rel_context ctx in + fold_right (fun (n, b, t as decl) (acc, ids) -> + match n with Name _ -> (decl :: acc), ids + | Anonymous -> let id = next_name_away Anonymous ids in + ((Name id, b, t) :: acc), (id :: ids)) + ctx ([], ids) + in let env' = push_rel_context ctx (Global.env ()) in let IndType (indf, args) = find_rectype env' Evd.empty ty in let ind, params = dest_ind_family indf in let constr = applist (mkConstruct (ind, succ i), params @ rels_of_tele ctx) in - let constrpat = PCstr ((ind, succ i), innacs_of_constrs params @ patvars_of_tele ctx) in + let constrpat = PCstr ((ind, succ i), inaccs_of_constrs params @ patvars_of_tele ctx) in env', ctx, constr, constrpat, (* params @ *)args) cstrs in + let res = Array.map (fun (env', ctxc, c, cpat, us) -> - let beforelen = length before and ctxclen = length ctxc in - let fullctx = (* lift_contextn beforelen 1 *)ctxc @ before in -(* let c = liftn beforelen (succ ctxclen) c and cpat = lift_pat beforelen ctxclen cpat in *) + let _beforelen = length before and ctxclen = length ctxc in + let fullctx = ctxc @ before in try let fullenv = push_rel_context fullctx (Global.env ()) in - let vs' = map (lift ctxclen) vs - and us' = map (liftn beforelen (succ ctxclen)) us in - let subst = unify_constrs fullenv [] us' vs' in + let vs' = map (lift ctxclen) vs in + let subst = unify_constrs fullenv [] us vs' in let subst', ctx' = substituted_context subst fullctx in - (ctx', ctxc, c, cpat, Some subst') + (ctx', ctxclen, c, cpat, Some subst') with Conflict -> - (fullctx, ctxc, c, cpat, None)) cstrs, indf + (fullctx, ctxclen, c, cpat, None)) cstrs + in Some (res, indf) with Not_found -> (* not an inductive type *) - raise (Invalid_argument "unify_type: Not an inductive type") + None let rec id_of_rel n l = match n, l with | 0, (Name id, _, _) :: tl -> id | n, _ :: tl -> id_of_rel (pred n) tl | _, _ -> raise (Invalid_argument "id_of_rel") + +let constrs_of_lhs ?(inacc=true) env (ctx, _, pats) = + constrs_of_pats ~inacc (push_rel_context ctx env) pats let rec valid_splitting (f, delta, t, pats) tree = split_solves tree (delta, f, pats) && valid_splitting_tree (f, delta, t) tree and valid_splitting_tree (f, delta, t) = function - | Compute (ctx, lhs, Program rhs) -> - let subst = constrs_of_pats lhs in - ignore(check_judgment ctx rhs (substl subst t)); true + | Compute (lhs, Program rhs) -> + let subst = constrs_of_lhs ~inacc:false (Global.env ()) lhs in + ignore(check_judgment (pi1 lhs) rhs (substl subst t)); true - | Compute (ctx, lhs, Empty split) -> + | Compute ((ctx, id, lhs), Empty split) -> let before, (x, _, ty), after = split_context split ctx in - let unify, _ = unify_type before ty in + let unify = + match unify_type before ty with + | Some (unify, _) -> unify + | None -> assert false + in array_for_all (fun (_, _, _, _, x) -> x = None) unify - | Split (ctx, lhs, rel, indf, unifs, ls) -> + | Split ((ctx, id, lhs), rel, indf, unifs, ls) -> let before, (id, _, ty), after = split_tele (pred rel) ctx in - let unify, indf' = unify_type before ty in + let unify, indf' = Option.get (unify_type before ty) in assert(indf = indf'); if not (array_exists (fun (_, _, _, _, x) -> x <> None) unify) then false else let ok, splits = - Array.fold_left (fun (ok, splits as acc) (ctx', ctxc, cstr, cstrpat, subst) -> + Array.fold_left (fun (ok, splits as acc) (ctx', ctxlen, cstr, cstrpat, subst) -> match subst with | None -> acc | Some subst -> @@ -374,13 +416,15 @@ and valid_splitting_tree (f, delta, t) = function (* in *) let newdelta = subst_context subst (subst_rel_context 0 cstr - (lift_contextn (length ctxc) 0 after)) @ before in - let liftpats = lift_pats (length ctxc) rel lhs in - let newpats = specialize_pats subst (subst_pats rel cstrpat liftpats) in + (lift_contextn ctxlen 0 after)) @ before in + let liftpats = lift_pats ctxlen rel lhs in + let newpats = specialize_pats subst (subst_pats (Global.env ()) rel cstrpat liftpats) in (ok, (f, newdelta, newpats) :: splits)) (true, []) unify in - let subst = List.map2 (fun (id, _, _) x -> out_name id, x) delta (constrs_of_pats lhs) in + let subst = List.map2 (fun (id, _, _) x -> out_name id, x) delta + (constrs_of_pats ~inacc:false (Global.env ()) lhs) + in let t' = replace_vars subst t in ok && for_all (fun (f, delta', pats') -> @@ -389,23 +433,17 @@ and valid_splitting_tree (f, delta, t) = function let valid_tree (f, delta, t) tree = valid_splitting (f, delta, t, patvars_of_tele delta) tree -let find_split curpats patcs = +let find_split (_, _, curpats : lhs) (_, _, patcs : lhs) = let rec find_split_pat curpat patc = - match kind_of_term patc with - | Rel _ -> (* The pattern's a variable, don't split *) None - | App (f, args) when isConstruct f -> - let f = destConstruct f in - (match curpat with - | PCstr (f', args') when f = f' -> (* Already split at this level, continue *) - find_split_pats args' (Array.to_list args) - | PRel i -> (* Split on i *) Some i - | _ -> None) - | Construct f -> + match patc with + | PRel _ -> (* The pattern's a variable, don't split *) None + | PCstr (f, args) -> (match curpat with - | PCstr (f', []) when f = f' -> (* Already split at this level, no args *) None + | PCstr (f', args') when f = f' -> (* Already split at this level, continue *) + find_split_pats args' args | PRel i -> (* Split on i *) Some i | _ -> None) - | _ -> None + | PInac _ -> None and find_split_pats curpats patcs = assert(List.length curpats = List.length patcs); @@ -424,45 +462,81 @@ let pr_constr_pat env c = | App _ -> str "(" ++ pr ++ str ")" | _ -> pr -let pr_clause env (delta, patcs, rhs) = +let pr_pat env c = + try + let patc = constr_of_pat env c in + try pr_constr_pat env patc with _ -> str"pr_constr_pat raised an exception" + with _ -> str"constr_of_pat raised an exception" + +let pr_context env c = + let pr_decl (id,b,_) = match id with Name id -> pr_id id | Anonymous -> str"_" in + prlist_with_sep pr_spc pr_decl (List.rev c) +(* Printer.pr_rel_context env c *) + +let pr_lhs env (delta, f, patcs) = let env = push_rel_context delta env in - prlist_with_sep spc (pr_constr_pat env) patcs + let ctx = pr_context env delta in + (if delta = [] then ctx else str "[" ++ ctx ++ str "]" ++ spc ()) + ++ pr_id f ++ spc () ++ prlist_with_sep spc (pr_pat env) patcs + +let pr_rhs env = function + | Empty var -> spc () ++ str ":=!" ++ spc () ++ print_constr_env env (mkRel var) + | Program rhs -> spc () ++ str ":=" ++ spc () ++ print_constr_env env rhs + +let pr_clause env (lhs, rhs) = + pr_lhs env lhs ++ + (let env' = push_rel_context (pi1 lhs) env in + pr_rhs env' rhs) + +(* let pr_splitting env = function *) +(* | Compute cl -> str "Compute " ++ pr_clause env cl *) +(* | Split (lhs, n, indf, results, splits) -> *) + +(* let pr_unification_result (ctx, n, c, pat, subst) = *) + +(* unification_result array * splitting option array *) let pr_clauses env = prlist_with_sep fnl (pr_clause env) + + +let lhs_matches (delta, _, patcs : lhs) (delta', _, patcs' : lhs) = + pattern_matches patcs patcs' -let rec split_on env fdt var delta curpats clauses = +let rec split_on env var (delta, f, curpats as lhs) clauses = let before, (id, _, ty), after = split_tele (pred var) delta in - let unify, indf = unify_type before ty in + let unify, indf = + match unify_type before ty with + | Some r -> r + | None -> assert false (* We decided... so it better be inductive *) + in let clauses = ref clauses in let splits = - Array.map (fun (ctx', ctxc, cstr, cstrpat, s) -> + Array.map (fun (ctx', ctxlen, cstr, cstrpat, s) -> match s with | None -> None | Some s -> (* ctx' |- s cstr, s cstrpat *) let newdelta = subst_context s (subst_rel_context 0 cstr - (lift_contextn (length ctxc) 1 after)) @ ctx' in + (lift_contextn ctxlen 1 after)) @ ctx' in let liftpats = (* delta |- curpats -> before; ctxc; id; after |- liftpats *) - lift_pats (length ctxc) (succ var) curpats + lift_pats ctxlen (succ var) curpats in let liftpat = (* before; ctxc |- cstrpat -> before; ctxc; after |- liftpat *) lift_pat (pred var) 1 cstrpat in let substpat = (* before; ctxc; after |- liftpats[id:=liftpat] *) - subst_pats var liftpat liftpats + subst_pats env var liftpat liftpats in let lifts = (* before; ctxc |- s : newdelta -> before; ctxc; after |- lifts : newdelta ; after *) map (fun (k,x) -> (pred var + k, lift (pred var) x)) s in let newpats = specialize_pats lifts substpat in - let matching, rest = partition (fun (delta', patcs, rhs) -> - try ignore(pattern_matches newpats patcs); true with Conflict -> false) - !clauses - in + let newlhs = (newdelta, f, newpats) in + let matching, rest = partition (fun (lhs, rhs) -> lhs_matches newlhs lhs) !clauses in clauses := rest; if matching = [] then ( (* Try finding a splittable variable *) @@ -471,43 +545,61 @@ let rec split_on env fdt var delta curpats clauses = match accid with | Some _ -> (accid, ctx) | None -> - let unify, indf = unify_type ctx ty in - if array_for_all (fun (_, _, _, _, x) -> x = None) unify then - (Some id, ctx) - else (None, decl :: ctx)) + match unify_type ctx ty with + | Some (unify, indf) -> + if array_for_all (fun (_, _, _, _, x) -> x = None) unify then + (Some id, ctx) + else (None, decl :: ctx) + | None -> (None, decl :: ctx)) newdelta (None, []) in match id with | None -> errorlabstrm "deppat" (str "Non-exhaustive pattern-matching, no clause found for:" ++ fnl () ++ - pr_clause env (newdelta, constrs_of_pats newpats, Empty var)) + pr_lhs env newlhs) | Some id -> - Some (Compute (newdelta, newpats, - Empty (fst (lookup_rel_id (out_name id) newdelta)))) + Some (Compute (newlhs, Empty (fst (lookup_rel_id (out_name id) newdelta)))) ) else ( - let splitting = make_split_aux env fdt newdelta newpats matching in + let splitting = make_split_aux env newlhs matching in Some splitting)) unify in - assert(!clauses = []); - Split (delta, curpats, var, indf, unify, splits) + if !clauses <> [] then + errorlabstrm "deppat" + (str "Impossible clauses:" ++ fnl () ++ pr_clauses env !clauses); + Split (lhs, var, indf, unify, splits) -and make_split_aux env (f, d, t as fdt) delta curpats clauses = - match clauses with - (delta', patcs, rhs) :: clauses' -> - (match find_split curpats patcs with - | None -> (* No need to split anymore *) - let res = Compute (delta', pats_of_constrs patcs, rhs) in - if clauses' <> [] then +and make_split_aux env lhs clauses = + let split = + fold_left (fun acc (lhs', rhs) -> + match acc with + | None -> find_split lhs lhs' + | _ -> acc) None clauses + in + match split with + | Some var -> split_on env var lhs clauses + | None -> + (match clauses with + | [] -> error "No clauses left" + | [(lhs, rhs)] -> + (* No need to split anymore *) + Compute (lhs, rhs) +(* (match rhs with *) +(* | Program _ -> *) +(* Compute (delta', pats_of_constrs patcs, rhs) *) +(* | Empty split -> (\* TODO : Check unify_type inductive type *\) *) +(* Compute (delta', pats_of_constrs patcs, rhs) *) + (* errorlabstrm "deppat" *) + (* (str "Splitting on " ++ pr_id x ++ str " of type " ++ *) + (* pr_constr_env (push_rel_context before env) *) + (* an empty type, on variable)) *) + | _ -> errorlabstrm "make_split_aux" - (str "Overlapping clauses:" ++ fnl () ++ pr_clauses env clauses) - else res - | Some var -> split_on env fdt var delta curpats clauses) - | [] -> error "No clauses left" + (str "Overlapping clauses:" ++ fnl () ++ pr_clauses env clauses)) let make_split env (f, delta, t) clauses = - make_split_aux env (f, delta, t) delta (patvars_of_tele delta) clauses + make_split_aux env (delta, f, patvars_of_tele delta) clauses open Evd open Evarutil @@ -515,29 +607,29 @@ open Evarutil let lift_substitution n s = map (fun (k, x) -> (k + n, x)) s let map_substitution s t = map (subst_rel_subst 0 s) t -let term_of_tree isevar env (i, delta, ty) tree = +let term_of_tree status isevar env (i, delta, ty) tree = let rec aux = function - | Compute (ctx, lhs, Program rhs) -> - let ty' = substl (rev (constrs_of_pats lhs)) ty in + | Compute ((ctx, _, pats as lhs), Program rhs) -> + let ty' = substl (rev (constrs_of_lhs ~inacc:false env lhs)) ty in let body = it_mkLambda_or_LetIn rhs ctx and typ = it_mkProd_or_LetIn ty' ctx in mkCast(body, DEFAULTcast, typ), typ - | Compute (ctx, lhs, Empty split) -> - let ty' = substl (rev (constrs_of_pats lhs)) ty in + | Compute ((ctx, _, pats as lhs), Empty split) -> + let ty' = substl (rev (constrs_of_lhs ~inacc:false env lhs)) ty in let split = (Name (id_of_string "split"), Some (Class_tactics.coq_nat_of_int (1 + (length ctx - split))), Lazy.force Class_tactics.coq_nat) in let ty' = it_mkProd_or_LetIn ty' ctx in let let_ty' = mkLambda_or_LetIn split (lift 1 ty') in - let term = e_new_evar isevar env ~src:(dummy_loc, QuestionMark true) let_ty' in + let term = e_new_evar isevar env ~src:(dummy_loc, QuestionMark (Define true)) let_ty' in term, ty' - | Split (ctx, lhs, rel, indf, unif, sp) -> + | Split ((ctx, _, pats as lhs), rel, indf, unif, sp) -> let before, decl, after = split_tele (pred rel) ctx in - let ty' = substl (rev (constrs_of_pats lhs)) ty in + let ty' = substl (rev (constrs_of_lhs ~inacc:false env lhs)) ty in let branches = - array_map2 (fun (ctx', ctxc, cstr, cstrpat, subst) split -> + array_map2 (fun (ctx', ctxlen, cstr, cstrpat, subst) split -> match split with | Some s -> aux s | None -> @@ -567,7 +659,7 @@ let term_of_tree isevar env (i, delta, ty) tree = Lazy.force Class_tactics.coq_nat) in let ty = it_mkLambda_or_LetIn (lift 2 ty) [nbbranches;nbdiscr] in - let term = e_new_evar isevar env ~src:(dummy_loc, QuestionMark true) ty in + let term = e_new_evar isevar env ~src:(dummy_loc, QuestionMark status) ty in term in let casetyp = it_mkProd_or_LetIn ty' ctx in @@ -644,10 +736,26 @@ let interp_eqn i isevar env impls sign arity recu (pats, rhs) = | Program p -> Program (interp_casted_constr_evars isevar env' ~impls p (substl patcs arity)) | Empty lid -> Empty (fst (lookup_rel_id (snd lid) ctx)) - in (ctx, rev patcs, rhs') + in ((ctx, i, pats_of_constrs (rev patcs)), rhs') open Entries +open Tacmach +open Tacexpr +open Tactics +open Tacticals + +let contrib_tactics_path = + make_dirpath (List.map id_of_string ["Equality";"Program";"Coq"]) + +let tactics_tac s = + make_kn (MPfile contrib_tactics_path) (make_dirpath []) (mk_label s) + +let equations_tac = lazy + (Tacinterp.eval_tactic + (TacArg(TacCall(dummy_loc, + ArgArg(dummy_loc, tactics_tac "equations"), [])))) + let define_by_eqs i l t nt eqs = let env = Global.env () in let isevar = ref (create_evar_defs Evd.empty) in @@ -655,7 +763,8 @@ let define_by_eqs i l t nt eqs = let arity = interp_type_evars isevar env' t in let ty = it_mkProd_or_LetIn arity sign in let data = Command.compute_interning_datas env [] [i] [ty] [impls] in - let fixenv = push_rel (Name i, None, ty) env in + let fixdecls = [(Name i, None, ty)] in + let fixenv = push_rel_context fixdecls env in let equations = States.with_heavy_rollback (fun () -> Option.iter (Command.declare_interning_data data) nt; @@ -665,10 +774,11 @@ let define_by_eqs i l t nt eqs = let arity = nf_evar (Evd.evars_of !isevar) arity in let prob = (i, sign, arity) in let fixenv = nf_env_evar (Evd.evars_of !isevar) fixenv in - let ce = check_evars fixenv Evd.empty !isevar in - List.iter (function (_, _, Program rhs) -> ce rhs | _ -> ()) equations; + let fixdecls = nf_rel_context_evar (Evd.evars_of !isevar) fixdecls in + (* let ce = check_evars fixenv Evd.empty !isevar in *) + (* List.iter (function (_, _, Program rhs) -> ce rhs | _ -> ()) equations; *) let is_recursive, env' = - let occur_eqn (ctx, _, rhs) = + let occur_eqn ((ctx, _, _), rhs) = match rhs with | Program c -> dependent (mkRel (succ (length ctx))) c | _ -> false @@ -676,19 +786,23 @@ let define_by_eqs i l t nt eqs = in let split = make_split env' prob equations in (* if valid_tree prob split then *) - let t, ty = term_of_tree isevar env' prob split in - let t = - if is_recursive then - let firstsplit = - match split with - | Split (ctx, lhs, rel, indf, unif, sp) -> (length ctx - rel) - | _ -> 0 - in mkFix (([|firstsplit|], 0), ([|Name i|], [|ty|], [|t|])) - else t - in + let status = (* if is_recursive then Expand else *) Define false in + let t, ty = term_of_tree status isevar env' prob split in let undef = undefined_evars !isevar in - let obls, t', ty' = Eterm.eterm_obligations env i !isevar (Evd.evars_of undef) 0 t ty in - ignore(Subtac_obligations.add_definition ~implicits:impls i t' ty' obls) + let t, ty = if is_recursive then + (it_mkLambda_or_LetIn t fixdecls, it_mkProd_or_LetIn ty fixdecls) + else t, ty + in + let obls, t', ty' = + Eterm.eterm_obligations env i !isevar (Evd.evars_of undef) 0 ~status t ty + in + if is_recursive then + ignore(Subtac_obligations.add_mutual_definitions [(i, t', ty', impls, obls)] [] + ~tactic:(Lazy.force equations_tac) + (Command.IsFixpoint [None, CStructRec])) + else + ignore(Subtac_obligations.add_definition + ~implicits:impls i t' ty' ~tactic:(Lazy.force equations_tac) obls) module Gram = Pcoq.Gram module Vernac = Pcoq.Vernac_ @@ -765,28 +879,13 @@ VERNAC COMMAND EXTEND Define_equations decl_notation(nt) ] -> [ define_by_eqs i l t nt eqs ] END - -open Tacmach -open Tacexpr -open Tactics -open Tacticals - -let contrib_tactics_path = - make_dirpath (List.map id_of_string ["Equality";"Program";"Coq"]) - -let tactics_tac s = - lazy(make_kn (MPfile contrib_tactics_path) (make_dirpath []) (mk_label s)) - -let destruct_last args = - Tacinterp.eval_tactic (TacArg(TacCall(dummy_loc, - ArgArg(dummy_loc, Lazy.force (tactics_tac "destruct_last")),args))) let rec int_of_coq_nat c = match kind_of_term c with | App (f, [| arg |]) -> succ (int_of_coq_nat arg) | _ -> 0 -let solve_equations_goal tac gl = +let solve_equations_goal destruct_tac tac gl = let concl = pf_concl gl in let targetn, branchesn, targ, brs, b = match kind_of_term concl with @@ -811,10 +910,10 @@ let solve_equations_goal tac gl = let cleantac = tclTHEN (intros_using ids) (thin ids) in let dotac = tclDO (succ targ) intro in let subtacs = - tclTHENS (destruct_last []) + tclTHENS destruct_tac (map (fun (id, br, brt) -> tclTHEN (letin_tac None (Name id) br onConcl) tac) branches) in tclTHENLIST [cleantac ; dotac ; subtacs] gl - + TACTIC EXTEND solve_equations - [ "solve_equations" tactic(tac) ] -> [ solve_equations_goal (snd tac) ] + [ "solve_equations" tactic(destruct) tactic(tac) ] -> [ solve_equations_goal (snd destruct) (snd tac) ] END diff --git a/proofs/logic.ml b/proofs/logic.ml index 818a32cea..c07b6a800 100644 --- a/proofs/logic.ml +++ b/proofs/logic.ml @@ -57,6 +57,8 @@ let rec catchable_exception = function |NoOccurrenceFound _|CannotUnifyBindingType _|NotClean _ |CannotFindWellTypedAbstraction _ |UnsolvableImplicit _)) -> true + | Typeclasses_errors.TypeClassError + (_, Typeclasses_errors.UnsatisfiableConstraints _) -> true | _ -> false (* Tells if the refiner should check that the submitted rules do not diff --git a/test-suite/success/Equations.v b/test-suite/success/Equations.v index ea4d693dd..160940185 100644 --- a/test-suite/success/Equations.v +++ b/test-suite/success/Equations.v @@ -1,8 +1,6 @@ Require Import Bvector. Require Import Program. -Obligation Tactic := try equations. - Equations neg (b : bool) : bool := neg true := false ; neg false := true. @@ -27,17 +25,16 @@ Eval compute in (tail (cons 1 nil)). Reserved Notation " x ++ y " (at level 60, right associativity). +Equations app' {A} (l l' : list A) : (list A) := +app' A nil l := l ; +app' A (cons a v) l := cons a (app' v l). + Equations app (l l' : list nat) : list nat := [] ++ l := l ; (a :: v) ++ l := a :: (v ++ l) where " x ++ y " := (app x y). -Equations app' {A} (l l' : list A) : (list A) := -app' A nil l := l ; -app' A (cons a v) l := cons a (app' v l). - - Eval compute in @app'. Equations zip' {A} (f : A -> A -> A) (l l' : list A) : (list A) := @@ -46,9 +43,8 @@ zip' A f (cons a v) (cons b w) := cons (f a b) (zip' f v w) ; zip' A f nil (cons b w) := nil ; zip' A f (cons a v) nil := nil. -Eval compute in @zip'. -Eval cbv delta [ zip' zip'_obligation_1 zip'_obligation_2 zip'_obligation_3 ] beta iota zeta in @zip'. +Eval compute in @zip'. Equations zip'' {A} (f : A -> A -> A) (l l' : list A) (def : list A) : (list A) := zip'' A f nil nil def := nil ; @@ -57,7 +53,6 @@ zip'' A f nil (cons b w) def := def ; zip'' A f (cons a v) nil def := def. Eval compute in @zip''. -Eval cbv delta [ zip'' ] beta iota zeta in @zip''. Implicit Arguments Vnil [[A]]. Implicit Arguments Vcons [[A] [n]]. @@ -105,8 +100,6 @@ Section Image. Equations inv (t : T) (im : Imf t) : S := inv (f s) (imf s) := s. - Eval compute in inv. - End Image. Section Univ. @@ -131,3 +124,91 @@ End Univ. Eval compute in (foo ubool false). Eval compute in (foo (uarrow ubool ubool) negb). Eval compute in (foo (uarrow ubool ubool) id). + +(* Overlap. *) + +Inductive foobar : Set := bar | baz. + +Equations bla f : bool := +bla bar := true ; +bla baz := false. + +Eval simpl in bla. +Print refl_equal. + +Notation "'refl'" := (@refl_equal _ _). + +Equations K {A} (x : A) (P : x = x -> Type) (p : P (refl_equal x)) (p : x = x) : P p := +K A x P p refl := p. + +Equations eq_sym {A} (x y : A) (H : x = y) : y = x := +eq_sym A x x refl := refl. + +(* Obligation Tactic := idtac. *) + +Equations eq_trans {A} (x y z : A) (p : x = y) (q : y = z) : x = z := +eq_trans A x x x refl refl := refl. + +Lemma eq_trans_eq A x : @eq_trans A x x x refl refl = refl. +Proof. reflexivity. Qed. + +Equations nth {A} {n} (v : vector A n) (f : fin n) : A := +nth A (S n) (Vcons a v) fz := a ; +nth A (S n) (Vcons a v) (fs f) := nth v f. + +Equations tabulate {A} {n} (f : fin n -> A) : vector A n := +tabulate A 0 f := Vnil ; +tabulate A (S n) f := Vcons (f fz) (tabulate (f ∘ fs)). + +Equations vlast {A} {n} (v : vector A (S n)) : A := +vlast A 0 (Vcons a Vnil) := a ; +vlast A (S n) (Vcons a v) := vlast v. + +Lemma vlast_equation1 A (a : A) : vlast (Vcons a Vnil) = a. +Proof. intros. compute ; reflexivity. Qed. + +Lemma vlast_equation2 A n a v : @vlast A (S n) (Vcons a v) = vlast v. +Proof. intros. compute ; reflexivity. Qed. + +Print Assumptions vlast. +Print Assumptions nth. +Print Assumptions tabulate. + +Equations vliat {A} {n} (v : vector A (S n)) : vector A n := +vliat A 0 (Vcons a Vnil) := Vnil ; +vliat A (S n) (Vcons a v) := Vcons a (vliat v). + +Eval compute in (vliat (Vcons 2 (Vcons 5 (Vcons 4 Vnil)))). + +Equations vapp {A} {n m} (v : vector A n) (w : vector A m) : vector A (n + m) := +vapp A 0 m Vnil w := w ; +vapp A (S n) m (Vcons a v) w := Vcons a (vapp v w). + +Lemma JMeq_Vcons_inj A n m a (x : vector A n) (y : vector A m) : n = m -> JMeq x y -> JMeq (Vcons a x) (Vcons a y). +Proof. intros until y. simplify_dep_elim. reflexivity. Qed. + +Equations NoConfusion_fin (P : Prop) {n : nat} (x y : fin n) : Prop := +NoConfusion_fin P (S n) fz fz := P -> P ; +NoConfusion_fin P (S n) fz (fs y) := P ; +NoConfusion_fin P (S n) (fs x) fz := P ; +NoConfusion_fin P (S n) (fs x) (fs y) := (x = y -> P) -> P. + +Equations noConfusion_fin P (n : nat) (x y : fin n) (H : x = y) : NoConfusion_fin P x y := +noConfusion_fin P (S n) fz fz refl := λ p, p ; +noConfusion_fin P (S n) (fs x) (fs x) refl := λ p : x = x -> P, p refl. + +Equations NoConfusion_vect (P : Prop) {A n} (x y : vector A n) : Prop := +NoConfusion_vect P A 0 Vnil Vnil := P -> P ; +NoConfusion_vect P A (S n) (Vcons a x) (Vcons b y) := (a = b -> x = y -> P) -> P. + +Equations noConfusion_vect (P : Prop) A n (x y : vector A n) (H : x = y) : NoConfusion_vect P x y := +noConfusion_vect P A 0 Vnil Vnil refl := λ p, p ; +noConfusion_vect P A (S n) (Vcons a v) (Vcons a v) refl := λ p : a = a -> v = v -> P, p refl refl. + +Instance fin_noconf n : NoConfusionPackage (fin n) := + NoConfusion := λ P, Π x y, x = y -> NoConfusion_fin P x y ; + noConfusion := λ P x y, noConfusion_fin P n x y. + +Instance vect_noconf A n : NoConfusionPackage (vector A n) := + NoConfusion := λ P, Π x y, x = y -> NoConfusion_vect P x y ; + noConfusion := λ P x y, noConfusion_vect P A n x y. diff --git a/theories/Program/Equality.v b/theories/Program/Equality.v index d11996a67..3e0e8ca2b 100644 --- a/theories/Program/Equality.v +++ b/theories/Program/Equality.v @@ -1,3 +1,4 @@ +(* -*- coq-prog-name: "~/research/coq/trunk/bin/coqtop.byte"; coq-prog-args: ("-emacs-U" "-top" "Coq.Program.Equality"); compile-command: "make -C ../.. TIME='time'" -*- *) (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) (* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) @@ -19,6 +20,10 @@ Require Import Coq.Program.Tactics. Notation " [ x : X ] = [ y : Y ] " := (@JMeq X x Y y) (at level 0, X at next level, Y at next level). +(** Notation for the single element of [x = x] *) + +Notation "'refl'" := (@refl_equal _ _). + (** Do something on an heterogeneous equality appearing in the context. *) Ltac on_JMeq tac := @@ -309,17 +314,15 @@ Tactic Notation "dependent" "induction" ident(H) "generalizing" ne_hyp_list(l) " These tactics implement the necessary machinery to solve goals produced by the [Equations] command relative to dependent pattern-matching. It is completely inspired from the "Eliminating Dependent Pattern-Matching" paper by - Goguen, McBride and McKinna. - -*) + Goguen, McBride and McKinna. *) (** Lemmas used by the simplifier, mainly rephrasings of [eq_rect], [eq_ind]. *) Lemma solution_left : Π A (B : A -> Type) (t : A), B t -> (Π x, x = t -> B x). -Proof. intros; subst; assumption. Defined. +Proof. intros; subst. apply X. Defined. Lemma solution_right : Π A (B : A -> Type) (t : A), B t -> (Π x, t = x -> B x). -Proof. intros; subst; assumption. Defined. +Proof. intros; subst; apply X. Defined. Lemma deletion : Π A B (t : A), B -> (t = t -> B). Proof. intros; assumption. Defined. @@ -331,6 +334,21 @@ Lemma simplification_existT : Π A (P : A -> Type) B (p : A) (x y : P p), (x = y -> B) -> (existT P p x = existT P p y -> B). Proof. intros. apply X. apply inj_pair2. exact H. Defined. +Lemma simplification_K : Π A (x : A) (B : x = x -> Type), B (refl_equal x) -> (Π p : x = x, B p). +Proof. intros. rewrite (UIP_refl A). assumption. Defined. + +(** The NoConfusionPackage class provides a method for making progress on proving a property + [P] implied by an equality on an inductive type [I]. The type of [noConfusion] for a given + [P] should be of the form [ Π Δ, (x y : I Δ) (x = y) -> NoConfusion P x y ], where + [NoConfusion P x y] for constructor-headed [x] and [y] will give a formula ending in [P]. + This gives a general method for simplifying by discrimination or injectivity of constructors. + + Some actual instances are defined later in the file using the more primitive [discriminate] and + [injection] tactics on which we can always fall back. + *) + +Class NoConfusionPackage (I : Type) := NoConfusion : Π P : Prop, Type ; noConfusion : Π P, NoConfusion P. + (** This hint database and the following tactic can be used with [autosimpl] to unfold everything to [eq_rect]s. *) @@ -354,18 +372,20 @@ Ltac simplify_equations := repeat (unfold_equations ; simplify_eqs). Ltac simplify_one_dep_elim_term c := match c with | @JMeq ?A ?a ?A ?b -> _ => refine (simplification_heq _ _ _ _ _) - | ?t = ?t -> _ => intros _ + | ?t = ?t -> _ => intros _ || refine (simplification_K _ t _ _) | eq (existT ?P ?p _) (existT ?P ?p _) -> _ => refine (simplification_existT _ _ _ _ _ _ _) - | ?f ?x = ?f ?y -> _ => let H := fresh in intros H ; injection H ; clear H | ?x = ?y -> _ => - (let hyp := fresh in intros hyp ; - move dependent hyp before x ; + (let hyp := fresh in intros hyp ; + move dependent hyp before x ; generalize dependent x ; refine (solution_left _ _ _ _) ; intros until 0) || - (let hyp := fresh in intros hyp ; - move dependent hyp before y ; + (let hyp := fresh in intros hyp ; + move dependent hyp before y ; generalize dependent y ; refine (solution_right _ _ _ _) ; intros until 0) + | @eq ?A ?t ?u -> ?P => apply (noConfusion (I:=A) P) + | ?f ?x = ?g ?y -> _ => let H := fresh in intros H ; injection H ; clear H | ?t = ?u -> _ => let hyp := fresh in intros hyp ; elimtype False ; discriminate + | id ?T => fail 1 (* Do not put any part of the rhs in the hyps *) | _ => intro end. @@ -392,32 +412,59 @@ Ltac destruct_last := (** The rest is support tactics for the [Equations] command. *) +(** Notation for inaccessible patterns. *) + +Definition inaccessible_pattern {A : Type} (t : A) := t. + +Notation "?( t )" := (inaccessible_pattern t). + +(** To handle sections, we need to separate the context in two parts: + variables introduced by the section and the rest. We introduce a dummy variable + between them to indicate that. *) + +CoInductive end_of_section := the_end_of_the_section. + +Ltac set_eos := let eos := fresh "eos" in + assert (eos:=the_end_of_the_section). + +(** We have a specialized [reverse_local] tactic to reverse the goal until the begining of the + section variables *) + +Ltac reverse_local := + match goal with + | [ H : ?T |- _ ] => + match T with + | end_of_section => idtac | _ => revert H ; reverse_local end + | _ => idtac + end. + (** Do as much as possible to apply a method, trying to get the arguments right. *) -Ltac try_intros m := - (eapply m ; eauto) || (intro ; try_intros m). +Ltac simpl_apply m := refine m. (* || apply m || simpl ; apply m. *) + +Ltac try_intros m := unfold Datatypes.id ; refine m || apply m. (* (repeat simpl_apply m || intro). *) (** To solve a goal by inversion on a particular target. *) Ltac solve_empty target := do_nat target intro ; elimtype False ; destruct_last ; simplify_dep_elim. -Ltac simplify_method H := clear H ; simplify_dep_elim ; reverse. +Ltac simplify_method tac := repeat (tac || simplify_one_dep_elim) ; reverse_local. -(** Solving a method call: we must refine the goal until the body - can be applied or just solve it by splitting on an empty family member. *) +(** Solving a method call: we can solve it by splitting on an empty family member + or we must refine the goal until the body can be applied. *) Ltac solve_method rec := match goal with - | [ H := ?body : nat |- _ ] => simplify_method H ; solve_empty body - | [ H := ?body |- _ ] => simplify_method H ; rec ; try_intros body + | [ H := ?body : nat |- _ ] => subst H ; clear ; abstract (simplify_method idtac ; solve_empty body) + | [ H := ?body |- _ ] => clear H ; simplify_method ltac:(exact body) ; rec ; try_intros body end. (** Impossible cases, by splitting on a given target. *) Ltac solve_split := match goal with - | [ |- let split := ?x : nat in _ ] => intros _ ; solve_empty x + | [ |- let split := ?x : nat in _ ] => clear ; abstract (intros _ ; solve_empty x) end. (** If defining recursive functions, the prototypes come first. *) @@ -428,19 +475,98 @@ Ltac intro_prototypes := | _ => idtac end. +Ltac case_last := + match goal with + | [ p : ?x = ?x |- ?T ] => change (id T) ; revert p ; refine (simplification_K _ x _ _) + | [ p : ?x = ?y |- ?T ] => change (id T) ; revert p + | [ p : _ |- ?T ] => simpl in p ; change (id T) ; generalize_eqs p ; destruct p + end. + Ltac nonrec_equations := - solve [solve_equations (solve_method idtac)] || solve [ solve_split ] + solve [solve_equations (case_last) (solve_method idtac)] || solve [ solve_split ] || fail "Unnexpected equations goal". Ltac recursive_equations := - solve [solve_equations (solve_method ltac:intro)] || solve [ solve_split ] + solve [solve_equations (case_last) (solve_method ltac:intro)] || solve [ solve_split ] || fail "Unnexpected recursive equations goal". (** The [equations] tactic is the toplevel tactic for solving goals generated by [Equations]. *) -Ltac equations := +Ltac equations := set_eos ; match goal with | [ |- Π x : _, _ ] => intro ; recursive_equations | _ => nonrec_equations end. + +Equations NoConfusion_nat (P : Prop) (x y : nat) : Prop := +NoConfusion_nat P 0 0 := P -> P ; +NoConfusion_nat P 0 (S y) := P ; +NoConfusion_nat P (S x) 0 := P ; +NoConfusion_nat P (S x) (S y) := (x = y -> P) -> P. +Debug Off. + Solve Obligations using equations. + +Equations noConfusion_nat (P : Prop) (x y : nat) (H : x = y) : NoConfusion_nat P x y := +noConfusion_nat P 0 0 refl := λ p, p ; +noConfusion_nat P (S n) (S n) refl := λ p : n = n -> P, p refl. + + Solve Obligations using equations. + +Instance nat_noconf : NoConfusionPackage nat := + NoConfusion := λ P, Π x y, x = y -> NoConfusion_nat P x y ; + noConfusion := λ P x y, noConfusion_nat P x y. + +Equations NoConfusion_bool (P : Prop) (x y : bool) : Prop := +NoConfusion_bool P true true := P -> P ; +NoConfusion_bool P false false := P -> P ; +NoConfusion_bool P true false := P ; +NoConfusion_bool P false true := P. + + Solve Obligations using equations. + +Equations noConfusion_bool (P : Prop) (x y : bool) (H : x = y) : NoConfusion_bool P x y := +noConfusion_bool P true true refl := λ p, p ; +noConfusion_bool P false false refl := λ p, p. + + Solve Obligations using equations. + +Instance bool_noconf : NoConfusionPackage bool := + NoConfusion := λ P, Π x y, x = y -> NoConfusion_bool P x y ; + noConfusion := λ P x y, noConfusion_bool P x y. + +Equations NoConfusion_unit (P : Prop) (x y : unit) : Prop := +NoConfusion_unit P tt tt := P -> P. + + Solve Obligations using equations. + +Equations noConfusion_unit (P : Prop) (x y : unit) (H : x = y) : NoConfusion_unit P x y := +noConfusion_unit P tt tt refl := λ p, p. + + Solve Obligations using equations. + +Instance unit_noconf : NoConfusionPackage unit := + NoConfusion := λ P, Π x y, x = y -> NoConfusion_unit P x y ; + noConfusion := λ P x y, noConfusion_unit P x y. + +Require Import List. + +Implicit Arguments nil [[A]]. + +Equations NoConfusion_list (P : Prop) (A : Type) (x y : list A) : Prop := +NoConfusion_list P A nil nil := P -> P ; +NoConfusion_list P A nil (cons a y) := P ; +NoConfusion_list P A (cons a x) nil := P ; +NoConfusion_list P A (cons a x) (cons b y) := (a = b -> x = y -> P) -> P. + + Solve Obligations using equations. + +Equations noConfusion_list (P : Prop) A (x y : list A) (H : x = y) : NoConfusion_list P A x y := +noConfusion_list P A nil nil refl := λ p, p ; +noConfusion_list P A (cons a x) (cons a x) refl := λ p : a = a -> x = x -> P, p refl refl. + + Solve Obligations using equations. + +Instance list_noconf A : NoConfusionPackage (list A) := + NoConfusion := λ P, Π x y, x = y -> NoConfusion_list P A x y ; + noConfusion := λ P x y, noConfusion_list P A x y. diff --git a/theories/Program/Tactics.v b/theories/Program/Tactics.v index 7fe5211af..9cb7725c0 100644 --- a/theories/Program/Tactics.v +++ b/theories/Program/Tactics.v @@ -121,6 +121,26 @@ Ltac on_application f tac T := | context [f ?x ?y] => tac (f x y) | context [f ?x] => tac (f x) end. + +(** A variant of [apply] using [refine], doing as much conversion as necessary. *) + +Ltac rapply p := + refine (p _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) || + refine (p _ _ _ _ _ _ _ _ _ _ _ _ _ _) || + refine (p _ _ _ _ _ _ _ _ _ _ _ _ _) || + refine (p _ _ _ _ _ _ _ _ _ _ _ _) || + refine (p _ _ _ _ _ _ _ _ _ _ _) || + refine (p _ _ _ _ _ _ _ _ _ _) || + refine (p _ _ _ _ _ _ _ _ _) || + refine (p _ _ _ _ _ _ _ _) || + refine (p _ _ _ _ _ _ _) || + refine (p _ _ _ _ _ _) || + refine (p _ _ _ _ _) || + refine (p _ _ _ _) || + refine (p _ _ _) || + refine (p _ _) || + refine (p _) || + refine p. (** Tactical [on_call f tac] applies [tac] on any application of [f] in the hypothesis or goal. *) @@ -213,21 +233,6 @@ Ltac replace_hyp H c := let H' := fresh "H" in assert(H' := c) ; clear H ; rename H' into H. -(** A tactic to refine an hypothesis by supplying some of its arguments. *) - -Ltac refine_hyp c := - let tac H := replace_hyp H c in - match c with - | ?H _ => tac H - | ?H _ _ => tac H - | ?H _ _ _ => tac H - | ?H _ _ _ _ => tac H - | ?H _ _ _ _ _ => tac H - | ?H _ _ _ _ _ _ => tac H - | ?H _ _ _ _ _ _ _ => tac H - | ?H _ _ _ _ _ _ _ _ => tac H - end. - (** The default simplification tactic used by Program is defined by [program_simpl], sometimes [auto] is not enough, better rebind using [Obligation Tactic := tac] in this case, possibly using [program_simplify] to use standard goal-cleaning tactics. *) |