Skip to content

Conversation

@strub
Copy link
Member

@strub strub commented Oct 1, 2025

New lemmas: int2bs_strikeE, int2bs_strike_succE

New lemmas: `int2bs_strikeE`, `int2bs_strike_succE`
@strub strub requested a review from a team October 1, 2025 00:13
@strub strub self-assigned this Oct 1, 2025
@strub strub added the library label Oct 1, 2025
@strub strub enabled auto-merge (rebase) October 1, 2025 00:14
Copy link
Contributor

@oskgo oskgo left a comment

Choose a reason for hiding this comment

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

These lemmas look like parts of some induction result. Is that how you're using it? Maybe it would make sense to provide an explicit induction rule as well? In the induction rule k could be left mostly abstract, which would make it a bit cleaner to use.

@strub
Copy link
Member Author

strub commented Oct 1, 2025

Not sure to understand. This lemmas tell you exactly what happens in the binary representation when incrementing by 1. How could k be left abstract?

@fdupress
Copy link
Member

fdupress commented Oct 1, 2025

Not sure to understand. This lemmas tell you exactly what happens in the binary representation when incrementing by 1. How could k be left abstract?

I think you could avoid specifying it exactly as the index of the first 1, and instead prove the result for all k that is the index of a 1 and such that all lower indices contain 0. But this is just a rewrite indexP away, I think. (Swap 0 and 1.)

@strub
Copy link
Member Author

strub commented Oct 1, 2025

"For all k (but there is at most one which is the first index of false or the size of the list if there is no such k)" doesn't make proofs easier. Especially when you use both lemmas and you need to know that they are the same.

@oskgo
Copy link
Contributor

oskgo commented Oct 1, 2025

I'll elaborate. Correct me if I'm wrong, but to me it looks like the main motivation of these lemmas is to use them when you have a statement like forall n, 0 <= n < 2^l => P (int2bs (l+1) n) and want to prove this using induction over n. I think that it should be possible to lift out an induction rule here that does the rewrite with these lemmas in the induction step for you. Something like forall k l, <bounds on k> => <hypothesis on l> => P (nseq k true ++ false :: l) => P (nseq k false ++ true :: l).

I recognize that they're also going to be useful even when you're not doing induction.

EDIT: If your usecase doesn't look anything like this you can ignore my remark.

@strub
Copy link
Member Author

strub commented Oct 1, 2025

I am using them in a hoare proof (in a while loop). So yes, there is an induction, but not at the ambient logic level.

Copy link
Contributor

@oskgo oskgo left a comment

Choose a reason for hiding this comment

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

Fair enough. Looks good to me. Approved.

@strub strub merged commit cda7fdf into main Oct 1, 2025
15 checks passed
@strub strub deleted the bs2int_strike branch October 1, 2025 12:10
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

Projects

None yet

Development

Successfully merging this pull request may close these issues.

4 participants