package rocq-runtime
The Rocq Prover -- Core Binaries and Tools
Install
Dune Dependency
Authors
Maintainers
Sources
rocq-9.0.0.tar.gz
md5=8d522602d23e7a665631826dab9aa92b
sha512=f4f76a6a178e421c99ee7a331a2fd97a06e9c5d0168d7e60c44e3820d8e1a124370ea104ad90c7f87a9a1e9d87b2d0d7d2d387c998feeaed4a75ed04e176a4be
doc/rocq-runtime.tactics/Induction/index.html
Module InductionSource
Elimination tactics.
Source
type elim_scheme = {elimt : EConstr.types;indref : Names.GlobRef.t option;params : EConstr.rel_context;(*(prm1,tprm1);(prm2,tprm2)...(prmp,tprmp)
*)nparams : int;(*number of parameters
*)predicates : EConstr.rel_context;(*(Qq, (Tq_1 -> Tq_2 ->...-> Tq_nq)), (Q1,...)
*)npredicates : int;(*Number of predicates
*)branches : EConstr.rel_context;(*branchr,...,branch1
*)nbranches : int;(*Number of branches
*)args : EConstr.rel_context;(*(xni, Ti_ni) ... (x1, Ti_1)
*)nargs : int;(*number of arguments
*)indarg : EConstr.rel_declaration option;(*Some (H,I prm1..prmp x1...xni) if HI is in premisses, None otherwise
*)concl : EConstr.types;(*Qi x1...xni HI (f...), HI and (f...) are optional and mutually exclusive
*)indarg_in_concl : bool;(*true if HI appears at the end of conclusion
*)farg_in_concl : bool;(*true if (f...) appears at the end of conclusion
*)
}rel_contexts and rel_declaration actually contain triples, and lists are actually in reverse order to fit compose_prod.
Source
val induction :
Tactics.evars_flag ->
Tactics.clear_flag ->
EConstr.constr ->
Tactypes.or_and_intro_pattern option ->
EConstr.constr Tactypes.with_bindings option ->
unit Proofview.tacticSource
val destruct :
Tactics.evars_flag ->
Tactics.clear_flag ->
EConstr.constr ->
Tactypes.or_and_intro_pattern option ->
EConstr.constr Tactypes.with_bindings option ->
unit Proofview.tacticGeneric case analysis / induction tactics.
Implements user-level "destruct" and "induction"
Source
val induction_destruct :
Tactics.rec_flag ->
Tactics.evars_flag ->
((Tactypes.delayed_open_constr_with_bindings Tactics.destruction_arg
* (Tactypes.intro_pattern_naming option
* Tactypes.or_and_intro_pattern option)
* Locus.clause option)
list
* EConstr.constr Tactypes.with_bindings option) ->
unit Proofview.tactic