diff options
author | Samuel Mimram <smimram@debian.org> | 2008-01-03 16:26:12 +0000 |
---|---|---|
committer | Samuel Mimram <smimram@debian.org> | 2008-01-03 16:26:12 +0000 |
commit | 2281410e38ef99d025ea77194585a9bc019fdaa9 (patch) | |
tree | 71ba76741c3ab6b752be876565dc34b0b0138dc5 /contrib/funind | |
parent | 4767d724d489a7ad67f696e9401e70b9f9ae2143 (diff) |
Imported Upstream version 8.1.pl3+dfsgupstream/8.1.pl3+dfsg
Diffstat (limited to 'contrib/funind')
-rw-r--r-- | contrib/funind/functional_principles_proofs.ml | 282 | ||||
-rw-r--r-- | contrib/funind/invfun.ml | 4 |
2 files changed, 186 insertions, 100 deletions
diff --git a/contrib/funind/functional_principles_proofs.ml b/contrib/funind/functional_principles_proofs.ml index dec7273b..975cf60b 100644 --- a/contrib/funind/functional_principles_proofs.ml +++ b/contrib/funind/functional_principles_proofs.ml @@ -46,10 +46,10 @@ let observe_tac_stream s tac g = let observe_tac s tac g = observe_tac_stream (str s) tac g -let tclTRYD tac = - if !Options.debug || do_observe () - then (fun g -> try (* do_observe_tac "" *)tac g with _ -> tclIDTAC g) - else tac +(* let tclTRYD tac = *) +(* if !Options.debug || do_observe () *) +(* then (fun g -> try (\* do_observe_tac "" *\)tac g with _ -> tclIDTAC g) *) +(* else tac *) let list_chop ?(msg="") n l = @@ -136,11 +136,11 @@ let change_hyp_with_using msg hyp_id t tac : tactic = fun g -> let prov_id = pf_get_new_id hyp_id g in tclTHENS - (observe_tac msg (forward (Some (tclCOMPLETE tac)) (Genarg.IntroIdentifier prov_id) t)) + ((* observe_tac msg *) (forward (Some (tclCOMPLETE tac)) (Genarg.IntroIdentifier prov_id) t)) [tclTHENLIST [ - observe_tac "change_hyp_with_using thin" (thin [hyp_id]); - observe_tac "change_hyp_with_using rename " (h_rename prov_id hyp_id) + (* observe_tac "change_hyp_with_using thin" *) (thin [hyp_id]); + (* observe_tac "change_hyp_with_using rename " *) (h_rename prov_id hyp_id) ]] g exception TOREMOVE @@ -179,7 +179,7 @@ let nf_betaiotazeta = (* Reductionops.local_strong Reductionops.whd_betaiotazeta let change_eq env sigma hyp_id (context:Sign.rel_context) x t end_of_type = let nochange msg = begin - observe (str ("Not treating ( "^msg^" )") ++ pr_lconstr t ); +(* observe (str ("Not treating ( "^msg^" )") ++ pr_lconstr t ); *) failwith "NoChange"; end in @@ -195,7 +195,7 @@ let change_eq env sigma hyp_id (context:Sign.rel_context) x t end_of_type = in if not (closed0 t1) then nochange "not a closed lhs"; let rec compute_substitution sub t1 t2 = - observe (str "compute_substitution : " ++ pr_lconstr t1 ++ str " === " ++ pr_lconstr t2); +(* observe (str "compute_substitution : " ++ pr_lconstr t1 ++ str " === " ++ pr_lconstr t2); *) if isRel t2 then let t2 = destRel t2 in @@ -386,11 +386,12 @@ let clean_hyp_with_heq ptes_infos eq_hyps hyp_id env sigma = List.rev_map mkVar (rec_pte_id::context_hyps_ids) ) in - observe_tac "rec hyp " +(* observe_tac "rec hyp " *) (tclTHENS (assert_as true (Genarg.IntroIdentifier rec_pte_id) t_x) - [observe_tac "prove rec hyp" (prove_rec_hyp eq_hyps); - observe_tac "prove rec hyp" + [ + (* observe_tac "prove rec hyp" *) (prove_rec_hyp eq_hyps); +(* observe_tac "prove rec hyp" *) (refine to_refine) ]) g @@ -399,7 +400,7 @@ let clean_hyp_with_heq ptes_infos eq_hyps hyp_id env sigma = in tclTHENLIST [ - observe_tac "hyp rec" +(* observe_tac "hyp rec" *) (change_hyp_with_using "rec_hyp_tac" hyp_id real_type_of_hyp prove_new_type_of_hyp); scan_type context popped_t' ] @@ -440,7 +441,7 @@ let clean_hyp_with_heq ptes_infos eq_hyps hyp_id env sigma = in tclTHENLIST[ change_hyp_with_using "prove_trivial" hyp_id real_type_of_hyp - (observe_tac "prove_trivial" prove_trivial); + ((* observe_tac "prove_trivial" *) prove_trivial); scan_type context popped_t' ] else if is_trivial_eq t_x @@ -456,7 +457,7 @@ let clean_hyp_with_heq ptes_infos eq_hyps hyp_id env sigma = "prove_trivial_eq" hyp_id real_type_of_hyp - (observe_tac "prove_trivial_eq" (prove_trivial_eq hyp_id context (args.(0),args.(1)))); + ((* observe_tac "prove_trivial_eq" *) (prove_trivial_eq hyp_id context (args.(0),args.(1)))); scan_type context popped_t' ] else @@ -505,7 +506,7 @@ let clean_goal_with_heq ptes_infos continue_tac dyn_infos = tclTHENLIST [ tac ; - observe_tac "clean_hyp_with_heq continue" (continue_tac new_infos) + (* observe_tac "clean_hyp_with_heq continue" *) (continue_tac new_infos) ] g @@ -523,7 +524,7 @@ let treat_new_case ptes_infos nb_prod continue_tac term dyn_infos = introduction_no_check heq_id; (* Then the new hypothesis *) tclMAP introduction_no_check dyn_infos.rec_hyps; - observe_tac "after_introduction" (fun g' -> + (* observe_tac "after_introduction" *)(fun g' -> (* We get infos on the equations introduced*) let new_term_value_eq = pf_type_of g' (mkVar heq_id) in (* compute the new value of the body *) @@ -572,7 +573,7 @@ let instanciate_hyps_with_args (do_prove:identifier list -> tactic) hyps args_id tclTHENLIST[ forward None (Genarg.IntroIdentifier prov_hid) (mkApp(mkVar hid,args)); thin [hid]; - h_rename prov_hid hid + (h_rename prov_hid hid) ] g ) ( (* @@ -619,9 +620,9 @@ let build_proof : tactic = let rec build_proof_aux do_finalize dyn_infos : tactic = fun g -> - (* observe (str "proving on " ++ Printer.pr_lconstr_env (pf_env g) term);*) - match kind_of_term dyn_infos.info with | Case(ci,ct,t,cb) -> + match kind_of_term dyn_infos.info with + | Case(ci,ct,t,cb) -> let do_finalize_t dyn_info' = fun g -> let t = dyn_info'.info in @@ -674,7 +675,7 @@ let build_proof nb_rec_hyps = List.length new_hyps } in - observe_tac "Lambda" (instanciate_hyps_with_args do_prove new_infos.rec_hyps [id]) g' +(* observe_tac "Lambda" *) (instanciate_hyps_with_args do_prove new_infos.rec_hyps [id]) g' (* build_proof do_finalize new_infos g' *) ) g | _ -> @@ -757,7 +758,7 @@ let build_proof | Rel _ -> anomaly "Free var in goal conclusion !" and build_proof do_finalize dyn_infos g = (* observe (str "proving with "++Printer.pr_lconstr dyn_infos.info++ str " on goal " ++ pr_gls g); *) - (build_proof_aux do_finalize dyn_infos) g + observe_tac "build_proof" (build_proof_aux do_finalize dyn_infos) g and build_proof_args do_finalize dyn_infos (* f_args' args *) :tactic = fun g -> let (f_args',args) = dyn_infos.info in @@ -783,14 +784,14 @@ let build_proof {dyn_infos with info = arg } g in - observe_tac "build_proof_args" (tac ) g + (* observe_tac "build_proof_args" *) (tac ) g in let do_finish_proof dyn_infos = (* tclTRYD *) (clean_goal_with_heq ptes_infos finish_proof dyn_infos) in - observe_tac "build_proof" + (* observe_tac "build_proof" *) (build_proof (clean_goal_with_heq ptes_infos do_finish_proof) dyn_infos) @@ -863,8 +864,8 @@ let generalize_non_dep hyp g = in (* observe (str "to_revert := " ++ prlist_with_sep spc Ppconstr.pr_id to_revert); *) tclTHEN - (observe_tac "h_generalize" (h_generalize (List.map mkVar to_revert) )) - (observe_tac "thin" (thin to_revert)) + ((* observe_tac "h_generalize" *) (h_generalize (List.map mkVar to_revert) )) + ((* observe_tac "thin" *) (thin to_revert)) g let id_of_decl (na,_,_) = (Nameops.out_name na) @@ -905,11 +906,11 @@ let generate_equation_lemma fnames f fun_num nb_params nb_args rec_args_num = tclTHENSEQ [ tclDO (nb_params + rec_args_num + 1) intro; - observe_tac "" (fun g -> + (* observe_tac "" *) (fun g -> let rec_id = pf_nth_hyp_id g 1 in tclTHENSEQ - [observe_tac "generalize_non_dep in generate_equation_lemma" (generalize_non_dep rec_id); - observe_tac "h_case" (h_case(mkVar rec_id,Rawterm.NoBindings)); + [(* observe_tac "generalize_non_dep in generate_equation_lemma" *) (generalize_non_dep rec_id); + (* observe_tac "h_case" *) (h_case (mkVar rec_id,Rawterm.NoBindings)); intros_reflexivity] g ) ] @@ -1138,7 +1139,7 @@ let prove_princ_for_struct interactive_proof fun_num fnames all_funs _nparams : in if other_fix_infos = [] then - observe_tac ("h_fix") (h_fix (Some this_fix_info.name) (this_fix_info.idx +1)) + (* observe_tac ("h_fix") *) (h_fix (Some this_fix_info.name) (this_fix_info.idx +1)) else h_mutual_fix this_fix_info.name (this_fix_info.idx + 1) other_fix_infos @@ -1146,10 +1147,10 @@ let prove_princ_for_struct interactive_proof fun_num fnames all_funs _nparams : in let first_tac : tactic = (* every operations until fix creations *) tclTHENSEQ - [ observe_tac "introducing params" (intros_using (List.rev_map id_of_decl princ_info.params)); - observe_tac "introducing predictes" (intros_using (List.rev_map id_of_decl princ_info.predicates)); - observe_tac "introducing branches" (intros_using (List.rev_map id_of_decl princ_info.branches)); - observe_tac "building fixes" mk_fixes; + [ (* observe_tac "introducing params" *) (intros_using (List.rev_map id_of_decl princ_info.params)); + (* observe_tac "introducing predictes" *) (intros_using (List.rev_map id_of_decl princ_info.predicates)); + (* observe_tac "introducing branches" *) (intros_using (List.rev_map id_of_decl princ_info.branches)); + (* observe_tac "building fixes" *) mk_fixes; ] in let intros_after_fixes : tactic = @@ -1162,7 +1163,7 @@ let prove_princ_for_struct interactive_proof fun_num fnames all_funs _nparams : let nb_args = fix_info.nb_realargs in tclTHENSEQ [ - observe_tac ("introducing args") (tclDO nb_args intro); + (* observe_tac ("introducing args") *) (tclDO nb_args intro); (fun g -> (* replacement of the function by its body *) let args = nLastHyps nb_args g in let fix_body = fix_info.body_with_param in @@ -1180,7 +1181,7 @@ let prove_princ_for_struct interactive_proof fun_num fnames all_funs _nparams : in tclTHENSEQ [ - observe_tac "do_replace" +(* observe_tac "do_replace" *) (do_replace full_params (fix_info.idx + List.length princ_params) @@ -1205,7 +1206,7 @@ let prove_princ_for_struct interactive_proof fun_num fnames all_funs _nparams : nb_rec_hyps = List.length branches } in - observe_tac "cleaning" (clean_goal_with_heq + (* observe_tac "cleaning" *) (clean_goal_with_heq (Idmap.map prove_rec_hyp ptes_to_fix) do_prove dyn_infos) @@ -1215,7 +1216,7 @@ let prove_princ_for_struct interactive_proof fun_num fnames all_funs _nparams : (* str "args := " ++ prlist_with_sep spc Ppconstr.pr_id args_id *) (* ); *) - observe_tac "instancing" (instanciate_hyps_with_args prove_tac + (* observe_tac "instancing" *) (instanciate_hyps_with_args prove_tac (List.rev_map id_of_decl princ_info.branches) (List.rev args_id)) ] @@ -1295,18 +1296,28 @@ and h_intros = Recdef.h_intros and list_rewrite = Recdef.list_rewrite and evaluable_of_global_reference = Recdef.evaluable_of_global_reference + + + + let prove_with_tcc tcc_lemma_constr eqs : tactic = match !tcc_lemma_constr with | None -> anomaly "No tcc proof !!" | Some lemma -> fun gls -> - let hid = next_global_ident_away true h_id (pf_ids_of_hyps gls) in +(* let hid = next_global_ident_away true h_id (pf_ids_of_hyps gls) in *) +(* let ids = hid::pf_ids_of_hyps gls in *) tclTHENSEQ [ - generalize [lemma]; - h_intro hid; - Elim.h_decompose_and (mkVar hid); +(* 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 (false,5) [] (Some []) ] gls @@ -1314,6 +1325,7 @@ let prove_with_tcc tcc_lemma_constr eqs : tactic = let backtrack_eqs_until_hrec hrec eqs : tactic = fun gls -> + let eqs = List.map mkVar eqs in let rewrite = tclFIRST (List.map Equality.rewriteRL eqs ) in @@ -1331,42 +1343,60 @@ let backtrack_eqs_until_hrec hrec eqs : tactic = - +let build_clause eqs = + { + Tacexpr.onhyps = + Some (List.map + (fun id -> ([],id),Tacexpr.InHyp) + eqs + ); + Tacexpr.onconcl = false; + Tacexpr.concl_occs = [] + } -let new_prove_with_tcc is_mes acc_inv hrec tcc_lemma_constr eqs : tactic = - match !tcc_lemma_constr with - | None -> tclIDTAC_MESSAGE (str "No tcc proof !!") - | Some lemma -> - fun gls -> - let hid = next_global_ident_away true Recdef.h_id (pf_ids_of_hyps gls) in - (tclTHENSEQ - [ - generalize [lemma]; - h_intro hid; - Elim.h_decompose_and (mkVar hid); - backtrack_eqs_until_hrec hrec eqs; - observe_tac ("new_prove_with_tcc ( applying "^(string_of_id hrec)^" )" ) - (tclTHENS (* We must have exactly ONE subgoal !*) - (apply (mkVar hrec)) - [ tclTHENSEQ - [ - thin [hrec]; - apply (Lazy.force acc_inv); - (fun g -> - if is_mes - then - unfold_in_concl [([], evaluable_of_global_reference (delayed_force ltof_ref))] g - else tclIDTAC g - ); - observe_tac "rew_and_finish" - (tclTHEN - (tclTRY(Recdef.list_rewrite true eqs)) - (observe_tac "finishing" (tclCOMPLETE (Eauto.gen_eauto false (false,5) [] (Some []))))) +let rec rewrite_eqs_in_eqs eqs = + match eqs with + | [] -> tclIDTAC + | eq::eqs -> + tclTHEN + (tclMAP (fun id -> tclTRY (Equality.general_rewrite_in true id (mkVar eq))) eqs) + (rewrite_eqs_in_eqs eqs) + +let new_prove_with_tcc is_mes acc_inv hrec tcc_hyps eqs : tactic = + fun gls -> + (tclTHENSEQ + [ + backtrack_eqs_until_hrec hrec eqs; + (* observe_tac ("new_prove_with_tcc ( applying "^(string_of_id hrec)^" )" ) *) + (tclTHENS (* We must have exactly ONE subgoal !*) + (apply (mkVar hrec)) + [ tclTHENSEQ + [ + keep (tcc_hyps@eqs); + + apply (Lazy.force acc_inv); + (fun g -> + if is_mes + then + unfold_in_concl [([], evaluable_of_global_reference (delayed_force ltof_ref))] g + else tclIDTAC g + ); + observe_tac "rew_and_finish" + (tclTHENLIST + [tclTRY(Recdef.list_rewrite false (List.map mkVar eqs)); + rewrite_eqs_in_eqs eqs; + (observe_tac "finishing" + (tclCOMPLETE ( + Eauto.gen_eauto false (false,5) [] (Some [])) + ) + ) ] - ]) + ) + ] ]) - gls - + ]) + gls + let is_valid_hypothesis predicates_name = let predicates_name = List.fold_right Idset.add predicates_name Idset.empty in @@ -1420,13 +1450,14 @@ let prove_principle_for_gen 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 ); +(* 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 @@ -1435,7 +1466,7 @@ let prove_principle_for_gen | (Name id,_,_)::_ -> id | _ -> assert false in - observe (str "rec_arg_id := " ++ pr_lconstr (mkVar rec_arg_id)); +(* observe (str "rec_arg_id := " ++ pr_lconstr (mkVar rec_arg_id)); *) let subst_constrs = List.map (fun (na,_,_) -> mkVar (Nameops.out_name na)) (pre_rec_arg@princ_info.params) in let relation = substl subst_constrs relation in let input_type = substl subst_constrs rec_arg_type in @@ -1448,19 +1479,17 @@ let prove_principle_for_gen in let fix_id = Nameops.out_name (fresh_id (Name hrec_id)) in let prove_rec_arg_acc g = - (observe_tac "prove_rec_arg_acc" + ((* observe_tac "prove_rec_arg_acc" *) (tclCOMPLETE (tclTHEN (forward - (Some ((fun g -> observe_tac "prove wf" (tclCOMPLETE (wf_tac is_mes)) g))) + (Some ((fun g -> (* observe_tac "prove wf" *) (tclCOMPLETE (wf_tac is_mes)) g))) (Genarg.IntroIdentifier wf_thm_id) (mkApp (delayed_force well_founded,[|input_type;relation|]))) ( - observe_tac - "apply wf_thm" - (h_apply ((mkApp(mkVar wf_thm_id, - [|mkVar rec_arg_id |])),Rawterm.NoBindings) - ) + (* observe_tac *) +(* "apply wf_thm" *) + h_simplest_apply (mkApp(mkVar wf_thm_id,[|mkVar rec_arg_id|])) ) ) ) @@ -1468,22 +1497,68 @@ let prove_principle_for_gen g in let args_ids = List.map (fun (na,_,_) -> Nameops.out_name na) princ_info.args in + let lemma = + match !tcc_lemma_ref with + | None -> anomaly ( "No tcc proof !!") + | Some lemma -> lemma + 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 gls = + let hyps = pf_ids_of_hyps gls in + let hid = + next_global_ident_away true + (id_of_string "prov") + hyps + in + tclTHENSEQ + [ + generalize [lemma]; + h_intro hid; + Elim.h_decompose_and (mkVar hid); + (fun g -> + let new_hyps = pf_ids_of_hyps g in + tcc_list := list_diff new_hyps (hid::hyps); + if !tcc_list = [] + then + begin + tcc_list := [hid]; + tclIDTAC g + end + else thin [hid] g + ) + ] + gls + in tclTHENSEQ - [ + [ + observe_tac "start_tac" start_tac; h_intros (List.rev_map (fun (na,_,_) -> Nameops.out_name na) (princ_info.args@princ_info.branches@princ_info.predicates@princ_info.params) ); - observe_tac "" (forward + (* observe_tac "" *) (forward (Some (prove_rec_arg_acc)) (Genarg.IntroIdentifier acc_rec_arg_id) (mkApp (delayed_force acc_rel,[|input_type;relation;mkVar rec_arg_id|])) ); - observe_tac "reverting" (revert (List.rev (acc_rec_arg_id::args_ids))); - observe_tac "h_fix" (h_fix (Some fix_id) (List.length args_ids + 1)); +(* observe_tac "reverting" *) (revert (List.rev (acc_rec_arg_id::args_ids))); +(* (fun g -> observe (Printer.pr_goal (sig_it g) ++ fnl () ++ *) +(* str "fix arg num" ++ int (List.length args_ids + 1) ); tclIDTAC g); *) + (* observe_tac "h_fix " *) (h_fix (Some fix_id) (List.length args_ids + 1)); +(* (fun g -> observe (Printer.pr_goal (sig_it g) ++ fnl() ++ pr_lconstr_env (pf_env g ) (pf_type_of g (mkVar fix_id) )); tclIDTAC g); *) h_intros (List.rev (acc_rec_arg_id::args_ids)); Equality.rewriteLR (mkConst eq_ref); - observe_tac "finish" (fun gl' -> + (* observe_tac "finish" *) (fun gl' -> let body = let _,args = destApp (pf_concl gl') in array_last args @@ -1511,9 +1586,20 @@ let prove_principle_for_gen let pte_info = { proving_tac = (fun eqs -> - observe_tac "new_prove_with_tcc" +(* 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.out_name na)) princ_info.args)); *) +(* msgnl (str "princ_info.params := "++ prlist_with_sep spc Ppconstr.pr_id (List.map (fun (na,_,_) -> (Nameops.out_name 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_lemma_ref (List.map mkVar eqs) + is_mes acc_inv fix_id + !tcc_list + ((List.map + (fun (na,_,_) -> (Nameops.out_name na)) + (princ_info.args@princ_info.params) + )@ (acc_rec_arg_id::eqs)) ) ); is_valid = is_valid_hypothesis predicates_names @@ -1536,7 +1622,7 @@ let prove_principle_for_gen ptes_info (body_info rec_hyps) in - observe_tac "instanciate_hyps_with_args" + (* observe_tac "instanciate_hyps_with_args" *) (instanciate_hyps_with_args make_proof (List.map (fun (na,_,_) -> Nameops.out_name na) princ_info.branches) diff --git a/contrib/funind/invfun.ml b/contrib/funind/invfun.ml index 9ec02d4c..c7a3d164 100644 --- a/contrib/funind/invfun.ml +++ b/contrib/funind/invfun.ml @@ -569,14 +569,14 @@ let rec reflexivity_with_destruct_cases g = if Equality.discriminable (pf_env g) (project g) t1 t2 then Equality.discr id g else if Equality.injectable (pf_env g) (project g) t1 t2 - then tclTHEN (Equality.inj [] id) intros_with_rewrite g + then tclTHENSEQ [Equality.inj [] id;thin [id];intros_with_rewrite] g else tclIDTAC g | _ -> tclIDTAC g ) in (tclFIRST [ reflexivity; - destruct_case (); + tclTHEN (tclPROGRESS discr_inject) (destruct_case ()); (* We reach this point ONLY if the same value is matched (at least) two times along binding path. |