diff options
author | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-11-09 09:42:24 +0000 |
---|---|---|
committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-11-09 09:42:24 +0000 |
commit | cb2f5d06481f9021f600eaefbdc6b33118bd346d (patch) | |
tree | 8ae02c329fc3530368137996398c2c576a368574 | |
parent | c70d2b83582f5ea7b2218843859ad230afdb96a0 (diff) |
Quick fix for restoring a left-to-right rewriting lemma compatible
with the guard condition + typo in the generation of _rec schemes in
the impredicative case.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12484 85f007b7-540e-0410-9357-904b9bb8a0f7
-rw-r--r-- | tactics/eqschemes.ml | 53 | ||||
-rw-r--r-- | tactics/eqschemes.mli | 1 | ||||
-rw-r--r-- | tactics/equality.ml | 32 | ||||
-rw-r--r-- | toplevel/indschemes.ml | 2 |
4 files changed, 55 insertions, 33 deletions
diff --git a/tactics/eqschemes.ml b/tactics/eqschemes.ml index 058abb2b7..a9ced0a69 100644 --- a/tactics/eqschemes.ml +++ b/tactics/eqschemes.ml @@ -313,24 +313,28 @@ let build_l2r_rew_scheme dep env ind kind = rel_vect (nrealargs+4) nrealargs; rel_vect 4 nrealargs; [|mkRel 2|]])|]]) in + let main_body = + mkCase (ci, + my_it_mkLambda_or_LetIn_name realsign_ind_G applied_PG, + applied_sym_C 3, + [|mkVar varHC|]) in (my_it_mkLambda_or_LetIn mib.mind_params_ctxt (my_it_mkLambda_or_LetIn_name realsign (mkNamedLambda varP (my_it_mkProd_or_LetIn (if dep then realsign_ind_P else realsign_P) s) (mkNamedLambda varHC applied_PC (mkNamedLambda varH (lift 2 applied_ind) - (mkCase (cieq, - mkLambda (Name varH,lift 3 applied_ind, - mkLambda (Anonymous, - mkApp (eq,[|lift 4 applied_ind;applied_sym_sym;mkRel 1|]), - applied_PR)), - (mkApp (sym_involutive, - Array.append (extended_rel_vect 3 mip.mind_arity_ctxt) [|mkVar varH|])), - [|mkCase (ci, - my_it_mkLambda_or_LetIn_name realsign_ind_G applied_PG, - applied_sym_C 3, - [|mkVar varHC|])|]))))))) - + (if dep then (* we need a coercion *) + mkCase (cieq, + mkLambda (Name varH,lift 3 applied_ind, + mkLambda (Anonymous, + mkApp (eq,[|lift 4 applied_ind;applied_sym_sym;mkRel 1|]), + applied_PR)), + mkApp (sym_involutive, + Array.append (extended_rel_vect 3 mip.mind_arity_ctxt) [|mkVar varH|]), + [|main_body|]) + else + main_body)))))) (**********************************************************************) (* Build the right-to-left rewriting lemma for hypotheses associated *) @@ -529,18 +533,25 @@ let rew_r2l_forward_dep_scheme_kind = declare_individual_scheme_object "_rew_fwd_r_dep" (fun ind -> build_r2l_forward_rew_scheme true (Global.env()) ind InType) -(* Rewrite from left-to-right in conclusion and left-to-right in hypotheses *) +(* Rewrite from left-to-right in conclusion and right-to-left in hypotheses *) let rew_l2r_scheme_kind = declare_individual_scheme_object "_rew_r" (fun ind -> - (* For the non-dependent case, we have two possible choices: *) - (* - build_l2r_forward_rew_scheme is ok even for non symmetric *) - (* equality like eq_true but it introduced a beta-expansion blocked *) - (* by the match and thus, it makes the guard condition fragile *) - (* Moreover, its standard form needs the inductive hypothesis not *) - (* in last position what breaks the order of goals and need a fix! *) - (* - build_l2r_rew_scheme uses symmetry and is better for guard *) - (* but it does not work for non-symmetric equalities *) + (* We cannot use the simply-proved build_l2r_forward_rew_scheme *) + (* because it is introduced a beta-expansion blocked by the match *) + (* and may thus block in turn guard condition *) + build_l2r_rew_scheme false (Global.env()) ind InType) + +(* Asymmetric rewrite in hypotheses *) +let rew_asym_scheme_kind = + declare_individual_scheme_object "_rew_r_asym" + (fun ind -> + (* For the asymmetrical non-dependent case, we (currently) have only *) + (* build_l2r_forward_rew_scheme available, though it may break the *) + (* guard condition due to the introduction of a beta-expansion *) + (* blocked by a match. *) + (* Moreover, its standard form needs the inductive hypothesis not *) + (* in last position what breaks the order of goals and need a fix! *) fix_l2r_forward_rew_scheme (build_l2r_forward_rew_scheme false (Global.env()) ind InType)) diff --git a/tactics/eqschemes.mli b/tactics/eqschemes.mli index bf72245d6..a6ffe9e21 100644 --- a/tactics/eqschemes.mli +++ b/tactics/eqschemes.mli @@ -23,6 +23,7 @@ val rew_l2r_forward_dep_scheme_kind : individual scheme_kind val rew_r2l_forward_dep_scheme_kind : individual scheme_kind val rew_r2l_dep_scheme_kind : individual scheme_kind val rew_r2l_scheme_kind : individual scheme_kind +val rew_asym_scheme_kind : individual scheme_kind val build_r2l_rew_scheme : bool -> env -> inductive -> sorts_family -> constr val build_l2r_rew_scheme : bool -> env -> inductive -> sorts_family -> constr diff --git a/tactics/equality.ml b/tactics/equality.ml index 8ad73c672..7db751372 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -176,13 +176,22 @@ let register_is_applied_rewrite_relation = (:=) is_applied_rewrite_relation eliminate lbeq on sort_of_gl. *) let find_elim hdcncl lft2rgt dep cls = - let scheme_name = match dep, lft2rgt, (cls = None) with - | false, true, true | false, false, false -> rew_l2r_scheme_kind - | false, false, true | false, true, false -> rew_r2l_scheme_kind - | true, true, true -> rew_l2r_dep_scheme_kind - | true, true, false -> rew_r2l_forward_dep_scheme_kind - | true, false, true -> rew_r2l_dep_scheme_kind - | true, false, false -> rew_l2r_forward_dep_scheme_kind + let inccl = (cls = None) in + let scheme_name = match dep, lft2rgt, inccl with + (* Non dependent case with symmetric equality *) + | false, Some true, true | false, Some false, false -> rew_l2r_scheme_kind + | false, Some false, true | false, Some true, false -> rew_r2l_scheme_kind + (* Dependent case with symmetric equality *) + | true, Some true, true -> rew_l2r_dep_scheme_kind + | true, Some true, false -> rew_r2l_forward_dep_scheme_kind + | true, Some false, true -> rew_r2l_dep_scheme_kind + | true, Some false, false -> rew_l2r_forward_dep_scheme_kind + (* Non dependent case with non-symmetric rewriting lemma *) + | false, None, true -> rew_r2l_scheme_kind + | false, None, false -> rew_asym_scheme_kind + (* Dependent case with non-symmetric rewriting lemma *) + | true, None, true -> rew_r2l_dep_scheme_kind + | true, None, false -> rew_l2r_forward_dep_scheme_kind in match kind_of_term hdcncl with | Ind ind -> mkConst (find_scheme scheme_name ind) @@ -195,7 +204,8 @@ let type_of_clause gl = function let leibniz_rewrite_ebindings_clause cls lft2rgt tac sigma c t l with_evars gl hdcncl = let dep = occur_term c (type_of_clause gl cls) in let elim = find_elim hdcncl lft2rgt dep cls in - general_elim_clause with_evars tac cls sigma c t l lft2rgt + general_elim_clause with_evars tac cls sigma c t l + (match lft2rgt with None -> false | Some b -> b) {elimindex = None; elimbody = (elim,NoBindings)} gl let adjust_rewriting_direction args lft2rgt = @@ -204,11 +214,11 @@ let adjust_rewriting_direction args lft2rgt = (* more natural to see -> as the rewriting to the constant *) if not lft2rgt then error "Rewriting non-symmetric equality not allowed from right-to-left."; - not lft2rgt + None end else (* other equality *) - lft2rgt + Some lft2rgt let rewrite_side_tac tac sidetac = side_tac tac (Option.map fst sidetac) @@ -1069,7 +1079,7 @@ let swapEquandsInConcl gls = let bareRevSubstInConcl lbeq body (t,e1,e2) gls = (* find substitution scheme *) - let eq_elim = find_elim lbeq.eq false false None in + let eq_elim = find_elim lbeq.eq (Some false) false None in (* build substitution predicate *) let p = lambda_create (pf_env gls) (t,body) in (* apply substitution scheme *) diff --git a/toplevel/indschemes.ml b/toplevel/indschemes.ml index 9f05c3e6c..abf53fd97 100644 --- a/toplevel/indschemes.ml +++ b/toplevel/indschemes.ml @@ -194,7 +194,7 @@ let optimize_non_type_induction_scheme kind dep sort ind = mib.mind_nparams in snd (weaken_sort_scheme (new_sort_in_family sort) npars c t) else - build_induction_scheme (Global.env()) Evd.empty ind dep InProp + build_induction_scheme (Global.env()) Evd.empty ind dep sort let build_induction_scheme_in_type dep sort ind = build_induction_scheme (Global.env()) Evd.empty ind dep sort |