PrincetonUniversity / VST

Verified Software Toolchain
https://vst.cs.princeton.edu
Other
425 stars 91 forks source link

subsumespec_app1, subsumespec_app2 #660

Closed andrew-appel closed 1 year ago

andrew-appel commented 1 year ago

In floyd/forward.v, the lemmas subsumespec_app1 and subsumespec_app1 take forever. Same for tycontext_sub_Gprog_app1, tycontext_sub_Gprog_app2.

Perhaps with explicitly instantiated arguments to funspec_sub_si_refl, these lemmas would be instantaneous.

andrew-appel commented 1 year ago

Solution: apply seplog.funspec_sub_si_refl instead of apply funspec_sub_si_refl. I've fixed this in a branch that may or may not make into master someday, but this fix can also be applied independently at any time.