Pattern matching in the presence of strict propositions

[Tuplanolla]

Version

Coq 8.12.2

Equations 1.2.3

Operating system

Red Hat Enterprise Linux Workstation 7.4

Description of the problem

The following attempt to define Spr2 via equations fails and
it is unclear whether it should actually work.

(* From Coq Require Import Logic.StrictProp. *)
From Equations Require Import Equations.

Inductive Ssig {A : Type} (P : A -> SProp) :=
  | Sexists (a : A) (b : P a) : Ssig P.

Equations Spr1 {A : Type} {P : A -> SProp} (s : Ssig P) : A :=
  Spr1 (Sexists _ a b) := a.

Fail Equations Spr2 {A : Type} {P : A -> SProp} (s : Ssig P) : P (Spr1 s) :=
  Spr2 (Sexists _ a b) := b.
Equations Spr2 {A : Type} {P : A -> SProp} (s : Ssig P) : P (Spr1 s) :=
  Spr2 s := _.
Next Obligation. destruct s as [a b]. now simp Spr1. Fail Defined. Abort.

The command has indeed failed with message:
Pattern-matching expression on an object of inductive type @Ssig
has invalid information.
The command has indeed failed with message:
Illegal application:
The term "@eq_refl" of type "forall (A : Type) (x : A), x = x"
cannot be applied to the terms
 "P (Spr1 s)" : "SProp"
 "Spr2_obligations_obligation_1 A P s" : "P (Spr1 s)"
The 1st term has type "SProp" which should be coercible to
"Type".

Notes

Changing SProp into Prop fixes the problem,
but makes the resulting program useless.

[Tuplanolla]

Looks like you can make the definition go through
if you turn on cumulativity of strict propositions.
The generated equations will still be bad,
but at least you can write better ones by hand.

Set Cumulative StrictProp.

(* From Coq Require Import Logic.StrictProp. *)
From Equations Require Import Equations.

Inductive Ssig {A : Type} (P : A -> SProp) :=
  | Sexists (a : A) (b : P a) : Ssig P.

Equations Spr1 {A : Type} {P : A -> SProp} (s : Ssig P) : A :=
  Spr1 (Sexists _ a b) := a.

Fail Equations Spr2 {A : Type} {P : A -> SProp} (s : Ssig P) : P (Spr1 s) :=
  Spr2 (Sexists _ a b) := b.
Equations Spr2 {A : Type} {P : A -> SProp} (s : Ssig P) : P (Spr1 s) :=
  Spr2 s := _.
Next Obligation. destruct s as [a b]. now simp Spr1. Defined.

Corollary Spr2_equation_1' (A : Type) (P : A -> SProp) (a : A) (b : P a) :
  Spr2 (Sexists P a b) = b.
Proof. reflexivity. Qed.

Hint Rewrite @Spr2_equation_1' : Spr2.

Print Rewrite HintDb Spr2.

The command has indeed failed with message:
Pattern-matching expression on an object of inductive type Ssig
has invalid information.
Spr2_obligations_obligation_1 cannot be used as a hint.
Database Spr2
rewrite -> Spr2_equation_1 of type forall (A : Type) 
                                     (P : A -> SProp) 
                                     (s : Ssig P),
                                   Spr2 s =
                                   Spr2_obligations_obligation_1 A P s
rewrite -> Spr2_equation_1' of type forall (A : Type) 
                                      (P : A -> SProp) 
                                      (a : A) (b : P a),
                                    Spr2 (Sexists P a b) = b

[mattam82]

Sorry that was an overlook, now everything's fine. Note however that equations and the graph are not generated in this case as they would be trivial equations.