diff options
author | 2006-12-23 18:11:18 +0000 | |
---|---|---|
committer | 2006-12-23 18:11:18 +0000 | |
commit | 03eaad01a90813c8656b0306888644106939f537 (patch) | |
tree | 45304597a0a7c0dad50366adb4b90e932610ad67 | |
parent | 1f578ef558355e48db8ae15e6ccad1a2f5d089f9 (diff) |
Addition of a "Combined Scheme" vernacular command for building the conjunction of mutual inductions principles.
e.g: Combined Scheme mutind from tree_ind, forest_ind gives a conclusion (forall t : tree, P t) /\ (forall f : forest, P0 f).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9461 85f007b7-540e-0410-9357-904b9bb8a0f7
-rw-r--r-- | .depend.coq | 6 | ||||
-rw-r--r-- | interp/coqlib.ml | 2 | ||||
-rw-r--r-- | interp/coqlib.mli | 1 | ||||
-rw-r--r-- | parsing/g_vernac.ml4 | 4 | ||||
-rw-r--r-- | parsing/ppvernac.ml | 5 | ||||
-rw-r--r-- | toplevel/command.ml | 52 | ||||
-rw-r--r-- | toplevel/command.mli | 2 | ||||
-rw-r--r-- | toplevel/vernacentries.ml | 3 | ||||
-rw-r--r-- | toplevel/vernacexpr.ml | 1 |
9 files changed, 72 insertions, 4 deletions
diff --git a/.depend.coq b/.depend.coq index 832ddc198..ef98c6a5a 100644 --- a/.depend.coq +++ b/.depend.coq @@ -28,7 +28,7 @@ theories/FSets/FMapAVL.vo: theories/FSets/FMapAVL.v theories/FSets/FSetInterface theories/FSets/FSetAVL.vo: theories/FSets/FSetAVL.v theories/FSets/FSetInterface.vo theories/FSets/FSetList.vo theories/ZArith/ZArith.vo theories/ZArith/Int.vo theories/Reals/Rdefinitions.vo: theories/Reals/Rdefinitions.v theories/ZArith/ZArith_base.vo theories/Reals/Raxioms.vo: theories/Reals/Raxioms.v theories/ZArith/ZArith_base.vo theories/Reals/Rdefinitions.vo -theories/Reals/RIneq.vo: theories/Reals/RIneq.v theories/Reals/Raxioms.vo contrib/setoid_ring/ZArithRing.vo contrib/omega/Omega.vo contrib/setoid_ring/RealField.vo +theories/Reals/RIneq.vo: theories/Reals/RIneq.v theories/Reals/Raxioms.vo theories/Reals/Rpow_def.vo theories/ZArith/Zpower.vo contrib/setoid_ring/ZArithRing.vo contrib/omega/Omega.vo contrib/setoid_ring/RealField.vo theories/Reals/DiscrR.vo: theories/Reals/DiscrR.v theories/Reals/RIneq.vo contrib/omega/Omega.vo theories/Reals/Rbase.vo: theories/Reals/Rbase.v theories/Reals/Rdefinitions.vo theories/Reals/Raxioms.vo theories/Reals/RIneq.vo theories/Reals/DiscrR.vo theories/Reals/LegacyRfield.vo: theories/Reals/LegacyRfield.v theories/Reals/Raxioms.vo contrib/field/LegacyField.vo @@ -267,7 +267,7 @@ theories/Relations/Rstar.vo: theories/Relations/Rstar.v theories/Wellfounded/Disjoint_Union.vo: theories/Wellfounded/Disjoint_Union.v theories/Relations/Relation_Operators.vo theories/Wellfounded/Inclusion.vo: theories/Wellfounded/Inclusion.v theories/Relations/Relation_Definitions.vo theories/Wellfounded/Inverse_Image.vo: theories/Wellfounded/Inverse_Image.v -theories/Wellfounded/Lexicographic_Exponentiation.vo: theories/Wellfounded/Lexicographic_Exponentiation.v theories/Logic/Eqdep.vo theories/Lists/List.vo theories/Relations/Relation_Operators.vo theories/Wellfounded/Transitive_Closure.vo +theories/Wellfounded/Lexicographic_Exponentiation.vo: theories/Wellfounded/Lexicographic_Exponentiation.v theories/Lists/List.vo theories/Relations/Relation_Operators.vo theories/Wellfounded/Transitive_Closure.vo theories/Wellfounded/Transitive_Closure.vo: theories/Wellfounded/Transitive_Closure.v theories/Relations/Relation_Definitions.vo theories/Relations/Relation_Operators.vo theories/Wellfounded/Union.vo: theories/Wellfounded/Union.v theories/Relations/Relation_Operators.vo theories/Relations/Relation_Definitions.vo theories/Wellfounded/Transitive_Closure.vo theories/Wellfounded/Wellfounded.vo: theories/Wellfounded/Wellfounded.v theories/Wellfounded/Disjoint_Union.vo theories/Wellfounded/Inclusion.vo theories/Wellfounded/Inverse_Image.vo theories/Wellfounded/Lexicographic_Exponentiation.vo theories/Wellfounded/Lexicographic_Product.vo theories/Wellfounded/Transitive_Closure.vo theories/Wellfounded/Union.vo theories/Wellfounded/Well_Ordering.vo @@ -275,7 +275,7 @@ theories/Wellfounded/Well_Ordering.vo: theories/Wellfounded/Well_Ordering.v theo theories/Wellfounded/Lexicographic_Product.vo: theories/Wellfounded/Lexicographic_Product.v theories/Logic/Eqdep.vo theories/Relations/Relation_Operators.vo theories/Wellfounded/Transitive_Closure.vo theories/Reals/Rdefinitions.vo: theories/Reals/Rdefinitions.v theories/ZArith/ZArith_base.vo theories/Reals/Raxioms.vo: theories/Reals/Raxioms.v theories/ZArith/ZArith_base.vo theories/Reals/Rdefinitions.vo -theories/Reals/RIneq.vo: theories/Reals/RIneq.v theories/Reals/Raxioms.vo contrib/setoid_ring/ZArithRing.vo contrib/omega/Omega.vo contrib/setoid_ring/RealField.vo +theories/Reals/RIneq.vo: theories/Reals/RIneq.v theories/Reals/Raxioms.vo theories/Reals/Rpow_def.vo theories/ZArith/Zpower.vo contrib/setoid_ring/ZArithRing.vo contrib/omega/Omega.vo contrib/setoid_ring/RealField.vo theories/Reals/DiscrR.vo: theories/Reals/DiscrR.v theories/Reals/RIneq.vo contrib/omega/Omega.vo theories/Reals/Rbase.vo: theories/Reals/Rbase.v theories/Reals/Rdefinitions.vo theories/Reals/Raxioms.vo theories/Reals/RIneq.vo theories/Reals/DiscrR.vo theories/Reals/LegacyRfield.vo: theories/Reals/LegacyRfield.v theories/Reals/Raxioms.vo contrib/field/LegacyField.vo diff --git a/interp/coqlib.ml b/interp/coqlib.ml index cfde10202..5952d3503 100644 --- a/interp/coqlib.ml +++ b/interp/coqlib.ml @@ -236,6 +236,7 @@ let coq_I = lazy_init_constant ["Logic"] "I" (* Connectives *) let coq_not = lazy_init_constant ["Logic"] "not" let coq_and = lazy_init_constant ["Logic"] "and" +let coq_conj = lazy_init_constant ["Logic"] "conj" let coq_or = lazy_init_constant ["Logic"] "or" let coq_ex = lazy_init_constant ["Logic"] "ex" @@ -246,6 +247,7 @@ let build_coq_I () = Lazy.force coq_I let build_coq_False () = Lazy.force coq_False let build_coq_not () = Lazy.force coq_not let build_coq_and () = Lazy.force coq_and +let build_coq_conj () = Lazy.force coq_conj let build_coq_or () = Lazy.force coq_or let build_coq_ex () = Lazy.force coq_ex diff --git a/interp/coqlib.mli b/interp/coqlib.mli index 098dad1d5..0a37eefbd 100644 --- a/interp/coqlib.mli +++ b/interp/coqlib.mli @@ -129,6 +129,7 @@ val build_coq_not : constr delayed (* Conjunction *) val build_coq_and : constr delayed +val build_coq_conj : constr delayed (* Disjunction *) val build_coq_or : constr delayed diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index ad42304ce..356c05e8f 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -143,7 +143,9 @@ GEXTEND Gram VernacFixpoint (recs,Options.boxed_definitions()) | "CoFixpoint"; corecs = LIST1 corec_definition SEP "with" -> VernacCoFixpoint (corecs,false) - | IDENT "Scheme"; l = LIST1 scheme SEP "with" -> VernacScheme l ] ] + | IDENT "Scheme"; l = LIST1 scheme SEP "with" -> VernacScheme l + | IDENT "Combined"; IDENT "Scheme"; id = identref; IDENT "from"; + l = LIST1 identref SEP "," -> VernacCombinedScheme (id, l) ] ] ; gallina_ext: [ [ b = record_token; oc = opt_coercion; name = identref; diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml index c74922351..6213e4fda 100644 --- a/parsing/ppvernac.ml +++ b/parsing/ppvernac.ml @@ -602,6 +602,11 @@ let rec pr_vernac = function | VernacScheme l -> hov 2 (str"Scheme" ++ spc() ++ prlist_with_sep (fun _ -> fnl() ++ str"with ") pr_onescheme l) + | VernacCombinedScheme (id, l) -> + hov 2 (str"Combined Scheme" ++ spc() ++ + pr_lident id ++ spc() ++ str"from" ++ spc() ++ + prlist_with_sep (fun _ -> fnl() ++ str", ") pr_lident l) + (* Gallina extensions *) | VernacRecord (b,(oc,name),ps,s,c,fs) -> diff --git a/toplevel/command.ml b/toplevel/command.ml index ff5b3bd3b..756ae31b6 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -656,6 +656,58 @@ let build_scheme lnamedepindsort = let _ = List.fold_right2 declare listdecl lrecnames [] in if_verbose ppnl (recursive_message Fixpoint lrecnames) +let rec get_concl n t = + if n = 0 then t + else + match kind_of_term t with + Prod (_,_,t) -> get_concl (pred n) t + | _ -> raise (Invalid_argument "get_concl") + +let cut_last l = + let rec aux acc = function + hd :: [] -> List.rev acc, hd + | hd :: tl -> aux (hd :: acc) tl + | [] -> raise (Invalid_argument "cut_last") + in aux [] l + +let build_combined_scheme name schemes = + let env = Global.env () in + let defs = + List.map (fun x -> + let refe = Ident x in + let qualid = qualid_of_reference refe in + let cst = Nametab.locate_constant (snd qualid) in + qualid, cst, Typeops.type_of_constant env cst) + schemes + in + let (qid, c, t) = List.hd defs in + let nargs = + let (_, arity, _) = destProd t in + nb_prod arity + in + let prods = nb_prod t - nargs in + let defs, (qid, c, t) = cut_last defs in + let (args, concl) = decompose_prod_n prods t in + let concls = List.map (fun (_, cst, t) -> cst, get_concl prods t) defs in + let coqand = Coqlib.build_coq_and () and coqconj = Coqlib.build_coq_conj () in + let relargs = rel_vect 0 prods in + let concl_typ, concl_bod = + List.fold_right + (fun (cst, x) (acct, accb) -> + mkApp (coqand, [| x; acct |]), + mkApp (coqconj, [| x; acct; mkApp(mkConst cst, relargs); accb |])) + concls (concl, mkApp (mkConst c, relargs)) + in + let ctx = List.map (fun (x, y) -> x, None, y) args in + let typ = it_mkProd_wo_LetIn concl_typ ctx in + let body = it_mkLambda_or_LetIn concl_bod ctx in + let ce = { const_entry_body = body; + const_entry_type = Some typ; + const_entry_opaque = false; + const_entry_boxed = Options.boxed_definitions() } in + let _ = declare_constant (snd name) (DefinitionEntry ce, IsDefinition Scheme) in + if_verbose ppnl (recursive_message Fixpoint [snd name]) + (* 4| Goal declaration *) let start_proof id kind c hook = diff --git a/toplevel/command.mli b/toplevel/command.mli index 7c3d51946..c4ef92447 100644 --- a/toplevel/command.mli +++ b/toplevel/command.mli @@ -50,6 +50,8 @@ val build_corecursive : (cofixpoint_expr * decl_notation) list -> bool -> unit val build_scheme : (identifier located * bool * reference * rawsort) list -> unit +val build_combined_scheme : identifier located -> identifier located list -> unit + val generalize_constr_expr : constr_expr -> local_binder list -> constr_expr val start_proof : identifier -> goal_kind -> constr -> diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index db30d7b95..44e7cbad7 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -359,6 +359,8 @@ let vernac_cofixpoint = build_corecursive let vernac_scheme = build_scheme +let vernac_combined_scheme = build_combined_scheme + (**********************) (* Modules *) @@ -1135,6 +1137,7 @@ let interp c = match c with | VernacFixpoint (l,b) -> vernac_fixpoint l b | VernacCoFixpoint (l,b) -> vernac_cofixpoint l b | VernacScheme l -> vernac_scheme l + | VernacCombinedScheme (id, l) -> vernac_combined_scheme id l (* Modules *) | VernacDeclareModule (export,(_,id),bl,mtyo) -> diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml index a87221c75..ffde10192 100644 --- a/toplevel/vernacexpr.ml +++ b/toplevel/vernacexpr.ml @@ -199,6 +199,7 @@ type vernac_expr = | VernacFixpoint of (fixpoint_expr * decl_notation) list * bool | VernacCoFixpoint of (cofixpoint_expr * decl_notation) list * bool | VernacScheme of (lident * bool * lreference * sort_expr) list + | VernacCombinedScheme of lident * lident list (* Gallina extensions *) | VernacRecord of bool (* = Record or Structure *) |