Merge pull request #134 from JasonGross/give-eqv-hyp

Provide a convenience hypothesis with eqv assumptions in rewrite rules side-conditions
mit-plv · Dec 23, 2023 · 604362b · 604362b
2 parents 44552d2 + 140c565
commit 604362b
Show file tree

Hide file tree

Showing 2 changed files with 8 additions and 2 deletions.
diff --git a/src/Rewriter/Rewriter/ProofsCommon.v b/src/Rewriter/Rewriter/ProofsCommon.v
@@ -3104,7 +3104,7 @@ Module Compilers.
                      {t} {p : pattern t} (r : @rewrite_rule_data t p)
             : Prop
             := under_with_unification_resultT_relation_hetero
-                 (fun _ => value_interp_related)
+                 (fun _ e v => value_interp_related e v /\ Proper type.eqv v)
                  (fun evm => deep_rewrite_ruleTP_gen_good_relation)
                  (rew_replacement r)
                  (pattern_default_interp p).
@@ -3151,7 +3151,12 @@ Module Compilers.
             intro H.
             repeat (let x := fresh "x" in intro x; specialize (H x)).
             intros X Y HXY.
-            pose proof (related_app_with_unification_resultT _ _ _ _ _ _ ltac:(eassumption) HXY) as H'.
+            assert (HYY : related_unification_resultT
+                            (fun _ e v => value_interp_related e v /\ Proper type.eqv v) X Y).
+            { eapply map_related_unification_resultT; [ | exact HXY ].
+              cbv beta; intros; split; try assumption.
+              eapply eqv_iff_value_interp_related1; eexists; eassumption. }
+            pose proof (related_app_with_unification_resultT _ _ _ _ _ _ ltac:(eassumption) HYY).
             progress cbv [deep_rewrite_ruleTP_gen] in *.
             match goal with
             | [ H : option_eq ?R ?x ?y |- option_eq ?R' ?x' ?y' ]

diff --git a/src/Rewriter/Rewriter/ProofsCommonTactics.v b/src/Rewriter/Rewriter/ProofsCommonTactics.v
@@ -417,6 +417,7 @@ Module Compilers.
                   => destruct (invert_expr.reflect_list ls) eqn:?
                 | [ |- context G[expr.interp_related_gen ?ident_interp (fun t : ?T => ?vii t ?b)] ]
                   => progress change (fun t : T => vii t b) with (fun t : T => @Compile.value_interp_related _ _ _ ident_interp t b)
+                | [ H : _ /\ Proper _ _ |- _ ] => destruct H
                 end ].
       Ltac preprocess base_interp_head := repeat preprocess_step base_interp_head.