From 05216ca1fbf783f6241dbf67083a8c3bee0134ad Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Fri, 22 Dec 2023 20:03:38 -0500 Subject: [PATCH 1/2] Provide a convenience hypothesis with eqv assumptions --- src/Rewriter/Rewriter/InterpProofs.v | 11 +++++++++-- src/Rewriter/Rewriter/ProofsCommon.v | 4 +++- 2 files changed, 12 insertions(+), 3 deletions(-) diff --git a/src/Rewriter/Rewriter/InterpProofs.v b/src/Rewriter/Rewriter/InterpProofs.v index 6f95a026f..89d8a1cb5 100644 --- 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. + Proof using Type. cbn [rawexpr_interp_related] in *; repeat first [ assumption | break_innermost_match_step @@ -1237,7 +1237,14 @@ 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) + => 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 ] | [ 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 index 6aebfc2d6..51c51d49c 100644 --- a/src/Rewriter/Rewriter/ProofsCommon.v +++ b/src/Rewriter/Rewriter/ProofsCommon.v @@ -3083,6 +3083,8 @@ 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 @@ -3150,7 +3152,7 @@ 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. + intros X Y HXY HYY. pose proof (related_app_with_unification_resultT _ _ _ _ _ _ ltac:(eassumption) HXY) as H'. progress cbv [deep_rewrite_ruleTP_gen] in *. match goal with From 140c5654c3ba255b13349a8364b0d8fb8df459b4 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Fri, 22 Dec 2023 20:34:58 -0500 Subject: [PATCH 2/2] 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. :-/ --- src/Rewriter/Rewriter/InterpProofs.v | 11 ++--------- src/Rewriter/Rewriter/ProofsCommon.v | 13 ++++++++----- src/Rewriter/Rewriter/ProofsCommonTactics.v | 1 + 3 files changed, 11 insertions(+), 14 deletions(-) diff --git a/src/Rewriter/Rewriter/InterpProofs.v b/src/Rewriter/Rewriter/InterpProofs.v index 89d8a1cb5..6f95a026f 100644 --- 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 index 51c51d49c..492ee6051 100644 --- 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 index fadb8c707..162add0ab 100644 --- 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.