diff options
author | Jason Gross <jgross@mit.edu> | 2019-04-04 17:53:03 -0400 |
---|---|---|
committer | Jason Gross <jgross@mit.edu> | 2019-04-04 17:53:03 -0400 |
commit | 145c680cc0c64780ff9cb58944565121daeb577a (patch) | |
tree | dc9a77a1351d6e57f88dc0a7a4e0c482ff3ff119 /src | |
parent | e0c9b5f803e63a91922cc0724119d39da0f24379 (diff) |
Add some more underlets lemmas
Diffstat (limited to 'src')
-rw-r--r-- | src/UnderLetsProofs.v | 27 |
1 files changed, 27 insertions, 0 deletions
diff --git a/src/UnderLetsProofs.v b/src/UnderLetsProofs.v index ccb872a44..015304fb2 100644 --- a/src/UnderLetsProofs.v +++ b/src/UnderLetsProofs.v @@ -527,6 +527,24 @@ Module Compilers. reflexivity. Qed. + Lemma of_expr_interp_related_gen_iff (R : forall t, var t -> type.interp base_interp t -> Prop) {t e v} + : interp_related_gen R (expr.interp_related_gen ident_interp R (t:=t)) (UnderLets.of_expr e) v + <-> expr.interp_related_gen ident_interp R e v. + Proof using Type. + revert v; induction e; cbn [UnderLets.of_expr interp_related_gen expr.interp_related_gen]; try reflexivity. + setoid_rewrite H. + reflexivity. + Qed. + + Global Instance interp_related_gen_Proper_impl {T1 T2 R} + : Proper (pointwise_relation _ (pointwise_relation _ Basics.impl) ==> eq ==> eq ==> Basics.impl) (@interp_related_gen T1 T2 R) | 10. + Proof using Type. + cbv [pointwise_relation respectful Proper]. + intros R1 R2 HR x y ? x' y' H'; subst y y'. + revert x'; induction x; [ apply HR | ]; cbn [interp_related_gen]. + setoid_rewrite H; reflexivity. + Qed. + Global Instance interp_related_gen_Proper_iff {T1 T2 R} : Proper (pointwise_relation _ (pointwise_relation _ iff) ==> eq ==> eq ==> iff) (@interp_related_gen T1 T2 R) | 10. Proof using Type. @@ -788,6 +806,15 @@ Module Compilers. <-> expr.interp_related ident_interp (UnderLets.to_expr e) v. Proof using Type. apply to_expr_interp_related_gen_iff. Qed. + Lemma of_expr_interp_related_iff {t e v} + : interp_related (expr.interp_related ident_interp (t:=t)) (UnderLets.of_expr e) v + <-> expr.interp_related ident_interp e v. + Proof using Type. apply of_expr_interp_related_gen_iff. Qed. + + Global Instance interp_related_Proper_impl {T1 T2} + : Proper (pointwise_relation _ (pointwise_relation _ Basics.impl) ==> eq ==> eq ==> Basics.impl) (@interp_related T1 T2) | 10. + Proof using Type. apply interp_related_gen_Proper_impl. Qed. + Global Instance interp_related_Proper_iff {T1 T2} : Proper (pointwise_relation _ (pointwise_relation _ iff) ==> eq ==> eq ==> iff) (@interp_related T1 T2) | 10. Proof using Type. apply interp_related_gen_Proper_iff. Qed. |