Odd Behavior for Substitution
Hello,
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 tryset
and check
even though they both depend on "x"
. However, when proving some properties about mk_oneshot
substituting "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?