package rocq-runtime

  1. Overview
  2. Docs
The Rocq Prover -- Core Binaries and Tools

Install 

dune-project
 Dependency

rocq-prover.org Readme Edit opam file Versions (5)

Authors

  1. T
    The Rocq development team, INRIA, CNRS, and contributors

Maintainers

  1. T
    The Rocq development team <rocq+rocq-development@discoursemail.com>

Sources

rocq-9.2.0.tar.gz
sha256=a45280ab4fbaac7540b136a6b073b4a6db15739ec1e149bded43fa6f4fc25f20

doc/rocq-runtime.tactics/AllScheme/index.html

Module AllSchemeSource

Strictly Positive Uniform Parameters
Sourceval compute_params_rec_strpos : Environ.env -> Names.MutInd.t -> Declarations.mutual_inductive_body -> bool list

Computes which uniform parameters are strictly positive in a mutual inductive body

Lookup All Predicate and its Theorem
Sourceval compute_positive_uparams_and_suffix : Environ.env -> Names.MutInd.t -> Declarations.mutual_inductive_body -> Names.Id.t list option -> bool list * (string * string) * (string * string)

Compute the default positivity of the uniform parameters, and generates the suffix for naming the all predicate, and its predicate, as well as the key for registering. If a positivity specification is given by users bool list option, it is checked to be included in the default one, and the suffix are modified accordingly.

Sourceval lookup_all_theorem : Names.inductive -> Names.inductive -> bool list -> (bool * Names.GlobRef.t * Names.GlobRef.t) option

Lookup the partial all predicate and its theorem for ind_nested for args_are_nested. If they are not found, lookup the general all predicate and its theorem. Returns if the partial all was found, and the global references. Raise a warning if none is found.

Instantiate the All Predicate and its Theorem
Sourceval make_all_predicate : partial_nesting:bool -> Names.GlobRef.t -> bool list -> EConstr.constr array -> EConstr.constr option array -> EConstr.constr array -> EConstr.constr -> EConstr.constr LibBinding.State.t

Make the all predicate for a fresh instance and using Typing.checked_appvect, given:

  • whether the all predicate is the partial one, or the general one partial_nesting:bool
  • the positivity of each uniform parameter bool list
  • the instantiation of the uniform parameter of the inductive type constr array
  • the instation of the fresh predicate constr option array, using fun ... => True if the values are none, and all is the general predicate
  • the instantiation of the non-uniform parameters and indices
  • the argument to apply it to
Sourceval make_all_theorem : partial_nesting:bool -> Names.GlobRef.t -> bool list -> EConstr.constr array -> EConstr.constr option array -> EConstr.constr option array -> EConstr.constr array -> EConstr.constr -> EConstr.constr LibBinding.State.t

Make the theorem for the all predicate for a fresh instance and using Typing.checked_appvect, given:

  • whether the all predicate is the partial one, or the general one partial_nesting:bool
  • the positivity of each uniform parameter bool list
  • the instantiation of the uniform parameter of the inductive type constr array
  • the instation of the fresh predicate and the proofs they hold constr option array, using fun ... => True and fun _ => I if the values are none, and all is the general predicate
  • the instantiation of the non-uniform parameters and indices
  • the argument to apply it to
View for Arguments
Sourcetype head_argument =
  1. | ArgIsSPUparam of int * EConstr.constr array
    (*

    constant context, position of the uniform parameter, args

    *)
  2. | ArgIsInd of int * EConstr.constr array * EConstr.constr array
    (*

    constant context, position of the one_inductive body, inst_nuparams inst_indices

    *)
  3. | ArgIsNested of Names.MutInd.t * int * Declarations.mutual_inductive_body * bool list * Declarations.one_inductive_body * EConstr.constr array * EConstr.constr array
    (*

    constant context, ind_nested, mutual and one body, strictly positivity of its uniform parameters, instantiation uniform paramerters, and of both non_uniform parameters and indices

    *)
  4. | ArgIsCst

View to decompose arguments as forall locs, X where X is further decomposed as a uniform parameter, the inductive, a nested argument or a constant.

Decompose the argument in it_Prod_or_LetIn local, X where X is a uniform parameter, Ind, nested or a constant

Generate All Predicate
Generate the Theorem for the All Predicate