Skip to content
GitLab
Projects Groups Topics Snippets
  • /
  • Help
    • Help
    • Support
    • Community forum
    • Submit feedback
    • Contribute to GitLab
  • Register
  • Sign in
  • Iris Iris
  • Project information
    • Project information
    • Activity
    • Labels
    • Members
  • Repository
    • Repository
    • Files
    • Commits
    • Branches
    • Tags
    • Contributor statistics
    • Graph
    • Compare revisions
  • Issues 173
    • Issues 173
    • List
    • Boards
    • Service Desk
    • Milestones
  • Merge requests 21
    • Merge requests 21
  • 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
  • #93
Closed
Open
Issue created Aug 14, 2017 by Ghost User@ghostContributor

Using wp_ tactics without making every tiny step a function is super slow solely because Coq has to keep proving this Closed obligation

Which would be fine, except that there is no good way right now to prove closed-ness under a binder without knowing string literals for the variable names.

Concrete example:

  Definition big_blob_of_code x :=
    (* huge blob of code here *)%E.

  Definition foo: val :=
    (λ: [ "x"; "y" ], big_blob_of_code "x" + big_blob_code "y").

I don't want big_blob_of_code to be a function (because it isn't in the source code, and I'd like to actually verify foo as written rather than some other thing). However, Coq takes far too long to execute wp_rec on my foo-like thing, and it only gets worse the more times it is called. It also requires an irritating number of rewrites. There may be some ways around this if you happen to have some closed values somewhere up the stack and use Notation for previous ones, with a typeclass instance for Closed for those functions, but even that is highly annoying, and proving Closed for any of the lower-level functions doesn't really work because of the way solve_closed is defined (and according to Janno, probably just can't work at all).

I don't really care what solution this has, just that there is one.

Edited Aug 22, 2017 by Ralf Jung
Assignee
Assign to
Time tracking