Changed reduction to mirror behaviour of native Rocq encodings#64
Merged
fblanqui merged 6 commits intoJul 8, 2026
Merged
Conversation
- removed Rocq incompatible rewrite rules - fixed proofs - moved the rules to dedicated file Reduction.lp
fblanqui
requested changes
Jun 29, 2026
fblanqui
left a comment
fblanqui
left a comment
Member
There was a problem hiding this comment.
Thank you Melanie. Just a few details to change.
Contributor
Author
Good catches, thank you! I made the changes. |
fblanqui
requested changes
Jun 30, 2026
| ### Changed | ||
|
|
||
| - Removed/ changed rewrite rules to match the native Rocq encodings | ||
| - Reintroduced the original rules in Reduction.lp |
Member
There was a problem hiding this comment.
Hi Melanie. I propose to have only one line: moved the rewrite rules that do not derive from the Rocq Stdlib definition to the file ExtraRules.lp.
| The rules given here all correspond to proved equalities in their corresponding file. | ||
| They were removed to increase the compatibility with native Rocq encodings. | ||
| */ | ||
|
|
Member
There was a problem hiding this comment.
I propose to rename the file to ExtraRules.lp and move the require commands as follows:
// rules from Bool
require Stdlib.Bool as B;
rule _ B.or B.true ↪ B.true
with $b B.or B.false ↪ $b;
// rules from Nat
require Stdlib.Nat as N;
...
Member
|
There are warnings related to Deducteam/lambdapi#1433. |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
This PR adapts the Lambdapi standard library to make its definitions more directly compatible with Rocq’s native reduction behavior during export.
Main changes:
Bool,Nat,List,Pos, andZso they match the symbolic computation performed by the corresponding Rocq primitives.Reduction.lp; these correspond to equalities proved in the relevant stdlib files and can be required explicitly by Lambdapi developments that need the former computational behavior.