Stdlib2: get started

CONTRIBUTING.md

@@ -0,0 +1,81 @@
+# Contribution Guide
+
+This guide describes the styling conventions that are applicable to the
+development of this library.
+
+This file is not comprehensive yet, it contains mistakes and unclear
+indications, and some topics may have been overlooked: please consider improving
+it.
+
+## Layout of the file system
+
+### Naming of files
+
+## Statements of lemmas, theorems and definitions.
+
+- Universal quantifications with dependent variable should appear on the left hand side of the colon, until we reach the first non dependent variables. e.g.
+  `Lemma example x y : x < y -> x >= y = false`
+
+### Naming of variables
+
+- Hypothesis should not be named `H`, `H'`,... but have meaningful names. For
+  example, an hypothesis `n > 0` should be named `n_gt0`.
+
+### Naming conventions
+
+To be defined…
+
+## Proof style
+
+### General guidelines
+
+- **A line should have no more than 80 characters**. What a
+character is is subject to interpretation. If a line is longer than that,
+it should be cut semantically. If there is no way to make a semantic
+cut (e.g. the user provides an explicit term that is too long to fit on
+one line), then just cut it over several lines to make it readable.
+
+### White space
+
+- Operators are surrounded by space, for example `n*m` should be written `n * m`.
+
+We write
+- `move=>` and `move:` (no space between `move` and `=>` or `:`)
+- `apply/` and `apply:` (no space between `apply` and `/` or `:`)
+- `rewrite /definition` (there is a space between `rewrite` and an unfold)
+
+### Indentation in proof scripts
+
+- Lines end with a point `.` and only have `;` inside them.
+- Lines that close a goal must start with a terminator (`by` or
+  `exact`).
+- When two subgoals are created, the first subgoal is indented by 2
+  spaces, the second is not. Use `last first` to bring the
+  smallest/less meaningful goal first, and keep the main flow of the
+  proof unindented.
+- When more than two subgoals are created, bullets are used `-` for
+  the first level, `+` for the second and `*` for the third as in:
+  ```
+  tactic.
+  - tactic.
+    + tactic.
+      * tactic.
+      * tactic.
+      * tactic.
+    + tactic.
+    + tactic.
+  - tactic
+  - tactic
+  ```
+
+  If all the subgoals have the same importance, use bullets for all of
+  them, however, if one goal is more important than the others
+  (i.e. is main flow of the proof). Then you might remove the bullet
+  for this last one and unindent it as in:
+  ```
+  tactic.
+  - tactic. (* secondary subgoal 1 *)
+  - tactic. (* secondary subgoal 2 *)
+  tactic. (* third subgoal is the main one *)
+  ```
+

README.md

@@ -2,18 +2,27 @@ The purpose of this project is to design and implement a new standard library
 for Coq. It will follow a clean slate approach, not aiming at compatibility with
 the current library, which will be maintained separately.
 
+## Organization
+
 This project is coordinated by @maximedenes and can be discussed and followed
 at: https://github.com/coq/coq/issues/7711 and
 https://github.com/orgs/coq/projects/1
 
 We foresee several stages:
-- Preliminary clean-up and infrastructure work
-- Implementation of prelude and basic tactics
-- Experimentation on existing libraries (for example, to compare canonical
-  structures and type classes)
-- Implementation of the first components of the library
-- Extensions of the library
+ 1. Preliminary clean-up and infrastructure work
+ 1. Implementation of prelude and basic tactics
+ 1. Enhancement of the core of the library.
+ 1. First release.
+ 1. Implementation of the first components of the library
+ 1. Extensions of the library
+
+## Current status
+
+The project is currently (February 2019) in its second phase (starting the
+actual implementation).
+
+Questions and discussions are welcome at this stage. In particular, the wiki and
+issues (as opposed to code reviews) can be used to share and discuss opinions.
 
-The project is currently in its first phase. Questions and discussions are
-welcome at this stage. External code contribution will be integrated during the
-last two phases.
+External code contribution will be integrated during the last two phases. See
+[CONTRIBUTING.md](contributing guide)

src/.gitignore

@@ -0,0 +1,6 @@
+Makefile
+Makefile.conf
+.coqdeps.d
+*.vo
+*.glob
+.*.aux

src/_CoqProject

@@ -0,0 +1,19 @@
+-arg -noinit
+-arg -w
+-arg +non-primitive-record
+-R . Stdlib
+
+abstract.v
+bool.v
+congr.v
+datatypes.v
+decimal.v
+equality.v
+functions.v
+lock.v
+nat.v
+prelude.v
+prelude_plugins.v
+prop.v
+ssreflect.v
+matching.v

src/abstract.v

@@ -0,0 +1,37 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+Require Import prelude ssreflect datatypes equality nat.
+
+(* Constants for abstract: and [: name ] intro pattern *)
+Definition abstract_lock := unit.
+Definition abstract_key := tt.
+
+Definition abstract (statement : Type) (id : nat) (lock : abstract_lock) :=
+  let: tt := lock in statement.
+
+Notation "<hidden n >" := (abstract _ n _).
+Notation "T (* n *)" := (abstract T n abstract_key).
+
+Register abstract_lock as plugins.ssreflect.abstract_lock.
+Register abstract_key as plugins.ssreflect.abstract_key.
+Register abstract as plugins.ssreflect.abstract.
+
+(* To focus non-ssreflect tactics on a subterm, eg vm_compute. *)
+(* Usage:                                                      *)
+(*   elim/abstract_context: (pattern) => G defG.               *)
+(*   vm_compute; rewrite {}defG {G}.                           *)
+(* Note that vm_cast are not stored in the proof term          *)
+(* for reductions occuring in the context, hence               *)
+(*   set here := pattern; vm_compute in (value of here)        *)
+(* blows up at Qed time.                                       *)
+Lemma abstract_context T (P : T -> Type) x :
+  (forall Q, Q = P -> Q x) -> P x.
+Proof. by move=> /(_ P); apply. Qed.