Actually give access to the Proper type.eqv hyp

It's a bit kludgy to stuff it in an `and`, but I didn't want to make the change too invasive right now. :-/
mit-plv · Dec 23, 2023 · 140c565 · 140c565
1 parent 05216ca
commit 140c565
Show file tree

Hide file tree

Showing 3 changed files with 11 additions and 14 deletions.
diff --git a/src/Rewriter/Rewriter/InterpProofs.v b/src/Rewriter/Rewriter/InterpProofs.v
@@ -938,7 +938,7 @@ Module Compilers.
               v
               (H : rawexpr_interp_related (rApp r1 r2 (t:=t) alt) v)
           : rawexpr_interp_related (rApp r1' r2' (t:=t) alt) v.
-        Proof using Type.
+        Proof.
           cbn [rawexpr_interp_related] in *;
             repeat first [ assumption
                          | break_innermost_match_step
@@ -1237,14 +1237,7 @@ Module Compilers.
                        | match goal with
                          | [ H : unify_pattern _ _ _ _ _ = Some _ |- _ ] => eapply interp_unify_pattern in H; [ | eassumption | eassumption ]
                          | [ H : unification_resultT_interp_related _ _, Hrewr : rewrite_rule_data_interp_goodT _ |- _ ]
-                           => specialize (Hrewr _ _ H);
-                              let T := lazymatch type of Hrewr with ?T -> _ => T end in
-                              cut T;
-                              [ let H' := fresh in
-                                intro H'; specialize (Hrewr H')
-                              | eapply map_related_unification_resultT; [ | refine H ];
-                                cbv [Proper]; intros; eapply eqv_iff_value_interp_related1;
-                                eexists; eassumption ]
+                           => specialize (Hrewr _ _ H)
                          | [ H : option_eq _ ?x ?y, H' : ?x' = Some _ |- _ ]
                            => change x with x' in H; rewrite H' in H;
                               destruct y eqn:?; cbn [option_eq] in H

diff --git a/src/Rewriter/Rewriter/ProofsCommon.v b/src/Rewriter/Rewriter/ProofsCommon.v
@@ -3083,8 +3083,6 @@ Module Compilers.
             : Prop
             := forall x y,
               related_unification_resultT (fun t => value_interp_related) x y
-              (* this next one is for convenience only *)
-              -> related_unification_resultT (fun t _ v => Proper type.eqv v) x y
               -> option_eq
                    (fun fx gy
                     => related_sigT_by_eq
@@ -3106,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).
@@ -3152,8 +3150,13 @@ Module Compilers.
             cbv [rewrite_rule_data_interp_goodT rewrite_rule_data_interp_goodT_curried].
             intro H.
             repeat (let x := fresh "x" in intro x; specialize (H x)).
-            intros X Y HXY HYY.
-            pose proof (related_app_with_unification_resultT _ _ _ _ _ _ ltac:(eassumption) HXY) as H'.
+            intros X Y HXY.
+            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.