Add value_interp_related1

1 files changed, 20 insertions, 0 deletions

diff --git a/src/Experiments/NewPipeline/RewriterWf1.v b/src/Experiments/NewPipeline/RewriterWf1.v
index 6ec85700a..d91ec0e69 100644
--- a/src/Experiments/NewPipeline/RewriterWf1.v
+++ b/src/Experiments/NewPipeline/RewriterWf1.v
@@ -1327,6 +1327,26 @@ Module Compilers.
                 then UnderLets.interp ident_interp
                 else (fun x => x)).
 
+          Fixpoint value'_interp_related1
+                   {with_lets1 t}
+            : @value' var with_lets1 t
+              -> var t
+              -> Prop
+            := match t return value' _ t -> var t -> Prop with
+               | type.base t
+                 => fun v1 v2
+                    => expr.interp ident_interp (UnderLets_maybe_interp with_lets1 v1)
+                       == v2
+               | type.arrow s d
+                 => fun (f1 : value' _ s -> value' _ d) (f2 : var s -> var d)
+                    => forall x1 x2,
+                        @value'_interp_related1 _ s x1 x2
+                        -> @value'_interp_related1 _ d (f1 x1) (f2 x2)
+               end.
+
+          Definition value_interp_related1 {t} : @value var t -> var t -> Prop
+            := value'_interp_related1.
+
           Fixpoint value'_interp_related
                    {with_lets1 with_lets2 t}
             : @value' var with_lets1 t