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.pretyping/Locus/index.html

Module Locus

Locus : positions in hypotheses and goals.

type 'a or_var =
  1. | ArgArg of 'a
  2. | ArgVar of Names.lident

'a or_var represents either a value of type 'a or a variable.

Occurrences
type 'a occurrences_gen =
  1. | AllOccurrences
  2. | AtLeastOneOccurrence
  3. | AllOccurrencesBut of 'a list
    (*

    The list should be non-empty.

    *)
  4. | NoOccurrences
  5. | OnlyOccurrences of 'a list
    (*

    The list should be non-empty.

    *)

Occurences in a hypothesis or conclusion.

type occurrences_expr = int or_var occurrences_gen
type 'a with_occurrences_expr = occurrences_expr * 'a
type occurrences = int occurrences_gen
type 'a with_occurrences = occurrences * 'a
Locations
type hyp_location_flag =
  1. | InHyp
  2. | InHypTypeOnly
  3. | InHypValueOnly

In a hypothesis, occurrences can refer to the body (if any), to the type, or to both.

Abstract clauses expressions
type 'a hyp_location_expr = 'a with_occurrences_expr * hyp_location_flag
type 'id clause_expr = {
  1. onhyps : 'id hyp_location_expr list option;
  2. concl_occs : occurrences_expr;
}

A clause_expr (and its instance clause) denotes occurrences and hypotheses in a goal in an abstract way; in particular, it can refer to the set of all hypotheses independently of the effective contents of the current goal.

Concerning the field onhyps:

  • None means *on every hypothesis*.
  • Some hyps means on hypotheses belonging to hyps.
type clause = Names.Id.t clause_expr
Concrete view of occurrence clauses
type clause_atom =
  1. | OnHyp of Names.Id.t * occurrences_expr * hyp_location_flag
  2. | OnConcl of occurrences_expr

clause_atom refers either to:

  • Some occurrences in a hypothesis.
  • Some occurrences in the conclusion .
type concrete_clause = clause_atom list

A concrete_clause is a collection of occurrences in hypotheses and in the conclusion.

A weaker form of clause with no mention of occurrences
type hyp_location = Names.Id.t * hyp_location_flag

A hyp_location is a hypothesis together with a location in this hypothesis (body, type, or both).

type goal_location = hyp_location option

A goal_location is either:

  • A hypothesis (together with a location in this hypothesis).
  • The conclusion (represented by None).
Simple clauses, without occurrences nor location
type simple_clause = Names.Id.t option list

A simple_clause is a set of hypotheses, possibly extended with the conclusion (conclusion is represented by None).

Occurences modulo conversion
type 'a or_like_first =
  1. | AtOccs of 'a
  2. | LikeFirst

A notion of occurrences allowing to express "all occurrences convertible to the first which matches".