diff options
| -rw-r--r-- | CHANGES | 2 | ||||
| -rw-r--r-- | doc/sphinx/proof-engine/tactics.rst | 1 | ||||
| -rw-r--r-- | doc/sphinx/user-extensions/proof-schemes.rst | 95 | ||||
| -rw-r--r-- | library/coqlib.ml | 6 | ||||
| -rw-r--r-- | library/coqlib.mli | 8 | ||||
| -rw-r--r-- | test-suite/success/CombinedScheme.v | 35 | ||||
| -rw-r--r-- | vernac/indschemes.ml | 29 |
7 files changed, 132 insertions, 44 deletions
@@ -164,6 +164,8 @@ Vernacular Commands scope. If you want the previous behavior, use `Global Set SsrHave NoTCResolution`. - Multiple sections with the same name are allowed. +- Combined Scheme can now work when inductive schemes are generated in sort + Type. It used to be limited to sort Prop. Coq binaries and process model diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst index f99c539251..db9f04ba11 100644 --- a/doc/sphinx/proof-engine/tactics.rst +++ b/doc/sphinx/proof-engine/tactics.rst @@ -2214,6 +2214,7 @@ and an explanation of the underlying technique. ``simple inversion``. .. tacv:: inversion @ident using @ident + :name: inversion ... using ... Let :n:`@ident` have type :g:`(I t)` (:g:`I` an inductive predicate) in the local context, and :n:`@ident` be a (dependent) inversion lemma. Then, this diff --git a/doc/sphinx/user-extensions/proof-schemes.rst b/doc/sphinx/user-extensions/proof-schemes.rst index 59cad3bea2..eacd7b4676 100644 --- a/doc/sphinx/user-extensions/proof-schemes.rst +++ b/doc/sphinx/user-extensions/proof-schemes.rst @@ -12,13 +12,15 @@ The ``Scheme`` command is a high-level tool for generating automatically (possibly mutual) induction principles for given types and sorts. Its syntax follows the schema: -.. cmd:: Scheme @ident := Induction for @ident Sort sort {* with @ident := Induction for @ident Sort sort} +.. cmd:: Scheme @ident__1 := Induction for @ident__2 Sort sort {* with @ident__i := Induction for @ident__j Sort sort} -where each `ident'ᵢ` is a different inductive type identifier -belonging to the same package of mutual inductive definitions. This -command generates the `identᵢ`s to be mutually recursive -definitions. Each term `identᵢ` proves a general principle of mutual -induction for objects in type `identᵢ`. + This command is a high-level tool for generating automatically + (possibly mutual) induction principles for given types and sorts. + Each :n:`@ident__j` is a different inductive type identifier belonging to + the same package of mutual inductive definitions. + The command generates the :n:`@ident__i`\s to be mutually recursive + definitions. Each term :n:`@ident__i` proves a general principle of mutual + induction for objects in type :n:`@ident__j`. .. cmdv:: Scheme @ident := Minimality for @ident Sort sort {* with @ident := Minimality for @ident' Sort sort} @@ -44,9 +46,9 @@ induction for objects in type `identᵢ`. .. coqtop:: none - Axiom A : Set. - Axiom B : Set. - + Axiom A : Set. + Axiom B : Set. + .. coqtop:: all Inductive tree : Set := node : A -> forest -> tree @@ -79,7 +81,7 @@ induction for objects in type `identᵢ`. .. coqtop:: all Inductive odd : nat -> Prop := oddS : forall n:nat, even n -> odd (S n) - with even : nat -> Prop := + with even : nat -> Prop := | evenO : even 0 | evenS : forall n:nat, odd n -> even (S n). @@ -136,19 +138,20 @@ Automatic declaration of schemes Combined Scheme ~~~~~~~~~~~~~~~~~~~~~~ -The ``Combined Scheme`` command is a tool for combining induction -principles generated by the ``Scheme command``. Its syntax follows the -schema : - -.. cmd:: Combined Scheme @ident from {+, ident} +.. cmd:: Combined Scheme @ident from {+, @ident__i} -where each identᵢ after the ``from`` is a different inductive principle that must -belong to the same package of mutual inductive principle definitions. -This command generates the leftmost `ident` to be the conjunction of the -principles: it is built from the common premises of the principles and -concluded by the conjunction of their conclusions. + This command is a tool for combining induction principles generated + by the :cmd:`Scheme` command. + Each :n:`@ident__i` is a different inductive principle that must belong + to the same package of mutual inductive principle definitions. + This command generates :n:`@ident` to be the conjunction of the + principles: it is built from the common premises of the principles + and concluded by the conjunction of their conclusions. + In the case where all the inductive principles used are in sort + ``Prop``, the propositional conjunction ``and`` is used, otherwise + the simple product ``prod`` is used instead. -.. example:: +.. example:: We can define the induction principles for trees and forests using: @@ -170,6 +173,23 @@ concluded by the conjunction of their conclusions. Check tree_forest_mutind. +.. example:: + + We can also combine schemes at sort ``Type``: + + .. coqtop:: all + + Scheme tree_forest_rect := Induction for tree Sort Type + with forest_tree_rect := Induction for forest Sort Type. + + .. coqtop:: all + + Combined Scheme tree_forest_mutrect from tree_forest_rect, forest_tree_rect. + + .. coqtop:: all + + Check tree_forest_mutrect. + .. _functional-scheme: Generation of induction principles with ``Functional`` ``Scheme`` @@ -186,7 +206,7 @@ schema: where each `ident'ᵢ` is a different mutually defined function name (the names must be in the same order as when they were defined). This command generates the induction principle for each `identᵢ`, following -the recursive structure and case analyses of the corresponding function +the recursive structure and case analyses of the corresponding function identᵢ’. .. warning:: @@ -196,7 +216,7 @@ identᵢ’. :cmd:`Function` generally produces smaller principles that are closer to how a user would implement them. See :ref:`advanced-recursive-functions` for details. -.. example:: +.. example:: Induction scheme for div2. @@ -262,11 +282,11 @@ identᵢ’. We define trees by the following mutual inductive type: .. original LaTeX had "Variable" instead of "Axiom", which generates an ugly warning - + .. coqtop:: reset all Axiom A : Set. - + Inductive tree : Set := node : A -> forest -> tree with forest : Set := @@ -313,20 +333,21 @@ identᵢ’. Check tree_size_ind2. .. _derive-inversion: - + Generation of inversion principles with ``Derive`` ``Inversion`` ----------------------------------------------------------------- -The syntax of ``Derive`` ``Inversion`` follows the schema: - .. cmd:: Derive Inversion @ident with forall (x : T), I t Sort sort -This command generates an inversion principle for the `inversion … using` -tactic. Let `I` be an inductive predicate and `x` the variables occurring -in t. This command generates and stocks the inversion lemma for the -sort `sort` corresponding to the instance `∀ (x:T), I t` with the name -`ident` in the global environment. When applied, it is equivalent to -having inverted the instance with the tactic `inversion`. + This command generates an inversion principle for the + :tacn:`inversion ... using ...` tactic. Let :g:`I` be an inductive + predicate and :g:`x` the variables occurring in t. This command + generates and stocks the inversion lemma for the sort :g:`sort` + corresponding to the instance :g:`∀ (x:T), I t` with the name + :n:`@ident` in the global environment. When applied, it is + equivalent to having inverted the instance with the tactic + :g:`inversion`. + .. cmdv:: Derive Inversion_clear @ident with forall (x:T), I t Sort sort @@ -347,7 +368,7 @@ having inverted the instance with the tactic `inversion`. Consider the relation `Le` over natural numbers and the following parameter ``P``: - + .. coqtop:: all Inductive Le : nat -> nat -> Set := @@ -370,9 +391,9 @@ having inverted the instance with the tactic `inversion`. .. coqtop:: none - Goal forall (n m : nat) (H : Le (S n) m), P n m. + Goal forall (n m : nat) (H : Le (S n) m), P n m. intros. - + .. coqtop:: all Show. diff --git a/library/coqlib.ml b/library/coqlib.ml index 36a9598f36..026b7aa316 100644 --- a/library/coqlib.ml +++ b/library/coqlib.ml @@ -349,6 +349,9 @@ let coq_iff = lazy_init_reference ["Logic"] "iff" let coq_iff_left_proj = lazy_init_reference ["Logic"] "proj1" let coq_iff_right_proj = lazy_init_reference ["Logic"] "proj2" +let coq_prod = lazy_init_reference ["Datatypes"] "prod" +let coq_pair = lazy_init_reference ["Datatypes"] "pair" + (* Runtime part *) let build_coq_True () = Lazy.force coq_True let build_coq_I () = Lazy.force coq_I @@ -364,6 +367,9 @@ let build_coq_iff () = Lazy.force coq_iff let build_coq_iff_left_proj () = Lazy.force coq_iff_left_proj let build_coq_iff_right_proj () = Lazy.force coq_iff_right_proj +let build_coq_prod () = Lazy.force coq_prod +let build_coq_pair () = Lazy.force coq_pair + (* The following is less readable but does not depend on parsing *) let coq_eq_ref = lazy (init_reference ["Logic"] "eq") diff --git a/library/coqlib.mli b/library/coqlib.mli index b4bd1b0e06..8844684957 100644 --- a/library/coqlib.mli +++ b/library/coqlib.mli @@ -101,7 +101,7 @@ val glob_jmeq : GlobRef.t at compile time. Therefore, we can only provide methods to build them at runtime. This is the purpose of the [constr delayed] and [constr_pattern delayed] types. Objects of this time needs to be - forced with [delayed_force] to get the actual constr or pattern + forced with [delayed_force] to get the actual constr or pattern at runtime. *) type coq_bool_data = { @@ -167,7 +167,7 @@ val build_coq_inversion_eq_true_data : coq_inversion_data delayed val build_coq_sumbool : GlobRef.t delayed (** {6 ... } *) -(** Connectives +(** Connectives The False proposition *) val build_coq_False : GlobRef.t delayed @@ -186,6 +186,10 @@ val build_coq_iff : GlobRef.t delayed val build_coq_iff_left_proj : GlobRef.t delayed val build_coq_iff_right_proj : GlobRef.t delayed +(** Pairs *) +val build_coq_prod : GlobRef.t delayed +val build_coq_pair : GlobRef.t delayed + (** Disjunction *) val build_coq_or : GlobRef.t delayed diff --git a/test-suite/success/CombinedScheme.v b/test-suite/success/CombinedScheme.v new file mode 100644 index 0000000000..d6ca7a299f --- /dev/null +++ b/test-suite/success/CombinedScheme.v @@ -0,0 +1,35 @@ +Inductive even (x : bool) : nat -> Type := +| evenO : even x 0 +| evenS : forall n, odd x n -> even x (S n) +with odd (x : bool) : nat -> Type := +| oddS : forall n, even x n -> odd x (S n). + +Scheme even_ind_prop := Induction for even Sort Prop +with odd_ind_prop := Induction for odd Sort Prop. + +Combined Scheme even_cprop from even_ind_prop, odd_ind_prop. + +Check even_cprop : + forall (x : bool) (P : forall n : nat, even x n -> Prop) + (P0 : forall n : nat, odd x n -> Prop), + P 0 (evenO x) -> + (forall (n : nat) (o : odd x n), P0 n o -> P (S n) (evenS x n o)) -> + (forall (n : nat) (e : even x n), P n e -> P0 (S n) (oddS x n e)) -> + (forall (n : nat) (e : even x n), P n e) /\ + (forall (n : nat) (o : odd x n), P0 n o). + +Scheme even_ind_type := Induction for even Sort Type +with odd_ind_type := Induction for odd Sort Type. + +(* This didn't work in v8.7 *) + +Combined Scheme even_ctype from even_ind_type, odd_ind_type. + +Check even_ctype : + forall (x : bool) (P : forall n : nat, even x n -> Prop) + (P0 : forall n : nat, odd x n -> Prop), + P 0 (evenO x) -> + (forall (n : nat) (o : odd x n), P0 n o -> P (S n) (evenS x n o)) -> + (forall (n : nat) (e : even x n), P n e -> P0 (S n) (oddS x n e)) -> + (forall (n : nat) (e : even x n), P n e) * + (forall (n : nat) (o : odd x n), P0 n o). diff --git a/vernac/indschemes.ml b/vernac/indschemes.ml index e86e108772..1ec15588ff 100644 --- a/vernac/indschemes.ml +++ b/vernac/indschemes.ml @@ -82,7 +82,7 @@ let _ = let is_eq_flag () = !eq_flag -let eq_dec_flag = ref false +let eq_dec_flag = ref false let _ = declare_bool_option { optdepr = false; @@ -375,7 +375,7 @@ let do_mutual_induction_scheme ?(force_mutual=false) lnamedepindsort = and env0 = Global.env() in let sigma, lrecspec, _ = List.fold_right - (fun (_,dep,ind,sort) (evd, l, inst) -> + (fun (_,dep,ind,sort) (evd, l, inst) -> let evd, indu, inst = match inst with | None -> @@ -445,6 +445,9 @@ let fold_left' f = function let mk_coq_and sigma = Evarutil.new_global sigma (Coqlib.build_coq_and ()) let mk_coq_conj sigma = Evarutil.new_global sigma (Coqlib.build_coq_conj ()) +let mk_coq_prod sigma = Evarutil.new_global sigma (Coqlib.build_coq_prod ()) +let mk_coq_pair sigma = Evarutil.new_global sigma (Coqlib.build_coq_pair ()) + let build_combined_scheme env schemes = let evdref = ref (Evd.from_env env) in let defs = List.map (fun cst -> @@ -462,10 +465,25 @@ let build_combined_scheme env schemes = in let (c, t) = List.hd defs in let ctx, ind, nargs = find_inductive t in + (* We check if ALL the predicates are in Prop, if so we use propositional + conjunction '/\', otherwise we use the simple product '*'. + *) + let inprop = + let inprop (_,t) = + Retyping.get_sort_family_of env !evdref (EConstr.of_constr t) + == Sorts.InProp + in + List.for_all inprop defs + in + let mk_and, mk_conj = + if inprop + then (mk_coq_and, mk_coq_conj) + else (mk_coq_prod, mk_coq_pair) + in (* Number of clauses, including the predicates quantification *) let prods = nb_prod !evdref (EConstr.of_constr t) - (nargs + 1) in - let sigma, coqand = mk_coq_and !evdref in - let sigma, coqconj = mk_coq_conj sigma in + let sigma, coqand = mk_and !evdref in + let sigma, coqconj = mk_conj sigma in let () = evdref := sigma in let relargs = rel_vect 0 prods in let concls = List.rev_map @@ -483,7 +501,8 @@ let build_combined_scheme env schemes = (List.rev_map (fun (x, y) -> LocalAssum (x, y)) ctx) in let typ = List.fold_left (fun d c -> Term.mkProd_wo_LetIn c d) concl_typ ctx in let body = it_mkLambda_or_LetIn concl_bod ctx in - (!evdref, body, typ) + let sigma = Typing.check env !evdref (EConstr.of_constr body) (EConstr.of_constr typ) in + (sigma, body, typ) let do_combined_scheme name schemes = let open CAst in |