Merge PR #8817: SProp: the definitionally proof irrelevant universe

Ack-by: JasonGross
Ack-by: SkySkimmer
Reviewed-by: Zimmi48
Reviewed-by: ejgallego
Ack-by: gares
Ack-by: mattam82

3 files changed, 39 insertions, 6 deletions

diff --git a/test-suite/bugs/closed/bug_3325.v b/test-suite/bugs/closed/bug_3325.v
index 36c065ebe8..835b8a7f33 100644
--- a/test-suite/bugs/closed/bug_3325.v
+++ b/test-suite/bugs/closed/bug_3325.v
@@ -1,13 +1,13 @@
 Typeclasses eauto := debug.
 Set Printing All.
 
-Axiom SProp : Set.
-Axiom sp : SProp.
+Axiom sProp : Set.
+Axiom sp : sProp.
 
 (* If we hardcode valueType := nat, it goes through *)
 Class StateIs := {
   valueType : Type;
-  stateIs : valueType -> SProp
+  stateIs : valueType -> sProp
 }.
 
 Instance NatStateIs : StateIs := {
@@ -17,17 +17,17 @@ Instance NatStateIs : StateIs := {
 Canonical Structure NatStateIs.
 
 Class LogicOps F := { land: F -> F }.
-Instance : LogicOps SProp. Admitted.
+Instance : LogicOps sProp. Admitted.
 Instance : LogicOps Prop. Admitted.
 
 Parameter (n : nat).
 (* If this is a [Definition], the resolution goes through fine. *)
 Notation vn := (@stateIs _ n).
 Definition vn' := (@stateIs _ n).
-Definition GOOD : SProp :=
+Definition GOOD : sProp :=
   @land _ _ vn'.
 (* This doesn't resolve, if PropLogicOps is defined later than SPropLogicOps *)
-Definition BAD : SProp :=
+Definition BAD : sProp :=
   @land _ _ vn.
 
 
diff --git a/test-suite/bugs/closed/bug_sprop_13.v b/test-suite/bugs/closed/bug_sprop_13.v
new file mode 100644
index 0000000000..ae80c9c51f
--- /dev/null
+++ b/test-suite/bugs/closed/bug_sprop_13.v
@@ -0,0 +1,7 @@
+(* -*- mode: coq; coq-prog-args: ("-allow-sprop") -*- *)
+Goal forall (P : SProp), P -> P.
+Proof.
+  intros P H. set (H0 := H).
+  (* goal is now H0 *)
+  exact H0.
+Qed.
diff --git a/test-suite/bugs/closed/bug_sprop_14.v b/test-suite/bugs/closed/bug_sprop_14.v
new file mode 100644
index 0000000000..1e6e9b30de
--- /dev/null
+++ b/test-suite/bugs/closed/bug_sprop_14.v
@@ -0,0 +1,26 @@
+(* -*- coq-prog-args: ("-allow-sprop"); -*- *)
+
+Set Universe Polymorphism.
+
+Inductive False : SProp :=.
+
+Axiom ℙ@{} : SProp.
+
+Definition TYPE@{i} := ℙ -> Type@{i}.
+Definition PROP@{} := ℙ -> SProp.
+
+Definition El@{i} (A : TYPE@{i}) := forall p, A p.
+Definition sEl@{} (A : PROP@{}) : SProp := forall p, A p.
+
+Definition SPropᶠ@{} := fun (p : ℙ) => SProp.
+
+Definition sProdᶠ@{i}
+  (A : TYPE@{i})
+  (B : forall (p : ℙ), El A -> SProp) : PROP := fun (p : ℙ) => forall x : El A, B p x.
+
+Definition Falseᶠ : El SPropᶠ := fun p => False.
+
+Definition EMᶠ : sEl (sProdᶠ SPropᶠ (fun p A => ((sProdᶠ A (fun p _ => Falseᶠ p))) p)).
+Proof.
+Fail Admitted.
+Abort.