From 77d7a09c173afbd18bafa26d89b3114a42de88d0 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 28 Jul 2021 09:40:18 +0200
Subject: [PATCH] Move `sprop` file to `base` and improve documentation.

---
 README.md          |  3 +++
 _CoqProject        |  1 -
 theories/base.v    | 20 ++++++++++++++++++++
 theories/numbers.v |  2 +-
 theories/pmap.v    |  1 -
 theories/sprop.v   | 20 --------------------
 6 files changed, 24 insertions(+), 23 deletions(-)
 delete mode 100644 theories/sprop.v

diff --git a/README.md b/README.md
index 75614756..afe795b0 100644
--- a/README.md
+++ b/README.md
@@ -40,6 +40,9 @@ Notably:
   [Coq bug #5039](https://github.com/coq/coq/issues/5039) the `omega` tactic
   becomes unreliable. We do not consider this an issue since we use `lia` (for
   which the aforementioned Coq bug was fixed) instead of `omega` everywhere.
+* `Set Allow StrictProp`: the type of strict propositions (`SProp`) is enabled
+  by default since Coq 8.12. To make prior versions of Coq happy we need to
+  allow it explicitly.
 
 ## Prerequisites
 
diff --git a/_CoqProject b/_CoqProject
index 01aefbbf..6ea277df 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -5,7 +5,6 @@
 theories/options.v
 theories/base.v
 theories/tactics.v
-theories/sprop.v
 theories/option.v
 theories/fin_map_dom.v
 theories/boolset.v
diff --git a/theories/base.v b/theories/base.v
index ad373c01..b8bc0b8f 100644
--- a/theories/base.v
+++ b/theories/base.v
@@ -10,6 +10,7 @@ we must export [Coq.Peano] later than any export of [Coq.Bool]. *)
 over the ones of [Coq.Peano] (see Coq PR#12950), so we import [Utf8] last. *)
 From Coq Require Export Morphisms RelationClasses List Bool Setoid Peano Utf8.
 From Coq Require Import Permutation.
+From Coq Require Export Logic.StrictProp.
 Export ListNotations.
 From Coq.Program Require Export Basics Syntax.
 From stdpp Require Import options.
@@ -49,6 +50,10 @@ Obligation Tactic := idtac.
 (** 3. Hide obligations from the results of the [Search] commands. *)
 Add Search Blacklist "_obligation_".
 
+(** 4. [StrictProp] is enabled by default since Coq 8.12. To make prior versions
+of Coq happy we need to allow it explicitly. *)
+Global Set Allow StrictProp.
+
 (** * Sealing off definitions *)
 Section seal.
   Local Set Primitive Projections.
@@ -645,6 +650,21 @@ Proof. destruct b; simpl; tauto. Qed.
 Lemma Is_true_false (b : bool) : b = false → ¬b.
 Proof. now intros -> ?. Qed.
 
+(** ** SProp *)
+Lemma unsquash (P : Prop) `{!Decision P} : Squash P → P.
+Proof.
+  intros HP. destruct (decide P) as [?|HnotP]; [assumption|].
+  assert sEmpty as []. destruct HP. destruct HnotP; assumption.
+Qed.
+
+Definition SIs_true (b : bool) : SProp := Squash (Is_true b).
+
+Lemma SIs_true_intro b : Is_true b → SIs_true b.
+Proof. apply squash. Qed.
+Lemma SIs_true_elim b : SIs_true b → Is_true b.
+Proof. apply unsquash. destruct b; [left|right]; simpl; tauto. Qed.
+
+
 (** ** Unit *)
 Global Instance unit_equiv : Equiv unit := λ _ _, True.
 Global Instance unit_equivalence : Equivalence (≡@{unit}).
diff --git a/theories/numbers.v b/theories/numbers.v
index 13e32b54..4c15f5a8 100644
--- a/theories/numbers.v
+++ b/theories/numbers.v
@@ -3,7 +3,7 @@ natural numbers, and the type [Z] for integers. It also declares some useful
 notations. *)
 From Coq Require Export EqdepFacts PArith NArith ZArith NPeano.
 From Coq Require Import QArith Qcanon.
-From stdpp Require Export base decidable option sprop.
+From stdpp Require Export base decidable option.
 From stdpp Require Import options.
 Local Open Scope nat_scope.
 
diff --git a/theories/pmap.v b/theories/pmap.v
index 16425021..a57840b1 100644
--- a/theories/pmap.v
+++ b/theories/pmap.v
@@ -8,7 +8,6 @@ Leibniz equality to become extensional. *)
 From Coq Require Import PArith.
 From stdpp Require Import mapset countable.
 From stdpp Require Export fin_maps.
-From stdpp Require Export sprop.
 From stdpp Require Import options.
 
 Local Open Scope positive_scope.
diff --git a/theories/sprop.v b/theories/sprop.v
deleted file mode 100644
index f2c68709..00000000
--- a/theories/sprop.v
+++ /dev/null
@@ -1,20 +0,0 @@
-From Coq Require Export Logic.StrictProp.
-From stdpp Require Import decidable.
-From stdpp Require Import options.
-
-(** [StrictProp] is enabled by default since Coq 8.12. To make prior versions
-of Coq happy we need to allow it explicitly. *)
-Global Set Allow StrictProp.
-
-Lemma unsquash (P : Prop) `{!Decision P} : Squash P → P.
-Proof.
-  intros HP. destruct (decide P) as [?|HnotP]; [assumption|].
-  assert sEmpty as []. destruct HP. destruct HnotP; assumption.
-Qed.
-
-Definition SIs_true (b : bool) : SProp := Squash (Is_true b).
-
-Lemma SIs_true_intro b : Is_true b → SIs_true b.
-Proof. apply squash. Qed.
-Lemma SIs_true_elim b : SIs_true b → Is_true b.
-Proof. apply (unsquash _). Qed.
-- 
GitLab