Skip to content

Add tactic for lossless while #669

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom
Merged
merged 1 commit into from
Aug 7, 2025
Merged

Add tactic for lossless while #669

merged 1 commit into from
Aug 7, 2025

Conversation

lyonel2017
Copy link
Contributor

@lyonel2017 lyonel2017 commented Dec 11, 2024 •
edited
Loading

Add tactic for one-sided while rule with lossless proof:

    {I} while b do c {T}   {I}c{I}   P => I /\ (not b => I => Q)
    ------------------------------------------------------------
                 {P} while b do c ~ skip {Q}

    {I} while b do c {T}   {I}c{I}   P => I /\ (not b => I => Q)
    ------------------------------------------------------------
                 {P} skip ~ while b do c {Q}

@strub
Copy link
Member

strub commented Dec 18, 2024

Restarting the CI.

@strub strub force-pushed the feature-lossless-while branch from 7c41c72 to f27a007 Compare December 23, 2024 09:20
@strub strub marked this pull request as draft December 23, 2024 09:25
@strub strub changed the title WIP: Add tactic for lossless while Add tactic for lossless while Dec 23, 2024
@lyonel2017 lyonel2017 force-pushed the feature-lossless-while branch from f27a007 to 0173967 Compare December 23, 2024 11:12
@lyonel2017 lyonel2017 force-pushed the feature-lossless-while branch from 0173967 to 54cb0d0 Compare January 21, 2025 15:59
@lyonel2017 lyonel2017 marked this pull request as ready for review January 21, 2025 16:02
@fdupress fdupress requested a review from strub May 2, 2025 12:03
@strub strub self-assigned this Jul 4, 2025
strub
strub requested changes Aug 6, 2025
View reviewed changes
Copy link
Member

@strub strub left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Just add a description in the PR. This is use for generating the ChangeLog.

@lyonel2017
Add one sided while rule with lossless proof:
17260fa 
{I} while b do c {T}   {I}c{I}   P => I /\ (not b => I => Q)
-------------------------------------------------------------
             {P} while b do c ~ skip {Q}

{I} while b do c {T}   {I}c{I}   P => I /\ (not b => I => Q)
-------------------------------------------------------------
             {P} skip ~ while b do c {Q}
@lyonel2017 lyonel2017 force-pushed the feature-lossless-while branch from 54cb0d0 to 17260fa Compare August 6, 2025 23:19
@lyonel2017 lyonel2017 requested a review from strub August 7, 2025 09:18
@strub strub merged commit e6c14f7 into main Aug 7, 2025
15 checks passed
@strub strub deleted the feature-lossless-while branch August 7, 2025 13:47
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@strub strub strub approved these changes

Assignees

@strub strub

Labels
enhancement
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
2 participants
@lyonel2017 @strub