Generalize type.eqv a bit

4 files changed, 13 insertions, 10 deletions

diff --git a/src/Experiments/NewPipeline/AbstractInterpretationProofs.v b/src/Experiments/NewPipeline/AbstractInterpretationProofs.v
index 60007288f..5c20da75b 100644
--- a/src/Experiments/NewPipeline/AbstractInterpretationProofs.v
+++ b/src/Experiments/NewPipeline/AbstractInterpretationProofs.v
@@ -51,7 +51,7 @@ Module Compilers.
         (Hwf : Wf E)
         (b_in : type.for_each_lhs_of_arrow ZRange.type.option.interp t)
     : forall arg1 arg2
-        (Harg12 : type.and_for_each_lhs_of_arrow (@type.eqv _ _) arg1 arg2)
+        (Harg12 : type.and_for_each_lhs_of_arrow (@type.eqv) arg1 arg2)
         (Harg1 : type.andb_bool_for_each_lhs_of_arrow (@ZRange.type.option.is_bounded_by) b_in arg1 = true),
       type.app_curried (Interp (PartialEvaluateWithListInfoFromBounds E b_in)) arg1 = type.app_curried (Interp E) arg2.
   Proof.
@@ -70,7 +70,7 @@ Module Compilers.
           (b_out : ZRange.type.base.option.interp (type.final_codomain t))
           rv (Hrv : CheckedPartialEvaluateWithBounds relax_zrange E b_in b_out = inl rv)
     : forall arg1 arg2
-             (Harg12 : type.and_for_each_lhs_of_arrow (@type.eqv _ _) arg1 arg2)
+             (Harg12 : type.and_for_each_lhs_of_arrow (@type.eqv) arg1 arg2)
              (Harg1 : type.andb_bool_for_each_lhs_of_arrow (@ZRange.type.option.is_bounded_by) b_in arg1 = true),
       ZRange.type.base.option.is_bounded_by b_out (type.app_curried (Interp rv) arg1) = true
       /\ forall cast_outside_of_range, type.app_curried (expr.Interp (@ident.gen_interp cast_outside_of_range) rv) arg1
diff --git a/src/Experiments/NewPipeline/Language.v b/src/Experiments/NewPipeline/Language.v
index 6c31dd0d9..5fa3a25bd 100644
--- a/src/Experiments/NewPipeline/Language.v
+++ b/src/Experiments/NewPipeline/Language.v
@@ -104,12 +104,15 @@ Module Compilers.
          | arrow s d => @interp _ base_interp s -> @interp _ base_interp d
          end.
 
-    Fixpoint eqv {base_type} {base_interp : base_type -> Type} {t : type base_type} : relation (interp base_interp t)
+    Fixpoint related {base_type} {base_interp : base_type -> Type} (R : forall t, relation (base_interp t)) {t : type base_type}
+      : relation (interp base_interp t)
       := match t with
-         | base t => @eq (base_interp t)
-         | arrow s d => @eqv _ base_interp s ==> @eqv _ base_interp d
+         | base t => R t
+         | arrow s d => @related _ _ R s ==> @related _ _ R d
          end%signature.
 
+    Notation eqv := (@related _ _ (fun _ => eq)).
+
     Fixpoint app_curried {base_type} {f : base_type -> Type} {t : type base_type}
       : interp f t -> for_each_lhs_of_arrow (interp f) t -> f (final_codomain t)
       := match t with
diff --git a/src/Experiments/NewPipeline/LanguageWf.v b/src/Experiments/NewPipeline/LanguageWf.v
index 4f4a2f473..009396770 100644
--- a/src/Experiments/NewPipeline/LanguageWf.v
+++ b/src/Experiments/NewPipeline/LanguageWf.v
@@ -33,7 +33,7 @@ Module Compilers.
   Module type.
     Section eqv.
       Context {base_type} {interp_base_type : base_type -> Type}.
-      Local Notation eqv := (@type.eqv base_type interp_base_type).
+      Local Notation eqv := (@type.related base_type interp_base_type (fun _ => eq)).
 
       Global Instance eqv_Symmetric {t} : Symmetric (@eqv t) | 10.
       Proof. induction t; cbn [type.eqv type.interp] in *; repeat intro; eauto. Qed.
@@ -62,7 +62,7 @@ Hint Extern 10 (Proper ?R ?x) => simple eapply (@PER_valid_r _ R); [ | | solve [
 >>
 *)
       Lemma app_curried_Proper {t}
-        : Proper (@type.eqv base_type base_interp t ==> type.and_for_each_lhs_of_arrow (@type.eqv _ _) ==> eq)
+        : Proper (@type.related base_type base_interp (fun _ => eq) t ==> type.and_for_each_lhs_of_arrow (@type.eqv) ==> eq)
                  (@type.app_curried base_type base_interp t).
       Proof.
         cbv [Proper respectful]; induction t; cbn [type.eqv type.app_curried]; cbv [Proper respectful]; [ intros; subst; reflexivity | ].
diff --git a/src/Experiments/NewPipeline/Toplevel1.v b/src/Experiments/NewPipeline/Toplevel1.v
index bec153f53..476bcb7fc 100644
--- a/src/Experiments/NewPipeline/Toplevel1.v
+++ b/src/Experiments/NewPipeline/Toplevel1.v
@@ -788,7 +788,7 @@ Module Pipeline.
                        | None => True
                        end)
     : forall arg1 arg2
-             (Harg12 : type.and_for_each_lhs_of_arrow (@type.eqv _ _) arg1 arg2)
+             (Harg12 : type.and_for_each_lhs_of_arrow (@type.eqv) arg1 arg2)
              (Harg1 : type.andb_bool_for_each_lhs_of_arrow (@ZRange.type.option.is_bounded_by) arg_bounds arg1 = true),
       ZRange.type.base.option.is_bounded_by out_bounds (type.app_curried (Interp rv) arg1) = true
       /\ forall cast_outside_of_range, type.app_curried (expr.Interp (@ident.gen_interp cast_outside_of_range) rv) arg1
@@ -832,7 +832,7 @@ Module Pipeline.
              (InterpE : type.interp base.interp t)
              (rv : Expr t)
     := forall arg1 arg2
-              (Harg12 : type.and_for_each_lhs_of_arrow (@type.eqv _ _) arg1 arg2)
+              (Harg12 : type.and_for_each_lhs_of_arrow (@type.eqv) arg1 arg2)
               (Harg1 : type.andb_bool_for_each_lhs_of_arrow (@ZRange.type.option.is_bounded_by) arg_bounds arg1 = true),
       ZRange.type.base.option.is_bounded_by out_bounds (type.app_curried (Interp rv) arg1) = true
       /\ forall cast_outside_of_range, type.app_curried (expr.Interp (@ident.gen_interp cast_outside_of_range) rv) arg1
@@ -858,7 +858,7 @@ Module Pipeline.
         (InterpE : type.interp base.interp t)
         (InterpE_correct_and_Wf
          : (forall arg1 arg2
-                   (Harg12 : type.and_for_each_lhs_of_arrow (@type.eqv _ _) arg1 arg2)
+                   (Harg12 : type.and_for_each_lhs_of_arrow (@type.eqv) arg1 arg2)
                    (Harg1 : type.andb_bool_for_each_lhs_of_arrow (@ZRange.type.option.is_bounded_by) arg_bounds arg1 = true),
                type.app_curried (Interp e) arg1 = type.app_curried InterpE arg2)
            /\ Wf e)