Library Coq.ssr.ssreflect

This file is the Gallina part of the ssreflect plugin implementation. Files that use the ssreflect plugin should always Require ssreflect and either Import ssreflect or Import ssreflect.SsrSyntax. Part of the contents of this file is technical and will only interest advanced developers; in addition the following are defined: [the str of v by f] == the Canonical s : str such that f s = v. [the str of v] == the Canonical s : str that coerces to v. argumentType c == the T such that c : forall x : T, P x. returnType c == the R such that c : T -> R. {type of c for s} == P s where c : forall x : T, P x. nonPropType == an interface for non-Prop Types: a nonPropType coerces to a Type, and only types that do not have sort Prop are canonical nonPropType instances. This is useful for applied views (see mid-file comment). notProp T == the nonPropType instance for type T. phantom T v == singleton type with inhabitant Phantom T v. phant T == singleton type with inhabitant Phant v. =^~ r == the converse of rewriting rule r (e.g., in a rewrite multirule). unkeyed t == t, but treated as an unkeyed matching pattern by the ssreflect matching algorithm. nosimpl t == t, but on the right-hand side of Definition C := nosimpl disables expansion of C by /=. locked t == t, but locked t is not convertible to t. locked_with k t == t, but not convertible to t or locked_with k' t unless k = k' (with k : unit). Coq type-checking will be much more efficient if locked_with with a bespoke k is used for sealed definitions. unlockable v == interface for sealed constant definitions of v. Unlockable def == the unlockable that registers def : C = v. [unlockable of C] == a clone for C of the canonical unlockable for the definition of C (e.g., if it uses locked_with). [unlockable fun C] == [unlockable of C] with the expansion forced to be an explicit lambda expression.

• > The usage pattern for ADT operations is: Definition foo_def x1 .. xn := big_foo_expression. Fact foo_key : unit. Proof. by [ ]. Qed. Definition foo := locked_with foo_key foo_def. Canonical foo_unlockable := [unlockable fun foo]. This minimizes the comparison overhead for foo, while still allowing rewrite unlock to expose big_foo_expression.

More information about these definitions and their use can be found in the ssreflect manual, and in specific comments below.

Declare Ssr keywords: 'is' 'of' '//' '/=' and '//='. We also declare the parsing level 8, as a workaround for a notation grammar factoring problem. Arguments of application-style notations (at level 10) should be declared at level 8 rather than 9 or the camlp5 grammar will not factor properly.

Non ambiguous keyword to check if the SsrSyntax module is imported

Save primitive notation that will be overloaded.

Reserve notation that introduced in this file.

To define notations for tactic in intro patterns. When "=> /t" is parsed, "t:

Make the general "if" into a notation, so that we can override it below. The notations are "only parsing" because the Coq decompiler will not recognize the expansion of the boolean if; using the default printer avoids a spurious trailing %GEN_IF.

Force boolean interpretation of simple if expressions.

To allow a wider variety of notations without reserving a large number of of identifiers, the ssreflect library systematically uses "forms" to enclose complex mixfix syntax. A "form" is simply a mixfix expression enclosed in square brackets and introduced by a keyword: [keyword ... ] Because the keyword follows a bracket it does not need to be reserved. Non-ssreflect libraries that do not respect the form syntax (e.g., the Coq Lists library) should be loaded before ssreflect so that their notations do not mask all ssreflect forms.

Allow overloading of the cast (x : T) syntax, put whitespace around the ":" symbol to avoid lexical clashes (and for consistency with the parsing precedence of the notation, which binds less tightly than application), and put printing boxes that print the type of a long definition on a separate line rather than force-fit it at the right margin.

Allow the casual use of notations like nat * nat for explicit Type declarations. Note that (nat * nat : Type) is NOT equivalent to (nat * nat)%type, whose inferred type is legacy type "Set".

Allow similarly Prop annotation for, e.g., rewrite multirules.

Constants for abstract: and [: name ] intro pattern

Constants for tactic-views

Syntax for referring to canonical structures: [the struct_type of proj_val by proj_fun] This form denotes the Canonical instance s of the Structure type struct_type whose proj_fun projection is proj_val, i.e., such that proj_fun s = proj_val. Typically proj_fun will be A record field accessors of struct_type, but this need not be the case; it can be, for instance, a field of a record type to which struct_type coerces; proj_val will likewise be coerced to the return type of proj_fun. In all but the simplest cases, proj_fun should be eta-expanded to allow for the insertion of implicit arguments. In the common case where proj_fun itself is a coercion, the "by" part can be omitted entirely; in this case it is inferred by casting s to the inferred type of proj_val. Obviously the latter can be fixed by using an explicit cast on proj_val, and it is highly recommended to do so when the return type intended for proj_fun is "Type", as the type inferred for proj_val may vary because of sort polymorphism (it could be Set or Prop). Note when using the [the _ of _ ] form to generate a substructure from a telescopes-style canonical hierarchy (implementing inheritance with coercions), one should always project or coerce the value to the BASE structure, because Coq will only find a Canonical derived structure for the Canonical base structure -- not for a base structure that is specific to proj_value.

The following are "format only" versions of the above notations. We need to do this to prevent the formatter from being be thrown off by application collapsing, coercion insertion and beta reduction in the right hand side of the notations above.

We would like to recognize Notation " [ 'the' sT 'of' v : 'Type' ]" := (@get Type sT v _ ) (at level 0, format " [ 'the' sT 'of' v : 'Type' ]") : form_scope. Helper notation for canonical structure inheritance support. This is a workaround for the poor interaction between delta reduction and canonical projections in Coq's unification algorithm, by which transparent definitions hide canonical instances, i.e., in Canonical a_type_struct := @Struct a_type ... Definition my_type := a_type. my_type doesn't effectively inherit the struct structure from a_type. Our solution is to redeclare the instance as follows Canonical my_type_struct := Eval hnf in [struct of my_type]. The special notation [str of _ ] must be defined for each Strucure "str" with constructor "Str", typically as follows Definition clone_str s := let: Str _ x y ... z := s return {type of Str for s} -> str in fun k => k _ x y ... z. Notation " [ 'str' 'of' T 'for' s ]" := (@clone_str s (@Str T)) (at level 0, format " [ 'str' 'of' T 'for' s ]") : form_scope. Notation " [ 'str' 'of' T ]" := (repack_str (fun x => @Str T x)) (at level 0, format " [ 'str' 'of' T ]") : form_scope. The notation for the match return predicate is defined below; the eta expansion in the second form serves both to distinguish it from the first and to avoid the delta reduction problem. There are several variations on the notation and the definition of the the "clone" function, for telescopes, mixin classes, and join (multiple inheritance) classes. We describe a different idiom for clones in ssrfun; it uses phantom types (see below) and static unification; see fintype and ssralg for examples.

A generic "phantom" type (actually, a unit type with a phantom parameter). This type can be used for type definitions that require some Structure on one of their parameters, to allow Coq to infer said structure so it does not have to be supplied explicitly or via the " [the _ of _ ]" notation (the latter interacts poorly with other Notation). The definition of a (co)inductive type with a parameter p : p_type, that needs to use the operations of a structure Structure p_str : Type := p_Str {p_repr :> p_type; p_op : p_repr -> ...} should be given as Inductive indt_type (p : p_str) := Indt ... . Definition indt_of (p : p_str) & phantom p_type p := indt_type p. Notation "{ 'indt' p }" := (indt_of (Phantom p)). Definition indt p x y ... z : {indt p} := @Indt p x y ... z. Notation " [ 'indt' x y ... z ]" := (indt x y ... z). That is, the concrete type and its constructor should be shadowed by definitions that use a phantom argument to infer and display the true value of p (in practice, the "indt" constructor often performs additional functions, like "locking" the representation -- see below). We also define a simpler version ("phant" / "Phant") of phantom for the common case where p_type is Type.

Internal tagging used by the implementation of the ssreflect elim.

The ssreflect idiom for a non-keyed pattern:

• unkeyed t will match any subterm that unifies with t, regardless of whether it displays the same head symbol as t.
• unkeyed t a b will match any application of a term f unifying with t, to two arguments unifying with with a and b, respectively, regardless of apparent head symbols.
• unkeyed x where x is a variable will match any subterm with the same type as x (when x would raise the 'indeterminate pattern' error).

Ssreflect converse rewrite rule rule idiom.

Term tagging (user-level). The ssreflect library uses four strengths of term tagging to restrict convertibility during type checking: nosimpl t simplifies to t EXCEPT in a definition; more precisely, given Definition foo := nosimpl bar, foo (or foo t') will NOT be expanded by the /= and //= switches unless it is in a forcing context (e.g., in match foo t' with ... end, foo t' will be reduced if this allows the match to be reduced). Note that nosimpl bar is simply notation for a a term that beta-iota reduces to bar; hence rewrite /foo will replace foo by bar, and rewrite -/foo will replace bar by foo. CAVEAT: nosimpl should not be used inside a Section, because the end of section "cooking" removes the iota redex. locked t is provably equal to t, but is not convertible to t; 'locked' provides support for selective rewriting, via the lock t : t = locked t Lemma, and the ssreflect unlock tactic. locked_with k t is equal but not convertible to t, much like locked t, but supports explicit tagging with a value k : unit. This is used to mitigate a flaw in the term comparison heuristic of the Coq kernel, which treats all terms of the form locked t as equal and compares their arguments recursively, leading to an exponential blowup of comparison. For this reason locked_with should be used rather than locked when defining ADT operations. The unlock tactic does not support locked_with but the unlock rewrite rule does, via the unlockable interface. we also use Module Type ascription to create truly opaque constants, because simple expansion of constants to reveal an unreducible term doubles the time complexity of a negative comparison. Such opaque constants can be expanded generically with the unlock rewrite rule. See the definition of card and subset in fintype for examples of this.

Needed for locked predicates, in particular for eqType's.

The basic closing tactic "done".

Quicker done tactic not including split, syntax: /0/

To unlock opaque constants.

Generic keyed constant locking. The argument order ensures that k is always compared before T.

This can be used as a cheap alternative to cloning the unlockable instance below, but with caution as unkeyed matching can be expensive.

Intensionaly, this instance will not apply to locked u.

More accurate variant of unlock, and safer alternative to locked_withE.

The internal lemmas for the have tactics.

Internal N-ary congruence lemmas for the congr tactic.

View lemmas that don't use reflection.

To focus non-ssreflect tactics on a subterm, eg vm_compute. Usage: elim/abstract_context: (pattern) => G defG. vm_compute; rewrite {}defG {G}. Note that vm_cast are not stored in the proof term for reductions occurring in the context, hence set here := pattern; vm_compute in (value of here) blows up at Qed time.

Closing rewrite rule

Closing tactic

Convenience rewrite rule to unprotect evars, e.g., to instantiate them in another way than with reflexivity.

An interface for non-Prop types; used to avoid improper instantiation of polymorphic lemmas with on-demand implicits when they are used as views. For example: Some_inj {T} : forall x y : T, Some x = Some y -> x = y. Using move/Some_inj on a goal of the form Some n = Some 0 will fail: SSReflect will interpret the view as @Some_inj ?T top_assumption since this is the well-typed application of the view with the minimal number of inserted evars (taking ?T := Some n = Some 0), and then will later complain that it cannot erase top_assumption after having abstracted the viewed assumption. Making x and y maximal implicits would avoid this and force the intended @Some_inj nat x y top_assumption interpretation, but is undesirable as it makes it harder to use Some_inj with the many SSReflect and MathComp lemmas that have an injectivity premise. Specifying {T : nonPropType} solves this more elegantly, as then (?T : Type) no longer unifies with (Some n = Some 0), which has sort Prop.

Implementation notes: We rely on three interface Structures:

• test_of r, the middle structure, performs the actual check: it has two canonical instances whose 'condition' projection are maybeProj (?P : Prop) and tt, and which set r := true and r := false, respectively. Unifying condition (?t : test_of ?r) with maybeProj T will thus set ?r to true if T is in Prop as the test_Prop T instance will apply, and otherwise simplify maybeProp T to tt and use the test_negative instance and set ?r to false.
• call_of c r sets up a call to test_of on condition c with expected result r. It has a default instance for its 'callee' projection to Type, which sets c := maybeProj T and r := false when unifying with a type T.
• type is a telescope on call_of c r, which checks that unifying test_of ?r1 with c indeed sets ?r1 := r; the type structure bundles the 'test' instance and its 'result' value along with its call_of c r projection. The default instance essentially provides eta-expansion for 'type'. This is only essential for the first 'result' projection to bool; using the instance for other projection merely avoids spurious delta expansions that would spoil the notProp T notation.

In detail, unifying T =~= ?S with ?S : nonPropType, i.e., (1) T =~= @callee (@condition (result ?S) (test ?S)) (result ?S) (frame ?S) first uses the default call instance with ?T := T to reduce (1) to (2a) @condition (result ?S) (test ?S) =~= maybeProp T (3) result ?S =~= false (4) frame ?S =~= call T along with some trivial universe-related checks which are irrelevant here. Then the unification tries to use the test_Prop instance to reduce (2a) to (6a) result ?S =~= true (7a) ?P =~= T with ?P : Prop (8a) test ?S =~= test_Prop ?P Now the default 'check' instance with ?result := true resolves (6a) as (9a) ?S := @check true ?test ?frame Then (7a) can be solved precisely if T has sort at most (hence exactly) Prop, and then (8a) is solved by the check instance, yielding ?test := test_Prop T, and completing the solution of (2a), and committing to it. But now (3) is inconsistent with (9a), and this makes the entire problem (1) fails. If on the othe hand T does not have sort Prop then (7a) fails and the unification resorts to delta expanding (2a), which gives (2b) @condition (result ?S) (test ?S) =~= tt which is then reduced, using the test_negative instance, to (6b) result ?S =~= false (8b) test ?S =~= test_negative Both are solved using the check default instance, as in the (2a) branch, giving (9b) ?S := @check false test_negative ?frame Then (3) and (4) are similarly soved using check, giving the final assignment (9) ?S := notProp T Observe that we must perform the actual test unification on the arguments of the initial canonical instance, and not on the instance itself as we do in mathcomp/matrix and mathcomp/vector, because we want the unification to fail when T has sort Prop. If both the test_of and the result check unifications were done as part of the structure telescope then the latter would be a sub-problem of the former, and thus failing the check would merely make the test_of unification backtrack and delta-expand and we would not get failure.