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

8 files changed, 314 insertions, 27 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.
diff --git a/test-suite/misc/poly-capture-global-univs/src/evilImpl.ml b/test-suite/misc/poly-capture-global-univs/src/evilImpl.ml
index f5043db099..adabb7a0a0 100644
--- a/test-suite/misc/poly-capture-global-univs/src/evilImpl.ml
+++ b/test-suite/misc/poly-capture-global-univs/src/evilImpl.ml
@@ -16,7 +16,7 @@ let evil t f =
 
   let fe = Declare.definition_entry
       ~univs:(Polymorphic_entry ([|Anonymous|], UContext.make (Instance.of_array [|u|],Constraint.empty)))
-      ~types:(Term.mkArrow tc tu)
-      (mkLambda (Name.Name (Id.of_string "x"), tc, mkRel 1))
+      ~types:(Term.mkArrowR tc tu)
+      (mkLambda (Context.nameR (Id.of_string "x"), tc, mkRel 1))
   in
   ignore (Declare.declare_constant f (DefinitionEntry fe, k))
diff --git a/test-suite/output/RealSyntax.v b/test-suite/output/RealSyntax.v
index 15ae66010e..44e8c7a50c 100644
--- a/test-suite/output/RealSyntax.v
+++ b/test-suite/output/RealSyntax.v
@@ -1,3 +1,3 @@
-Require Import Reals.
+Require Import Reals.Rdefinitions.
 Check 32%R.
 Check (-31)%R.
diff --git a/test-suite/output/Search.out b/test-suite/output/Search.out
index f4544a0df3..ffba1d35cc 100644
--- a/test-suite/output/Search.out
+++ b/test-suite/output/Search.out
@@ -1,59 +1,72 @@
 le_n: forall n : nat, n <= n
 le_0_n: forall n : nat, 0 <= n
 le_S: forall n m : nat, n <= m -> n <= S m
-le_n_S: forall n m : nat, n <= m -> S n <= S m
-le_pred: forall n m : nat, n <= m -> Nat.pred n <= Nat.pred m
 le_S_n: forall n m : nat, S n <= S m -> n <= m
-min_l: forall n m : nat, n <= m -> Nat.min n m = n
+le_pred: forall n m : nat, n <= m -> Nat.pred n <= Nat.pred m
+le_n_S: forall n m : nat, n <= m -> S n <= S m
+max_l: forall n m : nat, m <= n -> Nat.max n m = n
 max_r: forall n m : nat, n <= m -> Nat.max n m = m
 min_r: forall n m : nat, m <= n -> Nat.min n m = m
-max_l: forall n m : nat, m <= n -> Nat.max n m = n
+min_l: forall n m : nat, n <= m -> Nat.min n m = n
 le_ind:
   forall (n : nat) (P : nat -> Prop),
   P n ->
   (forall m : nat, n <= m -> P m -> P (S m)) ->
   forall n0 : nat, n <= n0 -> P n0
+le_sind:
+  forall (n : nat) (P : nat -> SProp),
+  P n ->
+  (forall m : nat, n <= m -> P m -> P (S m)) ->
+  forall n0 : nat, n <= n0 -> P n0
 false: bool
 true: bool
+eq_true: bool -> Prop
 is_true: bool -> Prop
 negb: bool -> bool
-eq_true: bool -> Prop
-implb: bool -> bool -> bool
-orb: bool -> bool -> bool
 andb: bool -> bool -> bool
+orb: bool -> bool -> bool
+implb: bool -> bool -> bool
 xorb: bool -> bool -> bool
 Nat.even: nat -> bool
 Nat.odd: nat -> bool
 BoolSpec: Prop -> Prop -> bool -> Prop
-Nat.eqb: nat -> nat -> bool
-Nat.testbit: nat -> nat -> bool
 Nat.ltb: nat -> nat -> bool
+Nat.testbit: nat -> nat -> bool
+Nat.eqb: nat -> nat -> bool
 Nat.leb: nat -> nat -> bool
 Nat.bitwise: (bool -> bool -> bool) -> nat -> nat -> nat -> nat
-bool_ind: forall P : bool -> Prop, P true -> P false -> forall b : bool, P b
 bool_rec: forall P : bool -> Set, P true -> P false -> forall b : bool, P b
+eq_true_ind_r:
+  forall (P : bool -> Prop) (b : bool), P b -> eq_true b -> P true
 eq_true_rec:
   forall P : bool -> Set, P true -> forall b : bool, eq_true b -> P b
-bool_rect: forall P : bool -> Type, P true -> P false -> forall b : bool, P b
-eq_true_rect_r:
-  forall (P : bool -> Type) (b : bool), P b -> eq_true b -> P true
-eq_true_rec_r:
-  forall (P : bool -> Set) (b : bool), P b -> eq_true b -> P true
+bool_ind: forall P : bool -> Prop, P true -> P false -> forall b : bool, P b
 eq_true_rect:
   forall P : bool -> Type, P true -> forall b : bool, eq_true b -> P b
+eq_true_sind:
+  forall P : bool -> SProp, P true -> forall b : bool, eq_true b -> P b
+bool_rect: forall P : bool -> Type, P true -> P false -> forall b : bool, P b
 eq_true_ind:
   forall P : bool -> Prop, P true -> forall b : bool, eq_true b -> P b
-eq_true_ind_r:
-  forall (P : bool -> Prop) (b : bool), P b -> eq_true b -> P true
+eq_true_rec_r:
+  forall (P : bool -> Set) (b : bool), P b -> eq_true b -> P true
+eq_true_rect_r:
+  forall (P : bool -> Type) (b : bool), P b -> eq_true b -> P true
+bool_sind:
+  forall P : bool -> SProp, P true -> P false -> forall b : bool, P b
 Byte.to_bits:
   Byte.byte ->
   bool * (bool * (bool * (bool * (bool * (bool * (bool * bool))))))
 Byte.of_bits:
   bool * (bool * (bool * (bool * (bool * (bool * (bool * bool)))))) ->
   Byte.byte
+andb_prop: forall a b : bool, (a && b)%bool = true -> a = true /\ b = true
 andb_true_intro:
   forall b1 b2 : bool, b1 = true /\ b2 = true -> (b1 && b2)%bool = true
-andb_prop: forall a b : bool, (a && b)%bool = true -> a = true /\ b = true
+BoolSpec_sind:
+  forall (P Q : Prop) (P0 : bool -> SProp),
+  (P -> P0 true) ->
+  (Q -> P0 false) -> forall b : bool, BoolSpec P Q b -> P0 b
 BoolSpec_ind:
   forall (P Q : Prop) (P0 : bool -> Prop),
   (P -> P0 true) ->
diff --git a/test-suite/success/sprop.v b/test-suite/success/sprop.v
new file mode 100644
index 0000000000..268c1880d2
--- /dev/null
+++ b/test-suite/success/sprop.v
@@ -0,0 +1,189 @@
+(* -*- mode: coq; coq-prog-args: ("-allow-sprop") -*- *)
+
+Set Primitive Projections.
+Set Warnings "+non-primitive-record".
+Set Warnings "+bad-relevance".
+
+Check SProp.
+
+Definition iUnit : SProp := forall A : SProp, A -> A.
+
+Definition itt : iUnit := fun A a => a.
+
+Definition iUnit_irr (P : iUnit -> Type) (x y : iUnit) : P x -> P y
+  := fun v => v.
+
+Definition iSquash (A:Type) : SProp
+  := forall P : SProp, (A -> P) -> P.
+Definition isquash A : A -> iSquash A
+  := fun a P f => f a.
+Definition iSquash_rect A (P : iSquash A -> SProp) (H : forall x : A, P (isquash A x))
+  : forall x : iSquash A, P x
+  := fun x => x (P x) (H : A -> P x).
+
+Fail Check (fun A : SProp => A : Type).
+
+Lemma foo : Prop.
+Proof. pose (fun A : SProp => A : Type); exact True. Fail Qed. Abort.
+
+(* define evar as product *)
+Check (fun (f:(_:SProp)) => f _).
+
+Inductive sBox (A:SProp) : Prop
+  := sbox : A -> sBox A.
+
+Definition uBox := sBox iUnit.
+
+Definition sBox_irr A (x y : sBox A) : x = y.
+Proof.
+  Fail reflexivity.
+  destruct x as [x], y as [y].
+  reflexivity.
+Defined.
+
+(* Primitive record with all fields in SProp has the eta property of SProp so must be SProp. *)
+Fail Record rBox (A:SProp) : Prop := rmkbox { runbox : A }.
+Section Opt.
+  Local Unset Primitive Projections.
+  Record rBox (A:SProp) : Prop := rmkbox { runbox : A }.
+End Opt.
+
+(* Check that defining as an emulated record worked *)
+Check runbox.
+
+(* Check that it doesn't have eta *)
+Fail Check (fun (A : SProp) (x : rBox A) => eq_refl : x = @rmkbox _ (@runbox _ x)).
+
+Inductive sEmpty : SProp := .
+
+Inductive sUnit : SProp := stt.
+
+Inductive BIG : SProp := foo | bar.
+
+Inductive Squash (A:Type) : SProp
+  := squash : A -> Squash A.
+
+Definition BIG_flip : BIG -> BIG.
+Proof.
+  intros [|]. exact bar. exact foo.
+Defined.
+
+Inductive pb : Prop := pt | pf.
+
+Definition pb_big : pb -> BIG.
+Proof.
+  intros [|]. exact foo. exact bar.
+Defined.
+
+Fail Definition big_pb (b:BIG) : pb :=
+  match b return pb with foo => pt | bar => pf end.
+
+Inductive which_pb : pb -> SProp :=
+| is_pt : which_pb pt
+| is_pf : which_pb pf.
+
+Fail Definition pb_which b (w:which_pb b) : bool
+  := match w with
+     | is_pt => true
+     | is_pf => false
+     end.
+
+(* Non primitive because no arguments, but maybe we should allow it for sprops? *)
+Fail Record UnitRecord : SProp := {}.
+
+Section Opt.
+  Local Unset Primitive Projections.
+  Record UnitRecord' : SProp := {}.
+End Opt.
+Fail Scheme Induction for UnitRecord' Sort Set.
+
+Record sProd (A B : SProp) : SProp := sPair { sFst : A; sSnd : B }.
+
+Scheme Induction for sProd Sort Set.
+
+Unset Primitive Projections.
+Record sProd' (A B : SProp) : SProp := sPair' { sFst' : A; sSnd' : B }.
+Set Primitive Projections.
+
+Fail Scheme Induction for sProd' Sort Set.
+
+Inductive Istrue : bool -> SProp := istrue : Istrue true.
+
+Definition Istrue_sym (b:bool) := if b then sUnit else sEmpty.
+Definition Istrue_to_sym b (i:Istrue b) : Istrue_sym b := match i with istrue => stt end.
+
+Definition Istrue_rec (P:forall b, Istrue b -> Set) (H:P true istrue) b (i:Istrue b) : P b i.
+Proof.
+  destruct b.
+  - exact_no_check H.
+  - apply sEmpty_rec. apply Istrue_to_sym in i. exact i.
+Defined.
+
+Check (fun P v (e:Istrue true) => eq_refl : Istrue_rec P v _ e = v).
+
+Record Truepack := truepack { trueval :> bool; trueprop : Istrue trueval }.
+
+Definition Truepack_eta (x : Truepack) (i : Istrue x) : x = truepack x i := @eq_refl Truepack x.
+
+Class emptyclass : SProp := emptyinstance : forall A:SProp, A.
+
+(** Sigma in SProp can be done through Squash and relevant sigma. *)
+Definition sSigma (A:SProp) (B:A -> SProp) : SProp
+  := Squash (@sigT (rBox A) (fun x => rBox (B (runbox _ x)))).
+
+Definition spair (A:SProp) (B:A->SProp) (x:A) (y:B x) : sSigma A B
+  := squash _ (existT _ (rmkbox _ x) (rmkbox _ y)).
+
+Definition spr1 (A:SProp) (B:A->SProp) (p:sSigma A B) : A
+  := let 'squash _ (existT _ x y) := p in runbox _ x.
+
+Definition spr2 (A:SProp) (B:A->SProp) (p:sSigma A B) : B (spr1 A B p)
+  := let 'squash _ (existT _ x y) := p return B (spr1 A B p) in runbox _ y.
+(* it's SProp so it computes properly *)
+
+(** Fixpoints on SProp values are only allowed to produce SProp results *)
+Inductive sAcc (x:nat) : SProp := sAcc_in : (forall y, y < x -> sAcc y) -> sAcc x.
+
+Definition sAcc_inv x (s:sAcc x) : forall y, y < x -> sAcc y.
+Proof.
+  destruct s as [H]. exact H.
+Defined.
+
+Section sFix_fail.
+  Variable P : nat -> Type.
+  Variable F : forall x:nat, (forall y:nat, y < x -> P y) -> P x.
+
+  Fail Fixpoint sFix (x:nat) (a:sAcc x) {struct a} : P x :=
+    F x (fun (y:nat) (h: y < x) => sFix y (sAcc_inv x a y h)).
+End sFix_fail.
+
+Section sFix.
+  Variable P : nat -> SProp.
+  Variable F : forall x:nat, (forall y:nat, y < x -> P y) -> P x.
+
+  Fixpoint sFix (x:nat) (a:sAcc x) {struct a} : P x :=
+    F x (fun (y:nat) (h: y < x) => sFix y (sAcc_inv x a y h)).
+
+End sFix.
+
+(** Relevance repairs *)
+
+Fail Definition fix_relevance : _ -> nat := fun _ : iUnit => 0.
+
+Require Import ssreflect.
+
+Goal forall T : SProp, T -> True.
+Proof.
+  move=> T +.
+  intros X;exact I.
+Qed.
+
+Set Warnings "-bad-relevance".
+Definition fix_relevance : _ -> nat := fun _ : iUnit => 0.
+
+(* relevance isn't fixed when checking P x == P y *)
+Fail Definition relevance_unfixed := fun (A:SProp) (P:A -> Prop) x y (v:P x) => v : P y.
+
+(* but the kernel is fine *)
+Definition relevance_unfixed := fun (A:SProp) (P:A -> Prop) x y (v:P x) =>
+                                  ltac:(exact_no_check v) : P y.
diff --git a/test-suite/success/sprop_hcons.v b/test-suite/success/sprop_hcons.v
new file mode 100644
index 0000000000..14772dd62b
--- /dev/null
+++ b/test-suite/success/sprop_hcons.v
@@ -0,0 +1,52 @@
+(* -*- coq-prog-args: ("-allow-sprop"); -*- *)
+
+(* A bug due to bad hashconsing of case info *)
+
+Inductive sBox (A : SProp) : Type :=
+  sbox : A -> sBox A.
+
+Definition ubox {A : SProp} (bA : sBox A) : A :=
+  match bA with
+    sbox _ X => X
+  end.
+
+Inductive sle : nat -> nat -> SProp :=
+  sle_0 : forall n, sle 0 n
+| sle_S : forall n m : nat, sle n m -> sle (S n) (S m).
+
+Definition sle_Sn (n : nat) : sle n (S n).
+Proof.
+  induction n; constructor; auto.
+Defined.
+
+Definition sle_trans {n m p} (H : sle n m) (H': sle m  p) : sle n p.
+Proof.
+  revert H'. revert p. induction H.
+  - intros p H'. apply sle_0.
+  - intros p H'. inversion H'. apply ubox. subst. apply sbox. apply sle_S. apply IHsle;auto.
+Defined.
+
+Lemma sle_Sn_m {n m} : sle n m -> sle n (S m).
+Proof.
+  intros H. destruct n.
+  - constructor.
+  - constructor;auto. assert (H1 : sle n (S n)) by apply sle_Sn.
+    exact (sle_trans H1 H ).
+Defined.
+
+Definition sle_Sn_Sm {n m} : sle (S n) (S m) -> sle n m.
+Proof.
+  intros H.
+  inversion H. apply ubox. subst. apply sbox. exact H2.
+Qed.
+
+
+Notation "g ∘ f" := (sle_trans g f) (at level 40).
+
+Lemma bazz q0 m (f : sle (S q0) (S m)) :
+  sbox _ (sle_Sn q0 ∘ f) = sbox _ (sle_Sn_m (sle_Sn_Sm f)).
+Proof.
+  reflexivity. (* used to fail *)
+  (* NB: exact eq_refl succeeded even with the bug so no guarantee
+  that this test will continue to test the right thing. *)
+Qed.