diff options
Diffstat (limited to 'plugins/ssr')
| -rw-r--r-- | plugins/ssr/ssrast.mli | 6 | ||||
| -rw-r--r-- | plugins/ssr/ssrbool.v | 936 | ||||
| -rw-r--r-- | plugins/ssr/ssrcommon.ml | 43 | ||||
| -rw-r--r-- | plugins/ssr/ssrcommon.mli | 4 | ||||
| -rw-r--r-- | plugins/ssr/ssreflect.v | 439 | ||||
| -rw-r--r-- | plugins/ssr/ssrelim.ml | 7 | ||||
| -rw-r--r-- | plugins/ssr/ssrequality.ml | 32 | ||||
| -rw-r--r-- | plugins/ssr/ssrfun.v | 487 | ||||
| -rw-r--r-- | plugins/ssr/ssrfwd.ml | 15 | ||||
| -rw-r--r-- | plugins/ssr/ssripats.ml | 85 | ||||
| -rw-r--r-- | plugins/ssr/ssrparser.ml4 | 74 | ||||
| -rw-r--r-- | plugins/ssr/ssrparser.mli | 8 | ||||
| -rw-r--r-- | plugins/ssr/ssrprinters.ml | 5 | ||||
| -rw-r--r-- | plugins/ssr/ssrtacticals.ml | 15 | ||||
| -rw-r--r-- | plugins/ssr/ssrtacticals.mli | 4 | ||||
| -rw-r--r-- | plugins/ssr/ssrvernac.ml4 | 38 | ||||
| -rw-r--r-- | plugins/ssr/ssrview.ml | 99 | ||||
| -rw-r--r-- | plugins/ssr/ssrview.mli | 6 |
18 files changed, 1199 insertions, 1104 deletions
diff --git a/plugins/ssr/ssrast.mli b/plugins/ssr/ssrast.mli index 7f5f2f63..a786b995 100644 --- a/plugins/ssr/ssrast.mli +++ b/plugins/ssr/ssrast.mli @@ -37,7 +37,7 @@ type ssrmult = int * ssrmmod type ssrocc = (bool * int list) option (* index MAYBE REMOVE ONLY INTERNAL stuff between {} *) -type ssrindex = int Misctypes.or_var +type ssrindex = int Locus.or_var (* clear switch {H G} *) type ssrclear = ssrhyps @@ -84,11 +84,11 @@ type ssripat = | IPatId of (*TODO id_mod option * *) Id.t | IPatAnon of anon_iter (* inaccessible name *) (* TODO | IPatClearMark *) - | IPatDispatch of ssripatss (* /[..|..] *) + | IPatDispatch of bool (* ssr exception: accept a dispatch on the empty list even when there are subgoals *) * ssripatss (* (..|..) *) | IPatCase of (* ipats_mod option * *) ssripatss (* this is not equivalent to /case /[..|..] if there are already multiple goals *) | IPatInj of ssripatss | IPatRewrite of (*occurrence option * rewrite_pattern **) ssrocc * ssrdir - | IPatView of ssrview (* /view *) + | IPatView of bool * ssrview (* {}/view (true if the clear is present) *) | IPatClear of ssrclear (* {H1 H2} *) | IPatSimpl of ssrsimpl | IPatAbstractVars of Id.t list diff --git a/plugins/ssr/ssrbool.v b/plugins/ssr/ssrbool.v index 7d05b643..a618fc78 100644 --- a/plugins/ssr/ssrbool.v +++ b/plugins/ssr/ssrbool.v @@ -10,264 +10,266 @@ (* This file is (C) Copyright 2006-2015 Microsoft Corporation and Inria. *) +(** #<style> .doc { font-family: monospace; white-space: pre; } </style># **) + Require Bool. Require Import ssreflect ssrfun. -(******************************************************************************) -(* A theory of boolean predicates and operators. A large part of this file is *) -(* concerned with boolean reflection. *) -(* Definitions and notations: *) -(* is_true b == the coercion of b : bool to Prop (:= b = true). *) -(* This is just input and displayed as `b''. *) -(* reflect P b == the reflection inductive predicate, asserting *) -(* that the logical proposition P : prop with the *) -(* formula b : bool. Lemmas asserting reflect P b *) -(* are often referred to as "views". *) -(* iffP, appP, sameP, rwP :: lemmas for direct manipulation of reflection *) -(* views: iffP is used to prove reflection from *) -(* logical equivalence, appP to compose views, and *) -(* sameP and rwP to perform boolean and setoid *) -(* rewriting. *) -(* elimT :: coercion reflect >-> Funclass, which allows the *) -(* direct application of `reflect' views to *) -(* boolean assertions. *) -(* decidable P <-> P is effectively decidable (:= {P} + {~ P}. *) -(* contra, contraL, ... :: contraposition lemmas. *) -(* altP my_viewP :: natural alternative for reflection; given *) -(* lemma myviewP: reflect my_Prop my_formula, *) -(* have [myP | not_myP] := altP my_viewP. *) -(* generates two subgoals, in which my_formula has *) -(* been replaced by true and false, resp., with *) -(* new assumptions myP : my_Prop and *) -(* not_myP: ~~ my_formula. *) -(* Caveat: my_formula must be an APPLICATION, not *) -(* a variable, constant, let-in, etc. (due to the *) -(* poor behaviour of dependent index matching). *) -(* boolP my_formula :: boolean disjunction, equivalent to *) -(* altP (idP my_formula) but circumventing the *) -(* dependent index capture issue; destructing *) -(* boolP my_formula generates two subgoals with *) -(* assumtions my_formula and ~~ myformula. As *) -(* with altP, my_formula must be an application. *) -(* \unless C, P <-> we can assume property P when a something that *) -(* holds under condition C (such as C itself). *) -(* := forall G : Prop, (C -> G) -> (P -> G) -> G. *) -(* This is just C \/ P or rather its impredicative *) -(* encoding, whose usage better fits the above *) -(* description: given a lemma UCP whose conclusion *) -(* is \unless C, P we can assume P by writing: *) -(* wlog hP: / P by apply/UCP; (prove C -> goal). *) -(* or even apply: UCP id _ => hP if the goal is C. *) -(* classically P <-> we can assume P when proving is_true b. *) -(* := forall b : bool, (P -> b) -> b. *) -(* This is equivalent to ~ (~ P) when P : Prop. *) -(* implies P Q == wrapper coinductive type that coerces to P -> Q *) -(* and can be used as a P -> Q view unambigously. *) -(* Useful to avoid spurious insertion of <-> views *) -(* when Q is a conjunction of foralls, as in Lemma *) -(* all_and2 below; conversely, avoids confusion in *) -(* apply views for impredicative properties, such *) -(* as \unless C, P. Also supports contrapositives. *) -(* a && b == the boolean conjunction of a and b. *) -(* a || b == the boolean disjunction of a and b. *) -(* a ==> b == the boolean implication of b by a. *) -(* ~~ a == the boolean negation of a. *) -(* a (+) b == the boolean exclusive or (or sum) of a and b. *) -(* [ /\ P1 , P2 & P3 ] == multiway logical conjunction, up to 5 terms. *) -(* [ \/ P1 , P2 | P3 ] == multiway logical disjunction, up to 4 terms. *) -(* [&& a, b, c & d] == iterated, right associative boolean conjunction *) -(* with arbitrary arity. *) -(* [|| a, b, c | d] == iterated, right associative boolean disjunction *) -(* with arbitrary arity. *) -(* [==> a, b, c => d] == iterated, right associative boolean implication *) -(* with arbitrary arity. *) -(* and3P, ... == specific reflection lemmas for iterated *) -(* connectives. *) -(* andTb, orbAC, ... == systematic names for boolean connective *) -(* properties (see suffix conventions below). *) -(* prop_congr == a tactic to move a boolean equality from *) -(* its coerced form in Prop to the equality *) -(* in bool. *) -(* bool_congr == resolution tactic for blindly weeding out *) -(* like terms from boolean equalities (can fail). *) -(* This file provides a theory of boolean predicates and relations: *) -(* pred T == the type of bool predicates (:= T -> bool). *) -(* simpl_pred T == the type of simplifying bool predicates, using *) -(* the simpl_fun from ssrfun.v. *) -(* rel T == the type of bool relations. *) -(* := T -> pred T or T -> T -> bool. *) -(* simpl_rel T == type of simplifying relations. *) -(* predType == the generic predicate interface, supported for *) -(* for lists and sets. *) -(* pred_class == a coercion class for the predType projection to *) -(* pred; declaring a coercion to pred_class is an *) -(* alternative way of equipping a type with a *) -(* predType structure, which interoperates better *) -(* with coercion subtyping. This is used, e.g., *) -(* for finite sets, so that finite groups inherit *) -(* the membership operation by coercing to sets. *) -(* If P is a predicate the proposition "x satisfies P" can be written *) -(* applicatively as (P x), or using an explicit connective as (x \in P); in *) -(* the latter case we say that P is a "collective" predicate. We use A, B *) -(* rather than P, Q for collective predicates: *) -(* x \in A == x satisfies the (collective) predicate A. *) -(* x \notin A == x doesn't satisfy the (collective) predicate A. *) -(* The pred T type can be used as a generic predicate type for either kind, *) -(* but the two kinds of predicates should not be confused. When a "generic" *) -(* pred T value of one type needs to be passed as the other the following *) -(* conversions should be used explicitly: *) -(* SimplPred P == a (simplifying) applicative equivalent of P. *) -(* mem A == an applicative equivalent of A: *) -(* mem A x simplifies to x \in A. *) -(* Alternatively one can use the syntax for explicit simplifying predicates *) -(* and relations (in the following x is bound in E): *) -(* [pred x | E] == simplifying (see ssrfun) predicate x => E. *) -(* [pred x : T | E] == predicate x => E, with a cast on the argument. *) -(* [pred : T | P] == constant predicate P on type T. *) -(* [pred x | E1 & E2] == [pred x | E1 && E2]; an x : T cast is allowed. *) -(* [pred x in A] == [pred x | x in A]. *) -(* [pred x in A | E] == [pred x | x in A & E]. *) -(* [pred x in A | E1 & E2] == [pred x in A | E1 && E2]. *) -(* [predU A & B] == union of two collective predicates A and B. *) -(* [predI A & B] == intersection of collective predicates A and B. *) -(* [predD A & B] == difference of collective predicates A and B. *) -(* [predC A] == complement of the collective predicate A. *) -(* [preim f of A] == preimage under f of the collective predicate A. *) -(* predU P Q, ... == union, etc of applicative predicates. *) -(* pred0 == the empty predicate. *) -(* predT == the total (always true) predicate. *) -(* if T : predArgType, then T coerces to predT. *) -(* {: T} == T cast to predArgType (e.g., {: bool * nat}) *) -(* In the following, x and y are bound in E: *) -(* [rel x y | E] == simplifying relation x, y => E. *) -(* [rel x y : T | E] == simplifying relation with arguments cast. *) -(* [rel x y in A & B | E] == [rel x y | [&& x \in A, y \in B & E]]. *) -(* [rel x y in A & B] == [rel x y | (x \in A) && (y \in B)]. *) -(* [rel x y in A | E] == [rel x y in A & A | E]. *) -(* [rel x y in A] == [rel x y in A & A]. *) -(* relU R S == union of relations R and S. *) -(* Explicit values of type pred T (i.e., lamdba terms) should always be used *) -(* applicatively, while values of collection types implementing the predType *) -(* interface, such as sequences or sets should always be used as collective *) -(* predicates. Defined constants and functions of type pred T or simpl_pred T *) -(* as well as the explicit simpl_pred T values described below, can generally *) -(* be used either way. Note however that x \in A will not auto-simplify when *) -(* A is an explicit simpl_pred T value; the generic simplification rule inE *) -(* must be used (when A : pred T, the unfold_in rule can be used). Constants *) -(* of type pred T with an explicit simpl_pred value do not auto-simplify when *) -(* used applicatively, but can still be expanded with inE. This behavior can *) -(* be controlled as follows: *) -(* Let A : collective_pred T := [pred x | ... ]. *) -(* The collective_pred T type is just an alias for pred T, but this cast *) -(* stops rewrite inE from expanding the definition of A, thus treating A *) -(* into an abstract collection (unfold_in or in_collective can be used to *) -(* expand manually). *) -(* Let A : applicative_pred T := [pred x | ...]. *) -(* This cast causes inE to turn x \in A into the applicative A x form; *) -(* A will then have to unfolded explicitly with the /A rule. This will *) -(* also apply to any definition that reduces to A (e.g., Let B := A). *) -(* Canonical A_app_pred := ApplicativePred A. *) -(* This declaration, given after definition of A, similarly causes inE to *) -(* turn x \in A into A x, but in addition allows the app_predE rule to *) -(* turn A x back into x \in A; it can be used for any definition of type *) -(* pred T, which makes it especially useful for ambivalent predicates *) -(* as the relational transitive closure connect, that are used in both *) -(* applicative and collective styles. *) -(* Purely for aesthetics, we provide a subtype of collective predicates: *) -(* qualifier q T == a pred T pretty-printing wrapper. An A : qualifier q T *) -(* coerces to pred_class and thus behaves as a collective *) -(* predicate, but x \in A and x \notin A are displayed as: *) -(* x \is A and x \isn't A when q = 0, *) -(* x \is a A and x \isn't a A when q = 1, *) -(* x \is an A and x \isn't an A when q = 2, respectively. *) -(* [qualify x | P] := Qualifier 0 (fun x => P), constructor for the above. *) -(* [qualify x : T | P], [qualify a x | P], [qualify an X | P], etc. *) -(* variants of the above with type constraints and different *) -(* values of q. *) -(* We provide an internal interface to support attaching properties (such as *) -(* being multiplicative) to predicates: *) -(* pred_key p == phantom type that will serve as a support for properties *) -(* to be attached to p : pred_class; instances should be *) -(* created with Fact/Qed so as to be opaque. *) -(* KeyedPred k_p == an instance of the interface structure that attaches *) -(* (k_p : pred_key P) to P; the structure projection is a *) -(* coercion to pred_class. *) -(* KeyedQualifier k_q == an instance of the interface structure that attaches *) -(* (k_q : pred_key q) to (q : qualifier n T). *) -(* DefaultPredKey p == a default value for pred_key p; the vernacular command *) -(* Import DefaultKeying attaches this key to all predicates *) -(* that are not explicitly keyed. *) -(* Keys can be used to attach properties to predicates, qualifiers and *) -(* generic nouns in a way that allows them to be used transparently. The key *) -(* projection of a predicate property structure such as unsignedPred should *) -(* be a pred_key, not a pred, and corresponding lemmas will have the form *) -(* Lemma rpredN R S (oppS : @opprPred R S) (kS : keyed_pred oppS) : *) -(* {mono -%R: x / x \in kS}. *) -(* Because x \in kS will be displayed as x \in S (or x \is S, etc), the *) -(* canonical instance of opprPred will not normally be exposed (it will also *) -(* be erased by /= simplification). In addition each predicate structure *) -(* should have a DefaultPredKey Canonical instance that simply issues the *) -(* property as a proof obligation (which can be caught by the Prop-irrelevant *) -(* feature of the ssreflect plugin). *) -(* Some properties of predicates and relations: *) -(* A =i B <-> A and B are extensionally equivalent. *) -(* {subset A <= B} <-> A is a (collective) subpredicate of B. *) -(* subpred P Q <-> P is an (applicative) subpredicate or Q. *) -(* subrel R S <-> R is a subrelation of S. *) -(* In the following R is in rel T: *) -(* reflexive R <-> R is reflexive. *) -(* irreflexive R <-> R is irreflexive. *) -(* symmetric R <-> R (in rel T) is symmetric (equation). *) -(* pre_symmetric R <-> R is symmetric (implication). *) -(* antisymmetric R <-> R is antisymmetric. *) -(* total R <-> R is total. *) -(* transitive R <-> R is transitive. *) -(* left_transitive R <-> R is a congruence on its left hand side. *) -(* right_transitive R <-> R is a congruence on its right hand side. *) -(* equivalence_rel R <-> R is an equivalence relation. *) -(* Localization of (Prop) predicates; if P1 is convertible to forall x, Qx, *) -(* P2 to forall x y, Qxy and P3 to forall x y z, Qxyz : *) -(* {for y, P1} <-> Qx{y / x}. *) -(* {in A, P1} <-> forall x, x \in A -> Qx. *) -(* {in A1 & A2, P2} <-> forall x y, x \in A1 -> y \in A2 -> Qxy. *) -(* {in A &, P2} <-> forall x y, x \in A -> y \in A -> Qxy. *) -(* {in A1 & A2 & A3, Q3} <-> forall x y z, *) -(* x \in A1 -> y \in A2 -> z \in A3 -> Qxyz. *) -(* {in A1 & A2 &, Q3} == {in A1 & A2 & A2, Q3}. *) -(* {in A1 && A3, Q3} == {in A1 & A1 & A3, Q3}. *) -(* {in A &&, Q3} == {in A & A & A, Q3}. *) -(* {in A, bijective f} == f has a right inverse in A. *) -(* {on C, P1} == forall x, (f x) \in C -> Qx *) -(* when P1 is also convertible to Pf f. *) -(* {on C &, P2} == forall x y, f x \in C -> f y \in C -> Qxy *) -(* when P2 is also convertible to Pf f. *) -(* {on C, P1' & g} == forall x, (f x) \in cd -> Qx *) -(* when P1' is convertible to Pf f *) -(* and P1' g is convertible to forall x, Qx. *) -(* {on C, bijective f} == f has a right inverse on C. *) -(* This file extends the lemma name suffix conventions of ssrfun as follows: *) -(* A -- associativity, as in andbA : associative andb. *) -(* AC -- right commutativity. *) -(* ACA -- self-interchange (inner commutativity), e.g., *) -(* orbACA : (a || b) || (c || d) = (a || c) || (b || d). *) -(* b -- a boolean argument, as in andbb : idempotent andb. *) -(* C -- commutativity, as in andbC : commutative andb, *) -(* or predicate complement, as in predC. *) -(* CA -- left commutativity. *) -(* D -- predicate difference, as in predD. *) -(* E -- elimination, as in negbFE : ~~ b = false -> b. *) -(* F or f -- boolean false, as in andbF : b && false = false. *) -(* I -- left/right injectivity, as in addbI : right_injective addb, *) -(* or predicate intersection, as in predI. *) -(* l -- a left-hand operation, as andb_orl : left_distributive andb orb. *) -(* N or n -- boolean negation, as in andbN : a && (~~ a) = false. *) -(* P -- a characteristic property, often a reflection lemma, as in *) -(* andP : reflect (a /\ b) (a && b). *) -(* r -- a right-hand operation, as orb_andr : rightt_distributive orb andb. *) -(* T or t -- boolean truth, as in andbT: right_id true andb. *) -(* U -- predicate union, as in predU. *) -(* W -- weakening, as in in1W : {in D, forall x, P} -> forall x, P. *) -(******************************************************************************) +(** + A theory of boolean predicates and operators. A large part of this file is + concerned with boolean reflection. + Definitions and notations: + is_true b == the coercion of b : bool to Prop (:= b = true). + This is just input and displayed as `b''. + reflect P b == the reflection inductive predicate, asserting + that the logical proposition P : prop with the + formula b : bool. Lemmas asserting reflect P b + are often referred to as "views". + iffP, appP, sameP, rwP :: lemmas for direct manipulation of reflection + views: iffP is used to prove reflection from + logical equivalence, appP to compose views, and + sameP and rwP to perform boolean and setoid + rewriting. + elimT :: coercion reflect >-> Funclass, which allows the + direct application of `reflect' views to + boolean assertions. + decidable P <-> P is effectively decidable (:= {P} + {~ P}. + contra, contraL, ... :: contraposition lemmas. + altP my_viewP :: natural alternative for reflection; given + lemma myviewP: reflect my_Prop my_formula, + have #[#myP | not_myP#]# := altP my_viewP. + generates two subgoals, in which my_formula has + been replaced by true and false, resp., with + new assumptions myP : my_Prop and + not_myP: ~~ my_formula. + Caveat: my_formula must be an APPLICATION, not + a variable, constant, let-in, etc. (due to the + poor behaviour of dependent index matching). + boolP my_formula :: boolean disjunction, equivalent to + altP (idP my_formula) but circumventing the + dependent index capture issue; destructing + boolP my_formula generates two subgoals with + assumtions my_formula and ~~ myformula. As + with altP, my_formula must be an application. + \unless C, P <-> we can assume property P when a something that + holds under condition C (such as C itself). + := forall G : Prop, (C -> G) -> (P -> G) -> G. + This is just C \/ P or rather its impredicative + encoding, whose usage better fits the above + description: given a lemma UCP whose conclusion + is \unless C, P we can assume P by writing: + wlog hP: / P by apply/UCP; (prove C -> goal). + or even apply: UCP id _ => hP if the goal is C. + classically P <-> we can assume P when proving is_true b. + := forall b : bool, (P -> b) -> b. + This is equivalent to ~ (~ P) when P : Prop. + implies P Q == wrapper variant type that coerces to P -> Q and + can be used as a P -> Q view unambigously. + Useful to avoid spurious insertion of <-> views + when Q is a conjunction of foralls, as in Lemma + all_and2 below; conversely, avoids confusion in + apply views for impredicative properties, such + as \unless C, P. Also supports contrapositives. + a && b == the boolean conjunction of a and b. + a || b == the boolean disjunction of a and b. + a ==> b == the boolean implication of b by a. + ~~ a == the boolean negation of a. + a (+) b == the boolean exclusive or (or sum) of a and b. + #[# /\ P1 , P2 & P3 #]# == multiway logical conjunction, up to 5 terms. + #[# \/ P1 , P2 | P3 #]# == multiway logical disjunction, up to 4 terms. + #[#&& a, b, c & d#]# == iterated, right associative boolean conjunction + with arbitrary arity. + #[#|| a, b, c | d#]# == iterated, right associative boolean disjunction + with arbitrary arity. + #[#==> a, b, c => d#]# == iterated, right associative boolean implication + with arbitrary arity. + and3P, ... == specific reflection lemmas for iterated + connectives. + andTb, orbAC, ... == systematic names for boolean connective + properties (see suffix conventions below). + prop_congr == a tactic to move a boolean equality from + its coerced form in Prop to the equality + in bool. + bool_congr == resolution tactic for blindly weeding out + like terms from boolean equalities (can fail). + This file provides a theory of boolean predicates and relations: + pred T == the type of bool predicates (:= T -> bool). + simpl_pred T == the type of simplifying bool predicates, using + the simpl_fun from ssrfun.v. + rel T == the type of bool relations. + := T -> pred T or T -> T -> bool. + simpl_rel T == type of simplifying relations. + predType == the generic predicate interface, supported for + for lists and sets. + pred_class == a coercion class for the predType projection to + pred; declaring a coercion to pred_class is an + alternative way of equipping a type with a + predType structure, which interoperates better + with coercion subtyping. This is used, e.g., + for finite sets, so that finite groups inherit + the membership operation by coercing to sets. + If P is a predicate the proposition "x satisfies P" can be written + applicatively as (P x), or using an explicit connective as (x \in P); in + the latter case we say that P is a "collective" predicate. We use A, B + rather than P, Q for collective predicates: + x \in A == x satisfies the (collective) predicate A. + x \notin A == x doesn't satisfy the (collective) predicate A. + The pred T type can be used as a generic predicate type for either kind, + but the two kinds of predicates should not be confused. When a "generic" + pred T value of one type needs to be passed as the other the following + conversions should be used explicitly: + SimplPred P == a (simplifying) applicative equivalent of P. + mem A == an applicative equivalent of A: + mem A x simplifies to x \in A. + Alternatively one can use the syntax for explicit simplifying predicates + and relations (in the following x is bound in E): + #[#pred x | E#]# == simplifying (see ssrfun) predicate x => E. + #[#pred x : T | E#]# == predicate x => E, with a cast on the argument. + #[#pred : T | P#]# == constant predicate P on type T. + #[#pred x | E1 & E2#]# == #[#pred x | E1 && E2#]#; an x : T cast is allowed. + #[#pred x in A#]# == #[#pred x | x in A#]#. + #[#pred x in A | E#]# == #[#pred x | x in A & E#]#. + #[#pred x in A | E1 & E2#]# == #[#pred x in A | E1 && E2#]#. + #[#predU A & B#]# == union of two collective predicates A and B. + #[#predI A & B#]# == intersection of collective predicates A and B. + #[#predD A & B#]# == difference of collective predicates A and B. + #[#predC A#]# == complement of the collective predicate A. + #[#preim f of A#]# == preimage under f of the collective predicate A. + predU P Q, ... == union, etc of applicative predicates. + pred0 == the empty predicate. + predT == the total (always true) predicate. + if T : predArgType, then T coerces to predT. + {: T} == T cast to predArgType (e.g., {: bool * nat}) + In the following, x and y are bound in E: + #[#rel x y | E#]# == simplifying relation x, y => E. + #[#rel x y : T | E#]# == simplifying relation with arguments cast. + #[#rel x y in A & B | E#]# == #[#rel x y | #[#&& x \in A, y \in B & E#]# #]#. + #[#rel x y in A & B#]# == #[#rel x y | (x \in A) && (y \in B) #]#. + #[#rel x y in A | E#]# == #[#rel x y in A & A | E#]#. + #[#rel x y in A#]# == #[#rel x y in A & A#]#. + relU R S == union of relations R and S. + Explicit values of type pred T (i.e., lamdba terms) should always be used + applicatively, while values of collection types implementing the predType + interface, such as sequences or sets should always be used as collective + predicates. Defined constants and functions of type pred T or simpl_pred T + as well as the explicit simpl_pred T values described below, can generally + be used either way. Note however that x \in A will not auto-simplify when + A is an explicit simpl_pred T value; the generic simplification rule inE + must be used (when A : pred T, the unfold_in rule can be used). Constants + of type pred T with an explicit simpl_pred value do not auto-simplify when + used applicatively, but can still be expanded with inE. This behavior can + be controlled as follows: + Let A : collective_pred T := #[#pred x | ... #]#. + The collective_pred T type is just an alias for pred T, but this cast + stops rewrite inE from expanding the definition of A, thus treating A + into an abstract collection (unfold_in or in_collective can be used to + expand manually). + Let A : applicative_pred T := #[#pred x | ... #]#. + This cast causes inE to turn x \in A into the applicative A x form; + A will then have to unfolded explicitly with the /A rule. This will + also apply to any definition that reduces to A (e.g., Let B := A). + Canonical A_app_pred := ApplicativePred A. + This declaration, given after definition of A, similarly causes inE to + turn x \in A into A x, but in addition allows the app_predE rule to + turn A x back into x \in A; it can be used for any definition of type + pred T, which makes it especially useful for ambivalent predicates + as the relational transitive closure connect, that are used in both + applicative and collective styles. + Purely for aesthetics, we provide a subtype of collective predicates: + qualifier q T == a pred T pretty-printing wrapper. An A : qualifier q T + coerces to pred_class and thus behaves as a collective + predicate, but x \in A and x \notin A are displayed as: + x \is A and x \isn't A when q = 0, + x \is a A and x \isn't a A when q = 1, + x \is an A and x \isn't an A when q = 2, respectively. + #[#qualify x | P#]# := Qualifier 0 (fun x => P), constructor for the above. + #[#qualify x : T | P#]#, #[#qualify a x | P#]#, #[#qualify an X | P#]#, etc. + variants of the above with type constraints and different + values of q. + We provide an internal interface to support attaching properties (such as + being multiplicative) to predicates: + pred_key p == phantom type that will serve as a support for properties + to be attached to p : pred_class; instances should be + created with Fact/Qed so as to be opaque. + KeyedPred k_p == an instance of the interface structure that attaches + (k_p : pred_key P) to P; the structure projection is a + coercion to pred_class. + KeyedQualifier k_q == an instance of the interface structure that attaches + (k_q : pred_key q) to (q : qualifier n T). + DefaultPredKey p == a default value for pred_key p; the vernacular command + Import DefaultKeying attaches this key to all predicates + that are not explicitly keyed. + Keys can be used to attach properties to predicates, qualifiers and + generic nouns in a way that allows them to be used transparently. The key + projection of a predicate property structure such as unsignedPred should + be a pred_key, not a pred, and corresponding lemmas will have the form + Lemma rpredN R S (oppS : @opprPred R S) (kS : keyed_pred oppS) : + {mono -%%R: x / x \in kS}. + Because x \in kS will be displayed as x \in S (or x \is S, etc), the + canonical instance of opprPred will not normally be exposed (it will also + be erased by /= simplification). In addition each predicate structure + should have a DefaultPredKey Canonical instance that simply issues the + property as a proof obligation (which can be caught by the Prop-irrelevant + feature of the ssreflect plugin). + Some properties of predicates and relations: + A =i B <-> A and B are extensionally equivalent. + {subset A <= B} <-> A is a (collective) subpredicate of B. + subpred P Q <-> P is an (applicative) subpredicate or Q. + subrel R S <-> R is a subrelation of S. + In the following R is in rel T: + reflexive R <-> R is reflexive. + irreflexive R <-> R is irreflexive. + symmetric R <-> R (in rel T) is symmetric (equation). + pre_symmetric R <-> R is symmetric (implication). + antisymmetric R <-> R is antisymmetric. + total R <-> R is total. + transitive R <-> R is transitive. + left_transitive R <-> R is a congruence on its left hand side. + right_transitive R <-> R is a congruence on its right hand side. + equivalence_rel R <-> R is an equivalence relation. + Localization of (Prop) predicates; if P1 is convertible to forall x, Qx, + P2 to forall x y, Qxy and P3 to forall x y z, Qxyz : + {for y, P1} <-> Qx{y / x}. + {in A, P1} <-> forall x, x \in A -> Qx. + {in A1 & A2, P2} <-> forall x y, x \in A1 -> y \in A2 -> Qxy. + {in A &, P2} <-> forall x y, x \in A -> y \in A -> Qxy. + {in A1 & A2 & A3, Q3} <-> forall x y z, + x \in A1 -> y \in A2 -> z \in A3 -> Qxyz. + {in A1 & A2 &, Q3} == {in A1 & A2 & A2, Q3}. + {in A1 && A3, Q3} == {in A1 & A1 & A3, Q3}. + {in A &&, Q3} == {in A & A & A, Q3}. + {in A, bijective f} == f has a right inverse in A. + {on C, P1} == forall x, (f x) \in C -> Qx + when P1 is also convertible to Pf f. + {on C &, P2} == forall x y, f x \in C -> f y \in C -> Qxy + when P2 is also convertible to Pf f. + {on C, P1' & g} == forall x, (f x) \in cd -> Qx + when P1' is convertible to Pf f + and P1' g is convertible to forall x, Qx. + {on C, bijective f} == f has a right inverse on C. + This file extends the lemma name suffix conventions of ssrfun as follows: + A -- associativity, as in andbA : associative andb. + AC -- right commutativity. + ACA -- self-interchange (inner commutativity), e.g., + orbACA : (a || b) || (c || d) = (a || c) || (b || d). + b -- a boolean argument, as in andbb : idempotent andb. + C -- commutativity, as in andbC : commutative andb, + or predicate complement, as in predC. + CA -- left commutativity. + D -- predicate difference, as in predD. + E -- elimination, as in negbFE : ~~ b = false -> b. + F or f -- boolean false, as in andbF : b && false = false. + I -- left/right injectivity, as in addbI : right_injective addb, + or predicate intersection, as in predI. + l -- a left-hand operation, as andb_orl : left_distributive andb orb. + N or n -- boolean negation, as in andbN : a && (~~ a) = false. + P -- a characteristic property, often a reflection lemma, as in + andP : reflect (a /\ b) (a && b). + r -- a right-hand operation, as orb_andr : rightt_distributive orb andb. + T or t -- boolean truth, as in andbT: right_id true andb. + U -- predicate union, as in predU. + W -- weakening, as in in1W : {in D, forall x, P} -> forall x, P. **) + Set Implicit Arguments. Unset Strict Implicit. @@ -288,23 +290,24 @@ Reserved Notation "x \notin A" Reserved Notation "p1 =i p2" (at level 70, format "'[hv' p1 '/ ' =i p2 ']'", no associativity). -(* We introduce a number of n-ary "list-style" notations that share a common *) -(* format, namely *) -(* [op arg1, arg2, ... last_separator last_arg] *) -(* This usually denotes a right-associative applications of op, e.g., *) -(* [&& a, b, c & d] denotes a && (b && (c && d)) *) -(* The last_separator must be a non-operator token. Here we use &, | or =>; *) -(* our default is &, but we try to match the intended meaning of op. The *) -(* separator is a workaround for limitations of the parsing engine; the same *) -(* limitations mean the separator cannot be omitted even when last_arg can. *) -(* The Notation declarations are complicated by the separate treatment for *) -(* some fixed arities (binary for bool operators, and all arities for Prop *) -(* operators). *) -(* We also use the square brackets in comprehension-style notations *) -(* [type var separator expr] *) -(* where "type" is the type of the comprehension (e.g., pred) and "separator" *) -(* is | or => . It is important that in other notations a leading square *) -(* bracket [ is always followed by an operator symbol or a fixed identifier. *) +(** + We introduce a number of n-ary "list-style" notations that share a common + format, namely + #[#op arg1, arg2, ... last_separator last_arg#]# + This usually denotes a right-associative applications of op, e.g., + #[#&& a, b, c & d#]# denotes a && (b && (c && d)) + The last_separator must be a non-operator token. Here we use &, | or =>; + our default is &, but we try to match the intended meaning of op. The + separator is a workaround for limitations of the parsing engine; the same + limitations mean the separator cannot be omitted even when last_arg can. + The Notation declarations are complicated by the separate treatment for + some fixed arities (binary for bool operators, and all arities for Prop + operators). + We also use the square brackets in comprehension-style notations + #[#type var separator expr#]# + where "type" is the type of the comprehension (e.g., pred) and "separator" + is | or => . It is important that in other notations a leading square + bracket #[# is always followed by an operator symbol or a fixed identifier. **) Reserved Notation "[ /\ P1 & P2 ]" (at level 0, only parsing). Reserved Notation "[ /\ P1 , P2 & P3 ]" (at level 0, format @@ -344,19 +347,19 @@ Reserved Notation "[ 'rel' x y => E ]" (at level 0, x, y at level 8, format Reserved Notation "[ 'rel' x y : T => E ]" (at level 0, x, y at level 8, format "'[hv' [ 'rel' x y : T => '/ ' E ] ']'"). -(* Shorter delimiter *) +(** Shorter delimiter **) Delimit Scope bool_scope with B. Open Scope bool_scope. -(* An alternative to xorb that behaves somewhat better wrt simplification. *) +(** An alternative to xorb that behaves somewhat better wrt simplification. **) Definition addb b := if b then negb else id. -(* Notation for && and || is declared in Init.Datatypes. *) +(** Notation for && and || is declared in Init.Datatypes. **) Notation "~~ b" := (negb b) : bool_scope. Notation "b ==> c" := (implb b c) : bool_scope. Notation "b1 (+) b2" := (addb b1 b2) : bool_scope. -(* Constant is_true b := b = true is defined in Init.Datatypes. *) +(** Constant is_true b := b = true is defined in Init.Datatypes. **) Coercion is_true : bool >-> Sortclass. (* Prop *) Lemma prop_congr : forall b b' : bool, b = b' -> b = b' :> Prop. @@ -364,21 +367,22 @@ Proof. by move=> b b' ->. Qed. Ltac prop_congr := apply: prop_congr. -(* Lemmas for trivial. *) +(** Lemmas for trivial. **) Lemma is_true_true : true. Proof. by []. Qed. Lemma not_false_is_true : ~ false. Proof. by []. Qed. Lemma is_true_locked_true : locked true. Proof. by unlock. Qed. Hint Resolve is_true_true not_false_is_true is_true_locked_true. -(* Shorter names. *) +(** Shorter names. **) Definition isT := is_true_true. Definition notF := not_false_is_true. -(* Negation lemmas. *) +(** Negation lemmas. **) -(* We generally take NEGATION as the standard form of a false condition: *) -(* negative boolean hypotheses should be of the form ~~ b, rather than ~ b or *) -(* b = false, as much as possible. *) +(** + We generally take NEGATION as the standard form of a false condition: + negative boolean hypotheses should be of the form ~~ b, rather than ~ b or + b = false, as much as possible. **) Lemma negbT b : b = false -> ~~ b. Proof. by case: b. Qed. Lemma negbTE b : ~~ b -> b = false. Proof. by case: b. Qed. @@ -426,8 +430,9 @@ Proof. by move/contra=> notb_notc /notb_notc/negbTE. Qed. Lemma contraFF (c b : bool) : (c -> b) -> b = false -> c = false. Proof. by move/contraFN=> bF_notc /bF_notc/negbTE. Qed. -(* Coercion of sum-style datatypes into bool, which makes it possible *) -(* to use ssr's boolean if rather than Coq's "generic" if. *) +(** + Coercion of sum-style datatypes into bool, which makes it possible + to use ssr's boolean if rather than Coq's "generic" if. **) Coercion isSome T (u : option T) := if u is Some _ then true else false. @@ -441,22 +446,23 @@ Prenex Implicits isSome is_inl is_left is_inleft. Definition decidable P := {P} + {~ P}. -(* Lemmas for ifs with large conditions, which allow reasoning about the *) -(* condition without repeating it inside the proof (the latter IS *) -(* preferable when the condition is short). *) -(* Usage : *) -(* if the goal contains (if cond then ...) = ... *) -(* case: ifP => Hcond. *) -(* generates two subgoal, with the assumption Hcond : cond = true/false *) -(* Rewrite if_same eliminates redundant ifs *) -(* Rewrite (fun_if f) moves a function f inside an if *) -(* Rewrite if_arg moves an argument inside a function-valued if *) +(** + Lemmas for ifs with large conditions, which allow reasoning about the + condition without repeating it inside the proof (the latter IS + preferable when the condition is short). + Usage : + if the goal contains (if cond then ...) = ... + case: ifP => Hcond. + generates two subgoal, with the assumption Hcond : cond = true/false + Rewrite if_same eliminates redundant ifs + Rewrite (fun_if f) moves a function f inside an if + Rewrite if_arg moves an argument inside a function-valued if **) Section BoolIf. Variables (A B : Type) (x : A) (f : A -> B) (b : bool) (vT vF : A). -CoInductive if_spec (not_b : Prop) : bool -> A -> Set := +Variant if_spec (not_b : Prop) : bool -> A -> Set := | IfSpecTrue of b : if_spec not_b true vT | IfSpecFalse of not_b : if_spec not_b false vF. @@ -483,13 +489,13 @@ Lemma if_arg (fT fF : A -> B) : (if b then fT else fF) x = if b then fT x else fF x. Proof. by case b. Qed. -(* Turning a boolean "if" form into an application. *) +(** Turning a boolean "if" form into an application. **) Definition if_expr := if b then vT else vF. Lemma ifE : (if b then vT else vF) = if_expr. Proof. by []. Qed. End BoolIf. -(* Core (internal) reflection lemmas, used for the three kinds of views. *) +(** Core (internal) reflection lemmas, used for the three kinds of views. **) Section ReflectCore. @@ -517,7 +523,7 @@ Proof. by case Hb => [? _ H ? | ? H _]; case: H. Qed. End ReflectCore. -(* Internal negated reflection lemmas *) +(** Internal negated reflection lemmas **) Section ReflectNegCore. Variables (P Q : Prop) (b c : bool). @@ -537,7 +543,7 @@ Proof. by rewrite -if_neg; apply: xorPif. Qed. End ReflectNegCore. -(* User-oriented reflection lemmas *) +(** User-oriented reflection lemmas **) Section Reflect. Variables (P Q : Prop) (b b' c : bool). @@ -584,8 +590,8 @@ Lemma rwP : P <-> b. Proof. by split; [apply: introT | apply: elimT]. Qed. Lemma rwP2 : reflect Q b -> (P <-> Q). Proof. by move=> Qb; split=> ?; [apply: appP | apply: elimT; case: Qb]. Qed. -(* Predicate family to reflect excluded middle in bool. *) -CoInductive alt_spec : bool -> Type := +(** Predicate family to reflect excluded middle in bool. **) +Variant alt_spec : bool -> Type := | AltTrue of P : alt_spec true | AltFalse of ~~ b : alt_spec false. @@ -600,10 +606,10 @@ Hint View for apply/ introTF|3 introNTF|3 introTFn|3 elimT|2 elimTn|2 elimN|2. Hint View for apply// equivPif|3 xorPif|3 equivPifn|3 xorPifn|3. -(* Allow the direct application of a reflection lemma to a boolean assertion. *) +(** Allow the direct application of a reflection lemma to a boolean assertion. **) Coercion elimT : reflect >-> Funclass. -CoInductive implies P Q := Implies of P -> Q. +Variant implies P Q := Implies of P -> Q. Lemma impliesP P Q : implies P Q -> P -> Q. Proof. by case. Qed. Lemma impliesPn (P Q : Prop) : implies P Q -> ~ Q -> ~ P. Proof. by case=> iP ? /iP. Qed. @@ -611,7 +617,7 @@ Coercion impliesP : implies >-> Funclass. Hint View for move/ impliesPn|2 impliesP|2. Hint View for apply/ impliesPn|2 impliesP|2. -(* Impredicative or, which can emulate a classical not-implies. *) +(** Impredicative or, which can emulate a classical not-implies. **) Definition unless condition property : Prop := forall goal : Prop, (condition -> goal) -> (property -> goal) -> goal. @@ -637,8 +643,9 @@ Proof. by split; apply=> [hC|hP]; [apply/unlessL/unlessL | apply/unlessR]. Qed. Lemma unless_contra b C : implies (~~ b -> C) (\unless C, b). Proof. by split; case: b => [_ | hC]; [apply/unlessR | apply/unlessL/hC]. Qed. -(* Classical reasoning becomes directly accessible for any bool subgoal. *) -(* Note that we cannot use "unless" here for lack of universe polymorphism. *) +(** + Classical reasoning becomes directly accessible for any bool subgoal. + Note that we cannot use "unless" here for lack of universe polymorphism. **) Definition classically P : Prop := forall b : bool, (P -> b) -> b. Lemma classicP (P : Prop) : classically P <-> ~ ~ P. @@ -669,11 +676,12 @@ move=> iPQ []// notPQ; apply/notPQ=> /iPQ-cQ. by case: notF; apply: cQ => hQ; apply: notPQ. Qed. -(* List notations for wider connectives; the Prop connectives have a fixed *) -(* width so as to avoid iterated destruction (we go up to width 5 for /\, and *) -(* width 4 for or). The bool connectives have arbitrary widths, but denote *) -(* expressions that associate to the RIGHT. This is consistent with the right *) -(* associativity of list expressions and thus more convenient in most proofs. *) +(** + List notations for wider connectives; the Prop connectives have a fixed + width so as to avoid iterated destruction (we go up to width 5 for /\, and + width 4 for or). The bool connectives have arbitrary widths, but denote + expressions that associate to the RIGHT. This is consistent with the right + associativity of list expressions and thus more convenient in most proofs. **) Inductive and3 (P1 P2 P3 : Prop) : Prop := And3 of P1 & P2 & P3. @@ -822,7 +830,7 @@ Arguments implyP [b1 b2]. Prenex Implicits idP idPn negP negPn negPf. Prenex Implicits andP and3P and4P and5P orP or3P or4P nandP norP implyP. -(* Shorter, more systematic names for the boolean connectives laws. *) +(** Shorter, more systematic names for the boolean connectives laws. **) Lemma andTb : left_id true andb. Proof. by []. Qed. Lemma andFb : left_zero false andb. Proof. by []. Qed. @@ -880,14 +888,14 @@ Proof. by case: a; case: b. Qed. Lemma negb_or (a b : bool) : ~~ (a || b) = ~~ a && ~~ b. Proof. by case: a; case: b. Qed. -(* Pseudo-cancellation -- i.e, absorbtion *) +(** Pseudo-cancellation -- i.e, absorbtion **) Lemma andbK a b : a && b || a = a. Proof. by case: a; case: b. Qed. Lemma andKb a b : a || b && a = a. Proof. by case: a; case: b. Qed. Lemma orbK a b : (a || b) && a = a. Proof. by case: a; case: b. Qed. Lemma orKb a b : a && (b || a) = a. Proof. by case: a; case: b. Qed. -(* Imply *) +(** Imply **) Lemma implybT b : b ==> true. Proof. by case: b. Qed. Lemma implybF b : (b ==> false) = ~~ b. Proof. by case: b. Qed. @@ -917,7 +925,7 @@ Proof. by case: a; case: b => // ->. Qed. Lemma implyb_id2l (a b c : bool) : (a -> b = c) -> (a ==> b) = (a ==> c). Proof. by case: a; case: b; case: c => // ->. Qed. -(* Addition (xor) *) +(** Addition (xor) **) Lemma addFb : left_id false addb. Proof. by []. Qed. Lemma addbF : right_id false addb. Proof. by case. Qed. @@ -946,9 +954,10 @@ Lemma addbP a b : reflect (~~ a = b) (a (+) b). Proof. by case: a; case: b; constructor. Qed. Arguments addbP [a b]. -(* Resolution tactic for blindly weeding out common terms from boolean *) -(* equalities. When faced with a goal of the form (andb/orb/addb b1 b2) = b3 *) -(* they will try to locate b1 in b3 and remove it. This can fail! *) +(** + Resolution tactic for blindly weeding out common terms from boolean + equalities. When faced with a goal of the form (andb/orb/addb b1 b2) = b3 + they will try to locate b1 in b3 and remove it. This can fail! **) Ltac bool_congr := match goal with @@ -963,100 +972,101 @@ Ltac bool_congr := | |- (~~ ?X1 = ?X2) => congr 1 negb end. -(******************************************************************************) -(* Predicates, i.e., packaged functions to bool. *) -(* - pred T, the basic type for predicates over a type T, is simply an alias *) -(* for T -> bool. *) -(* We actually distinguish two kinds of predicates, which we call applicative *) -(* and collective, based on the syntax used to test them at some x in T: *) -(* - For an applicative predicate P, one uses prefix syntax: *) -(* P x *) -(* Also, most operations on applicative predicates use prefix syntax as *) -(* well (e.g., predI P Q). *) -(* - For a collective predicate A, one uses infix syntax: *) -(* x \in A *) -(* and all operations on collective predicates use infix syntax as well *) -(* (e.g., [predI A & B]). *) -(* There are only two kinds of applicative predicates: *) -(* - pred T, the alias for T -> bool mentioned above *) -(* - simpl_pred T, an alias for simpl_fun T bool with a coercion to pred T *) -(* that auto-simplifies on application (see ssrfun). *) -(* On the other hand, the set of collective predicate types is open-ended via *) -(* - predType T, a Structure that can be used to put Canonical collective *) -(* predicate interpretation on other types, such as lists, tuples, *) -(* finite sets, etc. *) -(* Indeed, we define such interpretations for applicative predicate types, *) -(* which can therefore also be used with the infix syntax, e.g., *) -(* x \in predI P Q *) -(* Moreover these infix forms are convertible to their prefix counterpart *) -(* (e.g., predI P Q x which in turn simplifies to P x && Q x). The converse *) -(* is not true, however; collective predicate types cannot, in general, be *) -(* general, be used applicatively, because of the "uniform inheritance" *) -(* restriction on implicit coercions. *) -(* However, we do define an explicit generic coercion *) -(* - mem : forall (pT : predType), pT -> mem_pred T *) -(* where mem_pred T is a variant of simpl_pred T that preserves the infix *) -(* syntax, i.e., mem A x auto-simplifies to x \in A. *) -(* Indeed, the infix "collective" operators are notation for a prefix *) -(* operator with arguments of type mem_pred T or pred T, applied to coerced *) -(* collective predicates, e.g., *) -(* Notation "x \in A" := (in_mem x (mem A)). *) -(* This prevents the variability in the predicate type from interfering with *) -(* the application of generic lemmas. Moreover this also makes it much easier *) -(* to define generic lemmas, because the simplest type -- pred T -- can be *) -(* used as the type of generic collective predicates, provided one takes care *) -(* not to use it applicatively; this avoids the burden of having to declare a *) -(* different predicate type for each predicate parameter of each section or *) -(* lemma. *) -(* This trick is made possible by the fact that the constructor of the *) -(* mem_pred T type aligns the unification process, forcing a generic *) -(* "collective" predicate A : pred T to unify with the actual collective B, *) -(* which mem has coerced to pred T via an internal, hidden implicit coercion, *) -(* supplied by the predType structure for B. Users should take care not to *) -(* inadvertently "strip" (mem B) down to the coerced B, since this will *) -(* expose the internal coercion: Coq will display a term B x that cannot be *) -(* typed as such. The topredE lemma can be used to restore the x \in B *) -(* syntax in this case. While -topredE can conversely be used to change *) -(* x \in P into P x, it is safer to use the inE and memE lemmas instead, as *) -(* they do not run the risk of exposing internal coercions. As a consequence *) -(* it is better to explicitly cast a generic applicative pred T to simpl_pred *) -(* using the SimplPred constructor, when it is used as a collective predicate *) -(* (see, e.g., Lemma eq_big in bigop). *) -(* We also sometimes "instantiate" the predType structure by defining a *) -(* coercion to the sort of the predPredType structure. This works better for *) -(* types such as {set T} that have subtypes that coerce to them, since the *) -(* same coercion will be inserted by the application of mem. It also lets us *) -(* turn any Type aT : predArgType into the total predicate over that type, *) -(* i.e., fun _: aT => true. This allows us to write, e.g., #|'I_n| for the *) -(* cardinal of the (finite) type of integers less than n. *) -(* Collective predicates have a specific extensional equality, *) -(* - A =i B, *) -(* while applicative predicates use the extensional equality of functions, *) -(* - P =1 Q *) -(* The two forms are convertible, however. *) -(* We lift boolean operations to predicates, defining: *) -(* - predU (union), predI (intersection), predC (complement), *) -(* predD (difference), and preim (preimage, i.e., composition) *) -(* For each operation we define three forms, typically: *) -(* - predU : pred T -> pred T -> simpl_pred T *) -(* - [predU A & B], a Notation for predU (mem A) (mem B) *) -(* - xpredU, a Notation for the lambda-expression inside predU, *) -(* which is mostly useful as an argument of =1, since it exposes the head *) -(* head constant of the expression to the ssreflect matching algorithm. *) -(* The syntax for the preimage of a collective predicate A is *) -(* - [preim f of A] *) -(* Finally, the generic syntax for defining a simpl_pred T is *) -(* - [pred x : T | P(x)], [pred x | P(x)], [pred x in A | P(x)], etc. *) -(* We also support boolean relations, but only the applicative form, with *) -(* types *) -(* - rel T, an alias for T -> pred T *) -(* - simpl_rel T, an auto-simplifying version, and syntax *) -(* [rel x y | P(x,y)], [rel x y in A & B | P(x,y)], etc. *) -(* The notation [rel of fA] can be used to coerce a function returning a *) -(* collective predicate to one returning pred T. *) -(* Finally, note that there is specific support for ambivalent predicates *) -(* that can work in either style, as per this file's head descriptor. *) -(******************************************************************************) + +(** + Predicates, i.e., packaged functions to bool. + - pred T, the basic type for predicates over a type T, is simply an alias + for T -> bool. + We actually distinguish two kinds of predicates, which we call applicative + and collective, based on the syntax used to test them at some x in T: + - For an applicative predicate P, one uses prefix syntax: + P x + Also, most operations on applicative predicates use prefix syntax as + well (e.g., predI P Q). + - For a collective predicate A, one uses infix syntax: + x \in A + and all operations on collective predicates use infix syntax as well + (e.g., #[#predI A & B#]#). + There are only two kinds of applicative predicates: + - pred T, the alias for T -> bool mentioned above + - simpl_pred T, an alias for simpl_fun T bool with a coercion to pred T + that auto-simplifies on application (see ssrfun). + On the other hand, the set of collective predicate types is open-ended via + - predType T, a Structure that can be used to put Canonical collective + predicate interpretation on other types, such as lists, tuples, + finite sets, etc. + Indeed, we define such interpretations for applicative predicate types, + which can therefore also be used with the infix syntax, e.g., + x \in predI P Q + Moreover these infix forms are convertible to their prefix counterpart + (e.g., predI P Q x which in turn simplifies to P x && Q x). The converse + is not true, however; collective predicate types cannot, in general, be + general, be used applicatively, because of the "uniform inheritance" + restriction on implicit coercions. + However, we do define an explicit generic coercion + - mem : forall (pT : predType), pT -> mem_pred T + where mem_pred T is a variant of simpl_pred T that preserves the infix + syntax, i.e., mem A x auto-simplifies to x \in A. + Indeed, the infix "collective" operators are notation for a prefix + operator with arguments of type mem_pred T or pred T, applied to coerced + collective predicates, e.g., + Notation "x \in A" := (in_mem x (mem A)). + This prevents the variability in the predicate type from interfering with + the application of generic lemmas. Moreover this also makes it much easier + to define generic lemmas, because the simplest type -- pred T -- can be + used as the type of generic collective predicates, provided one takes care + not to use it applicatively; this avoids the burden of having to declare a + different predicate type for each predicate parameter of each section or + lemma. + This trick is made possible by the fact that the constructor of the + mem_pred T type aligns the unification process, forcing a generic + "collective" predicate A : pred T to unify with the actual collective B, + which mem has coerced to pred T via an internal, hidden implicit coercion, + supplied by the predType structure for B. Users should take care not to + inadvertently "strip" (mem B) down to the coerced B, since this will + expose the internal coercion: Coq will display a term B x that cannot be + typed as such. The topredE lemma can be used to restore the x \in B + syntax in this case. While -topredE can conversely be used to change + x \in P into P x, it is safer to use the inE and memE lemmas instead, as + they do not run the risk of exposing internal coercions. As a consequence + it is better to explicitly cast a generic applicative pred T to simpl_pred + using the SimplPred constructor, when it is used as a collective predicate + (see, e.g., Lemma eq_big in bigop). + We also sometimes "instantiate" the predType structure by defining a + coercion to the sort of the predPredType structure. This works better for + types such as {set T} that have subtypes that coerce to them, since the + same coercion will be inserted by the application of mem. It also lets us + turn any Type aT : predArgType into the total predicate over that type, + i.e., fun _: aT => true. This allows us to write, e.g., ##|'I_n| for the + cardinal of the (finite) type of integers less than n. + Collective predicates have a specific extensional equality, + - A =i B, + while applicative predicates use the extensional equality of functions, + - P =1 Q + The two forms are convertible, however. + We lift boolean operations to predicates, defining: + - predU (union), predI (intersection), predC (complement), + predD (difference), and preim (preimage, i.e., composition) + For each operation we define three forms, typically: + - predU : pred T -> pred T -> simpl_pred T + - #[#predU A & B#]#, a Notation for predU (mem A) (mem B) + - xpredU, a Notation for the lambda-expression inside predU, + which is mostly useful as an argument of =1, since it exposes the head + head constant of the expression to the ssreflect matching algorithm. + The syntax for the preimage of a collective predicate A is + - #[#preim f of A#]# + Finally, the generic syntax for defining a simpl_pred T is + - #[#pred x : T | P(x) #]#, #[#pred x | P(x) #]#, #[#pred x in A | P(x) #]#, etc. + We also support boolean relations, but only the applicative form, with + types + - rel T, an alias for T -> pred T + - simpl_rel T, an auto-simplifying version, and syntax + #[#rel x y | P(x,y) #]#, #[#rel x y in A & B | P(x,y) #]#, etc. + The notation #[#rel of fA#]# can be used to coerce a function returning a + collective predicate to one returning pred T. + Finally, note that there is specific support for ambivalent predicates + that can work in either style, as per this file's head descriptor. **) + Definition pred T := T -> bool. @@ -1094,8 +1104,9 @@ Coercion applicative_pred_of_simpl (p : simpl_pred) : applicative_pred := fun_of_simpl p. Coercion collective_pred_of_simpl (p : simpl_pred) : collective_pred := fun x => (let: SimplFun f := p in fun _ => f x) x. -(* Note: applicative_of_simpl is convertible to pred_of_simpl, while *) -(* collective_of_simpl is not. *) +(** + Note: applicative_of_simpl is convertible to pred_of_simpl, while + collective_of_simpl is not. **) Definition pred0 := SimplPred xpred0. Definition predT := SimplPred xpredT. @@ -1119,7 +1130,7 @@ Proof. by move=> *; apply/orP; left. Qed. Lemma subrelUr r1 r2 : subrel r2 (relU r1 r2). Proof. by move=> *; apply/orP; right. Qed. -CoInductive mem_pred := Mem of pred T. +Variant mem_pred := Mem of pred T. Definition isMem pT topred mem := mem = (fun p : pT => Mem [eta topred p]). @@ -1166,19 +1177,21 @@ Notation "[ 'rel' x y : T | E ]" := (SimplRel (fun x y : T => E%B)) Notation "[ 'predType' 'of' T ]" := (@clone_pred _ T _ id _ _ id) (at level 0, format "[ 'predType' 'of' T ]") : form_scope. -(* This redundant coercion lets us "inherit" the simpl_predType canonical *) -(* instance by declaring a coercion to simpl_pred. This hack is the only way *) -(* to put a predType structure on a predArgType. We use simpl_pred rather *) -(* than pred to ensure that /= removes the identity coercion. Note that the *) -(* coercion will never be used directly for simpl_pred, since the canonical *) -(* instance should always be resolved. *) +(** + This redundant coercion lets us "inherit" the simpl_predType canonical + instance by declaring a coercion to simpl_pred. This hack is the only way + to put a predType structure on a predArgType. We use simpl_pred rather + than pred to ensure that /= removes the identity coercion. Note that the + coercion will never be used directly for simpl_pred, since the canonical + instance should always be resolved. **) Notation pred_class := (pred_sort (predPredType _)). Coercion sort_of_simpl_pred T (p : simpl_pred T) : pred_class := p : pred T. -(* This lets us use some types as a synonym for their universal predicate. *) -(* Unfortunately, this won't work for existing types like bool, unless we *) -(* redefine bool, true, false and all bool ops. *) +(** + This lets us use some types as a synonym for their universal predicate. + Unfortunately, this won't work for existing types like bool, unless we + redefine bool, true, false and all bool ops. **) Definition predArgType := Type. Bind Scope type_scope with predArgType. Identity Coercion sort_of_predArgType : predArgType >-> Sortclass. @@ -1187,8 +1200,9 @@ Coercion pred_of_argType (T : predArgType) : simpl_pred T := predT. Notation "{ : T }" := (T%type : predArgType) (at level 0, format "{ : T }") : type_scope. -(* These must be defined outside a Section because "cooking" kills the *) -(* nosimpl tag. *) +(** + These must be defined outside a Section because "cooking" kills the + nosimpl tag. **) Definition mem T (pT : predType T) : pT -> mem_pred T := nosimpl (let: @PredType _ _ _ (exist _ mem _) := pT return pT -> _ in mem). @@ -1254,12 +1268,13 @@ Section simpl_mem. Variables (T : Type) (pT : predType T). Implicit Types (x : T) (p : pred T) (sp : simpl_pred T) (pp : pT). -(* Bespoke structures that provide fine-grained control over matching the *) -(* various forms of the \in predicate; note in particular the different forms *) -(* of hoisting that are used. We had to work around several bugs in the *) -(* implementation of unification, notably improper expansion of telescope *) -(* projections and overwriting of a variable assignment by a later *) -(* unification (probably due to conversion cache cross-talk). *) +(** + Bespoke structures that provide fine-grained control over matching the + various forms of the \in predicate; note in particular the different forms + of hoisting that are used. We had to work around several bugs in the + implementation of unification, notably improper expansion of telescope + projections and overwriting of a variable assignment by a later + unification (probably due to conversion cache cross-talk). **) Structure manifest_applicative_pred p := ManifestApplicativePred { manifest_applicative_pred_value :> pred T; _ : manifest_applicative_pred_value = p @@ -1305,10 +1320,11 @@ Lemma in_simpl x p (msp : manifest_simpl_pred p) : in_mem x (Mem [eta fun_of_simpl (msp : simpl_pred T)]) = p x. Proof. by case: msp => _ /= ->. Qed. -(* Because of the explicit eta expansion in the left-hand side, this lemma *) -(* should only be used in a right-to-left direction. The 8.3 hack allowing *) -(* partial right-to-left use does not work with the improved expansion *) -(* heuristics in 8.4. *) +(** + Because of the explicit eta expansion in the left-hand side, this lemma + should only be used in a right-to-left direction. The 8.3 hack allowing + partial right-to-left use does not work with the improved expansion + heuristics in 8.4. **) Lemma unfold_in x p : (x \in ([eta p] : pred T)) = p x. Proof. by []. Qed. @@ -1327,9 +1343,9 @@ Proof. by rewrite -mem_topred. Qed. End simpl_mem. -(* Qualifiers and keyed predicates. *) +(** Qualifiers and keyed predicates. **) -CoInductive qualifier (q : nat) T := Qualifier of predPredType T. +Variant qualifier (q : nat) T := Qualifier of predPredType T. Coercion has_quality n T (q : qualifier n T) : pred_class := fun x => let: Qualifier _ p := q in p x. @@ -1371,12 +1387,12 @@ Notation "[ 'qualify' 'an' x | P ]" := (Qualifier 2 (fun x => P%B)) Notation "[ 'qualify' 'an' x : T | P ]" := (Qualifier 2 (fun x : T => P%B)) (at level 0, x at level 99, only parsing) : form_scope. -(* Keyed predicates: support for property-bearing predicate interfaces. *) +(** Keyed predicates: support for property-bearing predicate interfaces. **) Section KeyPred. Variable T : Type. -CoInductive pred_key (p : predPredType T) := DefaultPredKey. +Variant pred_key (p : predPredType T) := DefaultPredKey. Variable p : predPredType T. Structure keyed_pred (k : pred_key p) := @@ -1388,13 +1404,14 @@ Definition KeyedPred := @PackKeyedPred k p (frefl _). Variable k_p : keyed_pred k. Lemma keyed_predE : k_p =i p. Proof. by case: k_p. Qed. -(* Instances that strip the mem cast; the first one has "pred_of_mem" as its *) -(* projection head value, while the second has "pred_of_simpl". The latter *) -(* has the side benefit of preempting accidental misdeclarations. *) -(* Note: pred_of_mem is the registered mem >-> pred_class coercion, while *) -(* simpl_of_mem; pred_of_simpl is the mem >-> pred >=> Funclass coercion. We *) -(* must write down the coercions explicitly as the Canonical head constant *) -(* computation does not strip casts !! *) +(** + Instances that strip the mem cast; the first one has "pred_of_mem" as its + projection head value, while the second has "pred_of_simpl". The latter + has the side benefit of preempting accidental misdeclarations. + Note: pred_of_mem is the registered mem >-> pred_class coercion, while + simpl_of_mem; pred_of_simpl is the mem >-> pred >=> Funclass coercion. We + must write down the coercions explicitly as the Canonical head constant + computation does not strip casts !! **) Canonical keyed_mem := @PackKeyedPred k (pred_of_mem (mem k_p)) keyed_predE. Canonical keyed_mem_simpl := @@ -1434,7 +1451,7 @@ Canonical default_keyed_qualifier T n (q : qualifier n T) := End DefaultKeying. -(* Skolemizing with conditions. *) +(** Skolemizing with conditions. **) Lemma all_tag_cond_dep I T (C : pred I) U : (forall x, T x) -> (forall x, C x -> {y : T x & U x y}) -> @@ -1461,8 +1478,9 @@ Proof. by move=> y0; apply: all_sig_cond_dep. Qed. Section RelationProperties. -(* Caveat: reflexive should not be used to state lemmas, as auto and trivial *) -(* will not expand the constant. *) +(** + Caveat: reflexive should not be used to state lemmas, as auto and trivial + will not expand the constant. **) Variable T : Type. @@ -1496,8 +1514,9 @@ Proof. by move=> x y /sym_left_transitive Rxy z; rewrite !(symR z) Rxy. Qed. End PER. -(* We define the equivalence property with prenex quantification so that it *) -(* can be localized using the {in ..., ..} form defined below. *) +(** + We define the equivalence property with prenex quantification so that it + can be localized using the {in ..., ..} form defined below. **) Definition equivalence_rel := forall x y z, R z z * (R x y -> R x z = R y z). @@ -1512,7 +1531,7 @@ End RelationProperties. Lemma rev_trans T (R : rel T) : transitive R -> transitive (fun x y => R y x). Proof. by move=> trR x y z Ryx Rzy; apply: trR Rzy Ryx. Qed. -(* Property localization *) +(** Property localization **) Local Notation "{ 'all1' P }" := (forall x, P x : Prop) (at level 0). Local Notation "{ 'all2' P }" := (forall x y, P x y : Prop) (at level 0). @@ -1626,11 +1645,12 @@ Notation "{ 'on' cd , 'bijective' f }" := (bijective_on (mem cd) f) (at level 0, f at level 8, format "{ 'on' cd , 'bijective' f }") : type_scope. -(* Weakening and monotonicity lemmas for localized predicates. *) -(* Note that using these lemmas in backward reasoning will force expansion of *) -(* the predicate definition, as Coq needs to expose the quantifier to apply *) -(* these lemmas. We define a few specialized variants to avoid this for some *) -(* of the ssrfun predicates. *) +(** + Weakening and monotonicity lemmas for localized predicates. + Note that using these lemmas in backward reasoning will force expansion of + the predicate definition, as Coq needs to expose the quantifier to apply + these lemmas. We define a few specialized variants to avoid this for some + of the ssrfun predicates. **) Section LocalGlobal. diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml index 82cae439..c94039a6 100644 --- a/plugins/ssr/ssrcommon.ml +++ b/plugins/ssr/ssrcommon.ml @@ -181,10 +181,9 @@ let option_assert_get o msg = (** Constructors for rawconstr *) open Glob_term open Globnames -open Misctypes open Decl_kinds -let mkRHole = DAst.make @@ GHole (Evar_kinds.InternalHole, IntroAnonymous, None) +let mkRHole = DAst.make @@ GHole (Evar_kinds.InternalHole, Namegen.IntroAnonymous, None) let rec mkRHoles n = if n > 0 then mkRHole :: mkRHoles (n - 1) else [] let rec isRHoles cl = match cl with @@ -254,7 +253,7 @@ let interp_refine ist gl rc = let interp_open_constr ist gl gc = - let (sigma, (c, _)) = Tacinterp.interp_open_constr_with_bindings ist (pf_env gl) (project gl) (gc, Misctypes.NoBindings) in + let (sigma, (c, _)) = Tacinterp.interp_open_constr_with_bindings ist (pf_env gl) (project gl) (gc, Tactypes.NoBindings) in (project gl, (sigma, c)) let interp_term ist gl (_, c) = snd (interp_open_constr ist gl c) @@ -423,12 +422,12 @@ let mk_anon_id t gl_ids = (set s i (Char.chr (Char.code (get s i) + 1)); s) in Id.of_bytes (loop (n - 1)) -let convert_concl_no_check t = Tactics.convert_concl_no_check t Term.DEFAULTcast -let convert_concl t = Tactics.convert_concl t Term.DEFAULTcast +let convert_concl_no_check t = Tactics.convert_concl_no_check t DEFAULTcast +let convert_concl t = Tactics.convert_concl t DEFAULTcast let rename_hd_prod orig_name_ref gl = match EConstr.kind (project gl) (pf_concl gl) with - | Term.Prod(_,src,tgt) -> + | Prod(_,src,tgt) -> Proofview.V82.of_tactic (convert_concl_no_check (EConstr.mkProd (!orig_name_ref,src,tgt))) gl | _ -> CErrors.anomaly (str "gentac creates no product") @@ -504,16 +503,17 @@ let nf_evar sigma t = EConstr.Unsafe.to_constr (Evarutil.nf_evar sigma (EConstr.of_constr t)) let pf_abs_evars2 gl rigid (sigma, c0) = - let c0 = EConstr.to_constr sigma c0 in + let c0 = EConstr.to_constr ~abort_on_undefined_evars:false sigma c0 in let sigma0, ucst = project gl, Evd.evar_universe_context sigma in let nenv = env_size (pf_env gl) in let abs_evar n k = let evi = Evd.find sigma k in - let dc = CList.firstn n (evar_filtered_context evi) in + let concl = EConstr.Unsafe.to_constr evi.evar_concl in + let dc = EConstr.Unsafe.to_named_context (CList.firstn n (evar_filtered_context evi)) in let abs_dc c = function | NamedDecl.LocalDef (x,b,t) -> mkNamedLetIn x b t (mkArrow t c) | NamedDecl.LocalAssum (x,t) -> mkNamedProd x t c in - let t = Context.Named.fold_inside abs_dc ~init:evi.evar_concl dc in + let t = Context.Named.fold_inside abs_dc ~init:concl dc in nf_evar sigma t in let rec put evlist c = match Constr.kind c with | Evar (k, a) -> @@ -569,11 +569,12 @@ let pf_abs_evars_pirrel gl (sigma, c0) = let nenv = env_size (pf_env gl) in let abs_evar n k = let evi = Evd.find sigma k in - let dc = CList.firstn n (evar_filtered_context evi) in + let concl = EConstr.Unsafe.to_constr evi.evar_concl in + let dc = EConstr.Unsafe.to_named_context (CList.firstn n (evar_filtered_context evi)) in let abs_dc c = function | NamedDecl.LocalDef (x,b,t) -> mkNamedLetIn x b t (mkArrow t c) | NamedDecl.LocalAssum (x,t) -> mkNamedProd x t c in - let t = Context.Named.fold_inside abs_dc ~init:evi.evar_concl dc in + let t = Context.Named.fold_inside abs_dc ~init:concl dc in nf_evar sigma0 (nf_evar sigma t) in let rec put evlist c = match Constr.kind c with | Evar (k, a) -> @@ -581,7 +582,7 @@ let pf_abs_evars_pirrel gl (sigma, c0) = let n = max 0 (Array.length a - nenv) in let k_ty = Retyping.get_sort_family_of - (pf_env gl) sigma (EConstr.of_constr (Evd.evar_concl (Evd.find sigma k))) in + (pf_env gl) sigma (Evd.evar_concl (Evd.find sigma k)) in let is_prop = k_ty = InProp in let t = abs_evar n k in (k, (n, t, is_prop)) :: put evlist t | _ -> Constr.fold put evlist c in @@ -746,7 +747,7 @@ let pf_mkSsrConst name gl = let pf_fresh_global name gl = let sigma, env, it = project gl, pf_env gl, sig_it gl in let sigma,t = Evd.fresh_global env sigma name in - t, re_sig it sigma + EConstr.Unsafe.to_constr t, re_sig it sigma let mkProt t c gl = let prot, gl = pf_mkSsrConst "protect_term" gl in @@ -802,7 +803,7 @@ let rec is_name_in_ipats name = function | IPatId id :: tl -> id = name || is_name_in_ipats name tl | IPatAbstractVars ids :: tl -> CList.mem_f Id.equal name ids || is_name_in_ipats name tl - | (IPatCase l | IPatDispatch l | IPatInj l) :: tl -> + | (IPatCase l | IPatDispatch (_,l) | IPatInj l) :: tl -> List.exists (is_name_in_ipats name) l || is_name_in_ipats name tl | (IPatView _ | IPatAnon _ | IPatSimpl _ | IPatRewrite _ | IPatTac _ | IPatNoop) :: tl -> is_name_in_ipats name tl | [] -> false @@ -857,10 +858,10 @@ open Util (** Constructors for constr_expr *) let mkCProp loc = CAst.make ?loc @@ CSort GProp let mkCType loc = CAst.make ?loc @@ CSort (GType []) -let mkCVar ?loc id = CAst.make ?loc @@ CRef (CAst.make ?loc @@ Ident id, None) +let mkCVar ?loc id = CAst.make ?loc @@ CRef (qualid_of_ident ?loc id, None) let rec mkCHoles ?loc n = - if n <= 0 then [] else (CAst.make ?loc @@ CHole (None, IntroAnonymous, None)) :: mkCHoles ?loc (n - 1) -let mkCHole loc = CAst.make ?loc @@ CHole (None, IntroAnonymous, None) + if n <= 0 then [] else (CAst.make ?loc @@ CHole (None, Namegen.IntroAnonymous, None)) :: mkCHoles ?loc (n - 1) +let mkCHole loc = CAst.make ?loc @@ CHole (None, Namegen.IntroAnonymous, None) let mkCLambda ?loc name ty t = CAst.make ?loc @@ CLambdaN ([CLocalAssum([CAst.make ?loc name], Default Explicit, ty)], t) let mkCArrow ?loc ty t = CAst.make ?loc @@ @@ -983,7 +984,7 @@ let applyn ~with_evars ?beta ?(with_shelve=false) n t gl = if not (EConstr.Vars.closed0 sigma ty) then raise dependent_apply_error; let m = Evarutil.new_meta () in - loop (meta_declare m (EConstr.Unsafe.to_constr ty) sigma) bo ((EConstr.mkMeta m)::args) (n-1) + loop (meta_declare m ty sigma) bo ((EConstr.mkMeta m)::args) (n-1) | _ -> assert false in loop sigma t [] n in pp(lazy(str"Refiner.refiner " ++ Printer.pr_econstr_env (pf_env gl) (project gl) t)); @@ -1219,7 +1220,7 @@ let genclrtac cl cs clr = (fun type_err gl -> tclTHEN (tclTHEN (Proofview.V82.of_tactic (Tactics.elim_type (EConstr.of_constr - (Universes.constr_of_global @@ Coqlib.build_coq_False ())))) (old_cleartac clr)) + (UnivGen.constr_of_global @@ Coqlib.build_coq_False ())))) (old_cleartac clr)) (fun gl -> raise type_err) gl)) (old_cleartac clr) @@ -1444,7 +1445,7 @@ let tclINTRO_ANON = tclINTRO ~id:None ~conclusion:return let tclRENAME_HD_PROD name = Goal.enter begin fun gl -> let convert_concl_no_check t = - Tactics.convert_concl_no_check t Term.DEFAULTcast in + Tactics.convert_concl_no_check t DEFAULTcast in let concl = Goal.concl gl in let sigma = Goal.sigma gl in match EConstr.kind sigma concl with @@ -1503,7 +1504,7 @@ let tclOPTION o d = let tacIS_INJECTION_CASE ?ty t = begin tclOPTION ty (tacTYPEOF t) >>= fun ty -> tacREDUCE_TO_QUANTIFIED_IND ty >>= fun ((mind,_),_) -> - tclUNIT (Globnames.eq_gr (Globnames.IndRef mind) (Coqlib.build_coq_eq ())) + tclUNIT (GlobRef.equal (GlobRef.IndRef mind) (Coqlib.build_coq_eq ())) end let tclWITHTOP tac = Goal.enter begin fun gl -> diff --git a/plugins/ssr/ssrcommon.mli b/plugins/ssr/ssrcommon.mli index 2b8f1d54..9ba23467 100644 --- a/plugins/ssr/ssrcommon.mli +++ b/plugins/ssr/ssrcommon.mli @@ -212,7 +212,7 @@ val pf_abs_prod : EConstr.t -> Goal.goal Evd.sigma * EConstr.types val mkSsrRRef : string -> Glob_term.glob_constr * 'a option -val mkSsrRef : string -> Globnames.global_reference +val mkSsrRef : string -> GlobRef.t val mkSsrConst : string -> env -> evar_map -> evar_map * EConstr.t @@ -224,7 +224,7 @@ val new_wild_id : tac_ctx -> Names.Id.t * tac_ctx val pf_fresh_global : - Globnames.global_reference -> + GlobRef.t -> Goal.goal Evd.sigma -> Constr.constr * Goal.goal Evd.sigma diff --git a/plugins/ssr/ssreflect.v b/plugins/ssr/ssreflect.v index b0a94413..bebbd4ad 100644 --- a/plugins/ssr/ssreflect.v +++ b/plugins/ssr/ssreflect.v @@ -10,50 +10,53 @@ (* This file is (C) Copyright 2006-2015 Microsoft Corporation and Inria. *) +(** #<style> .doc { font-family: monospace; white-space: pre; } </style># **) + Require Import Bool. (* For bool_scope delimiter 'bool'. *) Require Import ssrmatching. Declare ML Module "ssreflect_plugin". -(******************************************************************************) -(* 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. *) -(* 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. *) -(******************************************************************************) + +(** + 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. + 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. **) + Set Implicit Arguments. @@ -62,15 +65,16 @@ Unset Printing Implicit Defensive. Module SsrSyntax. -(* 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. *) +(** + 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. **) Reserved Notation "(* x 'is' y 'of' z 'isn't' // /= //= *)" (at level 8). Reserved Notation "(* 69 *)" (at level 69). -(* Non ambiguous keyword to check if the SsrSyntax module is imported *) +(** Non ambiguous keyword to check if the SsrSyntax module is imported **) Reserved Notation "(* Use to test if 'SsrSyntax_is_Imported' *)" (at level 8). Reserved Notation "<hidden n >" (at level 200). @@ -81,10 +85,11 @@ End SsrSyntax. Export SsrMatchingSyntax. Export SsrSyntax. -(* 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 spurrious trailing %GEN_IF. *) +(** + 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 spurrious trailing %%GEN_IF. **) Delimit Scope general_if_scope with GEN_IF. @@ -101,7 +106,7 @@ Notation "'if' c 'as' x 'return' t 'then' v1 'else' v2" := (at level 200, c, t, v1, v2 at level 200, x ident, only parsing) : general_if_scope. -(* Force boolean interpretation of simple if expressions. *) +(** Force boolean interpretation of simple if expressions. **) Delimit Scope boolean_if_scope with BOOL_IF. @@ -116,37 +121,40 @@ Notation "'if' c 'as' x 'return' t 'then' v1 'else' v2" := Open Scope boolean_if_scope. -(* 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. *) +(** + 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. **) Delimit Scope form_scope with FORM. Open Scope form_scope. -(* 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 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. **) Notation "x : T" := (x : T) (at level 100, right associativity, format "'[hv' x '/ ' : T ']'") : core_scope. -(* 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 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". **) Notation "T : 'Type'" := (T%type : Type) (at level 100, only parsing) : core_scope. -(* Allow similarly Prop annotation for, e.g., rewrite multirules. *) +(** Allow similarly Prop annotation for, e.g., rewrite multirules. **) Notation "P : 'Prop'" := (P%type : Prop) (at level 100, only parsing) : core_scope. -(* Constants for abstract: and [: name ] intro pattern *) +(** Constants for abstract: and #[#: name #]# intro pattern **) Definition abstract_lock := unit. Definition abstract_key := tt. @@ -156,35 +164,36 @@ Definition abstract (statement : Type) (id : nat) (lock : abstract_lock) := Notation "<hidden n >" := (abstract _ n _). Notation "T (* n *)" := (abstract T n abstract_key). -(* Constants for tactic-views *) +(** Constants for tactic-views **) Inductive external_view : Type := tactic_view of Type. -(* 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. *) +(** + 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. **) Module TheCanonical. -CoInductive put vT sT (v1 v2 : vT) (s : sT) := Put. +Variant put vT sT (v1 v2 : vT) (s : sT) := Put. Definition get vT sT v s (p : @put vT sT v v s) := let: Put _ _ _ := p in s. @@ -203,11 +212,12 @@ Notation "[ 'the' sT 'of' v 'by' f ]" := Notation "[ 'the' sT 'of' v ]" := (get ((fun s : sT => Put v (*coerce*)s s) _)) (at level 0, only parsing) : form_scope. -(* The following are "format only" versions of the above notations. Since Coq *) -(* doesn't provide this facility, we fake it by splitting the "the" keyword. *) -(* 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. *) +(** + The following are "format only" versions of the above notations. Since Coq + doesn't provide this facility, we fake it by splitting the "the" keyword. + 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. **) Notation "[ 'th' 'e' sT 'of' v 'by' f ]" := (@get_by _ sT f v _ _) (at level 0, format "[ 'th' 'e' sT 'of' v 'by' f ]") : form_scope. @@ -215,37 +225,39 @@ Notation "[ 'th' 'e' sT 'of' v 'by' f ]" := (@get_by _ sT f v _ _) Notation "[ 'th' 'e' sT 'of' v ]" := (@get _ sT v _ _) (at level 0, format "[ 'th' 'e' sT 'of' v ]") : form_scope. -(* We would like to recognize -Notation "[ 'th' 'e' sT 'of' v : 'Type' ]" := (@get Type sT v _ _) - (at level 0, format "[ 'th' 'e' 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. *) +(** + We would like to recognize +Notation " #[# 'th' 'e' sT 'of' v : 'Type' #]#" := (@get Type sT v _ _) + (at level 0, format " #[# 'th' 'e' 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. **) Definition argumentType T P & forall x : T, P x := T. Definition dependentReturnType T P & forall x : T, P x := P. @@ -254,79 +266,82 @@ Definition returnType aT rT & aT -> rT := rT. Notation "{ 'type' 'of' c 'for' s }" := (dependentReturnType c s) (at level 0, format "{ 'type' 'of' c 'for' s }") : type_scope. -(* 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. *) - -CoInductive phantom T (p : T) := Phantom. +(** + 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. **) + +Variant phantom T (p : T) := Phantom. Arguments phantom : clear implicits. Arguments Phantom : clear implicits. -CoInductive phant (p : Type) := Phant. +Variant phant (p : Type) := Phant. -(* Internal tagging used by the implementation of the ssreflect elim. *) +(** Internal tagging used by the implementation of the ssreflect elim. **) Definition protect_term (A : Type) (x : A) : A := x. -(* The ssreflect idiom for a non-keyed pattern: *) -(* - unkeyed t wiil 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, repectively, 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). *) +(** + The ssreflect idiom for a non-keyed pattern: + - unkeyed t wiil 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, repectively, 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). **) Notation unkeyed x := (let flex := x in flex). -(* Ssreflect converse rewrite rule rule idiom. *) +(** Ssreflect converse rewrite rule rule idiom. **) Definition ssr_converse R (r : R) := (Logic.I, r). Notation "=^~ r" := (ssr_converse r) (at level 100) : form_scope. -(* 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 conpares 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. *) +(** + 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 conpares 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. **) Notation nosimpl t := (let: tt := tt in t). @@ -335,11 +350,11 @@ Definition locked A := let: tt := master_key in fun x : A => x. Lemma lock A x : x = locked x :> A. Proof. unlock; reflexivity. Qed. -(* Needed for locked predicates, in particular for eqType's. *) +(** Needed for locked predicates, in particular for eqType's. **) Lemma not_locked_false_eq_true : locked false <> true. Proof. unlock; discriminate. Qed. -(* The basic closing tactic "done". *) +(** The basic closing tactic "done". **) Ltac done := trivial; hnf; intros; solve [ do ![solve [trivial | apply: sym_equal; trivial] @@ -347,7 +362,7 @@ Ltac done := | case not_locked_false_eq_true; assumption | match goal with H : ~ _ |- _ => solve [case H; trivial] end ]. -(* Quicker done tactic not including split, syntax: /0/ *) +(** Quicker done tactic not including split, syntax: /0/ **) Ltac ssrdone0 := trivial; hnf; intros; solve [ do ![solve [trivial | apply: sym_equal; trivial] @@ -355,7 +370,7 @@ Ltac ssrdone0 := | case not_locked_false_eq_true; assumption | match goal with H : ~ _ |- _ => solve [case H; trivial] end ]. -(* To unlock opaque constants. *) +(** To unlock opaque constants. **) Structure unlockable T v := Unlockable {unlocked : T; _ : unlocked = v}. Lemma unlock T x C : @unlocked T x C = x. Proof. by case: C. Qed. @@ -365,25 +380,26 @@ Notation "[ 'unlockable' 'of' C ]" := (@Unlockable _ _ C (unlock _)) Notation "[ 'unlockable' 'fun' C ]" := (@Unlockable _ (fun _ => _) C (unlock _)) (at level 0, format "[ 'unlockable' 'fun' C ]") : form_scope. -(* Generic keyed constant locking. *) +(** Generic keyed constant locking. **) -(* The argument order ensures that k is always compared before T. *) +(** The argument order ensures that k is always compared before T. **) Definition locked_with k := let: tt := k in fun T x => x : T. -(* This can be used as a cheap alternative to cloning the unlockable instance *) -(* below, but with caution as unkeyed matching can be expensive. *) +(** + This can be used as a cheap alternative to cloning the unlockable instance + below, but with caution as unkeyed matching can be expensive. **) Lemma locked_withE T k x : unkeyed (locked_with k x) = x :> T. Proof. by case: k. Qed. -(* Intensionaly, this instance will not apply to locked u. *) +(** Intensionaly, this instance will not apply to locked u. **) Canonical locked_with_unlockable T k x := @Unlockable T x (locked_with k x) (locked_withE k x). -(* More accurate variant of unlock, and safer alternative to locked_withE. *) +(** More accurate variant of unlock, and safer alternative to locked_withE. **) Lemma unlock_with T k x : unlocked (locked_with_unlockable k x) = x :> T. Proof. exact: unlock. Qed. -(* The internal lemmas for the have tactics. *) +(** The internal lemmas for the have tactics. **) Definition ssr_have Plemma Pgoal (step : Plemma) rest : Pgoal := rest step. Arguments ssr_have Plemma [Pgoal]. @@ -398,7 +414,7 @@ Arguments ssr_suff Plemma [Pgoal]. Definition ssr_wlog := ssr_suff. Arguments ssr_wlog Plemma [Pgoal]. -(* Internal N-ary congruence lemmas for the congr tactic. *) +(** Internal N-ary congruence lemmas for the congr tactic. **) Fixpoint nary_congruence_statement (n : nat) : (forall B, (B -> B -> Prop) -> Prop) -> Prop := @@ -422,7 +438,7 @@ Lemma ssr_congr_arrow Plemma Pgoal : Plemma = Pgoal -> Plemma -> Pgoal. Proof. by move->. Qed. Arguments ssr_congr_arrow : clear implicits. -(* View lemmas that don't use reflection. *) +(** View lemmas that don't use reflection. **) Section ApplyIff. @@ -440,14 +456,15 @@ End ApplyIff. Hint View for move/ iffLRn|2 iffRLn|2 iffLR|2 iffRL|2. Hint View for apply/ iffRLn|2 iffLRn|2 iffRL|2 iffLR|2. -(* 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 occuring in the context, hence *) -(* set here := pattern; vm_compute in (value of here) *) -(* blows up at Qed time. *) +(** + 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 occuring in the context, hence + set here := pattern; vm_compute in (value of here) + blows up at Qed time. **) Lemma abstract_context T (P : T -> Type) x : (forall Q, Q = P -> Q x) -> P x. Proof. by move=> /(_ P); apply. Qed. diff --git a/plugins/ssr/ssrelim.ml b/plugins/ssr/ssrelim.ml index 40af5187..602fcfca 100644 --- a/plugins/ssr/ssrelim.ml +++ b/plugins/ssr/ssrelim.ml @@ -14,9 +14,10 @@ open Util open Names open Printer open Term +open Constr open Termops open Globnames -open Misctypes +open Tactypes open Tacmach open Ssrmatching_plugin @@ -358,7 +359,7 @@ let ssrelim ?(ind=ref None) ?(is_case=false) deps what ?elim eqid elim_intro_tac let ev = List.fold_left Evar.Set.union Evar.Set.empty patterns_ev in let ty_ev = Evar.Set.fold (fun i e -> let ex = i in - let i_ty = EConstr.of_constr (Evd.evar_concl (Evd.find (project gl) ex)) in + let i_ty = Evd.evar_concl (Evd.find (project gl) ex) in Evar.Set.union e (evars_of_term i_ty)) ev Evar.Set.empty in let inter = Evar.Set.inter ev ty_ev in @@ -420,7 +421,7 @@ let injectl2rtac sigma c = match EConstr.kind sigma c with let is_injection_case c gl = let gl, cty = pfe_type_of gl c in let (mind,_), _ = pf_reduce_to_quantified_ind gl cty in - eq_gr (IndRef mind) (Coqlib.build_coq_eq ()) + GlobRef.equal (IndRef mind) (Coqlib.build_coq_eq ()) let perform_injection c gl = let gl, cty = pfe_type_of gl c in diff --git a/plugins/ssr/ssrequality.ml b/plugins/ssr/ssrequality.ml index c29203de..f23433f2 100644 --- a/plugins/ssr/ssrequality.ml +++ b/plugins/ssr/ssrequality.ml @@ -277,7 +277,7 @@ let unfoldintac occ rdx t (kt,_) gl = let foldtac occ rdx ft gl = let sigma0, concl0, env0 = project gl, pf_concl gl, pf_env gl in let sigma, t = ft in - let t = EConstr.to_constr sigma t in + let t = EConstr.to_constr ~abort_on_undefined_evars:false sigma t in let fold, conclude = match rdx with | Some (_, (In_T _ | In_X_In_T _)) | None -> let ise = Evd.create_evar_defs sigma in @@ -288,7 +288,10 @@ let foldtac occ rdx ft gl = (fun env c _ h -> try find_T env c h ~k:(fun env t _ _ -> t) with NoMatch ->c), (fun () -> try end_T () with NoMatch -> fake_pmatcher_end ()) | _ -> - (fun env c _ h -> try let sigma = unify_HO env sigma (EConstr.of_constr c) (EConstr.of_constr t) in EConstr.to_constr sigma (EConstr.of_constr t) + (fun env c _ h -> + try + let sigma = unify_HO env sigma (EConstr.of_constr c) (EConstr.of_constr t) in + EConstr.to_constr ~abort_on_undefined_evars:false sigma (EConstr.of_constr t) with _ -> errorstrm Pp.(str "fold pattern " ++ pr_constr_pat t ++ spc () ++ str "does not match redex " ++ pr_constr_pat c)), fake_pmatcher_end in @@ -360,7 +363,7 @@ let pirrel_rewrite pred rdx rdx_ty new_rdx dir (sigma, c) c_ty gl = let evs = Evar.Set.elements (Evarutil.undefined_evars_of_term sigma t) in let open_evs = List.filter (fun k -> Sorts.InProp <> Retyping.get_sort_family_of - env sigma (EConstr.of_constr (Evd.evar_concl (Evd.find sigma k)))) + env sigma (Evd.evar_concl (Evd.find sigma k))) evs in if open_evs <> [] then Some name else None) (List.combine (Array.to_list args) names) @@ -370,8 +373,8 @@ let pirrel_rewrite pred rdx rdx_ty new_rdx dir (sigma, c) c_ty gl = ;; let is_construct_ref sigma c r = - EConstr.isConstruct sigma c && eq_gr (ConstructRef (fst(EConstr.destConstruct sigma c))) r -let is_ind_ref sigma c r = EConstr.isInd sigma c && eq_gr (IndRef (fst(EConstr.destInd sigma c))) r + EConstr.isConstruct sigma c && GlobRef.equal (ConstructRef (fst(EConstr.destConstruct sigma c))) r +let is_ind_ref sigma c r = EConstr.isInd sigma c && GlobRef.equal (IndRef (fst(EConstr.destInd sigma c))) r let rwcltac cl rdx dir sr gl = let n, r_n,_, ucst = pf_abs_evars gl sr in @@ -415,8 +418,6 @@ let rwcltac cl rdx dir sr gl = then errorstrm Pp.(str "Rewriting impacts evars") else errorstrm Pp.(str "Dependent type error in rewrite of " ++ pr_constr_env (pf_env gl) (project gl) (Term.mkNamedLambda pattern_id (EConstr.Unsafe.to_constr rdxt) (EConstr.Unsafe.to_constr cl))) - | CErrors.UserError _ as e -> raise e - | e -> anomaly ("cvtac's exception: " ^ Printexc.to_string e); in tclTHEN cvtac' rwtac gl @@ -436,7 +437,7 @@ let lz_setoid_relation = | env', srel when env' == env -> srel | _ -> let srel = - try Some (Universes.constr_of_global @@ + try Some (UnivGen.constr_of_global @@ Coqlib.coq_reference "Class_setoid" sdir "RewriteRelation") with _ -> None in last_srel := (env, srel); srel @@ -479,11 +480,11 @@ let rwprocess_rule dir rule gl = | _ -> let ra = Array.append a [|r|] in function 1 -> let sigma, pi1 = Evd.fresh_global env sigma coq_prod.Coqlib.proj1 in - EConstr.mkApp (EConstr.of_constr pi1, ra), sigma + EConstr.mkApp (pi1, ra), sigma | _ -> let sigma, pi2 = Evd.fresh_global env sigma coq_prod.Coqlib.proj2 in - EConstr.mkApp (EConstr.of_constr pi2, ra), sigma in - if EConstr.eq_constr sigma a.(0) (EConstr.of_constr (Universes.constr_of_global @@ Coqlib.build_coq_True ())) then + EConstr.mkApp (pi2, ra), sigma in + if EConstr.eq_constr sigma a.(0) (EConstr.of_constr (UnivGen.constr_of_global @@ Coqlib.build_coq_True ())) then let s, sigma = sr sigma 2 in loop (converse_dir d) sigma s a.(1) rs 0 else @@ -558,7 +559,7 @@ let rwrxtac occ rdx_pat dir rule gl = let rpat env sigma0 (sigma, pats) (d, r, lhs, rhs) = let sigma, pat = let rw_progress rhs t evd = rw_progress rhs (EConstr.of_constr t) evd in - mk_tpattern env sigma0 (sigma,EConstr.to_constr sigma r) (rw_progress rhs) d (EConstr.to_constr sigma lhs) in + mk_tpattern env sigma0 (sigma, EConstr.to_constr ~abort_on_undefined_evars:false sigma r) (rw_progress rhs) d (EConstr.to_constr ~abort_on_undefined_evars:false sigma lhs) in sigma, pats @ [pat] in let rpats = List.fold_left (rpat env0 sigma0) (r_sigma,[]) rules in let find_R, end_R = mk_tpattern_matcher sigma0 occ ~upats_origin rpats in @@ -568,7 +569,7 @@ let rwrxtac occ rdx_pat dir rule gl = let r = ref None in (fun env c _ h -> do_once r (fun () -> find_rule (EConstr.of_constr c), c); mkRel h), (fun concl -> closed0_check concl e gl; - let (d,(ev,ctx,c)) , x = assert_done r in (d,(ev,ctx, EConstr.to_constr ev c)) , x) in + let (d,(ev,ctx,c)) , x = assert_done r in (d,(ev,ctx, EConstr.to_constr ~abort_on_undefined_evars:false ev c)) , x) in let concl0 = EConstr.Unsafe.to_constr concl0 in let concl = eval_pattern env0 sigma0 concl0 rdx_pat occ find_R in let (d, r), rdx = conclude concl in @@ -590,7 +591,10 @@ let ssrinstancesofrule ist dir arg gl = let rpat env sigma0 (sigma, pats) (d, r, lhs, rhs) = let sigma, pat = let rw_progress rhs t evd = rw_progress rhs (EConstr.of_constr t) evd in - mk_tpattern env sigma0 (sigma,EConstr.to_constr sigma r) (rw_progress rhs) d (EConstr.to_constr sigma lhs) in + mk_tpattern env sigma0 + (sigma,EConstr.to_constr ~abort_on_undefined_evars:false sigma r) + (rw_progress rhs) d + (EConstr.to_constr ~abort_on_undefined_evars:false sigma lhs) in sigma, pats @ [pat] in let rpats = List.fold_left (rpat env0 sigma0) (r_sigma,[]) rules in mk_tpattern_matcher ~all_instances:true ~raise_NoMatch:true sigma0 None ~upats_origin rpats in diff --git a/plugins/ssr/ssrfun.v b/plugins/ssr/ssrfun.v index ac2c7824..4810c6e1 100644 --- a/plugins/ssr/ssrfun.v +++ b/plugins/ssr/ssrfun.v @@ -10,207 +10,210 @@ (* This file is (C) Copyright 2006-2015 Microsoft Corporation and Inria. *) +(** #<style> .doc { font-family: monospace; white-space: pre; } </style># **) + Require Import ssreflect. -(******************************************************************************) -(* This file contains the basic definitions and notations for working with *) -(* functions. The definitions provide for: *) -(* *) -(* - Pair projections: *) -(* p.1 == first element of a pair *) -(* p.2 == second element of a pair *) -(* These notations also apply to p : P /\ Q, via an and >-> pair coercion. *) -(* *) -(* - Simplifying functions, beta-reduced by /= and simpl: *) -(* [fun : T => E] == constant function from type T that returns E *) -(* [fun x => E] == unary function *) -(* [fun x : T => E] == unary function with explicit domain type *) -(* [fun x y => E] == binary function *) -(* [fun x y : T => E] == binary function with common domain type *) -(* [fun (x : T) y => E] \ *) -(* [fun (x : xT) (y : yT) => E] | == binary function with (some) explicit, *) -(* [fun x (y : T) => E] / independent domain types for each argument *) -(* *) -(* - Partial functions using option type: *) -(* oapp f d ox == if ox is Some x returns f x, d otherwise *) -(* odflt d ox == if ox is Some x returns x, d otherwise *) -(* obind f ox == if ox is Some x returns f x, None otherwise *) -(* omap f ox == if ox is Some x returns Some (f x), None otherwise *) -(* *) -(* - Singleton types: *) -(* all_equal_to x0 == x0 is the only value in its type, so any such value *) -(* can be rewritten to x0. *) -(* *) -(* - A generic wrapper type: *) -(* wrapped T == the inductive type with values Wrap x for x : T. *) -(* unwrap w == the projection of w : wrapped T on T. *) -(* wrap x == the canonical injection of x : T into wrapped T; it is *) -(* equivalent to Wrap x, but is declared as a (default) *) -(* Canonical Structure, which lets the Coq HO unification *) -(* automatically expand x into unwrap (wrap x). The delta *) -(* reduction of wrap x to Wrap can be exploited to *) -(* introduce controlled nondeterminism in Canonical *) -(* Structure inference, as in the implementation of *) -(* the mxdirect predicate in matrix.v. *) -(* *) -(* - Sigma types: *) -(* tag w == the i of w : {i : I & T i}. *) -(* tagged w == the T i component of w : {i : I & T i}. *) -(* Tagged T x == the {i : I & T i} with component x : T i. *) -(* tag2 w == the i of w : {i : I & T i & U i}. *) -(* tagged2 w == the T i component of w : {i : I & T i & U i}. *) -(* tagged2' w == the U i component of w : {i : I & T i & U i}. *) -(* Tagged2 T U x y == the {i : I & T i} with components x : T i and y : U i. *) -(* sval u == the x of u : {x : T | P x}. *) -(* s2val u == the x of u : {x : T | P x & Q x}. *) -(* The properties of sval u, s2val u are given by lemmas svalP, s2valP, and *) -(* s2valP'. We provide coercions sigT2 >-> sigT and sig2 >-> sig >-> sigT. *) -(* A suite of lemmas (all_sig, ...) let us skolemize sig, sig2, sigT, sigT2 *) -(* and pair, e.g., *) -(* have /all_sig[f fP] (x : T): {y : U | P y} by ... *) -(* yields an f : T -> U such that fP : forall x, P (f x). *) -(* - Identity functions: *) -(* id == NOTATION for the explicit identity function fun x => x. *) -(* @id T == notation for the explicit identity at type T. *) -(* idfun == an expression with a head constant, convertible to id; *) -(* idfun x simplifies to x. *) -(* @idfun T == the expression above, specialized to type T. *) -(* phant_id x y == the function type phantom _ x -> phantom _ y. *) -(* *** In addition to their casual use in functional programming, identity *) -(* functions are often used to trigger static unification as part of the *) -(* construction of dependent Records and Structures. For example, if we need *) -(* a structure sT over a type T, we take as arguments T, sT, and a "dummy" *) -(* function T -> sort sT: *) -(* Definition foo T sT & T -> sort sT := ... *) -(* We can avoid specifying sT directly by calling foo (@id T), or specify *) -(* the call completely while still ensuring the consistency of T and sT, by *) -(* calling @foo T sT idfun. The phant_id type allows us to extend this trick *) -(* to non-Type canonical projections. It also allows us to sidestep *) -(* dependent type constraints when building explicit records, e.g., given *) -(* Record r := R {x; y : T(x)}. *) -(* if we need to build an r from a given y0 while inferring some x0, such *) -(* that y0 : T(x0), we pose *) -(* Definition mk_r .. y .. (x := ...) y' & phant_id y y' := R x y'. *) -(* Calling @mk_r .. y0 .. id will cause Coq to use y' := y0, while checking *) -(* the dependent type constraint y0 : T(x0). *) -(* *) -(* - Extensional equality for functions and relations (i.e. functions of two *) -(* arguments): *) -(* f1 =1 f2 == f1 x is equal to f2 x for all x. *) -(* f1 =1 f2 :> A == ... and f2 is explicitly typed. *) -(* f1 =2 f2 == f1 x y is equal to f2 x y for all x y. *) -(* f1 =2 f2 :> A == ... and f2 is explicitly typed. *) -(* *) -(* - Composition for total and partial functions: *) -(* f^~ y == function f with second argument specialised to y, *) -(* i.e., fun x => f x y *) -(* CAVEAT: conditional (non-maximal) implicit arguments *) -(* of f are NOT inserted in this context *) -(* @^~ x == application at x, i.e., fun f => f x *) -(* [eta f] == the explicit eta-expansion of f, i.e., fun x => f x *) -(* CAVEAT: conditional (non-maximal) implicit arguments *) -(* of f are NOT inserted in this context. *) -(* fun=> v := the constant function fun _ => v. *) -(* f1 \o f2 == composition of f1 and f2. *) -(* Note: (f1 \o f2) x simplifies to f1 (f2 x). *) -(* f1 \; f2 == categorical composition of f1 and f2. This expands to *) -(* to f2 \o f1 and (f1 \; f2) x simplifies to f2 (f1 x). *) -(* pcomp f1 f2 == composition of partial functions f1 and f2. *) -(* *) -(* *) -(* - Properties of functions: *) -(* injective f <-> f is injective. *) -(* cancel f g <-> g is a left inverse of f / f is a right inverse of g. *) -(* pcancel f g <-> g is a left inverse of f where g is partial. *) -(* ocancel f g <-> g is a left inverse of f where f is partial. *) -(* bijective f <-> f is bijective (has a left and right inverse). *) -(* involutive f <-> f is involutive. *) -(* *) -(* - Properties for operations. *) -(* left_id e op <-> e is a left identity for op (e op x = x). *) -(* right_id e op <-> e is a right identity for op (x op e = x). *) -(* left_inverse e inv op <-> inv is a left inverse for op wrt identity e, *) -(* i.e., (inv x) op x = e. *) -(* right_inverse e inv op <-> inv is a right inverse for op wrt identity e *) -(* i.e., x op (i x) = e. *) -(* self_inverse e op <-> each x is its own op-inverse (x op x = e). *) -(* idempotent op <-> op is idempotent for op (x op x = x). *) -(* associative op <-> op is associative, i.e., *) -(* x op (y op z) = (x op y) op z. *) -(* commutative op <-> op is commutative (x op y = y op x). *) -(* left_commutative op <-> op is left commutative, i.e., *) -(* x op (y op z) = y op (x op z). *) -(* right_commutative op <-> op is right commutative, i.e., *) -(* (x op y) op z = (x op z) op y. *) -(* left_zero z op <-> z is a left zero for op (z op x = z). *) -(* right_zero z op <-> z is a right zero for op (x op z = z). *) -(* left_distributive op1 op2 <-> op1 distributes over op2 to the left: *) -(* (x op2 y) op1 z = (x op1 z) op2 (y op1 z). *) -(* right_distributive op1 op2 <-> op distributes over add to the right: *) -(* x op1 (y op2 z) = (x op1 z) op2 (x op1 z). *) -(* interchange op1 op2 <-> op1 and op2 satisfy an interchange law: *) -(* (x op2 y) op1 (z op2 t) = (x op1 z) op2 (y op1 t). *) -(* Note that interchange op op is a commutativity property. *) -(* left_injective op <-> op is injective in its left argument: *) -(* x op y = z op y -> x = z. *) -(* right_injective op <-> op is injective in its right argument: *) -(* x op y = x op z -> y = z. *) -(* left_loop inv op <-> op, inv obey the inverse loop left axiom: *) -(* (inv x) op (x op y) = y for all x, y, i.e., *) -(* op (inv x) is always a left inverse of op x *) -(* rev_left_loop inv op <-> op, inv obey the inverse loop reverse left *) -(* axiom: x op ((inv x) op y) = y, for all x, y. *) -(* right_loop inv op <-> op, inv obey the inverse loop right axiom: *) -(* (x op y) op (inv y) = x for all x, y. *) -(* rev_right_loop inv op <-> op, inv obey the inverse loop reverse right *) -(* axiom: (x op y) op (inv y) = x for all x, y. *) -(* Note that familiar "cancellation" identities like x + y - y = x or *) -(* x - y + y = x are respectively instances of right_loop and rev_right_loop *) -(* The corresponding lemmas will use the K and NK/VK suffixes, respectively. *) -(* *) -(* - Morphisms for functions and relations: *) -(* {morph f : x / a >-> r} <-> f is a morphism with respect to functions *) -(* (fun x => a) and (fun x => r); if r == R[x], *) -(* this states that f a = R[f x] for all x. *) -(* {morph f : x / a} <-> f is a morphism with respect to the *) -(* function expression (fun x => a). This is *) -(* shorthand for {morph f : x / a >-> a}; note *) -(* that the two instances of a are often *) -(* interpreted at different types. *) -(* {morph f : x y / a >-> r} <-> f is a morphism with respect to functions *) -(* (fun x y => a) and (fun x y => r). *) -(* {morph f : x y / a} <-> f is a morphism with respect to the *) -(* function expression (fun x y => a). *) -(* {homo f : x / a >-> r} <-> f is a homomorphism with respect to the *) -(* predicates (fun x => a) and (fun x => r); *) -(* if r == R[x], this states that a -> R[f x] *) -(* for all x. *) -(* {homo f : x / a} <-> f is a homomorphism with respect to the *) -(* predicate expression (fun x => a). *) -(* {homo f : x y / a >-> r} <-> f is a homomorphism with respect to the *) -(* relations (fun x y => a) and (fun x y => r). *) -(* {homo f : x y / a} <-> f is a homomorphism with respect to the *) -(* relation expression (fun x y => a). *) -(* {mono f : x / a >-> r} <-> f is monotone with respect to projectors *) -(* (fun x => a) and (fun x => r); if r == R[x], *) -(* this states that R[f x] = a for all x. *) -(* {mono f : x / a} <-> f is monotone with respect to the projector *) -(* expression (fun x => a). *) -(* {mono f : x y / a >-> r} <-> f is monotone with respect to relators *) -(* (fun x y => a) and (fun x y => r). *) -(* {mono f : x y / a} <-> f is monotone with respect to the relator *) -(* expression (fun x y => a). *) -(* *) -(* The file also contains some basic lemmas for the above concepts. *) -(* Lemmas relative to cancellation laws use some abbreviated suffixes: *) -(* K - a cancellation rule like esymK : cancel (@esym T x y) (@esym T y x). *) -(* LR - a lemma moving an operation from the left hand side of a relation to *) -(* the right hand side, like canLR: cancel g f -> x = g y -> f x = y. *) -(* RL - a lemma moving an operation from the right to the left, e.g., canRL. *) -(* Beware that the LR and RL orientations refer to an "apply" (back chaining) *) -(* usage; when using the same lemmas with "have" or "move" (forward chaining) *) -(* the directions will be reversed!. *) -(******************************************************************************) + +(** + This file contains the basic definitions and notations for working with + functions. The definitions provide for: + + - Pair projections: + p.1 == first element of a pair + p.2 == second element of a pair + These notations also apply to p : P /\ Q, via an and >-> pair coercion. + + - Simplifying functions, beta-reduced by /= and simpl: + #[#fun : T => E#]# == constant function from type T that returns E + #[#fun x => E#]# == unary function + #[#fun x : T => E#]# == unary function with explicit domain type + #[#fun x y => E#]# == binary function + #[#fun x y : T => E#]# == binary function with common domain type + #[#fun (x : T) y => E#]# \ + #[#fun (x : xT) (y : yT) => E#]# | == binary function with (some) explicit, + #[#fun x (y : T) => E#]# / independent domain types for each argument + + - Partial functions using option type: + oapp f d ox == if ox is Some x returns f x, d otherwise + odflt d ox == if ox is Some x returns x, d otherwise + obind f ox == if ox is Some x returns f x, None otherwise + omap f ox == if ox is Some x returns Some (f x), None otherwise + + - Singleton types: + all_equal_to x0 == x0 is the only value in its type, so any such value + can be rewritten to x0. + + - A generic wrapper type: + wrapped T == the inductive type with values Wrap x for x : T. + unwrap w == the projection of w : wrapped T on T. + wrap x == the canonical injection of x : T into wrapped T; it is + equivalent to Wrap x, but is declared as a (default) + Canonical Structure, which lets the Coq HO unification + automatically expand x into unwrap (wrap x). The delta + reduction of wrap x to Wrap can be exploited to + introduce controlled nondeterminism in Canonical + Structure inference, as in the implementation of + the mxdirect predicate in matrix.v. + + - Sigma types: + tag w == the i of w : {i : I & T i}. + tagged w == the T i component of w : {i : I & T i}. + Tagged T x == the {i : I & T i} with component x : T i. + tag2 w == the i of w : {i : I & T i & U i}. + tagged2 w == the T i component of w : {i : I & T i & U i}. + tagged2' w == the U i component of w : {i : I & T i & U i}. + Tagged2 T U x y == the {i : I & T i} with components x : T i and y : U i. + sval u == the x of u : {x : T | P x}. + s2val u == the x of u : {x : T | P x & Q x}. + The properties of sval u, s2val u are given by lemmas svalP, s2valP, and + s2valP'. We provide coercions sigT2 >-> sigT and sig2 >-> sig >-> sigT. + A suite of lemmas (all_sig, ...) let us skolemize sig, sig2, sigT, sigT2 + and pair, e.g., + have /all_sig#[#f fP#]# (x : T): {y : U | P y} by ... + yields an f : T -> U such that fP : forall x, P (f x). + - Identity functions: + id == NOTATION for the explicit identity function fun x => x. + @id T == notation for the explicit identity at type T. + idfun == an expression with a head constant, convertible to id; + idfun x simplifies to x. + @idfun T == the expression above, specialized to type T. + phant_id x y == the function type phantom _ x -> phantom _ y. + *** In addition to their casual use in functional programming, identity + functions are often used to trigger static unification as part of the + construction of dependent Records and Structures. For example, if we need + a structure sT over a type T, we take as arguments T, sT, and a "dummy" + function T -> sort sT: + Definition foo T sT & T -> sort sT := ... + We can avoid specifying sT directly by calling foo (@id T), or specify + the call completely while still ensuring the consistency of T and sT, by + calling @foo T sT idfun. The phant_id type allows us to extend this trick + to non-Type canonical projections. It also allows us to sidestep + dependent type constraints when building explicit records, e.g., given + Record r := R {x; y : T(x)}. + if we need to build an r from a given y0 while inferring some x0, such + that y0 : T(x0), we pose + Definition mk_r .. y .. (x := ...) y' & phant_id y y' := R x y'. + Calling @mk_r .. y0 .. id will cause Coq to use y' := y0, while checking + the dependent type constraint y0 : T(x0). + + - Extensional equality for functions and relations (i.e. functions of two + arguments): + f1 =1 f2 == f1 x is equal to f2 x for all x. + f1 =1 f2 :> A == ... and f2 is explicitly typed. + f1 =2 f2 == f1 x y is equal to f2 x y for all x y. + f1 =2 f2 :> A == ... and f2 is explicitly typed. + + - Composition for total and partial functions: + f^~ y == function f with second argument specialised to y, + i.e., fun x => f x y + CAVEAT: conditional (non-maximal) implicit arguments + of f are NOT inserted in this context + @^~ x == application at x, i.e., fun f => f x + #[#eta f#]# == the explicit eta-expansion of f, i.e., fun x => f x + CAVEAT: conditional (non-maximal) implicit arguments + of f are NOT inserted in this context. + fun=> v := the constant function fun _ => v. + f1 \o f2 == composition of f1 and f2. + Note: (f1 \o f2) x simplifies to f1 (f2 x). + f1 \; f2 == categorical composition of f1 and f2. This expands to + to f2 \o f1 and (f1 \; f2) x simplifies to f2 (f1 x). + pcomp f1 f2 == composition of partial functions f1 and f2. + + + - Properties of functions: + injective f <-> f is injective. + cancel f g <-> g is a left inverse of f / f is a right inverse of g. + pcancel f g <-> g is a left inverse of f where g is partial. + ocancel f g <-> g is a left inverse of f where f is partial. + bijective f <-> f is bijective (has a left and right inverse). + involutive f <-> f is involutive. + + - Properties for operations. + left_id e op <-> e is a left identity for op (e op x = x). + right_id e op <-> e is a right identity for op (x op e = x). + left_inverse e inv op <-> inv is a left inverse for op wrt identity e, + i.e., (inv x) op x = e. + right_inverse e inv op <-> inv is a right inverse for op wrt identity e + i.e., x op (i x) = e. + self_inverse e op <-> each x is its own op-inverse (x op x = e). + idempotent op <-> op is idempotent for op (x op x = x). + associative op <-> op is associative, i.e., + x op (y op z) = (x op y) op z. + commutative op <-> op is commutative (x op y = y op x). + left_commutative op <-> op is left commutative, i.e., + x op (y op z) = y op (x op z). + right_commutative op <-> op is right commutative, i.e., + (x op y) op z = (x op z) op y. + left_zero z op <-> z is a left zero for op (z op x = z). + right_zero z op <-> z is a right zero for op (x op z = z). + left_distributive op1 op2 <-> op1 distributes over op2 to the left: + (x op2 y) op1 z = (x op1 z) op2 (y op1 z). + right_distributive op1 op2 <-> op distributes over add to the right: + x op1 (y op2 z) = (x op1 z) op2 (x op1 z). + interchange op1 op2 <-> op1 and op2 satisfy an interchange law: + (x op2 y) op1 (z op2 t) = (x op1 z) op2 (y op1 t). + Note that interchange op op is a commutativity property. + left_injective op <-> op is injective in its left argument: + x op y = z op y -> x = z. + right_injective op <-> op is injective in its right argument: + x op y = x op z -> y = z. + left_loop inv op <-> op, inv obey the inverse loop left axiom: + (inv x) op (x op y) = y for all x, y, i.e., + op (inv x) is always a left inverse of op x + rev_left_loop inv op <-> op, inv obey the inverse loop reverse left + axiom: x op ((inv x) op y) = y, for all x, y. + right_loop inv op <-> op, inv obey the inverse loop right axiom: + (x op y) op (inv y) = x for all x, y. + rev_right_loop inv op <-> op, inv obey the inverse loop reverse right + axiom: (x op y) op (inv y) = x for all x, y. + Note that familiar "cancellation" identities like x + y - y = x or + x - y + y = x are respectively instances of right_loop and rev_right_loop + The corresponding lemmas will use the K and NK/VK suffixes, respectively. + + - Morphisms for functions and relations: + {morph f : x / a >-> r} <-> f is a morphism with respect to functions + (fun x => a) and (fun x => r); if r == R#[#x#]#, + this states that f a = R#[#f x#]# for all x. + {morph f : x / a} <-> f is a morphism with respect to the + function expression (fun x => a). This is + shorthand for {morph f : x / a >-> a}; note + that the two instances of a are often + interpreted at different types. + {morph f : x y / a >-> r} <-> f is a morphism with respect to functions + (fun x y => a) and (fun x y => r). + {morph f : x y / a} <-> f is a morphism with respect to the + function expression (fun x y => a). + {homo f : x / a >-> r} <-> f is a homomorphism with respect to the + predicates (fun x => a) and (fun x => r); + if r == R#[#x#]#, this states that a -> R#[#f x#]# + for all x. + {homo f : x / a} <-> f is a homomorphism with respect to the + predicate expression (fun x => a). + {homo f : x y / a >-> r} <-> f is a homomorphism with respect to the + relations (fun x y => a) and (fun x y => r). + {homo f : x y / a} <-> f is a homomorphism with respect to the + relation expression (fun x y => a). + {mono f : x / a >-> r} <-> f is monotone with respect to projectors + (fun x => a) and (fun x => r); if r == R#[#x#]#, + this states that R#[#f x#]# = a for all x. + {mono f : x / a} <-> f is monotone with respect to the projector + expression (fun x => a). + {mono f : x y / a >-> r} <-> f is monotone with respect to relators + (fun x y => a) and (fun x y => r). + {mono f : x y / a} <-> f is monotone with respect to the relator + expression (fun x y => a). + + The file also contains some basic lemmas for the above concepts. + Lemmas relative to cancellation laws use some abbreviated suffixes: + K - a cancellation rule like esymK : cancel (@esym T x y) (@esym T y x). + LR - a lemma moving an operation from the left hand side of a relation to + the right hand side, like canLR: cancel g f -> x = g y -> f x = y. + RL - a lemma moving an operation from the right to the left, e.g., canRL. + Beware that the LR and RL orientations refer to an "apply" (back chaining) + usage; when using the same lemmas with "have" or "move" (forward chaining) + the directions will be reversed!. **) + Set Implicit Arguments. Unset Strict Implicit. @@ -219,7 +222,7 @@ Unset Printing Implicit Defensive. Delimit Scope fun_scope with FUN. Open Scope fun_scope. -(* Notations for argument transpose *) +(** Notations for argument transpose **) Notation "f ^~ y" := (fun x => f x y) (at level 10, y at level 8, no associativity, format "f ^~ y") : fun_scope. Notation "@^~ x" := (fun f => f x) @@ -228,7 +231,7 @@ Notation "@^~ x" := (fun f => f x) Delimit Scope pair_scope with PAIR. Open Scope pair_scope. -(* Notations for pair/conjunction projections *) +(** Notations for pair/conjunction projections **) Notation "p .1" := (fst p) (at level 2, left associativity, format "p .1") : pair_scope. Notation "p .2" := (snd p) @@ -239,8 +242,9 @@ Coercion pair_of_and P Q (PandQ : P /\ Q) := (proj1 PandQ, proj2 PandQ). Definition all_pair I T U (w : forall i : I, T i * U i) := (fun i => (w i).1, fun i => (w i).2). -(* Complements on the option type constructor, used below to *) -(* encode partial functions. *) +(** + Complements on the option type constructor, used below to + encode partial functions. **) Module Option. @@ -260,7 +264,7 @@ Notation obind := Option.bind. Notation omap := Option.map. Notation some := (@Some _) (only parsing). -(* Shorthand for some basic equality lemmas. *) +(** Shorthand for some basic equality lemmas. **) Notation erefl := refl_equal. Notation ecast i T e x := (let: erefl in _ = i := e return T in x). @@ -269,31 +273,32 @@ Definition nesym := sym_not_eq. Definition etrans := trans_eq. Definition congr1 := f_equal. Definition congr2 := f_equal2. -(* Force at least one implicit when used as a view. *) +(** Force at least one implicit when used as a view. **) Prenex Implicits esym nesym. -(* A predicate for singleton types. *) +(** A predicate for singleton types. **) Definition all_equal_to T (x0 : T) := forall x, unkeyed x = x0. Lemma unitE : all_equal_to tt. Proof. by case. Qed. -(* A generic wrapper type *) +(** A generic wrapper type **) Structure wrapped T := Wrap {unwrap : T}. Canonical wrap T x := @Wrap T x. Prenex Implicits unwrap wrap Wrap. -(* Syntax for defining auxiliary recursive function. *) -(* Usage: *) -(* Section FooDefinition. *) -(* Variables (g1 : T1) (g2 : T2). (globals) *) -(* Fixoint foo_auxiliary (a3 : T3) ... := *) -(* body, using [rec e3, ...] for recursive calls *) -(* where "[ 'rec' a3 , a4 , ... ]" := foo_auxiliary. *) -(* Definition foo x y .. := [rec e1, ...]. *) -(* + proofs about foo *) -(* End FooDefinition. *) +(** + Syntax for defining auxiliary recursive function. + Usage: + Section FooDefinition. + Variables (g1 : T1) (g2 : T2). (globals) + Fixoint foo_auxiliary (a3 : T3) ... := + body, using #[#rec e3, ... #]# for recursive calls + where " #[# 'rec' a3 , a4 , ... #]#" := foo_auxiliary. + Definition foo x y .. := #[#rec e1, ... #]#. + + proofs about foo + End FooDefinition. **) Reserved Notation "[ 'rec' a0 ]" (at level 0, format "[ 'rec' a0 ]"). @@ -319,14 +324,15 @@ Reserved Notation "[ 'rec' a0 , a1 , a2 , a3 , a4 , a5 , a6 , a7 , a8 , a9 ]" (at level 0, format "[ 'rec' a0 , a1 , a2 , a3 , a4 , a5 , a6 , a7 , a8 , a9 ]"). -(* Definitions and notation for explicit functions with simplification, *) -(* i.e., which simpl and /= beta expand (this is complementary to nosimpl). *) +(** + Definitions and notation for explicit functions with simplification, + i.e., which simpl and /= beta expand (this is complementary to nosimpl). **) Section SimplFun. Variables aT rT : Type. -CoInductive simpl_fun := SimplFun of aT -> rT. +Variant simpl_fun := SimplFun of aT -> rT. Definition fun_of_simpl f := fun x => let: SimplFun lam := f in lam x. @@ -362,11 +368,12 @@ Notation "[ 'fun' ( x : xT ) ( y : yT ) => E ]" := (fun x : xT => [fun y : yT => E]) (at level 0, x ident, y ident, only parsing) : fun_scope. -(* For delta functions in eqtype.v. *) +(** For delta functions in eqtype.v. **) Definition SimplFunDelta aT rT (f : aT -> aT -> rT) := [fun z => f z z]. -(* Extensional equality, for unary and binary functions, including syntactic *) -(* sugar. *) +(** + Extensional equality, for unary and binary functions, including syntactic + sugar. **) Section ExtensionalEquality. @@ -439,7 +446,7 @@ Notation "@ 'idfun' T " := (@id_head T explicit_id_key) Definition phant_id T1 T2 v1 v2 := phantom T1 v1 -> phantom T2 v2. -(* Strong sigma types. *) +(** Strong sigma types. **) Section Tag. @@ -473,9 +480,9 @@ Lemma all_tag2 I T U V : {f : forall i, T i & forall i, U i (f i) & forall i, V i (f i)}. Proof. by case/all_tag=> f /all_pair[]; exists f. Qed. -(* Refinement types. *) +(** Refinement types. **) -(* Prenex Implicits and renaming. *) +(** Prenex Implicits and renaming. **) Notation sval := (@proj1_sig _ _). Notation "@ 'sval'" := (@proj1_sig) (at level 10, format "@ 'sval'"). @@ -514,16 +521,16 @@ Section Morphism. Variables (aT rT sT : Type) (f : aT -> rT). -(* Morphism property for unary and binary functions *) +(** Morphism property for unary and binary functions **) Definition morphism_1 aF rF := forall x, f (aF x) = rF (f x). Definition morphism_2 aOp rOp := forall x y, f (aOp x y) = rOp (f x) (f y). -(* Homomorphism property for unary and binary relations *) +(** Homomorphism property for unary and binary relations **) Definition homomorphism_1 (aP rP : _ -> Prop) := forall x, aP x -> rP (f x). Definition homomorphism_2 (aR rR : _ -> _ -> Prop) := forall x y, aR x y -> rR (f x) (f y). -(* Stability property for unary and binary relations *) +(** Stability property for unary and binary relations **) Definition monomorphism_1 (aP rP : _ -> sT) := forall x, rP (f x) = aP x. Definition monomorphism_2 (aR rR : _ -> _ -> sT) := forall x y, rR (f x) (f y) = aR x y. @@ -600,16 +607,18 @@ Notation "{ 'mono' f : x y /~ a }" := (at level 0, f at level 99, x ident, y ident, format "{ 'mono' f : x y /~ a }") : type_scope. -(* In an intuitionistic setting, we have two degrees of injectivity. The *) -(* weaker one gives only simplification, and the strong one provides a left *) -(* inverse (we show in `fintype' that they coincide for finite types). *) -(* We also define an intermediate version where the left inverse is only a *) -(* partial function. *) +(** + In an intuitionistic setting, we have two degrees of injectivity. The + weaker one gives only simplification, and the strong one provides a left + inverse (we show in `fintype' that they coincide for finite types). + We also define an intermediate version where the left inverse is only a + partial function. **) Section Injections. -(* rT must come first so we can use @ to mitigate the Coq 1st order *) -(* unification bug (e..g., Coq can't infer rT from a "cancel" lemma). *) +(** + rT must come first so we can use @ to mitigate the Coq 1st order + unification bug (e..g., Coq can't infer rT from a "cancel" lemma). **) Variables (rT aT : Type) (f : aT -> rT). Definition injective := forall x1 x2, f x1 = f x2 -> x1 = x2. @@ -639,10 +648,10 @@ End Injections. Lemma Some_inj {T} : injective (@Some T). Proof. by move=> x y []. Qed. -(* Force implicits to use as a view. *) +(** Force implicits to use as a view. **) Prenex Implicits Some_inj. -(* cancellation lemmas for dependent type casts. *) +(** cancellation lemmas for dependent type casts. **) Lemma esymK T x y : cancel (@esym T x y) (@esym T y x). Proof. by case: y /. Qed. @@ -684,7 +693,7 @@ Section Bijections. Variables (A B : Type) (f : B -> A). -CoInductive bijective : Prop := Bijective g of cancel f g & cancel g f. +Variant bijective : Prop := Bijective g of cancel f g & cancel g f. Hypothesis bijf : bijective. diff --git a/plugins/ssr/ssrfwd.ml b/plugins/ssr/ssrfwd.ml index a5765feb..e367cd32 100644 --- a/plugins/ssr/ssrfwd.ml +++ b/plugins/ssr/ssrfwd.ml @@ -68,25 +68,18 @@ open Ssripats let ssrhaveNOtcresolution = Summary.ref ~name:"SSR:havenotcresolution" false -let inHaveTCResolution = Libobject.declare_object { - (Libobject.default_object "SSRHAVETCRESOLUTION") with - Libobject.cache_function = (fun (_,v) -> ssrhaveNOtcresolution := v); - Libobject.load_function = (fun _ (_,v) -> ssrhaveNOtcresolution := v); - Libobject.classify_function = (fun v -> Libobject.Keep v); -} let _ = Goptions.declare_bool_option { Goptions.optname = "have type classes"; Goptions.optkey = ["SsrHave";"NoTCResolution"]; Goptions.optread = (fun _ -> !ssrhaveNOtcresolution); Goptions.optdepr = false; - Goptions.optwrite = (fun b -> - Lib.add_anonymous_leaf (inHaveTCResolution b)) } + Goptions.optwrite = (fun b -> ssrhaveNOtcresolution := b); + } open Constrexpr open Glob_term -open Misctypes let combineCG t1 t2 f g = match t1, t2 with | (x, (t1, None)), (_, (t2, None)) -> x, (g t1 t2, None) @@ -184,9 +177,7 @@ let havetac ist let gs = List.map (fun (_,a) -> Ssripats.Internal.pf_find_abstract_proof false gl (EConstr.Unsafe.to_constr a.(1))) skols_args in - let tacopen_skols gl = - let stuff, g = Refiner.unpackage gl in - Refiner.repackage stuff (gs @ [g]) in + let tacopen_skols gl = re_sig (gs @ [gl.Evd.it]) gl.Evd.sigma in let gl, ty = pf_e_type_of gl t in gl, ty, Proofview.V82.of_tactic (Tactics.apply t), id, Tacticals.tclTHEN (Tacticals.tclTHEN itac_c simpltac) diff --git a/plugins/ssr/ssripats.ml b/plugins/ssr/ssripats.ml index 35036b6c..37dd00a7 100644 --- a/plugins/ssr/ssripats.ml +++ b/plugins/ssr/ssripats.ml @@ -12,6 +12,7 @@ open Ssrmatching_plugin open Util open Names +open Constr open Proofview open Proofview.Notations @@ -90,11 +91,11 @@ open State (** Warning: unlike [nb_deps_assums], it does not perform reduction *) let rec nb_assums cur env sigma t = match EConstr.kind sigma t with - | Term.Prod(name,ty,body) -> + | Prod(name,ty,body) -> nb_assums (cur+1) env sigma body - | Term.LetIn(name,ty,t1,t2) -> + | LetIn(name,ty,t1,t2) -> nb_assums (cur+1) env sigma t2 - | Term.Cast(t,_,_) -> + | Cast(t,_,_) -> nb_assums cur env sigma t | _ -> cur let nb_assums = nb_assums 0 @@ -118,13 +119,10 @@ let intro_end = Ssrcommon.tcl0G (isCLR_CONSUME) (** [=> _] *****************************************************************) -let intro_clear ids future_ipats = +let intro_clear ids = Goal.enter begin fun gl -> let _, clear_ids, ren = List.fold_left (fun (used_ids, clear_ids, ren) id -> - if not(Ssrcommon.is_name_in_ipats id future_ipats) then begin - used_ids, id :: clear_ids, ren - end else let new_id = Ssrcommon.mk_anon_id (Id.to_string id) used_ids in (new_id :: used_ids, new_id :: clear_ids, (id, new_id) :: ren)) (Tacmach.New.pf_ids_of_hyps gl, [], []) ids @@ -212,22 +210,25 @@ let tclLOG p t = tclUNIT () end -let rec ipat_tac1 future_ipats ipat : unit tactic = +let rec ipat_tac1 ipat : unit tactic = match ipat with - | IPatView l -> - Ssrview.tclIPAT_VIEWS ~views:l - ~conclusion:(fun ~to_clear:clr -> intro_clear clr future_ipats) - | IPatDispatch ipatss -> - tclEXTEND (List.map (ipat_tac future_ipats) ipatss) (tclUNIT ()) [] + | IPatView (clear_if_id,l) -> + Ssrview.tclIPAT_VIEWS ~views:l ~clear_if_id + ~conclusion:(fun ~to_clear:clr -> intro_clear clr) + + | IPatDispatch(true,[[]]) -> + tclUNIT () + | IPatDispatch(_,ipatss) -> + tclDISPATCH (List.map ipat_tac ipatss) | IPatId id -> Ssrcommon.tclINTRO_ID id | IPatCase ipatss -> - tclIORPAT (Ssrcommon.tclWITHTOP tac_case) future_ipats ipatss + tclIORPAT (Ssrcommon.tclWITHTOP tac_case) ipatss | IPatInj ipatss -> tclIORPAT (Ssrcommon.tclWITHTOP (fun t -> V82.tactic ~nf_evars:false (Ssrelim.perform_injection t))) - future_ipats ipatss + ipatss | IPatAnon Drop -> intro_drop | IPatAnon One -> Ssrcommon.tclINTRO_ANON @@ -238,7 +239,7 @@ let rec ipat_tac1 future_ipats ipat : unit tactic = | IPatClear ids -> tacCHECK_HYPS_EXIST ids <*> - intro_clear (List.map Ssrcommon.hyp_id ids) future_ipats + intro_clear (List.map Ssrcommon.hyp_id ids) | IPatSimpl (Simpl n) -> V82.tactic ~nf_evars:false (Ssrequality.simpltac (Simpl n)) @@ -255,17 +256,17 @@ let rec ipat_tac1 future_ipats ipat : unit tactic = | IPatTac t -> t -and ipat_tac future_ipats pl : unit tactic = +and ipat_tac pl : unit tactic = match pl with | [] -> tclUNIT () | pat :: pl -> - Ssrcommon.tcl0G (tclLOG pat (ipat_tac1 (pl @ future_ipats))) <*> + Ssrcommon.tcl0G (tclLOG pat ipat_tac1) <*> isTICK pat <*> - ipat_tac future_ipats pl + ipat_tac pl -and tclIORPAT tac future_ipats = function +and tclIORPAT tac = function | [[]] -> tac - | p -> Tacticals.New.tclTHENS tac (List.map (ipat_tac future_ipats) p) + | p -> Tacticals.New.tclTHENS tac (List.map ipat_tac p) let split_at_first_case ipats = let rec loop acc = function @@ -276,17 +277,32 @@ let split_at_first_case ipats = loop [] ipats let ssr_exception is_on = function - | Some (IPatCase l) when is_on -> Some (IPatDispatch l) + | Some (IPatCase l) when is_on -> Some (IPatDispatch(true, l)) | x -> x let option_to_list = function None -> [] | Some x -> [x] +(* Simple pass doing {x}/v -> /v{x} *) +let elaborate_ipats l = + let rec elab = function + | [] -> [] + | (IPatClear _ as p1) :: (IPatView _ as p2) :: rest -> p2 :: p1 :: elab rest + | IPatDispatch(s,p) :: rest -> IPatDispatch (s,List.map elab p) :: elab rest + | IPatCase p :: rest -> IPatCase (List.map elab p) :: elab rest + | IPatInj p :: rest -> IPatInj (List.map elab p) :: elab rest + | (IPatTac _ | IPatId _ | IPatSimpl _ | IPatClear _ | + IPatAnon _ | IPatView _ | IPatNoop | IPatRewrite _ | + IPatAbstractVars _) as x :: rest -> x :: elab rest + in + elab l + let main ?eqtac ~first_case_is_dispatch ipats = + let ipats = elaborate_ipats ipats in let ip_before, case, ip_after = split_at_first_case ipats in let case = ssr_exception first_case_is_dispatch case in let case = option_to_list case in let eqtac = option_to_list (Option.map (fun x -> IPatTac x) eqtac) in - Ssrcommon.tcl0G (ipat_tac [] (ip_before @ case @ eqtac @ ip_after) <*> intro_end) + Ssrcommon.tcl0G (ipat_tac (ip_before @ case @ eqtac @ ip_after) <*> intro_end) end (* }}} *) @@ -366,8 +382,9 @@ let elim_intro_tac ipats ?ist what eqid ssrelim is_rec clr = let ctx, last = EConstr.decompose_prod_assum sigma concl in let args = match EConstr.kind_of_type sigma last with | Term.AtomicType (hd, args) -> - assert(Ssrcommon.is_protect hd env sigma); - args + if Ssrcommon.is_protect hd env sigma then args + else Ssrcommon.errorstrm + (Pp.str "Too many names in intro pattern") | _ -> assert false in let case = args.(Array.length args-1) in if not(EConstr.Vars.closed0 sigma case) @@ -419,7 +436,7 @@ let tclLAST_GEN ~to_ind ((oclr, occ), t) conclusion = tclINDEPENDENTL begin Goal.enter_one begin fun g -> let pat = Ssrmatching.interp_cpattern sigma0 t None in let cl0, env, sigma, hyps = Goal.(concl g, env g, sigma g, hyps g) in - let cl = EConstr.to_constr sigma cl0 in + let cl = EConstr.to_constr ~abort_on_undefined_evars:false sigma cl0 in let (c, ucst), cl = try Ssrmatching.fill_occ_pattern ~raise_NoMatch:true env sigma cl pat occ 1 with Ssrmatching.NoMatch -> Ssrmatching.redex_of_pattern env pat, cl in @@ -556,7 +573,7 @@ let rec eqmoveipats eqpat = function let ssrsmovetac = Goal.enter begin fun g -> let sigma, concl = Goal.(sigma g, concl g) in match EConstr.kind sigma concl with - | Term.Prod _ | Term.LetIn _ -> tclUNIT () + | Prod _ | LetIn _ -> tclUNIT () | _ -> Tactics.hnf_in_concl end @@ -575,7 +592,7 @@ let ssrmovetac = function (tacVIEW_THEN_GRAB view ~conclusion) <*> tclIPAT (IPatClear clr :: ipats) | _::_ as view, (_, ({ gens = []; clr }, ipats)) -> - tclIPAT (IPatView view :: IPatClear clr :: ipats) + tclIPAT (IPatView (false,view) :: IPatClear clr :: ipats) | _, (Some pat, (dgens, ipats)) -> let dgentac = with_dgens dgens eqmovetac in dgentac <*> tclIPAT (eqmoveipats pat ipats) @@ -594,8 +611,8 @@ let rec is_Evar_or_CastedMeta sigma x = let occur_existential_or_casted_meta sigma c = let rec occrec c = match EConstr.kind sigma c with - | Term.Evar _ -> raise Not_found - | Term.Cast (m,_,_) when EConstr.isMeta sigma m -> raise Not_found + | Evar _ -> raise Not_found + | Cast (m,_,_) when EConstr.isMeta sigma m -> raise Not_found | _ -> EConstr.iter sigma occrec c in try occrec c; false @@ -624,8 +641,8 @@ let tacFIND_ABSTRACT_PROOF check_lock abstract_n = Goal.enter_one ~__LOC__ begin fun g -> let sigma, env = Goal.(sigma g, env g) in let l = Evd.fold_undefined (fun e ei l -> - match EConstr.kind sigma (EConstr.of_constr ei.Evd.evar_concl) with - | Term.App(hd, [|ty; n; lock|]) + match EConstr.kind sigma ei.Evd.evar_concl with + | App(hd, [|ty; n; lock|]) when (not check_lock || (occur_existential_or_casted_meta sigma ty && is_Evar_or_CastedMeta sigma lock)) && @@ -654,8 +671,8 @@ let ssrabstract dgens = let sigma, env, concl = Goal.(sigma g, env g, concl g) in let t = args_id.(0) in match EConstr.kind sigma t with - | (Term.Evar _ | Term.Meta _) -> Ssrcommon.tacUNIFY concl t <*> tclUNIT id - | Term.Cast(m,_,_) + | (Evar _ | Meta _) -> Ssrcommon.tacUNIFY concl t <*> tclUNIT id + | Cast(m,_,_) when EConstr.isEvar sigma m || EConstr.isMeta sigma m -> Ssrcommon.tacUNIFY concl t <*> tclUNIT id | _ -> diff --git a/plugins/ssr/ssrparser.ml4 b/plugins/ssr/ssrparser.ml4 index 5f396744..eb69dca9 100644 --- a/plugins/ssr/ssrparser.ml4 +++ b/plugins/ssr/ssrparser.ml4 @@ -10,6 +10,7 @@ (* This file is (C) Copyright 2006-2015 Microsoft Corporation and Inria. *) +let _vmcast = Constr.VMcast open Names open Pp open Pcoq @@ -17,18 +18,19 @@ open Ltac_plugin open Genarg open Stdarg open Tacarg -open Term open Libnames open Tactics open Tacmach open Util +open Locus open Tacexpr open Tacinterp open Pltac open Extraargs open Ppconstr -open Misctypes +open Namegen +open Tactypes open Decl_kinds open Constrexpr open Constrexpr_ops @@ -64,7 +66,7 @@ DECLARE PLUGIN "ssreflect_plugin" * we thus save the lexer to restore it at the end of the file *) let frozen_lexer = CLexer.get_keyword_state () ;; -let tacltop = (5,Notation_term.E) +let tacltop = (5,Notation_gram.E) let pr_ssrtacarg _ _ prt = prt tacltop ARGUMENT EXTEND ssrtacarg TYPED AS tactic PRINTED BY pr_ssrtacarg @@ -301,24 +303,24 @@ END let pr_index = function - | Misctypes.ArgVar {CAst.v=id} -> pr_id id - | Misctypes.ArgArg n when n > 0 -> int n + | ArgVar {CAst.v=id} -> pr_id id + | ArgArg n when n > 0 -> int n | _ -> mt () let pr_ssrindex _ _ _ = pr_index -let noindex = Misctypes.ArgArg 0 +let noindex = ArgArg 0 let check_index ?loc i = if i > 0 then i else CErrors.user_err ?loc (str"Index not positive") let mk_index ?loc = function - | Misctypes.ArgArg i -> Misctypes.ArgArg (check_index ?loc i) + | ArgArg i -> ArgArg (check_index ?loc i) | iv -> iv let interp_index ist gl idx = Tacmach.project gl, match idx with - | Misctypes.ArgArg _ -> idx - | Misctypes.ArgVar id -> + | ArgArg _ -> idx + | ArgVar id -> let i = try let v = Id.Map.find id.CAst.v ist.Tacinterp.lfun in @@ -336,7 +338,7 @@ let interp_index ist gl idx = | None -> raise Not_found end end with _ -> CErrors.user_err ?loc:id.CAst.loc (str"Index not a number") in - Misctypes.ArgArg (check_index ?loc:id.CAst.loc i) + ArgArg (check_index ?loc:id.CAst.loc i) open Pltac @@ -410,8 +412,8 @@ let pr_docc = function let pr_ssrdocc _ _ _ = pr_docc ARGUMENT EXTEND ssrdocc TYPED AS ssrclear option * ssrocc PRINTED BY pr_ssrdocc -| [ "{" ne_ssrhyp_list(clr) "}" ] -> [ mkclr clr ] | [ "{" ssrocc(occ) "}" ] -> [ mkocc occ ] +| [ "{" ssrhyp_list(clr) "}" ] -> [ mkclr clr ] END (* Old kinds of terms *) @@ -543,7 +545,7 @@ END let remove_loc x = x.CAst.v -let ipat_of_intro_pattern p = Misctypes.( +let ipat_of_intro_pattern p = Tactypes.( let rec ipat_of_intro_pattern = function | IntroNaming (IntroIdentifier id) -> IPatId id | IntroAction IntroWildcard -> IPatAnon Drop @@ -574,9 +576,9 @@ let rec map_ipat map_id map_ssrhyp map_ast_closure_term = function | IPatAbstractVars l -> IPatAbstractVars (List.map map_id l) | IPatClear clr -> IPatClear (List.map map_ssrhyp clr) | IPatCase iorpat -> IPatCase (List.map (List.map (map_ipat map_id map_ssrhyp map_ast_closure_term)) iorpat) - | IPatDispatch iorpat -> IPatDispatch (List.map (List.map (map_ipat map_id map_ssrhyp map_ast_closure_term)) iorpat) + | IPatDispatch (s,iorpat) -> IPatDispatch (s,List.map (List.map (map_ipat map_id map_ssrhyp map_ast_closure_term)) iorpat) | IPatInj iorpat -> IPatInj (List.map (List.map (map_ipat map_id map_ssrhyp map_ast_closure_term)) iorpat) - | IPatView v -> IPatView (List.map map_ast_closure_term v) + | IPatView (clr,v) -> IPatView (clr,List.map map_ast_closure_term v) | IPatTac _ -> assert false (*internal usage only *) let wit_ssripatrep = add_genarg "ssripatrep" pr_ipat @@ -595,16 +597,15 @@ let intern_ipats ist = List.map (intern_ipat ist) let interp_intro_pattern = interp_wit wit_intro_pattern -let interp_introid ist gl id = Misctypes.( +let interp_introid ist gl id = try IntroNaming (IntroIdentifier (hyp_id (snd (interp_hyp ist gl (SsrHyp (Loc.tag id)))))) with _ -> (snd (interp_intro_pattern ist gl (CAst.make @@ IntroNaming (IntroIdentifier id)))).CAst.v -) let get_intro_id = function | IntroNaming (IntroIdentifier id) -> id | _ -> assert false -let rec add_intro_pattern_hyps ipat hyps = Misctypes.( +let rec add_intro_pattern_hyps ipat hyps = let {CAst.loc=loc;v=ipat} = ipat in match ipat with | IntroNaming (IntroIdentifier id) -> @@ -623,7 +624,6 @@ let rec add_intro_pattern_hyps ipat hyps = Misctypes.( | IntroForthcoming _ -> (* As in ipat_of_intro_pattern, was unable to determine which kind of ipat interp_introid could return [HH] *) assert false -) (* We interp the ipat using the standard ltac machinery for ids, since * we have no clue what a name could be bound to (maybe another ipat) *) @@ -641,12 +641,12 @@ let interp_ipat ist gl = check_hyps_uniq [] clr'; IPatClear clr' | IPatCase(iorpat) -> IPatCase(List.map (List.map interp) iorpat) - | IPatDispatch(iorpat) -> - IPatDispatch(List.map (List.map interp) iorpat) + | IPatDispatch(s,iorpat) -> + IPatDispatch(s,List.map (List.map interp) iorpat) | IPatInj iorpat -> IPatInj (List.map (List.map interp) iorpat) | IPatAbstractVars l -> IPatAbstractVars (List.map get_intro_id (List.map (interp_introid ist gl) l)) - | IPatView l -> IPatView (List.map (fun x -> snd(interp_ast_closure_term ist + | IPatView (clr,l) -> IPatView (clr,List.map (fun x -> snd(interp_ast_closure_term ist gl x)) l) | (IPatSimpl _ | IPatAnon _ | IPatRewrite _ | IPatNoop) as x -> x | IPatTac _ -> assert false (*internal usage only *) @@ -683,11 +683,17 @@ ARGUMENT EXTEND ssripat TYPED AS ssripatrep list PRINTED BY pr_ssripats (* TODO | [ "+" ] -> [ [IPatAnon Temporary] ] *) | [ ssrsimpl_ne(sim) ] -> [ [IPatSimpl sim] ] | [ ssrdocc(occ) "->" ] -> [ match occ with + | Some [], _ -> CErrors.user_err ~loc (str"occ_switch expected") | None, occ -> [IPatRewrite (occ, L2R)] | Some clr, _ -> [IPatClear clr; IPatRewrite (allocc, L2R)]] | [ ssrdocc(occ) "<-" ] -> [ match occ with + | Some [], _ -> CErrors.user_err ~loc (str"occ_switch expected") | None, occ -> [IPatRewrite (occ, R2L)] | Some clr, _ -> [IPatClear clr; IPatRewrite (allocc, R2L)]] + | [ ssrdocc(occ) ssrfwdview(v) ] -> [ match occ with + | Some [], _ -> [IPatView (true,v)] + | Some cl, _ -> check_hyps_uniq [] cl; [IPatClear cl;IPatView (false,v)] + | _ -> CErrors.user_err ~loc (str"Only identifiers are allowed here") ] | [ ssrdocc(occ) ] -> [ match occ with | Some cl, _ -> check_hyps_uniq [] cl; [IPatClear cl] | _ -> CErrors.user_err ~loc (str"Only identifiers are allowed here")] @@ -705,7 +711,7 @@ ARGUMENT EXTEND ssripat TYPED AS ssripatrep list PRINTED BY pr_ssripats | [ "-/" integer(n) "/=" ] -> [ [IPatNoop;IPatSimpl(SimplCut (n,~-1))] ] | [ "-/" integer(n) "/" integer (m) "=" ] -> [ [IPatNoop;IPatSimpl(SimplCut(n,m))] ] - | [ ssrfwdview(v) ] -> [ [IPatView v] ] + | [ ssrfwdview(v) ] -> [ [IPatView (false,v)] ] | [ "[" ":" ident_list(idl) "]" ] -> [ [IPatAbstractVars idl] ] | [ "[:" ident_list(idl) "]" ] -> [ [IPatAbstractVars idl] ] END @@ -956,6 +962,7 @@ END (* the default simpl and unfold tactics would erase blindly. *) open Ssrmatching_plugin.Ssrmatching +open Ssrmatching_plugin.G_ssrmatching let pr_wgen = function | (clr, Some((id,k),None)) -> spc() ++ pr_clear mt clr ++ str k ++ pr_hoi id @@ -1064,7 +1071,7 @@ let rec format_constr_expr h0 c0 = let open CAst in match h0, c0 with | BFdef :: h, { v = CLetIn({CAst.v=x}, v, oty, c) } -> let bs, c' = format_constr_expr h c in Bdef (x, oty, v) :: bs, c' - | [BFcast], { v = CCast (c, CastConv t) } -> + | [BFcast], { v = CCast (c, Glob_term.CastConv t) } -> [Bcast t], c | BFrec (has_str, has_cast) :: h, { v = CFix ( _, [_, (Some locn, CStructRec), bl, t, c]) } -> @@ -1093,7 +1100,7 @@ let wit_ssrfwdfmt = add_genarg "ssrfwdfmt" pr_fwdfmt let mkFwdVal fk c = ((fk, []), c) let mkssrFwdVal fk c = ((fk, []), (c,None)) -let dC t = CastConv t +let dC t = Glob_term.CastConv t let same_ist { interp_env = x } { interp_env = y } = match x,y with @@ -1154,7 +1161,8 @@ ARGUMENT EXTEND ssrbvar TYPED AS constr PRINTED BY pr_ssrbvar END let bvar_lname = let open CAst in function - | { v = CRef ({loc;v=Ident id}, _) } -> CAst.make ?loc @@ Name id + | { v = CRef (qid, _) } when qualid_is_ident qid -> + CAst.make ?loc:qid.CAst.loc @@ Name (qualid_basename qid) | { loc = loc } -> CAst.make ?loc Anonymous let pr_ssrbinder prc _ _ (_, c) = prc c @@ -1210,8 +1218,8 @@ let push_binders c2 bs = | [] -> c | _ -> anomaly "binder not a lambda nor a let in" in match c2 with - | { loc; v = CCast (ct, CastConv cty) } -> - CAst.make ?loc @@ (CCast (loop false ct bs, CastConv (loop true cty bs))) + | { loc; v = CCast (ct, Glob_term.CastConv cty) } -> + CAst.make ?loc @@ (CCast (loop false ct bs, Glob_term.CastConv (loop true cty bs))) | ct -> loop false ct bs let rec fix_binders = let open CAst in function @@ -1246,7 +1254,8 @@ END let pr_ssrfixfwd _ _ _ (id, fwd) = str " fix " ++ pr_id id ++ pr_fwd fwd let bvar_locid = function - | { CAst.v = CRef ({CAst.loc=loc;v=Ident id}, _) } -> CAst.make ?loc id + | { CAst.v = CRef (qid, _) } when qualid_is_ident qid -> + CAst.make ?loc:qid.CAst.loc (qualid_basename qid) | _ -> CErrors.user_err (Pp.str "Missing identifier after \"(co)fix\"") @@ -1399,7 +1408,7 @@ let check_seqtacarg dir arg = match snd arg, dir with CErrors.user_err ?loc (str "expected \"first\"") | _, _ -> arg -let ssrorelse = Gram.entry_create "ssrorelse" +let ssrorelse = Entry.create "ssrorelse" GEXTEND Gram GLOBAL: ssrorelse ssrseqarg; ssrseqidx: [ @@ -1676,7 +1685,10 @@ let pr_gen (docc, dt) = pr_docc docc ++ pr_cpattern dt let pr_ssrgen _ _ _ = pr_gen ARGUMENT EXTEND ssrgen TYPED AS ssrdocc * cpattern PRINTED BY pr_ssrgen -| [ ssrdocc(docc) cpattern(dt) ] -> [ docc, dt ] +| [ ssrdocc(docc) cpattern(dt) ] -> [ + match docc with + | Some [], _ -> CErrors.user_err ~loc (str"Clear flag {} not allowed here") + | _ -> docc, dt ] | [ cpattern(dt) ] -> [ nodocc, dt ] END @@ -1938,7 +1950,7 @@ END let vmexacttac pf = Goal.nf_enter begin fun gl -> - exact_no_check (EConstr.mkCast (pf, VMcast, Tacmach.New.pf_concl gl)) + exact_no_check (EConstr.mkCast (pf, _vmcast, Tacmach.New.pf_concl gl)) end TACTIC EXTEND ssrexact diff --git a/plugins/ssr/ssrparser.mli b/plugins/ssr/ssrparser.mli index 2ac7c7e2..862a9376 100644 --- a/plugins/ssr/ssrparser.mli +++ b/plugins/ssr/ssrparser.mli @@ -12,13 +12,13 @@ open Ltac_plugin -val ssrtacarg : Tacexpr.raw_tactic_expr Pcoq.Gram.entry +val ssrtacarg : Tacexpr.raw_tactic_expr Pcoq.Entry.t val wit_ssrtacarg : (Tacexpr.raw_tactic_expr, Tacexpr.glob_tactic_expr, Geninterp.Val.t) Genarg.genarg_type -val pr_ssrtacarg : 'a -> 'b -> (Notation_term.tolerability -> 'c) -> 'c +val pr_ssrtacarg : 'a -> 'b -> (Notation_gram.tolerability -> 'c) -> 'c -val ssrtclarg : Tacexpr.raw_tactic_expr Pcoq.Gram.entry +val ssrtclarg : Tacexpr.raw_tactic_expr Pcoq.Entry.t val wit_ssrtclarg : (Tacexpr.raw_tactic_expr, Tacexpr.glob_tactic_expr, Geninterp.Val.t) Genarg.genarg_type -val pr_ssrtclarg : 'a -> 'b -> (Notation_term.tolerability -> 'c -> 'd) -> 'c -> 'd +val pr_ssrtclarg : 'a -> 'b -> (Notation_gram.tolerability -> 'c -> 'd) -> 'c -> 'd val add_genarg : string -> ('a -> Pp.t) -> 'a Genarg.uniform_genarg_type diff --git a/plugins/ssr/ssrprinters.ml b/plugins/ssr/ssrprinters.ml index 11369228..824666ba 100644 --- a/plugins/ssr/ssrprinters.ml +++ b/plugins/ssr/ssrprinters.ml @@ -101,13 +101,14 @@ let rec pr_ipat p = | IPatSimpl sim -> pr_simpl sim | IPatClear clr -> pr_clear mt clr | IPatCase iorpat -> hov 1 (str "[" ++ pr_iorpat iorpat ++ str "]") - | IPatDispatch iorpat -> hov 1 (str "/[" ++ pr_iorpat iorpat ++ str "]") + | IPatDispatch(_,iorpat) -> hov 1 (str "/[" ++ pr_iorpat iorpat ++ str "]") | IPatInj iorpat -> hov 1 (str "[=" ++ pr_iorpat iorpat ++ str "]") | IPatRewrite (occ, dir) -> pr_occ occ ++ pr_dir dir | IPatAnon All -> str "*" | IPatAnon Drop -> str "_" | IPatAnon One -> str "?" - | IPatView v -> pr_view2 v + | IPatView (false,v) -> pr_view2 v + | IPatView (true,v) -> str"{}" ++ pr_view2 v | IPatNoop -> str "-" | IPatAbstractVars l -> str "[:" ++ pr_list spc Id.print l ++ str "]" | IPatTac _ -> str "<tac>" diff --git a/plugins/ssr/ssrtacticals.ml b/plugins/ssr/ssrtacticals.ml index 9cc4f5ce..83581f34 100644 --- a/plugins/ssr/ssrtacticals.ml +++ b/plugins/ssr/ssrtacticals.ml @@ -11,9 +11,9 @@ (* This file is (C) Copyright 2006-2015 Microsoft Corporation and Inria. *) open Names +open Constr open Termops open Tacmach -open Misctypes open Locusops open Ssrast @@ -24,7 +24,7 @@ module NamedDecl = Context.Named.Declaration (** Tacticals (+, -, *, done, by, do, =>, first, and last). *) -let get_index = function ArgArg i -> i | _ -> +let get_index = function Locus.ArgArg i -> i | _ -> anomaly "Uninterpreted index" (* Toplevel constr must be globalized twice ! *) @@ -32,9 +32,8 @@ let get_index = function ArgArg i -> i | _ -> let tclPERM perm tac gls = let subgls = tac gls in - let sigma, subgll = Refiner.unpackage subgls in - let subgll' = perm subgll in - Refiner.repackage sigma subgll' + let subgll' = perm subgls.Evd.it in + re_sig subgll' subgls.Evd.sigma let rot_hyps dir i hyps = let n = List.length hyps in @@ -104,10 +103,10 @@ let endclausestac id_map clseq gl_id cl0 gl = | ids, dc' -> forced && ids = [] && (not hide_goal || dc' = [] && c_hidden) in let rec unmark c = match EConstr.kind (project gl) c with - | Term.Var id when hidden_clseq clseq && id = gl_id -> cl0 - | Term.Prod (Name id, t, c') when List.mem_assoc id id_map -> + | Var id when hidden_clseq clseq && id = gl_id -> cl0 + | Prod (Name id, t, c') when List.mem_assoc id id_map -> EConstr.mkProd (Name (orig_id id), unmark t, unmark c') - | Term.LetIn (Name id, v, t, c') when List.mem_assoc id id_map -> + | LetIn (Name id, v, t, c') when List.mem_assoc id id_map -> EConstr.mkLetIn (Name (orig_id id), unmark v, unmark t, unmark c') | _ -> EConstr.map (project gl) unmark c in let utac hyp = diff --git a/plugins/ssr/ssrtacticals.mli b/plugins/ssr/ssrtacticals.mli index a5636ad0..684e0023 100644 --- a/plugins/ssr/ssrtacticals.mli +++ b/plugins/ssr/ssrtacticals.mli @@ -17,7 +17,7 @@ val tclSEQAT : Tacinterp.interp_sign -> Tacinterp.Value.t -> Ssrast.ssrdir -> - int Misctypes.or_var * + int Locus.or_var * (('a * Tacinterp.Value.t option list) * Tacinterp.Value.t option) -> Tacmach.tactic @@ -37,7 +37,7 @@ val hinttac : val ssrdotac : Tacinterp.interp_sign -> - ((int Misctypes.or_var * Ssrast.ssrmmod) * + ((int Locus.or_var * Ssrast.ssrmmod) * (bool * Tacinterp.Value.t option list)) * ((Ssrast.ssrhyps * ((Ssrast.ssrhyp_or_id * string) * diff --git a/plugins/ssr/ssrvernac.ml4 b/plugins/ssr/ssrvernac.ml4 index 05dbf0a8..989a6c5b 100644 --- a/plugins/ssr/ssrvernac.ml4 +++ b/plugins/ssr/ssrvernac.ml4 @@ -19,17 +19,14 @@ open Constrexpr_ops open Pcoq open Pcoq.Prim open Pcoq.Constr -open Pcoq.Vernac_ +open Pvernac.Vernac_ open Ltac_plugin open Notation_ops open Notation_term open Glob_term -open Globnames open Stdarg open Genarg -open Misctypes open Decl_kinds -open Libnames open Pp open Ppconstr open Printer @@ -144,21 +141,21 @@ END let declare_one_prenex_implicit locality f = let fref = try Smartlocate.global_with_alias f - with _ -> errorstrm (pr_reference f ++ str " is not declared") in + with _ -> errorstrm (pr_qualid f ++ str " is not declared") in let rec loop = function | a :: args' when Impargs.is_status_implicit a -> (ExplByName (Impargs.name_of_implicit a), (true, true, true)) :: loop args' | args' when List.exists Impargs.is_status_implicit args' -> - errorstrm (str "Expected prenex implicits for " ++ pr_reference f) + errorstrm (str "Expected prenex implicits for " ++ pr_qualid f) | _ -> [] in let impls = match Impargs.implicits_of_global fref with | [cond,impls] -> impls - | [] -> errorstrm (str "Expected some implicits for " ++ pr_reference f) + | [] -> errorstrm (str "Expected some implicits for " ++ pr_qualid f) | _ -> errorstrm (str "Multiple implicits not supported") in match loop impls with | [] -> - errorstrm (str "Expected some implicits for " ++ pr_reference f) + errorstrm (str "Expected some implicits for " ++ pr_qualid f) | impls -> Impargs.declare_manual_implicits locality fref ~enriching:false [impls] @@ -220,8 +217,8 @@ let interp_search_notation ?loc tag okey = (Bytes.set s' i' '_'; loop (j + 1) (i' + 2)) else (String.blit s i s' i' m; loop (j + 1) (i' + m + 1)) in loop 0 1 in - let trim_ntn (pntn, m) = Bytes.sub_string pntn 1 (max 0 m) in - let pr_ntn ntn = str "(" ++ str ntn ++ str ")" in + let trim_ntn (pntn, m) = (InConstrEntrySomeLevel,Bytes.sub_string pntn 1 (max 0 m)) in + let pr_ntn ntn = str "(" ++ Notation.pr_notation ntn ++ str ")" in let pr_and_list pr = function | [x] -> pr x | x :: lx -> pr_list pr_comma pr lx ++ pr_comma () ++ str "and " ++ pr x @@ -296,7 +293,7 @@ let interp_search_notation ?loc tag okey = let scs' = List.remove (=) sc !scs in let w = pr_ntn ntn ++ str " is also defined " ++ pr_scs scs' in Feedback.msg_warning (hov 4 w) - else if String.string_contains ~where:ntn ~what:" .. " then + else if String.string_contains ~where:(snd ntn) ~what:" .. " then err (pr_ntn ntn ++ str " is an n-ary notation"); let nvars = List.filter (fun (_,(_,typ)) -> typ = NtnTypeConstr) nvars in let rec sub () = function @@ -361,13 +358,12 @@ let coerce_search_pattern_to_sort hpat = true, cp with _ -> false, [] in let coerce hp coe_index = - let coe = Classops.get_coercion_value coe_index in + let coe_ref = coe_index.Classops.coe_value in try - let coe_ref = global_of_constr coe in let n_imps = Option.get (Classops.hide_coercion coe_ref) in mkPApp (Pattern.PRef coe_ref) n_imps [|hp|] - with _ -> - errorstrm (str "need explicit coercion " ++ pr_constr_env env sigma coe ++ spc () + with Not_found | Option.IsNone -> + errorstrm (str "need explicit coercion " ++ pr_global coe_ref ++ spc () ++ str "to interpret head search pattern as type") in filter_head, List.fold_left coerce hpat' coe_path @@ -377,7 +373,10 @@ let interp_head_pat hpat = | Cast (c', _, _) -> loop c' | Prod (_, _, c') -> loop c' | LetIn (_, _, _, c') -> loop c' - | _ -> Constr_matching.is_matching (Global.env()) Evd.empty p (EConstr.of_constr c) in + | _ -> + let env = Global.env () in + let sigma = Evd.from_env env in + Constr_matching.is_matching env sigma p (EConstr.of_constr c) in filter_head, loop let all_true _ = true @@ -413,7 +412,7 @@ let interp_search_arg arg = (* Module path postfilter *) -let pr_modloc (b, m) = if b then str "-" ++ pr_reference m else pr_reference m +let pr_modloc (b, m) = if b then str "-" ++ pr_qualid m else pr_qualid m let wit_ssrmodloc = add_genarg "ssrmodloc" pr_modloc @@ -431,10 +430,9 @@ GEXTEND Gram END let interp_modloc mr = - let interp_mod (_, mr) = - let {CAst.loc=loc; v=qid} = qualid_of_reference mr in + let interp_mod (_, qid) = try Nametab.full_name_module qid with Not_found -> - CErrors.user_err ?loc (str "No Module " ++ pr_qualid qid) in + CErrors.user_err ?loc:qid.CAst.loc (str "No Module " ++ pr_qualid qid) in let mr_out, mr_in = List.partition fst mr in let interp_bmod b = function | [] -> fun _ _ _ -> true diff --git a/plugins/ssr/ssrview.ml b/plugins/ssr/ssrview.ml index aa614fbc..3f974ea0 100644 --- a/plugins/ssr/ssrview.ml +++ b/plugins/ssr/ssrview.ml @@ -67,9 +67,9 @@ end module State : sig (* View storage API *) - val vsINIT : EConstr.t -> unit tactic - val vsPUSH : (EConstr.t -> EConstr.t tactic) -> unit tactic - val vsCONSUME : (Id.t option -> EConstr.t -> unit tactic) -> unit tactic + val vsINIT : EConstr.t * Id.t list -> unit tactic + val vsPUSH : (EConstr.t -> (EConstr.t * Id.t list) tactic) -> unit tactic + val vsCONSUME : (name:Id.t option -> EConstr.t -> to_clear:Id.t list -> unit tactic) -> unit tactic val vsASSERT_EMPTY : unit tactic end = struct (* {{{ *) @@ -78,6 +78,7 @@ type vstate = { subject_name : Id.t option; (* top *) (* None if views are being applied to a term *) view : EConstr.t; (* v2 (v1 top) *) + to_clear : Id.t list; } include Ssrcommon.MakeState(struct @@ -85,13 +86,14 @@ include Ssrcommon.MakeState(struct let init = None end) -let vsINIT view = tclSET (Some { subject_name = None; view }) +let vsINIT (view, to_clear) = + tclSET (Some { subject_name = None; view; to_clear }) let vsPUSH k = tacUPDATE (fun s -> match s with - | Some { subject_name; view } -> - k view >>= fun view -> - tclUNIT (Some { subject_name; view }) + | Some { subject_name; view; to_clear } -> + k view >>= fun (view, clr) -> + tclUNIT (Some { subject_name; view; to_clear = to_clear @ clr }) | None -> Goal.enter_one ~__LOC__ begin fun gl -> let concl = Goal.concl gl in @@ -102,15 +104,15 @@ let vsPUSH k = | _ -> mk_anon_id "view_subject" (Tacmach.New.pf_ids_of_hyps gl) in let view = EConstr.mkVar id in Ssrcommon.tclINTRO_ID id <*> - k view >>= fun view -> - tclUNIT (Some { subject_name = Some id; view }) + k view >>= fun (view, to_clear) -> + tclUNIT (Some { subject_name = Some id; view; to_clear }) end) let vsCONSUME k = tclGET (fun s -> match s with - | Some { subject_name; view } -> + | Some { subject_name; view; to_clear } -> tclSET None <*> - k subject_name view + k ~name:subject_name view ~to_clear | None -> anomaly "vsCONSUME: empty storage") let vsASSERT_EMPTY = @@ -157,7 +159,7 @@ let tclINJ_CONSTR_IST ist p = let mkGHole = DAst.make - (Glob_term.GHole(Evar_kinds.InternalHole, Misctypes.IntroAnonymous, None)) + (Glob_term.GHole(Evar_kinds.InternalHole, Namegen.IntroAnonymous, None)) let rec mkGHoles n = if n > 0 then mkGHole :: mkGHoles (n - 1) else [] let mkGApp f args = if args = [] then f @@ -187,6 +189,16 @@ end * modular, see the 2 functions below that would need to "uncommit" *) let tclKeepOpenConstr (_env, sigma, t) = Unsafe.tclEVARS sigma <*> tclUNIT t +let tclADD_CLEAR_IF_ID (env, ist, t) x = + Ssrprinters.ppdebug (lazy + Pp.(str"tclADD_CLEAR_IF_ID: " ++ Printer.pr_econstr_env env ist t)); + let hd, _ = EConstr.decompose_app ist t in + match EConstr.kind ist hd with + | Constr.Var id when Ssrcommon.not_section_id id -> tclUNIT (x, [id]) + | _ -> tclUNIT (x,[]) + +let tclPAIR p x = tclUNIT (x, p) + (* The ssr heuristic : *) (* Estimate a bound on the number of arguments of a raw constr. *) (* This is not perfect, because the unifier may fail to *) @@ -203,14 +215,15 @@ let guess_max_implicits ist glob = (fun _ -> tclUNIT 5) let pad_to_inductive ist glob = Goal.enter_one ~__LOC__ begin fun goal -> - interp_glob ist glob >>= fun (env, sigma, term) -> + interp_glob ist glob >>= fun (env, sigma, term as ot) -> let term_ty = Retyping.get_type_of env sigma term in let ctx, i = Reductionops.splay_prod env sigma term_ty in let rel_ctx = List.map (fun (a,b) -> Context.Rel.Declaration.LocalAssum(a,b)) ctx in - if Ssrcommon.isAppInd (EConstr.push_rel_context rel_ctx env) sigma i - then tclUNIT (mkGApp glob (mkGHoles (List.length ctx))) - else Tacticals.New.tclZEROMSG Pp.(str"not an inductive") + if not (Ssrcommon.isAppInd (EConstr.push_rel_context rel_ctx env) sigma i) + then Tacticals.New.tclZEROMSG Pp.(str"not an inductive") + else tclUNIT (mkGApp glob (mkGHoles (List.length ctx))) + >>= tclADD_CLEAR_IF_ID ot end (* There are two ways of "applying" a view to term: *) @@ -221,7 +234,7 @@ end (* They require guessing the view hints and the number of *) (* implicits, respectively, which we do by brute force. *) (* Builds v p *) -let interp_view ist v p = +let interp_view ~clear_if_id ist v p = let is_specialize hd = match DAst.get hd with Glob_term.GHole _ -> true | _ -> false in (* We cast the pile of views p into a term p_id *) @@ -230,42 +243,48 @@ let interp_view ist v p = match DAst.get v with | Glob_term.GApp (hd, rargs) when is_specialize hd -> Ssrprinters.ppdebug (lazy Pp.(str "specialize")); - interp_glob ist (mkGApp p_id rargs) >>= tclKeepOpenConstr + interp_glob ist (mkGApp p_id rargs) + >>= tclKeepOpenConstr >>= tclPAIR [] | _ -> Ssrprinters.ppdebug (lazy Pp.(str "view")); (* We find out how to build (v p) eventually using an adaptor *) let adaptors = AdaptorDb.(get Forward) in Proofview.tclORELSE - (pad_to_inductive ist v >>= fun vpad -> + (pad_to_inductive ist v >>= fun (vpad,clr) -> Ssrcommon.tclFIRSTa (List.map - (fun a -> interp_glob ist (mkGApp a [vpad; p_id])) adaptors)) + (fun a -> interp_glob ist (mkGApp a [vpad; p_id])) adaptors) + >>= tclPAIR clr) (fun _ -> guess_max_implicits ist v >>= fun n -> Ssrcommon.tclFIRSTi (fun n -> - interp_glob ist (mkGApp v (mkGHoles n @ [p_id]))) n) - >>= tclKeepOpenConstr + interp_glob ist (mkGApp v (mkGHoles n @ [p_id]))) n + >>= fun x -> tclADD_CLEAR_IF_ID x x) + >>= fun (ot,clr) -> + if clear_if_id + then tclKeepOpenConstr ot >>= tclPAIR clr + else tclKeepOpenConstr ot >>= tclPAIR [] (* we store in the state (v top), then (v1 (v2 top))... *) -let pile_up_view (ist, v) = +let pile_up_view ~clear_if_id (ist, v) = let ist = Ssrcommon.option_assert_get ist (Pp.str"not a term") in - State.vsPUSH (fun p -> interp_view ist v p) + State.vsPUSH (fun p -> interp_view ~clear_if_id ist v p) let finalize_view s0 ?(simple_types=true) p = Goal.enter_one ~__LOC__ begin fun g -> let env = Goal.env g in let sigma = Goal.sigma g in - let evars_of_p = Evd.evars_of_term (EConstr.to_constr sigma p) in + let evars_of_p = Evd.evars_of_term (EConstr.to_constr ~abort_on_undefined_evars:false sigma p) in let filter x _ = Evar.Set.mem x evars_of_p in let sigma = Typeclasses.resolve_typeclasses ~fail:false ~filter env sigma in let p = Reductionops.nf_evar sigma p in let get_body = function Evd.Evar_defined x -> x | _ -> assert false in let evars_of_econstr sigma t = - Evd.evars_of_term (EConstr.to_constr sigma (EConstr.of_constr t)) in + Evarutil.undefined_evars_of_term sigma (EConstr.of_constr t) in let rigid_of s = List.fold_left (fun l k -> if Evd.is_defined sigma k then let bo = get_body Evd.(evar_body (find sigma k)) in - k :: l @ Evar.Set.elements (evars_of_econstr sigma bo) + k :: l @ Evar.Set.elements (evars_of_econstr sigma (EConstr.Unsafe.to_constr bo)) else l ) [] s in let und0 = (* Unassigned evars in the initial goal *) @@ -292,7 +311,7 @@ let pose_proof subject_name p = <*> Tactics.New.reduce_after_refine -let rec apply_all_views ending vs s0 = +let rec apply_all_views ~clear_if_id ending vs s0 = match vs with | [] -> ending s0 | v :: vs -> @@ -301,31 +320,35 @@ let rec apply_all_views ending vs s0 = | `Tac tac -> Ssrprinters.ppdebug (lazy Pp.(str"..a tactic")); ending s0 <*> Tacinterp.eval_tactic tac <*> - Ssrcommon.tacSIGMA >>= apply_all_views ending vs + Ssrcommon.tacSIGMA >>= apply_all_views ~clear_if_id ending vs | `Term v -> Ssrprinters.ppdebug (lazy Pp.(str"..a term")); - pile_up_view v <*> apply_all_views ending vs s0 + pile_up_view ~clear_if_id v <*> + apply_all_views ~clear_if_id ending vs s0 (* Entry points *********************************************************) -let tclIPAT_VIEWS ~views:vs ~conclusion:tac = +let tclIPAT_VIEWS ~views:vs ?(clear_if_id=false) ~conclusion:tac = let end_view_application s0 = - State.vsCONSUME (fun name t -> - finalize_view s0 t >>= pose_proof name <*> - tac ~to_clear:(Option.cata (fun x -> [x]) [] name)) in + State.vsCONSUME (fun ~name t ~to_clear -> + let to_clear = Option.cata (fun x -> [x]) [] name @ to_clear in + finalize_view s0 t >>= pose_proof name <*> tac ~to_clear) in tclINDEPENDENT begin State.vsASSERT_EMPTY <*> - Ssrcommon.tacSIGMA >>= apply_all_views end_view_application vs <*> + Ssrcommon.tacSIGMA >>= + apply_all_views ~clear_if_id end_view_application vs <*> State.vsASSERT_EMPTY end let tclWITH_FWD_VIEWS ~simple_types ~subject ~views:vs ~conclusion:tac = let ending_tac s0 = - State.vsCONSUME (fun _ t -> finalize_view s0 ~simple_types t >>= tac) in + State.vsCONSUME (fun ~name:_ t ~to_clear:_ -> + finalize_view s0 ~simple_types t >>= tac) in tclINDEPENDENT begin State.vsASSERT_EMPTY <*> - State.vsINIT subject <*> - Ssrcommon.tacSIGMA >>= apply_all_views ending_tac vs <*> + State.vsINIT (subject,[]) <*> + Ssrcommon.tacSIGMA >>= + apply_all_views ~clear_if_id:false ending_tac vs <*> State.vsASSERT_EMPTY end diff --git a/plugins/ssr/ssrview.mli b/plugins/ssr/ssrview.mli index be51fe7f..b128a95d 100644 --- a/plugins/ssr/ssrview.mli +++ b/plugins/ssr/ssrview.mli @@ -20,9 +20,11 @@ module AdaptorDb : sig end -(* Apply views to the top of the stack (intro pattern) *) +(* Apply views to the top of the stack (intro pattern). If clear_if_id is + * true (default false) then views that happen to be a variable are considered + * as to be cleared (see the to_clear argument to the continuation) *) val tclIPAT_VIEWS : - views:ast_closure_term list -> + views:ast_closure_term list -> ?clear_if_id:bool -> conclusion:(to_clear:Names.Id.t list -> unit Proofview.tactic) -> unit Proofview.tactic |