[Merged by Bors] - feat: port cc tactic (2/3)#11960
Closed
Conversation
1 task
Vierkantor
reviewed
May 14, 2024
Contributor
Vierkantor
left a comment
There was a problem hiding this comment.
Some further comments.
Observation: many procedures iterate over a collection of objects and index through pureIsDefEq. This can likely be optimized in future PRs using keyed matching in a discrimination tree, but is not a concern for the current implementation.
Contributor
|
Overall the documentation is very good, most suggestions are for style issues. Good work! |
Vierkantor
reviewed
May 15, 2024
Contributor
Vierkantor
left a comment
There was a problem hiding this comment.
Done with the review! Thank you so much for the work in porting and commenting the code.
Mathlib/Tactic/CC/Addition.lean
Outdated
Comment on lines
+1188
to
+1192
| /-- Internalize `e` so that the AC module can deal with the given expression. -/ | ||
| def internalizeAC (e : Expr) (parent? : Option Expr) : CCM Unit := do | ||
| let some op ← isAC e | return | ||
| let parentOp? ← parent?.casesOn (pure none) isAC | ||
| if parentOp?.any (op == ·) then return |
Contributor
There was a problem hiding this comment.
I'm not sure what the check on lines 1191-1192 is supposed to do, could you verify?
Suggested change
| /-- Internalize `e` so that the AC module can deal with the given expression. -/ | |
| def internalizeAC (e : Expr) (parent? : Option Expr) : CCM Unit := do | |
| let some op ← isAC e | return | |
| let parentOp? ← parent?.casesOn (pure none) isAC | |
| if parentOp?.any (op == ·) then return | |
| /-- Internalize `e` so that the AC module can deal with the given expression. | |
| If the expression does not contain an AC operator, or the parent expression | |
| is already processed by `internalizeAC`, this operation does nothing. | |
| -/ | |
| def internalizeAC (e : Expr) (parent? : Option Expr) : CCM Unit := do | |
| let some op ← isAC e | return | |
| let parentOp? ← parent?.casesOn (pure none) isAC | |
| if parentOp?.any (op == ·) then return |
Contributor
Author
There was a problem hiding this comment.
If the binary AC operatior in parent expression is the same to one in e, stop the process.
Contributor
|
Thanks! Let's get this merged 🥳 bors r+ |
mathlib-bors bot
pushed a commit
that referenced
this pull request
May 15, 2024
In this PR, we implements process when an new equation is added to a congruence closure. Also, `Lean.Expr.relSidesIfSymm?` is removed in #11162, but this def is required for `cc` tactic, so we recover this. Co-authored-by: Pol'tta / Miyahara Kō <52843868+Komyyy@users.noreply.github.com>
Contributor
|
Pull request successfully merged into master. Build succeeded: |
cc tactic (2/3)cc tactic (2/3)
callesonne
pushed a commit
that referenced
this pull request
May 16, 2024
In this PR, we implements process when an new equation is added to a congruence closure. Also, `Lean.Expr.relSidesIfSymm?` is removed in #11162, but this def is required for `cc` tactic, so we recover this. Co-authored-by: Pol'tta / Miyahara Kō <52843868+Komyyy@users.noreply.github.com>
grunweg
pushed a commit
that referenced
this pull request
May 17, 2024
In this PR, we implements process when an new equation is added to a congruence closure. Also, `Lean.Expr.relSidesIfSymm?` is removed in #11162, but this def is required for `cc` tactic, so we recover this. Co-authored-by: Pol'tta / Miyahara Kō <52843868+Komyyy@users.noreply.github.com>
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.
In this PR, we implements process when an new equation is added to a congruence closure.
Also,
Lean.Expr.relSidesIfSymm?is removed in #11162, but this def is required forcctactic, so we recover this.cctactic (1/3) #11956