Odd Behavior for Substitution
Simon noticed a somewhat odd occurrence with substitution today. Apparently values are no longer required to be closed (?) but defining a value which is open seems to break substitution in a confusing way?
Definition tryset : val := λ: "n", CAS "x" NONE (SOME "n"). Definition check : val := λ: <>, let: "y" := !"x" in λ: <>, match: "y" with NONE => #() | SOME "n" => match: !"x" with NONE => assert: #false | SOME "m" => assert: "n" = "m" end end. Definition mk_oneshot : val := λ: <>, let: "x" := ref NONE in (tryset, check).
With this example program we have separated out
check even though they both depend on
"x". However, when proving some properties about
"x" for a new location
#l does not replace
"x in either.
This behavior is demonstrated by the attached file: oneshot.v. Am I missing something obvious here?