Failed attempt at improving performances of pairs by using inductives

algebra/cmra.v

@@ -934,8 +934,12 @@ Section prod.
   Instance prod_pcore : PCore (A * B) := λ x,
     c1 ← pcore (x.1); c2 ← pcore (x.2); Some (c1, c2).
   Arguments prod_pcore !_ /.
-  Instance prod_valid : Valid (A * B) := λ x, ✓ x.1 ∧ ✓ x.2.
-  Instance prod_validN : ValidN (A * B) := λ n x, ✓{n} x.1 ∧ ✓{n} x.2.
+  Inductive prod_valid' (x : A * B) : Prop :=
+  | Prod_valid : ✓ x.1 → ✓ x.2 → prod_valid' x.
+  Instance prod_valid : Valid (A * B) := prod_valid'.
+  Inductive prod_validN' n (x : A * B) : Prop :=
+  | Prod_validN : ✓{n} x.1 → ✓{n} x.2 → prod_validN' n x.
+  Instance prod_validN : ValidN (A * B) := prod_validN'.
 
   Lemma prod_pcore_Some (x cx : A * B) :
     pcore x = Some cx ↔ pcore (x.1) = Some (cx.1) ∧ pcore (x.2) = Some (cx.2).
@@ -968,7 +972,7 @@ Section prod.
       destruct (cmra_pcore_ne n (x.1) (y.1) (cx.1)) as (z1&->&?); auto.
       destruct (cmra_pcore_ne n (x.2) (y.2) (cx.2)) as (z2&->&?); auto.
       exists (z1,z2); repeat constructor; auto.
-    - by intros n y1 y2 [Hy1 Hy2] [??]; split; rewrite /= -?Hy1 -?Hy2.
+    - by intros n y1 y2 [Hy1 Hy2] [??]; split; rewrite -?Hy1 -?Hy2.
     - intros x; split.
       + intros [??] n; split; by apply cmra_valid_validN.
       + intros Hxy; split; apply cmra_valid_validN=> n; apply Hxy.

algebra/cofe.v

@@ -315,8 +315,7 @@ Section product.
   Definition prod_cofe_mixin : CofeMixin (A * B).
   Proof.
     split.
-    - intros x y; unfold dist, prod_dist, equiv, prod_equiv, prod_relation.
-      rewrite !equiv_dist; naive_solver.
+    - intros x y; split; intro H; constructor; apply equiv_dist; apply H.
     - apply _.
     - by intros n [x1 y1] [x2 y2] [??]; split; apply dist_S.
     - intros n c; split. apply (conv_compl n (chain_map fst c)).

algebra/upred.v

@@ -1058,9 +1058,9 @@ Proof. intros a b [b' ->]. rewrite ownM_op. eauto. Qed.
 
 (* Products *)
 Lemma prod_equivI {A B : cofeT} (x y : A * B) : x ≡ y ⊣⊢ x.1 ≡ y.1 ∧ x.2 ≡ y.2.
-Proof. by unseal. Qed.
+Proof. by unseal; do 2 constructor; intros []; constructor. Qed.
 Lemma prod_validI {A B : cmraT} (x : A * B) : ✓ x ⊣⊢ ✓ x.1 ∧ ✓ x.2.
-Proof. by unseal. Qed.
+Proof. by unseal; do 2 constructor; intros []; constructor. Qed.
 
 (* Later *)
 Lemma later_equivI {A : cofeT} (x y : later A) :

prelude/base.v

@@ -431,8 +431,9 @@ Proof.
     [apply (inj f)|apply (inj g)]; congruence.
 Qed.
 
-Definition prod_relation {A B} (R1 : relation A) (R2 : relation B) :
-  relation (A * B) := λ x y, R1 (x.1) (y.1) ∧ R2 (x.2) (y.2).
+Inductive prod_relation {A B} (R1 : relation A) (R2 : relation B) (x y : A * B)
+  : Prop :=
+| Prod_rel : R1 (x.1) (y.1) → R2 (x.2) (y.2) → prod_relation R1 R2 x y.
 Section prod_relation.
   Context `{R1 : relation A, R2 : relation B}.
   Global Instance prod_relation_refl :