diff options
author | Jason Gross <jgross@mit.edu> | 2019-04-05 01:19:24 -0400 |
---|---|---|
committer | Jason Gross <jgross@mit.edu> | 2019-04-05 01:19:24 -0400 |
commit | 2172994d31ffc63bb27bc558d2861285fba45e40 (patch) | |
tree | cf0fb567824941937592ec72a90496ab324a5d9d /src/UnderLetsProofs.v | |
parent | 145c680cc0c64780ff9cb58944565121daeb577a (diff) |
Add interp_related lemmas
Diffstat (limited to 'src/UnderLetsProofs.v')
-rw-r--r-- | src/UnderLetsProofs.v | 10 |
1 files changed, 10 insertions, 0 deletions
diff --git a/src/UnderLetsProofs.v b/src/UnderLetsProofs.v index 015304fb2..457c0e596 100644 --- a/src/UnderLetsProofs.v +++ b/src/UnderLetsProofs.v @@ -965,6 +965,16 @@ Module Compilers. : @interp_related A B R1 e v -> @interp_related A B' R2 e (f v). Proof using Type. now apply interp_related_gen_Proper_impl_same_UnderLets. Qed. + + Lemma eqv_of_interp_related {t e v} + : interp_related (expr.interp_related (@ident_interp)) e v + -> @type.eqv t (expr.interp ident_interp (interp e)) v. + Proof using Type. + induction e; cbn [interp_related interp_related_gen interp type.related]; intros; destruct_head'_ex; destruct_head'_and; subst. + { now apply expr.eqv_of_interp_related. } + { repeat match goal with H : _ |- _ => apply H end. + now apply expr.eqv_of_interp_related. } + Qed. End for_interp. Section for_interp2. |