From 5b7eafd0f00a16d78f99a27f5c7d5a0de77dc7e6 Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Wed, 21 Jul 2010 09:46:51 +0200 Subject: Imported Upstream snapshot 8.3~beta0+13298 --- tactics/eqschemes.ml | 741 +++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 741 insertions(+) create mode 100644 tactics/eqschemes.ml (limited to 'tactics/eqschemes.ml') diff --git a/tactics/eqschemes.ml b/tactics/eqschemes.ml new file mode 100644 index 00000000..236eff72 --- /dev/null +++ b/tactics/eqschemes.ml @@ -0,0 +1,741 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* hid | InType -> xid +let fresh env id = next_global_ident_away id [] + +let build_dependent_inductive ind (mib,mip) = + let realargs,_ = list_chop mip.mind_nrealargs_ctxt mip.mind_arity_ctxt in + applist + (mkInd ind, + extended_rel_list mip.mind_nrealargs_ctxt mib.mind_params_ctxt + @ extended_rel_list 0 realargs) + +let my_it_mkLambda_or_LetIn s c = it_mkLambda_or_LetIn ~init:c s +let my_it_mkProd_or_LetIn s c = it_mkProd_or_LetIn ~init:c s +let my_it_mkLambda_or_LetIn_name s c = + it_mkLambda_or_LetIn_name (Global.env()) c s + +let get_coq_eq () = + try + let eq = Libnames.destIndRef Coqlib.glob_eq in + let _ = Global.lookup_inductive eq in + (* Do not force the lazy if they are not defined *) + mkInd eq, Coqlib.build_coq_eq_refl () + with Not_found -> + error "eq not found." + +(**********************************************************************) +(* Check if an inductive type [ind] has the form *) +(* *) +(* I q1..qm,p1..pn a1..an with one constructor *) +(* C : I q1..qm,p1..pn p1..pn *) +(* *) +(* in which case, a symmetry lemma is definable *) +(**********************************************************************) + +let get_sym_eq_data env ind = + let (mib,mip as specif) = lookup_mind_specif env ind in + if Array.length mib.mind_packets <> 1 or Array.length mip.mind_nf_lc <> 1 then + error "Not an inductive type with a single constructor."; + let realsign,_ = list_chop mip.mind_nrealargs_ctxt mip.mind_arity_ctxt in + if List.exists (fun (_,b,_) -> b <> None) realsign then + error "Inductive equalities with local definitions in arity not supported."; + let constrsign,ccl = decompose_prod_assum mip.mind_nf_lc.(0) in + let _,constrargs = decompose_app ccl in + if rel_context_length constrsign<>rel_context_length mib.mind_params_ctxt then + error "Constructor must have no arguments"; (* This can be relaxed... *) + let params,constrargs = list_chop mib.mind_nparams constrargs in + if mip.mind_nrealargs > mib.mind_nparams then + error "Constructors arguments must repeat the parameters."; + let _,params2 = list_chop (mib.mind_nparams-mip.mind_nrealargs) params in + let paramsctxt1,_ = + list_chop (mib.mind_nparams-mip.mind_nrealargs) mib.mind_params_ctxt in + if params2 <> constrargs then + error "Constructors arguments must repeat the parameters."; + (* nrealargs_ctxt and nrealargs are the same here *) + (specif,mip.mind_nrealargs,realsign,mib.mind_params_ctxt,paramsctxt1) + +(**********************************************************************) +(* Check if an inductive type [ind] has the form *) +(* *) +(* I q1..qm a1..an with one constructor *) +(* C : I q1..qm b1..bn *) +(* *) +(* in which case it expresses the equalities ai=bi, but not in a way *) +(* such that symmetry is a priori definable *) +(**********************************************************************) + +let get_non_sym_eq_data env ind = + let (mib,mip as specif) = lookup_mind_specif env ind in + if Array.length mib.mind_packets <> 1 or Array.length mip.mind_nf_lc <> 1 then + error "Not an inductive type with a single constructor."; + let realsign,_ = list_chop mip.mind_nrealargs_ctxt mip.mind_arity_ctxt in + if List.exists (fun (_,b,_) -> b <> None) realsign then + error "Inductive equalities with local definitions in arity not supported"; + let constrsign,ccl = decompose_prod_assum mip.mind_nf_lc.(0) in + let _,constrargs = decompose_app ccl in + if rel_context_length constrsign<>rel_context_length mib.mind_params_ctxt then + error "Constructor must have no arguments"; + let _,constrargs = list_chop mib.mind_nparams constrargs in + (specif,constrargs,realsign,mip.mind_nrealargs) + +(**********************************************************************) +(* Build the symmetry lemma associated to an inductive type *) +(* I q1..qm,p1..pn a1..an with one constructor *) +(* C : I q1..qm,p1..pn p1..pn *) +(* *) +(* sym := fun q1..qn p1..pn a1..an (H:I q1..qm p1..pn a1..an) => *) +(* match H in I _.._ a1..an return I q1..qm a1..an p1..pn with *) +(* C => C *) +(* end *) +(* : forall q1..qm p1..pn a1..an I q1..qm p1..pn a1..an -> *) +(* I q1..qm a1..an p1..pn *) +(* *) +(**********************************************************************) + +let build_sym_scheme env ind = + let (mib,mip as specif),nrealargs,realsign,paramsctxt,paramsctxt1 = + get_sym_eq_data env ind in + let cstr n = + mkApp (mkConstruct(ind,1),extended_rel_vect n mib.mind_params_ctxt) in + let varH = fresh env (default_id_of_sort (snd (mind_arity mip))) in + let applied_ind = build_dependent_inductive ind specif in + let realsign_ind = + name_context env ((Name varH,None,applied_ind)::realsign) in + let ci = make_case_info (Global.env()) ind RegularStyle in + (my_it_mkLambda_or_LetIn mib.mind_params_ctxt + (my_it_mkLambda_or_LetIn_name realsign_ind + (mkCase (ci, + my_it_mkLambda_or_LetIn_name + (lift_rel_context (nrealargs+1) realsign_ind) + (mkApp (mkInd ind,Array.concat + [extended_rel_vect (3*nrealargs+2) paramsctxt1; + rel_vect 1 nrealargs; + rel_vect (2*nrealargs+2) nrealargs])), + mkRel 1 (* varH *), + [|cstr (nrealargs+1)|])))) + +let sym_scheme_kind = + declare_individual_scheme_object "_sym" + (fun ind -> build_sym_scheme (Global.env() (* side-effect! *)) ind) + +(**********************************************************************) +(* Build the involutivity of symmetry for an inductive type *) +(* I q1..qm,p1..pn a1..an with one constructor *) +(* C : I q1..qm,p1..pn p1..pn *) +(* *) +(* inv := fun q1..qn p1..pn a1..an (H:I q1..qm p1..pn a1..an) => *) +(* match H in I _.._ a1..an return *) +(* sym q1..qm p1..pn a1..an (sym q1..qm a1..an p1..pn H) = H *) +(* with *) +(* C => refl_equal C *) +(* end *) +(* : forall q1..qm p1..pn a1..an (H:I q1..qm a1..an p1..pn), *) +(* sym q1..qm p1..pn a1..an (sym q1..qm a1..an p1..pn H) = H *) +(* *) +(**********************************************************************) + +let build_sym_involutive_scheme env ind = + let (mib,mip as specif),nrealargs,realsign,paramsctxt,paramsctxt1 = + get_sym_eq_data env ind in + let sym = mkConst (find_scheme sym_scheme_kind ind) in + let (eq,eqrefl) = get_coq_eq () in + let cstr n = mkApp (mkConstruct(ind,1),extended_rel_vect n paramsctxt) in + let varH = fresh env (default_id_of_sort (snd (mind_arity mip))) in + let applied_ind = build_dependent_inductive ind specif in + let applied_ind_C = + mkApp + (mkInd ind, Array.append + (extended_rel_vect (nrealargs+1) mib.mind_params_ctxt) + (rel_vect (nrealargs+1) nrealargs)) in + let realsign_ind = + name_context env ((Name varH,None,applied_ind)::realsign) in + let ci = make_case_info (Global.env()) ind RegularStyle in + (my_it_mkLambda_or_LetIn paramsctxt + (my_it_mkLambda_or_LetIn_name realsign_ind + (mkCase (ci, + my_it_mkLambda_or_LetIn_name + (lift_rel_context (nrealargs+1) realsign_ind) + (mkApp (eq,[| + mkApp + (mkInd ind, Array.concat + [extended_rel_vect (3*nrealargs+2) paramsctxt1; + rel_vect (2*nrealargs+2) nrealargs; + rel_vect 1 nrealargs]); + mkApp (sym,Array.concat + [extended_rel_vect (3*nrealargs+2) paramsctxt1; + rel_vect 1 nrealargs; + rel_vect (2*nrealargs+2) nrealargs; + [|mkApp (sym,Array.concat + [extended_rel_vect (3*nrealargs+2) paramsctxt1; + rel_vect (2*nrealargs+2) nrealargs; + rel_vect 1 nrealargs; + [|mkRel 1|]])|]]); + mkRel 1|])), + mkRel 1 (* varH *), + [|mkApp(eqrefl,[|applied_ind_C;cstr (nrealargs+1)|])|])))) + +let sym_involutive_scheme_kind = + declare_individual_scheme_object "_sym_involutive" + (fun ind -> build_sym_involutive_scheme (Global.env() (* side-effect! *)) ind) + +(**********************************************************************) +(* Build the left-to-right rewriting lemma for conclusion associated *) +(* to an inductive type I q1..qm,p1..pn a1..an with one constructor *) +(* C : I q1..qm,p1..pn p1..pn *) +(* (symmetric equality in non-dependent and dependent cases) *) +(* *) +(* We could have defined the scheme in one match over a generalized *) +(* type but this behaves badly wrt the guard condition, so we use *) +(* symmetry instead; with commutative-cuts-aware guard condition a *) +(* proof in the style of l2r_forward is also possible (see below) *) +(* *) +(* rew := fun q1..qm p1..pn a1..an *) +(* (P:forall p1..pn, I q1..qm p1..pn a1..an -> kind) *) +(* (HC:P a1..an C) *) +(* (H:I q1..qm p1..pn a1..an) => *) +(* match sym_involutive q1..qm p1..pn a1..an H as Heq *) +(* in _ = H return P p1..pn H *) +(* with *) +(* refl => *) +(* match sym q1..qm p1..pn a1..an H as H *) +(* in I _.._ p1..pn *) +(* return P p1..pn (sym q1..qm a1..an p1..pn H) *) +(* with *) +(* C => HC *) +(* end *) +(* end *) +(* : forall q1..qn p1..pn a1..an *) +(* (P:forall p1..pn, I q1..qm p1..pn a1..an -> kind), *) +(* P a1..an C -> *) +(* forall (H:I q1..qm p1..pn a1..an), P p1..pn H *) +(* *) +(* where A1..An are the common types of p1..pn and a1..an *) +(* *) +(* Note: the symmetry is needed in the dependent case since the *) +(* dependency is on the inner arguments (the indices in C) and these *) +(* inner arguments need to be visible as parameters to be able to *) +(* abstract over them in P. *) +(**********************************************************************) + +(**********************************************************************) +(* For information, the alternative proof of dependent l2r_rew scheme *) +(* that would use commutative cuts is the following *) +(* *) +(* rew := fun q1..qm p1..pn a1..an *) +(* (P:forall p1..pn, I q1..qm p1..pn a1..an -> kind) *) +(* (HC:P a1..an C) *) +(* (H:I q1..qm p1..pn a1..an) => *) +(* match H in I .._.. a1..an return *) +(* forall p1..pn, I q1..qm p1..pn a1..an -> kind), *) +(* P a1..an C -> P p1..pn H *) +(* with *) +(* C => fun P HC => HC *) +(* end P HC *) +(* : forall q1..qn p1..pn a1..an *) +(* (P:forall p1..pn, I q1..qm p1..pn a1..an -> kind), *) +(* P a1..an C -> *) +(* forall (H:I q1..qm p1..pn a1..an), P p1..pn H *) +(* *) +(**********************************************************************) + +let build_l2r_rew_scheme dep env ind kind = + let (mib,mip as specif),nrealargs,realsign,paramsctxt,paramsctxt1 = + get_sym_eq_data env ind in + let sym = mkConst (find_scheme sym_scheme_kind ind) in + let sym_involutive = mkConst (find_scheme sym_involutive_scheme_kind ind) in + let (eq,eqrefl) = get_coq_eq () in + let cstr n p = + mkApp (mkConstruct(ind,1), + Array.concat [extended_rel_vect n paramsctxt1; + rel_vect p nrealargs]) in + let varH = fresh env (default_id_of_sort (snd (mind_arity mip))) in + let varHC = fresh env (id_of_string "HC") in + let varP = fresh env (id_of_string "P") in + let applied_ind = build_dependent_inductive ind specif in + let applied_ind_P = + mkApp (mkInd ind, Array.concat + [extended_rel_vect (3*nrealargs) paramsctxt1; + rel_vect 0 nrealargs; + rel_vect nrealargs nrealargs]) in + let applied_ind_G = + mkApp (mkInd ind, Array.concat + [extended_rel_vect (3*nrealargs+3) paramsctxt1; + rel_vect (nrealargs+3) nrealargs; + rel_vect 0 nrealargs]) in + let realsign_P = lift_rel_context nrealargs realsign in + let realsign_ind_P = + name_context env ((Name varH,None,applied_ind_P)::realsign_P) in + let realsign_ind_G = + name_context env ((Name varH,None,applied_ind_G):: + lift_rel_context (nrealargs+3) realsign) in + let applied_sym_C n = + mkApp(sym, + Array.append (extended_rel_vect n mip.mind_arity_ctxt) [|mkVar varH|]) in + let applied_sym_G = + mkApp(sym, + Array.concat [extended_rel_vect (nrealargs*3+4) paramsctxt1; + rel_vect (nrealargs+4) nrealargs; + rel_vect 1 nrealargs; + [|mkRel 1|]]) in + let s = mkSort (new_sort_in_family kind) in + let ci = make_case_info (Global.env()) ind RegularStyle in + let cieq = make_case_info (Global.env()) (destInd eq) RegularStyle in + let applied_PC = + mkApp (mkVar varP,Array.append (extended_rel_vect 1 realsign) + (if dep then [|cstr (2*nrealargs+1) 1|] else [||])) in + let applied_PG = + mkApp (mkVar varP,Array.append (rel_vect 1 nrealargs) + (if dep then [|applied_sym_G|] else [||])) in + let applied_PR = + mkApp (mkVar varP,Array.append (rel_vect (nrealargs+5) nrealargs) + (if dep then [|mkRel 2|] else [||])) in + let applied_sym_sym = + mkApp (sym,Array.concat + [extended_rel_vect (2*nrealargs+4) paramsctxt1; + rel_vect 4 nrealargs; + rel_vect (nrealargs+4) nrealargs; + [|mkApp (sym,Array.concat + [extended_rel_vect (2*nrealargs+4) paramsctxt1; + 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) + (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 left-to-right rewriting lemma for hypotheses associated *) +(* to an inductive type I q1..qm,p1..pn a1..an with one constructor *) +(* C : I q1..qm,p1..pn p1..pn *) +(* (symmetric equality in non dependent and dependent cases) *) +(* *) +(* rew := fun q1..qm p1..pn a1..an (H:I q1..qm p1..pn a1..an) *) +(* match H in I _.._ a1..an *) +(* return forall *) +(* (P:forall p1..pn, I q1..qm p1..pn a1..an -> kind) *) +(* (HC:P p1..pn H) => *) +(* P a1..an C *) +(* with *) +(* C => fun P HC => HC *) +(* end *) +(* : forall q1..qm p1..pn a1..an *) +(* (H:I q1..qm p1..pn a1..an) *) +(* (P:forall p1..pn, I q1..qm p1..pn a1..an ->kind), *) +(* P p1..pn H -> P a1..an C *) +(* *) +(* Note: the symmetry is needed in the dependent case since the *) +(* dependency is on the inner arguments (the indices in C) and these *) +(* inner arguments need to be visible as parameters to be able to *) +(* abstract over them in P. *) +(**********************************************************************) + +let build_l2r_forward_rew_scheme dep env ind kind = + let (mib,mip as specif),nrealargs,realsign,paramsctxt,paramsctxt1 = + get_sym_eq_data env ind in + let cstr n p = + mkApp (mkConstruct(ind,1), + Array.concat [extended_rel_vect n paramsctxt1; + rel_vect p nrealargs]) in + let varH = fresh env (default_id_of_sort (snd (mind_arity mip))) in + let varHC = fresh env (id_of_string "HC") in + let varP = fresh env (id_of_string "P") in + let applied_ind = build_dependent_inductive ind specif in + let applied_ind_P = + mkApp (mkInd ind, Array.concat + [extended_rel_vect (4*nrealargs+2) paramsctxt1; + rel_vect 0 nrealargs; + rel_vect (nrealargs+1) nrealargs]) in + let applied_ind_P' = + mkApp (mkInd ind, Array.concat + [extended_rel_vect (3*nrealargs+1) paramsctxt1; + rel_vect 0 nrealargs; + rel_vect (2*nrealargs+1) nrealargs]) in + let realsign_P n = lift_rel_context (nrealargs*n+n) realsign in + let realsign_ind = + name_context env ((Name varH,None,applied_ind)::realsign) in + let realsign_ind_P n aP = + name_context env ((Name varH,None,aP)::realsign_P n) in + let s = mkSort (new_sort_in_family kind) in + let ci = make_case_info (Global.env()) ind RegularStyle in + let applied_PC = + mkApp (mkVar varP,Array.append + (rel_vect (nrealargs*2+3) nrealargs) + (if dep then [|mkRel 2|] else [||])) in + let applied_PC' = + mkApp (mkVar varP,Array.append + (rel_vect (nrealargs+2) nrealargs) + (if dep then [|cstr (2*nrealargs+2) (nrealargs+2)|] + else [||])) in + let applied_PG = + mkApp (mkVar varP,Array.append (rel_vect 3 nrealargs) + (if dep then [|cstr (3*nrealargs+4) 3|] else [||])) in + (my_it_mkLambda_or_LetIn mib.mind_params_ctxt + (my_it_mkLambda_or_LetIn_name realsign + (mkNamedLambda varH applied_ind + (mkCase (ci, + my_it_mkLambda_or_LetIn_name + (lift_rel_context (nrealargs+1) realsign_ind) + (mkNamedProd varP + (my_it_mkProd_or_LetIn + (if dep then realsign_ind_P 2 applied_ind_P else realsign_P 2) s) + (mkNamedProd varHC applied_PC applied_PG)), + (mkVar varH), + [|mkNamedLambda varP + (my_it_mkProd_or_LetIn + (if dep then realsign_ind_P 1 applied_ind_P' else realsign_P 2) s) + (mkNamedLambda varHC applied_PC' + (mkVar varHC))|]))))) + +(**********************************************************************) +(* Build the right-to-left rewriting lemma for hypotheses associated *) +(* to an inductive type I q1..qm a1..an with one constructor *) +(* C : I q1..qm b1..bn *) +(* (arbitrary equality in non-dependent and dependent cases) *) +(* *) +(* rew := fun q1..qm a1..an (H:I q1..qm a1..an) *) +(* (P:forall a1..an, I q1..qm a1..an -> kind) *) +(* (HC:P a1..an H) => *) +(* match H in I _.._ a1..an return P a1..an H -> P b1..bn C *) +(* with *) +(* C => fun x => x *) +(* end HC *) +(* : forall q1..pm a1..an (H:I q1..qm a1..an) *) +(* (P:forall a1..an, I q1..qm a1..an -> kind), *) +(* P a1..an H -> P b1..bn C *) +(* *) +(* Note that the dependent elimination here is not a dependency *) +(* in the conclusion of the scheme but a dependency in the premise of *) +(* the scheme. This is unfortunately incompatible with the standard *) +(* pattern for schemes in Coq which expects that the eliminated *) +(* object is the last premise of the scheme. We then have no choice *) +(* than following the more liberal pattern of having the eliminated *) +(* object coming before the premises. *) +(* *) +(* Note that in the non-dependent case, this scheme (up to the order *) +(* of premises) generalizes the (backward) l2r scheme above: same *) +(* statement but no need for symmetry of the equality. *) +(**********************************************************************) + +let build_r2l_forward_rew_scheme dep env ind kind = + let ((mib,mip as specif),constrargs,realsign,nrealargs) = + get_non_sym_eq_data env ind in + let cstr n = + mkApp (mkConstruct(ind,1),extended_rel_vect n mib.mind_params_ctxt) in + let constrargs_cstr = constrargs@[cstr 0] in + let varH = fresh env (default_id_of_sort (snd (mind_arity mip))) in + let varHC = fresh env (id_of_string "HC") in + let varP = fresh env (id_of_string "P") in + let applied_ind = build_dependent_inductive ind specif in + let realsign_ind = + name_context env ((Name varH,None,applied_ind)::realsign) in + let s = mkSort (new_sort_in_family kind) in + let ci = make_case_info (Global.env()) ind RegularStyle in + let applied_PC = + applist (mkVar varP,if dep then constrargs_cstr else constrargs) in + let applied_PG = + mkApp (mkVar varP, + if dep then extended_rel_vect 0 realsign_ind + else extended_rel_vect 1 realsign) in + (my_it_mkLambda_or_LetIn mib.mind_params_ctxt + (my_it_mkLambda_or_LetIn_name realsign_ind + (mkNamedLambda varP + (my_it_mkProd_or_LetIn (lift_rel_context (nrealargs+1) + (if dep then realsign_ind else realsign)) s) + (mkNamedLambda varHC (lift 1 applied_PG) + (mkApp + (mkCase (ci, + my_it_mkLambda_or_LetIn_name + (lift_rel_context (nrealargs+3) realsign_ind) + (mkArrow applied_PG (lift (2*nrealargs+5) applied_PC)), + mkRel 3 (* varH *), + [|mkLambda + (Name varHC, + lift (nrealargs+3) applied_PC, + mkRel 1)|]), + [|mkVar varHC|])))))) + +(**********************************************************************) +(* This function "repairs" the non-dependent r2l forward rewriting *) +(* scheme by making it comply with the standard pattern of schemes *) +(* in Coq. Otherwise said, it turns a scheme of type *) +(* *) +(* forall q1..pm a1..an, I q1..qm a1..an -> *) +(* forall (P: forall a1..an, kind), *) +(* P a1..an -> P b1..bn *) +(* *) +(* into a scheme of type *) +(* *) +(* forall q1..pm (P:forall a1..an, kind), *) +(* P a1..an -> forall a1..an, I q1..qm a1..an -> P b1..bn *) +(* *) +(**********************************************************************) + +let fix_r2l_forward_rew_scheme c = + let t = Retyping.get_type_of (Global.env()) Evd.empty c in + let ctx,_ = decompose_prod_assum t in + match ctx with + | hp :: p :: ind :: indargs -> + my_it_mkLambda_or_LetIn indargs + (mkLambda_or_LetIn (map_rel_declaration (liftn (-1) 1) p) + (mkLambda_or_LetIn (map_rel_declaration (liftn (-1) 2) hp) + (mkLambda_or_LetIn (map_rel_declaration (lift 2) ind) + (Reductionops.whd_beta Evd.empty + (applist (c, + extended_rel_list 3 indargs @ [mkRel 1;mkRel 3;mkRel 2])))))) + | _ -> anomaly "Ill-formed non-dependent left-to-right rewriting scheme" + +(**********************************************************************) +(* Build the right-to-left rewriting lemma for conclusion associated *) +(* to an inductive type I q1..qm a1..an with one constructor *) +(* C : I q1..qm b1..bn *) +(* (arbitrary equality in non-dependent and dependent case) *) +(* *) +(* This is actually the standard case analysis scheme *) +(* *) +(* rew := fun q1..qm a1..an *) +(* (P:forall a1..an, I q1..qm a1..an -> kind) *) +(* (H:I q1..qm a1..an) *) +(* (HC:P b1..bn C) => *) +(* match H in I _.._ a1..an return P a1..an H with *) +(* C => HC *) +(* end *) +(* : forall q1..pm a1..an *) +(* (P:forall a1..an, I q1..qm a1..an -> kind) *) +(* (H:I q1..qm a1..an), *) +(* P b1..bn C -> P a1..an H *) +(**********************************************************************) + +let build_r2l_rew_scheme dep env ind k = + build_case_analysis_scheme env Evd.empty ind dep k + +(**********************************************************************) +(* Register the rewriting schemes *) +(**********************************************************************) + +(**********************************************************************) +(* Dependent rewrite from left-to-right in conclusion *) +(* (symmetrical equality type only) *) +(* Gamma |- P p1..pn H ==> Gamma |- P a1..an C *) +(* with H:I p1..pn a1..an in Gamma *) +(**********************************************************************) +let rew_l2r_dep_scheme_kind = + declare_individual_scheme_object "_rew_r_dep" + (fun ind -> build_l2r_rew_scheme true (Global.env()) ind InType) + +(**********************************************************************) +(* Dependent rewrite from right-to-left in conclusion *) +(* Gamma |- P a1..an H ==> Gamma |- P b1..bn C *) +(* with H:I a1..an in Gamma (non symmetric case) *) +(* or H:I b1..bn a1..an in Gamma (symmetric case) *) +(**********************************************************************) +let rew_r2l_dep_scheme_kind = + declare_individual_scheme_object "_rew_dep" + (fun ind -> build_r2l_rew_scheme true (Global.env()) ind InType) + +(**********************************************************************) +(* Dependent rewrite from right-to-left in hypotheses *) +(* Gamma, P a1..an H |- D ==> Gamma, P b1..bn C |- D *) +(* with H:I a1..an in Gamma (non symmetric case) *) +(* or H:I b1..bn a1..an in Gamma (symmetric case) *) +(**********************************************************************) +let rew_r2l_forward_dep_scheme_kind = + declare_individual_scheme_object "_rew_fwd_dep" + (fun ind -> build_r2l_forward_rew_scheme true (Global.env()) ind InType) + +(**********************************************************************) +(* Dependent rewrite from left-to-right in hypotheses *) +(* (symmetrical equality type only) *) +(* Gamma, P p1..pn H |- D ==> Gamma, P a1..an C |- D *) +(* with H:I p1..pn a1..an in Gamma *) +(**********************************************************************) +let rew_l2r_forward_dep_scheme_kind = + declare_individual_scheme_object "_rew_fwd_r_dep" + (fun ind -> build_l2r_forward_rew_scheme true (Global.env()) ind InType) + +(**********************************************************************) +(* Non-dependent rewrite from either left-to-right in conclusion or *) +(* right-to-left in hypotheses: both l2r_rew and r2l_forward_rew are *) +(* potential candidates. However r2l_forward_rew introduces a blocked *) +(* beta-expansion that blocks in turn the guard condition if this *) +(* one does not support commutative cuts while l2r_rew does not *) +(* support non symmetrical equalities, so... *) +(**********************************************************************) + +(**********************************************************************) +(* ... we use l2r_rew for the symmetrical case: *) +(**********************************************************************) +let rew_l2r_scheme_kind = + declare_individual_scheme_object "_rew_r" + (fun ind -> build_l2r_rew_scheme false (Global.env()) ind InType) + +(**********************************************************************) +(* ... and r2l_forward_rew for the non-symmetrical case, even though *) +(* it may break the guard condition. Moreover, its standard form *) +(* needs the inductive hypothesis not in last position what breaks *) +(* the order of goals and need a fix: *) +(**********************************************************************) +let rew_asym_scheme_kind = + declare_individual_scheme_object "_rew_r_asym" + (fun ind -> fix_r2l_forward_rew_scheme + (build_r2l_forward_rew_scheme false (Global.env()) ind InType)) + +(**********************************************************************) +(* Non-dependent rewrite from either right-to-left in conclusion or *) +(* left-to-right in hypotheses: both r2l_rew and l2r_forward_rew but *) +(* since r2l_rew works in the non-symmetric case as well as without *) +(* introducing commutative cuts, we adopt it *) +(**********************************************************************) +let rew_r2l_scheme_kind = + declare_individual_scheme_object "_rew" + (fun ind -> build_r2l_rew_scheme false (Global.env()) ind InType) + +(* End of rewriting schemes *) + +(**********************************************************************) +(* Build the congruence lemma associated to an inductive type *) +(* I p1..pn a with one constructor C : I q1..qn b *) +(* *) +(* congr := fun p1..pn (B:Type) (f:A->B) a (H:I p1..pn a) => *) +(* match H in I _.._ a' return f b = f a' with *) +(* C => eq_refl (f b) *) +(* end *) +(* : forall p1..pn (B:Type) (f:A->B) a, I p1..pn a -> f b = f a *) +(* *) +(* where A is the common type of a and b *) +(**********************************************************************) + +(* TODO: extend it to types with more than one index *) + +let build_congr env (eq,refl) ind = + let (mib,mip) = lookup_mind_specif env ind in + if Array.length mib.mind_packets <> 1 or Array.length mip.mind_nf_lc <> 1 then + error "Not an inductive type with a single constructor."; + if mip.mind_nrealargs <> 1 then + error "Expect an inductive type with one predicate parameter."; + let i = 1 in + let realsign,_ = list_chop mip.mind_nrealargs_ctxt mip.mind_arity_ctxt in + if List.exists (fun (_,b,_) -> b <> None) realsign then + error "Inductive equalities with local definitions in arity not supported."; + let env_with_arity = push_rel_context mip.mind_arity_ctxt env in + let (_,_,ty) = lookup_rel (mip.mind_nrealargs - i + 1) env_with_arity in + let constrsign,ccl = decompose_prod_assum mip.mind_nf_lc.(0) in + let _,constrargs = decompose_app ccl in + if rel_context_length constrsign<>rel_context_length mib.mind_params_ctxt then + error "Constructor must have no arguments"; + let b = List.nth constrargs (i + mib.mind_nparams - 1) in + let varB = fresh env (id_of_string "B") in + let varH = fresh env (id_of_string "H") in + let varf = fresh env (id_of_string "f") in + let ci = make_case_info (Global.env()) ind RegularStyle in + my_it_mkLambda_or_LetIn mib.mind_params_ctxt + (mkNamedLambda varB (new_Type ()) + (mkNamedLambda varf (mkArrow (lift 1 ty) (mkVar varB)) + (my_it_mkLambda_or_LetIn_name (lift_rel_context 2 realsign) + (mkNamedLambda varH + (applist + (mkInd ind, + extended_rel_list (mip.mind_nrealargs+2) mib.mind_params_ctxt @ + extended_rel_list 0 realsign)) + (mkCase (ci, + my_it_mkLambda_or_LetIn_name + (lift_rel_context (mip.mind_nrealargs+3) realsign) + (mkLambda + (Anonymous, + applist + (mkInd ind, + extended_rel_list (2*mip.mind_nrealargs_ctxt+3) + mib.mind_params_ctxt + @ extended_rel_list 0 realsign), + mkApp (eq, + [|mkVar varB; + mkApp (mkVar varf, [|lift (2*mip.mind_nrealargs_ctxt+4) b|]); + mkApp (mkVar varf, [|mkRel (mip.mind_nrealargs - i + 2)|])|]))), + mkVar varH, + [|mkApp (refl, + [|mkVar varB; + mkApp (mkVar varf, [|lift (mip.mind_nrealargs+3) b|])|])|])))))) + +let congr_scheme_kind = declare_individual_scheme_object "_congr" + (fun ind -> + (* May fail if equality is not defined *) + build_congr (Global.env()) (get_coq_eq ()) ind) -- cgit v1.2.3