package coq

  1. Overview
  2. Docs
Formal proof management system

Install 

dune-project
 Dependency

coq.inria.fr Edit opam file Versions (40)

Authors

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

Maintainers

  1. C
    coqdev@inria.fr

Sources

coq-8.15.1.tar.gz
sha256=513e953b7183d478acb75fd6e80e4dc32ac1a918cf4343ac31a859cfb4e9aad2

doc/coq-core.proofs/Clenv/index.html

Module ClenvSource

This file defines clausenv, which is a deprecated way to handle open terms in the proof engine. Most of the API here is legacy except for the evar-based clauses.

The Type of Constructions clausale environments.
Sourcetype clausenv = private {
  1. env : Environ.env;
    (*

    the typing context

    *)
  2. evd : Evd.evar_map;
    (*

    the mapping from metavar and evar numbers to their types and values

    *)
  3. templval : EConstr.constr Evd.freelisted;
    (*

    the template which we are trying to fill out

    *)
  4. templtyp : EConstr.constr Evd.freelisted;
    (*

    its type

    *)
  5. cache : Reductionops.meta_instance_subst;
}
Sourceval update_clenv_evd : clausenv -> Evd.evar_map -> clausenv
Sourceval clenv_value : clausenv -> EConstr.constr

subject of clenv (instantiated)

Sourceval clenv_type : clausenv -> EConstr.types

type of clenv (instantiated)

type of a meta in clenv context

Sourceval mk_clenv_from_n : Environ.env -> Evd.evar_map -> int -> (EConstr.constr * EConstr.types) -> clausenv
linking of clenvs
Sourceval clenv_fchain : ?with_univs:bool -> ?flags:Unification.unify_flags -> Constr.metavariable -> clausenv -> clausenv -> clausenv
Unification with clenvs

Unifies two terms in a clenv. The boolean is allow_K (see Unification)

Bindings
Sourceval clenv_independent : clausenv -> Constr.metavariable list

bindings where the key is the position in the template of the clenv (dependent or not). Positions can be negative meaning to start from the rightmost argument of the template.

Sourceval clenv_missing : clausenv -> Constr.metavariable list
Sourceexception NoSuchBinding

for the purpose of inversion tactics

Sourceval clenv_constrain_last_binding : EConstr.constr -> clausenv -> clausenv
Sourceval clenv_unify_meta_types : ?flags:Unification.unify_flags -> clausenv -> clausenv

start with a clenv to refine with a given term with bindings

Sourceval make_clenv_binding_apply : Environ.env -> Evd.evar_map -> int option -> (EConstr.constr * EConstr.constr) -> EConstr.constr Tactypes.bindings -> clausenv

the arity of the lemma is fixed the optional int tells how many prods of the lemma have to be used use all of them if None

Sourceval clenv_push_prod : clausenv -> (Constr.metavariable * bool * clausenv) option

if the clause is a product, add an extra meta for this product

Clenv tactics
Sourceval res_pf : ?with_evars:bool -> ?with_classes:bool -> ?flags:Unification.unify_flags -> clausenv -> unit Proofview.tactic
Sourceval clenv_pose_dependent_evars : ?with_evars:bool -> clausenv -> clausenv
Sourceval pr_clenv : clausenv -> Pp.t

Pretty-print (debug only)

Evar-based clauses

The following code is an adaptation of the make_clenv_* functions above, except that it uses evars instead of metas, and naturally fits in the new refinement monad. It should eventually replace all uses of the aforementioned functions.

A clause is constructed as follows: assume a type t := forall (x1 : A1) ... (xn : An), T, we instantiate all the xi with a fresh evar ei and return T(xi := ei) together with the ei enriched with a bit of additional data. This is the simple part done by make_evar_clause.

The problem lies in the fact we want to solve such holes with some constr bindings. This entails some subtleties, because the provided terms may only be well-typed up to a coercion, which we can only infer if we have enough typing information. The meta machinery could insert coercions through tricky instantiation delays. The only solution we have now is to delay the tentative resolution of clauses by providing the solve_evar_clause function, to be called at a smart enough time.

Sourcetype hole = {
  1. hole_evar : EConstr.constr;
    (*

    The hole itself. Guaranteed to be an evar.

    *)
  2. hole_type : EConstr.types;
    (*

    Type of the hole in the current environment.

    *)
  3. hole_deps : bool;
    (*

    Whether the remainder of the clause was dependent in the hole. Note that because let binders are substituted, it does not mean that it actually appears somewhere in the returned clause.

    *)
  4. hole_name : Names.Name.t;
    (*

    Name of the hole coming from its binder.

    *)
}
Sourcetype clause = {
  1. cl_holes : hole list;
  2. cl_concl : EConstr.types;
}
Sourceval make_evar_clause : Environ.env -> Evd.evar_map -> ?len:int -> EConstr.types -> Evd.evar_map * clause

An evar version of make_clenv_binding. Given a type t, evar_environments env sigma ~len t bl tries to eliminate at most len products of the type t by filling it with evars. It returns the resulting type together with the list of holes generated. Assumes that t is well-typed in the environment.

solve_evar_clause env sigma hyps cl bl tries to solve the holes contained in cl according to the bl argument. Assumes that bl are well-typed in the environment. The boolean hyps is a compatibility flag that allows to consider arguments to be dependent only when they appear in hypotheses and not in the conclusion. This boolean is only used when bl is of the form ImplicitBindings _.

Sourceval rename_with : unit -> bool

For funind