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 24
    • Merge requests 24
  • 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
  • #174
Closed
Open
Issue created Mar 19, 2018 by Robbert Krebbers@robbertkrebbersMaintainer

Confusing result by `wp_op`

As reported in private by @birkedal:

From iris.program_logic Require Export weakestpre.
From iris.heap_lang Require Import proofmode notation.
Set Default Proof Using "Type".

Definition test `{heapG Σ} (n : nat) (v : val) :
  (WP if: #n = v then #true else #false {{ _, True }})%I.
Proof.
  wp_op.

This gives

bin_op_eval EqOp #n v = Some ?Goal0
______________________________________(2/2)
--------------------------------------∗
WP if: ?Goal0 then #true else #false {{ _, True }}

Pre !97 (merged) this used to work because bin_op_eval used to match first on the operations and then on the operand. Right now, it first matches on the operands, and only then on the operation.

Assignee
Assign to
Time tracking