diff options
43 files changed, 256 insertions, 200 deletions
@@ -12,6 +12,18 @@ Program - The "Shrink Obligations" flag now applies to all obligations, not only those solved by the automatic tactic. +Changes from V8.5beta3 +====================== + +Specification language + +- Syntax "$(tactic)$" changed to "ltac:(tactic)". + +Tactics + +- Syntax "destruct !hyp" changed to "destruct (hyp)", and similarly + for induction. + Changes from V8.5beta2 to V8.5beta3 =================================== @@ -24,10 +36,6 @@ Vernacular commands introducing it. - New command "Show id" to show goal named id. -Specification language - -- Syntax "$(tactic)$" changed to "ltac: tactic". - Tactics - New flag "Regular Subst Tactic" which fixes "subst" in situations where diff --git a/Makefile.build b/Makefile.build index f74bf1759..a3766a50f 100644 --- a/Makefile.build +++ b/Makefile.build @@ -133,9 +133,9 @@ SYSCMA:=$(addsuffix .cma,$(SYSMOD)) SYSCMXA:=$(addsuffix .cmxa,$(SYSMOD)) ifeq ($(CAMLP4),camlp5) -P4CMA:=gramlib.cma +P4CMA:=gramlib.cma str.cma else -P4CMA:=dynlink.cma camlp4lib.cma +P4CMA:=dynlink.cma camlp4lib.cma str.cma endif @@ -888,7 +888,7 @@ dev/printers.cma: | dev/printers.mllib.d $(HIDE)$(OCAMLC) $(MLINCLUDES) $(BYTEFLAGS) -thread $(SYSCMA) $(P4CMA) $^ -o test-printer @rm -f test-printer $(SHOW)'OCAMLC -a $@' - $(HIDE)$(OCAMLC) $(MLINCLUDES) $(BYTEFLAGS) -thread $(SYSCMA) $^ -linkall -a -o $@ + $(HIDE)$(OCAMLC) $(MLINCLUDES) $(BYTEFLAGS) -thread $(SYSCMA) $(P4CMA) $^ -linkall -a -o $@ grammar/grammar.cma: | grammar/grammar.mllib.d $(SHOW)'Testing $@' @@ -1,5 +1,3 @@ -load_printer "gramlib.cma" -load_printer "str.cma" load_printer "printers.cma" install_printer Top_printers.ppfuture diff --git a/dev/v8-syntax/syntax-v8.tex b/dev/v8-syntax/syntax-v8.tex index 6630be06a..64431ea16 100644 --- a/dev/v8-syntax/syntax-v8.tex +++ b/dev/v8-syntax/syntax-v8.tex @@ -81,7 +81,7 @@ Parenthesis are used to group regexps. Beware to distinguish this operator $\GR{~}$ from the terminals $\ETERM{( )}$, and $\mid$ from terminal \TERMbar. -Rules are optionaly annotated in the right margin with: +Rules are optionally annotated in the right margin with: \begin{itemize} \item a precedence and associativity (L for left, R for right and N for no associativity), indicating how to solve conflicts; lower levels are tighter; diff --git a/doc/refman/Program.tex b/doc/refman/Program.tex index efcc84ee9..11dd3a051 100644 --- a/doc/refman/Program.tex +++ b/doc/refman/Program.tex @@ -201,7 +201,7 @@ in their context. In this case, the obligations should be transparent recursive calls can be checked by the kernel's type-checker. There is an optimization in the generation of obligations which gets rid of the hypothesis corresponding to the -functionnal when it is not necessary, so that the obligation can be +functional when it is not necessary, so that the obligation can be declared opaque (e.g. using {\tt Qed}). However, as soon as it appears in the context, the proof of the obligation is \emph{required} to be declared transparent. @@ -216,7 +216,7 @@ properties. It will generate obligations, try to solve them automatically and fail if some unsolved obligations remain. In this case, one can first define the lemma's statement using {\tt Program Definition} and use it as the goal afterwards. -Otherwise the proof will be started with the elobarted version as a goal. +Otherwise the proof will be started with the elaborated version as a goal. The {\tt Program} prefix can similarly be used as a prefix for {\tt Variable}, {\tt Hypothesis}, {\tt Axiom} etc... diff --git a/doc/refman/RefMan-cic.tex b/doc/refman/RefMan-cic.tex index 3fd5ae0b2..9d79f7cac 100644 --- a/doc/refman/RefMan-cic.tex +++ b/doc/refman/RefMan-cic.tex @@ -109,7 +109,7 @@ sets, namely the sorts {\Set} and {\Type$(j)$} for $j<i$, and all products, subsets and function types over these sorts. Formally, we call {\Sort} the set of sorts which is defined by: -\[\Sort \equiv \{\Prop,\Set,\Type(i)| i \in \NN\} \] +\[\Sort \equiv \{\Prop,\Set,\Type(i)\;|\; i \in \NN\} \] \index{Type@{\Type}} \index{Prop@{\Prop}} \index{Set@{\Set}} @@ -128,7 +128,7 @@ the universe \Type$(i)$. One only writes \Type. The system itself generates for each instance of \Type\ a new index for the universe and checks that the constraints between these indexes can be solved. From the user point of view we consequently -have {\sf Type :Type}. +have {\Type}:{\Type}. We shall make precise in the typing rules the constraints between the indexes. @@ -140,7 +140,8 @@ identifier with a number) or a successor of an algebraic universe (an expression $u+1$), or an upper bound of algebraic universes (an expression $max(u_1,...,u_n)$), or the base universe (the expression $0$) which corresponds, in the arity of sort-polymorphic inductive -types, to the predicative sort {\Set}. A graph of constraints between +types (see Section \ref{Sort-polymorphism-inductive}), +to the predicative sort {\Set}. A graph of constraints between the universe variables is maintained globally. To ensure the existence of a mapping of the universes to the positive integers, the graph of constraints must remain acyclic. Typing expressions that violate the @@ -148,9 +149,10 @@ acyclicity of the graph of constraints results in a \errindex{Universe inconsistency} error (see also Section~\ref{PrintingUniverses}). \subsection{Constants} -Besides the sorts, the language also contains constants denoting -objects in the environment. These constants may denote previously -defined objects but also objects related to inductive definitions + +Constants refers to +objects in the global environment. These constants may denote previously +defined objects, but also objects related to inductive definitions (either the type itself or one of its constructors or destructors). \medskip\noindent {\bf Remark. } In other presentations of \CIC, @@ -174,7 +176,7 @@ in a theory where inductive objects are represented by terms. \subsection{Terms} -Terms are built from variables, global names, constructors, +Terms are built from variables, constants, constructors, abstraction, application, local declarations bindings (``let-in'' expressions) and product. @@ -213,7 +215,7 @@ More precisely the language of the {\em Calculus of Inductive \end{enumerate} \paragraph{Notations.} Application associates to the left such that -$(t~t_1\ldots t_n)$ represents $(\ldots (t~t_1)\ldots t_n)$. The +$(t\;t_1\;t_2\ldots t_n)$ represents $(\ldots ((t\;t_1)\;t_2)\ldots t_n)$. The products and arrows associate to the right such that $\forall~x:A,B\ra C\ra D$ represents $\forall~x:A,(B\ra (C\ra D))$. One uses sometimes $\forall~x~y:A,B$ or @@ -236,33 +238,33 @@ is written $\subst{u}{x}{t}$. \section[Typed terms]{Typed terms\label{Typed-terms}} As objects of type theory, terms are subjected to {\em type -discipline}. The well typing of a term depends on an environment which -consists in a global environment (see below) and a local context. +discipline}. The well typing of a term depends on +a global environment (see below) and a local context. \paragraph{Local context.} -A {\em local context} (or shortly context) is an ordered list of +A {\em local context} is an ordered list of declarations of variables. The declaration of some variable $x$ is -either an assumption, written $x:T$ ($T$ is a type) or a definition, -written $x:=t:T$. We use brackets to write contexts. A +either a local assumption, written $x:T$ ($T$ is a type) or a local definition, +written $x:=t:T$. We use brackets to write local contexts. A typical example is $[x:T;y:=u:U;z:V]$. Notice that the variables -declared in a context must be distinct. If $\Gamma$ declares some $x$, +declared in a local context must be distinct. If $\Gamma$ declares some $x$, we write $x \in \Gamma$. By writing $(x:T) \in \Gamma$ we mean that either $x:T$ is an assumption in $\Gamma$ or that there exists some $t$ such that $x:=t:T$ is a definition in $\Gamma$. If $\Gamma$ defines some -$x:=t:T$, we also write $(x:=t:T) \in \Gamma$. Contexts must be -themselves {\em well formed}. For the rest of the chapter, the -notation $\Gamma::(y:T)$ (resp. $\Gamma::(y:=t:T)$) denotes the context +$x:=t:T$, we also write $(x:=t:T) \in \Gamma$. +For the rest of the chapter, the +notation $\Gamma::(y:T)$ (resp. $\Gamma::(y:=t:T)$) denotes the local context $\Gamma$ enriched with the declaration $y:T$ (resp. $y:=t:T$). The -notation $[]$ denotes the empty context. \index{Context} +notation $[]$ denotes the empty local context. \index{Local context} % Does not seem to be used further... % Si dans l'explication WF(E)[Gamma] concernant les constantes % definies ds un contexte -We define the inclusion of two contexts $\Gamma$ and $\Delta$ (written -as $\Gamma \subset \Delta$) as the property, for all variable $x$, -type $T$ and term $t$, if $(x:T) \in \Gamma$ then $(x:T) \in \Delta$ -and if $(x:=t:T) \in \Gamma$ then $(x:=t:T) \in \Delta$. +%We define the inclusion of two local contexts $\Gamma$ and $\Delta$ (written +%as $\Gamma \subset \Delta$) as the property, for all variable $x$, +%type $T$ and term $t$, if $(x:T) \in \Gamma$ then $(x:T) \in \Delta$ +%and if $(x:=t:T) \in \Gamma$ then $(x:=t:T) \in \Delta$. %We write % $|\Delta|$ for the length of the context $\Delta$, that is for the number % of declarations (assumptions or definitions) in $\Delta$. @@ -270,22 +272,20 @@ and if $(x:=t:T) \in \Gamma$ then $(x:=t:T) \in \Delta$. A variable $x$ is said to be free in $\Gamma$ if $\Gamma$ contains a declaration $y:T$ such that $x$ is free in $T$. -\paragraph[Environment.]{Environment.\index{Environment}} -Because we are manipulating global declarations (constants and global -assumptions), we also need to consider a global environment $E$. +\paragraph[Global environment.]{Global environment.\index{Global environment}} +%Because we are manipulating global declarations (global constants and global +%assumptions), we also need to consider a global environment $E$. -An environment is an ordered list of declarations of global -names. Declarations are either assumptions or ``standard'' -definitions, that is abbreviations for well-formed terms -but also definitions of inductive objects. In the latter -case, an object in the environment will define one or more constants -(that is types and constructors, see Section~\ref{Cic-inductive-definitions}). +A {\em global environment} is an ordered list of global declarations. +Global declarations are either global assumptions or global +definitions, but also declarations of inductive objects. Inductive objects themselves declares both inductive or coinductive types and constructors +(see Section~\ref{Cic-inductive-definitions}). -An assumption will be represented in the environment as +A global assumption will be represented in the global environment as \Assum{\Gamma}{c}{T} which means that $c$ is assumed of some type $T$ -well-defined in some context $\Gamma$. An (ordinary) definition will -be represented in the environment as \Def{\Gamma}{c}{t}{T} which means -that $c$ is a constant which is valid in some context $\Gamma$ whose +well-defined in some local context $\Gamma$. A global definition will +be represented in the global environment as \Def{\Gamma}{c}{t}{T} which means +that $c$ is a constant which is valid in some local context $\Gamma$ whose value is $t$ and type is $T$. The rules for inductive definitions (see section @@ -295,23 +295,27 @@ declared in $E$, we write $c \in E$ and if $c:T$ or $c:=t:T$ is declared in $E$, we write $(c : T) \in E$. \paragraph[Typing rules.]{Typing rules.\label{Typing-rules}\index{Typing rules}} -In the following, we assume $E$ is a valid environment w.r.t. -inductive definitions. We define simultaneously two +In the following, we define simultaneously two judgments. The first one \WTEG{t}{T} means the term $t$ is well-typed -and has type $T$ in the environment $E$ and context $\Gamma$. The -second judgment \WFE{\Gamma} means that the environment $E$ is -well-formed and the context $\Gamma$ is a valid context in this -environment. It also means a third property which makes sure that any -constant in $E$ was defined in an environment which is included in -$\Gamma$ -\footnote{This requirement could be relaxed if we instead introduced - an explicit mechanism for instantiating constants. At the external - level, the Coq engine works accordingly to this view that all the - definitions in the environment were built in a sub-context of the - current context.}. - -A term $t$ is well typed in an environment $E$ iff there exists a -context $\Gamma$ and a term $T$ such that the judgment \WTEG{t}{T} can +and has type $T$ in the global environment $E$ and local context $\Gamma$. The +second judgment \WFE{\Gamma} means that the global environment $E$ is +well-formed and the local context $\Gamma$ is a valid local context in this +global environment. +% HH: This looks to me complicated. I think it would be better to talk +% about ``discharge'' as a transformation of global environments, +% rather than as keeping a local context next to global constants. +% +%% It also means a third property which makes sure that any +%%constant in $E$ was defined in an environment which is included in +%%$\Gamma$ +%%\footnote{This requirement could be relaxed if we instead introduced +%% an explicit mechanism for instantiating constants. At the external +%% level, the Coq engine works accordingly to this view that all the +%% definitions in the environment were built in a local sub-context of the +%% current local context.}. + +A term $t$ is well typed in a global environment $E$ iff there exists a +local context $\Gamma$ and a term $T$ such that the judgment \WTEG{t}{T} can be derived from the following rules. \begin{description} \item[W-E] \inference{\WF{[]}{[]}} @@ -368,7 +372,7 @@ may be used in a conversion rule (see Section~\ref{conv-rules}). We want to be able to identify some terms as we can identify the application of a function to a given argument with its result. For instance the identity function over a given type $T$ can be written -$\lb x:T\mto x$. In any environment $E$ and context $\Gamma$, we want to identify any object $a$ (of type $T$) with the +$\lb x:T\mto x$. In any global environment $E$ and local context $\Gamma$, we want to identify any object $a$ (of type $T$) with the application $((\lb x:T\mto x)~a)$. We define for this a {\em reduction} (or a {\em conversion}) rule we call $\beta$: \[ \WTEGRED{((\lb x:T\mto @@ -385,7 +389,7 @@ refer the interested reader to \cite{Coq85}. \paragraph[$\iota$-reduction.]{$\iota$-reduction.\label{iota}\index{iota-reduction@$\iota$-reduction}} A specific conversion rule is associated to the inductive objects in -the environment. We shall give later on (see Section~\ref{iotared}) the +the global environment. We shall give later on (see Section~\ref{iotared}) the precise rules but it just says that a destructor applied to an object built from a constructor behaves as expected. This reduction is called $\iota$-reduction and is more precisely studied in @@ -394,7 +398,7 @@ called $\iota$-reduction and is more precisely studied in \paragraph[$\delta$-reduction.]{$\delta$-reduction.\label{delta}\index{delta-reduction@$\delta$-reduction}} -We may have defined variables in contexts or constants in the global +We may have defined variables in local contexts or constants in the global environment. It is legal to identify such a reference with its value, that is to expand (or unfold) it into its value. This reduction is called $\delta$-reduction and shows as follows. @@ -421,7 +425,7 @@ term $t$ of functional type $\forall x:T, U$ with its so-called $\eta$-expansion $\lb x:T\mto (t\ x)$ for $x$ an arbitrary variable name fresh in $t$. -The notion of $\eta$-reduction ${\lb x:T\mto (t\ x)}{\triangleright}{t}$ +The notion of $\eta$-reduction ${\lb x:T\mto (t\ x)}{\;\triangleright\;}{t}$ (for $x$ not occurring in $t$) is not type-sound because of subtyping (think about $\lb x:\Type(1)\mto (f x)$ of type $\forall x:\Type(1), \Type(1)$ for $f$ of type $\forall x:\Type(2), @@ -433,12 +437,12 @@ the type. However, $\eta$ can be used as a conversion rule. \paragraph[Convertibility.]{Convertibility.\label{convertibility} \index{beta-reduction@$\beta$-reduction}\index{iota-reduction@$\iota$-reduction}\index{delta-reduction@$\delta$-reduction}\index{zeta-reduction@$\zeta$-reduction}} -Let us write $\WTEGRED{t}{\triangleright}{u}$ for the contextual closure of the relation $t$ reduces to $u$ in the environment $E$ and context $\Gamma$ with one of the previous reduction $\beta$, $\iota$, $\delta$ or $\zeta$. +Let us write $\WTEGRED{t}{\triangleright}{u}$ for the contextual closure of the relation $t$ reduces to $u$ in the global environment $E$ and local context $\Gamma$ with one of the previous reduction $\beta$, $\iota$, $\delta$ or $\zeta$. We say that two terms $t_1$ and $t_2$ are {\em $\beta\iota\delta\zeta\eta$-convertible}, or simply {\em - convertible}, or {\em equivalent}, in the environment $E$ and -context $\Gamma$ iff there exist terms $u_1$ and $u_2$ such that + convertible}, or {\em equivalent}, in the global environment $E$ and +local context $\Gamma$ iff there exist terms $u_1$ and $u_2$ such that $\WTEGRED{t_1}{\triangleright \ldots \triangleright}{u_1}$ and $\WTEGRED{t_2}{\triangleright \ldots \triangleright}{u_2}$ and either $u_1$ and $u_2$ are identical, or they are convertible up to @@ -501,10 +505,10 @@ $u_i$ can be reducible. Similar notions of head-normal forms involving $\delta$, $\iota$ and $\zeta$ reductions or any combination of those can also be defined. -\section{Derived rules for environments} +\section{Derived rules for global environments} From the original rules of the type system, one can derive new rules -which change the context of definition of objects in the environment. +which change the local context of definition of objects in the global environment. Because these rules correspond to elementary operations in the \Coq\ engine used in the discharge mechanism at the end of a section, we state them explicitly. @@ -512,9 +516,9 @@ state them explicitly. \paragraph{Mechanism of substitution.} One rule which can be proved valid, is to replace a term $c$ by its -value in the environment. As we defined the substitution of a term for +value in the global environment. As we defined the substitution of a term for a variable in a term, one can define the substitution of a term for a -constant. One easily extends this substitution to contexts and +constant. One easily extends this substitution to local contexts and global environments. \paragraph{Substitution Property:} @@ -524,13 +528,13 @@ environments. \paragraph{Abstraction.} -One can modify the context of definition of a constant $c$ by +One can modify the local context of definition of a constant $c$ by abstracting a constant with respect to the last variable $x$ of its -defining context. For doing that, we need to check that the constants +defining local context. For doing that, we need to check that the constants appearing in the body of the declaration do not depend on $x$, we need -also to modify the reference to the constant $c$ in the environment -and context by explicitly applying this constant to the variable $x$. -Because of the rules for building environments and terms we know the +also to modify the reference to the constant $c$ in the global environment +and local context by explicitly applying this constant to the variable $x$. +Because of the rules for building global environments and terms we know the variable $x$ is available at each stage where $c$ is mentioned. \paragraph{Abstracting property:} @@ -539,13 +543,13 @@ variable $x$ is available at each stage where $c$ is mentioned. {\WF{E;\Def{\Gamma}{c}{\lb x:U\mto t}{\forall~x:U,T}; \subst{F}{c}{(c~x)}}{\subst{\Delta}{c}{(c~x)}}}} -\paragraph{Pruning the context.} -We said the judgment \WFE{\Gamma} means that the defining contexts of +\paragraph{Pruning the local context.} +We said the judgment \WFE{\Gamma} means that the defining local contexts of constants in $E$ are included in $\Gamma$. If one abstracts or substitutes the constants with the above rules then it may happen -that the context $\Gamma$ is now bigger than the one needed for -defining the constants in $E$. Because defining contexts are growing -in $E$, the minimum context needed for defining the constants in $E$ +that the local context $\Gamma$ is now bigger than the one needed for +defining the constants in $E$. Because defining local contexts are growing +in $E$, the minimum local context needed for defining the constants in $E$ is the same as the one for the last constant. One can consequently derive the following property. @@ -559,8 +563,8 @@ derive the following property. A (possibly mutual) inductive definition is specified by giving the names and the type of the inductive sets or families to be defined and the names and types of the constructors of the inductive -predicates. An inductive declaration in the environment can -consequently be represented with two contexts (one for inductive +predicates. An inductive declaration in the global environment can +consequently be represented with two local contexts (one for inductive definitions, one for constructors). Stating the rules for inductive definitions in their general form @@ -574,15 +578,15 @@ forests. \subsection{Representing an inductive definition} \subsubsection{Inductive definitions without parameters} As for constants, inductive definitions can be defined in a non-empty -context. \\ +local context. \\ We write \NInd{\Gamma}{\Gamma_I}{\Gamma_C} an inductive -definition valid in a context $\Gamma$, a -context of definitions $\Gamma_I$ and a context of constructors +definition valid in a local context $\Gamma$, a +context of type definitions $\Gamma_I$ and a context of constructors $\Gamma_C$. \paragraph{Examples.} The inductive declaration for the type of natural numbers will be: \[\NInd{}{\nat:\Set}{\nO:\nat,\nS:\nat\ra\nat}\] -In a context with a variable $A:\Set$, the lists of elements in $A$ are +In a local context with a variable $A:\Set$, the lists of elements in $A$ are represented by: \[\NInd{A:\Set}{\List:\Set}{\Nil:\List,\cons : A \ra \List \ra \List}\] @@ -601,7 +605,7 @@ represented by: We have to slightly complicate the representation above in order to handle the delicate problem of parameters. Let us explain that on the example of \List. With the above definition, -the type \List\ can only be used in an environment where we +the type \List\ can only be used in a global environment where we have a variable $A:\Set$. Generally one want to consider lists of elements in different types. For constants this is easily done by abstracting the value over the parameter. In the case of inductive definitions we @@ -628,11 +632,11 @@ We say that $q$ is the number of real arguments of the constructor $c$. \paragraph{Context of parameters.} If an inductive definition $\NInd{\Gamma}{\Gamma_I}{\Gamma_C}$ admits -$r$ inductive parameters, then there exists a context $\Gamma_P$ of +$r$ inductive parameters, then there exists a local context $\Gamma_P$ of size $r$, such that $\Gamma_P=[p_1:P_1;\ldots;p_r:P_r]$ and if $(t:A) \in \Gamma_I,\Gamma_C$ then $A$ can be written as $\forall p_1:P_1,\ldots \forall p_r:P_r,A'$. -We call $\Gamma_P$ the context of parameters of the inductive +We call $\Gamma_P$ the local context of parameters of the inductive definition and use the notation $\forall \Gamma_P,A'$ for the term $A$. \paragraph{Remark.} If we have a term $t$ in an instance of an @@ -660,7 +664,7 @@ But the following definition has $0$ parameters: %$\NInd{}{\List:\Set\ra\Set}{\Nil:(A:\Set)(\List~A),\cons : (A:\Set)A % \ra (\List~A\ra A) \ra (\List~A)}$.} \paragraph{Concrete syntax.} -In the Coq system, the context of parameters is given explicitly +In the Coq system, the local context of parameters is given explicitly after the name of the inductive definitions and is shared between the arities and the type of constructors. % The vernacular declaration of polymorphic trees and forests will be:\\ @@ -683,7 +687,7 @@ parameters. Formally the representation of an inductive declaration will be \Ind{\Gamma}{p}{\Gamma_I}{\Gamma_C} for an inductive -definition valid in a context $\Gamma$ with $p$ parameters, a +definition valid in a local context $\Gamma$ with $p$ parameters, a context of definitions $\Gamma_I$ and a context of constructors $\Gamma_C$. @@ -761,7 +765,7 @@ Inductive list' (A:Set) : Set := \subsection{Types of inductive objects} -We have to give the type of constants in an environment $E$ which +We have to give the type of constants in a global environment $E$ which contains an inductive declaration. \begin{description} @@ -879,7 +883,7 @@ We shall now describe the rules allowing the introduction of a new inductive definition. \begin{description} -\item[W-Ind] Let $E$ be an environment and +\item[W-Ind] Let $E$ be a global environment and $\Gamma,\Gamma_P,\Gamma_I,\Gamma_C$ are contexts such that $\Gamma_I$ is $[I_1:\forall \Gamma_P,A_1;\ldots;I_k:\forall \Gamma_P,A_k]$ and $\Gamma_C$ is @@ -939,20 +943,21 @@ Inductive exType (P:Type->Prop) : Type %a recursive argument and $(x:_P T)C$ if the argument is not recursive. \paragraph[Sort-polymorphism of inductive families.]{Sort-polymorphism of inductive families.\index{Sort-polymorphism of inductive families}} +\label{Sort-polymorphism-inductive} From {\Coq} version 8.1, inductive families declared in {\Type} are polymorphic over their arguments in {\Type}. If $A$ is an arity and $s$ a sort, we write $A_{/s}$ for the arity obtained from $A$ by replacing its sort with $s$. Especially, if $A$ -is well-typed in some environment and context, then $A_{/s}$ is typable +is well-typed in some global environment and local context, then $A_{/s}$ is typable by typability of all products in the Calculus of Inductive Constructions. The following typing rule is added to the theory. \begin{description} \item[Ind-Family] Let $\Ind{\Gamma}{p}{\Gamma_I}{\Gamma_C}$ be an inductive definition. Let $\Gamma_P = [p_1:P_1;\ldots;p_{p}:P_{p}]$ - be its context of parameters, $\Gamma_I = [I_1:\forall + be its local context of parameters, $\Gamma_I = [I_1:\forall \Gamma_P,A_1;\ldots;I_k:\forall \Gamma_P,A_k]$ its context of definitions and $\Gamma_C = [c_1:\forall \Gamma_P,C_1;\ldots;c_n:\forall \Gamma_P,C_n]$ its context of @@ -1103,7 +1108,7 @@ a strongly normalizing reduction, we cannot accept any sort of recursion (even terminating). So the basic idea is to restrict ourselves to primitive recursive functions and functionals. -For instance, assuming a parameter $A:\Set$ exists in the context, we +For instance, assuming a parameter $A:\Set$ exists in the local context, we want to build a function \length\ of type $\ListA\ra \nat$ which computes the length of the list, so such that $(\length~(\Nil~A)) = \nO$ and $(\length~(\cons~A~a~l)) = (\nS~(\length~l))$. We want these @@ -1362,7 +1367,7 @@ constructor have type \Prop. In that case, there is a canonical way to interpret the informative extraction on an object in that type, such that the elimination on any sort $s$ is legal. Typical examples are the conjunction of non-informative propositions and the equality. -If there is an hypothesis $h:a=b$ in the context, it can be used for +If there is an hypothesis $h:a=b$ in the local context, it can be used for rewriting not only in logical propositions but also in any type. % In that case, the term \verb!eq_rec! which was defined as an axiom, is % now a term of the calculus. @@ -1436,8 +1441,8 @@ only constructors of $I$. \paragraph{Example.} For \List\ and \Length\ the typing rules for the {\tt match} expression -are (writing just $t:M$ instead of \WTEG{t}{M}, the environment and -context being the same in all the judgments). +are (writing just $t:M$ instead of \WTEG{t}{M}, the global environment and +local context being the same in all the judgments). \[\frac{l:\ListA~~P:\ListA\ra s~~~f_1:(P~(\Nil~A))~~ f_2:\forall a:A, \forall l:\ListA, (P~(\cons~A~a~l))} diff --git a/doc/refman/RefMan-ext.tex b/doc/refman/RefMan-ext.tex index 80e12898f..a2be25c3b 100644 --- a/doc/refman/RefMan-ext.tex +++ b/doc/refman/RefMan-ext.tex @@ -1250,7 +1250,7 @@ possible, the correct argument will be automatically generated. \end{ErrMsgs} -\subsection{Declaration of implicit arguments for a constant +\subsection{Declaration of implicit arguments \comindex{Arguments}} \label{ImplicitArguments} @@ -1263,7 +1263,7 @@ a priori and a posteriori. \subsubsection{Implicit Argument Binders} In the first setting, one wants to explicitly give the implicit -arguments of a constant as part of its definition. To do this, one has +arguments of a declared object as part of its definition. To do this, one has to surround the bindings of implicit arguments by curly braces: \begin{coq_eval} Reset Initial. @@ -1300,7 +1300,7 @@ usual implicit arguments disambiguation syntax. \subsubsection{Declaring Implicit Arguments} -To set implicit arguments for a constant a posteriori, one can use the +To set implicit arguments a posteriori, one can use the command: \begin{quote} \tt Arguments {\qualid} \nelist{\possiblybracketedident}{} @@ -1379,7 +1379,7 @@ Check (fun l => map length l = map (list nat) nat length l). \Rem To know which are the implicit arguments of an object, use the command {\tt Print Implicit} (see \ref{PrintImplicit}). -\subsection{Automatic declaration of implicit arguments for a constant} +\subsection{Automatic declaration of implicit arguments} {\Coq} can also automatically detect what are the implicit arguments of a defined object. The command is just @@ -1582,7 +1582,7 @@ Implicit arguments names can be redefined using the following syntax: \end{quote} Without the {\tt rename} flag, {\tt Arguments} can be used to assert -that a given constant has the expected number of arguments and that +that a given object has the expected number of arguments and that these arguments are named as expected. \noindent {\bf Example (continued): } diff --git a/doc/refman/RefMan-gal.tex b/doc/refman/RefMan-gal.tex index 9b527053c..e49c82d8f 100644 --- a/doc/refman/RefMan-gal.tex +++ b/doc/refman/RefMan-gal.tex @@ -971,7 +971,7 @@ are the names of its constructors and {\type$_1$}, {\ldots}, {\type$_n$} their respective types. The types of the constructors have to satisfy a {\em positivity condition} (see Section~\ref{Positivity}) for {\ident}. This condition ensures the soundness of the inductive -definition. If this is the case, the constants {\ident}, +definition. If this is the case, the names {\ident}, {\ident$_1$}, {\ldots}, {\ident$_n$} are added to the environment with their respective types. Accordingly to the universe where the inductive type lives ({\it e.g.} its type {\sort}), {\Coq} provides a @@ -990,7 +990,7 @@ Inductive nat : Set := \end{coq_example} The type {\tt nat} is defined as the least \verb:Set: containing {\tt - O} and closed by the {\tt S} constructor. The constants {\tt nat}, + O} and closed by the {\tt S} constructor. The names {\tt nat}, {\tt O} and {\tt S} are added to the environment. Now let us have a look at the elimination principles. They are three @@ -1101,7 +1101,7 @@ Inductive list (A:Set) : Set := \end{coq_example*} Note that in the type of {\tt nil} and {\tt cons}, we write {\tt - (list A)} and not just {\tt list}.\\ The constants {\tt nil} and + (list A)} and not just {\tt list}.\\ The constructors {\tt nil} and {\tt cons} will have respectively types: \begin{coq_example} diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex index b855a0eac..ddb48b0c1 100644 --- a/doc/refman/RefMan-tac.tex +++ b/doc/refman/RefMan-tac.tex @@ -1531,25 +1531,27 @@ for each possible form of {\term}, i.e. one for each constructor of the inductive or co-inductive type. Unlike {\tt induction}, no induction hypothesis is generated by {\tt destruct}. -If the argument is dependent in either the conclusion or some -hypotheses of the goal, the argument is replaced by the appropriate -constructor form in each of the resulting subgoals, thus performing -case analysis. If non-dependent, the tactic simply exposes the -inductive or co-inductive structure of the argument. - There are special cases: \begin{itemize} \item If {\term} is an identifier {\ident} denoting a quantified -variable of the conclusion of the goal, then {\tt destruct {\ident}} -behaves as {\tt intros until {\ident}; destruct {\ident}}. + variable of the conclusion of the goal, then {\tt destruct {\ident}} + behaves as {\tt intros until {\ident}; destruct {\ident}}. If + {\ident} is not anymore dependent in the goal after application of + {\tt destruct}, it is erased (to avoid erasure, use + parentheses, as in {\tt destruct ({\ident})}). \item If {\term} is a {\num}, then {\tt destruct {\num}} behaves as {\tt intros until {\num}} followed by {\tt destruct} applied to the last introduced hypothesis. Remark: For destruction of a numeral, use syntax {\tt destruct ({\num})} (not very interesting anyway). +\item In case {\term} is an hypothesis {\ident} of the context, + and {\ident} is not anymore dependent in the goal after + application of {\tt destruct}, it is erased (to avoid erasure, use + parentheses, as in {\tt destruct ({\ident})}). + \item The argument {\term} can also be a pattern of which holes are denoted by ``\_''. In this case, the tactic checks that all subterms matching the pattern in the conclusion and the hypotheses are @@ -1626,14 +1628,6 @@ syntax {\tt destruct ({\num})} (not very interesting anyway). They combine the effects of the {\tt with}, {\tt as}, {\tt eqn:}, {\tt using}, and {\tt in} clauses. -\item{\tt destruct !{\ident}} - - This is a case when the destructed term is an hypothesis of the - context. The ``!'' modifier tells to keep the hypothesis in the - context after destruction. - - This applies also to the other form of {\tt destruct} and {\tt edestruct}. - \item{\tt case \term}\label{case}\tacindex{case} The tactic {\tt case} is a more basic tactic to perform case @@ -1699,14 +1693,22 @@ There are particular cases: \begin{itemize} \item If {\term} is an identifier {\ident} denoting a quantified -variable of the conclusion of the goal, then {\tt induction {\ident}} -behaves as {\tt intros until {\ident}; induction {\ident}}. + variable of the conclusion of the goal, then {\tt induction + {\ident}} behaves as {\tt intros until {\ident}; induction + {\ident}}. If {\ident} is not anymore dependent in the goal + after application of {\tt induction}, it is erased (to avoid + erasure, use parentheses, as in {\tt induction ({\ident})}). \item If {\term} is a {\num}, then {\tt induction {\num}} behaves as {\tt intros until {\num}} followed by {\tt induction} applied to the last introduced hypothesis. Remark: For simple induction on a numeral, use syntax {\tt induction ({\num})} (not very interesting anyway). +\item In case {\term} is an hypothesis {\ident} of the context, + and {\ident} is not anymore dependent in the goal after + application of {\tt induction}, it is erased (to avoid erasure, use + parentheses, as in {\tt induction ({\ident})}). + \item The argument {\term} can also be a pattern of which holes are denoted by ``\_''. In this case, the tactic checks that all subterms matching the pattern in the conclusion and the hypotheses are @@ -1821,15 +1823,6 @@ Show 2. einduction}. It combines the effects of the {\tt with}, {\tt as}, %%{\tt eqn:}, {\tt using}, and {\tt in} clauses. -\item{\tt induction !{\ident}} - - This is a case when the term on which to apply induction is an - hypothesis of the context. The ``!'' modifier tells to keep the - hypothesis in the context after induction. - - This applies also to the other form of {\tt induction} and {\tt - einduction}. - \item {\tt elim \term}\label{elim} This is a more basic induction tactic. Again, the type of the @@ -3562,7 +3555,7 @@ The hints for \texttt{auto} and \texttt{eauto} are stored in databases. Each database maps head symbols to a list of hints. One can use the command \texttt{Print Hint \ident} to display the hints associated to the head symbol \ident{} (see \ref{PrintHint}). Each -hint has a cost that is an nonnegative integer, and an optional pattern. +hint has a cost that is a nonnegative integer, and an optional pattern. The hints with lower cost are tried first. A hint is tried by \texttt{auto} when the conclusion of the current goal matches its pattern or when it has no pattern. @@ -3779,7 +3772,7 @@ Hint Extern 4 (~(_ = _)) => discriminate. with hints with a cost less than 4. One can even use some sub-patterns of the pattern in the tactic - script. A sub-pattern is a question mark followed by an ident, like + script. A sub-pattern is a question mark followed by an identifier, like \texttt{?X1} or \texttt{?X2}. Here is an example: % Require EqDecide. @@ -3822,7 +3815,7 @@ The \texttt{emp} regexp does not match any search path while \texttt{eps} matches the empty path. During proof search, the path of successive successful hints on a search branch is recorded, as a list of identifiers for the hints (note \texttt{Hint Extern}'s do not have an -associated identitier). Before applying any hint $\ident$ the current +associated identifier). Before applying any hint $\ident$ the current path $p$ extended with $\ident$ is matched against the current cut expression $c$ associated to the hint database. If matching succeeds, the hint is \emph{not} applied. The semantics of \texttt{Hint Cut} $e$ @@ -4679,7 +4672,7 @@ Use \texttt{classical\_right} to prove the right part of the disjunction with th %% procedure for first-order intuitionistic logic implemented in {\em %% NuPRL}\cite{Kre02}. -%% Search may optionnaly be bounded by a multiplicity parameter +%% Search may optionally be bounded by a multiplicity parameter %% indicating how many (at most) copies of a formula may be used in %% the proof process, its absence may lead to non-termination of the tactic. diff --git a/kernel/closure.ml b/kernel/closure.ml index bc414d971..1a50478e0 100644 --- a/kernel/closure.ml +++ b/kernel/closure.ml @@ -762,7 +762,7 @@ let drop_parameters depth n argstk = (* we know that n < stack_args_size(argstk) (if well-typed term) *) anomaly (Pp.str "ill-typed term: found a match on a partially applied constructor") -(** [eta_expand_ind_stack env ind c s t] computes stacks correspoding +(** [eta_expand_ind_stack env ind c s t] computes stacks corresponding to the conversion of the eta expansion of t, considered as an inhabitant of ind, and the Constructor c of this inductive type applied to arguments s. diff --git a/kernel/fast_typeops.ml b/kernel/fast_typeops.ml index 063c9cf12..b625478f2 100644 --- a/kernel/fast_typeops.ml +++ b/kernel/fast_typeops.ml @@ -33,7 +33,7 @@ let check_constraints cst env = if Environ.check_constraints cst env then () else error_unsatisfied_constraints env cst -(* This should be a type (a priori without intension to be an assumption) *) +(* This should be a type (a priori without intention to be an assumption) *) let type_judgment env c t = match kind_of_term(whd_betadeltaiota env t) with | Sort s -> {utj_val = c; utj_type = s } @@ -52,8 +52,8 @@ let assumption_of_judgment env t ty = error_assumption env (make_judge t ty) (************************************************) -(* Incremental typing rules: builds a typing judgement given the *) -(* judgements for the subterms. *) +(* Incremental typing rules: builds a typing judgment given the *) +(* judgments for the subterms. *) (*s Type of sorts *) diff --git a/kernel/opaqueproof.mli b/kernel/opaqueproof.mli index 0609c8517..009ff82ff 100644 --- a/kernel/opaqueproof.mli +++ b/kernel/opaqueproof.mli @@ -11,9 +11,9 @@ open Term open Mod_subst (** This module implements the handling of opaque proof terms. - Opauqe proof terms are special since: + Opaque proof terms are special since: - they can be lazily computed and substituted - - they are stoked in an optionally loaded segment of .vo files + - they are stored in an optionally loaded segment of .vo files An [opaque] proof terms holds the real data until fully discharged. In this case it is called [direct]. When it is [turn_indirect] the data is relocated to an opaque table diff --git a/library/universes.ml b/library/universes.ml index 96937b3b3..b9b148b57 100644 --- a/library/universes.ml +++ b/library/universes.ml @@ -899,22 +899,28 @@ let normalize_context_set ctx us algs = let noneqs = Constraint.union noneqs smallles in let partition = UF.partition uf in let flex x = LMap.mem x us in - let ctx, subst, eqs = List.fold_left (fun (ctx, subst, cstrs) s -> + let ctx, subst, us, eqs = List.fold_left (fun (ctx, subst, us, cstrs) s -> let canon, (global, rigid, flexible) = choose_canonical ctx flex algs s in (* Add equalities for globals which can't be merged anymore. *) let cstrs = LSet.fold (fun g cst -> Constraint.add (canon, Univ.Eq, g) cst) global cstrs in + (* Also add equalities for rigid variables *) + let cstrs = LSet.fold (fun g cst -> + Constraint.add (canon, Univ.Eq, g) cst) rigid + cstrs + in let subst = LSet.fold (fun f -> LMap.add f canon) rigid subst in - let subst = LSet.fold (fun f -> LMap.add f canon) flexible subst in - (LSet.diff (LSet.diff ctx rigid) flexible, subst, cstrs)) - (ctx, LMap.empty, Constraint.empty) partition + let subst = LSet.fold (fun f -> LMap.add f canon) flexible subst in + let canonu = Some (Universe.make canon) in + let us = LSet.fold (fun f -> LMap.add f canonu) flexible us in + (LSet.diff ctx flexible, subst, us, cstrs)) + (ctx, LMap.empty, us, Constraint.empty) partition in (* Noneqs is now in canonical form w.r.t. equality constraints, and contains only inequality constraints. *) let noneqs = subst_univs_level_constraints subst noneqs in - let us = LMap.fold (fun u v acc -> LMap.add u (Some (Universe.make v)) acc) subst us in (* Compute the left and right set of flexible variables, constraints mentionning other variables remain in noneqs. *) let noneqs, ucstrsl, ucstrsr = diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4 index b7559a198..4d42dfe85 100644 --- a/parsing/g_tactic.ml4 +++ b/parsing/g_tactic.ml4 @@ -44,6 +44,20 @@ let test_lpar_id_coloneq = | _ -> err ()) | _ -> err ()) +(* Hack to recognize "(x)" *) +let test_lpar_id_rpar = + Gram.Entry.of_parser "lpar_id_coloneq" + (fun strm -> + match get_tok (stream_nth 0 strm) with + | KEYWORD "(" -> + (match get_tok (stream_nth 1 strm) with + | IDENT _ -> + (match get_tok (stream_nth 2 strm) with + | KEYWORD ")" -> () + | _ -> err ()) + | _ -> err ()) + | _ -> err ()) + (* idem for (x:=t) and (1:=t) *) let test_lpar_idnum_coloneq = Gram.Entry.of_parser "test_lpar_idnum_coloneq" @@ -224,8 +238,9 @@ GEXTEND Gram ; induction_arg: [ [ n = natural -> (None,ElimOnAnonHyp n) + | test_lpar_id_rpar; c = constr_with_bindings -> + (Some false,induction_arg_of_constr c) | c = constr_with_bindings -> (None,induction_arg_of_constr c) - | "!"; c = constr_with_bindings -> (Some false,induction_arg_of_constr c) ] ] ; constr_with_bindings_arg: diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml index 6ae519ef6..1112c3b89 100644 --- a/plugins/extraction/extraction.ml +++ b/plugins/extraction/extraction.ml @@ -734,7 +734,7 @@ and extract_cst_app env mle mlt kn u args = if la >= ls then (* Enough args, cleanup already done in [mla], we only add the - additionnal dummy if needed. *) + additional dummy if needed. *) put_magic_if (magic2 && not magic1) (mlapp head (optdummy @ mla)) else (* Partially applied function with some logical arg missing. @@ -748,7 +748,7 @@ and extract_cst_app env mle mlt kn u args = (*s Extraction of an inductive constructor applied to arguments. *) (* \begin{itemize} - \item In ML, contructor arguments are uncurryfied. + \item In ML, constructor arguments are uncurryfied. \item We managed to suppress logical parts inside inductive definitions, but they must appears outside (for partial applications for instance) \item We also suppressed all Coq parameters to the inductives, since diff --git a/plugins/funind/functional_principles_proofs.mli b/plugins/funind/functional_principles_proofs.mli index 61fce267a..34ce66967 100644 --- a/plugins/funind/functional_principles_proofs.mli +++ b/plugins/funind/functional_principles_proofs.mli @@ -8,7 +8,7 @@ val prove_princ_for_struct : val prove_principle_for_gen : - constant*constant*constant -> (* name of the function, the fonctionnal and the fixpoint equation *) + constant*constant*constant -> (* name of the function, the functional and the fixpoint equation *) constr option ref -> (* a pointer to the obligation proofs lemma *) bool -> (* is that function uses measure *) int -> (* the number of recursive argument *) diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index 60ff10922..5a30da336 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -205,7 +205,7 @@ let (declare_f : Id.t -> logical_kind -> constr list -> global_reference -> glob -(* Debuging mechanism *) +(* Debugging mechanism *) let debug_queue = Stack.create () let rec print_debug_queue b e = @@ -293,9 +293,9 @@ let tclUSER_if_not_mes concl_tac is_mes names_to_suppress = -(* Travelling term. +(* Traveling term. Both definitions of [f_terminate] and [f_equation] use the same generic - travelling mechanism. + traveling mechanism. *) (* [check_not_nested forbidden e] checks that [e] does not contains any variable @@ -329,7 +329,7 @@ let check_not_nested forbidden e = with UserError(_,p) -> errorlabstrm "_" (str "on expr : " ++ Printer.pr_lconstr e ++ str " " ++ p) -(* ['a info] contains the local information for travelling *) +(* ['a info] contains the local information for traveling *) type 'a infos = { nb_arg : int; (* function number of arguments *) concl_tac : tactic; (* final tactic to finish proofs *) @@ -339,7 +339,7 @@ type 'a infos = f_id : Id.t; (* function name *) f_constr : constr; (* function term *) f_terminate : constr; (* termination proof term *) - func : global_reference; (* functionnal reference *) + func : global_reference; (* functional reference *) info : 'a; is_main_branch : bool; (* on the main branch or on a matched expression *) is_final : bool; (* final first order term or not *) @@ -359,7 +359,7 @@ type ('a,'b) journey_info_tac = 'b infos -> (* argument of the tactic *) tactic -(* journey_info : specifies the actions to do on the different term constructors during the travelling of the term +(* journey_info : specifies the actions to do on the different term constructors during the traveling of the term *) type journey_info = { letiN : ((Name.t*constr*types*constr),constr) journey_info_tac; diff --git a/plugins/romega/refl_omega.ml b/plugins/romega/refl_omega.ml index 95407c5ff..560e6a899 100644 --- a/plugins/romega/refl_omega.ml +++ b/plugins/romega/refl_omega.ml @@ -46,7 +46,7 @@ let occ_step_eq s1 s2 = match s1, s2 with d'une liste de pas à partir de la racine de l'hypothèse *) type occurrence = {o_hyp : Names.Id.t; o_path : occ_path} -(* \subsection{refiable formulas} *) +(* \subsection{reifiable formulas} *) type oformula = (* integer *) | Oint of Bigint.bigint @@ -55,7 +55,7 @@ type oformula = | Omult of oformula * oformula | Ominus of oformula * oformula | Oopp of oformula - (* an atome in the environment *) + (* an atom in the environment *) | Oatom of int (* weird expression that cannot be translated *) | Oufo of oformula @@ -75,7 +75,7 @@ type oproposition = | Pimp of int * oproposition * oproposition | Pprop of Term.constr -(* Les équations ou proposiitions atomiques utiles du calcul *) +(* Les équations ou propositions atomiques utiles du calcul *) and oequation = { e_comp: comparaison; (* comparaison *) e_left: oformula; (* formule brute gauche *) @@ -1266,7 +1266,7 @@ let resolution env full_reified_goal systems_list = | (O_right :: l) -> app coq_p_right [| loop l |] in let correct_index = let i = List.index0 Names.Id.equal e.e_origin.o_hyp l_hyps in - (* PL: it seems that additionnally introduced hyps are in the way during + (* PL: it seems that additionally introduced hyps are in the way during normalization, hence this index shifting... *) if Int.equal i 0 then 0 else Pervasives.(+) i (List.length to_introduce) in diff --git a/plugins/setoid_ring/InitialRing.v b/plugins/setoid_ring/InitialRing.v index b92b847be..56023bfb5 100644 --- a/plugins/setoid_ring/InitialRing.v +++ b/plugins/setoid_ring/InitialRing.v @@ -155,7 +155,7 @@ Section ZMORPHISM. Ltac norm := gen_srewrite Rsth Reqe ARth. Ltac add_push := gen_add_push radd Rsth Reqe ARth. -(*morphisms are extensionaly equal*) +(*morphisms are extensionally equal*) Lemma same_genZ : forall x, [x] == gen_phiZ1 x. Proof. destruct x;simpl; try rewrite (same_gen ARth);rrefl. @@ -246,7 +246,7 @@ Proof (SRth_ARth Nsth Nth). Lemma Neqb_ok : forall x y, N.eqb x y = true -> x = y. Proof. exact (fun x y => proj1 (N.eqb_eq x y)). Qed. -(**Same as above : definition of two,extensionaly equal, generic morphisms *) +(**Same as above : definition of two, extensionally equal, generic morphisms *) (**from N to any semi-ring*) Section NMORPHISM. Variable R : Type. @@ -671,7 +671,7 @@ End GEN_DIV. end. (* A simple tactic recognizing only 0 and 1. The inv_gen_phiX above - are only optimisations that directly returns the reifid constant + are only optimisations that directly returns the reified constant instead of resorting to the constant propagation of the simplification algorithm. *) Ltac inv_gen_phi rO rI cO cI t := diff --git a/plugins/setoid_ring/Ncring_initial.v b/plugins/setoid_ring/Ncring_initial.v index c40e0ffba..c2eafcdad 100644 --- a/plugins/setoid_ring/Ncring_initial.v +++ b/plugins/setoid_ring/Ncring_initial.v @@ -42,7 +42,7 @@ Defined. (*Instance ZEquality: @Equality Z:= (@eq Z).*) -(** Two generic morphisms from Z to (abrbitrary) rings, *) +(** Two generic morphisms from Z to (arbitrary) rings, *) (**second one is more convenient for proofs but they are ext. equal*) Section ZMORPHISM. Context {R:Type}`{Ring R}. @@ -130,7 +130,7 @@ Ltac rsimpl := simpl. Qed. -(*morphisms are extensionaly equal*) +(*morphisms are extensionally equal*) Lemma same_genZ : forall x, [x] == gen_phiZ1 x. Proof. destruct x;rsimpl; try rewrite same_gen; reflexivity. diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml index ea705e335..663b8b810 100644 --- a/printing/ppconstr.ml +++ b/printing/ppconstr.ml @@ -638,13 +638,13 @@ end) = struct | CLetTuple (_,nal,(na,po),c,b) -> return ( hv 0 ( - keyword "let" ++ spc () ++ - hov 0 (str "(" ++ + hov 2 (keyword "let" ++ spc () ++ + hov 1 (str "(" ++ prlist_with_sep sep_v pr_lname nal ++ str ")" ++ - pr_simple_return_type (pr mt) na po ++ str " :=" ++ - pr spc ltop c ++ spc () - ++ keyword "in") ++ + pr_simple_return_type (pr mt) na po ++ str " :=") ++ + pr spc ltop c + ++ keyword " in") ++ pr spc ltop b), lletin ) diff --git a/tactics/rewrite.ml b/tactics/rewrite.ml index 9a19d4bda..2dfebc9a3 100644 --- a/tactics/rewrite.ml +++ b/tactics/rewrite.ml @@ -407,7 +407,7 @@ module TypeGlobal = struct let inverse env (evd,cstrs) car rel = - let evd, (sort,_) = Evarutil.new_type_evar env evd Evd.univ_flexible in + let evd, sort = Evarutil.new_Type ~rigid:Evd.univ_flexible env evd in app_poly_check env (evd,cstrs) coq_inverse [| car ; car; sort; rel |] end diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 539c2ab71..59a7168e5 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -3252,7 +3252,7 @@ let make_abstract_generalize env id typ concl dep ctx body c eqs args refls = mkProd (Anonymous, eq, lift 1 concl), [| refl |] else concl, [||] in - (* Abstract by equalitites *) + (* Abstract by equalities *) let eqs = lift_togethern 1 eqs in (* lift together and past genarg *) let abseqs = it_mkProd_or_LetIn (lift eqslen abshypeq) (List.map (fun x -> (Anonymous, None, x)) eqs) in (* Abstract by the "generalized" hypothesis. *) @@ -3263,11 +3263,11 @@ let make_abstract_generalize env id typ concl dep ctx body c eqs args refls = let Sigma (genc, sigma, p) = Evarutil.new_evar env sigma ~principal:true genctyp in (* Apply the old arguments giving the proper instantiation of the hyp *) let instc = mkApp (genc, Array.of_list args) in - (* Then apply to the original instanciated hyp. *) + (* Then apply to the original instantiated hyp. *) let instc = Option.cata (fun _ -> instc) (mkApp (instc, [| mkVar id |])) body in (* Apply the reflexivity proofs on the indices. *) let appeqs = mkApp (instc, Array.of_list refls) in - (* Finaly, apply the reflexivity proof for the original hyp, to get a term of type gl again. *) + (* Finally, apply the reflexivity proof for the original hyp, to get a term of type gl again. *) Sigma (mkApp (appeqs, abshypt), sigma, p) end } diff --git a/test-suite/Makefile b/test-suite/Makefile index 742395422..f333ae63e 100644 --- a/test-suite/Makefile +++ b/test-suite/Makefile @@ -352,7 +352,7 @@ $(addsuffix .log,$(wildcard ideal-features/*.v)): %.v.log: %.v fi; \ } > "$@" -# Additionnal dependencies for module tests +# Additional dependencies for module tests $(addsuffix .log,$(wildcard modules/*.v)): %.v.log: modules/Nat.vo modules/plik.vo modules/%.vo: modules/%.v $(HIDE)$(coqtop) -R modules Mods -compile $< diff --git a/test-suite/bugs/closed/4443.v b/test-suite/bugs/closed/4443.v new file mode 100644 index 000000000..66dfa0e68 --- /dev/null +++ b/test-suite/bugs/closed/4443.v @@ -0,0 +1,31 @@ +Set Universe Polymorphism. + +Record TYPE@{i} := cType { + type : Type@{i}; +}. + +Definition PROD@{i j k} + (A : Type@{i}) + (B : A -> Type@{j}) + : TYPE@{k}. +Proof. + refine (cType@{i} _). ++ refine (forall x : A, B x). +Defined. + +Local Unset Strict Universe Declaration. +Definition PRODinj + (A : Type@{i}) + (B : A -> Type) + : TYPE. +Proof. + refine (cType@{i} _). ++ refine (forall x : A, B x). +Defined. + + Monomorphic Universe i j. + Monomorphic Constraint j < i. +Set Printing Universes. +Check PROD@{i i i}. +Check PRODinj@{i j}. +Fail Check PRODinj@{j i}.
\ No newline at end of file diff --git a/test-suite/success/destruct.v b/test-suite/success/destruct.v index 59cd25cd7..9f091e399 100644 --- a/test-suite/success/destruct.v +++ b/test-suite/success/destruct.v @@ -389,7 +389,7 @@ Abort. Goal forall b:bool, True. intro b. -destruct !b. +destruct (b). clear b. (* b has to be here *) Abort. diff --git a/theories/FSets/FMapFacts.v b/theories/FSets/FMapFacts.v index 8c6f4b64a..eaeb2914b 100644 --- a/theories/FSets/FMapFacts.v +++ b/theories/FSets/FMapFacts.v @@ -2143,7 +2143,7 @@ Module OrdProperties (M:S). Section Fold_properties. (** The following lemma has already been proved on Weak Maps, - but with one additionnal hypothesis (some [transpose] fact). *) + but with one additional hypothesis (some [transpose] fact). *) Lemma fold_Equal : forall m1 m2 (A:Type)(eqA:A->A->Prop)(st:Equivalence eqA) (f:key->elt->A->A)(i:A), diff --git a/theories/FSets/FMapPositive.v b/theories/FSets/FMapPositive.v index 3eac15b03..9e59f0c50 100644 --- a/theories/FSets/FMapPositive.v +++ b/theories/FSets/FMapPositive.v @@ -1061,7 +1061,7 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits. End PositiveMap. -(** Here come some additionnal facts about this implementation. +(** Here come some additional facts about this implementation. Most are facts that cannot be derivable from the general interface. *) diff --git a/theories/MMaps/MMapFacts.v b/theories/MMaps/MMapFacts.v index 69066a7b6..8b356d750 100644 --- a/theories/MMaps/MMapFacts.v +++ b/theories/MMaps/MMapFacts.v @@ -2381,7 +2381,7 @@ Module OrdProperties (M:S). Section Fold_properties. (** The following lemma has already been proved on Weak Maps, - but with one additionnal hypothesis (some [transpose] fact). *) + but with one additional hypothesis (some [transpose] fact). *) Lemma fold_Equal : forall m1 m2 (A:Type)(eqA:A->A->Prop)(st:Equivalence eqA) (f:key->elt->A->A)(i:A), diff --git a/theories/MMaps/MMapPositive.v b/theories/MMaps/MMapPositive.v index d3aab2389..adbec7057 100644 --- a/theories/MMaps/MMapPositive.v +++ b/theories/MMaps/MMapPositive.v @@ -641,7 +641,7 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits. End PositiveMap. -(** Here come some additionnal facts about this implementation. +(** Here come some additional facts about this implementation. Most are facts that cannot be derivable from the general interface. *) Module PositiveMapAdditionalFacts. diff --git a/theories/Numbers/Integer/Abstract/ZDivEucl.v b/theories/Numbers/Integer/Abstract/ZDivEucl.v index d0df8fb4a..ab73ebfe1 100644 --- a/theories/Numbers/Integer/Abstract/ZDivEucl.v +++ b/theories/Numbers/Integer/Abstract/ZDivEucl.v @@ -391,7 +391,7 @@ rewrite <- (add_0_r (b*(a/b))) at 2. apply add_cancel_l. Qed. -(** Some additionnal inequalities about div. *) +(** Some additional inequalities about div. *) Theorem div_lt_upper_bound: forall a b q, 0<b -> a < b*q -> a/b < q. diff --git a/theories/Numbers/Integer/Abstract/ZDivFloor.v b/theories/Numbers/Integer/Abstract/ZDivFloor.v index d5f3f4ada..c8260e516 100644 --- a/theories/Numbers/Integer/Abstract/ZDivFloor.v +++ b/theories/Numbers/Integer/Abstract/ZDivFloor.v @@ -436,7 +436,7 @@ rewrite <- (add_0_r (b*(a/b))) at 2. apply add_cancel_l. Qed. -(** Some additionnal inequalities about div. *) +(** Some additional inequalities about div. *) Theorem div_lt_upper_bound: forall a b q, 0<b -> a < b*q -> a/b < q. diff --git a/theories/Numbers/Integer/Abstract/ZDivTrunc.v b/theories/Numbers/Integer/Abstract/ZDivTrunc.v index de2e99ec3..464fe354b 100644 --- a/theories/Numbers/Integer/Abstract/ZDivTrunc.v +++ b/theories/Numbers/Integer/Abstract/ZDivTrunc.v @@ -404,7 +404,7 @@ Proof. intros. rewrite rem_eq by order. rewrite sub_move_r; nzsimpl; tauto. Qed. -(** Some additionnal inequalities about quot. *) +(** Some additional inequalities about quot. *) Theorem quot_lt_upper_bound: forall a b q, 0<=a -> 0<b -> a < b*q -> a÷b < q. diff --git a/theories/Numbers/NatInt/NZDiv.v b/theories/Numbers/NatInt/NZDiv.v index 4a127216f..e0dfdedbd 100644 --- a/theories/Numbers/NatInt/NZDiv.v +++ b/theories/Numbers/NatInt/NZDiv.v @@ -307,7 +307,7 @@ rewrite <- (add_0_r (b*(a/b))) at 2. apply add_cancel_l. Qed. -(** Some additionnal inequalities about div. *) +(** Some additional inequalities about div. *) Theorem div_lt_upper_bound: forall a b q, 0<=a -> 0<b -> a < b*q -> a/b < q. diff --git a/theories/Numbers/Natural/Abstract/NDiv.v b/theories/Numbers/Natural/Abstract/NDiv.v index fb68c139b..d3d3eb0fb 100644 --- a/theories/Numbers/Natural/Abstract/NDiv.v +++ b/theories/Numbers/Natural/Abstract/NDiv.v @@ -137,7 +137,7 @@ Proof. intros; apply mul_succ_div_gt; auto'. Qed. Lemma div_exact : forall a b, b~=0 -> (a == b*(a/b) <-> a mod b == 0). Proof. intros. apply div_exact; auto'. Qed. -(** Some additionnal inequalities about div. *) +(** Some additional inequalities about div. *) Theorem div_lt_upper_bound: forall a b q, b~=0 -> a < b*q -> a/b < q. diff --git a/theories/Numbers/Natural/Abstract/NParity.v b/theories/Numbers/Natural/Abstract/NParity.v index b3526c9a1..80a579f19 100644 --- a/theories/Numbers/Natural/Abstract/NParity.v +++ b/theories/Numbers/Natural/Abstract/NParity.v @@ -8,7 +8,7 @@ Require Import Bool NSub NZParity. -(** Some additionnal properties of [even], [odd]. *) +(** Some additional properties of [even], [odd]. *) Module Type NParityProp (Import N : NAxiomsSig')(Import NP : NSubProp N). diff --git a/theories/Program/Subset.v b/theories/Program/Subset.v index 50b89b5c0..ce1f7768d 100644 --- a/theories/Program/Subset.v +++ b/theories/Program/Subset.v @@ -82,7 +82,7 @@ Qed. Definition match_eq (A B : Type) (x : A) (fn : {y : A | y = x} -> B) : B := fn (exist _ x eq_refl). -(* This is what we want to be able to do: replace the originaly matched object by a new, +(* This is what we want to be able to do: replace the originally matched object by a new, propositionally equal one. If [fn] works on [x] it should work on any [y | y = x]. *) Lemma match_eq_rewrite : forall (A B : Type) (x : A) (fn : {y : A | y = x} -> B) diff --git a/theories/Structures/EqualitiesFacts.v b/theories/Structures/EqualitiesFacts.v index 8e2b2d081..d5827d87a 100644 --- a/theories/Structures/EqualitiesFacts.v +++ b/theories/Structures/EqualitiesFacts.v @@ -60,7 +60,7 @@ Module KeyDecidableType(D:DecidableType). Hint Resolve eqke_1 eqke_2 eqk_1. - (* Additionnal facts *) + (* Additional facts *) Lemma InA_eqke_eqk {elt} p (m:list (key*elt)) : InA eqke p m -> InA eqk p m. diff --git a/theories/Structures/OrderedType.v b/theories/Structures/OrderedType.v index cc8c2261b..93ca383b2 100644 --- a/theories/Structures/OrderedType.v +++ b/theories/Structures/OrderedType.v @@ -342,7 +342,7 @@ Module KeyOrderedType(O:OrderedType). compute in Hxx'; compute in Hyy'. rewrite Hxx', Hyy'; auto. Qed. - (* Additionnal facts *) + (* Additional facts *) Lemma eqk_not_ltk : forall x x', eqk x x' -> ~ltk x x'. Proof. diff --git a/theories/Structures/OrdersLists.v b/theories/Structures/OrdersLists.v index 4d49ac84e..41e65d728 100644 --- a/theories/Structures/OrdersLists.v +++ b/theories/Structures/OrdersLists.v @@ -76,7 +76,7 @@ Module KeyOrderedType(O:OrderedType). Instance ltk_compat' {elt} : Proper (eqke==>eqke==>iff) (@ltk elt). Proof. eapply subrelation_proper; eauto with *. Qed. - (* Additionnal facts *) + (* Additional facts *) Instance pair_compat {elt} : Proper (O.eq==>Logic.eq==>eqke) (@pair key elt). Proof. apply pair_compat. Qed. diff --git a/theories/ZArith/Zdiv.v b/theories/ZArith/Zdiv.v index d0d10891a..363b4fd03 100644 --- a/theories/ZArith/Zdiv.v +++ b/theories/ZArith/Zdiv.v @@ -279,7 +279,7 @@ Proof. intros; rewrite Z.div_exact; auto. Qed. Theorem Zmod_le: forall a b, 0 < b -> 0 <= a -> a mod b <= a. Proof. intros. apply Z.mod_le; auto. Qed. -(** Some additionnal inequalities about Z.div. *) +(** Some additional inequalities about Z.div. *) Theorem Zdiv_lt_upper_bound: forall a b q, 0 < b -> a < q*b -> a/b < q. diff --git a/theories/ZArith/Zpow_alt.v b/theories/ZArith/Zpow_alt.v index 8f661a9c8..c8627477b 100644 --- a/theories/ZArith/Zpow_alt.v +++ b/theories/ZArith/Zpow_alt.v @@ -11,7 +11,7 @@ Local Open Scope Z_scope. (** An alternative power function for Z *) -(** This [Zpower_alt] is extensionnaly equal to [Z.pow], +(** This [Zpower_alt] is extensionally equal to [Z.pow], but not convertible with it. The number of multiplications is logarithmic instead of linear, but these multiplications are bigger. Experimentally, it seems diff --git a/theories/ZArith/Zquot.v b/theories/ZArith/Zquot.v index 3ef111898..6db92edb7 100644 --- a/theories/ZArith/Zquot.v +++ b/theories/ZArith/Zquot.v @@ -243,7 +243,7 @@ Proof. intros. zero_or_not b. intuition. apply Z.quot_exact; auto. Qed. Theorem Zrem_le a b : 0 <= a -> 0 <= b -> Z.rem a b <= a. Proof. intros. zero_or_not b. apply Z.rem_le; auto with zarith. Qed. -(** Some additionnal inequalities about Zdiv. *) +(** Some additional inequalities about Zdiv. *) Theorem Zquot_le_upper_bound: forall a b q, 0 < b -> a <= q*b -> a÷b <= q. |