Default Typeclass opaque

By default we make all constants opaque in typeclass resolution (in Options.v). This make typeclass search much faster on average, at the cost of requiring more instances or transparency annotations. In general for most type definitions, one need either to declare it transparent, or define all the required typeclasses on it. Same for decidable predicates as this development use stdpp's Decision Some standard library (or stdpp) type abbreviations need to be typeclass-transparent: Add them here

This is needed to fix the behaviour or setoid rewriting under opaque typeclasses

For the decide_rel instance we want to be more lax that the default. If R is homogenous, we want to unify x y without typeclass opacity because that's what the type checker does

Axioms

We want to work in classical logic with extensional equality. Doing this in Prop and not SProp risks blocking reduction of recursive function using a generic Acc predicate. But it's fine for function whose termination is derived from a measure

Axiomatic proof irrelevance has low priority so that search for proof irrelevance try to find axiom-free instances first

Make functional extensionality work with rewriting

Notations

Heterogenous equality

Type-annotated list notations

Monad-annotated fmap notation

Monad annotated bind notations

This defines operators |> and |$> for pipe-style function application and fmap

Useful for defining decision procedures

Imperative loop in a monad (M). If l is a list A and the body E has type M B (with x : A in context), then the whole loop evaluate to a value M (list B) that yield the list of value of the loop body with monad effects applied in the list order (head first). If you want a truly imperative loop, use a state monad and have E evaluate to unit, you can then ignore the resulting list unit e.g. with ;;

Operator typeclasses

Utility functions

Convenient iff destruction

Convert a true proposition into a rewriting rule of that proposition to true

This is useful for keeping the equality in a match for dependent typing purposes

When matching inspect p instead of p, this notation allows to have the cases be | pat_for_p eq: Heq ⇒ ...

Cartesian product

Notation for cartesian product on sets and lists. × must be left associative because the * of types is left associative. Thus if you have sa : set A, sb : set B and sc : set C, then sa × sb × sc : set (A * B * C)

Constrained quantifiers

Relations

Ltac2 utilities

Pipe notation for function calls

Fix up the do notation. The default one doesn't work

or else notation, same as || in Ltac1. Due to parser limitations this is a the same level as ; and also right associative, so a ; b ||ₜ c is a ; (b ||ₜ c) but a ||ₜ b ; c is a ||ₜ (b ; c)

Throw a Tactic_failure with the provided formated message

Backtracks with a Tactic_failure with the provided formated message

Converts a result into an option, discarding the error payload

Get the name of the last hypothesis

Introduce an hypothesis and get the automatically generated name

If a term is an application, get the head function of that application

Separate a non-dependent function type like A → B → C into (A; B, C)

If a constr is a variable, get the variable name, otherwise None

Create an evar of the required type

Get an instance of a provided typeclass (evar allowed in output positions) Fail (backtracks) if the instance can't be found

Same but returns None if instance can't be found

Used when success has been found

Return true if the tactics succeeds in the context, and false otherwise

Backtrack if the boolean is not true

Ltac2 version of pose_proof

Remove the last element of a list and return the reverted version of the rest

match_pat p c decides if term c matches pattern p

Finds the highest hypothesis that matches the pattern and revert all hypotheses below it

Get an hypothesis by pattern

Get an hypothesis name by pattern

Ltac2 conversions that throw on error

Revert dependent is like generalize dependent but only on hypothesis

Ltac2 debug printers

Ident Ltac2 printer

Int Ltac2 printer

String Ltac2 printer

Quoted string Ltac2 printer

Term Ltac2 printer

Preterm Ltac2 printer

Bool Ltac2 printer

List Ltac2 printer

Option Ltac2 printer

Pair Ltac2 printer

Hypothesis Ltac2 printer. The name must exist in the current goal

Ltac2 inductive type manipulation

Get the number of constructor of an inductive type. Does get_head automatically if needed.

Takes an inductive type constructor, possibly partially applied to parameters, and return its nth constructor, partially applied to the same parameter. This will fail if the type constructor is applied to indices (non-uniform) parameters

Ltac2 goal printer

Allow to print the current goal anywhere

Conversion check

This allows to test whether two terms convert without unifying evars. This will be in Ltac2 standard library in 9.1, but this works in the mean time.

Tactic options

This development relies a lot on automation. This automation sometime needs to be configured in what it should or should not do. A typeclass option is an empty typeclass like Class Option1 := {} It can take parameter like Class Option2 (n : nat) := {}.. When defining options it nice to provide a default instance like Definition option1 : Option1 := ltac:(constructor). This allows the user to enable the option with a plain Existing Instance. Options can be used in typeclass resolution by requiring the option typeclass in specific instances: Instance myinstance: `{Option1} param1 param2 : MyTypeclass param 1 param2. To use such an option in a tactic, one can use has_option opt which will succeed if the option is turned on (aka the typeclass resolution found the option), and fail other wise. This can be used more generally to check if a typeclass instance exists

To enable an option locally, one can either do it at Section/Module scope with: #[local] Exixting Instance option1.. Alternatively one can use the # combinator to add an option for the time of a single tactic. If it's an option with universally quantified parameters you need to manually write the foralls: tac # (∀ n, Option2 (S n))

Another way to use options or other lemma is the use combinator. For example tac use lem add the lemma/Instance lem temporaryly, just while tac is running. In general, for clarity, prefer # for options and use for other lemmas.

Utility tactics

Hypothesis management

Introduces a variable or hypothesis with its default name and returns that name

Reverts the last hypothesis

Reverts all hypotheses

Reverts all hypotheses, print the goal and then undo everything. This is a debugging no-op tactic.

Run tac on all hypotheses in first-to-last order. Later hypotheses are moved into the goal when tac is ran

Actually simple inversion: Leave the generated equalities in the goal

Funelim that leave new hypotheses in the goal

Rewriting

Takes an evar and puts it in a pattern shape. Use as (do n pattern_evar) if you have n evars in your goal. This is might be needed for typeclass-based rewriting tactics that use "+" and not "!" as Hint Mode

Actual dependent rewrite by calling destruct on the equality. The rewrite must be of the form var = exp where var is a plain variable and not a complicated expression. Use subst if you can, this is last resort

Typeclass clean

Typeclass clean to help prove typeclasses lemmas. Call this when the goal is rewriting typeclass (generally with Unfold in its name), with other rewriting typeclasses in the context. This unfold all the typeclasses, apply the rewrites and leave with the actual rewriting goal to prove. Cleanup a single hypothesis

Introduce and cleans up all typeclass hypothesis and then cleans up the goal typeclass

Destruct decide

Convenient notation for deciding a proposition in a proof

Check if x = y. If yes, replace all y by x in the goal

Evar blocking

Yet another block like marker for blocking evar, mainly for typeclass resolution

Take a term as a parameter and blocks one evar from it

Take a tactic looking up the context to find a term

Proof search

Typeclass magic

Record management and lenses

We somewhat hack coq-record-update to provide a lens-like system with vertical composition and horizontal merges. We basically have standard way to compose record fields and more generic getters that can then be used to infer a setter using coq-record-update mechanisms.

Remove the set_wf instance because it make the search for a Setter much slower in the general case. Just allow to use it if there is a SetterWf in the immediate (or section) context, like in Setter_compose_wf

Set a value without looking at the previous value

This allows to use set fst and set snd on pairs

Getter and setter vertical composition

Getter and setter horizontal merging

Constants getter

Sometimes it is useful to have a fake constant getter to merge with other getters. It will not be well formed

Record equality unfolding

For a record type A, this typeclass provides an output predicate Q that is a conjunction of field_wise equality that is equivalent to the record equality. This is automatically derived from a Settable instance although the user is free to define his own instances

Helper for the following Hint Extern

Generate a RecordEqUnfold instance from a Settable instance

Tactic to prove record equality by proving equality for all fields. The number of subgoal is exactly the number of field

Take an equality hypothesis H of the form rec = rec' and destruct it into an equlity for each field. The "as" version is use with a conjunction pattern: record_inj H as (Hfield1 & Hfield2 & ...)

Pair management

EmptyT and DecisionT

Mark a type as empty, useable for guiding typeclass resolution.

Typeclass for type (and more usefully families of types) that are decidably empty or not

Trivial instances of Decision T if type is either inhabited or empty

Inhabited, EmptyT, and DecisionT, missing base type instances

Identity Monad

This is useful to apply transformers on, or in contexts that really expect a monad. The identity monad. We are not using a regular id to help type inference and avoid universes constraints

Computable transport

This allow to computably transport object of type families along an equality on the indices (e.g. fin, vec, bv). The equality must be on concrete values and not on types (e.g. n = m and not fin n = fin m). The goal for ctrans is to compute using vm_compute and similar tactics even if the equality proof is entirely opaque. Nevertheless it can safely be extracted to Obj.magic. This is a band aid until we have builtin cast from Observable Type Theory (OTT). CTrans is the main typeclass for computable transport. It only contains computational content and not soundness

CTransSimpl is a companion typeclass that the soundness proof of a CTrans instance

Computable transport combinators

Computable transport for fin