Skip to content

GitLab

  • Menu
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 148
    • Issues 148
    • List
    • Boards
    • Service Desk
    • Milestones
  • Merge requests 9
    • Merge requests 9
  • CI/CD
    • CI/CD
    • Pipelines
    • Jobs
    • Schedules
  • Deployments
    • Deployments
    • Environments
    • Releases
  • Monitor
    • Monitor
    • Incidents
  • Analytics
    • Analytics
    • Value stream
    • CI/CD
    • Repository
  • Wiki
    • Wiki
  • Activity
  • Graph
  • Create a new issue
  • Jobs
  • Commits
  • Issue Boards
Collapse sidebar
  • Iris
  • IrisIris
  • Merge requests
  • !483

Closed
Created Jul 22, 2020 by Tej Chajed@tchajedMaintainer
  • Report abuse
Report abuse

Support destructing exists with intro patterns

  • Overview 30
  • Commits 2
  • Changes 3

The syntax re-uses the existing support for pure names, namely the % and %H patterns. Using "[% H]" is like iDestruct ... as (?) "H" and using "[%x H]" (with the string-ident plugin) is like iDestruct ... as (x) "H".

This changes how these patterns are parsed. Previously, both would have been handled as conjunctions (using IntoAnd or IntoSep, depending on whether the hypothesis is persistent or not). This means it was possible for the user to use "[% H]" to destruct a pure hypothesis ⌜φ ∧ ψ⌝ and put only the first conjunct in the Gallina context, leaving the other one in the IPM; such patterns will now break, since iExistDestruct cannot handle this use case.

As a probably-mostly-complete solution, this MR special-cases "[% %]" (and similar patterns that name the hypotheses) to continue to use iAndDestruct, since most likely this would be the pattern used in existing code and not the unusual asymmetric "[% H]".

If we work this out it would fix #310 (closed) without new syntax.

Edited Dec 05, 2020 by Tej Chajed
Assignee
Assign to
Reviewer
Request review from
Time tracking
Source branch: exists-intro-pattern