[Merged by Bors] - feat: port cc tactic (3/3)#5938
Closed
Conversation
…ity/mathlib4 into port/Tactic.CC
|
This PR/issue depends on:
|
Vierkantor
reviewed
May 21, 2024
Contributor
Vierkantor
left a comment
There was a problem hiding this comment.
I'm very impressed by all the work! Just a few more comments and (assuming the extra tests pass) I think the tactic is totally ready to go!
Mathlib/Tactic/CC.lean
Outdated
Comment on lines
+206
to
+245
| /-- | ||
| The congruence closure tactic `cc` tries to solve the goal by chaining | ||
| equalities from context and applying congruence (i.e. if `a = b`, then `f a = f b`). | ||
| It is a finishing tactic, i.e. it is meant to close | ||
| the current goal, not to make some inconclusive progress. | ||
| A mostly trivial example would be: | ||
|
|
||
| ```lean | ||
| example (a b c : ℕ) (f : ℕ → ℕ) (h: a = b) (h' : b = c) : f a = f c := by | ||
| cc | ||
| ``` | ||
|
|
||
| As an example requiring some thinking to do by hand, consider: | ||
|
|
||
| ```lean | ||
| example (f : ℕ → ℕ) (x : ℕ) | ||
| (H1 : f (f (f x)) = x) (H2 : f (f (f (f (f x)))) = x) : | ||
| f x = x := by | ||
| cc | ||
| ``` | ||
|
|
||
| The tactic works by building an equality matching graph. It's a graph where | ||
| the vertices are terms and they are linked by edges if they are known to | ||
| be equal. Once you've added all the equalities in your context, you take | ||
| the transitive closure of the graph and, for each connected component | ||
| (i.e. equivalence class) you can elect a term that will represent the | ||
| whole class and store proofs that the other elements are equal to it. | ||
| You then take the transitive closure of these equalities under the | ||
| congruence lemmas. | ||
|
|
||
| The `cc` implementation in Lean does a few more tricks: for example it | ||
| derives `a = b` from `Nat.succ a = Nat.succ b`, and `Nat.succ a != Nat.zero` for any `a`. | ||
|
|
||
| * The starting reference point is Nelson, Oppen, [Fast decision procedures based on congruence | ||
| closure](http://www.cs.colorado.edu/~bec/courses/csci5535-s09/reading/nelson-oppen-congruence.pdf), | ||
| Journal of the ACM (1980) | ||
|
|
||
| * The congruence lemmas for dependent type theory as used in Lean are described in | ||
| [Congruence closure in intensional type theory](https://leanprover.github.io/papers/congr.pdf) | ||
| (de Moura, Selsam IJCAR 2016). -/ |
Contributor
There was a problem hiding this comment.
I think this docstring should be used only on the cc tactic elaborator itself (and then perhaps copied via @[inherit_doc cc]). Otherwise someone will modify one but not the other.
Suggested change
| /-- | |
| The congruence closure tactic `cc` tries to solve the goal by chaining | |
| equalities from context and applying congruence (i.e. if `a = b`, then `f a = f b`). | |
| It is a finishing tactic, i.e. it is meant to close | |
| the current goal, not to make some inconclusive progress. | |
| A mostly trivial example would be: | |
| ```lean | |
| example (a b c : ℕ) (f : ℕ → ℕ) (h: a = b) (h' : b = c) : f a = f c := by | |
| cc | |
| ``` | |
| As an example requiring some thinking to do by hand, consider: | |
| ```lean | |
| example (f : ℕ → ℕ) (x : ℕ) | |
| (H1 : f (f (f x)) = x) (H2 : f (f (f (f (f x)))) = x) : | |
| f x = x := by | |
| cc | |
| ``` | |
| The tactic works by building an equality matching graph. It's a graph where | |
| the vertices are terms and they are linked by edges if they are known to | |
| be equal. Once you've added all the equalities in your context, you take | |
| the transitive closure of the graph and, for each connected component | |
| (i.e. equivalence class) you can elect a term that will represent the | |
| whole class and store proofs that the other elements are equal to it. | |
| You then take the transitive closure of these equalities under the | |
| congruence lemmas. | |
| The `cc` implementation in Lean does a few more tricks: for example it | |
| derives `a = b` from `Nat.succ a = Nat.succ b`, and `Nat.succ a != Nat.zero` for any `a`. | |
| * The starting reference point is Nelson, Oppen, [Fast decision procedures based on congruence | |
| closure](http://www.cs.colorado.edu/~bec/courses/csci5535-s09/reading/nelson-oppen-congruence.pdf), | |
| Journal of the ACM (1980) | |
| * The congruence lemmas for dependent type theory as used in Lean are described in | |
| [Congruence closure in intensional type theory](https://leanprover.github.io/papers/congr.pdf) | |
| (de Moura, Selsam IJCAR 2016). -/ | |
| /-- Solve the metavariable using the congruence closure tactic. | |
| See the docstring on the `cc` tactic for a full explanation of how the tactic works. | |
| -/ |
Contributor
There was a problem hiding this comment.
An alternative is to keep the explanation of the algorithm (everything from "The tactic works by ..." onwards) here, removing it from the cc tactic docstring. The tactic user doesn't need to know too much about the implementation, after all.
Contributor
Author
There was a problem hiding this comment.
If we use the inherit_doc attribute on the elaborator, tactic docs can't be displayed.
Vierkantor
reviewed
May 21, 2024
Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>
Vierkantor
approved these changes
May 21, 2024
Contributor
Vierkantor
left a comment
There was a problem hiding this comment.
Great work, thank you very much! Let's Get This Merged 🎉
bors r+
Contributor
|
Pull request successfully merged into master. Build succeeded: |
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
4 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.
https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/cc.20tactic.20comes.20to.20Lean4
cctactic (2/3) #11960