aboutsummaryrefslogtreecommitdiff
path: root/plugins/funind
diff options
context:
space:
mode:
authorHugo Herbelin2020-09-29 22:23:54 +0200
committerHugo Herbelin2020-09-29 22:24:02 +0200
commitbe3a5ac947cb57499b668a3745439b15ff8c48a8 (patch)
tree4be94702b8e6796c08b509d260cf2c9fcb0d1918 /plugins/funind
parent5cac24428e448c12ab292265bb2ffd1146b38c25 (diff)
Applying ocamlformat.
Diffstat (limited to 'plugins/funind')
-rw-r--r--plugins/funind/functional_principles_proofs.ml1883
-rw-r--r--plugins/funind/gen_principle.ml1007
-rw-r--r--plugins/funind/indfun_common.ml4
-rw-r--r--plugins/funind/recdef.ml1314
4 files changed, 2146 insertions, 2062 deletions
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index 118a2f3a2e..e50c6087bb 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -44,14 +44,11 @@ type 'a dynamic_info =
type body_info = constr dynamic_info
-let observe_tac s = New.observe_tac ~header:(str "observation") (fun _ _ -> Pp.str s)
-
-let finish_proof dynamic_infos =
- observe_tac "finish" assumption
-
-let refine c =
- Logic.refiner ~check:true EConstr.Unsafe.(to_constr c)
+let observe_tac s =
+ New.observe_tac ~header:(str "observation") (fun _ _ -> Pp.str s)
+let finish_proof dynamic_infos = observe_tac "finish" assumption
+let refine c = Logic.refiner ~check:true EConstr.Unsafe.(to_constr c)
let thin = clear
let eq_constr sigma u v = EConstr.eq_constr_nounivs sigma u v
@@ -95,15 +92,16 @@ let pf_get_new_id id env =
let change_hyp_with_using msg hyp_id t tac =
Proofview.Goal.enter (fun gl ->
- let prov_id = pf_get_new_id hyp_id (Proofview.Goal.hyps gl) in
- Tacticals.New.tclTHENS
- ((* observe_tac msg *)
- (assert_by (Name prov_id) t (Tacticals.New.tclCOMPLETE tac)))
- [ Tacticals.New.tclTHENLIST
- [ (* observe_tac "change_hyp_with_using thin" *)
- Tactics.clear [hyp_id]
- ; (* observe_tac "change_hyp_with_using rename " *)
- rename_hyp [(prov_id, hyp_id)] ] ])
+ let prov_id = pf_get_new_id hyp_id (Proofview.Goal.hyps gl) in
+ Tacticals.New.tclTHENS
+ ((* observe_tac msg *)
+ assert_by (Name prov_id) t
+ (Tacticals.New.tclCOMPLETE tac))
+ [ Tacticals.New.tclTHENLIST
+ [ (* observe_tac "change_hyp_with_using thin" *)
+ Tactics.clear [hyp_id]
+ ; (* observe_tac "change_hyp_with_using rename " *)
+ rename_hyp [(prov_id, hyp_id)] ] ])
exception TOREMOVE
@@ -113,17 +111,18 @@ let prove_trivial_eq h_id context (constructor, type_of_term, term) =
[ Tacticals.New.tclDO nb_intros intro
; (* introducing context *)
Proofview.Goal.enter (fun g ->
- let hyps = Proofview.Goal.hyps g in
- let context_hyps =
- fst
- (list_chop ~msg:"prove_trivial_eq : " nb_intros (ids_of_named_context hyps))
- in
- let context_hyps' =
- mkApp (constructor, [|type_of_term; term|])
- :: List.map mkVar context_hyps
- in
- let to_refine = applist (mkVar h_id, List.rev context_hyps') in
- refine to_refine) ]
+ let hyps = Proofview.Goal.hyps g in
+ let context_hyps =
+ fst
+ (list_chop ~msg:"prove_trivial_eq : " nb_intros
+ (ids_of_named_context hyps))
+ in
+ let context_hyps' =
+ mkApp (constructor, [|type_of_term; term|])
+ :: List.map mkVar context_hyps
+ in
+ let to_refine = applist (mkVar h_id, List.rev context_hyps') in
+ refine to_refine) ]
let find_rectype env sigma c =
let t, l = decompose_app sigma (Reductionops.whd_betaiotazeta env sigma c) in
@@ -265,9 +264,7 @@ let change_eq env sigma hyp_id (context : rel_context) x t end_of_type =
Typing.type_of (Proofview.Goal.env g) (Proofview.Goal.sigma g)
to_refine
in
- tclTHEN
- (Proofview.Unsafe.tclEVARS evm)
- (refine to_refine)))
+ tclTHEN (Proofview.Unsafe.tclEVARS evm) (refine to_refine)))
in
let simpl_eq_tac =
change_hyp_with_using "prove_pattern_simplification" hyp_id new_type_of_hyp
@@ -304,9 +301,7 @@ let isLetIn sigma t =
match EConstr.kind sigma t with LetIn _ -> true | _ -> false
let h_reduce_with_zeta cl =
- reduce
- (Genredexpr.Cbv {Redops.all_flags with Genredexpr.rDelta = false})
- cl
+ reduce (Genredexpr.Cbv {Redops.all_flags with Genredexpr.rDelta = false}) cl
let rewrite_until_var arg_num eq_ids : unit Proofview.tactic =
let open Tacticals.New in
@@ -321,14 +316,15 @@ let rewrite_until_var arg_num eq_ids : unit Proofview.tactic =
in
let rec do_rewrite eq_ids =
Proofview.Goal.enter (fun g ->
- if test_var g then Proofview.tclUNIT ()
- else
- match eq_ids with
- | [] -> anomaly (Pp.str "Cannot find a way to prove recursive property.")
- | eq_id :: eq_ids ->
- tclTHEN
- (tclTRY (Equality.rewriteRL (mkVar eq_id)))
- (do_rewrite eq_ids))
+ if test_var g then Proofview.tclUNIT ()
+ else
+ match eq_ids with
+ | [] ->
+ anomaly (Pp.str "Cannot find a way to prove recursive property.")
+ | eq_id :: eq_ids ->
+ tclTHEN
+ (tclTRY (Equality.rewriteRL (mkVar eq_id)))
+ (do_rewrite eq_ids))
in
do_rewrite eq_ids
@@ -376,26 +372,25 @@ let clean_hyp_with_heq ptes_infos eq_hyps hyp_id env sigma =
tclTHENLIST
[ tclDO context_length intro
; Proofview.Goal.enter (fun g ->
- let hyps = Proofview.Goal.hyps g in
- let context_hyps_ids =
- fst
- (list_chop ~msg:"rec hyp : context_hyps" context_length
- (ids_of_named_context hyps))
- in
- let rec_pte_id = pf_get_new_id rec_pte_id hyps in
- let to_refine =
- applist
- ( mkVar hyp_id
- , List.rev_map mkVar (rec_pte_id :: context_hyps_ids) )
- in
- (* observe_tac "rec hyp " *)
- tclTHENS
- (assert_before (Name rec_pte_id) t_x)
- [ (* observe_tac "prove rec hyp" *)
- prove_rec_hyp eq_hyps
- ; (* observe_tac "prove rec hyp" *)
- refine to_refine ])
- ]
+ let hyps = Proofview.Goal.hyps g in
+ let context_hyps_ids =
+ fst
+ (list_chop ~msg:"rec hyp : context_hyps" context_length
+ (ids_of_named_context hyps))
+ in
+ let rec_pte_id = pf_get_new_id rec_pte_id hyps in
+ let to_refine =
+ applist
+ ( mkVar hyp_id
+ , List.rev_map mkVar (rec_pte_id :: context_hyps_ids) )
+ in
+ (* observe_tac "rec hyp " *)
+ tclTHENS
+ (assert_before (Name rec_pte_id) t_x)
+ [ (* observe_tac "prove rec hyp" *)
+ prove_rec_hyp eq_hyps
+ ; (* observe_tac "prove rec hyp" *)
+ refine to_refine ]) ]
in
tclTHENLIST
[ (* observe_tac "hyp rec" *)
@@ -422,18 +417,18 @@ let clean_hyp_with_heq ptes_infos eq_hyps hyp_id env sigma =
tclTHENLIST
[ tclDO nb_intro intro
; Proofview.Goal.enter (fun g ->
- let hyps = Proofview.Goal.hyps g in
- let context_hyps =
- fst
- (list_chop ~msg:"removing True : context_hyps " nb_intro
- (ids_of_named_context hyps))
- in
- let to_refine =
- applist
- ( mkVar hyp_id
- , List.rev (coq_I :: List.map mkVar context_hyps) )
- in
- refine to_refine) ]
+ let hyps = Proofview.Goal.hyps g in
+ let context_hyps =
+ fst
+ (list_chop ~msg:"removing True : context_hyps " nb_intro
+ (ids_of_named_context hyps))
+ in
+ let to_refine =
+ applist
+ ( mkVar hyp_id
+ , List.rev (coq_I :: List.map mkVar context_hyps) )
+ in
+ refine to_refine) ]
in
tclTHENLIST
[ change_hyp_with_using "prove_trivial" hyp_id real_type_of_hyp
@@ -471,94 +466,99 @@ let clean_hyp_with_heq ptes_infos eq_hyps hyp_id env sigma =
let clean_goal_with_heq ptes_infos continue_tac (dyn_infos : body_info) =
let open Tacticals.New in
Proofview.Goal.enter (fun g ->
- let env = Proofview.Goal.env g in
- let sigma = Proofview.Goal.sigma g in
- let tac, new_hyps =
- List.fold_left
- (fun (hyps_tac, new_hyps) hyp_id ->
- let hyp_tac, new_hyp =
- clean_hyp_with_heq ptes_infos dyn_infos.eq_hyps hyp_id env sigma
- in
- (tclTHEN hyp_tac hyps_tac, new_hyp @ new_hyps))
- (tclIDTAC, []) dyn_infos.rec_hyps
- in
- let new_infos =
- {dyn_infos with rec_hyps = new_hyps; nb_rec_hyps = List.length new_hyps}
- in
- tclTHENLIST
- [tac; (* observe_tac "clean_hyp_with_heq continue" *) continue_tac new_infos])
+ let env = Proofview.Goal.env g in
+ let sigma = Proofview.Goal.sigma g in
+ let tac, new_hyps =
+ List.fold_left
+ (fun (hyps_tac, new_hyps) hyp_id ->
+ let hyp_tac, new_hyp =
+ clean_hyp_with_heq ptes_infos dyn_infos.eq_hyps hyp_id env sigma
+ in
+ (tclTHEN hyp_tac hyps_tac, new_hyp @ new_hyps))
+ (tclIDTAC, []) dyn_infos.rec_hyps
+ in
+ let new_infos =
+ {dyn_infos with rec_hyps = new_hyps; nb_rec_hyps = List.length new_hyps}
+ in
+ tclTHENLIST
+ [ tac
+ ; (* observe_tac "clean_hyp_with_heq continue" *)
+ continue_tac new_infos ])
let heq_id = Id.of_string "Heq"
let treat_new_case ptes_infos nb_prod continue_tac term dyn_infos =
let open Tacticals.New in
Proofview.Goal.enter (fun g ->
- let nb_first_intro = nb_prod - 1 - dyn_infos.nb_rec_hyps in
- tclTHENLIST
- [ (* We first introduce the variables *)
- tclDO nb_first_intro
- (intro_avoiding (Id.Set.of_list dyn_infos.rec_hyps))
- ; (* Then the equation itself *)
- (intro_using_then heq_id
- (* we get the fresh name with onLastHypId *)
- (fun _ -> Proofview.tclUNIT ()))
- ; onLastHypId (fun heq_id ->
- tclTHENLIST
- [ (* Then the new hypothesis *)
- tclMAP
- introduction
- dyn_infos.rec_hyps
- ; observe_tac "after_introduction"
- (Proofview.Goal.enter (fun g' ->
- let env = Proofview.Goal.env g' in
- let sigma = Proofview.Goal.sigma g' in
- (* We get infos on the equations introduced*)
- let new_term_value_eq = Tacmach.New.pf_get_hyp_typ heq_id g' in
- (* compute the new value of the body *)
- let new_term_value =
- match EConstr.kind sigma new_term_value_eq with
- | App (f, [|_; _; args2|]) -> args2
- | _ ->
- observe
- ( str "cannot compute new term value : "
- ++ Tacmach.New.pr_gls g' ++ fnl () ++ str "last hyp is"
- ++ pr_leconstr_env env sigma new_term_value_eq );
- anomaly (Pp.str "cannot compute new term value.")
- in
- tclTYPEOFTHEN term (fun sigma termtyp ->
- let fun_body =
- mkLambda
- ( make_annot Anonymous Sorts.Relevant
- , termtyp
- , Termops.replace_term sigma term (mkRel 1)
- dyn_infos.info )
- in
- let new_body =
- Reductionops.nf_betaiota env sigma (mkApp (fun_body, [|new_term_value|]))
- in
- let new_infos =
- { dyn_infos with
- info = new_body
- ; eq_hyps = heq_id :: dyn_infos.eq_hyps }
- in
- clean_goal_with_heq ptes_infos continue_tac new_infos))) ])
- ])
+ let nb_first_intro = nb_prod - 1 - dyn_infos.nb_rec_hyps in
+ tclTHENLIST
+ [ (* We first introduce the variables *)
+ tclDO nb_first_intro
+ (intro_avoiding (Id.Set.of_list dyn_infos.rec_hyps))
+ ; (* Then the equation itself *)
+ intro_using_then heq_id
+ (* we get the fresh name with onLastHypId *)
+ (fun _ -> Proofview.tclUNIT ())
+ ; onLastHypId (fun heq_id ->
+ tclTHENLIST
+ [ (* Then the new hypothesis *)
+ tclMAP introduction dyn_infos.rec_hyps
+ ; observe_tac "after_introduction"
+ (Proofview.Goal.enter (fun g' ->
+ let env = Proofview.Goal.env g' in
+ let sigma = Proofview.Goal.sigma g' in
+ (* We get infos on the equations introduced*)
+ let new_term_value_eq =
+ Tacmach.New.pf_get_hyp_typ heq_id g'
+ in
+ (* compute the new value of the body *)
+ let new_term_value =
+ match EConstr.kind sigma new_term_value_eq with
+ | App (f, [|_; _; args2|]) -> args2
+ | _ ->
+ observe
+ ( str "cannot compute new term value : "
+ ++ Tacmach.New.pr_gls g' ++ fnl ()
+ ++ str "last hyp is"
+ ++ pr_leconstr_env env sigma new_term_value_eq );
+ anomaly (Pp.str "cannot compute new term value.")
+ in
+ tclTYPEOFTHEN term (fun sigma termtyp ->
+ let fun_body =
+ mkLambda
+ ( make_annot Anonymous Sorts.Relevant
+ , termtyp
+ , Termops.replace_term sigma term (mkRel 1)
+ dyn_infos.info )
+ in
+ let new_body =
+ Reductionops.nf_betaiota env sigma
+ (mkApp (fun_body, [|new_term_value|]))
+ in
+ let new_infos =
+ { dyn_infos with
+ info = new_body
+ ; eq_hyps = heq_id :: dyn_infos.eq_hyps }
+ in
+ clean_goal_with_heq ptes_infos continue_tac
+ new_infos))) ]) ])
-let instantiate_hyps_with_args (do_prove : Id.t list -> unit Proofview.tactic) hyps args_id =
+let instantiate_hyps_with_args (do_prove : Id.t list -> unit Proofview.tactic)
+ hyps args_id =
let args = Array.of_list (List.map mkVar args_id) in
let open Tacticals.New in
let instantiate_one_hyp hid =
tclORELSE0
- (* we instantiate the hyp if possible *)
+ (* we instantiate the hyp if possible *)
(Proofview.Goal.enter (fun g ->
- let prov_hid = Tacmach.New.pf_get_new_id hid g in
- let c = mkApp (mkVar hid, args) in
- (* Check typing *)
- tclTYPEOFTHEN c (fun _ _ ->
- tclTHENLIST
- [ pose_proof (Name prov_hid) c
- ; thin [hid]
- ; rename_hyp [(prov_hid, hid)]])))
+ let prov_hid = Tacmach.New.pf_get_new_id hid g in
+ let c = mkApp (mkVar hid, args) in
+ (* Check typing *)
+ tclTYPEOFTHEN c (fun _ _ ->
+ tclTHENLIST
+ [ pose_proof (Name prov_hid) c
+ ; thin [hid]
+ ; rename_hyp [(prov_hid, hid)] ])))
(*
if not then we are in a mutual function block
and this hyp is a recursive hyp on an other function.
@@ -567,8 +567,8 @@ let instantiate_hyps_with_args (do_prove : Id.t list -> unit Proofview.tactic) h
principle so that we can trash it
*)
- (* observe (str "Instantiation: removing hyp " ++ Ppconstr.pr_id hid); *)
- (thin [hid])
+ (* observe (str "Instantiation: removing hyp " ++ Ppconstr.pr_id hid); *)
+ (thin [hid])
in
if List.is_empty args_id then
tclTHENLIST
@@ -579,130 +579,144 @@ let instantiate_hyps_with_args (do_prove : Id.t list -> unit Proofview.tactic) h
[ tclMAP (fun hyp_id -> h_reduce_with_zeta (Locusops.onHyp hyp_id)) hyps
; tclMAP instantiate_one_hyp hyps
; Proofview.Goal.enter (fun g ->
- let all_g_hyps_id =
- List.fold_right Id.Set.add (Tacmach.New.pf_ids_of_hyps g) Id.Set.empty
- in
- let remaining_hyps =
- List.filter (fun id -> Id.Set.mem id all_g_hyps_id) hyps
- in
- do_prove remaining_hyps) ]
+ let all_g_hyps_id =
+ List.fold_right Id.Set.add
+ (Tacmach.New.pf_ids_of_hyps g)
+ Id.Set.empty
+ in
+ let remaining_hyps =
+ List.filter (fun id -> Id.Set.mem id all_g_hyps_id) hyps
+ in
+ do_prove remaining_hyps) ]
let build_proof (interactive_proof : bool) (fnames : Constant.t list) ptes_infos
dyn_infos : unit Proofview.tactic =
let open Tacticals.New in
let rec build_proof_aux do_finalize dyn_infos : unit Proofview.tactic =
Proofview.Goal.enter (fun g ->
- let env = Proofview.Goal.env g in
- let sigma = Proofview.Goal.sigma g in
- (* observe (str "proving on " ++ Printer.pr_lconstr_env (pf_env g) term);*)
- match EConstr.kind sigma dyn_infos.info with
- | Case (ci, ct, iv, t, cb) ->
- let do_finalize_t dyn_info' =
- Proofview.Goal.enter (fun g ->
- let t = dyn_info'.info in
- let dyn_infos = {dyn_info' with info = mkCase (ci, ct, iv, t, cb)} in
- let g_nb_prod = nb_prod (Proofview.Goal.sigma g) (Proofview.Goal.concl g) in
- tclTYPEOFTHEN t (fun _ type_of_term ->
- let term_eq = make_refl_eq (Lazy.force refl_equal) type_of_term t in
- tclTHENLIST
- [ generalize (term_eq :: List.map mkVar dyn_infos.rec_hyps)
- ; thin dyn_infos.rec_hyps
- ; pattern_option [(Locus.AllOccurrencesBut [1], t)] None
- ; observe_tac "toto"
- (tclTHENLIST
- [ Simple.case t
- ; Proofview.Goal.enter (fun g' ->
- let g'_nb_prod = nb_prod (Proofview.Goal.sigma g') (Proofview.Goal.concl g') in
- let nb_instantiate_partial = g'_nb_prod - g_nb_prod in
- observe_tac "treat_new_case"
- (treat_new_case ptes_infos nb_instantiate_partial
- (build_proof do_finalize) t dyn_infos)
- ) ])
- ]))
- in
- build_proof do_finalize_t {dyn_infos with info = t}
- | Lambda (n, t, b) -> (
- match EConstr.kind sigma (Proofview.Goal.concl g) with
- | Prod _ ->
- tclTHEN
- intro
- (Proofview.Goal.enter (fun g' ->
- let open Context.Named.Declaration in
- let id = Tacmach.New.pf_last_hyp g' |> get_id in
- let new_term =
- Reductionops.nf_betaiota (Proofview.Goal.env g') (Proofview.Goal.sigma g') (mkApp (dyn_infos.info, [|mkVar id|]))
+ let env = Proofview.Goal.env g in
+ let sigma = Proofview.Goal.sigma g in
+ (* observe (str "proving on " ++ Printer.pr_lconstr_env (pf_env g) term);*)
+ match EConstr.kind sigma dyn_infos.info with
+ | Case (ci, ct, iv, t, cb) ->
+ let do_finalize_t dyn_info' =
+ Proofview.Goal.enter (fun g ->
+ let t = dyn_info'.info in
+ let dyn_infos =
+ {dyn_info' with info = mkCase (ci, ct, iv, t, cb)}
+ in
+ let g_nb_prod =
+ nb_prod (Proofview.Goal.sigma g) (Proofview.Goal.concl g)
+ in
+ tclTYPEOFTHEN t (fun _ type_of_term ->
+ let term_eq =
+ make_refl_eq (Lazy.force refl_equal) type_of_term t
+ in
+ tclTHENLIST
+ [ generalize (term_eq :: List.map mkVar dyn_infos.rec_hyps)
+ ; thin dyn_infos.rec_hyps
+ ; pattern_option [(Locus.AllOccurrencesBut [1], t)] None
+ ; observe_tac "toto"
+ (tclTHENLIST
+ [ Simple.case t
+ ; Proofview.Goal.enter (fun g' ->
+ let g'_nb_prod =
+ nb_prod (Proofview.Goal.sigma g')
+ (Proofview.Goal.concl g')
+ in
+ let nb_instantiate_partial =
+ g'_nb_prod - g_nb_prod
+ in
+ observe_tac "treat_new_case"
+ (treat_new_case ptes_infos
+ nb_instantiate_partial
+ (build_proof do_finalize) t dyn_infos))
+ ]) ]))
+ in
+ build_proof do_finalize_t {dyn_infos with info = t}
+ | Lambda (n, t, b) -> (
+ match EConstr.kind sigma (Proofview.Goal.concl g) with
+ | Prod _ ->
+ tclTHEN intro
+ (Proofview.Goal.enter (fun g' ->
+ let open Context.Named.Declaration in
+ let id = Tacmach.New.pf_last_hyp g' |> get_id in
+ let new_term =
+ Reductionops.nf_betaiota (Proofview.Goal.env g')
+ (Proofview.Goal.sigma g')
+ (mkApp (dyn_infos.info, [|mkVar id|]))
+ in
+ let new_infos = {dyn_infos with info = new_term} in
+ let do_prove new_hyps =
+ build_proof do_finalize
+ { new_infos with
+ rec_hyps = new_hyps
+ ; nb_rec_hyps = List.length new_hyps }
+ in
+ (* observe_tac "Lambda" *)
+ instantiate_hyps_with_args do_prove new_infos.rec_hyps [id]
+ (* build_proof do_finalize new_infos g' *)))
+ | _ -> do_finalize dyn_infos )
+ | Cast (t, _, _) -> build_proof do_finalize {dyn_infos with info = t}
+ | Const _ | Var _ | Meta _ | Evar _ | Sort _ | Construct _ | Ind _
+ |Int _ | Float _ ->
+ do_finalize dyn_infos
+ | App (_, _) -> (
+ let f, args = decompose_app sigma dyn_infos.info in
+ match EConstr.kind sigma f with
+ | Int _ -> user_err Pp.(str "integer cannot be applied")
+ | Float _ -> user_err Pp.(str "float cannot be applied")
+ | Array _ -> user_err Pp.(str "array cannot be applied")
+ | App _ ->
+ assert false (* we have collected all the app in decompose_app *)
+ | Proj _ -> assert false (*FIXME*)
+ | Var _ | Construct _ | Rel _ | Evar _ | Meta _ | Ind _ | Sort _
+ |Prod _ ->
+ let new_infos = {dyn_infos with info = (f, args)} in
+ build_proof_args env sigma do_finalize new_infos
+ | Const (c, _) when not (List.mem_f Constant.equal c fnames) ->
+ let new_infos = {dyn_infos with info = (f, args)} in
+ (* Pp.msgnl (str "proving in " ++ pr_lconstr_env (pf_env g) dyn_infos.info); *)
+ build_proof_args env sigma do_finalize new_infos
+ | Const _ -> do_finalize dyn_infos
+ | Lambda _ ->
+ let new_term = Reductionops.nf_beta env sigma dyn_infos.info in
+ build_proof do_finalize {dyn_infos with info = new_term}
+ | LetIn _ ->
+ let new_infos =
+ { dyn_infos with
+ info = Reductionops.nf_betaiotazeta env sigma dyn_infos.info }
in
- let new_infos = {dyn_infos with info = new_term} in
- let do_prove new_hyps =
- build_proof do_finalize
- { new_infos with
- rec_hyps = new_hyps
- ; nb_rec_hyps = List.length new_hyps }
+ tclTHENLIST
+ [ tclMAP
+ (fun hyp_id -> h_reduce_with_zeta (Locusops.onHyp hyp_id))
+ dyn_infos.rec_hyps
+ ; h_reduce_with_zeta Locusops.onConcl
+ ; build_proof do_finalize new_infos ]
+ | Cast (b, _, _) -> build_proof do_finalize {dyn_infos with info = b}
+ | Case _ | Fix _ | CoFix _ ->
+ let new_finalize dyn_infos =
+ let new_infos = {dyn_infos with info = (dyn_infos.info, args)} in
+ build_proof_args env sigma do_finalize new_infos
in
- (* observe_tac "Lambda" *)
- (instantiate_hyps_with_args do_prove new_infos.rec_hyps [id])
- (* build_proof do_finalize new_infos g' *)))
- | _ -> do_finalize dyn_infos)
- | Cast (t, _, _) -> build_proof do_finalize {dyn_infos with info = t}
- | Const _ | Var _ | Meta _ | Evar _ | Sort _ | Construct _ | Ind _ | Int _
- | Float _ ->
- do_finalize dyn_infos
- | App (_, _) -> (
- let f, args = decompose_app sigma dyn_infos.info in
- match EConstr.kind sigma f with
- | Int _ -> user_err Pp.(str "integer cannot be applied")
- | Float _ -> user_err Pp.(str "float cannot be applied")
- | Array _ -> user_err Pp.(str "array cannot be applied")
- | App _ ->
- assert false (* we have collected all the app in decompose_app *)
- | Proj _ -> assert false (*FIXME*)
- | Var _ | Construct _ | Rel _ | Evar _ | Meta _ | Ind _ | Sort _ | Prod _
- ->
- let new_infos = {dyn_infos with info = (f, args)} in
- build_proof_args env sigma do_finalize new_infos
- | Const (c, _) when not (List.mem_f Constant.equal c fnames) ->
- let new_infos = {dyn_infos with info = (f, args)} in
- (* Pp.msgnl (str "proving in " ++ pr_lconstr_env (pf_env g) dyn_infos.info); *)
- build_proof_args env sigma do_finalize new_infos
- | Const _ -> do_finalize dyn_infos
- | Lambda _ ->
- let new_term = Reductionops.nf_beta env sigma dyn_infos.info in
- build_proof do_finalize {dyn_infos with info = new_term}
- | LetIn _ ->
- let new_infos =
- { dyn_infos with
- info = Reductionops.nf_betaiotazeta env sigma dyn_infos.info }
- in
- tclTHENLIST
- [ tclMAP
- (fun hyp_id -> h_reduce_with_zeta (Locusops.onHyp hyp_id))
- dyn_infos.rec_hyps
- ; h_reduce_with_zeta Locusops.onConcl
- ; build_proof do_finalize new_infos ]
- | Cast (b, _, _) -> build_proof do_finalize {dyn_infos with info = b}
- | Case _ | Fix _ | CoFix _ ->
- let new_finalize dyn_infos =
- let new_infos = {dyn_infos with info = (dyn_infos.info, args)} in
- build_proof_args env sigma do_finalize new_infos
- in
- build_proof new_finalize {dyn_infos with info = f})
- | Fix _ | CoFix _ ->
- user_err Pp.(str "Anonymous local (co)fixpoints are not handled yet")
- | Proj _ -> user_err Pp.(str "Prod")
- | Prod _ -> do_finalize dyn_infos
- | LetIn _ ->
- let new_infos =
- { dyn_infos with
- info = Reductionops.nf_betaiotazeta env sigma dyn_infos.info }
- in
- tclTHENLIST
- [ tclMAP
- (fun hyp_id -> h_reduce_with_zeta (Locusops.onHyp hyp_id))
- dyn_infos.rec_hyps
- ; h_reduce_with_zeta Locusops.onConcl
- ; build_proof do_finalize new_infos ]
- | Rel _ -> anomaly (Pp.str "Free var in goal conclusion!")
- | Array _ -> CErrors.user_err Pp.(str "Arrays not handled yet"))
+ build_proof new_finalize {dyn_infos with info = f} )
+ | Fix _ | CoFix _ ->
+ user_err Pp.(str "Anonymous local (co)fixpoints are not handled yet")
+ | Proj _ -> user_err Pp.(str "Prod")
+ | Prod _ -> do_finalize dyn_infos
+ | LetIn _ ->
+ let new_infos =
+ { dyn_infos with
+ info = Reductionops.nf_betaiotazeta env sigma dyn_infos.info }
+ in
+ tclTHENLIST
+ [ tclMAP
+ (fun hyp_id -> h_reduce_with_zeta (Locusops.onHyp hyp_id))
+ dyn_infos.rec_hyps
+ ; h_reduce_with_zeta Locusops.onConcl
+ ; build_proof do_finalize new_infos ]
+ | Rel _ -> anomaly (Pp.str "Free var in goal conclusion!")
+ | Array _ -> CErrors.user_err Pp.(str "Arrays not handled yet"))
and build_proof do_finalize dyn_infos =
(* observe (str "proving with "++Printer.pr_lconstr dyn_infos.info++ str " on goal " ++ pr_gls g); *)
Indfun_common.New.observe_tac ~header:(str "observation")
@@ -710,31 +724,32 @@ let build_proof (interactive_proof : bool) (fnames : Constant.t list) ptes_infos
str "build_proof with " ++ pr_leconstr_env env sigma dyn_infos.info)
(build_proof_aux do_finalize dyn_infos)
and build_proof_args env sigma do_finalize dyn_infos : unit Proofview.tactic =
- (* f_args' args *)
- Proofview.Goal.enter (fun g ->
- let f_args', args = dyn_infos.info in
- let tac = match args with
- | [] -> do_finalize {dyn_infos with info = f_args'}
- | arg :: args ->
- (* observe (str "build_proof_args with arg := "++ pr_lconstr_env (pf_env g) arg++ *)
- (* fnl () ++ *)
- (* pr_goal (Tacmach.sig_it g) *)
- (* ); *)
- let do_finalize dyn_infos =
- let new_arg = dyn_infos.info in
- (* tclTRYD *)
- build_proof_args env sigma do_finalize
- {dyn_infos with info = (mkApp (f_args', [|new_arg|]), args)}
+ (* f_args' args *)
+ Proofview.Goal.enter (fun g ->
+ let f_args', args = dyn_infos.info in
+ let tac =
+ match args with
+ | [] -> do_finalize {dyn_infos with info = f_args'}
+ | arg :: args ->
+ (* observe (str "build_proof_args with arg := "++ pr_lconstr_env (pf_env g) arg++ *)
+ (* fnl () ++ *)
+ (* pr_goal (Tacmach.sig_it g) *)
+ (* ); *)
+ let do_finalize dyn_infos =
+ let new_arg = dyn_infos.info in
+ (* tclTRYD *)
+ build_proof_args env sigma do_finalize
+ {dyn_infos with info = (mkApp (f_args', [|new_arg|]), args)}
+ in
+ build_proof do_finalize {dyn_infos with info = arg}
in
- build_proof do_finalize {dyn_infos with info = arg}
- in
- (* observe_tac "build_proof_args" *) tac)
+ (* observe_tac "build_proof_args" *) tac)
in
let do_finish_proof dyn_infos =
(* tclTRYD *) clean_goal_with_heq ptes_infos finish_proof dyn_infos
in
(* observe_tac "build_proof" *)
- build_proof (clean_goal_with_heq ptes_infos do_finish_proof) dyn_infos
+ build_proof (clean_goal_with_heq ptes_infos do_finish_proof) dyn_infos
(* Proof of principles from structural functions *)
@@ -749,45 +764,48 @@ type static_fix_info =
let prove_rec_hyp_for_struct fix_info eq_hyps =
let open Tacticals.New in
- tclTHEN (rewrite_until_var fix_info.idx eq_hyps)
+ tclTHEN
+ (rewrite_until_var fix_info.idx eq_hyps)
(Proofview.Goal.enter (fun g ->
- let _, pte_args = destApp (Proofview.Goal.sigma g) (Proofview.Goal.concl g) in
- let rec_hyp_proof =
- mkApp (mkVar fix_info.name, array_get_start pte_args)
- in
- refine rec_hyp_proof))
+ let _, pte_args =
+ destApp (Proofview.Goal.sigma g) (Proofview.Goal.concl g)
+ in
+ let rec_hyp_proof =
+ mkApp (mkVar fix_info.name, array_get_start pte_args)
+ in
+ refine rec_hyp_proof))
let prove_rec_hyp fix_info =
{proving_tac = prove_rec_hyp_for_struct fix_info; is_valid = (fun _ -> true)}
let generalize_non_dep hyp =
Proofview.Goal.enter (fun g ->
- (* observe (str "rec id := " ++ Ppconstr.pr_id hyp); *)
- let hyps = [hyp] in
- let env = Global.env () in
- let sigma = Proofview.Goal.sigma g in
- let hyp_typ = Tacmach.New.pf_get_hyp_typ hyp g in
- let to_revert, _ =
- let open Context.Named.Declaration in
- Environ.fold_named_context_reverse
- (fun (clear, keep) decl ->
- let decl = map_named_decl EConstr.of_constr decl in
- let hyp = get_id decl in
- if
- Id.List.mem hyp hyps
- || List.exists (Termops.occur_var_in_decl env sigma hyp) keep
- || Termops.occur_var env sigma hyp hyp_typ
- || Termops.is_section_variable hyp
- (* should be dangerous *)
- then (clear, decl :: keep)
- else (hyp :: clear, keep))
- ~init:([], []) (Proofview.Goal.env g)
- in
- (* observe (str "to_revert := " ++ prlist_with_sep spc Ppconstr.pr_id to_revert); *)
- Tacticals.New.tclTHEN
- ((* observe_tac "h_generalize" *)
- (generalize (List.map mkVar to_revert)))
- ((* observe_tac "thin" *) clear to_revert))
+ (* observe (str "rec id := " ++ Ppconstr.pr_id hyp); *)
+ let hyps = [hyp] in
+ let env = Global.env () in
+ let sigma = Proofview.Goal.sigma g in
+ let hyp_typ = Tacmach.New.pf_get_hyp_typ hyp g in
+ let to_revert, _ =
+ let open Context.Named.Declaration in
+ Environ.fold_named_context_reverse
+ (fun (clear, keep) decl ->
+ let decl = map_named_decl EConstr.of_constr decl in
+ let hyp = get_id decl in
+ if
+ Id.List.mem hyp hyps
+ || List.exists (Termops.occur_var_in_decl env sigma hyp) keep
+ || Termops.occur_var env sigma hyp hyp_typ
+ || Termops.is_section_variable hyp
+ (* should be dangerous *)
+ then (clear, decl :: keep)
+ else (hyp :: clear, keep))
+ ~init:([], []) (Proofview.Goal.env g)
+ in
+ (* observe (str "to_revert := " ++ prlist_with_sep spc Ppconstr.pr_id to_revert); *)
+ Tacticals.New.tclTHEN
+ ((* observe_tac "h_generalize" *)
+ generalize (List.map mkVar to_revert))
+ ((* observe_tac "thin" *) clear to_revert))
let id_of_decl = RelDecl.get_name %> Nameops.Name.get_id
let var_of_decl = id_of_decl %> mkVar
@@ -795,7 +813,8 @@ let var_of_decl = id_of_decl %> mkVar
let revert idl =
Tacticals.New.tclTHEN (generalize (List.map mkVar idl)) (clear idl)
-let generate_equation_lemma evd fnames f fun_num nb_params nb_args rec_args_num =
+let generate_equation_lemma evd fnames f fun_num nb_params nb_args rec_args_num
+ =
let open Tacticals.New in
(* observe (str "nb_args := " ++ str (string_of_int nb_args)); *)
(* observe (str "nb_params := " ++ str (string_of_int nb_params)); *)
@@ -845,14 +864,13 @@ let generate_equation_lemma evd fnames f fun_num nb_params nb_args rec_args_num
let prove_replacement =
tclTHENLIST
[ tclDO (nb_params + rec_args_num + 1) intro
- ; observe_tac "" (onNthHypId 1 (fun rec_id ->
- tclTHENLIST
- [ observe_tac "generalize_non_dep in generate_equation_lemma"
- (generalize_non_dep rec_id)
- ; observe_tac "h_case"
- (simplest_case (mkVar rec_id))
- ; intros_reflexivity ]))
- ]
+ ; observe_tac ""
+ (onNthHypId 1 (fun rec_id ->
+ tclTHENLIST
+ [ observe_tac "generalize_non_dep in generate_equation_lemma"
+ (generalize_non_dep rec_id)
+ ; observe_tac "h_case" (simplest_case (mkVar rec_id))
+ ; intros_reflexivity ])) ]
in
(* Pp.msgnl (str "lemma type (2) " ++ Printer.pr_lconstr_env (Global.env ()) evd lemma_type); *)
@@ -873,375 +891,396 @@ let generate_equation_lemma evd fnames f fun_num nb_params nb_args rec_args_num
let do_replace (evd : Evd.evar_map ref) params rec_arg_num rev_args_id f fun_num
all_funs =
Proofview.Goal.enter (fun g ->
- let equation_lemma =
- try
- let finfos =
- match find_Function_infos (fst (destConst !evd f)) (*FIXME*) with
- | None -> raise Not_found
- | Some finfos -> finfos
- in
- mkConst (Option.get finfos.equation_lemma)
- with (Not_found | Option.IsNone) as e ->
- let f_id = Label.to_id (Constant.label (fst (destConst !evd f))) in
- (*i The next call to mk_equation_id is valid since we will construct the lemma
- Ensures by: obvious
- i*)
- let equation_lemma_id = mk_equation_id f_id in
- evd :=
- generate_equation_lemma !evd all_funs f fun_num (List.length params)
- (List.length rev_args_id) rec_arg_num;
- let _ =
- match e with
- | Option.IsNone ->
+ let equation_lemma =
+ try
let finfos =
- match find_Function_infos (fst (destConst !evd f)) with
+ match find_Function_infos (fst (destConst !evd f)) (*FIXME*) with
| None -> raise Not_found
| Some finfos -> finfos
in
- update_Function
- { finfos with
- equation_lemma =
- Some
- ( match Nametab.locate (qualid_of_ident equation_lemma_id) with
- | GlobRef.ConstRef c -> c
- | _ -> CErrors.anomaly (Pp.str "Not a constant.") ) }
- | _ -> ()
+ mkConst (Option.get finfos.equation_lemma)
+ with (Not_found | Option.IsNone) as e ->
+ let f_id = Label.to_id (Constant.label (fst (destConst !evd f))) in
+ (*i The next call to mk_equation_id is valid since we will construct the lemma
+ Ensures by: obvious
+ i*)
+ let equation_lemma_id = mk_equation_id f_id in
+ evd :=
+ generate_equation_lemma !evd all_funs f fun_num (List.length params)
+ (List.length rev_args_id) rec_arg_num;
+ let _ =
+ match e with
+ | Option.IsNone ->
+ let finfos =
+ match find_Function_infos (fst (destConst !evd f)) with
+ | None -> raise Not_found
+ | Some finfos -> finfos
+ in
+ update_Function
+ { finfos with
+ equation_lemma =
+ Some
+ ( match
+ Nametab.locate (qualid_of_ident equation_lemma_id)
+ with
+ | GlobRef.ConstRef c -> c
+ | _ -> CErrors.anomaly (Pp.str "Not a constant.") ) }
+ | _ -> ()
+ in
+ (* let res = Constrintern.construct_reference (pf_hyps g) equation_lemma_id in *)
+ let evd', res =
+ Evd.fresh_global (Global.env ()) !evd
+ (Constrintern.locate_reference
+ (qualid_of_ident equation_lemma_id))
+ in
+ evd := evd';
+ let sigma, _ =
+ Typing.type_of ~refresh:true (Global.env ()) !evd res
+ in
+ evd := sigma;
+ res
in
- (* let res = Constrintern.construct_reference (pf_hyps g) equation_lemma_id in *)
- let evd', res =
- Evd.fresh_global (Global.env ()) !evd
- (Constrintern.locate_reference (qualid_of_ident equation_lemma_id))
+ let nb_intro_to_do =
+ nb_prod (Proofview.Goal.sigma g) (Proofview.Goal.concl g)
in
- evd := evd';
- let sigma, _ = Typing.type_of ~refresh:true (Global.env ()) !evd res in
- evd := sigma;
- res
- in
- let nb_intro_to_do = nb_prod (Proofview.Goal.sigma g) (Proofview.Goal.concl g) in
- let open Tacticals.New in
- tclTHEN
- (tclDO nb_intro_to_do intro)
- (Proofview.Goal.enter (fun g' ->
- let just_introduced = Tacticals.New.nLastDecls g' nb_intro_to_do in
- let open Context.Named.Declaration in
- let just_introduced_id = List.map get_id just_introduced in
+ let open Tacticals.New in
tclTHEN
- (* Hack to synchronize the goal with the global env *)
- (Proofview.V82.tactic (Proofview.V82.of_tactic (Equality.rewriteLR equation_lemma)))
- (revert just_introduced_id))))
+ (tclDO nb_intro_to_do intro)
+ (Proofview.Goal.enter (fun g' ->
+ let just_introduced = Tacticals.New.nLastDecls g' nb_intro_to_do in
+ let open Context.Named.Declaration in
+ let just_introduced_id = List.map get_id just_introduced in
+ tclTHEN
+ (* Hack to synchronize the goal with the global env *)
+ (Proofview.V82.tactic
+ (Proofview.V82.of_tactic (Equality.rewriteLR equation_lemma)))
+ (revert just_introduced_id))))
let prove_princ_for_struct (evd : Evd.evar_map ref) interactive_proof fun_num
fnames all_funs _nparams : unit Proofview.tactic =
let open Tacticals.New in
Proofview.Goal.enter (fun g ->
- let princ_type = Proofview.Goal.concl g in
- let env = Proofview.Goal.env g in
- let sigma = Proofview.Goal.sigma g in
- (* Pp.msgnl (str "princ_type " ++ Printer.pr_lconstr princ_type); *)
- (* Pp.msgnl (str "all_funs "); *)
- (* Array.iter (fun c -> Pp.msgnl (Printer.pr_lconstr c)) all_funs; *)
- let princ_info = compute_elim_sig sigma princ_type in
- let fresh_id =
- let avoid = ref (Tacmach.New.pf_ids_of_hyps g) in
- fun na ->
- let new_id =
- match na with
- | Name id -> fresh_id !avoid (Id.to_string id)
- | Anonymous -> fresh_id !avoid "H"
+ let princ_type = Proofview.Goal.concl g in
+ let env = Proofview.Goal.env g in
+ let sigma = Proofview.Goal.sigma g in
+ (* Pp.msgnl (str "princ_type " ++ Printer.pr_lconstr princ_type); *)
+ (* Pp.msgnl (str "all_funs "); *)
+ (* Array.iter (fun c -> Pp.msgnl (Printer.pr_lconstr c)) all_funs; *)
+ let princ_info = compute_elim_sig sigma princ_type in
+ let fresh_id =
+ let avoid = ref (Tacmach.New.pf_ids_of_hyps g) in
+ fun na ->
+ let new_id =
+ match na with
+ | Name id -> fresh_id !avoid (Id.to_string id)
+ | Anonymous -> fresh_id !avoid "H"
+ in
+ avoid := new_id :: !avoid;
+ Name new_id
in
- avoid := new_id :: !avoid;
- Name new_id
- in
- let fresh_decl = RelDecl.map_name fresh_id in
- let princ_info : elim_scheme =
- { princ_info with
- params = List.map fresh_decl princ_info.params
- ; predicates = List.map fresh_decl princ_info.predicates
- ; branches = List.map fresh_decl princ_info.branches
- ; args = List.map fresh_decl princ_info.args }
- in
- let get_body const =
- match Global.body_of_constant Library.indirect_accessor const with
- | Some (body, _, _) ->
- let env = Global.env () in
- let sigma = Evd.from_env env in
- Tacred.cbv_norm_flags
- (CClosure.RedFlags.mkflags [CClosure.RedFlags.fZETA])
- env sigma (EConstr.of_constr body)
- | None -> user_err Pp.(str "Cannot define a principle over an axiom ")
- in
- let fbody = get_body fnames.(fun_num) in
- let f_ctxt, f_body = decompose_lam sigma fbody in
- let f_ctxt_length = List.length f_ctxt in
- let diff_params = princ_info.nparams - f_ctxt_length in
- let full_params, princ_params, fbody_with_full_params =
- if diff_params > 0 then
- let princ_params, full_params = list_chop diff_params princ_info.params in
- ( full_params
- , (* real params *)
- princ_params
- , (* the params of the principle which are not params of the function *)
- substl (* function instantiated with real params *)
- (List.map var_of_decl full_params)
- f_body )
- else
- let f_ctxt_other, f_ctxt_params = list_chop (-diff_params) f_ctxt in
- let f_body = compose_lam f_ctxt_other f_body in
- ( princ_info.params
- , (* real params *)
- []
- , (* all params are full params *)
- substl (* function instantiated with real params *)
- (List.map var_of_decl princ_info.params)
- f_body )
- in
- observe
- ( str "full_params := "
- ++ prlist_with_sep spc
- (RelDecl.get_name %> Nameops.Name.get_id %> Ppconstr.pr_id)
- full_params );
- observe
- ( str "princ_params := "
- ++ prlist_with_sep spc
- (RelDecl.get_name %> Nameops.Name.get_id %> Ppconstr.pr_id)
- princ_params );
- observe
- ( str "fbody_with_full_params := "
- ++ pr_leconstr_env (Global.env ()) !evd fbody_with_full_params );
- let all_funs_with_full_params =
- Array.map
- (fun f -> applist (f, List.rev_map var_of_decl full_params))
- all_funs
- in
- let fix_offset = List.length princ_params in
- let ptes_to_fix, infos =
- match EConstr.kind sigma fbody_with_full_params with
- | Fix ((idxs, i), (names, typess, bodies)) ->
- let bodies_with_all_params =
- Array.map
- (fun body ->
- Reductionops.nf_betaiota env sigma
- (applist
- ( substl
- (List.rev (Array.to_list all_funs_with_full_params))
- body
- , List.rev_map var_of_decl princ_params )))
- bodies
+ let fresh_decl = RelDecl.map_name fresh_id in
+ let princ_info : elim_scheme =
+ { princ_info with
+ params = List.map fresh_decl princ_info.params
+ ; predicates = List.map fresh_decl princ_info.predicates
+ ; branches = List.map fresh_decl princ_info.branches
+ ; args = List.map fresh_decl princ_info.args }
in
- let info_array =
- Array.mapi
- (fun i types ->
- let types =
- prod_applist sigma types
- (List.rev_map var_of_decl princ_params)
- in
- { idx = idxs.(i) - fix_offset
- ; name = Nameops.Name.get_id (fresh_id names.(i).binder_name)
- ; types
- ; offset = fix_offset
- ; nb_realargs =
- List.length (fst (decompose_lam sigma bodies.(i)))
- - fix_offset
- ; body_with_param = bodies_with_all_params.(i)
- ; num_in_block = i })
- typess
+ let get_body const =
+ match Global.body_of_constant Library.indirect_accessor const with
+ | Some (body, _, _) ->
+ let env = Global.env () in
+ let sigma = Evd.from_env env in
+ Tacred.cbv_norm_flags
+ (CClosure.RedFlags.mkflags [CClosure.RedFlags.fZETA])
+ env sigma (EConstr.of_constr body)
+ | None -> user_err Pp.(str "Cannot define a principle over an axiom ")
in
- let pte_to_fix, rev_info =
- List.fold_left_i
- (fun i (acc_map, acc_info) decl ->
- let pte = RelDecl.get_name decl in
- let infos = info_array.(i) in
- let type_args, _ = decompose_prod sigma infos.types in
- let nargs = List.length type_args in
- let f =
- applist
- (mkConst fnames.(i), List.rev_map var_of_decl princ_info.params)
- in
- let first_args = Array.init nargs (fun i -> mkRel (nargs - i)) in
- let app_f = mkApp (f, first_args) in
- let pte_args = Array.to_list first_args @ [app_f] in
- let app_pte = applist (mkVar (Nameops.Name.get_id pte), pte_args) in
- let body_with_param, num =
- let body = get_body fnames.(i) in
- let body_with_full_params =
+ let fbody = get_body fnames.(fun_num) in
+ let f_ctxt, f_body = decompose_lam sigma fbody in
+ let f_ctxt_length = List.length f_ctxt in
+ let diff_params = princ_info.nparams - f_ctxt_length in
+ let full_params, princ_params, fbody_with_full_params =
+ if diff_params > 0 then
+ let princ_params, full_params =
+ list_chop diff_params princ_info.params
+ in
+ ( full_params
+ , (* real params *)
+ princ_params
+ , (* the params of the principle which are not params of the function *)
+ substl (* function instantiated with real params *)
+ (List.map var_of_decl full_params)
+ f_body )
+ else
+ let f_ctxt_other, f_ctxt_params = list_chop (-diff_params) f_ctxt in
+ let f_body = compose_lam f_ctxt_other f_body in
+ ( princ_info.params
+ , (* real params *)
+ []
+ , (* all params are full params *)
+ substl (* function instantiated with real params *)
+ (List.map var_of_decl princ_info.params)
+ f_body )
+ in
+ observe
+ ( str "full_params := "
+ ++ prlist_with_sep spc
+ (RelDecl.get_name %> Nameops.Name.get_id %> Ppconstr.pr_id)
+ full_params );
+ observe
+ ( str "princ_params := "
+ ++ prlist_with_sep spc
+ (RelDecl.get_name %> Nameops.Name.get_id %> Ppconstr.pr_id)
+ princ_params );
+ observe
+ ( str "fbody_with_full_params := "
+ ++ pr_leconstr_env (Global.env ()) !evd fbody_with_full_params );
+ let all_funs_with_full_params =
+ Array.map
+ (fun f -> applist (f, List.rev_map var_of_decl full_params))
+ all_funs
+ in
+ let fix_offset = List.length princ_params in
+ let ptes_to_fix, infos =
+ match EConstr.kind sigma fbody_with_full_params with
+ | Fix ((idxs, i), (names, typess, bodies)) ->
+ let bodies_with_all_params =
+ Array.map
+ (fun body ->
Reductionops.nf_betaiota env sigma
- (applist (body, List.rev_map var_of_decl full_params))
- in
- match EConstr.kind sigma body_with_full_params with
- | Fix ((_, num), (_, _, bs)) ->
- ( Reductionops.nf_betaiota env sigma
- (applist
- ( substl
- (List.rev (Array.to_list all_funs_with_full_params))
- bs.(num)
- , List.rev_map var_of_decl princ_params ))
- , num )
- | _ -> user_err Pp.(str "Not a mutual block")
- in
- let info =
- { infos with
- types = compose_prod type_args app_pte
- ; body_with_param
- ; num_in_block = num }
- in
- (* observe (str "binding " ++ Ppconstr.pr_id (Nameops.Name.get_id pte) ++ *)
- (* str " to " ++ Ppconstr.pr_id info.name); *)
- (Id.Map.add (Nameops.Name.get_id pte) info acc_map, info :: acc_info))
- 0 (Id.Map.empty, [])
- (List.rev princ_info.predicates)
+ (applist
+ ( substl
+ (List.rev (Array.to_list all_funs_with_full_params))
+ body
+ , List.rev_map var_of_decl princ_params )))
+ bodies
+ in
+ let info_array =
+ Array.mapi
+ (fun i types ->
+ let types =
+ prod_applist sigma types
+ (List.rev_map var_of_decl princ_params)
+ in
+ { idx = idxs.(i) - fix_offset
+ ; name = Nameops.Name.get_id (fresh_id names.(i).binder_name)
+ ; types
+ ; offset = fix_offset
+ ; nb_realargs =
+ List.length (fst (decompose_lam sigma bodies.(i)))
+ - fix_offset
+ ; body_with_param = bodies_with_all_params.(i)
+ ; num_in_block = i })
+ typess
+ in
+ let pte_to_fix, rev_info =
+ List.fold_left_i
+ (fun i (acc_map, acc_info) decl ->
+ let pte = RelDecl.get_name decl in
+ let infos = info_array.(i) in
+ let type_args, _ = decompose_prod sigma infos.types in
+ let nargs = List.length type_args in
+ let f =
+ applist
+ ( mkConst fnames.(i)
+ , List.rev_map var_of_decl princ_info.params )
+ in
+ let first_args =
+ Array.init nargs (fun i -> mkRel (nargs - i))
+ in
+ let app_f = mkApp (f, first_args) in
+ let pte_args = Array.to_list first_args @ [app_f] in
+ let app_pte =
+ applist (mkVar (Nameops.Name.get_id pte), pte_args)
+ in
+ let body_with_param, num =
+ let body = get_body fnames.(i) in
+ let body_with_full_params =
+ Reductionops.nf_betaiota env sigma
+ (applist (body, List.rev_map var_of_decl full_params))
+ in
+ match EConstr.kind sigma body_with_full_params with
+ | Fix ((_, num), (_, _, bs)) ->
+ ( Reductionops.nf_betaiota env sigma
+ (applist
+ ( substl
+ (List.rev
+ (Array.to_list all_funs_with_full_params))
+ bs.(num)
+ , List.rev_map var_of_decl princ_params ))
+ , num )
+ | _ -> user_err Pp.(str "Not a mutual block")
+ in
+ let info =
+ { infos with
+ types = compose_prod type_args app_pte
+ ; body_with_param
+ ; num_in_block = num }
+ in
+ (* observe (str "binding " ++ Ppconstr.pr_id (Nameops.Name.get_id pte) ++ *)
+ (* str " to " ++ Ppconstr.pr_id info.name); *)
+ ( Id.Map.add (Nameops.Name.get_id pte) info acc_map
+ , info :: acc_info ))
+ 0 (Id.Map.empty, [])
+ (List.rev princ_info.predicates)
+ in
+ (pte_to_fix, List.rev rev_info)
+ | _ -> (Id.Map.empty, [])
in
- (pte_to_fix, List.rev rev_info)
- | _ -> (Id.Map.empty, [])
- in
- let mk_fixes : unit Proofview.tactic =
- let pre_info, infos = list_chop fun_num infos in
- match (pre_info, infos) with
- | _, [] -> Proofview.tclUNIT ()
- | _, this_fix_info :: others_infos ->
- let other_fix_infos =
- List.map
- (fun fi -> (fi.name, fi.idx + 1, fi.types))
- (pre_info @ others_infos)
+ let mk_fixes : unit Proofview.tactic =
+ let pre_info, infos = list_chop fun_num infos in
+ match (pre_info, infos) with
+ | _, [] -> Proofview.tclUNIT ()
+ | _, this_fix_info :: others_infos ->
+ let other_fix_infos =
+ List.map
+ (fun fi -> (fi.name, fi.idx + 1, fi.types))
+ (pre_info @ others_infos)
+ in
+ if List.is_empty other_fix_infos then
+ if this_fix_info.idx + 1 = 0 then Proofview.tclUNIT ()
+ (* Someone tries to defined a principle on a fully parametric definition declared as a fixpoint (strange but ....) *)
+ else
+ Indfun_common.New.observe_tac ~header:(str "observation")
+ (fun _ _ -> str "h_fix " ++ int (this_fix_info.idx + 1))
+ (fix this_fix_info.name (this_fix_info.idx + 1))
+ else
+ Tactics.mutual_fix this_fix_info.name (this_fix_info.idx + 1)
+ other_fix_infos 0
in
- if List.is_empty other_fix_infos then
- if this_fix_info.idx + 1 = 0 then Proofview.tclUNIT ()
- (* Someone tries to defined a principle on a fully parametric definition declared as a fixpoint (strange but ....) *)
- else
- Indfun_common.New.observe_tac ~header:(str "observation")
- (fun _ _ -> str "h_fix " ++ int (this_fix_info.idx + 1))
- (fix this_fix_info.name (this_fix_info.idx + 1))
- else
- (Tactics.mutual_fix this_fix_info.name (this_fix_info.idx + 1)
- other_fix_infos 0)
- in
- let first_tac : unit Proofview.tactic =
- (* every operations until fix creations *)
- (* names are already refreshed *)
- tclTHENLIST
- [ observe_tac "introducing params"
- (intros_mustbe_force (List.rev_map id_of_decl princ_info.params))
- ; observe_tac "introducing predicates"
- (intros_mustbe_force
- (List.rev_map id_of_decl princ_info.predicates))
- ; observe_tac "introducing branches"
- (intros_mustbe_force (List.rev_map id_of_decl princ_info.branches))
- ; observe_tac "building fixes" mk_fixes ]
- in
- let intros_after_fixes : unit Proofview.tactic =
- Proofview.Goal.enter (fun gl ->
- let sigma = Proofview.Goal.sigma gl in
- let ccl = Proofview.Goal.concl gl in
- let ctxt, pte_app = decompose_prod_assum sigma ccl in
- let pte, pte_args = decompose_app sigma pte_app in
- try
- let pte =
- try destVar sigma pte
- with DestKO -> anomaly (Pp.str "Property is not a variable.")
+ let first_tac : unit Proofview.tactic =
+ (* every operations until fix creations *)
+ (* names are already refreshed *)
+ tclTHENLIST
+ [ observe_tac "introducing params"
+ (intros_mustbe_force (List.rev_map id_of_decl princ_info.params))
+ ; observe_tac "introducing predicates"
+ (intros_mustbe_force
+ (List.rev_map id_of_decl princ_info.predicates))
+ ; observe_tac "introducing branches"
+ (intros_mustbe_force
+ (List.rev_map id_of_decl princ_info.branches))
+ ; observe_tac "building fixes" mk_fixes ]
in
- let fix_info = Id.Map.find pte ptes_to_fix in
- let nb_args = fix_info.nb_realargs in
- tclTHENLIST
- [ (* observe_tac ("introducing args") *)
- tclDO nb_args intro
- ; Proofview.Goal.enter (fun g ->
- (* replacement of the function by its body *)
- let args = Tacticals.New.nLastDecls g nb_args in
- let fix_body = fix_info.body_with_param in
- (* observe (str "fix_body := "++ pr_lconstr_env (pf_env gl) fix_body); *)
- let open Context.Named.Declaration in
- let args_id = List.map get_id args in
- let dyn_infos =
- { nb_rec_hyps = -100
- ; rec_hyps = []
- ; info =
- Reductionops.nf_betaiota (Proofview.Goal.env g) (Proofview.Goal.sigma g)
- (applist (fix_body, List.rev_map mkVar args_id))
- ; eq_hyps = [] }
- in
- tclTHENLIST
- [ observe_tac "do_replace"
- (do_replace evd full_params
- (fix_info.idx + List.length princ_params)
- ( args_id
- @ List.map
- (RelDecl.get_name %> Nameops.Name.get_id)
- princ_params )
- all_funs.(fix_info.num_in_block)
- fix_info.num_in_block all_funs)
- ; let do_prove =
- build_proof interactive_proof (Array.to_list fnames)
- (Id.Map.map prove_rec_hyp ptes_to_fix)
- in
- let prove_tac branches =
- let dyn_infos =
- { dyn_infos with
- rec_hyps = branches
- ; nb_rec_hyps = List.length branches }
- in
- observe_tac "cleaning"
- (clean_goal_with_heq
- (Id.Map.map prove_rec_hyp ptes_to_fix)
- do_prove dyn_infos)
- in
- (* observe (str "branches := " ++ *)
- (* prlist_with_sep spc (fun decl -> Ppconstr.pr_id (id_of_decl decl)) princ_info.branches ++ fnl () ++ *)
- (* str "args := " ++ prlist_with_sep spc Ppconstr.pr_id args_id *)
+ let intros_after_fixes : unit Proofview.tactic =
+ Proofview.Goal.enter (fun gl ->
+ let sigma = Proofview.Goal.sigma gl in
+ let ccl = Proofview.Goal.concl gl in
+ let ctxt, pte_app = decompose_prod_assum sigma ccl in
+ let pte, pte_args = decompose_app sigma pte_app in
+ try
+ let pte =
+ try destVar sigma pte
+ with DestKO -> anomaly (Pp.str "Property is not a variable.")
+ in
+ let fix_info = Id.Map.find pte ptes_to_fix in
+ let nb_args = fix_info.nb_realargs in
+ tclTHENLIST
+ [ (* observe_tac ("introducing args") *)
+ tclDO nb_args intro
+ ; Proofview.Goal.enter (fun g ->
+ (* replacement of the function by its body *)
+ let args = Tacticals.New.nLastDecls g nb_args in
+ let fix_body = fix_info.body_with_param in
+ (* observe (str "fix_body := "++ pr_lconstr_env (pf_env gl) fix_body); *)
+ let open Context.Named.Declaration in
+ let args_id = List.map get_id args in
+ let dyn_infos =
+ { nb_rec_hyps = -100
+ ; rec_hyps = []
+ ; info =
+ Reductionops.nf_betaiota (Proofview.Goal.env g)
+ (Proofview.Goal.sigma g)
+ (applist (fix_body, List.rev_map mkVar args_id))
+ ; eq_hyps = [] }
+ in
+ tclTHENLIST
+ [ observe_tac "do_replace"
+ (do_replace evd full_params
+ (fix_info.idx + List.length princ_params)
+ ( args_id
+ @ List.map
+ (RelDecl.get_name %> Nameops.Name.get_id)
+ princ_params )
+ all_funs.(fix_info.num_in_block)
+ fix_info.num_in_block all_funs)
+ ; (let do_prove =
+ build_proof interactive_proof
+ (Array.to_list fnames)
+ (Id.Map.map prove_rec_hyp ptes_to_fix)
+ in
+ let prove_tac branches =
+ let dyn_infos =
+ { dyn_infos with
+ rec_hyps = branches
+ ; nb_rec_hyps = List.length branches }
+ in
+ observe_tac "cleaning"
+ (clean_goal_with_heq
+ (Id.Map.map prove_rec_hyp ptes_to_fix)
+ do_prove dyn_infos)
+ in
+ (* observe (str "branches := " ++ *)
+ (* prlist_with_sep spc (fun decl -> Ppconstr.pr_id (id_of_decl decl)) princ_info.branches ++ fnl () ++ *)
+ (* str "args := " ++ prlist_with_sep spc Ppconstr.pr_id args_id *)
- (* ); *)
- (* observe_tac "instancing" *)
- instantiate_hyps_with_args prove_tac
- (List.rev_map id_of_decl princ_info.branches)
- (List.rev args_id) ]
- ) ]
- with Not_found ->
- let nb_args = min princ_info.nargs (List.length ctxt) in
- tclTHENLIST
- [ tclDO nb_args intro
- ; Proofview.Goal.enter (fun g ->
- let env = Proofview.Goal.env g in
- let sigma = Proofview.Goal.sigma g in
- (* replacement of the function by its body *)
- let args = Tacticals.New.nLastDecls g nb_args in
- let open Context.Named.Declaration in
- let args_id = List.map get_id args in
- let dyn_infos =
- { nb_rec_hyps = -100
- ; rec_hyps = []
- ; info =
- Reductionops.nf_betaiota env sigma
- (applist
- ( fbody_with_full_params
- , List.rev_map var_of_decl princ_params
- @ List.rev_map mkVar args_id ))
- ; eq_hyps = [] }
- in
- let fname =
- destConst sigma
- (fst (decompose_app sigma (List.hd (List.rev pte_args))))
- in
- tclTHENLIST
- [ unfold_in_concl
- [(Locus.AllOccurrences, Names.EvalConstRef (fst fname))]
- ; (let do_prove =
- build_proof interactive_proof (Array.to_list fnames)
- (Id.Map.map prove_rec_hyp ptes_to_fix)
- in
- let prove_tac branches =
- let dyn_infos =
- { dyn_infos with
- rec_hyps = branches
- ; nb_rec_hyps = List.length branches }
- in
- clean_goal_with_heq
- (Id.Map.map prove_rec_hyp ptes_to_fix)
- do_prove dyn_infos
- in
- instantiate_hyps_with_args prove_tac
- (List.rev_map id_of_decl princ_info.branches)
- (List.rev args_id)) ]
- ) ])
- in
- tclTHEN first_tac intros_after_fixes)
+ (* ); *)
+ (* observe_tac "instancing" *)
+ instantiate_hyps_with_args prove_tac
+ (List.rev_map id_of_decl princ_info.branches)
+ (List.rev args_id)) ]) ]
+ with Not_found ->
+ let nb_args = min princ_info.nargs (List.length ctxt) in
+ tclTHENLIST
+ [ tclDO nb_args intro
+ ; Proofview.Goal.enter (fun g ->
+ let env = Proofview.Goal.env g in
+ let sigma = Proofview.Goal.sigma g in
+ (* replacement of the function by its body *)
+ let args = Tacticals.New.nLastDecls g nb_args in
+ let open Context.Named.Declaration in
+ let args_id = List.map get_id args in
+ let dyn_infos =
+ { nb_rec_hyps = -100
+ ; rec_hyps = []
+ ; info =
+ Reductionops.nf_betaiota env sigma
+ (applist
+ ( fbody_with_full_params
+ , List.rev_map var_of_decl princ_params
+ @ List.rev_map mkVar args_id ))
+ ; eq_hyps = [] }
+ in
+ let fname =
+ destConst sigma
+ (fst
+ (decompose_app sigma (List.hd (List.rev pte_args))))
+ in
+ tclTHENLIST
+ [ unfold_in_concl
+ [ ( Locus.AllOccurrences
+ , Names.EvalConstRef (fst fname) ) ]
+ ; (let do_prove =
+ build_proof interactive_proof
+ (Array.to_list fnames)
+ (Id.Map.map prove_rec_hyp ptes_to_fix)
+ in
+ let prove_tac branches =
+ let dyn_infos =
+ { dyn_infos with
+ rec_hyps = branches
+ ; nb_rec_hyps = List.length branches }
+ in
+ clean_goal_with_heq
+ (Id.Map.map prove_rec_hyp ptes_to_fix)
+ do_prove dyn_infos
+ in
+ instantiate_hyps_with_args prove_tac
+ (List.rev_map id_of_decl princ_info.branches)
+ (List.rev args_id)) ]) ])
+ in
+ tclTHEN first_tac intros_after_fixes)
(* Proof of principles of general functions *)
(* let hrec_id = Recdef.hrec_id *)
@@ -1257,39 +1296,43 @@ let prove_with_tcc tcc_lemma_constr eqs : unit Proofview.tactic =
match !tcc_lemma_constr with
| Undefined -> anomaly (Pp.str "No tcc proof !!")
| Value lemma ->
- (* let hid = next_ident_away_in_goal h_id (pf_ids_of_hyps gls) in *)
- (* let ids = hid::pf_ids_of_hyps gls in *)
- tclTHENLIST
- [ (* generalize [lemma]; *)
- (* h_intro hid; *)
- (* Elim.h_decompose_and (mkVar hid); *)
- tclTRY (list_rewrite true eqs)
- ; (* (fun g -> *)
- (* let ids' = pf_ids_of_hyps g in *)
- (* let ids = List.filter (fun id -> not (List.mem id ids)) ids' in *)
- (* rewrite *)
- (* ) *)
- Eauto.gen_eauto (false, 5) [] (Some []) ]
+ (* let hid = next_ident_away_in_goal h_id (pf_ids_of_hyps gls) in *)
+ (* let ids = hid::pf_ids_of_hyps gls in *)
+ tclTHENLIST
+ [ (* generalize [lemma]; *)
+ (* h_intro hid; *)
+ (* Elim.h_decompose_and (mkVar hid); *)
+ tclTRY (list_rewrite true eqs)
+ ; (* (fun g -> *)
+ (* let ids' = pf_ids_of_hyps g in *)
+ (* let ids = List.filter (fun id -> not (List.mem id ids)) ids' in *)
+ (* rewrite *)
+ (* ) *)
+ Eauto.gen_eauto (false, 5) [] (Some []) ]
| Not_needed -> Proofview.tclUNIT ()
let backtrack_eqs_until_hrec hrec eqs : unit Proofview.tactic =
let open Tacticals.New in
Proofview.Goal.enter (fun gls ->
- let sigma = Proofview.Goal.sigma gls in
- let eqs = List.map mkVar eqs in
- let rewrite = tclFIRST (List.map Equality.rewriteRL eqs) in
- let _, hrec_concl = decompose_prod sigma (Tacmach.New.pf_get_hyp_typ hrec gls) in
- let f_app = Array.last (snd (destApp sigma hrec_concl)) in
- let f = fst (destApp sigma f_app) in
- let rec backtrack () : unit Proofview.tactic =
- Proofview.Goal.enter (fun g ->
- let sigma = Proofview.Goal.sigma gls in
- let f_app = Array.last (snd (destApp sigma (Proofview.Goal.concl g))) in
- match EConstr.kind sigma f_app with
- | App (f', _) when eq_constr sigma f' f -> Proofview.tclUNIT ()
- | _ -> tclTHEN rewrite (backtrack ()))
- in
- backtrack ())
+ let sigma = Proofview.Goal.sigma gls in
+ let eqs = List.map mkVar eqs in
+ let rewrite = tclFIRST (List.map Equality.rewriteRL eqs) in
+ let _, hrec_concl =
+ decompose_prod sigma (Tacmach.New.pf_get_hyp_typ hrec gls)
+ in
+ let f_app = Array.last (snd (destApp sigma hrec_concl)) in
+ let f = fst (destApp sigma f_app) in
+ let rec backtrack () : unit Proofview.tactic =
+ Proofview.Goal.enter (fun g ->
+ let sigma = Proofview.Goal.sigma gls in
+ let f_app =
+ Array.last (snd (destApp sigma (Proofview.Goal.concl g)))
+ in
+ match EConstr.kind sigma f_app with
+ | App (f', _) when eq_constr sigma f' f -> Proofview.tclUNIT ()
+ | _ -> tclTHEN rewrite (backtrack ()))
+ in
+ backtrack ())
let rec rewrite_eqs_in_eqs eqs =
let open Tacticals.New in
@@ -1303,39 +1346,40 @@ let rec rewrite_eqs_in_eqs eqs =
(Format.sprintf "rewrite %s in %s " (Id.to_string eq)
(Id.to_string id))
(tclTRY
- (Equality.general_rewrite_in true Locus.AllOccurrences true
- (* dep proofs also: *) true id (mkVar eq) false)))
+ (Equality.general_rewrite_in true Locus.AllOccurrences true
+ (* dep proofs also: *) true id (mkVar eq) false)))
eqs)
(rewrite_eqs_in_eqs eqs)
-let new_prove_with_tcc is_mes acc_inv hrec tcc_hyps eqs : unit Proofview.tactic =
+let new_prove_with_tcc is_mes acc_inv hrec tcc_hyps eqs : unit Proofview.tactic
+ =
let open Tacticals.New in
tclTHENLIST
- [ backtrack_eqs_until_hrec hrec eqs
- ; (* observe_tac ("new_prove_with_tcc ( applying "^(Id.to_string hrec)^" )" ) *)
- tclTHENS (* We must have exactly ONE subgoal !*)
- (apply (mkVar hrec))
- [ tclTHENLIST
- [ keep (tcc_hyps @ eqs)
- ; apply (Lazy.force acc_inv)
- ; if is_mes then
- (unfold_in_concl
- [ ( Locus.AllOccurrences
- , evaluable_of_global_reference
- (delayed_force ltof_ref) ) ])
- else Proofview.tclUNIT ()
- ; observe_tac "rew_and_finish"
- (tclTHENLIST
- [ tclTRY
- (list_rewrite false
- (List.map (fun v -> (mkVar v, true)) eqs))
- ; observe_tac "rewrite_eqs_in_eqs" (rewrite_eqs_in_eqs eqs)
- ; observe_tac "finishing using"
- (tclCOMPLETE
- (Eauto.eauto_with_bases (true, 5)
- [(fun _ sigma -> (sigma, Lazy.force refl_equal))]
- [ Hints.Hint_db.empty TransparentState.empty
- false ] )) ]) ] ] ]
+ [ backtrack_eqs_until_hrec hrec eqs
+ ; (* observe_tac ("new_prove_with_tcc ( applying "^(Id.to_string hrec)^" )" ) *)
+ tclTHENS (* We must have exactly ONE subgoal !*)
+ (apply (mkVar hrec))
+ [ tclTHENLIST
+ [ keep (tcc_hyps @ eqs)
+ ; apply (Lazy.force acc_inv)
+ ; ( if is_mes then
+ unfold_in_concl
+ [ ( Locus.AllOccurrences
+ , evaluable_of_global_reference (delayed_force ltof_ref) )
+ ]
+ else Proofview.tclUNIT () )
+ ; observe_tac "rew_and_finish"
+ (tclTHENLIST
+ [ tclTRY
+ (list_rewrite false
+ (List.map (fun v -> (mkVar v, true)) eqs))
+ ; observe_tac "rewrite_eqs_in_eqs" (rewrite_eqs_in_eqs eqs)
+ ; observe_tac "finishing using"
+ (tclCOMPLETE
+ (Eauto.eauto_with_bases (true, 5)
+ [(fun _ sigma -> (sigma, Lazy.force refl_equal))]
+ [Hints.Hint_db.empty TransparentState.empty false]))
+ ]) ] ] ]
let is_valid_hypothesis sigma predicates_name =
let predicates_name =
@@ -1360,193 +1404,202 @@ let is_valid_hypothesis sigma predicates_name =
let prove_principle_for_gen (f_ref, functional_ref, eq_ref) tcc_lemma_ref is_mes
rec_arg_num rec_arg_type relation =
Proofview.Goal.enter (fun gl ->
- let sigma = Proofview.Goal.sigma gl in
- let princ_type = Proofview.Goal.concl gl in
- let princ_info = compute_elim_sig sigma princ_type in
- let fresh_id =
- let avoid = ref (Tacmach.New.pf_ids_of_hyps gl) in
- fun na ->
- let new_id =
- match na with
- | Name id -> fresh_id !avoid (Id.to_string id)
- | Anonymous -> fresh_id !avoid "H"
+ let sigma = Proofview.Goal.sigma gl in
+ let princ_type = Proofview.Goal.concl gl in
+ let princ_info = compute_elim_sig sigma princ_type in
+ let fresh_id =
+ let avoid = ref (Tacmach.New.pf_ids_of_hyps gl) in
+ fun na ->
+ let new_id =
+ match na with
+ | Name id -> fresh_id !avoid (Id.to_string id)
+ | Anonymous -> fresh_id !avoid "H"
+ in
+ avoid := new_id :: !avoid;
+ Name new_id
in
- avoid := new_id :: !avoid;
- Name new_id
- in
- let fresh_decl = map_name fresh_id in
- let princ_info : elim_scheme =
- { princ_info with
- params = List.map fresh_decl princ_info.params
- ; predicates = List.map fresh_decl princ_info.predicates
- ; branches = List.map fresh_decl princ_info.branches
- ; args = List.map fresh_decl princ_info.args }
- in
- let wf_tac =
- if is_mes then fun b ->
- Recdef.tclUSER_if_not_mes Tacticals.New.tclIDTAC b None
- else fun _ -> prove_with_tcc tcc_lemma_ref []
- in
- let real_rec_arg_num = rec_arg_num - princ_info.nparams in
- let npost_rec_arg = princ_info.nargs - real_rec_arg_num + 1 in
- (* observe ( *)
- (* str "princ_type := " ++ pr_lconstr princ_type ++ fnl () ++ *)
- (* str "princ_info.nparams := " ++ int princ_info.nparams ++ fnl () ++ *)
+ let fresh_decl = map_name fresh_id in
+ let princ_info : elim_scheme =
+ { princ_info with
+ params = List.map fresh_decl princ_info.params
+ ; predicates = List.map fresh_decl princ_info.predicates
+ ; branches = List.map fresh_decl princ_info.branches
+ ; args = List.map fresh_decl princ_info.args }
+ in
+ let wf_tac =
+ if is_mes then fun b ->
+ Recdef.tclUSER_if_not_mes Tacticals.New.tclIDTAC b None
+ else fun _ -> prove_with_tcc tcc_lemma_ref []
+ in
+ let real_rec_arg_num = rec_arg_num - princ_info.nparams in
+ let npost_rec_arg = princ_info.nargs - real_rec_arg_num + 1 in
+ (* observe ( *)
+ (* str "princ_type := " ++ pr_lconstr princ_type ++ fnl () ++ *)
+ (* str "princ_info.nparams := " ++ int princ_info.nparams ++ fnl () ++ *)
- (* str "princ_info.nargs := " ++ int princ_info.nargs ++ fnl () ++ *)
- (* str "rec_arg_num := " ++ int rec_arg_num ++ fnl() ++ *)
- (* str "real_rec_arg_num := " ++ int real_rec_arg_num ++ fnl () ++ *)
- (* str "npost_rec_arg := " ++ int npost_rec_arg ); *)
- let post_rec_arg, pre_rec_arg =
- Util.List.chop npost_rec_arg princ_info.args
- in
- let rec_arg_id =
- match List.rev post_rec_arg with
- | ( LocalAssum ({binder_name = Name id}, _)
- | LocalDef ({binder_name = Name id}, _, _) )
- :: _ ->
- id
- | _ -> assert false
- in
- (* observe (str "rec_arg_id := " ++ pr_lconstr (mkVar rec_arg_id)); *)
- let subst_constrs =
- List.map
- (get_name %> Nameops.Name.get_id %> mkVar)
- (pre_rec_arg @ princ_info.params)
- in
- let relation = substl subst_constrs relation in
- let input_type = substl subst_constrs rec_arg_type in
- let wf_thm_id = Nameops.Name.get_id (fresh_id (Name (Id.of_string "wf_R"))) in
- let acc_rec_arg_id =
- Nameops.Name.get_id
- (fresh_id (Name (Id.of_string ("Acc_" ^ Id.to_string rec_arg_id))))
- in
- let open Tacticals.New in
- let revert l =
- tclTHEN
- (Tactics.generalize (List.map mkVar l))
- (clear l)
- in
- let fix_id = Nameops.Name.get_id (fresh_id (Name hrec_id)) in
- let prove_rec_arg_acc =
- (* observe_tac "prove_rec_arg_acc" *)
- tclCOMPLETE
- (tclTHEN
+ (* str "princ_info.nargs := " ++ int princ_info.nargs ++ fnl () ++ *)
+ (* str "rec_arg_num := " ++ int rec_arg_num ++ fnl() ++ *)
+ (* str "real_rec_arg_num := " ++ int real_rec_arg_num ++ fnl () ++ *)
+ (* str "npost_rec_arg := " ++ int npost_rec_arg ); *)
+ let post_rec_arg, pre_rec_arg =
+ Util.List.chop npost_rec_arg princ_info.args
+ in
+ let rec_arg_id =
+ match List.rev post_rec_arg with
+ | ( LocalAssum ({binder_name = Name id}, _)
+ | LocalDef ({binder_name = Name id}, _, _) )
+ :: _ ->
+ id
+ | _ -> assert false
+ in
+ (* observe (str "rec_arg_id := " ++ pr_lconstr (mkVar rec_arg_id)); *)
+ let subst_constrs =
+ List.map
+ (get_name %> Nameops.Name.get_id %> mkVar)
+ (pre_rec_arg @ princ_info.params)
+ in
+ let relation = substl subst_constrs relation in
+ let input_type = substl subst_constrs rec_arg_type in
+ let wf_thm_id =
+ Nameops.Name.get_id (fresh_id (Name (Id.of_string "wf_R")))
+ in
+ let acc_rec_arg_id =
+ Nameops.Name.get_id
+ (fresh_id (Name (Id.of_string ("Acc_" ^ Id.to_string rec_arg_id))))
+ in
+ let open Tacticals.New in
+ let revert l =
+ tclTHEN (Tactics.generalize (List.map mkVar l)) (clear l)
+ in
+ let fix_id = Nameops.Name.get_id (fresh_id (Name hrec_id)) in
+ let prove_rec_arg_acc =
+ (* observe_tac "prove_rec_arg_acc" *)
+ tclCOMPLETE
+ (tclTHEN
(assert_by (Name wf_thm_id)
(mkApp (delayed_force well_founded, [|input_type; relation|]))
- (* observe_tac "prove wf" *)
- (tclCOMPLETE (wf_tac is_mes)))
- ((* observe_tac *)
- (* "apply wf_thm" *)
- (Tactics.Simple.apply
- (mkApp (mkVar wf_thm_id, [|mkVar rec_arg_id|])))))
- in
- let args_ids = List.map (get_name %> Nameops.Name.get_id) princ_info.args in
- let lemma =
- match !tcc_lemma_ref with
- | Undefined -> user_err Pp.(str "No tcc proof !!")
- | Value lemma -> EConstr.of_constr lemma
- | Not_needed ->
- EConstr.of_constr
- (UnivGen.constr_of_monomorphic_global @@ Coqlib.lib_ref "core.True.I")
- in
- (* let rec list_diff del_list check_list = *)
- (* match del_list with *)
- (* [] -> *)
- (* [] *)
- (* | f::r -> *)
- (* if List.mem f check_list then *)
- (* list_diff r check_list *)
- (* else *)
- (* f::(list_diff r check_list) *)
- (* in *)
- let tcc_list = ref [] in
- let start_tac =
- Proofview.Goal.enter (fun gls ->
- let hyps = Tacmach.New.pf_ids_of_hyps gls in
- let hid =
- next_ident_away_in_goal (Id.of_string "prov") (Id.Set.of_list hyps)
- in
- tclTHENLIST
- [ generalize [lemma]
- ; Simple.intro hid
- ; Elim.h_decompose_and (mkVar hid)
- ; Proofview.Goal.enter (fun g ->
- let new_hyps = Tacmach.New.pf_ids_of_hyps g in
- tcc_list := List.rev (List.subtract Id.equal new_hyps (hid :: hyps));
- if List.is_empty !tcc_list then begin
- tcc_list := [hid];
- Proofview.tclUNIT ()
- end
- else clear [hid]) ])
- in
- tclTHENLIST
- [ observe_tac "start_tac" start_tac
- ; h_intros
- (List.rev_map
- (get_name %> Nameops.Name.get_id)
- ( princ_info.args @ princ_info.branches @ princ_info.predicates
- @ princ_info.params ))
- ; assert_by (Name acc_rec_arg_id)
- (mkApp
- (delayed_force acc_rel, [|input_type; relation; mkVar rec_arg_id|]))
- prove_rec_arg_acc
- ; revert (List.rev (acc_rec_arg_id :: args_ids))
- ; fix fix_id (List.length args_ids + 1)
- ; h_intros (List.rev (acc_rec_arg_id :: args_ids))
- ; Equality.rewriteLR (mkConst eq_ref)
- ; Proofview.Goal.enter (fun gl' ->
- let body =
- let _, args = destApp (Proofview.Goal.sigma gl') (Proofview.Goal.concl gl') in
- Array.last args
- in
- let body_info rec_hyps =
- { nb_rec_hyps = List.length rec_hyps
- ; rec_hyps
- ; eq_hyps = []
- ; info = body }
- in
- let acc_inv =
- lazy
+ (* observe_tac "prove wf" *)
+ (tclCOMPLETE (wf_tac is_mes)))
+ ((* observe_tac *)
+ (* "apply wf_thm" *)
+ Tactics.Simple.apply
+ (mkApp (mkVar wf_thm_id, [|mkVar rec_arg_id|]))))
+ in
+ let args_ids =
+ List.map (get_name %> Nameops.Name.get_id) princ_info.args
+ in
+ let lemma =
+ match !tcc_lemma_ref with
+ | Undefined -> user_err Pp.(str "No tcc proof !!")
+ | Value lemma -> EConstr.of_constr lemma
+ | Not_needed ->
+ EConstr.of_constr
+ ( UnivGen.constr_of_monomorphic_global
+ @@ Coqlib.lib_ref "core.True.I" )
+ in
+ (* let rec list_diff del_list check_list = *)
+ (* match del_list with *)
+ (* [] -> *)
+ (* [] *)
+ (* | f::r -> *)
+ (* if List.mem f check_list then *)
+ (* list_diff r check_list *)
+ (* else *)
+ (* f::(list_diff r check_list) *)
+ (* in *)
+ let tcc_list = ref [] in
+ let start_tac =
+ Proofview.Goal.enter (fun gls ->
+ let hyps = Tacmach.New.pf_ids_of_hyps gls in
+ let hid =
+ next_ident_away_in_goal (Id.of_string "prov")
+ (Id.Set.of_list hyps)
+ in
+ tclTHENLIST
+ [ generalize [lemma]
+ ; Simple.intro hid
+ ; Elim.h_decompose_and (mkVar hid)
+ ; Proofview.Goal.enter (fun g ->
+ let new_hyps = Tacmach.New.pf_ids_of_hyps g in
+ tcc_list :=
+ List.rev (List.subtract Id.equal new_hyps (hid :: hyps));
+ if List.is_empty !tcc_list then begin
+ tcc_list := [hid];
+ Proofview.tclUNIT ()
+ end
+ else clear [hid]) ])
+ in
+ tclTHENLIST
+ [ observe_tac "start_tac" start_tac
+ ; h_intros
+ (List.rev_map
+ (get_name %> Nameops.Name.get_id)
+ ( princ_info.args @ princ_info.branches @ princ_info.predicates
+ @ princ_info.params ))
+ ; assert_by (Name acc_rec_arg_id)
(mkApp
- ( delayed_force acc_inv_id
+ ( delayed_force acc_rel
, [|input_type; relation; mkVar rec_arg_id|] ))
- in
- let acc_inv =
- lazy (mkApp (Lazy.force acc_inv, [|mkVar acc_rec_arg_id|]))
- in
- let predicates_names =
- List.map (get_name %> Nameops.Name.get_id) princ_info.predicates
- in
- let pte_info =
- { proving_tac =
- (fun eqs ->
- (* msgnl (str "tcc_list := "++ prlist_with_sep spc Ppconstr.pr_id !tcc_list); *)
- (* msgnl (str "princ_info.args := "++ prlist_with_sep spc Ppconstr.pr_id (List.map (fun (na,_,_) -> (Nameops.Name.get_id na)) princ_info.args)); *)
- (* msgnl (str "princ_info.params := "++ prlist_with_sep spc Ppconstr.pr_id (List.map (fun (na,_,_) -> (Nameops.Name.get_id na)) princ_info.params)); *)
- (* msgnl (str "acc_rec_arg_id := "++ Ppconstr.pr_id acc_rec_arg_id); *)
- (* msgnl (str "eqs := "++ prlist_with_sep spc Ppconstr.pr_id eqs); *)
+ prove_rec_arg_acc
+ ; revert (List.rev (acc_rec_arg_id :: args_ids))
+ ; fix fix_id (List.length args_ids + 1)
+ ; h_intros (List.rev (acc_rec_arg_id :: args_ids))
+ ; Equality.rewriteLR (mkConst eq_ref)
+ ; Proofview.Goal.enter (fun gl' ->
+ let body =
+ let _, args =
+ destApp (Proofview.Goal.sigma gl') (Proofview.Goal.concl gl')
+ in
+ Array.last args
+ in
+ let body_info rec_hyps =
+ { nb_rec_hyps = List.length rec_hyps
+ ; rec_hyps
+ ; eq_hyps = []
+ ; info = body }
+ in
+ let acc_inv =
+ lazy
+ (mkApp
+ ( delayed_force acc_inv_id
+ , [|input_type; relation; mkVar rec_arg_id|] ))
+ in
+ let acc_inv =
+ lazy (mkApp (Lazy.force acc_inv, [|mkVar acc_rec_arg_id|]))
+ in
+ let predicates_names =
+ List.map (get_name %> Nameops.Name.get_id) princ_info.predicates
+ in
+ let pte_info =
+ { proving_tac =
+ (fun eqs ->
+ (* msgnl (str "tcc_list := "++ prlist_with_sep spc Ppconstr.pr_id !tcc_list); *)
+ (* msgnl (str "princ_info.args := "++ prlist_with_sep spc Ppconstr.pr_id (List.map (fun (na,_,_) -> (Nameops.Name.get_id na)) princ_info.args)); *)
+ (* msgnl (str "princ_info.params := "++ prlist_with_sep spc Ppconstr.pr_id (List.map (fun (na,_,_) -> (Nameops.Name.get_id na)) princ_info.params)); *)
+ (* msgnl (str "acc_rec_arg_id := "++ Ppconstr.pr_id acc_rec_arg_id); *)
+ (* msgnl (str "eqs := "++ prlist_with_sep spc Ppconstr.pr_id eqs); *)
- (* observe_tac "new_prove_with_tcc" *)
- new_prove_with_tcc is_mes acc_inv fix_id
- ( !tcc_list
- @ List.map
- (get_name %> Nameops.Name.get_id)
- (princ_info.args @ princ_info.params)
- @ [acc_rec_arg_id] )
- eqs)
- ; is_valid = is_valid_hypothesis (Proofview.Goal.sigma gl') predicates_names }
- in
- let ptes_info : pte_info Id.Map.t =
- List.fold_left
- (fun map pte_id -> Id.Map.add pte_id pte_info map)
- Id.Map.empty predicates_names
- in
- let make_proof rec_hyps =
- build_proof false [f_ref] ptes_info (body_info rec_hyps)
- in
- (* observe_tac "instantiate_hyps_with_args" *)
- (instantiate_hyps_with_args make_proof
- (List.map (get_name %> Nameops.Name.get_id) princ_info.branches)
- (List.rev args_ids))
- ) ])
+ (* observe_tac "new_prove_with_tcc" *)
+ new_prove_with_tcc is_mes acc_inv fix_id
+ ( !tcc_list
+ @ List.map
+ (get_name %> Nameops.Name.get_id)
+ (princ_info.args @ princ_info.params)
+ @ [acc_rec_arg_id] )
+ eqs)
+ ; is_valid =
+ is_valid_hypothesis (Proofview.Goal.sigma gl')
+ predicates_names }
+ in
+ let ptes_info : pte_info Id.Map.t =
+ List.fold_left
+ (fun map pte_id -> Id.Map.add pte_id pte_info map)
+ Id.Map.empty predicates_names
+ in
+ let make_proof rec_hyps =
+ build_proof false [f_ref] ptes_info (body_info rec_hyps)
+ in
+ (* observe_tac "instantiate_hyps_with_args" *)
+ instantiate_hyps_with_args make_proof
+ (List.map (get_name %> Nameops.Name.get_id) princ_info.branches)
+ (List.rev args_ids)) ])
diff --git a/plugins/funind/gen_principle.ml b/plugins/funind/gen_principle.ml
index 402082d01e..1ea803f561 100644
--- a/plugins/funind/gen_principle.ml
+++ b/plugins/funind/gen_principle.ml
@@ -600,230 +600,233 @@ let prove_fun_correct evd graphs_constr schemes lemmas_types_infos i :
let open Tactics in
let open Tacticals.New in
Proofview.Goal.enter (fun g ->
- (* first of all we recreate the lemmas types to be used as predicates of the induction principle
- that is~:
- \[fun (x_1:t_1)\ldots(x_n:t_n)=> fun fv => fun res => res = fv \rightarrow graph\ x_1\ldots x_n\ res\]
- *)
- (* we the get the definition of the graphs block *)
- let graph_ind, u = destInd evd graphs_constr.(i) in
- let kn = fst graph_ind in
- let mib, _ = Global.lookup_inductive graph_ind in
- (* and the principle to use in this lemma in $\zeta$ normal form *)
- let f_principle, princ_type = schemes.(i) in
- let princ_type = Reductionops.nf_zeta (Global.env ()) evd princ_type in
- let princ_infos = Tactics.compute_elim_sig evd princ_type in
- (* The number of args of the function is then easily computable *)
- let nb_fun_args = Termops.nb_prod (Proofview.Goal.sigma g) (Proofview.Goal.concl g) - 2 in
- let args_names = generate_fresh_id (Id.of_string "x") [] nb_fun_args in
- let ids = args_names @ pf_ids_of_hyps g in
- (* Since we cannot ensure that the functional principle is defined in the
- environment and due to the bug #1174, we will need to pose the principle
- using a name
- *)
- let principle_id =
- Namegen.next_ident_away_in_goal (Id.of_string "princ")
- (Id.Set.of_list ids)
- in
- let ids = principle_id :: ids in
- (* We get the branches of the principle *)
- let branches = List.rev princ_infos.Tactics.branches in
- (* and built the intro pattern for each of them *)
- let intro_pats =
- List.map
- (fun decl ->
- List.map
- (fun id ->
- CAst.make @@ Tactypes.IntroNaming (Namegen.IntroIdentifier id))
- (generate_fresh_id (Id.of_string "y") ids
- (List.length
- (fst (decompose_prod_assum evd (RelDecl.get_type decl))))))
- branches
- in
- (* before building the full intro pattern for the principle *)
- let eq_ind = make_eq () in
- let eq_construct = mkConstructUi (destInd evd eq_ind, 1) in
- (* The next to referencies will be used to find out which constructor to apply in each branch *)
- let ind_number = ref 0 and min_constr_number = ref 0 in
- (* The tactic to prove the ith branch of the principle *)
- let prove_branch i pat =
- (* We get the identifiers of this branch *)
- let pre_args =
- List.fold_right
- (fun {CAst.v = pat} acc ->
- match pat with
- | Tactypes.IntroNaming (Namegen.IntroIdentifier id) -> id :: acc
- | _ -> CErrors.anomaly (Pp.str "Not an identifier."))
- pat
- []
+ (* first of all we recreate the lemmas types to be used as predicates of the induction principle
+ that is~:
+ \[fun (x_1:t_1)\ldots(x_n:t_n)=> fun fv => fun res => res = fv \rightarrow graph\ x_1\ldots x_n\ res\]
+ *)
+ (* we the get the definition of the graphs block *)
+ let graph_ind, u = destInd evd graphs_constr.(i) in
+ let kn = fst graph_ind in
+ let mib, _ = Global.lookup_inductive graph_ind in
+ (* and the principle to use in this lemma in $\zeta$ normal form *)
+ let f_principle, princ_type = schemes.(i) in
+ let princ_type = Reductionops.nf_zeta (Global.env ()) evd princ_type in
+ let princ_infos = Tactics.compute_elim_sig evd princ_type in
+ (* The number of args of the function is then easily computable *)
+ let nb_fun_args =
+ Termops.nb_prod (Proofview.Goal.sigma g) (Proofview.Goal.concl g) - 2
+ in
+ let args_names = generate_fresh_id (Id.of_string "x") [] nb_fun_args in
+ let ids = args_names @ pf_ids_of_hyps g in
+ (* Since we cannot ensure that the functional principle is defined in the
+ environment and due to the bug #1174, we will need to pose the principle
+ using a name
+ *)
+ let principle_id =
+ Namegen.next_ident_away_in_goal (Id.of_string "princ")
+ (Id.Set.of_list ids)
+ in
+ let ids = principle_id :: ids in
+ (* We get the branches of the principle *)
+ let branches = List.rev princ_infos.Tactics.branches in
+ (* and built the intro pattern for each of them *)
+ let intro_pats =
+ List.map
+ (fun decl ->
+ List.map
+ (fun id ->
+ CAst.make @@ Tactypes.IntroNaming (Namegen.IntroIdentifier id))
+ (generate_fresh_id (Id.of_string "y") ids
+ (List.length
+ (fst (decompose_prod_assum evd (RelDecl.get_type decl))))))
+ branches
in
- (* and get the real args of the branch by unfolding the defined constant *)
- (*
+ (* before building the full intro pattern for the principle *)
+ let eq_ind = make_eq () in
+ let eq_construct = mkConstructUi (destInd evd eq_ind, 1) in
+ (* The next to referencies will be used to find out which constructor to apply in each branch *)
+ let ind_number = ref 0 and min_constr_number = ref 0 in
+ (* The tactic to prove the ith branch of the principle *)
+ let prove_branch i pat =
+ (* We get the identifiers of this branch *)
+ let pre_args =
+ List.fold_right
+ (fun {CAst.v = pat} acc ->
+ match pat with
+ | Tactypes.IntroNaming (Namegen.IntroIdentifier id) -> id :: acc
+ | _ -> CErrors.anomaly (Pp.str "Not an identifier."))
+ pat []
+ in
+ (* and get the real args of the branch by unfolding the defined constant *)
+ (*
We can then recompute the arguments of the constructor.
For each [hid] introduced by this branch, if [hid] has type
$forall res, res=fv -> graph.(j)\ x_1\ x_n res$ the corresponding arguments of the constructor are
[ fv (hid fv (refl_equal fv)) ].
If [hid] has another type the corresponding argument of the constructor is [hid]
*)
- let constructor_args g =
- List.fold_right
- (fun hid acc ->
- let type_of_hid = pf_get_hyp_typ hid g in
- let sigma = Proofview.Goal.sigma g in
- match EConstr.kind sigma type_of_hid with
- | Prod (_, _, t') -> (
- match EConstr.kind sigma t' with
- | Prod (_, t'', t''') -> (
- match (EConstr.kind sigma t'', EConstr.kind sigma t''') with
- | App (eq, args), App (graph', _)
- when EConstr.eq_constr sigma eq eq_ind
- && Array.exists
- (EConstr.eq_constr_nounivs sigma graph')
- graphs_constr ->
- args.(2)
- :: mkApp
- ( mkVar hid
- , [| args.(2)
- ; mkApp (eq_construct, [|args.(0); args.(2)|]) |] )
- :: acc
+ let constructor_args g =
+ List.fold_right
+ (fun hid acc ->
+ let type_of_hid = pf_get_hyp_typ hid g in
+ let sigma = Proofview.Goal.sigma g in
+ match EConstr.kind sigma type_of_hid with
+ | Prod (_, _, t') -> (
+ match EConstr.kind sigma t' with
+ | Prod (_, t'', t''') -> (
+ match (EConstr.kind sigma t'', EConstr.kind sigma t''') with
+ | App (eq, args), App (graph', _)
+ when EConstr.eq_constr sigma eq eq_ind
+ && Array.exists
+ (EConstr.eq_constr_nounivs sigma graph')
+ graphs_constr ->
+ args.(2)
+ :: mkApp
+ ( mkVar hid
+ , [| args.(2)
+ ; mkApp (eq_construct, [|args.(0); args.(2)|]) |] )
+ :: acc
+ | _ -> mkVar hid :: acc )
| _ -> mkVar hid :: acc )
- | _ -> mkVar hid :: acc )
- | _ -> mkVar hid :: acc)
- pre_args []
- in
- (* in fact we must also add the parameters to the constructor args *)
- let constructor_args g =
- let params_id =
- fst (List.chop princ_infos.Tactics.nparams args_names)
+ | _ -> mkVar hid :: acc)
+ pre_args []
in
- List.map mkVar params_id @ constructor_args g
- in
- (* We then get the constructor corresponding to this branch and
- modifies the references has needed i.e.
- if the constructor is the last one of the current inductive then
- add one the number of the inductive to take and add the number of constructor of the previous
- graph to the minimal constructor number
- *)
- let constructor =
- let constructor_num = i - !min_constr_number in
- let length =
- Array.length
- mib.Declarations.mind_packets.(!ind_number)
- .Declarations.mind_consnames
+ (* in fact we must also add the parameters to the constructor args *)
+ let constructor_args g =
+ let params_id =
+ fst (List.chop princ_infos.Tactics.nparams args_names)
+ in
+ List.map mkVar params_id @ constructor_args g
in
- if constructor_num <= length then ((kn, !ind_number), constructor_num)
- else begin
- incr ind_number;
- min_constr_number := !min_constr_number + length;
- ((kn, !ind_number), 1)
- end
- in
- (* we can then build the final proof term *)
- let app_constructor g =
- applist (mkConstructU (constructor, u), constructor_args g)
+ (* We then get the constructor corresponding to this branch and
+ modifies the references has needed i.e.
+ if the constructor is the last one of the current inductive then
+ add one the number of the inductive to take and add the number of constructor of the previous
+ graph to the minimal constructor number
+ *)
+ let constructor =
+ let constructor_num = i - !min_constr_number in
+ let length =
+ Array.length
+ mib.Declarations.mind_packets.(!ind_number)
+ .Declarations.mind_consnames
+ in
+ if constructor_num <= length then ((kn, !ind_number), constructor_num)
+ else begin
+ incr ind_number;
+ min_constr_number := !min_constr_number + length;
+ ((kn, !ind_number), 1)
+ end
+ in
+ (* we can then build the final proof term *)
+ let app_constructor g =
+ applist (mkConstructU (constructor, u), constructor_args g)
+ in
+ (* an apply the tactic *)
+ let res, hres =
+ match
+ generate_fresh_id (Id.of_string "z") ids (* @this_branche_ids *) 2
+ with
+ | [res; hres] -> (res, hres)
+ | _ -> assert false
+ in
+ (* observe (str "constructor := " ++ Printer.pr_lconstr_env (pf_env g) app_constructor); *)
+ tclTHENLIST
+ [ observe_tac "h_intro_patterns "
+ (match pat with [] -> tclIDTAC | _ -> intro_patterns false pat)
+ ; (* unfolding of all the defined variables introduced by this branch *)
+ (* observe_tac "unfolding" pre_tac; *)
+ (* $zeta$ normalizing of the conclusion *)
+ reduce
+ (Genredexpr.Cbv
+ { Redops.all_flags with
+ Genredexpr.rDelta = false
+ ; Genredexpr.rConst = [] })
+ Locusops.onConcl
+ ; observe_tac "toto " (Proofview.tclUNIT ())
+ ; (* introducing the result of the graph and the equality hypothesis *)
+ observe_tac "introducing" (tclMAP Simple.intro [res; hres])
+ ; (* replacing [res] with its value *)
+ observe_tac "rewriting res value" (Equality.rewriteLR (mkVar hres))
+ ; (* Conclusion *)
+ observe_tac "exact"
+ (Proofview.Goal.enter (fun g -> exact_check (app_constructor g)))
+ ]
in
- (* an apply the tactic *)
- let res, hres =
- match
- generate_fresh_id (Id.of_string "z") ids (* @this_branche_ids *) 2
- with
- | [res; hres] -> (res, hres)
- | _ -> assert false
+ (* end of branche proof *)
+ let lemmas =
+ Array.map
+ (fun (_, (ctxt, concl)) ->
+ match ctxt with
+ | [] | [_] | [_; _] -> CErrors.anomaly (Pp.str "bad context.")
+ | hres :: res :: decl :: ctxt ->
+ let res =
+ EConstr.it_mkLambda_or_LetIn
+ (EConstr.it_mkProd_or_LetIn concl [hres; res])
+ ( LocalAssum (RelDecl.get_annot decl, RelDecl.get_type decl)
+ :: ctxt )
+ in
+ res)
+ lemmas_types_infos
in
- (* observe (str "constructor := " ++ Printer.pr_lconstr_env (pf_env g) app_constructor); *)
- (tclTHENLIST
- [ observe_tac "h_intro_patterns "
- (match pat with
- | [] -> tclIDTAC
- | _ -> intro_patterns false pat)
- ; (* unfolding of all the defined variables introduced by this branch *)
- (* observe_tac "unfolding" pre_tac; *)
- (* $zeta$ normalizing of the conclusion *)
- reduce
- (Genredexpr.Cbv
- { Redops.all_flags with
- Genredexpr.rDelta = false
- ; Genredexpr.rConst = [] })
- Locusops.onConcl
- ; observe_tac "toto " (Proofview.tclUNIT ())
- ; (* introducing the result of the graph and the equality hypothesis *)
- observe_tac "introducing"
- (tclMAP Simple.intro [res; hres])
- ; (* replacing [res] with its value *)
- observe_tac "rewriting res value"
- (Equality.rewriteLR (mkVar hres))
- ; (* Conclusion *)
- observe_tac "exact" (Proofview.Goal.enter (fun g ->
- exact_check (app_constructor g))) ])
- in
- (* end of branche proof *)
- let lemmas =
- Array.map
- (fun (_, (ctxt, concl)) ->
- match ctxt with
- | [] | [_] | [_; _] -> CErrors.anomaly (Pp.str "bad context.")
- | hres :: res :: decl :: ctxt ->
- let res =
- EConstr.it_mkLambda_or_LetIn
- (EConstr.it_mkProd_or_LetIn concl [hres; res])
- ( LocalAssum (RelDecl.get_annot decl, RelDecl.get_type decl)
- :: ctxt )
- in
- res)
- lemmas_types_infos
- in
- let param_names = fst (List.chop princ_infos.nparams args_names) in
- let params = List.map mkVar param_names in
- let lemmas =
- Array.to_list (Array.map (fun c -> applist (c, params)) lemmas)
- in
- (* The bindings of the principle
- that is the params of the principle and the different lemma types
- *)
- let bindings =
- let params_bindings, avoid =
- List.fold_left2
- (fun (bindings, avoid) decl p ->
- let id =
- Namegen.next_ident_away
- (Nameops.Name.get_id (RelDecl.get_name decl))
- (Id.Set.of_list avoid)
- in
- (p :: bindings, id :: avoid))
- ([], pf_ids_of_hyps g)
- princ_infos.params (List.rev params)
+ let param_names = fst (List.chop princ_infos.nparams args_names) in
+ let params = List.map mkVar param_names in
+ let lemmas =
+ Array.to_list (Array.map (fun c -> applist (c, params)) lemmas)
in
- let lemmas_bindings =
- List.rev
- (fst
- (List.fold_left2
- (fun (bindings, avoid) decl p ->
- let id =
- Namegen.next_ident_away
- (Nameops.Name.get_id (RelDecl.get_name decl))
- (Id.Set.of_list avoid)
- in
- ( Reductionops.nf_zeta (Proofview.Goal.env g) (Proofview.Goal.sigma g) p :: bindings
- , id :: avoid ))
- ([], avoid) princ_infos.predicates lemmas))
+ (* The bindings of the principle
+ that is the params of the principle and the different lemma types
+ *)
+ let bindings =
+ let params_bindings, avoid =
+ List.fold_left2
+ (fun (bindings, avoid) decl p ->
+ let id =
+ Namegen.next_ident_away
+ (Nameops.Name.get_id (RelDecl.get_name decl))
+ (Id.Set.of_list avoid)
+ in
+ (p :: bindings, id :: avoid))
+ ([], pf_ids_of_hyps g)
+ princ_infos.params (List.rev params)
+ in
+ let lemmas_bindings =
+ List.rev
+ (fst
+ (List.fold_left2
+ (fun (bindings, avoid) decl p ->
+ let id =
+ Namegen.next_ident_away
+ (Nameops.Name.get_id (RelDecl.get_name decl))
+ (Id.Set.of_list avoid)
+ in
+ ( Reductionops.nf_zeta (Proofview.Goal.env g)
+ (Proofview.Goal.sigma g) p
+ :: bindings
+ , id :: avoid ))
+ ([], avoid) princ_infos.predicates lemmas))
+ in
+ params_bindings @ lemmas_bindings
in
- params_bindings @ lemmas_bindings
- in
- tclTHENLIST
- [ observe_tac "principle"
- (assert_by (Name principle_id) princ_type
- (exact_check f_principle))
- ; observe_tac "intro args_names"
- (tclMAP Simple.intro args_names)
- ; (* observe_tac "titi" (pose_proof (Name (Id.of_string "__")) (Reductionops.nf_beta Evd.empty ((mkApp (mkVar principle_id,Array.of_list bindings))))); *)
- observe_tac "idtac" tclIDTAC
- ; tclTHENS
- (observe_tac "functional_induction" (Proofview.Goal.enter (fun gl ->
- let term = mkApp (mkVar principle_id, Array.of_list bindings) in
- tclTYPEOFTHEN ~refresh:true term (fun _ _ ->
- apply term))))
- (List.map_i (fun i pat -> observe_tac
- ("proving branch " ^ string_of_int i)
- (prove_branch i pat)) 1 intro_pats) ])
+ tclTHENLIST
+ [ observe_tac "principle"
+ (assert_by (Name principle_id) princ_type (exact_check f_principle))
+ ; observe_tac "intro args_names" (tclMAP Simple.intro args_names)
+ ; (* observe_tac "titi" (pose_proof (Name (Id.of_string "__")) (Reductionops.nf_beta Evd.empty ((mkApp (mkVar principle_id,Array.of_list bindings))))); *)
+ observe_tac "idtac" tclIDTAC
+ ; tclTHENS
+ (observe_tac "functional_induction"
+ (Proofview.Goal.enter (fun gl ->
+ let term =
+ mkApp (mkVar principle_id, Array.of_list bindings)
+ in
+ tclTYPEOFTHEN ~refresh:true term (fun _ _ -> apply term))))
+ (List.map_i
+ (fun i pat ->
+ observe_tac
+ ("proving branch " ^ string_of_int i)
+ (prove_branch i pat))
+ 1 intro_pats) ])
(* [prove_fun_complete funs graphs schemes lemmas_types_infos i]
is the tactic used to prove completeness lemma.
@@ -873,16 +876,15 @@ let generalize_dependent_of x hyp =
let open Context.Named.Declaration in
let open Tacticals.New in
Proofview.Goal.enter (fun g ->
- tclMAP
- (function
- | LocalAssum ({Context.binder_name = id}, t)
- when (not (Id.equal id hyp))
- && Termops.occur_var (Proofview.Goal.env g) (Proofview.Goal.sigma g) x t ->
- tclTHEN
- (Tactics.generalize [EConstr.mkVar id])
- (thin [id])
- | _ -> Proofview.tclUNIT ())
- (Proofview.Goal.hyps g))
+ tclMAP
+ (function
+ | LocalAssum ({Context.binder_name = id}, t)
+ when (not (Id.equal id hyp))
+ && Termops.occur_var (Proofview.Goal.env g)
+ (Proofview.Goal.sigma g) x t ->
+ tclTHEN (Tactics.generalize [EConstr.mkVar id]) (thin [id])
+ | _ -> Proofview.tclUNIT ())
+ (Proofview.Goal.hyps g))
let rec intros_with_rewrite () =
observe_tac "intros_with_rewrite" (intros_with_rewrite_aux ())
@@ -894,100 +896,100 @@ and intros_with_rewrite_aux () : unit Proofview.tactic =
let open Tactics in
let open Tacticals.New in
Proofview.Goal.enter (fun g ->
- let eq_ind = make_eq () in
- let sigma = Proofview.Goal.sigma g in
- match EConstr.kind sigma (Proofview.Goal.concl g) with
- | Prod (_, t, t') -> (
- match EConstr.kind sigma t with
- | App (eq, args) when EConstr.eq_constr sigma eq eq_ind ->
- if Reductionops.is_conv (Proofview.Goal.env g) (Proofview.Goal.sigma g) args.(1) args.(2) then
- let id = pf_get_new_id (Id.of_string "y") g in
- tclTHENLIST
- [ Simple.intro id
- ; thin [id]
- ; intros_with_rewrite () ]
- else if
- isVar sigma args.(1)
- && Environ.evaluable_named (destVar sigma args.(1)) (Proofview.Goal.env g)
- then
- tclTHENLIST
- [ unfold_in_concl
- [ ( Locus.AllOccurrences
- , Names.EvalVarRef (destVar sigma args.(1)) ) ]
- ; tclMAP
- (fun id ->
- tclTRY
- (unfold_in_hyp
- [ ( Locus.AllOccurrences
- , Names.EvalVarRef (destVar sigma args.(1)) ) ]
- (destVar sigma args.(1), Locus.InHyp)))
- (pf_ids_of_hyps g)
- ; intros_with_rewrite () ]
- else if
- isVar sigma args.(2)
- && Environ.evaluable_named (destVar sigma args.(2)) (Proofview.Goal.env g)
- then
- tclTHENLIST
- [ unfold_in_concl
- [ ( Locus.AllOccurrences
- , Names.EvalVarRef (destVar sigma args.(2)) ) ]
- ; tclMAP
- (fun id ->
- tclTRY
- (unfold_in_hyp
- [ ( Locus.AllOccurrences
- , Names.EvalVarRef (destVar sigma args.(2)) ) ]
- (destVar sigma args.(2), Locus.InHyp)))
- (pf_ids_of_hyps g)
- ; intros_with_rewrite () ]
- else if isVar sigma args.(1) then
- let id = pf_get_new_id (Id.of_string "y") g in
- tclTHENLIST
- [ Simple.intro id
- ; generalize_dependent_of (destVar sigma args.(1)) id
- ; tclTRY (Equality.rewriteLR (mkVar id))
- ; intros_with_rewrite () ]
- else if isVar sigma args.(2) then
- let id = pf_get_new_id (Id.of_string "y") g in
+ let eq_ind = make_eq () in
+ let sigma = Proofview.Goal.sigma g in
+ match EConstr.kind sigma (Proofview.Goal.concl g) with
+ | Prod (_, t, t') -> (
+ match EConstr.kind sigma t with
+ | App (eq, args) when EConstr.eq_constr sigma eq eq_ind ->
+ if
+ Reductionops.is_conv (Proofview.Goal.env g) (Proofview.Goal.sigma g)
+ args.(1) args.(2)
+ then
+ let id = pf_get_new_id (Id.of_string "y") g in
+ tclTHENLIST [Simple.intro id; thin [id]; intros_with_rewrite ()]
+ else if
+ isVar sigma args.(1)
+ && Environ.evaluable_named
+ (destVar sigma args.(1))
+ (Proofview.Goal.env g)
+ then
+ tclTHENLIST
+ [ unfold_in_concl
+ [ ( Locus.AllOccurrences
+ , Names.EvalVarRef (destVar sigma args.(1)) ) ]
+ ; tclMAP
+ (fun id ->
+ tclTRY
+ (unfold_in_hyp
+ [ ( Locus.AllOccurrences
+ , Names.EvalVarRef (destVar sigma args.(1)) ) ]
+ (destVar sigma args.(1), Locus.InHyp)))
+ (pf_ids_of_hyps g)
+ ; intros_with_rewrite () ]
+ else if
+ isVar sigma args.(2)
+ && Environ.evaluable_named
+ (destVar sigma args.(2))
+ (Proofview.Goal.env g)
+ then
+ tclTHENLIST
+ [ unfold_in_concl
+ [ ( Locus.AllOccurrences
+ , Names.EvalVarRef (destVar sigma args.(2)) ) ]
+ ; tclMAP
+ (fun id ->
+ tclTRY
+ (unfold_in_hyp
+ [ ( Locus.AllOccurrences
+ , Names.EvalVarRef (destVar sigma args.(2)) ) ]
+ (destVar sigma args.(2), Locus.InHyp)))
+ (pf_ids_of_hyps g)
+ ; intros_with_rewrite () ]
+ else if isVar sigma args.(1) then
+ let id = pf_get_new_id (Id.of_string "y") g in
+ tclTHENLIST
+ [ Simple.intro id
+ ; generalize_dependent_of (destVar sigma args.(1)) id
+ ; tclTRY (Equality.rewriteLR (mkVar id))
+ ; intros_with_rewrite () ]
+ else if isVar sigma args.(2) then
+ let id = pf_get_new_id (Id.of_string "y") g in
+ tclTHENLIST
+ [ Simple.intro id
+ ; generalize_dependent_of (destVar sigma args.(2)) id
+ ; tclTRY (Equality.rewriteRL (mkVar id))
+ ; intros_with_rewrite () ]
+ else
+ let id = pf_get_new_id (Id.of_string "y") g in
+ tclTHENLIST
+ [ Simple.intro id
+ ; tclTRY (Equality.rewriteLR (mkVar id))
+ ; intros_with_rewrite () ]
+ | Ind _
+ when EConstr.eq_constr sigma t
+ (EConstr.of_constr
+ ( UnivGen.constr_of_monomorphic_global
+ @@ Coqlib.lib_ref "core.False.type" )) ->
+ tauto
+ | Case (_, _, _, v, _) ->
+ tclTHENLIST [simplest_case v; intros_with_rewrite ()]
+ | LetIn _ ->
tclTHENLIST
- [ Simple.intro id
- ; generalize_dependent_of (destVar sigma args.(2)) id
- ; tclTRY (Equality.rewriteRL (mkVar id))
+ [ reduce
+ (Genredexpr.Cbv {Redops.all_flags with Genredexpr.rDelta = false})
+ Locusops.onConcl
; intros_with_rewrite () ]
- else
+ | _ ->
let id = pf_get_new_id (Id.of_string "y") g in
- tclTHENLIST
- [ Simple.intro id
- ; tclTRY (Equality.rewriteLR (mkVar id))
- ; intros_with_rewrite () ]
- | Ind _
- when EConstr.eq_constr sigma t
- (EConstr.of_constr
- ( UnivGen.constr_of_monomorphic_global
- @@ Coqlib.lib_ref "core.False.type" )) ->
- tauto
- | Case (_, _, _, v, _) ->
- tclTHENLIST
- [simplest_case v; intros_with_rewrite ()]
+ tclTHENLIST [Simple.intro id; intros_with_rewrite ()] )
| LetIn _ ->
tclTHENLIST
[ reduce
- (Genredexpr.Cbv
- {Redops.all_flags with Genredexpr.rDelta = false})
- Locusops.onConcl
+ (Genredexpr.Cbv {Redops.all_flags with Genredexpr.rDelta = false})
+ Locusops.onConcl
; intros_with_rewrite () ]
- | _ ->
- let id = pf_get_new_id (Id.of_string "y") g in
- tclTHENLIST
- [Simple.intro id; intros_with_rewrite ()]
- )
- | LetIn _ ->
- tclTHENLIST
- [ reduce
- (Genredexpr.Cbv {Redops.all_flags with Genredexpr.rDelta = false})
- Locusops.onConcl
- ; intros_with_rewrite () ]
- | _ -> Proofview.tclUNIT ())
+ | _ -> Proofview.tclUNIT ())
let rec reflexivity_with_destruct_cases () =
let open Constr in
@@ -996,64 +998,72 @@ let rec reflexivity_with_destruct_cases () =
let open Tactics in
let open Tacticals.New in
Proofview.Goal.enter (fun g ->
- let destruct_case () =
- try
- match
- EConstr.kind (Proofview.Goal.sigma g) (snd (destApp (Proofview.Goal.sigma g) (Proofview.Goal.concl g))).(2)
- with
- | Case (_, _, _, v, _) ->
- tclTHENLIST
- [ simplest_case v
- ; intros
- ; observe_tac "reflexivity_with_destruct_cases"
- (reflexivity_with_destruct_cases ()) ]
- | _ -> reflexivity
- with e when CErrors.noncritical e -> reflexivity
- in
- let eq_ind = make_eq () in
- let my_inj_flags =
- Some
- { Equality.keep_proof_equalities = false
- ; injection_in_context = false
- ; (* for compatibility, necessary *)
- injection_pattern_l2r_order =
- false (* probably does not matter; except maybe with dependent hyps *)
- }
- in
- let discr_inject =
- onAllHypsAndConcl (fun sc ->
- match sc with
- | None -> Proofview.tclUNIT ()
- | Some id ->
- Proofview.Goal.enter (fun g ->
- match EConstr.kind (Proofview.Goal.sigma g) (pf_get_hyp_typ id g) with
- | App (eq, [|_; t1; t2|]) when EConstr.eq_constr (Proofview.Goal.sigma g) eq eq_ind
- ->
- if Equality.discriminable (Proofview.Goal.env g) (Proofview.Goal.sigma g) t1 t2 then
- Equality.discrHyp id
- else if
- Equality.injectable (Proofview.Goal.env g) (Proofview.Goal.sigma g) ~keep_proofs:None t1 t2
- then
- tclTHENLIST
- [ Equality.injHyp my_inj_flags None id
- ; thin [id]
- ; intros_with_rewrite () ]
- else Proofview.tclUNIT ()
- | _ -> Proofview.tclUNIT ()))
- in
- tclFIRST
- [ observe_tac "reflexivity_with_destruct_cases : reflexivity"
- reflexivity
- ; observe_tac "reflexivity_with_destruct_cases : 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
- *)
- observe_tac "reflexivity_with_destruct_cases : others"
- (tclTHEN (tclPROGRESS discr_inject) (reflexivity_with_destruct_cases ())) ])
+ let destruct_case () =
+ try
+ match
+ EConstr.kind (Proofview.Goal.sigma g)
+ (snd (destApp (Proofview.Goal.sigma g) (Proofview.Goal.concl g))).(
+ 2)
+ with
+ | Case (_, _, _, v, _) ->
+ tclTHENLIST
+ [ simplest_case v
+ ; intros
+ ; observe_tac "reflexivity_with_destruct_cases"
+ (reflexivity_with_destruct_cases ()) ]
+ | _ -> reflexivity
+ with e when CErrors.noncritical e -> reflexivity
+ in
+ let eq_ind = make_eq () in
+ let my_inj_flags =
+ Some
+ { Equality.keep_proof_equalities = false
+ ; injection_in_context = false
+ ; (* for compatibility, necessary *)
+ injection_pattern_l2r_order =
+ false
+ (* probably does not matter; except maybe with dependent hyps *)
+ }
+ in
+ let discr_inject =
+ onAllHypsAndConcl (fun sc ->
+ match sc with
+ | None -> Proofview.tclUNIT ()
+ | Some id ->
+ Proofview.Goal.enter (fun g ->
+ match
+ EConstr.kind (Proofview.Goal.sigma g) (pf_get_hyp_typ id g)
+ with
+ | App (eq, [|_; t1; t2|])
+ when EConstr.eq_constr (Proofview.Goal.sigma g) eq eq_ind ->
+ if
+ Equality.discriminable (Proofview.Goal.env g)
+ (Proofview.Goal.sigma g) t1 t2
+ then Equality.discrHyp id
+ else if
+ Equality.injectable (Proofview.Goal.env g)
+ (Proofview.Goal.sigma g) ~keep_proofs:None t1 t2
+ then
+ tclTHENLIST
+ [ Equality.injHyp my_inj_flags None id
+ ; thin [id]
+ ; intros_with_rewrite () ]
+ else Proofview.tclUNIT ()
+ | _ -> Proofview.tclUNIT ()))
+ in
+ tclFIRST
+ [ observe_tac "reflexivity_with_destruct_cases : reflexivity" reflexivity
+ ; observe_tac "reflexivity_with_destruct_cases : 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
+ *)
+ observe_tac "reflexivity_with_destruct_cases : others"
+ (tclTHEN (tclPROGRESS discr_inject)
+ (reflexivity_with_destruct_cases ())) ])
let prove_fun_complete funcs graphs schemes lemmas_types_infos i :
unit Proofview.tactic =
@@ -1062,130 +1072,143 @@ let prove_fun_complete funcs graphs schemes lemmas_types_infos i :
let open Tactics in
let open Tacticals.New in
Proofview.Goal.enter (fun g ->
- (* We compute the types of the different mutually recursive lemmas
- in $\zeta$ normal form
- *)
- let lemmas =
- Array.map
- (fun (_, (ctxt, concl)) ->
- Reductionops.nf_zeta (Proofview.Goal.env g) (Proofview.Goal.sigma g)
- (EConstr.it_mkLambda_or_LetIn concl ctxt))
- lemmas_types_infos
- in
- (* We get the constant and the principle corresponding to this lemma *)
- let f = funcs.(i) in
- let graph_principle =
- Reductionops.nf_zeta (Proofview.Goal.env g) (Proofview.Goal.sigma g)
- (EConstr.of_constr schemes.(i))
- in
- tclTYPEOFTHEN graph_principle (fun sigma princ_type ->
- let princ_infos = Tactics.compute_elim_sig sigma princ_type in
- (* Then we get the number of argument of the function
- and compute a fresh name for each of them
- *)
- let nb_fun_args = Termops.nb_prod sigma (Proofview.Goal.concl g) - 2 in
- let args_names = generate_fresh_id (Id.of_string "x") [] nb_fun_args in
- let ids = args_names @ pf_ids_of_hyps g in
- (* and fresh names for res H and the principle (cf bug bug #1174) *)
- let res, hres, graph_principle_id =
- match generate_fresh_id (Id.of_string "z") ids 3 with
- | [res; hres; graph_principle_id] -> (res, hres, graph_principle_id)
- | _ -> assert false
- in
- let ids = res :: hres :: graph_principle_id :: ids in
- (* we also compute fresh names for each hyptohesis of each branch
- of the principle *)
- let branches = List.rev princ_infos.branches in
- let intro_pats =
- List.map
- (fun decl ->
- List.map
- (fun id -> id)
- (generate_fresh_id (Id.of_string "y") ids
- (Termops.nb_prod (Proofview.Goal.sigma g) (RelDecl.get_type decl))))
- branches
- 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
- *)
- let rewrite_tac j ids : unit Proofview.tactic =
- let graph_def = graphs.(j) in
- let infos =
- match find_Function_infos (fst (destConst (Proofview.Goal.sigma g) funcs.(j))) with
- | None -> CErrors.user_err Pp.(str "No graph found")
- | Some infos -> infos
+ (* We compute the types of the different mutually recursive lemmas
+ in $\zeta$ normal form
+ *)
+ let lemmas =
+ Array.map
+ (fun (_, (ctxt, concl)) ->
+ Reductionops.nf_zeta (Proofview.Goal.env g) (Proofview.Goal.sigma g)
+ (EConstr.it_mkLambda_or_LetIn concl ctxt))
+ lemmas_types_infos
in
- if
- infos.is_general
- || Rtree.is_infinite Declareops.eq_recarg
- graph_def.Declarations.mind_recargs
- then
- let eq_lemma =
- try Option.get infos.equation_lemma
- with Option.IsNone ->
- CErrors.anomaly (Pp.str "Cannot find equation lemma.")
- in
- tclTHENLIST
- [ tclMAP Simple.intro ids
- ; Equality.rewriteLR (mkConst eq_lemma)
- ; (* Don't forget to $\zeta$ normlize the term since the principles
- have been $\zeta$-normalized *)
- reduce
- (Genredexpr.Cbv
- {Redops.all_flags with Genredexpr.rDelta = false})
- Locusops.onConcl
- ; generalize (List.map mkVar ids)
- ; thin ids ]
- else
- unfold_in_concl
- [ ( Locus.AllOccurrences
- , Names.EvalConstRef (fst (destConst (Proofview.Goal.sigma g) f)) ) ]
- in
- (* The proof of each branche itself *)
- let ind_number = ref 0 in
- let min_constr_number = ref 0 in
- let prove_branch i this_branche_ids =
- (* we fist compute the inductive corresponding to the branch *)
- let this_ind_number =
- let constructor_num = i - !min_constr_number in
- let length =
- Array.length graphs.(!ind_number).Declarations.mind_consnames
- in
- if constructor_num <= length then !ind_number
- else begin
- incr ind_number;
- min_constr_number := !min_constr_number + length;
- !ind_number
- end
+ (* We get the constant and the principle corresponding to this lemma *)
+ let f = funcs.(i) in
+ let graph_principle =
+ Reductionops.nf_zeta (Proofview.Goal.env g) (Proofview.Goal.sigma g)
+ (EConstr.of_constr schemes.(i))
in
- tclTHENLIST
- [ (* we expand the definition of the function *)
- observe_tac "rewrite_tac"
- (rewrite_tac this_ind_number this_branche_ids)
- ; (* introduce hypothesis with some rewrite *)
- observe_tac "intros_with_rewrite (all)" (intros_with_rewrite ())
- ; (* The proof is (almost) complete *)
- observe_tac "reflexivity" (reflexivity_with_destruct_cases ()) ]
- in
- let params_names = fst (List.chop princ_infos.nparams args_names) in
- let open EConstr in
- let params = List.map mkVar params_names in
- tclTHENLIST
- [ tclMAP Simple.intro (args_names @ [res; hres])
- ; observe_tac "h_generalize"
- (generalize
- [ mkApp
- ( applist (graph_principle, params)
- , Array.map (fun c -> applist (c, params)) lemmas ) ])
- ; Simple.intro graph_principle_id
- ; observe_tac ""
- (tclTHENS
- (observe_tac "elim"
- (elim false None
- (mkVar hres, Tactypes.NoBindings)
- (Some (mkVar graph_principle_id, Tactypes.NoBindings))))
- (List.map_i (fun i pat -> observe_tac "prove_branch" (prove_branch i pat)) 1 intro_pats)) ]))
+ tclTYPEOFTHEN graph_principle (fun sigma princ_type ->
+ let princ_infos = Tactics.compute_elim_sig sigma princ_type in
+ (* Then we get the number of argument of the function
+ and compute a fresh name for each of them
+ *)
+ let nb_fun_args =
+ Termops.nb_prod sigma (Proofview.Goal.concl g) - 2
+ in
+ let args_names =
+ generate_fresh_id (Id.of_string "x") [] nb_fun_args
+ in
+ let ids = args_names @ pf_ids_of_hyps g in
+ (* and fresh names for res H and the principle (cf bug bug #1174) *)
+ let res, hres, graph_principle_id =
+ match generate_fresh_id (Id.of_string "z") ids 3 with
+ | [res; hres; graph_principle_id] -> (res, hres, graph_principle_id)
+ | _ -> assert false
+ in
+ let ids = res :: hres :: graph_principle_id :: ids in
+ (* we also compute fresh names for each hyptohesis of each branch
+ of the principle *)
+ let branches = List.rev princ_infos.branches in
+ let intro_pats =
+ List.map
+ (fun decl ->
+ List.map
+ (fun id -> id)
+ (generate_fresh_id (Id.of_string "y") ids
+ (Termops.nb_prod (Proofview.Goal.sigma g)
+ (RelDecl.get_type decl))))
+ branches
+ 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
+ *)
+ let rewrite_tac j ids : unit Proofview.tactic =
+ let graph_def = graphs.(j) in
+ let infos =
+ match
+ find_Function_infos
+ (fst (destConst (Proofview.Goal.sigma g) funcs.(j)))
+ with
+ | None -> CErrors.user_err Pp.(str "No graph found")
+ | Some infos -> infos
+ in
+ if
+ infos.is_general
+ || Rtree.is_infinite Declareops.eq_recarg
+ graph_def.Declarations.mind_recargs
+ then
+ let eq_lemma =
+ try Option.get infos.equation_lemma
+ with Option.IsNone ->
+ CErrors.anomaly (Pp.str "Cannot find equation lemma.")
+ in
+ tclTHENLIST
+ [ tclMAP Simple.intro ids
+ ; Equality.rewriteLR (mkConst eq_lemma)
+ ; (* Don't forget to $\zeta$ normlize the term since the principles
+ have been $\zeta$-normalized *)
+ reduce
+ (Genredexpr.Cbv
+ {Redops.all_flags with Genredexpr.rDelta = false})
+ Locusops.onConcl
+ ; generalize (List.map mkVar ids)
+ ; thin ids ]
+ else
+ unfold_in_concl
+ [ ( Locus.AllOccurrences
+ , Names.EvalConstRef
+ (fst (destConst (Proofview.Goal.sigma g) f)) ) ]
+ in
+ (* The proof of each branche itself *)
+ let ind_number = ref 0 in
+ let min_constr_number = ref 0 in
+ let prove_branch i this_branche_ids =
+ (* we fist compute the inductive corresponding to the branch *)
+ let this_ind_number =
+ let constructor_num = i - !min_constr_number in
+ let length =
+ Array.length graphs.(!ind_number).Declarations.mind_consnames
+ in
+ if constructor_num <= length then !ind_number
+ else begin
+ incr ind_number;
+ min_constr_number := !min_constr_number + length;
+ !ind_number
+ end
+ in
+ tclTHENLIST
+ [ (* we expand the definition of the function *)
+ observe_tac "rewrite_tac"
+ (rewrite_tac this_ind_number this_branche_ids)
+ ; (* introduce hypothesis with some rewrite *)
+ observe_tac "intros_with_rewrite (all)" (intros_with_rewrite ())
+ ; (* The proof is (almost) complete *)
+ observe_tac "reflexivity" (reflexivity_with_destruct_cases ())
+ ]
+ in
+ let params_names = fst (List.chop princ_infos.nparams args_names) in
+ let open EConstr in
+ let params = List.map mkVar params_names in
+ tclTHENLIST
+ [ tclMAP Simple.intro (args_names @ [res; hres])
+ ; observe_tac "h_generalize"
+ (generalize
+ [ mkApp
+ ( applist (graph_principle, params)
+ , Array.map (fun c -> applist (c, params)) lemmas ) ])
+ ; Simple.intro graph_principle_id
+ ; observe_tac ""
+ (tclTHENS
+ (observe_tac "elim"
+ (elim false None
+ (mkVar hres, Tactypes.NoBindings)
+ (Some (mkVar graph_principle_id, Tactypes.NoBindings))))
+ (List.map_i
+ (fun i pat ->
+ observe_tac "prove_branch" (prove_branch i pat))
+ 1 intro_pats)) ]))
exception No_graph_found
@@ -1486,9 +1509,7 @@ let derive_correctness (funs : Constr.pconstant list) (graphs : inductive list)
let info = Declare.Info.make () in
let cinfo = Declare.CInfo.make ~name:lem_id ~typ () in
let lemma = Declare.Proof.start ~cinfo ~info !evd in
- let lemma =
- fst @@ Declare.Proof.by (proving_tac i) lemma
- in
+ let lemma = fst @@ Declare.Proof.by (proving_tac i) lemma in
let (_ : _ list) =
Declare.Proof.save_regular ~proof:lemma
~opaque:Vernacexpr.Transparent ~idopt:None
@@ -1555,9 +1576,9 @@ let derive_correctness (funs : Constr.pconstant list) (graphs : inductive list)
let lemma =
fst
(Declare.Proof.by
- (observe_tac
- ("prove completeness (" ^ Id.to_string f_id ^ ")")
- (proving_tac i))
+ (observe_tac
+ ("prove completeness (" ^ Id.to_string f_id ^ ")")
+ (proving_tac i))
lemma)
in
let (_ : _ list) =
diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml
index fadf0d0b3e..0179215d6a 100644
--- a/plugins/funind/indfun_common.ml
+++ b/plugins/funind/indfun_common.ml
@@ -394,9 +394,7 @@ let jmeq_refl () =
@@ Coqlib.lib_ref "core.JMeq.refl"
with e when CErrors.noncritical e -> raise (ToShow e)
-let h_intros l =
- Tacticals.New.tclMAP (fun x -> Tactics.Simple.intro x) l
-
+let h_intros l = Tacticals.New.tclMAP (fun x -> Tactics.Simple.intro x) l
let h_id = Id.of_string "h"
let hrec_id = Id.of_string "hrec"
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 90a8d82700..33076a876b 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -104,8 +104,9 @@ let next_ident_away_in_goal ids avoid =
next_ident_away_in_goal ids (Id.Set.of_list avoid)
let compute_renamed_type gls id =
- rename_bound_vars_as_displayed (Proofview.Goal.sigma gls) (*no avoid*) Id.Set.empty
- (*no rels*) [] (Tacmach.New.pf_get_hyp_typ id gls)
+ rename_bound_vars_as_displayed (Proofview.Goal.sigma gls)
+ (*no avoid*) Id.Set.empty (*no rels*) []
+ (Tacmach.New.pf_get_hyp_typ id gls)
let h'_id = Id.of_string "h'"
let teq_id = Id.of_string "teq"
@@ -361,7 +362,9 @@ type journey_info =
{ letiN : (Name.t * constr * types * constr, constr) journey_info_tac
; lambdA : (Name.t * types * constr, constr) journey_info_tac
; casE :
- ((constr infos -> unit Proofview.tactic) -> constr infos -> unit Proofview.tactic)
+ ( (constr infos -> unit Proofview.tactic)
+ -> constr infos
+ -> unit Proofview.tactic)
-> ( case_info
* constr
* (constr, EInstance.t) case_invert
@@ -382,131 +385,131 @@ let add_vars sigma forbidden e =
in
aux forbidden e
-let treat_case forbid_new_ids to_intros finalize_tac nb_lam e infos : unit Proofview.tactic =
+let treat_case forbid_new_ids to_intros finalize_tac nb_lam e infos :
+ unit Proofview.tactic =
Proofview.Goal.enter (fun g ->
- let rev_context, b = decompose_lam_n (Proofview.Goal.sigma g) nb_lam e in
- let ids =
- List.fold_left
- (fun acc (na, _) ->
- let pre_id =
- match na.binder_name with Name x -> x | Anonymous -> ano_id
- in
- pre_id :: acc)
- [] rev_context
- in
- let rev_ids = pf_get_new_ids (List.rev ids) g in
- let new_b = substl (List.map mkVar rev_ids) b in
- New.observe_tclTHENLIST
- (fun _ _ -> str "treat_case1")
- [ h_intros (List.rev rev_ids)
- ; intro_using_then teq_id (fun _ -> Proofview.tclUNIT ())
- ; Tacticals.New.onLastHypId (fun heq ->
- New.observe_tclTHENLIST
- (fun _ _ -> str "treat_case2")
- [ clear to_intros
- ; h_intros to_intros
- ; Proofview.Goal.enter (fun g' ->
- let sigma = Proofview.Goal.sigma g' in
- let ty_teq = Tacmach.New.pf_get_hyp_typ heq g' in
- let teq_lhs, teq_rhs =
- let _, args =
- try destApp sigma ty_teq
- with DestKO -> assert false
- in
- (args.(1), args.(2))
- in
- let new_b' =
- Termops.replace_term sigma teq_lhs teq_rhs new_b
- in
- let new_infos =
- { infos with
- info = new_b'
- ; eqs = heq :: infos.eqs
- ; forbidden_ids =
- ( if forbid_new_ids then
- add_vars sigma infos.forbidden_ids new_b'
- else infos.forbidden_ids ) }
- in
- finalize_tac new_infos) ]) ])
+ let rev_context, b = decompose_lam_n (Proofview.Goal.sigma g) nb_lam e in
+ let ids =
+ List.fold_left
+ (fun acc (na, _) ->
+ let pre_id =
+ match na.binder_name with Name x -> x | Anonymous -> ano_id
+ in
+ pre_id :: acc)
+ [] rev_context
+ in
+ let rev_ids = pf_get_new_ids (List.rev ids) g in
+ let new_b = substl (List.map mkVar rev_ids) b in
+ New.observe_tclTHENLIST
+ (fun _ _ -> str "treat_case1")
+ [ h_intros (List.rev rev_ids)
+ ; intro_using_then teq_id (fun _ -> Proofview.tclUNIT ())
+ ; Tacticals.New.onLastHypId (fun heq ->
+ New.observe_tclTHENLIST
+ (fun _ _ -> str "treat_case2")
+ [ clear to_intros
+ ; h_intros to_intros
+ ; Proofview.Goal.enter (fun g' ->
+ let sigma = Proofview.Goal.sigma g' in
+ let ty_teq = Tacmach.New.pf_get_hyp_typ heq g' in
+ let teq_lhs, teq_rhs =
+ let _, args =
+ try destApp sigma ty_teq with DestKO -> assert false
+ in
+ (args.(1), args.(2))
+ in
+ let new_b' =
+ Termops.replace_term sigma teq_lhs teq_rhs new_b
+ in
+ let new_infos =
+ { infos with
+ info = new_b'
+ ; eqs = heq :: infos.eqs
+ ; forbidden_ids =
+ ( if forbid_new_ids then
+ add_vars sigma infos.forbidden_ids new_b'
+ else infos.forbidden_ids ) }
+ in
+ finalize_tac new_infos) ]) ])
let rec travel_aux jinfo continuation_tac (expr_info : constr infos) =
Proofview.Goal.enter (fun g ->
- let sigma = Proofview.Goal.sigma g in
- let env = Proofview.Goal.env g in
- match EConstr.kind sigma expr_info.info with
- | CoFix _ | Fix _ ->
- user_err Pp.(str "Function cannot treat local fixpoint or cofixpoint")
- | Array _ -> user_err Pp.(str "Function cannot treat arrays")
- | Proj _ -> user_err Pp.(str "Function cannot treat projections")
- | LetIn (na, b, t, e) ->
- let new_continuation_tac =
- jinfo.letiN (na.binder_name, b, t, e) expr_info continuation_tac
- in
- travel jinfo new_continuation_tac
- {expr_info with info = b; is_final = false}
- | Rel _ -> anomaly (Pp.str "Free var in goal conclusion!")
- | Prod _ -> (
- try
- check_not_nested env sigma
- (expr_info.f_id :: expr_info.forbidden_ids)
- expr_info.info;
- jinfo.otherS () expr_info continuation_tac expr_info
- with e when CErrors.noncritical e ->
- user_err ~hdr:"Recdef.travel"
- ( str "the term "
- ++ Printer.pr_leconstr_env env sigma expr_info.info
- ++ str " can not contain a recursive call to "
- ++ Id.print expr_info.f_id ) )
- | Lambda (n, t, b) -> (
- try
- check_not_nested env sigma
- (expr_info.f_id :: expr_info.forbidden_ids)
- expr_info.info;
- jinfo.otherS () expr_info continuation_tac expr_info
- with e when CErrors.noncritical e ->
- user_err ~hdr:"Recdef.travel"
- ( str "the term "
- ++ Printer.pr_leconstr_env env sigma expr_info.info
- ++ str " can not contain a recursive call to "
- ++ Id.print expr_info.f_id ) )
- | Case (ci, t, iv, a, l) ->
- let continuation_tac_a =
- jinfo.casE (travel jinfo) (ci, t, iv, a, l) expr_info continuation_tac
- in
- travel jinfo continuation_tac_a
- {expr_info with info = a; is_main_branch = false; is_final = false}
- | App _ -> (
- let f, args = decompose_app sigma expr_info.info in
- if EConstr.eq_constr sigma f expr_info.f_constr then
- jinfo.app_reC (f, args) expr_info continuation_tac expr_info
- else
- match EConstr.kind sigma f with
- | App _ -> assert false (* f is coming from a decompose_app *)
- | Const _ | Construct _ | Rel _ | Evar _ | Meta _ | Ind _ | Sort _
- |Prod _ | Var _ ->
- let new_infos = {expr_info with info = (f, args)} in
+ let sigma = Proofview.Goal.sigma g in
+ let env = Proofview.Goal.env g in
+ match EConstr.kind sigma expr_info.info with
+ | CoFix _ | Fix _ ->
+ user_err Pp.(str "Function cannot treat local fixpoint or cofixpoint")
+ | Array _ -> user_err Pp.(str "Function cannot treat arrays")
+ | Proj _ -> user_err Pp.(str "Function cannot treat projections")
+ | LetIn (na, b, t, e) ->
let new_continuation_tac =
- jinfo.apP (f, args) expr_info continuation_tac
+ jinfo.letiN (na.binder_name, b, t, e) expr_info continuation_tac
in
- travel_args jinfo expr_info.is_main_branch new_continuation_tac
- new_infos
- | Case _ ->
- user_err ~hdr:"Recdef.travel"
- ( str "the term "
- ++ Printer.pr_leconstr_env env sigma expr_info.info
- ++ str
- " can not contain an applied match (See Limitation in Section \
- 2.3 of refman)" )
- | _ ->
- anomaly
- ( Pp.str "travel_aux : unexpected "
- ++ Printer.pr_leconstr_env env sigma expr_info.info
- ++ Pp.str "." ) )
- | Cast (t, _, _) -> travel jinfo continuation_tac {expr_info with info = t}
- | Const _ | Var _ | Meta _ | Evar _ | Sort _ | Construct _ | Ind _ | Int _
- |Float _ ->
- let new_continuation_tac = jinfo.otherS () expr_info continuation_tac in
- new_continuation_tac expr_info)
+ travel jinfo new_continuation_tac
+ {expr_info with info = b; is_final = false}
+ | Rel _ -> anomaly (Pp.str "Free var in goal conclusion!")
+ | Prod _ -> (
+ try
+ check_not_nested env sigma
+ (expr_info.f_id :: expr_info.forbidden_ids)
+ expr_info.info;
+ jinfo.otherS () expr_info continuation_tac expr_info
+ with e when CErrors.noncritical e ->
+ user_err ~hdr:"Recdef.travel"
+ ( str "the term "
+ ++ Printer.pr_leconstr_env env sigma expr_info.info
+ ++ str " can not contain a recursive call to "
+ ++ Id.print expr_info.f_id ) )
+ | Lambda (n, t, b) -> (
+ try
+ check_not_nested env sigma
+ (expr_info.f_id :: expr_info.forbidden_ids)
+ expr_info.info;
+ jinfo.otherS () expr_info continuation_tac expr_info
+ with e when CErrors.noncritical e ->
+ user_err ~hdr:"Recdef.travel"
+ ( str "the term "
+ ++ Printer.pr_leconstr_env env sigma expr_info.info
+ ++ str " can not contain a recursive call to "
+ ++ Id.print expr_info.f_id ) )
+ | Case (ci, t, iv, a, l) ->
+ let continuation_tac_a =
+ jinfo.casE (travel jinfo) (ci, t, iv, a, l) expr_info continuation_tac
+ in
+ travel jinfo continuation_tac_a
+ {expr_info with info = a; is_main_branch = false; is_final = false}
+ | App _ -> (
+ let f, args = decompose_app sigma expr_info.info in
+ if EConstr.eq_constr sigma f expr_info.f_constr then
+ jinfo.app_reC (f, args) expr_info continuation_tac expr_info
+ else
+ match EConstr.kind sigma f with
+ | App _ -> assert false (* f is coming from a decompose_app *)
+ | Const _ | Construct _ | Rel _ | Evar _ | Meta _ | Ind _ | Sort _
+ |Prod _ | Var _ ->
+ let new_infos = {expr_info with info = (f, args)} in
+ let new_continuation_tac =
+ jinfo.apP (f, args) expr_info continuation_tac
+ in
+ travel_args jinfo expr_info.is_main_branch new_continuation_tac
+ new_infos
+ | Case _ ->
+ user_err ~hdr:"Recdef.travel"
+ ( str "the term "
+ ++ Printer.pr_leconstr_env env sigma expr_info.info
+ ++ str
+ " can not contain an applied match (See Limitation in \
+ Section 2.3 of refman)" )
+ | _ ->
+ anomaly
+ ( Pp.str "travel_aux : unexpected "
+ ++ Printer.pr_leconstr_env env sigma expr_info.info
+ ++ Pp.str "." ) )
+ | Cast (t, _, _) -> travel jinfo continuation_tac {expr_info with info = t}
+ | Const _ | Var _ | Meta _ | Evar _ | Sort _ | Construct _ | Ind _
+ |Int _ | Float _ ->
+ let new_continuation_tac = jinfo.otherS () expr_info continuation_tac in
+ new_continuation_tac expr_info)
and travel_args jinfo is_final continuation_tac infos =
let f_args', args = infos.info in
@@ -530,121 +533,122 @@ and travel jinfo continuation_tac expr_info =
let rec prove_lt hyple =
Proofview.Goal.enter (fun g ->
- let sigma = Proofview.Goal.sigma g in
- begin
- try
- let varx, varz =
- match decompose_app sigma (Proofview.Goal.concl g) with
- | _, x :: z :: _ when isVar sigma x && isVar sigma z -> (x, z)
- | _ -> assert false
- in
- let h =
- List.find
- (fun id ->
- match decompose_app sigma (Tacmach.New.pf_get_hyp_typ id g) with
- | _, t :: _ -> EConstr.eq_constr sigma t varx
- | _ -> false)
- hyple
- in
- let y =
- List.hd (List.tl (snd (decompose_app sigma (Tacmach.New.pf_get_hyp_typ h g))))
- in
- New.observe_tclTHENLIST
- (fun _ _ -> str "prove_lt1")
- [ apply (mkApp (le_lt_trans (), [|varx; y; varz; mkVar h|]))
- ; New.observe_tac (fun _ _ -> str "prove_lt") (prove_lt hyple) ]
- with Not_found ->
- New.observe_tclTHENLIST
- (fun _ _ -> str "prove_lt2")
- [ apply (delayed_force lt_S_n)
- ; New.observe_tac
- (fun _ _ -> str "assumption: " ++ Printer.pr_goal Evd.{it = Proofview.Goal.goal g; sigma})
- assumption ]
- end)
+ let sigma = Proofview.Goal.sigma g in
+ try
+ let varx, varz =
+ match decompose_app sigma (Proofview.Goal.concl g) with
+ | _, x :: z :: _ when isVar sigma x && isVar sigma z -> (x, z)
+ | _ -> assert false
+ in
+ let h =
+ List.find
+ (fun id ->
+ match decompose_app sigma (Tacmach.New.pf_get_hyp_typ id g) with
+ | _, t :: _ -> EConstr.eq_constr sigma t varx
+ | _ -> false)
+ hyple
+ in
+ let y =
+ List.hd
+ (List.tl
+ (snd (decompose_app sigma (Tacmach.New.pf_get_hyp_typ h g))))
+ in
+ New.observe_tclTHENLIST
+ (fun _ _ -> str "prove_lt1")
+ [ apply (mkApp (le_lt_trans (), [|varx; y; varz; mkVar h|]))
+ ; New.observe_tac (fun _ _ -> str "prove_lt") (prove_lt hyple) ]
+ with Not_found ->
+ New.observe_tclTHENLIST
+ (fun _ _ -> str "prove_lt2")
+ [ apply (delayed_force lt_S_n)
+ ; New.observe_tac
+ (fun _ _ ->
+ str "assumption: "
+ ++ Printer.pr_goal Evd.{it = Proofview.Goal.goal g; sigma})
+ assumption ])
let rec destruct_bounds_aux infos (bound, hyple, rechyps) lbounds =
let open Tacticals.New in
Proofview.Goal.enter (fun g ->
- match lbounds with
- | [] ->
- let ids = Tacmach.New.pf_ids_of_hyps g in
- let s_max = mkApp (delayed_force coq_S, [|bound|]) in
- let k = next_ident_away_in_goal k_id ids in
- let ids = k :: ids in
- let h' = next_ident_away_in_goal h'_id ids in
- let ids = h' :: ids in
- let def = next_ident_away_in_goal def_id ids in
- New.observe_tclTHENLIST
- (fun _ _ -> str "destruct_bounds_aux1")
- [ split (ImplicitBindings [s_max])
- ; intro_then (fun id ->
- (New.observe_tac
- (fun _ _ -> str "destruct_bounds_aux")
- (tclTHENS
- (simplest_case (mkVar id))
- [ New.observe_tclTHENLIST
- (fun _ _ -> str "")
- [ intro_using_then h_id
- (* We don't care about the refreshed name,
- accessed only through auto? *)
- (fun _ -> Proofview.tclUNIT ())
- ; simplest_elim
- (mkApp (delayed_force lt_n_O, [|s_max|]))
- ; default_full_auto ]
- ; New.observe_tclTHENLIST
- (fun _ _ -> str "destruct_bounds_aux2")
- [ New.observe_tac
- (fun _ _ -> str "clearing k ")
- (clear [id])
- ; h_intros [k; h'; def]
- ; New.observe_tac
- (fun _ _ -> str "simple_iter")
- (simpl_iter Locusops.onConcl)
- ; New.observe_tac
- (fun _ _ -> str "unfold functional")
- (unfold_in_concl
- [ ( Locus.OnlyOccurrences [1]
- , evaluable_of_global_reference
- infos.func ) ])
- ; New.observe_tclTHENLIST
- (fun _ _ -> str "test")
- [ list_rewrite true
- (List.fold_right
- (fun e acc -> (mkVar e, true) :: acc)
- infos.eqs
- (List.map (fun e -> (e, true)) rechyps))
- ; (* list_rewrite true *)
- (* (List.map (fun e -> (mkVar e,true)) infos.eqs) *)
- (* ; *)
- New.observe_tac
- (fun _ _ -> str "finishing")
- (tclORELSE
- intros_reflexivity
- (New.observe_tac
- (fun _ _ -> str "calling prove_lt")
- (prove_lt hyple))) ] ] ]))) ]
- | (_, v_bound) :: l ->
- New.observe_tclTHENLIST
- (fun _ _ -> str "destruct_bounds_aux3")
- [ simplest_elim (mkVar v_bound)
- ; clear [v_bound]
- ; tclDO 2 intro
- ; onNthHypId 1 (fun p_hyp ->
- onNthHypId 2 (fun p ->
- New.observe_tclTHENLIST
- (fun _ _ -> str "destruct_bounds_aux4")
- [ simplest_elim
- (mkApp (delayed_force max_constr, [|bound; mkVar p|]))
- ; tclDO 3 intro
- ; onNLastHypsId 3 (fun lids ->
- match lids with
- | [hle2; hle1; pmax] ->
- destruct_bounds_aux infos
- ( mkVar pmax
- , hle1 :: hle2 :: hyple
- , mkVar p_hyp :: rechyps )
- l
- | _ -> assert false) ])) ])
+ match lbounds with
+ | [] ->
+ let ids = Tacmach.New.pf_ids_of_hyps g in
+ let s_max = mkApp (delayed_force coq_S, [|bound|]) in
+ let k = next_ident_away_in_goal k_id ids in
+ let ids = k :: ids in
+ let h' = next_ident_away_in_goal h'_id ids in
+ let ids = h' :: ids in
+ let def = next_ident_away_in_goal def_id ids in
+ New.observe_tclTHENLIST
+ (fun _ _ -> str "destruct_bounds_aux1")
+ [ split (ImplicitBindings [s_max])
+ ; intro_then (fun id ->
+ New.observe_tac
+ (fun _ _ -> str "destruct_bounds_aux")
+ (tclTHENS
+ (simplest_case (mkVar id))
+ [ New.observe_tclTHENLIST
+ (fun _ _ -> str "")
+ [ intro_using_then h_id
+ (* We don't care about the refreshed name,
+ accessed only through auto? *)
+ (fun _ -> Proofview.tclUNIT ())
+ ; simplest_elim
+ (mkApp (delayed_force lt_n_O, [|s_max|]))
+ ; default_full_auto ]
+ ; New.observe_tclTHENLIST
+ (fun _ _ -> str "destruct_bounds_aux2")
+ [ New.observe_tac
+ (fun _ _ -> str "clearing k ")
+ (clear [id])
+ ; h_intros [k; h'; def]
+ ; New.observe_tac
+ (fun _ _ -> str "simple_iter")
+ (simpl_iter Locusops.onConcl)
+ ; New.observe_tac
+ (fun _ _ -> str "unfold functional")
+ (unfold_in_concl
+ [ ( Locus.OnlyOccurrences [1]
+ , evaluable_of_global_reference infos.func )
+ ])
+ ; New.observe_tclTHENLIST
+ (fun _ _ -> str "test")
+ [ list_rewrite true
+ (List.fold_right
+ (fun e acc -> (mkVar e, true) :: acc)
+ infos.eqs
+ (List.map (fun e -> (e, true)) rechyps))
+ ; (* list_rewrite true *)
+ (* (List.map (fun e -> (mkVar e,true)) infos.eqs) *)
+ (* ; *)
+ New.observe_tac
+ (fun _ _ -> str "finishing")
+ (tclORELSE intros_reflexivity
+ (New.observe_tac
+ (fun _ _ -> str "calling prove_lt")
+ (prove_lt hyple))) ] ] ])) ]
+ | (_, v_bound) :: l ->
+ New.observe_tclTHENLIST
+ (fun _ _ -> str "destruct_bounds_aux3")
+ [ simplest_elim (mkVar v_bound)
+ ; clear [v_bound]
+ ; tclDO 2 intro
+ ; onNthHypId 1 (fun p_hyp ->
+ onNthHypId 2 (fun p ->
+ New.observe_tclTHENLIST
+ (fun _ _ -> str "destruct_bounds_aux4")
+ [ simplest_elim
+ (mkApp (delayed_force max_constr, [|bound; mkVar p|]))
+ ; tclDO 3 intro
+ ; onNLastHypsId 3 (fun lids ->
+ match lids with
+ | [hle2; hle1; pmax] ->
+ destruct_bounds_aux infos
+ ( mkVar pmax
+ , hle1 :: hle2 :: hyple
+ , mkVar p_hyp :: rechyps )
+ l
+ | _ -> assert false) ])) ])
let destruct_bounds infos =
destruct_bounds_aux infos
@@ -672,29 +676,32 @@ let terminate_others _ expr_info continuation_tac infos =
; New.observe_tac
(fun _ _ -> str "first split")
(split (ImplicitBindings [infos.info]))
- ; New.observe_tac (fun _ _ -> str "destruct_bounds") (destruct_bounds infos)
- ]
+ ; New.observe_tac
+ (fun _ _ -> str "destruct_bounds")
+ (destruct_bounds infos) ]
else continuation_tac infos
let terminate_letin (na, b, t, e) expr_info continuation_tac info =
Proofview.Goal.enter (fun g ->
- let sigma = Proofview.Goal.sigma g in
- let env = Proofview.Goal.env g in
- let new_e = subst1 info.info e in
- let new_forbidden =
- let forbid =
- try
- check_not_nested env sigma (expr_info.f_id :: expr_info.forbidden_ids) b;
- true
- with e when CErrors.noncritical e -> false
- in
- if forbid then
- match na with
- | Anonymous -> info.forbidden_ids
- | Name id -> id :: info.forbidden_ids
- else info.forbidden_ids
- in
- continuation_tac {info with info = new_e; forbidden_ids = new_forbidden})
+ let sigma = Proofview.Goal.sigma g in
+ let env = Proofview.Goal.env g in
+ let new_e = subst1 info.info e in
+ let new_forbidden =
+ let forbid =
+ try
+ check_not_nested env sigma
+ (expr_info.f_id :: expr_info.forbidden_ids)
+ b;
+ true
+ with e when CErrors.noncritical e -> false
+ in
+ if forbid then
+ match na with
+ | Anonymous -> info.forbidden_ids
+ | Name id -> id :: info.forbidden_ids
+ else info.forbidden_ids
+ in
+ continuation_tac {info with info = new_e; forbidden_ids = new_forbidden})
let pf_type c tac =
let open Tacticals.New in
@@ -742,149 +749,153 @@ let mkDestructEq not_on_hyp env sigma expr =
(fun _ _ -> str "mkDestructEq")
[ generalize new_hyps
; Proofview.Goal.enter (fun g2 ->
- let changefun patvars env sigma =
- pattern_occs
- [(Locus.AllOccurrencesBut [1], expr)]
- (Proofview.Goal.env g2) sigma (Proofview.Goal.concl g2)
- in
- change_in_concl ~check:true None changefun)
+ let changefun patvars env sigma =
+ pattern_occs
+ [(Locus.AllOccurrencesBut [1], expr)]
+ (Proofview.Goal.env g2) sigma (Proofview.Goal.concl g2)
+ in
+ change_in_concl ~check:true None changefun)
; simplest_case expr ])
in
(sigma, tac, to_revert)
-let terminate_case next_step (ci, a, iv, t, l) expr_info continuation_tac infos =
+let terminate_case next_step (ci, a, iv, t, l) expr_info continuation_tac infos
+ =
let open Tacticals.New in
Proofview.Goal.enter (fun g ->
- let sigma = Proofview.Goal.sigma g in
- let env = Proofview.Goal.env g in
- let f_is_present =
- try
- check_not_nested env sigma (expr_info.f_id :: expr_info.forbidden_ids) a;
- false
- with e when CErrors.noncritical e -> true
- in
- let a' = infos.info in
- let new_info =
- { infos with
- info = mkCase (ci, t, iv, a', l)
- ; is_main_branch = expr_info.is_main_branch
- ; is_final = expr_info.is_final }
- in
- let sigma, destruct_tac, rev_to_thin_intro =
- mkDestructEq [expr_info.rec_arg_id] env sigma a'
- in
- let to_thin_intro = List.rev rev_to_thin_intro in
- New.observe_tac
- (fun _ _ ->
- str "treating cases ("
- ++ int (Array.length l)
- ++ str ")" ++ spc ()
- ++ Printer.pr_leconstr_env env sigma a')
- ( try
- tclTHENS destruct_tac
- (List.map_i
- (fun i e ->
- New.observe_tac
- (fun _ _ -> str "do treat case")
- (treat_case f_is_present to_thin_intro
- (next_step continuation_tac)
- ci.ci_cstr_ndecls.(i) e new_info))
- 0 (Array.to_list l))
- with
- | UserError (Some "Refiner.thensn_tac3", _)
- |UserError (Some "Refiner.tclFAIL_s", _)
- ->
- New.observe_tac
- (fun _ _ ->
- str "is computable "
- ++ Printer.pr_leconstr_env env sigma new_info.info)
- (next_step continuation_tac
- { new_info with
- info =
- Reductionops.nf_betaiotazeta env sigma new_info.info })
- ))
+ let sigma = Proofview.Goal.sigma g in
+ let env = Proofview.Goal.env g in
+ let f_is_present =
+ try
+ check_not_nested env sigma
+ (expr_info.f_id :: expr_info.forbidden_ids)
+ a;
+ false
+ with e when CErrors.noncritical e -> true
+ in
+ let a' = infos.info in
+ let new_info =
+ { infos with
+ info = mkCase (ci, t, iv, a', l)
+ ; is_main_branch = expr_info.is_main_branch
+ ; is_final = expr_info.is_final }
+ in
+ let sigma, destruct_tac, rev_to_thin_intro =
+ mkDestructEq [expr_info.rec_arg_id] env sigma a'
+ in
+ let to_thin_intro = List.rev rev_to_thin_intro in
+ New.observe_tac
+ (fun _ _ ->
+ str "treating cases ("
+ ++ int (Array.length l)
+ ++ str ")" ++ spc ()
+ ++ Printer.pr_leconstr_env env sigma a')
+ ( try
+ tclTHENS destruct_tac
+ (List.map_i
+ (fun i e ->
+ New.observe_tac
+ (fun _ _ -> str "do treat case")
+ (treat_case f_is_present to_thin_intro
+ (next_step continuation_tac)
+ ci.ci_cstr_ndecls.(i) e new_info))
+ 0 (Array.to_list l))
+ with
+ | UserError (Some "Refiner.thensn_tac3", _)
+ |UserError (Some "Refiner.tclFAIL_s", _)
+ ->
+ New.observe_tac
+ (fun _ _ ->
+ str "is computable "
+ ++ Printer.pr_leconstr_env env sigma new_info.info)
+ (next_step continuation_tac
+ { new_info with
+ info = Reductionops.nf_betaiotazeta env sigma new_info.info
+ }) ))
let terminate_app_rec (f, args) expr_info continuation_tac _ =
let open Tacticals.New in
Proofview.Goal.enter (fun g ->
- let sigma = Proofview.Goal.sigma g in
- let env = Proofview.Goal.env g in
- List.iter
- (check_not_nested env sigma (expr_info.f_id :: expr_info.forbidden_ids))
- args;
- try
- let v =
- List.assoc_f
- (List.equal (EConstr.eq_constr sigma))
- args expr_info.args_assoc
- in
- let new_infos = {expr_info with info = v} in
- New.observe_tclTHENLIST
- (fun _ _ -> str "terminate_app_rec")
- [ continuation_tac new_infos
- ; ( if expr_info.is_final && expr_info.is_main_branch then
- New.observe_tclTHENLIST
- (fun _ _ -> str "terminate_app_rec1")
- [ New.observe_tac
- (fun _ _ -> str "first split")
- (split (ImplicitBindings [new_infos.info]))
- ; New.observe_tac
- (fun _ _ -> str "destruct_bounds (3)")
- (destruct_bounds new_infos) ]
- else Proofview.tclUNIT () ) ]
- with Not_found ->
- New.observe_tac
- (fun _ _ -> str "terminate_app_rec not found")
- (tclTHENS
- (simplest_elim (mkApp (mkVar expr_info.ih, Array.of_list args)))
- [ New.observe_tclTHENLIST
- (fun _ _ -> str "terminate_app_rec2")
- [ intro_using_then rec_res_id
- (* refreshed name gotten from onNthHypId *)
- (fun _ -> Proofview.tclUNIT ())
- ; intro
- ; onNthHypId 1 (fun v_bound ->
- onNthHypId 2 (fun v ->
- let new_infos =
- { expr_info with
- info = mkVar v
- ; values_and_bounds =
- (v, v_bound) :: expr_info.values_and_bounds
- ; args_assoc = (args, mkVar v) :: expr_info.args_assoc
- }
- in
- New.observe_tclTHENLIST
- (fun _ _ -> str "terminate_app_rec3")
- [ continuation_tac new_infos
- ; ( if expr_info.is_final && expr_info.is_main_branch
- then
- New.observe_tclTHENLIST
- (fun _ _ -> str "terminate_app_rec4")
- [ New.observe_tac
- (fun _ _ -> str "first split")
- (split (ImplicitBindings [new_infos.info]))
- ; New.observe_tac
- (fun _ _ -> str "destruct_bounds (2)")
- (destruct_bounds new_infos) ]
- else Proofview.tclUNIT () ) ])) ]
- ; New.observe_tac
- (fun _ _ -> str "proving decreasing")
- (tclTHENS (* proof of args < formal args *)
- (apply (Lazy.force expr_info.acc_inv))
+ let sigma = Proofview.Goal.sigma g in
+ let env = Proofview.Goal.env g in
+ List.iter
+ (check_not_nested env sigma (expr_info.f_id :: expr_info.forbidden_ids))
+ args;
+ try
+ let v =
+ List.assoc_f
+ (List.equal (EConstr.eq_constr sigma))
+ args expr_info.args_assoc
+ in
+ let new_infos = {expr_info with info = v} in
+ New.observe_tclTHENLIST
+ (fun _ _ -> str "terminate_app_rec")
+ [ continuation_tac new_infos
+ ; ( if expr_info.is_final && expr_info.is_main_branch then
+ New.observe_tclTHENLIST
+ (fun _ _ -> str "terminate_app_rec1")
[ New.observe_tac
- (fun _ _ -> str "assumption")
- assumption
- ; New.observe_tclTHENLIST
- (fun _ _ -> str "terminate_app_rec5")
- [ tclTRY
- (list_rewrite true
- (List.map (fun e -> (mkVar e, true)) expr_info.eqs))
- ; tclUSER expr_info.concl_tac true
- (Some
- ( expr_info.ih :: expr_info.acc_id
- :: (fun (x, y) -> y)
- (List.split expr_info.values_and_bounds) ))
- ] ]) ]))
+ (fun _ _ -> str "first split")
+ (split (ImplicitBindings [new_infos.info]))
+ ; New.observe_tac
+ (fun _ _ -> str "destruct_bounds (3)")
+ (destruct_bounds new_infos) ]
+ else Proofview.tclUNIT () ) ]
+ with Not_found ->
+ New.observe_tac
+ (fun _ _ -> str "terminate_app_rec not found")
+ (tclTHENS
+ (simplest_elim (mkApp (mkVar expr_info.ih, Array.of_list args)))
+ [ New.observe_tclTHENLIST
+ (fun _ _ -> str "terminate_app_rec2")
+ [ intro_using_then rec_res_id
+ (* refreshed name gotten from onNthHypId *)
+ (fun _ -> Proofview.tclUNIT ())
+ ; intro
+ ; onNthHypId 1 (fun v_bound ->
+ onNthHypId 2 (fun v ->
+ let new_infos =
+ { expr_info with
+ info = mkVar v
+ ; values_and_bounds =
+ (v, v_bound) :: expr_info.values_and_bounds
+ ; args_assoc =
+ (args, mkVar v) :: expr_info.args_assoc }
+ in
+ New.observe_tclTHENLIST
+ (fun _ _ -> str "terminate_app_rec3")
+ [ continuation_tac new_infos
+ ; ( if
+ expr_info.is_final && expr_info.is_main_branch
+ then
+ New.observe_tclTHENLIST
+ (fun _ _ -> str "terminate_app_rec4")
+ [ New.observe_tac
+ (fun _ _ -> str "first split")
+ (split
+ (ImplicitBindings [new_infos.info]))
+ ; New.observe_tac
+ (fun _ _ -> str "destruct_bounds (2)")
+ (destruct_bounds new_infos) ]
+ else Proofview.tclUNIT () ) ])) ]
+ ; New.observe_tac
+ (fun _ _ -> str "proving decreasing")
+ (tclTHENS (* proof of args < formal args *)
+ (apply (Lazy.force expr_info.acc_inv))
+ [ New.observe_tac (fun _ _ -> str "assumption") assumption
+ ; New.observe_tclTHENLIST
+ (fun _ _ -> str "terminate_app_rec5")
+ [ tclTRY
+ (list_rewrite true
+ (List.map
+ (fun e -> (mkVar e, true))
+ expr_info.eqs))
+ ; tclUSER expr_info.concl_tac true
+ (Some
+ ( expr_info.ih :: expr_info.acc_id
+ :: (fun (x, y) -> y)
+ (List.split expr_info.values_and_bounds) ))
+ ] ]) ]))
let terminate_info =
{ message = "prove_terminate with term "
@@ -907,37 +918,41 @@ let equation_case next_step case expr_info continuation_tac infos =
let rec prove_le () =
let open Tacticals.New in
Proofview.Goal.enter (fun g ->
- let sigma = Proofview.Goal.sigma g in
- let x, z =
- let _, args = decompose_app sigma (Proofview.Goal.concl g) in
- (List.hd args, List.hd (List.tl args))
- in
- tclFIRST
- [ assumption
- ; apply (delayed_force le_n)
- ; begin
- try
- let matching_fun c =
- match EConstr.kind sigma c with
- | App (c, [|x0; _|]) ->
- EConstr.isVar sigma x0
- && Id.equal (destVar sigma x0) (destVar sigma x)
- && EConstr.isRefX sigma (le ()) c
- | _ -> false
- in
- let h, t =
- List.find (fun (_, t) -> matching_fun t) (Tacmach.New.pf_hyps_types g)
- in
- let y =
- let _, args = decompose_app sigma t in
- List.hd (List.tl args)
- in
- New.observe_tclTHENLIST
- (fun _ _ -> str "prove_le")
- [ apply (mkApp (le_trans (), [|x; y; z; mkVar h|]))
- ; New.observe_tac (fun _ _ -> str "prove_le (rec)") (prove_le ()) ]
- with Not_found -> Tacticals.New.tclFAIL 0 (mt ())
- end ])
+ let sigma = Proofview.Goal.sigma g in
+ let x, z =
+ let _, args = decompose_app sigma (Proofview.Goal.concl g) in
+ (List.hd args, List.hd (List.tl args))
+ in
+ tclFIRST
+ [ assumption
+ ; apply (delayed_force le_n)
+ ; begin
+ try
+ let matching_fun c =
+ match EConstr.kind sigma c with
+ | App (c, [|x0; _|]) ->
+ EConstr.isVar sigma x0
+ && Id.equal (destVar sigma x0) (destVar sigma x)
+ && EConstr.isRefX sigma (le ()) c
+ | _ -> false
+ in
+ let h, t =
+ List.find
+ (fun (_, t) -> matching_fun t)
+ (Tacmach.New.pf_hyps_types g)
+ in
+ let y =
+ let _, args = decompose_app sigma t in
+ List.hd (List.tl args)
+ in
+ New.observe_tclTHENLIST
+ (fun _ _ -> str "prove_le")
+ [ apply (mkApp (le_trans (), [|x; y; z; mkVar h|]))
+ ; New.observe_tac
+ (fun _ _ -> str "prove_le (rec)")
+ (prove_le ()) ]
+ with Not_found -> Tacticals.New.tclFAIL 0 (mt ())
+ end ])
let rec make_rewrite_list expr_info max = function
| [] -> Proofview.tclUNIT ()
@@ -949,16 +964,16 @@ let rec make_rewrite_list expr_info max = function
(New.observe_tac
(fun _ _ -> str "rewrite heq on " ++ Id.print p)
(Proofview.Goal.enter (fun g ->
- let sigma = Proofview.Goal.sigma g in
- let t_eq = compute_renamed_type g hp in
- let k, def =
- let k_na, _, t = destProd sigma t_eq in
- let _, _, t = destProd sigma t in
- let def_na, _, _ = destProd sigma t in
- ( Nameops.Name.get_id k_na.binder_name
- , Nameops.Name.get_id def_na.binder_name )
- in
- general_rewrite_bindings false Locus.AllOccurrences true
+ let sigma = Proofview.Goal.sigma g in
+ let t_eq = compute_renamed_type g hp in
+ let k, def =
+ let k_na, _, t = destProd sigma t_eq in
+ let _, _, t = destProd sigma t in
+ let def_na, _, _ = destProd sigma t in
+ ( Nameops.Name.get_id k_na.binder_name
+ , Nameops.Name.get_id def_na.binder_name )
+ in
+ general_rewrite_bindings false Locus.AllOccurrences true
(* dep proofs also: *) true
( mkVar hp
, ExplicitBindings
@@ -982,18 +997,18 @@ let make_rewrite expr_info l hp max =
(fun _ _ -> str "make_rewrite")
(tclTHENS
(Proofview.Goal.enter (fun g ->
- let sigma = Proofview.Goal.sigma g in
- let t_eq = compute_renamed_type g hp in
- let k, def =
- let k_na, _, t = destProd sigma t_eq in
- let _, _, t = destProd sigma t in
- let def_na, _, _ = destProd sigma t in
- ( Nameops.Name.get_id k_na.binder_name
- , Nameops.Name.get_id def_na.binder_name )
- in
- New.observe_tac
- (fun _ _ -> str "general_rewrite_bindings")
- (general_rewrite_bindings false Locus.AllOccurrences true
+ let sigma = Proofview.Goal.sigma g in
+ let t_eq = compute_renamed_type g hp in
+ let k, def =
+ let k_na, _, t = destProd sigma t_eq in
+ let _, _, t = destProd sigma t in
+ let def_na, _, _ = destProd sigma t in
+ ( Nameops.Name.get_id k_na.binder_name
+ , Nameops.Name.get_id def_na.binder_name )
+ in
+ New.observe_tac
+ (fun _ _ -> str "general_rewrite_bindings")
+ (general_rewrite_bindings false Locus.AllOccurrences true
(* dep proofs also: *) true
( mkVar hp
, ExplicitBindings
@@ -1009,8 +1024,8 @@ let make_rewrite expr_info l hp max =
; New.observe_tac
(fun _ _ -> str "unfold functional")
(unfold_in_concl
- [ ( Locus.OnlyOccurrences [1]
- , evaluable_of_global_reference expr_info.func ) ])
+ [ ( Locus.OnlyOccurrences [1]
+ , evaluable_of_global_reference expr_info.func ) ])
; list_rewrite true
(List.map (fun e -> (mkVar e, true)) expr_info.eqs)
; New.observe_tac
@@ -1020,7 +1035,8 @@ let make_rewrite expr_info l hp max =
(fun _ _ -> str "make_rewrite1")
[ (* x < S (S max) proof *)
apply (EConstr.of_constr (delayed_force le_lt_SS))
- ; New.observe_tac (fun _ _ -> str "prove_le (3)") (prove_le ()) ] ]))
+ ; New.observe_tac (fun _ _ -> str "prove_le (3)") (prove_le ()) ]
+ ]))
let rec compute_max rew_tac max l =
match l with
@@ -1100,37 +1116,39 @@ let equation_app f_and_args expr_info continuation_tac infos =
let equation_app_rec (f, args) expr_info continuation_tac info =
Proofview.Goal.enter (fun g ->
- let sigma = Proofview.Goal.sigma g in
- try
- let v =
- List.assoc_f
- (List.equal (EConstr.eq_constr sigma))
- args expr_info.args_assoc
- in
- let new_infos = {expr_info with info = v} in
- New.observe_tac (fun _ _ -> str "app_rec found") (continuation_tac new_infos)
- with Not_found ->
- if expr_info.is_final && expr_info.is_main_branch then
- New.observe_tclTHENLIST
- (fun _ _ -> str "equation_app_rec")
- [ simplest_case (mkApp (expr_info.f_terminate, Array.of_list args))
- ; continuation_tac
- { expr_info with
- args_assoc = (args, delayed_force coq_O) :: expr_info.args_assoc
- }
- ; New.observe_tac
- (fun _ _ -> str "app_rec intros_values_eq")
- (intros_values_eq expr_info []) ]
- else
- New.observe_tclTHENLIST
- (fun _ _ -> str "equation_app_rec1")
- [ simplest_case (mkApp (expr_info.f_terminate, Array.of_list args))
- ; New.observe_tac
- (fun _ _ -> str "app_rec not_found")
- (continuation_tac
- { expr_info with
- args_assoc =
- (args, delayed_force coq_O) :: expr_info.args_assoc }) ])
+ let sigma = Proofview.Goal.sigma g in
+ try
+ let v =
+ List.assoc_f
+ (List.equal (EConstr.eq_constr sigma))
+ args expr_info.args_assoc
+ in
+ let new_infos = {expr_info with info = v} in
+ New.observe_tac
+ (fun _ _ -> str "app_rec found")
+ (continuation_tac new_infos)
+ with Not_found ->
+ if expr_info.is_final && expr_info.is_main_branch then
+ New.observe_tclTHENLIST
+ (fun _ _ -> str "equation_app_rec")
+ [ simplest_case (mkApp (expr_info.f_terminate, Array.of_list args))
+ ; continuation_tac
+ { expr_info with
+ args_assoc =
+ (args, delayed_force coq_O) :: expr_info.args_assoc }
+ ; New.observe_tac
+ (fun _ _ -> str "app_rec intros_values_eq")
+ (intros_values_eq expr_info []) ]
+ else
+ New.observe_tclTHENLIST
+ (fun _ _ -> str "equation_app_rec1")
+ [ simplest_case (mkApp (expr_info.f_terminate, Array.of_list args))
+ ; New.observe_tac
+ (fun _ _ -> str "app_rec not_found")
+ (continuation_tac
+ { expr_info with
+ args_assoc =
+ (args, delayed_force coq_O) :: expr_info.args_assoc }) ])
let equation_info =
{ message = "prove_equation with term "
@@ -1193,66 +1211,65 @@ let termination_proof_header is_mes input_type ids args_id relation rec_arg_num
rec_arg_id tac wf_tac : unit Proofview.tactic =
let open Tacticals.New in
Proofview.Goal.enter (fun g ->
- let nargs = List.length args_id in
- let pre_rec_args =
- List.rev_map mkVar (fst (List.chop (rec_arg_num - 1) args_id))
- in
- let relation = substl pre_rec_args relation in
- let input_type = substl pre_rec_args input_type in
- let wf_thm = next_ident_away_in_goal (Id.of_string "wf_R") ids in
- let wf_rec_arg =
- next_ident_away_in_goal
- (Id.of_string ("Acc_" ^ Id.to_string rec_arg_id))
- (wf_thm :: ids)
- in
- let hrec = next_ident_away_in_goal hrec_id (wf_rec_arg :: wf_thm :: ids) in
- let acc_inv =
- lazy
- (mkApp
- (delayed_force acc_inv_id, [|input_type; relation; mkVar rec_arg_id|]))
- in
- tclTHEN (h_intros args_id)
- (tclTHENS
- (New.observe_tac
- (fun _ _ -> str "first assert")
- (assert_before (Name wf_rec_arg)
- (mkApp
- ( delayed_force acc_rel
- , [|input_type; relation; mkVar rec_arg_id|] ))))
- [ (* accesibility proof *)
- tclTHENS
+ let nargs = List.length args_id in
+ let pre_rec_args =
+ List.rev_map mkVar (fst (List.chop (rec_arg_num - 1) args_id))
+ in
+ let relation = substl pre_rec_args relation in
+ let input_type = substl pre_rec_args input_type in
+ let wf_thm = next_ident_away_in_goal (Id.of_string "wf_R") ids in
+ let wf_rec_arg =
+ next_ident_away_in_goal
+ (Id.of_string ("Acc_" ^ Id.to_string rec_arg_id))
+ (wf_thm :: ids)
+ in
+ let hrec =
+ next_ident_away_in_goal hrec_id (wf_rec_arg :: wf_thm :: ids)
+ in
+ let acc_inv =
+ lazy
+ (mkApp
+ ( delayed_force acc_inv_id
+ , [|input_type; relation; mkVar rec_arg_id|] ))
+ in
+ tclTHEN (h_intros args_id)
+ (tclTHENS
(New.observe_tac
- (fun _ _ -> str "second assert")
- (assert_before (Name wf_thm)
- (mkApp
- (delayed_force well_founded, [|input_type; relation|]))))
- [ (* interactive proof that the relation is well_founded *)
- New.observe_tac
- (fun _ _ -> str "wf_tac")
- (wf_tac is_mes (Some args_id))
- ; (* this gives the accessibility argument *)
- New.observe_tac
- (fun _ _ -> str "apply wf_thm")
- (Simple.apply (mkApp (mkVar wf_thm, [|mkVar rec_arg_id|])))
- ]
- ; (* rest of the proof *)
- New.observe_tclTHENLIST
- (fun _ _ -> str "rest of proof")
- [ New.observe_tac
- (fun _ _ -> str "generalize")
- (onNLastHypsId (nargs + 1)
- (tclMAP (fun id ->
- tclTHEN
- (Tactics.generalize [mkVar id])
- (clear [id]))))
- ; New.observe_tac
- (fun _ _ -> str "fix")
- (fix hrec (nargs + 1))
- ; h_intros args_id
- ; Simple.intro wf_rec_arg
- ; New.observe_tac
- (fun _ _ -> str "tac")
- (tac wf_rec_arg hrec wf_rec_arg acc_inv) ] ]))
+ (fun _ _ -> str "first assert")
+ (assert_before (Name wf_rec_arg)
+ (mkApp
+ ( delayed_force acc_rel
+ , [|input_type; relation; mkVar rec_arg_id|] ))))
+ [ (* accesibility proof *)
+ tclTHENS
+ (New.observe_tac
+ (fun _ _ -> str "second assert")
+ (assert_before (Name wf_thm)
+ (mkApp
+ (delayed_force well_founded, [|input_type; relation|]))))
+ [ (* interactive proof that the relation is well_founded *)
+ New.observe_tac
+ (fun _ _ -> str "wf_tac")
+ (wf_tac is_mes (Some args_id))
+ ; (* this gives the accessibility argument *)
+ New.observe_tac
+ (fun _ _ -> str "apply wf_thm")
+ (Simple.apply (mkApp (mkVar wf_thm, [|mkVar rec_arg_id|])))
+ ]
+ ; (* rest of the proof *)
+ New.observe_tclTHENLIST
+ (fun _ _ -> str "rest of proof")
+ [ New.observe_tac
+ (fun _ _ -> str "generalize")
+ (onNLastHypsId (nargs + 1)
+ (tclMAP (fun id ->
+ tclTHEN (Tactics.generalize [mkVar id]) (clear [id]))))
+ ; New.observe_tac (fun _ _ -> str "fix") (fix hrec (nargs + 1))
+ ; h_intros args_id
+ ; Simple.intro wf_rec_arg
+ ; New.observe_tac
+ (fun _ _ -> str "tac")
+ (tac wf_rec_arg hrec wf_rec_arg acc_inv) ] ]))
let rec instantiate_lambda sigma t l =
match l with
@@ -1264,59 +1281,59 @@ let rec instantiate_lambda sigma t l =
let whole_start concl_tac nb_args is_mes func input_type relation rec_arg_num :
unit Proofview.tactic =
Proofview.Goal.enter (fun g ->
- let sigma = Proofview.Goal.sigma g in
- let hyps = Proofview.Goal.hyps g in
- let ids = Termops.ids_of_named_context hyps in
- let func_body = def_of_const (constr_of_monomorphic_global func) in
- let func_body = EConstr.of_constr func_body in
- let f_name, _, body1 = destLambda sigma func_body in
- let f_id =
- match f_name.binder_name with
- | Name f_id -> next_ident_away_in_goal f_id ids
- | Anonymous -> anomaly (Pp.str "Anonymous function.")
- in
- let n_names_types, _ = decompose_lam_n sigma nb_args body1 in
- let n_ids, ids =
- List.fold_left
- (fun (n_ids, ids) (n_name, _) ->
- match n_name.binder_name with
- | Name id ->
- let n_id = next_ident_away_in_goal id ids in
- (n_id :: n_ids, n_id :: ids)
- | _ -> anomaly (Pp.str "anonymous argument."))
- ([], f_id :: ids)
- n_names_types
- in
- let rec_arg_id = List.nth n_ids (rec_arg_num - 1) in
- let expr =
- instantiate_lambda sigma func_body (mkVar f_id :: List.map mkVar n_ids)
- in
- termination_proof_header is_mes input_type ids n_ids relation rec_arg_num
- rec_arg_id
- (fun rec_arg_id hrec acc_id acc_inv ->
- (prove_terminate
- (fun infos -> Proofview.tclUNIT ())
- { is_main_branch = true
- ; (* we are on the main branche (i.e. still on a match ... with .... end *)
- is_final = true
- ; (* and on leaf (more or less) *)
- f_terminate = delayed_force coq_O
- ; nb_arg = nb_args
- ; concl_tac
- ; rec_arg_id
- ; is_mes
- ; ih = hrec
- ; f_id
- ; f_constr = mkVar f_id
- ; func
- ; info = expr
- ; acc_inv
- ; acc_id
- ; values_and_bounds = []
- ; eqs = []
- ; forbidden_ids = []
- ; args_assoc = [] }))
- (fun b ids -> tclUSER_if_not_mes concl_tac b ids))
+ let sigma = Proofview.Goal.sigma g in
+ let hyps = Proofview.Goal.hyps g in
+ let ids = Termops.ids_of_named_context hyps in
+ let func_body = def_of_const (constr_of_monomorphic_global func) in
+ let func_body = EConstr.of_constr func_body in
+ let f_name, _, body1 = destLambda sigma func_body in
+ let f_id =
+ match f_name.binder_name with
+ | Name f_id -> next_ident_away_in_goal f_id ids
+ | Anonymous -> anomaly (Pp.str "Anonymous function.")
+ in
+ let n_names_types, _ = decompose_lam_n sigma nb_args body1 in
+ let n_ids, ids =
+ List.fold_left
+ (fun (n_ids, ids) (n_name, _) ->
+ match n_name.binder_name with
+ | Name id ->
+ let n_id = next_ident_away_in_goal id ids in
+ (n_id :: n_ids, n_id :: ids)
+ | _ -> anomaly (Pp.str "anonymous argument."))
+ ([], f_id :: ids)
+ n_names_types
+ in
+ let rec_arg_id = List.nth n_ids (rec_arg_num - 1) in
+ let expr =
+ instantiate_lambda sigma func_body (mkVar f_id :: List.map mkVar n_ids)
+ in
+ termination_proof_header is_mes input_type ids n_ids relation rec_arg_num
+ rec_arg_id
+ (fun rec_arg_id hrec acc_id acc_inv ->
+ prove_terminate
+ (fun infos -> Proofview.tclUNIT ())
+ { is_main_branch = true
+ ; (* we are on the main branche (i.e. still on a match ... with .... end *)
+ is_final = true
+ ; (* and on leaf (more or less) *)
+ f_terminate = delayed_force coq_O
+ ; nb_arg = nb_args
+ ; concl_tac
+ ; rec_arg_id
+ ; is_mes
+ ; ih = hrec
+ ; f_id
+ ; f_constr = mkVar f_id
+ ; func
+ ; info = expr
+ ; acc_inv
+ ; acc_id
+ ; values_and_bounds = []
+ ; eqs = []
+ ; forbidden_ids = []
+ ; args_assoc = [] })
+ (fun b ids -> tclUSER_if_not_mes concl_tac b ids))
let get_current_subgoals_types pstate =
let p = Declare.Proof.get pstate in
@@ -1351,8 +1368,7 @@ let build_and_l sigma l =
let c, tac, nb = f pl in
( mk_and p1 c
, tclTHENS
- (apply
- (EConstr.of_constr (constr_of_monomorphic_global conj_constr)))
+ (apply (EConstr.of_constr (constr_of_monomorphic_global conj_constr)))
[tclIDTAC; tac]
, nb + 1 )
in
@@ -1479,21 +1495,18 @@ let open_new_goal ~lemma build_proof sigma using_lemmas ref_ goal_name
fst
@@ Declare.Proof.by
(tclTHEN decompose_and_tac
- (tclORELSE
- (tclFIRST
- (List.map
- (fun c ->
- Tacticals.New.tclTHENLIST
- [ intros
- ; Simple.apply
- (fst
- (interp_constr (Global.env ())
- Evd.empty c))
- (*FIXME*)
- ; Tacticals.New.tclCOMPLETE Auto.default_auto
- ])
- using_lemmas))
- tclIDTAC))
+ (tclORELSE
+ (tclFIRST
+ (List.map
+ (fun c ->
+ Tacticals.New.tclTHENLIST
+ [ intros
+ ; Simple.apply
+ (fst (interp_constr (Global.env ()) Evd.empty c))
+ (*FIXME*)
+ ; Tacticals.New.tclCOMPLETE Auto.default_auto ])
+ using_lemmas))
+ tclIDTAC))
lemma
in
if Declare.Proof.get_open_goals lemma = 0 then (defined lemma; None)
@@ -1519,9 +1532,9 @@ let com_terminate interactive_proof tcc_lemma_name tcc_lemma_ref is_mes
fst
@@ Declare.Proof.by
(New.observe_tac
- (fun _ _ -> str "whole_start")
- (whole_start tac_end nb_args is_mes fonctional_ref input_type
- relation rec_arg_num))
+ (fun _ _ -> str "whole_start")
+ (whole_start tac_end nb_args is_mes fonctional_ref input_type
+ relation rec_arg_num))
lemma
in
let lemma =
@@ -1542,27 +1555,26 @@ let com_terminate interactive_proof tcc_lemma_name tcc_lemma_ref is_mes
let start_equation (f : GlobRef.t) (term_f : GlobRef.t)
(cont_tactic : Id.t list -> unit Proofview.tactic) =
Proofview.Goal.enter (fun g ->
- let sigma = Proofview.Goal.sigma g in
- let ids = Tacmach.New.pf_ids_of_hyps g in
- let terminate_constr = constr_of_monomorphic_global term_f in
- let terminate_constr = EConstr.of_constr terminate_constr in
- let nargs =
- nb_prod sigma
- (EConstr.of_constr (type_of_const sigma terminate_constr))
- in
- let x = n_x_id ids nargs in
- New.observe_tac
- (fun _ _ -> str "start_equation")
- (New.observe_tclTHENLIST
- (fun _ _ -> str "start_equation")
- [ h_intros x
- ; unfold_in_concl
- [(Locus.AllOccurrences, evaluable_of_global_reference f)]
- ; New.observe_tac
- (fun _ _ -> str "simplest_case")
- (simplest_case
- (mkApp (terminate_constr, Array.of_list (List.map mkVar x))))
- ; New.observe_tac (fun _ _ -> str "prove_eq") (cont_tactic x) ]))
+ let sigma = Proofview.Goal.sigma g in
+ let ids = Tacmach.New.pf_ids_of_hyps g in
+ let terminate_constr = constr_of_monomorphic_global term_f in
+ let terminate_constr = EConstr.of_constr terminate_constr in
+ let nargs =
+ nb_prod sigma (EConstr.of_constr (type_of_const sigma terminate_constr))
+ in
+ let x = n_x_id ids nargs in
+ New.observe_tac
+ (fun _ _ -> str "start_equation")
+ (New.observe_tclTHENLIST
+ (fun _ _ -> str "start_equation")
+ [ h_intros x
+ ; unfold_in_concl
+ [(Locus.AllOccurrences, evaluable_of_global_reference f)]
+ ; New.observe_tac
+ (fun _ _ -> str "simplest_case")
+ (simplest_case
+ (mkApp (terminate_constr, Array.of_list (List.map mkVar x))))
+ ; New.observe_tac (fun _ _ -> str "prove_eq") (cont_tactic x) ]))
let com_eqn uctx nb_arg eq_name functional_ref f_ref terminate_ref
equation_lemma_type =
@@ -1586,33 +1598,33 @@ let com_eqn uctx nb_arg eq_name functional_ref f_ref terminate_ref
fst
@@ Declare.Proof.by
(start_equation f_ref terminate_ref (fun x ->
- prove_eq
- (fun _ -> Proofview.tclUNIT ())
- { nb_arg
- ; f_terminate =
- EConstr.of_constr
- (constr_of_monomorphic_global terminate_ref)
- ; f_constr = EConstr.of_constr f_constr
- ; concl_tac = Tacticals.New.tclIDTAC
- ; func = functional_ref
- ; info =
- instantiate_lambda Evd.empty
- (EConstr.of_constr
- (def_of_const
- (constr_of_monomorphic_global functional_ref)))
- (EConstr.of_constr f_constr :: List.map mkVar x)
- ; is_main_branch = true
- ; is_final = true
- ; values_and_bounds = []
- ; eqs = []
- ; forbidden_ids = []
- ; acc_inv = lazy (assert false)
- ; acc_id = Id.of_string "____"
- ; args_assoc = []
- ; f_id = Id.of_string "______"
- ; rec_arg_id = Id.of_string "______"
- ; is_mes = false
- ; ih = Id.of_string "______" }))
+ prove_eq
+ (fun _ -> Proofview.tclUNIT ())
+ { nb_arg
+ ; f_terminate =
+ EConstr.of_constr
+ (constr_of_monomorphic_global terminate_ref)
+ ; f_constr = EConstr.of_constr f_constr
+ ; concl_tac = Tacticals.New.tclIDTAC
+ ; func = functional_ref
+ ; info =
+ instantiate_lambda Evd.empty
+ (EConstr.of_constr
+ (def_of_const
+ (constr_of_monomorphic_global functional_ref)))
+ (EConstr.of_constr f_constr :: List.map mkVar x)
+ ; is_main_branch = true
+ ; is_final = true
+ ; values_and_bounds = []
+ ; eqs = []
+ ; forbidden_ids = []
+ ; acc_inv = lazy (assert false)
+ ; acc_id = Id.of_string "____"
+ ; args_assoc = []
+ ; f_id = Id.of_string "______"
+ ; rec_arg_id = Id.of_string "______"
+ ; is_mes = false
+ ; ih = Id.of_string "______" }))
lemma
in
let _ =
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 12:49:38 +0000