eq t u tests the equality of t and u (up to α-equivalence). It fails if t or u contain terms of the form Patt(i,s,e) or TEnv(te,env). In the process, subterms of the form TRef(r) in t and u may be set with the corresponding value to enforce equality, and variables appearing in ctx can be unfolded. In other words, eq t u can be used to implement non-linear matching. When the matching feature is used, one should make sure that TRef constructors do not appear both in t and in u at the same time. Indeed, the references are set naively, without occurrence checking.

Equality configuration.

get_eq_config ss pos returns the current configuration for equality, used by tactics such as “rewrite” or “reflexivity”.

get_eq_data pos cfg a returns ((a,l,r),v) if a ≡ Π v1:A1, .., Π vn:An, P (eq a l r) and fails otherwise.

Type of a term with the free variables that need to be substituted (during some unification process). It is usually used to store the LHS of a proof of equality, together with the variables that were quantified over.

add_refs t substitutes each wildcard of t using a fresh reference cell (TRef constructor). This is used for unification, by performing all the substitutions in-place.

match_pattern (xs,p) t attempts to match the pattern p (containing the “pattern variables” of xs) with the term t. If successful, it returns Some(ts) where ts is an array of terms such that substituting elements of xs by the corresponding elements of ts in p yields a term that is equal to t (in terms of eq).

find_subst t (xs,p) is given a term t and a pattern p (with “pattern variables” of xs), and it finds the first instance of (a term matching) p in t (if there is any). If successful, the function returns an array of terms corresponding to the substitution (see match_pattern).

make_pat t p is given a term t, and a pattern p containing reference cells (that are not instantiated) and wildcards. It then tries to find a subterm of t that matches p, using (instantiating) syntactic equality. In case of success, the function returns true, and the matching term is p itself (through instantiation).

bind_pattern p t replaces in the term t every occurence of the pattern p by a fresh variable, and returns the binder on this variable.

swap cfg a r l t returns a term of type P (eq a l r) from a term t of type P (eq a r l).

rewrite ss p pos gt l2r pat t generates a term for the refine tactic representing the application of the rewrite tactic to the goal type gt. Every occurrence of the first instance of the left-hand side is replaced by the right-hand side of the obtained proof (or the reverse if l2r is false). pat is an optional SSReflect pattern. t is the equational lemma that is appied. It handles the full set of SSReflect patterns.