GitLab

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?