TODO: Clean up

Basic tactics

This module implements various tactics used in the library. If the goal is x = z, path_via y will replace this with two goals, x = y and y = z.

The following tactic is designed to be more or less interchangeable with induction n as [ | n' IH ] whenever n is a nat or a trunc_index. The difference is that it produces proof terms involving fix explicitly rather than nat_ind or trunc_index_ind, and therefore does not introduce higher universe parameters. It works if n is in the context or in the goal.

Debugging tactics to show the goal during evaluation.

Do something on the last hypothesis, or fail

Revert the last hypothesis.

Repeatedly reverse the last hypothesis, putting everything in the goal.

Reverse everything up to hypothesis id (not included).

Clear duplicated hypotheses

Try to clear everything except some hyp

Tactical on_call f tac applies tac on any application of f in the hypothesis or goal.

Permit to name the results of destructing the call to f.

Specify the hypothesis in which the call occurs as well.

A marker for prototypes to destruct.

Try to inject any potential constructor equality hypothesis.

Destruct an hypothesis by first copying it to avoid dependencies.

A tactic to show contradiction by first asserting an automatically provable hypothesis.

A tactic that adds H:=p:typeof(p) to the context if no hypothesis of the same type appears in the goal. Useful to do saturation using tactics.

A tactic to replace an hypothesis by another term.

A tactic to refine an hypothesis by supplying some of its arguments.

TODO: From here comes from Overture.v Clear a hypothesis and also its dependencies. Taken from Coq stdlib, with the performance-enhancing change to lazymatch suggested at https://github.com/coq/coq/issues/11689.

A version of generalize dependent that applies only to a hypothesis. Taken from Coq stdlib.

Applying a tactic to a term with increasingly many arguments

Same thing but starting with many holes first

We keep a list of global axioms that we will solve automatically, even when not using typeclass search.

We add Funext to the list here, and will later add Univalence.

Add PropResizing to the list of global axioms.

A shorter name for simple refine.

A shorter name for notypeclasses refine; also handles global axioms.

A shorter name for simple notypeclasses refine; also handles global axioms.

Note that the Coq standard library has a rapply, but it is like our rapply' with many-holes first. We prefer fewer-holes first, for instance so that a theorem producing an equivalence will by preference be used to produce an equivalence rather than to apply the coercion of that equivalence to a function.

Apply a tactic to one side of an equation. For example, lhs rapply lemma. tac should produce a path.

Ssreflect tactics, adapted by Robbert Krebbers

Apply using the same opacity information as typeclass proof search.

A convenient tactic for using function extensionality.

funext apply functional extensionality (path_forall) to the goal and the introduce the arguments in the context. For instance, if you have to prove f = g where f and g take two arguments, you can use funext x y, and the goal become f x y = g x y.

This tactic doesn't end with auto, but you can always write "by (path_induction;auto with path_hints)" if you want.

The tactic f_ap is a replacement for the previously existing standard library tactic f_equal. This tactic works by repeatedly applying the fact that f = g → x = y → f x = g y to turn, e.g., f x y = f z w first into f x = f z and y = w, and then turns the first of these into f = f and x = z. The done tactic is used to detect the f = f case and finish, and the trivial is used to solve, e.g., x = x when using f_ap on f y x = f z x. This tactic only works for non-dependently-typed functions; we cannot express y = w in the first example if y and w have different types. If and when Arnaud's new-tacticals branch lands, and we can have a goal which depends on the term used to discharge another goal, then this tactic should probably be generalized to deal with dependent functions.

expand replaces both terms of an equality (either paths or pointwise_paths in the goal with their head normal forms

atomic x is the same as idtac if x is a variable or hypothesis, but is fail 0 if x has internal structure. This is useful, for example, to easily destruct all variables that show up as the discriminees of match statements, without destructing more complicated terms whose structures might matter.

Find the head of the given expression.

This tactic gets the constructor of any one-constructor inductive type.

case_path is a HoTT replacement for case_eq; case_path x is like destruct x, but it remembers the original value of x in an equation to be introduced.

revert_opaque x is like revert x, except that it fails if x is not an opaque variable (i.e. if it has a := definition rather than just a type).

transparent assert (H : T) is like assert (H : T), but leaves the body transparent. Since binders don't respect fresh, we use a name unlikely to be reused.

transparent eassert is like transparent assert, but allows holes in the type, which will be turned into evars.

A version of Coq's remember that uses our equality.

A variant that doesn't substitute in the goal and hypotheses.

rel_hnf, when given a goal of the form R x y for any relation R, puts x and y in head normal form.

This tactic is a version of tryif require () then if_yes () else if_no () which is suitable for use in constructing constrs by virtue of being evaluated during the Ltac expression evaluation phase rather than during the tactic running phase. All three arguments are expected to be tactic thunks which will be passed a dummy unit argument.

The following tactic issig proves automatically that a record type is equivalent to a nested Sigma-type. Specifically, it proves a goal that looks like

   { x : A & B x } <~> Some_Record

In fact you don't even have to write down the sigma type. Though it is good practice to write it out anyway, this tactic can work out the sigma type and tell you what it should look like. The following should generate the desired equivalence. You can check the definition to see what type it has and therefore what the sigma type should be.

  Definition issig_myrecord
    : _ <~> MyRecord := ltac:(issig).

  Check issig_myrecord.

In order to define this tactic we have many helper tactics.

We build an equivalence with 5 holes.

Going from a sigma type to a record

Going from a record to a sigma type

Proving eissect

Proving eisretr

Proving eisadj

We show how the tactic works in a couple of examples.

The general reasoning behind the issig tactic is: if we know the type of the record, econstructor will give us the constructor applied to evars for each field. If we assume that there are no evars in the type, we can unify the first evar with u.1, the next evar with u.2.1, the next with u.2.2.1, etc, and if we run out of evars or projections, we backtrack and instead fill the final evar with u.2.2....2. (Note that if we strip the trailing evars from the constructor before unifying them, we get a term with a Pi type, and if we drop the final codomain and turn the Pi type into a Sigma, this lets us autogenerate the Sigma type we should be using; this is how the versions that don't need a hand-crafted Sigma type work: they unify the generated type with the term in the goal that should be the Sigma type.) Generating the function the other way is a bit trickier, because there's no easy way to get our hands on all the projections of the record, and moreover we don't even know how many pairings we'll need. The thing we want to do is introduce the right number of pairings, destruct the variable of record type in the goal for each component, and then magically use the right projection. I'll get back to the magic in a moment; first we need to take care of the "right number" of pairings. We could pull a trick where we infer the number by looking at the term we get from econstructor in a goal whose type is the record. Instead, I chose the more concise route of coding a tactic that introduces the minimum number of pairings needed to make the magic work. How does it know the minimum number? It doesn't need to! The wonder of (recursive) multisuccess tactics is that you can say "try no pairings, and if that makes any future tactic fail, backtrack and try one pairing, and if that doesn't work, backtrack and try two pairings, etc". (The downside is that the error messages you get when you set things up wrong are truly incomprehensible, because if you make a typo in any of the fields of the Sigma type the error message you end up getting is something like "(_; _) is a Sigma type but it was expected to have the type of the final field" (and it's always about the final field, regardless of which field you made a typo in). So plausibly it's worth it to still do the small issig tactics by hand, and only use this tactic for >= 5 fields or something.) Okay, now onto the magic. How do we know which field is the right one? Well, there's only one answer that lets us prove the section and retraction by destruct+reflexivity, so we can let unification solve this problem for us. It's important to have destructed the record variable in each of the pair-component evars, because unification is not (yet) smart enough to invert records for us; this is what the destruct before shelve in the inverse function generation tactic is. We cbn pr1 and pr2 to make the unification problem be completely syntactic (no need to unfold anything during unification). This is probably not strictly necessary, but seems like good form to me. Finally, we can prove the other one of the section/retraction pair (I can never recall which is which), and the adjoint, by reflexivity. (Perhaps it would be better to use exact idpath, if we want to not have to unfold reflexivity when using equivalences generated by these tactics.)