summaryrefslogtreecommitdiff
path: root/contrib/funind
diff options
context:
space:
mode:
Diffstat (limited to 'contrib/funind')
-rw-r--r--contrib/funind/functional_principles_proofs.ml60
-rw-r--r--contrib/funind/indfun.ml55
-rw-r--r--contrib/funind/indfun_main.ml45
-rw-r--r--contrib/funind/invfun.ml165
-rw-r--r--contrib/funind/rawterm_to_relation.ml6
-rw-r--r--contrib/funind/rawtermops.ml35
6 files changed, 193 insertions, 133 deletions
diff --git a/contrib/funind/functional_principles_proofs.ml b/contrib/funind/functional_principles_proofs.ml
index ff4f7499..dec7273b 100644
--- a/contrib/funind/functional_principles_proofs.ml
+++ b/contrib/funind/functional_principles_proofs.ml
@@ -621,33 +621,39 @@ let build_proof
fun g ->
(* observe (str "proving on " ++ Printer.pr_lconstr_env (pf_env g) term);*)
- match kind_of_term dyn_infos.info with
- | Case(_,_,t,_) ->
- let g_nb_prod = nb_prod (pf_concl g) in
- let type_of_term = pf_type_of g t in
- let term_eq =
- make_refl_eq type_of_term t
+ match kind_of_term dyn_infos.info with | Case(ci,ct,t,cb) ->
+ let do_finalize_t dyn_info' =
+ fun g ->
+ let t = dyn_info'.info in
+ let dyn_infos = {dyn_info' with info =
+ mkCase(ci,ct,t,cb)} in
+ let g_nb_prod = nb_prod (pf_concl g) in
+ let type_of_term = pf_type_of g t in
+ let term_eq =
+ make_refl_eq type_of_term t
+ in
+ tclTHENSEQ
+ [
+ h_generalize (term_eq::(List.map mkVar dyn_infos.rec_hyps));
+ thin dyn_infos.rec_hyps;
+ pattern_option [[-1],t] None;
+ h_simplest_case t;
+ (fun g' ->
+ let g'_nb_prod = nb_prod (pf_concl g') in
+ let nb_instanciate_partial = g'_nb_prod - g_nb_prod in
+ observe_tac "treat_new_case"
+ (treat_new_case
+ ptes_infos
+ nb_instanciate_partial
+ (build_proof do_finalize)
+ t
+ dyn_infos)
+ g'
+ )
+
+ ] g
in
- tclTHENSEQ
- [
- h_generalize (term_eq::(List.map mkVar dyn_infos.rec_hyps));
- thin dyn_infos.rec_hyps;
- pattern_option [[-1],t] None;
- h_simplest_case t;
- (fun g' ->
- let g'_nb_prod = nb_prod (pf_concl g') in
- let nb_instanciate_partial = g'_nb_prod - g_nb_prod in
- observe_tac "treat_new_case"
- (treat_new_case
- ptes_infos
- nb_instanciate_partial
- (build_proof do_finalize)
- t
- dyn_infos)
- g'
- )
-
- ] g
+ build_proof do_finalize_t {dyn_infos with info = t} g
| Lambda(n,t,b) ->
begin
match kind_of_term( pf_concl g) with
@@ -1474,7 +1480,7 @@ let prove_principle_for_gen
(mkApp (delayed_force acc_rel,[|input_type;relation;mkVar rec_arg_id|]))
);
observe_tac "reverting" (revert (List.rev (acc_rec_arg_id::args_ids)));
- observe_tac "h_fix" (h_fix (Some fix_id) (npost_rec_arg + 1));
+ observe_tac "h_fix" (h_fix (Some fix_id) (List.length args_ids + 1));
h_intros (List.rev (acc_rec_arg_id::args_ids));
Equality.rewriteLR (mkConst eq_ref);
observe_tac "finish" (fun gl' ->
diff --git a/contrib/funind/indfun.ml b/contrib/funind/indfun.ml
index 6e2af224..82bee01f 100644
--- a/contrib/funind/indfun.ml
+++ b/contrib/funind/indfun.ml
@@ -209,7 +209,7 @@ let rec is_rec names =
let rec lookup names = function
| RVar(_,id) -> check_id id names
| RRef _ | REvar _ | RPatVar _ | RSort _ | RHole _ | RDynamic _ -> false
- | RCast(_,b,_,_) -> lookup names b
+ | RCast(_,b,_) -> lookup names b
| RRec _ -> error "RRec not handled"
| RIf(_,b,_,lhs,rhs) ->
(lookup names b) || (lookup names lhs) || (lookup names rhs)
@@ -270,7 +270,30 @@ let derive_inversion fix_names =
if do_observe () then Cerrors.explain_exn e else mt ())
with _ -> ()
-let generate_principle
+let warning_error names e =
+ match e with
+ | Building_graph e ->
+ Pp.msg_warning
+ (str "Cannot define graph(s) for " ++
+ h 1 (prlist_with_sep (fun _ -> str","++spc ()) Ppconstr.pr_id names) ++
+ if do_observe () then (spc () ++ Cerrors.explain_exn e) else mt ())
+ | Defining_principle e ->
+ Pp.msg_warning
+ (str "Cannot define principle(s) for "++
+ h 1 (prlist_with_sep (fun _ -> str","++spc ()) Ppconstr.pr_id names) ++
+ if do_observe () then Cerrors.explain_exn e else mt ())
+ | _ -> anomaly ""
+
+let error_error names e =
+ match e with
+ | Building_graph e ->
+ errorlabstrm ""
+ (str "Cannot define graph(s) for " ++
+ h 1 (prlist_with_sep (fun _ -> str","++spc ()) Ppconstr.pr_id names) ++
+ if do_observe () then (spc () ++ Cerrors.explain_exn e) else mt ())
+ | _ -> anomaly ""
+
+let generate_principle on_error
is_general do_built fix_rec_l recdefs interactive_proof
(continue_proof : int -> Names.constant array -> Term.constr array -> int ->
Tacmach.tactic) : unit =
@@ -324,18 +347,7 @@ let generate_principle
()
end
with e ->
- match e with
- | Building_graph e ->
- Pp.msg_warning
- (str "Cannot define graph(s) for " ++
- h 1 (prlist_with_sep (fun _ -> str","++spc ()) Ppconstr.pr_id names) ++
- if do_observe () then (spc () ++ Cerrors.explain_exn e) else mt ())
- | Defining_principle e ->
- Pp.msg_warning
- (str "Cannot define principle(s) for "++
- h 1 (prlist_with_sep (fun _ -> str","++spc ()) Ppconstr.pr_id names) ++
- if do_observe () then Cerrors.explain_exn e else mt ())
- | _ -> anomaly ""
+ on_error names e
let register_struct is_rec fixpoint_exprl =
match fixpoint_exprl with
@@ -459,13 +471,14 @@ let register_mes fname rec_impls wf_mes_expr wf_arg using_lemmas args ret_type b
using_lemmas args ret_type body
-let do_generate_principle register_built interactive_proof fixpoint_exprl =
+let do_generate_principle on_error register_built interactive_proof fixpoint_exprl =
let recdefs,rec_impls = build_newrecursive fixpoint_exprl in
let _is_struct =
match fixpoint_exprl with
| [((name,Some (Wf (wf_rel,wf_x,using_lemmas)),args,types,body))] ->
let pre_hook =
generate_principle
+ on_error
true
register_built
fixpoint_exprl
@@ -478,6 +491,7 @@ let do_generate_principle register_built interactive_proof fixpoint_exprl =
| [((name,Some (Mes (wf_mes,wf_x,using_lemmas)),args,types,body))] ->
let pre_hook =
generate_principle
+ on_error
true
register_built
fixpoint_exprl
@@ -530,6 +544,7 @@ let do_generate_principle register_built interactive_proof fixpoint_exprl =
let is_rec = List.exists (is_rec fix_names) recdefs in
if register_built then register_struct is_rec old_fixpoint_exprl;
generate_principle
+ on_error
false
register_built
fixpoint_exprl
@@ -596,8 +611,10 @@ let rec add_args id new_args b =
| CPatVar _ -> b
| CEvar _ -> b
| CSort _ -> b
- | CCast(loc,b1,ck,b2) ->
- CCast(loc,add_args id new_args b1,ck,add_args id new_args b2)
+ | CCast(loc,b1,CastConv(ck,b2)) ->
+ CCast(loc,add_args id new_args b1,CastConv(ck,add_args id new_args b2))
+ | CCast(loc,b1,CastCoerce) ->
+ CCast(loc,add_args id new_args b1,CastCoerce)
| CNotation _ -> anomaly "add_args : CNotation"
| CPrim _ -> b
| CDelimiters _ -> anomaly "add_args : CDelimiters"
@@ -732,7 +749,7 @@ let make_graph (f_ref:global_reference) =
let id = id_of_label (con_label c) in
[(id,None,nal_tas,t,b)]
in
- do_generate_principle false false expr_list;
+ do_generate_principle error_error false false expr_list;
(* We register the infos *)
let mp,dp,_ = repr_con c in
List.iter
@@ -742,6 +759,6 @@ let make_graph (f_ref:global_reference) =
(* let make_graph _ = assert false *)
-let do_generate_principle = do_generate_principle true
+let do_generate_principle = do_generate_principle warning_error true
diff --git a/contrib/funind/indfun_main.ml4 b/contrib/funind/indfun_main.ml4
index 26a1066c..9cee9edc 100644
--- a/contrib/funind/indfun_main.ml4
+++ b/contrib/funind/indfun_main.ml4
@@ -203,7 +203,10 @@ VERNAC COMMAND EXTEND NewFunctionalScheme
match fas with
| (_,fun_name,_)::_ ->
begin
- make_graph (Nametab.global fun_name);
+ begin
+ make_graph (Nametab.global fun_name)
+ end
+ ;
try Functional_principles_types.build_scheme fas
with Functional_principles_types.No_graph_found ->
Util.error ("Cannot generate induction principle(s)")
diff --git a/contrib/funind/invfun.ml b/contrib/funind/invfun.ml
index 04110ea9..9ec02d4c 100644
--- a/contrib/funind/invfun.ml
+++ b/contrib/funind/invfun.ml
@@ -478,7 +478,72 @@ let generalize_depedent_of x hyp g =
-
+ (* [intros_with_rewrite] do the intros in each branch and treat each new hypothesis
+ (unfolding, substituting, destructing cases \ldots)
+ *)
+let rec intros_with_rewrite g =
+ observe_tac "intros_with_rewrite" intros_with_rewrite_aux g
+and intros_with_rewrite_aux : tactic =
+ fun g ->
+ let eq_ind = Coqlib.build_coq_eq () in
+ match kind_of_term (pf_concl g) with
+ | Prod(_,t,t') ->
+ begin
+ match kind_of_term t with
+ | App(eq,args) when (eq_constr eq eq_ind) ->
+ if isVar args.(1)
+ then
+ let id = pf_get_new_id (id_of_string "y") g in
+ tclTHENSEQ [ h_intro id;
+ generalize_depedent_of (destVar args.(1)) id;
+ tclTRY (Equality.rewriteLR (mkVar id));
+ intros_with_rewrite
+ ]
+ g
+ else
+ begin
+ let id = pf_get_new_id (id_of_string "y") g in
+ tclTHENSEQ[
+ h_intro id;
+ tclTRY (Equality.rewriteLR (mkVar id));
+ intros_with_rewrite
+ ] g
+ end
+ | Ind _ when eq_constr t (Coqlib.build_coq_False ()) ->
+ Tauto.tauto g
+ | Case(_,_,v,_) ->
+ tclTHENSEQ[
+ h_case (v,Rawterm.NoBindings);
+ intros_with_rewrite
+ ] g
+ | LetIn _ ->
+ tclTHENSEQ[
+ h_reduce
+ (Rawterm.Cbv
+ {Rawterm.all_flags
+ with Rawterm.rDelta = false;
+ })
+ onConcl
+ ;
+ intros_with_rewrite
+ ] g
+ | _ ->
+ let id = pf_get_new_id (id_of_string "y") g in
+ tclTHENSEQ [ h_intro id;intros_with_rewrite] g
+ end
+ | LetIn _ ->
+ tclTHENSEQ[
+ h_reduce
+ (Rawterm.Cbv
+ {Rawterm.all_flags
+ with Rawterm.rDelta = false;
+ })
+ onConcl
+ ;
+ intros_with_rewrite
+ ] g
+ | _ -> tclIDTAC g
+
let rec reflexivity_with_destruct_cases g =
let destruct_case () =
try
@@ -492,10 +557,34 @@ let rec reflexivity_with_destruct_cases g =
| _ -> reflexivity
with _ -> reflexivity
in
- tclFIRST
+ let eq_ind = Coqlib.build_coq_eq () in
+ let discr_inject =
+ Tacticals.onAllClauses (
+ fun sc g ->
+ match sc with
+ None -> tclIDTAC g
+ | Some ((_,id),_) ->
+ match kind_of_term (pf_type_of g (mkVar id)) with
+ | App(eq,[|_;t1;t2|]) when eq_constr eq eq_ind ->
+ if Equality.discriminable (pf_env g) (project g) t1 t2
+ then Equality.discr id g
+ else if Equality.injectable (pf_env g) (project g) t1 t2
+ then tclTHEN (Equality.inj [] id) intros_with_rewrite g
+ else tclIDTAC g
+ | _ -> tclIDTAC g
+ )
+ in
+ (tclFIRST
[ reflexivity;
- destruct_case ()
- ]
+ destruct_case ();
+ (* We reach this point ONLY if
+ the same value is matched (at least) two times
+ along binding path.
+ In this case, either we have a discriminable hypothesis and we are done,
+ either at least an injectable one and we do the injection before continuing
+ *)
+ tclTHEN (tclPROGRESS discr_inject ) reflexivity_with_destruct_cases
+ ])
g
@@ -566,7 +655,6 @@ let prove_fun_complete funcs graphs schemes lemmas_types_infos i : tactic =
)
branches
in
- let eq_ind = Coqlib.build_coq_eq () in
(* We will need to change the function by its body
using [f_equation] if it is recursive (that is the graph is infinite
or unfold if the graph is finite
@@ -596,71 +684,6 @@ let prove_fun_complete funcs graphs schemes lemmas_types_infos i : tactic =
]
else unfold_in_concl [([],Names.EvalConstRef (destConst f))]
in
- (* [intros_with_rewrite] do the intros in each branch and treat each new hypothesis
- (unfolding, substituting, destructing cases \ldots)
- *)
- let rec intros_with_rewrite_aux : tactic =
- fun g ->
- match kind_of_term (pf_concl g) with
- | Prod(_,t,t') ->
- begin
- match kind_of_term t with
- | App(eq,args) when (eq_constr eq eq_ind) ->
- if isVar args.(1)
- then
- let id = pf_get_new_id (id_of_string "y") g in
- tclTHENSEQ [ h_intro id;
- generalize_depedent_of (destVar args.(1)) id;
- tclTRY (Equality.rewriteLR (mkVar id));
- intros_with_rewrite
- ]
- g
- else
- begin
- let id = pf_get_new_id (id_of_string "y") g in
- tclTHENSEQ[
- h_intro id;
- tclTRY (Equality.rewriteLR (mkVar id));
- intros_with_rewrite
- ] g
- end
- | Ind _ when eq_constr t (Coqlib.build_coq_False ()) ->
- Tauto.tauto g
- | Case(_,_,v,_) ->
- tclTHENSEQ[
- h_case (v,Rawterm.NoBindings);
- intros_with_rewrite
- ] g
- | LetIn _ ->
- tclTHENSEQ[
- h_reduce
- (Rawterm.Cbv
- {Rawterm.all_flags
- with Rawterm.rDelta = false;
- })
- onConcl
- ;
- intros_with_rewrite
- ] g
- | _ ->
- let id = pf_get_new_id (id_of_string "y") g in
- tclTHENSEQ [ h_intro id;intros_with_rewrite] g
- end
- | LetIn _ ->
- tclTHENSEQ[
- h_reduce
- (Rawterm.Cbv
- {Rawterm.all_flags
- with Rawterm.rDelta = false;
- })
- onConcl
- ;
- intros_with_rewrite
- ] g
- | _ -> tclIDTAC g
- and intros_with_rewrite g =
- observe_tac "intros_with_rewrite" intros_with_rewrite_aux g
- in
(* The proof of each branche itself *)
let ind_number = ref 0 in
let min_constr_number = ref 0 in
@@ -698,7 +721,7 @@ let prove_fun_complete funcs graphs schemes lemmas_types_infos i : tactic =
h_intro graph_principle_id;
observe_tac "" (tclTHEN_i
(observe_tac "elim" ((elim (mkVar hres,Rawterm.NoBindings) (Some (mkVar graph_principle_id,Rawterm.NoBindings)))))
- (fun i g -> prove_branche i g ))
+ (fun i g -> observe_tac "prove_branche" (prove_branche i) g ))
]
g
diff --git a/contrib/funind/rawterm_to_relation.ml b/contrib/funind/rawterm_to_relation.ml
index aca84f06..b34a1097 100644
--- a/contrib/funind/rawterm_to_relation.ml
+++ b/contrib/funind/rawterm_to_relation.ml
@@ -351,7 +351,7 @@ let rec find_type_of nb b =
then raise (Invalid_argument "find_type_of : not a valid inductive");
ind_type
end
- | RCast(_,b,_,_) -> find_type_of nb b
+ | RCast(_,b,_) -> find_type_of nb b
| RApp _ -> assert false (* we have decomposed any application via raw_decompose_app *)
| _ -> raise (Invalid_argument "not a ref")
@@ -575,7 +575,7 @@ let rec build_entry_lc env funnames avoid rt : rawconstr build_entry_return =
let f_res = build_entry_lc env funnames args_res.to_avoid f in
combine_results combine_app f_res args_res
| RDynamic _ ->error "Not handled RDynamic"
- | RCast(_,b,_,_) ->
+ | RCast(_,b,_) ->
(* for an applied cast we just trash the cast part
and restart the work.
@@ -685,7 +685,7 @@ let rec build_entry_lc env funnames avoid rt : rawconstr build_entry_return =
end
| RRec _ -> error "Not handled RRec"
- | RCast(_,b,_,_) ->
+ | RCast(_,b,_) ->
build_entry_lc env funnames avoid b
| RDynamic _ -> error "Not handled RDynamic"
and build_entry_lc_from_case env funname make_discr
diff --git a/contrib/funind/rawtermops.ml b/contrib/funind/rawtermops.ml
index ba5c2bbd..113ddd8b 100644
--- a/contrib/funind/rawtermops.ml
+++ b/contrib/funind/rawtermops.ml
@@ -18,7 +18,7 @@ let mkRLetIn(n,t,b) = RLetIn(dummy_loc,n,t,b)
let mkRCases(rto,l,brl) = RCases(dummy_loc,rto,l,brl)
let mkRSort s = RSort(dummy_loc,s)
let mkRHole () = RHole(dummy_loc,Evd.BinderType Anonymous)
-let mkRCast(b,t) = RCast(dummy_loc,b,CastCoerce,t)
+let mkRCast(b,t) = RCast(dummy_loc,b,CastConv (Term.DEFAULTcast,t))
(*
Some basic functions to decompose rawconstrs
@@ -145,8 +145,10 @@ let change_vars =
| RRec _ -> error "Local (co)fixes are not supported"
| RSort _ -> rt
| RHole _ -> rt
- | RCast(loc,b,k,t) ->
- RCast(loc,change_vars mapping b,k,change_vars mapping t)
+ | RCast(loc,b,CastConv (k,t)) ->
+ RCast(loc,change_vars mapping b, CastConv (k,change_vars mapping t))
+ | RCast(loc,b,CastCoerce) ->
+ RCast(loc,change_vars mapping b,CastCoerce)
| RDynamic _ -> error "Not handled RDynamic"
and change_vars_br mapping ((loc,idl,patl,res) as br) =
let new_mapping = List.fold_right Idmap.remove idl mapping in
@@ -324,8 +326,10 @@ let rec alpha_rt excluded rt =
| RRec _ -> error "Not handled RRec"
| RSort _ -> rt
| RHole _ -> rt
- | RCast (loc,b,k,t) ->
- RCast(loc,alpha_rt excluded b,k,alpha_rt excluded t)
+ | RCast (loc,b,CastConv (k,t)) ->
+ RCast(loc,alpha_rt excluded b,CastConv(k,alpha_rt excluded t))
+ | RCast (loc,b,CastCoerce) ->
+ RCast(loc,alpha_rt excluded b,CastCoerce)
| RDynamic _ -> error "Not handled RDynamic"
| RApp(loc,f,args) ->
RApp(loc,
@@ -375,7 +379,8 @@ let is_free_in id =
| RRec _ -> raise (UserError("",str "Not handled RRec"))
| RSort _ -> false
| RHole _ -> false
- | RCast (_,b,_,t) -> is_free_in b || is_free_in t
+ | RCast (_,b,CastConv (_,t)) -> is_free_in b || is_free_in t
+ | RCast (_,b,CastCoerce) -> is_free_in b
| RDynamic _ -> raise (UserError("",str "Not handled RDynamic"))
and is_free_in_br (_,ids,_,rt) =
(not (List.mem id ids)) && is_free_in rt
@@ -469,8 +474,10 @@ let replace_var_by_term x_id term =
| RRec _ -> raise (UserError("",str "Not handled RRec"))
| RSort _ -> rt
| RHole _ -> rt
- | RCast(loc,b,k,t) ->
- RCast(loc,replace_var_by_pattern b,k,replace_var_by_pattern t)
+ | RCast(loc,b,CastConv(k,t)) ->
+ RCast(loc,replace_var_by_pattern b,CastConv(k,replace_var_by_pattern t))
+ | RCast(loc,b,CastCoerce) ->
+ RCast(loc,replace_var_by_pattern b,CastCoerce)
| RDynamic _ -> raise (UserError("",str "Not handled RDynamic"))
and replace_var_by_pattern_br ((loc,idl,patl,res) as br) =
if List.exists (fun id -> id_ord id x_id == 0) idl
@@ -554,7 +561,8 @@ let ids_of_rawterm c =
| RLambda (loc,na,ty,c) -> idof na :: ids_of_rawterm [] ty @ ids_of_rawterm [] c @ acc
| RProd (loc,na,ty,c) -> idof na :: ids_of_rawterm [] ty @ ids_of_rawterm [] c @ acc
| RLetIn (loc,na,b,c) -> idof na :: ids_of_rawterm [] b @ ids_of_rawterm [] c @ acc
- | RCast (loc,c,k,t) -> ids_of_rawterm [] c @ ids_of_rawterm [] t @ acc
+ | RCast (loc,c,CastConv(k,t)) -> ids_of_rawterm [] c @ ids_of_rawterm [] t @ acc
+ | RCast (loc,c,CastCoerce) -> ids_of_rawterm [] c @ acc
| RIf (loc,c,(na,po),b1,b2) -> ids_of_rawterm [] c @ ids_of_rawterm [] b1 @ ids_of_rawterm [] b2 @ acc
| RLetTuple (_,nal,(na,po),b,c) ->
List.map idof nal @ ids_of_rawterm [] b @ ids_of_rawterm [] c @ acc
@@ -619,8 +627,10 @@ let zeta_normalize =
| RRec _ -> raise (UserError("",str "Not handled RRec"))
| RSort _ -> rt
| RHole _ -> rt
- | RCast(loc,b,k,t) ->
- RCast(loc,zeta_normalize_term b,k,zeta_normalize_term t)
+ | RCast(loc,b,CastConv(k,t)) ->
+ RCast(loc,zeta_normalize_term b,CastConv(k,zeta_normalize_term t))
+ | RCast(loc,b,CastCoerce) ->
+ RCast(loc,zeta_normalize_term b,CastCoerce)
| RDynamic _ -> raise (UserError("",str "Not handled RDynamic"))
and zeta_normalize_br (loc,idl,patl,res) =
(loc,idl,patl,zeta_normalize_term res)
@@ -660,7 +670,8 @@ let expand_as =
expand_as map br1, expand_as map br2)
| RRec _ -> error "Not handled RRec"
| RDynamic _ -> error "Not handled RDynamic"
- | RCast(loc,b,kind,t) -> RCast(loc,expand_as map b,kind,expand_as map t)
+ | RCast(loc,b,CastConv(kind,t)) -> RCast(loc,expand_as map b,CastConv(kind,expand_as map t))
+ | RCast(loc,b,CastCoerce) -> RCast(loc,expand_as map b,CastCoerce)
| RCases(loc,po,el,brl) ->
RCases(loc, option_map (expand_as map) po, List.map (fun (rt,t) -> expand_as map rt,t) el,
List.map (expand_as_br map) brl)
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-13 16:10:45 +0000