diff options
Diffstat (limited to 'contrib/funind/invfun.ml')
-rw-r--r-- | contrib/funind/invfun.ml | 148 |
1 files changed, 148 insertions, 0 deletions
diff --git a/contrib/funind/invfun.ml b/contrib/funind/invfun.ml new file mode 100644 index 00000000..1f711297 --- /dev/null +++ b/contrib/funind/invfun.ml @@ -0,0 +1,148 @@ +open Util +open Names +open Term +open Tacinvutils +open Pp +open Libnames +open Tacticals +open Tactics +open Indfun_common +open Tacmach +open Sign + + +let tac_pattern l = + (Hiddentac.h_reduce + (Rawterm.Pattern l) + Tacticals.onConcl + ) + + +let rec nb_prod x = + let rec count n c = + match kind_of_term c with + Prod(_,_,t) -> count (n+1) t + | LetIn(_,a,_,t) -> count n (subst1 a t) + | Cast(c,_,_) -> count n c + | _ -> n + in count 0 x + +let intro_discr_until n tac : tactic = + let rec intro_discr_until acc : tactic = + fun g -> + if nb_prod (pf_concl g) <= n then tac (List.rev acc) g + else + tclTHEN + intro + (fun g' -> + let id,_,t = pf_last_hyp g' in + tclORELSE + (tclABSTRACT None (Extratactics.h_discrHyp (Rawterm.NamedHyp id))) + (intro_discr_until ((id,t)::acc)) + g' + ) + g + in + intro_discr_until [] + + +let rec discr_rew_in_H hypname idl : tactic = + match idl with + | [] -> (Extratactics.h_discrHyp (Rawterm.NamedHyp hypname)) + | ((id,t)::idl') -> + match kind_of_term t with + | App(eq',[| _ ; arg1 ; _ |]) when eq_constr eq' (Lazy.force eq) -> + begin + let constr,_ = decompose_app arg1 in + if isConstruct constr + then + (discr_rew_in_H hypname idl') + else + tclTHEN + (tclTRY (Equality.general_rewrite_in true hypname (mkVar id))) + (discr_rew_in_H hypname idl') + end + | _ -> discr_rew_in_H hypname idl' + +let finalize fname hypname idl : tactic = + tclTRY ( + (tclTHEN + (Hiddentac.h_reduce + (Rawterm.Unfold [[],EvalConstRef fname]) + (Tacticals.onHyp hypname) + ) + (discr_rew_in_H hypname idl) + )) + +let gen_fargs fargs : tactic = + fun g -> + generalize + (List.map + (fun arg -> + let targ = pf_type_of g arg in + let refl_arg = mkApp (Lazy.force refl_equal , [|targ ; arg|]) in + refl_arg + ) + (Array.to_list fargs) + ) + g + + +let invfun (hypname:identifier) (fid:identifier) : tactic= + fun g -> + let nprod_goal = nb_prod (pf_concl g) in + let f_ind_id = + ( + Indrec.make_elimination_ident + fid + (Tacticals.elimination_sort_of_goal g) + ) + in + let fname = const_of_id fid in + let princ = const_of_id f_ind_id in + let princ_info = + let princ_type = + (try (match (Global.lookup_constant princ) with + {Declarations.const_type=t} -> t + ) + with _ -> assert false) + in + Tactics.compute_elim_sig princ_type + in + let _,_,typhyp = List.find (fun (id,_,_) -> hypname=id) (pf_hyps g) in + let do_invert fargs appf : tactic = + let frealargs = (snd (array_chop (List.length princ_info.params) fargs)) + in + let pat_args = + (List.map (fun e -> ([-1],e)) (Array.to_list frealargs)) @ [[],appf] + in + tclTHENSEQ + [ + gen_fargs frealargs; + tac_pattern pat_args; + Hiddentac.h_apply (mkConst princ,Rawterm.NoBindings); + intro_discr_until nprod_goal (finalize fname hypname) + + ] + in + match kind_of_term typhyp with + | App(eq',[| _ ; arg1 ; arg2 |]) when eq_constr eq' (Lazy.force eq) -> +(* let valf = def_of_const (mkConst fname) in *) + let eq_arg1 , eq_arg2 , good_eq_form , fargs = + match kind_of_term arg1 , kind_of_term arg2 with + | App(f, args),_ when eq_constr f (mkConst fname) -> + arg1 , arg2 , tclIDTAC , args + | _,App(f, args) when eq_constr f (mkConst fname) -> + arg2 , arg1 , symmetry_in hypname , args + | _ , _ -> error "inversion impossible" + in + tclTHEN + good_eq_form + (do_invert fargs eq_arg1) + g + | App(f',fargs) when eq_constr f' (mkConst fname) -> + do_invert fargs typhyp g + + + | _ -> error "inversion impossible" + |