aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Arith/Peano_dec.v
Commit message (Collapse)AuthorAge
* Merge PR #6855: Update headers following #6543.Gravatar Maxime Dénès2018-03-05
|\
* | Remove the deprecation for some 8.2-8.5 compatibility aliases.Gravatar Théo Zimmermann2018-03-02
| | | | | | | | | | | | | | | | | | | | This was decided during the Fall WG (2017). The aliases that are kept as deprecated are the ones where the difference is only a prefix becoming a qualified module name. The intention is to turn the warning for deprecated notations on. We change the compat version to 8.6 to allow the removal of VOld and V8_5.
| * Update headers following #6543.Gravatar Théo Zimmermann2018-02-27
|/
* Ensuring all .v files end with a newline to make "sed -i" work better on them.Gravatar Hugo Herbelin2017-08-21
|
* Bump year in headers.Gravatar Pierre-Marie Pédrot2017-07-04
|
* Giving a more natural semantics to injection by default.Gravatar Hugo Herbelin2016-06-18
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | There were three versions of injection: 1. "injection term" without "as" clause: was leaving hypotheses on the goal in reverse order 2. "injection term as ipat", first version: was introduction hypotheses using ipat in reverse order without checking that the number of ipat was the size of the injection (activated with "Unset Injection L2R Pattern Order") 3. "injection term as ipat", second version: was introduction hypotheses using ipat in left-to-right order checking that the number of ipat was the size of the injection and clearing the injecting term by default if an hypothesis (activated with "Set Injection L2R Pattern Order", default one from 8.5) There is now: 4. "injection term" without "as" clause, new version: introducing the components of the injection in the context in left-to-right order using default intro-patterns "?" and clearing the injecting term by default if an hypothesis (activated with "Set Structural Injection") The new versions 3. and 4. are the "expected" ones in the sense that they have the following good properties: - introduction in the context is in the natural left-to-right order - "injection" behaves the same with and without "as", always introducing the hypotheses in the goal what corresponds to the natural expectation as the changes I made in the proof scripts for adaptation confirm - clear the "injection" hypothesis when an hypothesis which is the natural expectation as the changes I made in the proof scripts for adaptation confirm The compatibility can be preserved by "Unset Structural Injection" or by calling "simple injection". The flag is currently off.
* Update copyright headers.Gravatar Maxime Dénès2016-01-20
|
* Update headers.Gravatar Maxime Dénès2015-01-12
|
* Fixed proof of irrelevance of le on nat, inspired by theGravatar Maxime Dénès2014-07-22
| | | | corresponding proof in ssreflect.
* Arith: full integration of the "Numbers" modular frameworkGravatar Pierre Letouzey2014-07-09
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | - The earlier proof-of-concept file NPeano (which instantiates the "Numbers" framework for nat) becomes now the entry point in the Arith lib, and gets renamed PeanoNat. It still provides an inner module "Nat" which sums up everything about type nat (functions, predicates and properties of them). This inner module Nat is usable as soon as you Require Import Arith, or just Arith_base, or simply PeanoNat. - Definitions of operations over type nat are now grouped in a new file Init/Nat.v. This file is meant to be used without "Import", hence providing for instance Nat.add or Nat.sqrt as soon as coqtop starts (but no proofs about them). - The definitions that used to be in Init/Peano.v (pred, plus, minus, mult) are now compatibility notations (for Nat.pred, Nat.add, Nat.sub, Nat.mul where here Nat is Init/Nat.v). - This Coq.Init.Nat module (with only pure definitions) is Include'd in the aforementioned Coq.Arith.PeanoNat.Nat. You might see Init.Nat sometimes instead of just Nat (for instance when doing "Print plus"). Normally it should be ok to just ignore these "Init" since Init.Nat is included in the full PeanoNat.Nat. I'm investigating if it's possible to get rid of these "Init" prefixes. - Concerning predicates, orders le and lt are still defined in Init/Peano.v, with their notations "<=" and "<". Properties in PeanoNat.Nat directly refer to these predicates in Peano. For instantation reasons, PeanoNat.Nat also contains a Nat.le and Nat.lt (defined via "Definition le := Peano.le", we cannot yet include an Inductive to implement a Parameter), but these aliased predicates won't probably be very convenient to use. - Technical remark: I've split the previous property functor NProp in two parts (NBasicProp and NExtraProp), it helps a lot for building PeanoNat.Nat incrementally. Roughly speaking, we have the following schema: Module Nat. Include Coq.Init.Nat. (* definition of operations : add ... sqrt ... *) ... (** proofs of specifications for basic ops such as + * - *) Include NBasicProp. (** generic properties of these basic ops *) ... (** proofs of specifications for advanced ops (pow sqrt log2...) that may rely on proofs for + * - *) Include NExtraProp. (** all remaining properties *) End Nat. - All other files in directory Arith are now taking advantage of PeanoNat : they are now filled with compatibility notations (when earlier lemmas have exact counterpart in the Nat module) or lemmas with one-line proofs based on the Nat module. All hints for database "arith" remain declared in these old-style file (such as Plus.v, Lt.v, etc). All the old-style files are still Require'd (or not) by Arith.v, just as before. - Compatibility should be almost complete. For instance in the stdlib, the only adaptations were due to .ml code referring to some Coq constant name such as Coq.Init.Peano.pred, which doesn't live well with the new compatibility notations.
* Unset Asymmetric PatternsGravatar pboutill2013-01-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16129 85f007b7-540e-0410-9357-904b9bb8a0f7
* Updating headers.Gravatar herbelin2012-08-08
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15715 85f007b7-540e-0410-9357-904b9bb8a0f7
* Kills the useless tactic annotations "in |- *"Gravatar letouzey2012-07-05
| | | | | | | Most of these heavyweight annotations were introduced a long time ago by the automatic 7.x -> 8.0 translator git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15518 85f007b7-540e-0410-9357-904b9bb8a0f7
* Open Local Scope ---> Local Open Scope, same with Notation and aliiGravatar letouzey2012-07-05
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15517 85f007b7-540e-0410-9357-904b9bb8a0f7
* First release of Vector library.Gravatar pboutill2010-12-10
| | | | | | | | | | To avoid names&notations clashs with list, Vector shouldn't be "Import"ed but one can "Import Vector.VectorNotations." to have notations. SetoidVector at least remains to do. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13702 85f007b7-540e-0410-9357-904b9bb8a0f7
* Updated all headers for 8.3 and trunkGravatar herbelin2010-07-24
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13323 85f007b7-540e-0410-9357-904b9bb8a0f7
* Remove the svn-specific $Id$ annotationsGravatar letouzey2010-04-29
| | | | | | | | | | | - Many of them were broken, some of them after Pierre B's rework of mli for ocamldoc, but not only (many bad annotation, many files with no svn property about Id, etc) - Useless for those of us that work with git-svn (and a fortiori in a forthcoming git-only setting) - Even in svn, they seem to be of little interest git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12972 85f007b7-540e-0410-9357-904b9bb8a0f7
* Proof simplification for eq_nat_dec et le_lt_dec: induction over Gravatar letouzey2007-03-12
| | | | | | | | | 2nd arg m can simply be a destruct. This helps (vm_)compute __a lot__. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9698 85f007b7-540e-0410-9357-904b9bb8a0f7
* Mise en forme des theoriesGravatar notin2006-10-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9245 85f007b7-540e-0410-9357-904b9bb8a0f7
* Modification des propriétés (svn:executable)Gravatar notin2006-03-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8642 85f007b7-540e-0410-9357-904b9bb8a0f7
* Nouvelle en-têteGravatar herbelin2004-07-16
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5920 85f007b7-540e-0410-9357-904b9bb8a0f7
* Remplacement des fichiers .v ancienne syntaxe de theories, contrib et states ↵Gravatar herbelin2003-11-29
| | | | | | par les fichiers nouvelle syntaxe git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5027 85f007b7-540e-0410-9357-904b9bb8a0f7
* Suppression de l'étage "Import nat/Z/R_scope". "Open Scope" remplace "Import".Gravatar herbelin2003-04-09
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3877 85f007b7-540e-0410-9357-904b9bb8a0f7
* Implicit Variables TypeGravatar herbelin2003-03-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3809 85f007b7-540e-0410-9357-904b9bb8a0f7
* *** empty log message ***Gravatar barras2003-03-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3761 85f007b7-540e-0410-9357-904b9bb8a0f7
* TransparentGravatar barras2001-09-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2035 85f007b7-540e-0410-9357-904b9bb8a0f7
* Expérimentation de NewDestruct et parfois NewInductionGravatar herbelin2001-08-05
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1880 85f007b7-540e-0410-9357-904b9bb8a0f7
* Mise de (*i autour CVS infoGravatar mohring2001-04-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1619 85f007b7-540e-0410-9357-904b9bb8a0f7
* ajout des lemmes ZimmermanGravatar mohring2001-04-08
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1556 85f007b7-540e-0410-9357-904b9bb8a0f7
* entetesGravatar filliatr2001-03-15
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1469 85f007b7-540e-0410-9357-904b9bb8a0f7
* mise sous CVS du repertoire theories/ArithGravatar filliatr2000-03-10
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@311 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-08 08:09:36 +0000