Enable proof irrelevance for SProp.

4 files changed, 123 insertions, 30 deletions

diff --git a/kernel/cClosure.ml b/kernel/cClosure.ml
index a29f3c6833..405d0b4223 100644
--- a/kernel/cClosure.ml
+++ b/kernel/cClosure.ml
@@ -1194,12 +1194,12 @@ and norm_head info tab m =
   if is_val m then (incr prune; term_of_fconstr m) else
     match m.term with
       | FLambda(_n,tys,f,e) ->
-          let (e',rvtys) =
-            List.fold_left (fun (e,ctxt) (na,ty) ->
-              (subs_lift e, (na,kl info tab (mk_clos e ty))::ctxt))
-              (e,[]) tys in
-          let bd = kl info tab (mk_clos e' f) in
-          List.fold_left (fun b (na,ty) -> mkLambda(na,ty,b)) bd rvtys
+        let (e',info,rvtys) =
+          List.fold_left (fun (e,info,ctxt) (na,ty) ->
+              (subs_lift e, info, (na,kl info tab (mk_clos e ty))::ctxt))
+            (e,info,[]) tys in
+        let bd = kl info tab (mk_clos e' f) in
+        List.fold_left (fun b (na,ty) -> mkLambda(na,ty,b)) bd rvtys
       | FLetIn(na,a,b,f,e) ->
           let c = mk_clos (subs_lift e) f in
           mkLetIn(na, kl info tab a, kl info tab b, kl info tab c)
diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index 101f02323f..f32531721c 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -293,12 +293,6 @@ let conv_table_key infos k1 k2 cuniv =
 
 exception IrregularPatternShape
 
-let rec skip_pattern n c =
-  if Int.equal n 0 then c
-  else match kind c with
-  | Lambda (_, _, c) -> skip_pattern (pred n) c
-  | _ -> raise IrregularPatternShape
-
 let unfold_ref_with_args infos tab fl v =
   match unfold_reference infos tab fl with
   | Def def -> Some (def, v)
@@ -310,6 +304,7 @@ let unfold_ref_with_args infos tab fl v =
 
 type conv_tab = {
   cnv_inf : clos_infos;
+  relevances : Sorts.relevance list;
   lft_tab : clos_tab;
   rgt_tab : clos_tab;
 }
@@ -319,9 +314,24 @@ type conv_tab = {
 (** The same heap separation invariant must hold for the fconstr arguments
     passed to each respective side of the conversion function below. *)
 
+let push_relevance infos r =
+  { infos with relevances = r.Context.binder_relevance :: infos.relevances }
+
+let rec skip_pattern infos n c1 c2 =
+  if Int.equal n 0 then infos, c1, c2
+  else match kind c1, kind c2 with
+  | Lambda (x, _, c1), Lambda (_, _, c2) -> skip_pattern (push_relevance infos x) (pred n) c1 c2
+  | _ -> raise IrregularPatternShape
+
+let is_irrelevant infos lft c =
+  let env = info_env infos.cnv_inf in
+  try Retypeops.relevance_of_fterm env infos.relevances lft c == Sorts.Irrelevant with _ -> false
+
 (* Conversion between  [lft1]term1 and [lft2]term2 *)
 let rec ccnv cv_pb l2r infos lft1 lft2 term1 term2 cuniv =
-  eqappr cv_pb l2r infos (lft1, (term1,[])) (lft2, (term2,[])) cuniv
+  if is_irrelevant infos lft1 term1 && is_irrelevant infos lft2 term2
+  then cuniv
+  else eqappr cv_pb l2r infos (lft1, (term1,[])) (lft2, (term2,[])) cuniv
 
 (* Conversion between [lft1](hd1 v1) and [lft2](hd2 v2) *)
 and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv =
@@ -399,14 +409,14 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv =
         match unfold_projection infos.cnv_inf p2 with
         | Some s2 ->
           eqappr cv_pb l2r infos appr1 (lft2, (c2, (s2 :: v2))) cuniv
-	| None -> 
+        | None ->
           if Projection.Repr.equal (Projection.repr p1) (Projection.repr p2)
-	     && compare_stack_shape v1 v2 then
+             && compare_stack_shape v1 v2 then
             let el1 = el_stack lft1 v1 in
             let el2 = el_stack lft2 v2 in
             let u1 = ccnv CONV l2r infos el1 el2 c1 c2 cuniv in
               convert_stacks l2r infos lft1 lft2 v1 v2 u1
-	  else (* Two projections in WHNF: unfold *)
+          else (* Two projections in WHNF: unfold *)
 	    raise NotConvertible)
 
     | (FProj (p1,c1), t2) ->
@@ -447,21 +457,21 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv =
            we throw them away *)
         if not (is_empty_stack v1 && is_empty_stack v2) then
           anomaly (Pp.str "conversion was given ill-typed terms (FLambda).");
-        let (_,ty1,bd1) = destFLambda mk_clos hd1 in
+        let (x1,ty1,bd1) = destFLambda mk_clos hd1 in
         let (_,ty2,bd2) = destFLambda mk_clos hd2 in
         let el1 = el_stack lft1 v1 in
         let el2 = el_stack lft2 v2 in
         let cuniv = ccnv CONV l2r infos el1 el2 ty1 ty2 cuniv in
-        ccnv CONV l2r infos (el_lift el1) (el_lift el2) bd1 bd2 cuniv
+        ccnv CONV l2r (push_relevance infos x1) (el_lift el1) (el_lift el2) bd1 bd2 cuniv
 
-    | (FProd (_, c1, c2, e), FProd (_, c'1, c'2, e')) ->
+    | (FProd (x1, c1, c2, e), FProd (_, c'1, c'2, e')) ->
         if not (is_empty_stack v1 && is_empty_stack v2) then
 	  anomaly (Pp.str "conversion was given ill-typed terms (FProd).");
 	(* Luo's system *)
         let el1 = el_stack lft1 v1 in
         let el2 = el_stack lft2 v2 in
         let cuniv = ccnv CONV l2r infos el1 el2 c1 c'1 cuniv in
-        ccnv cv_pb l2r infos (el_lift el1) (el_lift el2) (mk_clos (subs_lift e) c2) (mk_clos (subs_lift e') c'2) cuniv
+        ccnv cv_pb l2r (push_relevance infos x1) (el_lift el1) (el_lift el2) (mk_clos (subs_lift e) c2) (mk_clos (subs_lift e') c'2) cuniv
 
     (* Eta-expansion on the fly *)
     | (FLambda _, _) ->
@@ -470,18 +480,20 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv =
         | _ ->
           anomaly (Pp.str "conversion was given unreduced term (FLambda).")
         in
-        let (_,_,bd1) = destFLambda mk_clos hd1 in
+        let (x1,_ty1,bd1) = destFLambda mk_clos hd1 in
+        let infos = push_relevance infos x1 in
         eqappr CONV l2r infos
-	  (el_lift lft1, (bd1, [])) (el_lift lft2, (hd2, eta_expand_stack v2)) cuniv
+          (el_lift lft1, (bd1, [])) (el_lift lft2, (hd2, eta_expand_stack v2)) cuniv
     | (_, FLambda _) ->
         let () = match v2 with
         | [] -> ()
         | _ ->
 	  anomaly (Pp.str "conversion was given unreduced term (FLambda).")
 	in
-        let (_,_,bd2) = destFLambda mk_clos hd2 in
+        let (x2,_ty2,bd2) = destFLambda mk_clos hd2 in
+        let infos = push_relevance infos x2 in
         eqappr CONV l2r infos
-	  (el_lift lft1, (hd1, eta_expand_stack v1)) (el_lift lft2, (bd2, [])) cuniv
+          (el_lift lft1, (hd1, eta_expand_stack v1)) (el_lift lft2, (bd2, [])) cuniv
 
     (* only one constant, defined var or defined rel *)
     | (FFlex fl1, c2)      ->
@@ -568,7 +580,7 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv =
          in convert_stacks l2r infos lft1 lft2 v1 v2 cuniv
        with Not_found -> raise NotConvertible)
 
-    | (FFix (((op1, i1),(_,tys1,cl1)),e1), FFix(((op2, i2),(_,tys2,cl2)),e2)) ->
+    | (FFix (((op1, i1),(na1,tys1,cl1)),e1), FFix(((op2, i2),(_,tys2,cl2)),e2)) ->
         if Int.equal i1 i2 && Array.equal Int.equal op1 op2
 	then
 	  let n = Array.length cl1 in
@@ -580,12 +592,14 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv =
           let el2 = el_stack lft2 v2 in
           let cuniv = convert_vect l2r infos el1 el2 fty1 fty2 cuniv in
           let cuniv =
+            let infos = Array.fold_left push_relevance infos na1 in
             convert_vect l2r infos
-	      (el_liftn n el1) (el_liftn n el2) fcl1 fcl2 cuniv in
+                         (el_liftn n el1) (el_liftn n el2) fcl1 fcl2 cuniv
+          in
           convert_stacks l2r infos lft1 lft2 v1 v2 cuniv
         else raise NotConvertible
 
-    | (FCoFix ((op1,(_,tys1,cl1)),e1), FCoFix((op2,(_,tys2,cl2)),e2)) ->
+    | (FCoFix ((op1,(na1,tys1,cl1)),e1), FCoFix((op2,(_,tys2,cl2)),e2)) ->
         if Int.equal op1 op2
         then
 	  let n = Array.length cl1 in
@@ -597,8 +611,10 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv =
           let el2 = el_stack lft2 v2 in
           let cuniv = convert_vect l2r infos el1 el2 fty1 fty2 cuniv in
           let cuniv =
+            let infos = Array.fold_left push_relevance infos na1 in
             convert_vect l2r infos
-	      (el_liftn n el1) (el_liftn n el2) fcl1 fcl2 cuniv in
+                         (el_liftn n el1) (el_liftn n el2) fcl1 fcl2 cuniv
+          in
           convert_stacks l2r infos lft1 lft2 v1 v2 cuniv
         else raise NotConvertible
 
@@ -662,8 +678,8 @@ and convert_vect l2r infos lft1 lft2 v1 v2 cuniv =
 and convert_branches l2r infos ci e1 e2 lft1 lft2 br1 br2 cuniv =
   (** Skip comparison of the pattern types. We know that the two terms are
       living in a common type, thus this check is useless. *)
-  let fold n c1 c2 cuniv = match skip_pattern n c1, skip_pattern n c2 with
-  | (c1, c2) ->
+  let fold n c1 c2 cuniv = match skip_pattern infos n c1 c2 with
+  | (infos, c1, c2) ->
     let lft1 = el_liftn n lft1 in
     let lft2 = el_liftn n lft2 in
     let e1 = subs_liftn n e1 in
@@ -680,6 +696,7 @@ let clos_gen_conv trans cv_pb l2r evars env univs t1 t2 =
   let infos = create_clos_infos ~evars reds env in
   let infos = {
     cnv_inf = infos;
+    relevances = List.map Context.Rel.Declaration.get_relevance (rel_context env);
     lft_tab = create_tab ();
     rgt_tab = create_tab ();
   } in
diff --git a/test-suite/success/sprop.v b/test-suite/success/sprop.v
index 0e65211390..995fd7eccc 100644
--- a/test-suite/success/sprop.v
+++ b/test-suite/success/sprop.v
@@ -9,10 +9,16 @@ 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).
 
@@ -27,6 +33,13 @@ Inductive sBox (A:SProp) : Prop
 
 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.
@@ -98,8 +111,19 @@ 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. *)
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.