Initial PoC for a barebone Coq prelude.

The goal is to basically do nothing but the strictly necessary
things.

COPYING

@@ -0,0 +1,19 @@
+Copyright (c) 2024 Peio Borthelle
+
+Permission is hereby granted, free of charge, to any person obtaining a copy
+of this software and associated documentation files (the "Software"), to deal
+in the Software without restriction, including without limitation the rights
+to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
+copies of the Software, and to permit persons to whom the Software is
+furnished to do so, subject to the following conditions:
+
+The above copyright notice and this permission notice shall be included in all
+copies or substantial portions of the Software.
+
+THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
+IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
+FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
+AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
+LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
+OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
+SOFTWARE.

coq-barebone.opam

@@ -0,0 +1,28 @@
+# This file is generated by dune, edit dune-project instead
+opam-version: "2.0"
+version: "0.1"
+synopsis: "A barebone Coq prelude"
+authors: ["Peio Borthelle <peio.borthelle@univ-smb.fr>"]
+license: "MIT"
+homepage: "https://github.com/lapin0t/coq-barebone"
+bug-reports: "https://github.com/lapin0t/coq-barebone/issues"
+depends: [
+  "dune" {>= "3.11"}
+  "coq" {>= "8.18"}
+  "odoc" {with-doc}
+]
+build: [
+  ["dune" "subst"] {dev}
+  [
+    "dune"
+    "build"
+    "-p"
+    name
+    "-j"
+    jobs
+    "@install"
+    "@runtest" {with-test}
+    "@doc" {with-doc}
+  ]
+]
+dev-repo: "git+https://github.com/lapin0t/coq-barebone.git"

dune-project

@@ -0,0 +1,19 @@
+(lang dune 3.11)
+(using coq 0.8)
+(name coq-barebone)
+
+(license MIT)
+(authors "Peio Borthelle <peio.borthelle@univ-smb.fr>")
+(source (github "lapin0t/coq-barebone"))
+(bug_reports "https://github.com/lapin0t/coq-barebone/issues")
+
+(generate_opam_files true)
+
+(package
+ (name coq-barebone)
+ (synopsis "A barebone Coq prelude")
+ (version 0.1)
+ (depends
+  (coq (>= 8.18))
+ )
+)

theories/Prelude.v

@@ -0,0 +1,6 @@
+#[export] Unset Elimination Schemes.
+#[export] Set Implicit Arguments.
+#[export] Set Primitive Projections.
+
+#[global] Notation "A -> B" := (forall (_ : A), B)
+  (at level 99, right associativity, B at level 200) .

theories/Prim/Bool.v

@@ -0,0 +1,3 @@
+Require Import Barebone.Prelude.
+
+Variant bool : Set := true | false.

theories/Prim/Int63.v

@@ -0,0 +1,50 @@
+Require Import Barebone.Prelude.
+
+Require Barebone.Prim.Bool.
+Register Bool.bool as kernel.ind_bool.
+
+Require Barebone.Prim.Prod.
+Register Prod.prod as kernel.ind_pair.
+
+Variant carry (A : Type) : Type := C0 (a : A) | C1 (a : A).
+Register carry as kernel.ind_carry.
+
+Variant cmp : Set := Eq | Lt | Gt.
+Register cmp as kernel.ind_cmp.
+
+Primitive int := #int63_type.
+
+Primitive lsl := #int63_lsl.
+Primitive lsr := #int63_lsr.
+Primitive land := #int63_land.
+Primitive lor := #int63_lor.
+Primitive lxor := #int63_lxor.
+Primitive asr := #int63_asr.
+
+Primitive add := #int63_add.
+Primitive sub := #int63_sub.
+Primitive mul := #int63_mul.
+Primitive mulc := #int63_mulc.
+Primitive div := #int63_div.
+Primitive mod := #int63_mod.
+Primitive divs := #int63_divs.
+Primitive mods := #int63_mods.
+
+Primitive eqb := #int63_eq.
+Primitive ltb := #int63_lt.
+Primitive leb := #int63_le.
+Primitive ltsb := #int63_lts.
+Primitive lesb := #int63_les.
+Primitive compare := #int63_compare.
+Primitive compares := #int63_compares.
+
+Primitive addc := #int63_addc.
+Primitive addcarryc := #int63_addcarryc.
+Primitive subc := #int63_subc.
+Primitive subcarryc := #int63_subcarryc.
+Primitive diveucl := #int63_diveucl.
+Primitive diveucl_21 := #int63_div21.
+Primitive addmuldiv := #int63_addmuldiv.
+
+Primitive head0 := #int63_head0.
+Primitive tail0 := #int63_tail0.

theories/Prim/Prod.v

@@ -0,0 +1,3 @@
+Require Import Barebone.Prelude.
+
+Variant prod (A B : Type) : Type := pair (a : A) (b : B).

theories/dune

@@ -0,0 +1,6 @@
+(include_subdirs qualified)
+
+(coq.theory
+ (name Barebone)
+ (package coq-barebone)
+ (stdlib no))