Skip to content
GitLab
Projects Groups Snippets
  • /
  • Help
    • Help
    • Support
    • Community forum
    • Submit feedback
    • Contribute to GitLab
  • Sign in / Register
  • Iris Iris
  • Project information
    • Project information
    • Activity
    • Labels
    • Members
  • Repository
    • Repository
    • Files
    • Commits
    • Branches
    • Tags
    • Contributors
    • Graph
    • Compare
  • Issues 170
    • Issues 170
    • List
    • Boards
    • Service Desk
    • Milestones
  • Merge requests 22
    • Merge requests 22
  • CI/CD
    • CI/CD
    • Pipelines
    • Jobs
    • Schedules
  • Deployments
    • Deployments
    • Releases
  • Analytics
    • Analytics
    • Value stream
    • CI/CD
    • Repository
  • Wiki
    • Wiki
  • Activity
  • Graph
  • Create a new issue
  • Jobs
  • Commits
  • Issue Boards
Collapse sidebar
  • Iris
  • IrisIris
  • Issues
  • #229
Closed
Open
Issue created Feb 20, 2019 by Daniel Gratzer@jozefg

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?

Assignee
Assign to
Time tracking