diff options
| -rwxr-xr-x | doc/common/macros.tex | 4 | ||||
| -rw-r--r-- | doc/refman/RefMan-lib.tex | 184 | ||||
| -rw-r--r-- | doc/refman/RefMan-oth.tex | 2 | ||||
| -rw-r--r-- | tactics/equality.ml | 12 | ||||
| -rw-r--r-- | test-suite/bugs/closed/shouldsucceed/2021.v | 23 | ||||
| -rw-r--r-- | theories/Arith/Max.v | 4 |
6 files changed, 136 insertions, 93 deletions
diff --git a/doc/common/macros.tex b/doc/common/macros.tex index 89b7350f3..c27a3357e 100755 --- a/doc/common/macros.tex +++ b/doc/common/macros.tex @@ -47,7 +47,7 @@ \newcommand{\Rem}{\medskip \noindent {\bf Remark: }} \newcommand{\Rems}{\medskip \noindent {\bf Remarks: }} \newcommand{\Example}{\medskip \noindent {\bf Example: }} -\newcommand{\Examples}{\medskip \noindent {\bf Examples: }} +\newcommand{\examples}{\medskip \noindent {\bf Examples: }} \newcommand{\Warning}{\medskip \noindent {\bf Warning: }} \newcommand{\Warns}{\medskip \noindent {\bf Warnings: }} \newcounter{ex} @@ -61,6 +61,8 @@ \newenvironment{ErrMsgs}{\ErrMsgx\begin{enumerate}}{\end{enumerate}} \newenvironment{Remarks}{\Rems\begin{enumerate}}{\end{enumerate}} \newenvironment{Warnings}{\Warns\begin{enumerate}}{\end{enumerate}} +\newenvironment{Examples}{\medskip\noindent{\bf Examples:} +\begin{enumerate}}{\end{enumerate}} %\newcommand{\bd}{\noindent\bf} %\newcommand{\sbd}{\vspace{8pt}\noindent\bf} diff --git a/doc/refman/RefMan-lib.tex b/doc/refman/RefMan-lib.tex index 06da955d5..5cbe9c61b 100644 --- a/doc/refman/RefMan-lib.tex +++ b/doc/refman/RefMan-lib.tex @@ -1,10 +1,10 @@ \chapter[The {\Coq} library]{The {\Coq} library\index{Theories}\label{Theories}} -The \Coq\ library is structured into three parts: +The \Coq\ library is structured into two parts: \begin{description} \item[The initial library:] it contains - elementary logical notions and datatypes. It constitutes the + elementary logical notions and data-types. It constitutes the basic state of the system directly available when running \Coq; @@ -13,14 +13,14 @@ The \Coq\ library is structured into three parts: sorting, arithmetic, etc. This library comes with the system and its modules are directly accessible through the \verb!Require! command (see Section~\ref{Require}); - -\item[User contributions:] Other specification and proof developments - coming from the \Coq\ users' community. These libraries are - available for download at \texttt{http://coq.inria.fr} (see - Section~\ref{Contributions}). \end{description} -This chapter briefly reviews these libraries. +In addition, user-provided libraries or developments are provided by +\Coq\ users' community. These libraries and developments are available +for download at \texttt{http://coq.inria.fr} (see +Section~\ref{Contributions}). + +The chapter briefly reviews the \Coq\ libraries. \section[The basic library]{The basic library\label{Prelude}} @@ -34,16 +34,18 @@ root directory; this includes the modules {\tt Datatypes}, {\tt Specif}, {\tt Peano}, -and {\tt Wf}. +{\tt Wf} and +{\tt Tactics}. Module {\tt Logic\_Type} also makes it in the initial state}. \subsection[Notations]{Notations\label{Notations}} This module defines the parsing and pretty-printing of many symbols -(infixes, prefixes, etc.). However, it does not assign a meaning to these -notations. The purpose of this is to define precedence and -associativity of very common notations, and avoid users to use them -with other precedence, which may be confusing. +(infixes, prefixes, etc.). However, it does not assign a meaning to +these notations. The purpose of this is to define and fix once for all +the precedence and associativity of very common notations. The main +notations fixed in the initial state are listed on +Figure~\ref{init-notations}. \begin{figure} \begin{center} @@ -69,8 +71,10 @@ Notation & Precedence & Associativity \\ \verb!_ <= _ < _! & 70 & no \\ \verb!_ <= _ <= _! & 70 & no \\ \verb!_ + _! & 50 & left \\ +\verb!_ || _! & 50 & left \\ \verb!_ - _! & 50 & left \\ \verb!_ * _! & 40 & left \\ +\verb!_ && _! & 40 & left \\ \verb!_ / _! & 40 & left \\ \verb!- _! & 35 & right \\ \verb!/ _! & 35 & right \\ @@ -202,14 +206,14 @@ The following abbreviations are allowed: \end{tabular} \end{center} -The type annotation \texttt{:A} can be omitted when \texttt{A} can be +The type annotation ``\texttt{:A}'' can be omitted when \texttt{A} can be synthesized by the system. \subsubsection[Equality]{Equality\label{Equality} \index{Equality}} Then, we find equality, defined as an inductive relation. That is, -given a \verb:Type: \verb:A: and an \verb:x: of type \verb:A:, the +given a type \verb:A: and an \verb:x: of type \verb:A:, the predicate \verb:(eq A x): is the smallest one which contains \verb:x:. This definition, due to Christine Paulin-Mohring, is equivalent to define \verb:eq: as the smallest reflexive relation, and it is also @@ -309,14 +313,14 @@ Abort. & $|$ & {\tt \{} {\ident} {\tt :} {\specif} {\tt |} {\form} {\tt \&} {\form} {\tt \}} & ({\tt sig2})\\ & $|$ & {\tt \{} {\ident} {\tt :} {\specif} {\tt \&} {\specif} {\tt - \}} & ({\tt sigS})\\ + \}} & ({\tt sigT})\\ & $|$ & {\tt \{} {\ident} {\tt :} {\specif} {\tt \&} {\specif} {\tt - \&} {\specif} {\tt \}} & ({\tt sigS2})\\ + \&} {\specif} {\tt \}} & ({\tt sigT2})\\ & & & \\ {\term} & ::= & {\tt (} {\term} {\tt ,} {\term} {\tt )} & ({\tt pair}) \end{tabular} \end{centerframe} -\caption{Syntax of datatypes and specifications} +\caption{Syntax of data-types and specifications} \label{specif-syntax} \end{figure} @@ -355,8 +359,9 @@ Inductive identity (A:Type) (a:A) : A -> Type := Note that zero is the letter \verb:O:, and {\sl not} the numeral \verb:0:. -{\tt identity} is logically equivalent to equality but it lives in -sort {\tt Set}. Computationaly, it behaves like {\tt unit}. +The predicate {\tt identity} is logically +equivalent to equality but it lives in sort {\tt + Type}. It is mainly maintained for compatibility. We then define the disjoint sum of \verb:A+B: of two sets \verb:A: and \verb:B:, and their product \verb:A*B:. @@ -386,24 +391,27 @@ Definition snd (H: prod A B) := match H with End projections. \end{coq_example*} +Some operations on {\tt bool} are also provided: {\tt andb} (with +infix notation {\tt \&\&}), {\tt orb} (with +infix notation {\tt ||}), {\tt xorb}, {\tt implb} and {\tt negb}. + \subsection{Specification} The following notions\footnote{They are defined in module {\tt -Specif.v}} allows to build new datatypes and specifications. +Specif.v}} allow to build new data-types and specifications. They are available with the syntax shown on -Figure~\ref{specif-syntax}\footnote{This syntax can be found in the module -{\tt SpecifSyntax.v}}. +Figure~\ref{specif-syntax}. -For instance, given \verb|A:Set| and \verb|P:A->Prop|, the construct +For instance, given \verb|A:Type| and \verb|P:A->Prop|, the construct \verb+{x:A | P x}+ (in abstract syntax \verb+(sig A P)+) is a -\verb:Set:. We may build elements of this set as \verb:(exist x p): +\verb:Type:. We may build elements of this set as \verb:(exist x p): whenever we have a witness \verb|x:A| with its justification \verb|p:P x|. From such a \verb:(exist x p): we may in turn extract its witness \verb|x:A| (using an elimination construct such as \verb:match:) but {\sl not} its justification, which stays hidden, like in an abstract -data type. In technical terms, one says that \verb:sig: is a ``weak +data-type. In technical terms, one says that \verb:sig: is a ``weak (dependent) sum''. A variant \verb:sig2: with two predicates is also provided. @@ -420,32 +428,32 @@ Inductive sig2 (A:Set) (P Q:A -> Prop) : Set := exist2 (x:A) (_:P x) (_:Q x). \end{coq_example*} -A ``strong (dependent) sum'' \verb+{x:A & (P x)}+ may be also defined, -when the predicate \verb:P: is now defined as a \verb:Set: -constructor. +A ``strong (dependent) sum'' \verb+{x:A & P x}+ may be also defined, +when the predicate \verb:P: is now defined as a +constructor of types in \verb:Type:. \ttindex{\{x:A \& (P x)\}} \ttindex{\&} -\ttindex{sigS} -\ttindex{existS} -\ttindex{projS1} -\ttindex{projS2} -\ttindex{sigS2} -\ttindex{existS2} +\ttindex{sigT} +\ttindex{existT} +\ttindex{projT1} +\ttindex{projT2} +\ttindex{sigT2} +\ttindex{existT2} \begin{coq_example*} -Inductive sigS (A:Set) (P:A -> Set) : Set := existS (x:A) (_:P x). -Section sigSprojections. -Variable A : Set. -Variable P : A -> Set. -Definition projS1 (H:sigS A P) := let (x, h) := H in x. -Definition projS2 (H:sigS A P) := - match H return P (projS1 H) with - existS x h => h +Inductive sigT (A:Type) (P:A -> Type) : Type := existT (x:A) (_:P x). +Section Projections. +Variable A : Type. +Variable P : A -> Type. +Definition projT1 (H:sigT A P) := let (x, h) := H in x. +Definition projT2 (H:sigT A P) := + match H return P (projT1 H) with + existT x h => h end. -End sigSprojections. -Inductive sigS2 (A: Set) (P Q:A -> Set) : Set := - existS2 (x:A) (_:P x) (_:Q x). +End Projections. +Inductive sigT2 (A: Type) (P Q:A -> Type) : Type := + existT2 (x:A) (_:P x) (_:Q x). \end{coq_example*} A related non-dependent construct is the constructive sum @@ -461,7 +469,7 @@ Inductive sumbool (A B:Prop) : Set := left (_:A) | right (_:B). \end{coq_example*} This \verb"sumbool" construct may be used as a kind of indexed boolean -data type. An intermediate between \verb"sumbool" and \verb"sum" is +data-type. An intermediate between \verb"sumbool" and \verb"sum" is the mixed \verb"sumor" which combines \verb"A:Set" and \verb"B:Prop" in the \verb"Set" \verb"A+{B}". \ttindex{sumor} @@ -500,7 +508,7 @@ Abort. Abort. \end{coq_eval} -The next constructs builds a sum between a data type \verb|A:Set| and +The next construct builds a sum between a data-type \verb|A:Type| and an exceptional value encoding errors: \ttindex{Exc} @@ -515,23 +523,20 @@ Definition error := None. This module ends with theorems, -relating the sorts \verb:Set: and +relating the sorts \verb:Set: or \verb:Type: and \verb:Prop: in a way which is consistent with the realizability interpretation. +\ttindex{False\_rect} \ttindex{False\_rec} -\ttindex{eq\_rec} -\ttindex{Except} +\ttindex{eq\_rect} \ttindex{absurd\_set} -\ttindex{and\_rec} +\ttindex{and\_rect} -%Lemma False_rec : (P:Set)False->P. -%Lemma False_rect : (P:Type)False->P. \begin{coq_example*} Definition except := False_rec. -Notation Except := (except _). Theorem absurd_set : forall (A:Prop) (C:Set), A -> ~ A -> C. -Theorem and_rec : - forall (A B:Prop) (P:Set), (A -> B -> P) -> A /\ B -> P. +Theorem and_rect : + forall (A B:Prop) (P:Type), (A -> B -> P) -> A /\ B -> P. \end{coq_example*} %\begin{coq_eval} %Abort. @@ -544,7 +549,7 @@ The basic library includes a few elementary properties of natural numbers, together with the definitions of predecessor, addition and multiplication\footnote{This is in module {\tt Peano.v}}. It also provides a scope {\tt nat\_scope} gathering standard notations for -common operations (+,*) and a decimal notation for numbers. That is he +common operations (+, *) and a decimal notation for numbers. That is he can write \texttt{3} for \texttt{(S (S (S O)))}. This also works on the left hand side of a \texttt{match} expression (see for example section~\ref{refine-example}). This scope is opened by default. @@ -618,10 +623,11 @@ Abort All. Fixpoint plus (n m:nat) {struct n} : nat := match n with | 0 => m - | S p => S (plus p m) + | S p => S (p + m) end. -Lemma plus_n_O : forall n:nat, n = plus n 0. -Lemma plus_n_Sm : forall n m:nat, S (plus n m) = plus n (S m). +where "n + m" := (plus n m) : nat_scope. +Lemma plus_n_O : forall n:nat, n = n + 0. +Lemma plus_n_Sm : forall n m:nat, S (n + m) = n + S m. \end{coq_example*} \begin{coq_eval} Abort All. @@ -630,10 +636,11 @@ Abort All. Fixpoint mult (n m:nat) {struct n} : nat := match n with | 0 => 0 - | S p => m + mult p m + | S p => m + p * m end. -Lemma mult_n_O : forall n:nat, 0 = mult n 0. -Lemma mult_n_Sm : forall n m:nat, plus (mult n m) n = mult n (S m). +where "n * m" := (mult n m) : nat_scope. +Lemma mult_n_O : forall n:nat, 0 = n * 0. +Lemma mult_n_Sm : forall n m:nat, n * m + n = n * (S m). \end{coq_example*} \begin{coq_eval} Abort All. @@ -651,8 +658,8 @@ Finally, it gives the definition of the usual orderings \verb:le:, \begin{coq_example*} Inductive le (n:nat) : nat -> Prop := | le_n : le n n - | le_S : forall m:nat, le n m -> le n (S m). -Infix "+" := plus : nat_scope. + | le_S : forall m:nat, n <= m -> n <= (S m). +where "n <= m" := (le n m) : nat_scope. Definition lt (n m:nat) := S n <= m. Definition ge (n m:nat) := m <= n. Definition gt (n m:nat) := m < n. @@ -693,31 +700,32 @@ well-founded induction\footnote{This is defined in module {\tt Wf.v}}. \index{Well founded induction} \ttindex{Acc} \ttindex{Acc\_inv} -\ttindex{Acc\_rec} +\ttindex{Acc\_rect} \ttindex{well\_founded} \begin{coq_example*} Section Well_founded. -Variable A : Set. +Variable A : Type. Variable R : A -> A -> Prop. -Inductive Acc : A -> Prop := - Acc_intro : forall x:A, (forall y:A, R y x -> Acc y) -> Acc x. -Lemma Acc_inv : forall x:A, Acc x -> forall y:A, R y x -> Acc y. +Inductive Acc (x:A) : Prop := + Acc_intro : (forall y:A, R y x -> Acc y) -> Acc x. +Lemma Acc_inv : Acc x -> forall y:A, R y x -> Acc y. \end{coq_example*} \begin{coq_eval} -simple destruct 1; trivial. +destruct 1; trivial. Defined. \end{coq_eval} +%% Acc_rect now primitively defined +%% Section AccRec. +%% Variable P : A -> Set. +%% Variable F : +%% forall x:A, +%% (forall y:A, R y x -> Acc y) -> (forall y:A, R y x -> P y) -> P x. +%% Fixpoint Acc_rec (x:A) (a:Acc x) {struct a} : P x := +%% F x (Acc_inv x a) +%% (fun (y:A) (h:R y x) => Acc_rec y (Acc_inv x a y h)). +%% End AccRec. \begin{coq_example*} -Section AccRec. -Variable P : A -> Set. -Variable F : - forall x:A, - (forall y:A, R y x -> Acc y) -> (forall y:A, R y x -> P y) -> P x. -Fixpoint Acc_rec (x:A) (a:Acc x) {struct a} : P x := - F x (Acc_inv x a) - (fun (y:A) (h:R y x) => Acc_rec y (Acc_inv x a y h)). -End AccRec. Definition well_founded := forall a:A, Acc a. Hypothesis Rwf : well_founded. Theorem well_founded_induction : @@ -730,7 +738,8 @@ Theorem well_founded_ind : \begin{coq_eval} Abort All. \end{coq_eval} -{\tt Acc\_rec} can be used to define functions by fixpoints using +The automatically generated scheme {\tt Acc\_rect} +can be used to define functions by fixpoints using well-founded relations to justify termination. Assuming extensionality of the functional used for the recursive call, the fixpoint equation can be proved. @@ -740,7 +749,7 @@ fixpoint equation can be proved. \ttindex{Fix\_F\_eq} \begin{coq_example*} Section FixPoint. -Variable P : A -> Set. +Variable P : A -> Type. Variable F : forall x:A, (forall y:A, R y x -> P y) -> P x. Fixpoint Fix_F (x:A) (r:Acc x) {struct r} : P x := F x (fun (y:A) (p:R y x) => Fix_F y (Acc_inv x r y p)). @@ -765,7 +774,7 @@ End Well_founded. \subsection{Accessing the {\Type} level} The basic library includes the definitions\footnote{This is in module -{\tt Logic\_Type.v}} of the counterparts of some datatypes and logical +{\tt Logic\_Type.v}} of the counterparts of some data-types and logical quantifiers at the \verb:Type: level: negation, pair, and properties of {\tt identity}. @@ -780,8 +789,12 @@ Definition notT (A:Type) := A -> False. Inductive prodT (A B:Type) : Type := pairT (_:A) (_:B). \end{coq_example*} +At the end, it defines data-types at the {\Type} level. + +\subsection{Tactics} -At the end, it defines datatypes at the {\Type} level. +A few tactics defined at the user level are provided in the initial +state\footnote{This is in module {\tt Tactics.v}}. \section{The standard library} @@ -795,6 +808,7 @@ subdirectories: {\bf Arith} & Basic Peano arithmetic \\ {\bf NArith} & Basic positive integer arithmetic \\ {\bf ZArith} & Basic relative integer arithmetic \\ + {\bf Numbers} & Various approaches to natural, integer and cyclic numbers (currently axiomatically and on top of 2$^{31}$ binary words) \\ {\bf Bool} & Booleans (basic functions and results) \\ {\bf Lists} & Monomorphic and polymorphic lists (basic functions and results), Streams (infinite sequences defined with co-inductive diff --git a/doc/refman/RefMan-oth.tex b/doc/refman/RefMan-oth.tex index 3168f7737..dfb77e798 100644 --- a/doc/refman/RefMan-oth.tex +++ b/doc/refman/RefMan-oth.tex @@ -197,7 +197,7 @@ This restricts the search to constructions not defined in modules \end{Variants} -\Examples +\examples \begin{coq_example*} Require Import ZArith. diff --git a/tactics/equality.ml b/tactics/equality.ml index cdc096e84..259f51ad1 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -457,8 +457,9 @@ let injectable env sigma t1 t2 = let descend_then sigma env head dirn = let IndType (indf,_) = try find_rectype env sigma (get_type_of env sigma head) - with Not_found -> assert false in - let ind,_ = dest_ind_family indf in + with Not_found -> + error "Cannot project on an inductive type derived from a dependency." in + let ind,_ = dest_ind_family indf in let (mib,mip) = lookup_mind_specif env ind in let cstr = get_constructors env indf in let dirn_nlams = cstr.(dirn-1).cs_nargs in @@ -477,7 +478,7 @@ let descend_then sigma env head dirn = (interval 1 (Array.length mip.mind_consnames)) in let ci = make_case_info env ind RegularStyle in mkCase (ci, p, head, Array.of_list brl))) - + (* Now we need to construct the discriminator, given a discriminable position. This boils down to: @@ -828,11 +829,14 @@ let make_iterated_tuple env sigma dflt (z,zty) = let rec build_injrec sigma env dflt c = function | [] -> make_iterated_tuple env sigma dflt (c,type_of env sigma c) | ((sp,cnum),argnum)::l -> + try let (cnum_nlams,cnum_env,kont) = descend_then sigma env c cnum in let newc = mkRel(cnum_nlams-argnum) in let (subval,tuplety,dfltval) = build_injrec sigma cnum_env dflt newc l in (kont subval (dfltval,tuplety), - tuplety,dfltval) + tuplety,dfltval) + with + UserError _ -> failwith "caught" let build_injector sigma env dflt c cpath = let (injcode,resty,_) = build_injrec sigma env dflt c cpath in diff --git a/test-suite/bugs/closed/shouldsucceed/2021.v b/test-suite/bugs/closed/shouldsucceed/2021.v new file mode 100644 index 000000000..e598e5aed --- /dev/null +++ b/test-suite/bugs/closed/shouldsucceed/2021.v @@ -0,0 +1,23 @@ +(* correct failure of injection/discriminate on types whose inductive + status derives from the substitution of an argument *) + +Inductive t : nat -> Type := +| M : forall n: nat, nat -> t n. + +Lemma eq_t : forall n n' m m', + existT (fun B : Type => B) (t n) (M n m) = + existT (fun B : Type => B) (t n') (M n' m') -> True. +Proof. + intros. + injection H. + intro Ht. + exact I. +Qed. + +Lemma eq_t' : forall n n' : nat, + existT (fun B : Type => B) (t n) (M n 0) = + existT (fun B : Type => B) (t n') (M n' 1) -> True. +Proof. + intros. + discriminate H || exact I. +Qed. diff --git a/theories/Arith/Max.v b/theories/Arith/Max.v index 75e1cdf0c..52beecb74 100644 --- a/theories/Arith/Max.v +++ b/theories/Arith/Max.v @@ -74,13 +74,13 @@ Lemma max_dec : forall n m, {max n m = n} + {max n m = m}. Proof. induction n; induction m; simpl in |- *; auto with arith. elim (IHn m); intro H; elim H; auto. -Qed. +Defined. Lemma max_case : forall n m (P:nat -> Type), P n -> P m -> P (max n m). Proof. induction n; simpl in |- *; auto with arith. induction m; intros; simpl in |- *; auto with arith. pattern (max n m) in |- *; apply IHn; auto with arith. -Qed. +Defined. Notation max_case2 := max_case (only parsing). |