diff options
author | Jason Gross <jgross@mit.edu> | 2018-11-15 17:22:48 -0500 |
---|---|---|
committer | Jason Gross <jgross@mit.edu> | 2018-11-15 17:22:48 -0500 |
commit | 5549dcda8833de957efa14cd59fe22f2a33de683 (patch) | |
tree | a67f6fc2b7196dd907aacd1334d7eacaa2cd603b | |
parent | 3dc52eb8beb2d36d42245991db56766e2d181d5f (diff) |
Add a couple of useful lemmas
-rw-r--r-- | src/Experiments/NewPipeline/RewriterWf1.v | 28 |
1 files changed, 28 insertions, 0 deletions
diff --git a/src/Experiments/NewPipeline/RewriterWf1.v b/src/Experiments/NewPipeline/RewriterWf1.v index cedd56dc0..c37910fe4 100644 --- a/src/Experiments/NewPipeline/RewriterWf1.v +++ b/src/Experiments/NewPipeline/RewriterWf1.v @@ -1319,6 +1319,15 @@ Module Compilers. := { pf : projT1 x = projT1 y | R _ (rew pf in projT2 x) (projT2 y) }. + Definition map_related_sigT_by_eq {A P1 P2} {R1 R2 : forall x : A, P1 x -> P2 x -> Prop} + (HR : forall x v1 v2, R1 x v1 v2 -> R2 x v1 v2) + (x : @sigT A P1) (y : @sigT A P2) + : @related_sigT_by_eq A P1 P2 R1 x y -> @related_sigT_by_eq A P1 P2 R2 x y. + Proof using Type. + destruct x, y; cbv [related_sigT_by_eq projT1 projT2]. + intro H; exists (proj1_sig H); apply HR, (proj2_sig H). + Qed. + Definition related_unification_resultT (R : forall t, @value var1 t -> @value var2 t -> Prop) {t p} : @unification_resultT1 t p -> @unification_resultT2 t p -> Prop := related_sigT_by_eq (@related_unification_resultT' R t p). @@ -1454,6 +1463,25 @@ Module Compilers. (@app_with_unification_resultT_cps _ t p K2 f2 v2 _ (@Some _)). Proof using Type. apply related_app_with_unification_resultT. Qed. + Definition map_related_unification_resultT' {R1 R2 : forall t : type, value t -> value t -> Prop} + (HR : forall t v1 v2, R1 t v1 v2 -> R2 t v1 v2) + {t p evm v1 v2} + : @related_unification_resultT' R1 t p evm v1 v2 + -> @related_unification_resultT' R2 t p evm v1 v2. + Proof using Type. + induction p; cbn [related_unification_resultT']; intuition auto. + Qed. + + Definition map_related_unification_resultT {R1 R2 : forall t : type, value t -> value t -> Prop} + (HR : forall t v1 v2, R1 t v1 v2 -> R2 t v1 v2) + {t p v1 v2} + : @related_unification_resultT R1 t p v1 v2 + -> @related_unification_resultT R2 t p v1 v2. + Proof using Type. + cbv [related_unification_resultT]; apply map_related_sigT_by_eq; intros *. + apply map_related_unification_resultT'; auto. + Qed. + Definition wf_maybe_do_again_expr {t} {rew_should_do_again1 rew_should_do_again2 : bool} |