Documentation

Mathlib.Tactic.CC.Addition

Process when an new equation is added to a congruence closure #

@[reducible, inline]

The monad for the cc tactic stores the current state of the tactic.

Equations
Instances For
    @[inline]

    Run a computation in the CCM monad.

    Equations
    Instances For
      @[inline]

      Update the todo field of the state.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        @[inline]

        Update the acTodo field of the state.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          @[inline]

          Update the cache field of the state.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            @[inline]

            Read the todo field of the state.

            Equations
            Instances For
              @[inline]

              Read the acTodo field of the state.

              Equations
              Instances For
                @[inline]

                Read the cache field of the state.

                Equations
                Instances For

                  Look up an entry associated with the given expression.

                  Equations
                  Instances For

                    Use the normalizer to normalize e.

                    If no normalizer was configured, returns e itself.

                    Equations
                    Instances For

                      Add a new entry to the end of the todo list.

                      See also pushEq, pushHEq and pushReflEq.

                      Equations
                      Instances For
                        @[inline]

                        Add the equality proof H : lhs = rhs to the end of the todo list.

                        Equations
                        Instances For
                          @[inline]

                          Add the heterogeneous equality proof H : HEq lhs rhs to the end of the todo list.

                          Equations
                          Instances For

                            Return the root expression of the expression's congruence class.

                            Equations
                            Instances For

                              Is e the root of its congruence class?

                              Equations
                              Instances For

                                Update the child so its parent becomes parent.

                                Equations
                                • One or more equations did not get rendered due to their size.
                                Instances For

                                  Return true iff the given function application are congruent

                                  e₁ should have the form f a and e₂ the form g b.

                                  See paper: Congruence Closure for Intensional Type Theory.

                                  Return the CongruencesKey associated with an expression of the form f a.

                                  Equations
                                  Instances For

                                    Return the SymmCongruencesKey associated with the equality lhs = rhs.

                                    Equations
                                    • One or more equations did not get rendered due to their size.
                                    Instances For

                                      Try to find a congruence theorem for an application of fn with nargs arguments, with support for HEq.

                                      Equations
                                      • One or more equations did not get rendered due to their size.
                                      Instances For

                                        Try to find a congruence theorem for the expression e with support for HEq.

                                        Equations
                                        Instances For

                                          Record the instance e and add it to the set of known defeq instances.

                                          Equations
                                          • One or more equations did not get rendered due to their size.
                                          Instances For

                                            Treat the entry associated with e as a first-order function.

                                            Equations
                                            • One or more equations did not get rendered due to their size.
                                            Instances For

                                              Update the modification time of the congruence class of e.

                                              Does the congruence class with root root have any HEq proofs?

                                              Equations
                                              • One or more equations did not get rendered due to their size.
                                              Instances For

                                                Apply symmetry to H, which is an Eq or a HEq.

                                                • If heqProofs is true, ensure the result is a HEq (otherwise it is assumed to be Eq).
                                                • If flipped is true, apply symm, otherwise keep the same direction.
                                                Equations
                                                • One or more equations did not get rendered due to their size.
                                                Instances For

                                                  In a delayed way, apply symmetry to H, which is an Eq or a HEq.

                                                  • If heqProofs is true, ensure the result is a HEq (otherwise it is assumed to be Eq).
                                                  • If flipped is true, apply symm, otherwise keep the same direction.
                                                  Equations
                                                  • One or more equations did not get rendered due to their size.
                                                  Instances For

                                                    Apply symmetry to H, which is an Eq or a HEq.

                                                    • If heqProofs is true, ensure the result is a HEq (otherwise it is assumed to be Eq).
                                                    • If flipped is true, apply symm, otherwise keep the same direction.
                                                    Equations
                                                    Instances For

                                                      Are e₁ and e₂ known to be in the same equivalence class?

                                                      Equations
                                                      • One or more equations did not get rendered due to their size.
                                                      Instances For

                                                        Is e₁ ≠ e₂ known to be true?

                                                        Note that this is stronger than not (isEqv e₁ e₂): only if we can prove they are distinct this returns true.

                                                        Equations
                                                        • One or more equations did not get rendered due to their size.
                                                        Instances For
                                                          @[inline]

                                                          Is the proposition e known to be true?

                                                          Equations
                                                          Instances For
                                                            @[inline]

                                                            Is the proposition e known to be false?

                                                            Equations
                                                            Instances For

                                                              Apply transitivity to H₁ and H₂, which are both Eq or HEq depending on heqProofs.

                                                              Equations
                                                              Instances For

                                                                Apply transitivity to H₁? and H₂, which are both Eq or HEq depending on heqProofs.

                                                                If H₁? is none, return H₂ instead.

                                                                Equations
                                                                Instances For

                                                                  Use congruence on arguments to prove lhs = rhs.

                                                                  That is, tries to prove that lhsFn lhsArgs[0] ... lhsArgs[n-1] = lhsFn rhsArgs[0] ... rhsArgs[n-1] by showing that lhsArgs[i] = rhsArgs[i] for all i.

                                                                  Fails if the head function of lhs is not that of rhs.

                                                                  If e₁ : R lhs₁ rhs₁, e₂ : R lhs₂ rhs₂ and lhs₁ = rhs₂, where R is a symmetric relation, prove R lhs₁ rhs₁ is equivalent to R lhs₂ rhs₂.

                                                                  • if lhs₁ is known to equal lhs₂, return none
                                                                  • if lhs₁ is not known to equal rhs₂, fail.

                                                                  Use congruence on arguments to prove e₁ = e₂.

                                                                  Special case: if e₁ and e₂ have the form R lhs₁ rhs₁ and R lhs₂ rhs₂ such that R is symmetric and lhs₁ = rhs₂, then use those facts instead.

                                                                  Turn a delayed proof into an actual proof term.

                                                                  Use the format of H to try and construct a proof or lhs = rhs:

                                                                  • If H = .congr, then use congruence.
                                                                  • If H = .eqTrue, try to prove lhs = True or rhs = True, if they have the format R a b, by proving a = b.
                                                                  • Otherwise, return the (delayed) proof encoded by H itself.

                                                                  If asHEq is true, then build a proof for HEq e₁ e₂. Otherwise, build a proof for e₁ = e₂. The result is none if e₁ and e₂ are not in the same equivalence class.

                                                                  @[inline]

                                                                  Build a proof for e₁ = e₂. The result is none if e₁ and e₂ are not in the same equivalence class.

                                                                  @[inline]

                                                                  Build a proof for HEq e₁ e₂. The result is none if e₁ and e₂ are not in the same equivalence class.

                                                                  Build a proof for e = True. Fails if e is not known to be true.

                                                                  Equations
                                                                  • One or more equations did not get rendered due to their size.
                                                                  Instances For

                                                                    Build a proof for e = False. Fails if e is not known to be false.

                                                                    Equations
                                                                    • One or more equations did not get rendered due to their size.
                                                                    Instances For

                                                                      Build a proof for a = b. Fails if a and b are not known to be equal.

                                                                      Equations
                                                                      • One or more equations did not get rendered due to their size.
                                                                      Instances For

                                                                        Build a proof of False if the context is inconsistent. Returns none if False is not known to be true.

                                                                        Equations
                                                                        • One or more equations did not get rendered due to their size.
                                                                        Instances For

                                                                          Auxiliary function for comparing lhs₁ ~ rhs₁ and lhs₂ ~ rhs₂, when ~ is symmetric/commutative. It returns true (equal) for a ~ b b ~ a

                                                                          Equations
                                                                          • One or more equations did not get rendered due to their size.
                                                                          Instances For

                                                                            Given k₁ := (R₁ lhs₁ rhs₁, `R₁) and k₂ := (R₂ lhs₂ rhs₂, `R₂), return true if R₁ lhs₁ rhs₁ is equivalent to R₂ lhs₂ rhs₂ modulo the symmetry of R₁ and R₂.

                                                                            Equations
                                                                            • One or more equations did not get rendered due to their size.
                                                                            Instances For

                                                                              Given e := R lhs rhs, if R is a reflexive relation and lhs is equivalent to rhs, add equality e = True.

                                                                              Equations
                                                                              • One or more equations did not get rendered due to their size.
                                                                              Instances For

                                                                                If the congruence table (congruences field) has congruent expression to e, add the equality to the todo list. If not, add e to the congruence table.

                                                                                Equations
                                                                                • One or more equations did not get rendered due to their size.
                                                                                Instances For

                                                                                  If the symm congruence table (symmCongruences field) has congruent expression to e, add the equality to the todo list. If not, add e to the symm congruence table.

                                                                                  Equations
                                                                                  • One or more equations did not get rendered due to their size.
                                                                                  Instances For

                                                                                    Given subsingleton elements a and b which are not necessarily of the same type, if the types of a and b are equivalent, add the (heterogeneous) equality proof between a and b to the todo list.

                                                                                    Equations
                                                                                    • One or more equations did not get rendered due to their size.
                                                                                    Instances For

                                                                                      Given the equivalent expressions oldRoot and newRoot the root of oldRoot is newRoot, if oldRoot has root representative of subsingletons, try to push the equality proof between their root representatives to the todo list, or update the root representative to newRoot.

                                                                                      Equations
                                                                                      • One or more equations did not get rendered due to their size.
                                                                                      Instances For

                                                                                        Get all lambda expressions in the equivalence class of e and append to r.

                                                                                        e must be the root of its equivalence class.

                                                                                        Equations
                                                                                        • One or more equations did not get rendered due to their size.
                                                                                        Instances For

                                                                                          Remove fn and expressions whose type isn't def-eq to fn's type out from lambdas, return the remaining lambdas applied to the reversed arguments.

                                                                                          Equations
                                                                                          • One or more equations did not get rendered due to their size.
                                                                                          Instances For

                                                                                            Given a, a₁ and a₁NeB : a₁ ≠ b, return a proof of a ≠ b if a and a₁ are in the same equivalence class.

                                                                                            Equations
                                                                                            • One or more equations did not get rendered due to their size.
                                                                                            Instances For

                                                                                              Given aNeB₁ : a ≠ b₁, b₁ and b, return a proof of a ≠ b if b and b₁ are in the same equivalence class.

                                                                                              Equations
                                                                                              • One or more equations did not get rendered due to their size.
                                                                                              Instances For

                                                                                                If e is of the form op e₁ e₂ where op is an associative and commutative binary operator, return the canonical form of op.

                                                                                                Equations
                                                                                                Instances For

                                                                                                  Given lhs, rhs, and header := "my header:", Trace my header: lhs = rhs.

                                                                                                  Equations
                                                                                                  • One or more equations did not get rendered due to their size.
                                                                                                  Instances For

                                                                                                    Trace the state of AC module.

                                                                                                    Equations
                                                                                                    • One or more equations did not get rendered due to their size.
                                                                                                    Instances For

                                                                                                      Return the proof of e₁ = e₂ using ac_rfl tactic.

                                                                                                      Equations
                                                                                                      • One or more equations did not get rendered due to their size.
                                                                                                      Instances For

                                                                                                        Given tr := t*r sr := s*r tEqs : t = s, return a proof for tr = sr

                                                                                                        We use a*b to denote an AC application. That is, (a*b)*(c*a) is the term a*a*b*c.

                                                                                                        Equations
                                                                                                        • One or more equations did not get rendered due to their size.
                                                                                                        Instances For

                                                                                                          Given ra := a*r sb := b*s ts := t*s tr := t*r tsEqa : t*s = a trEqb : t*r = b, return a proof for ra = sb.

                                                                                                          We use a*b to denote an AC application. That is, (a*b)*(c*a) is the term a*a*b*c.

                                                                                                          Equations
                                                                                                          Instances For

                                                                                                            Given e := lhs * r and H : lhs = rhs, return rhs * r and the proof of e = rhs * r.

                                                                                                            Equations
                                                                                                            Instances For

                                                                                                              The single step of simplifyAC.

                                                                                                              Simplifies an expression e by either simplifying one argument to the AC operator, or the whole expression.

                                                                                                              Equations
                                                                                                              • One or more equations did not get rendered due to their size.
                                                                                                              Instances For

                                                                                                                If e can be simplified by the AC module, return the simplified term and the proof term of the equality.

                                                                                                                Equations
                                                                                                                • One or more equations did not get rendered due to their size.
                                                                                                                Instances For

                                                                                                                  Insert or erase lhs to the occurrences of arg on an equality in acR.

                                                                                                                  Equations
                                                                                                                  • One or more equations did not get rendered due to their size.
                                                                                                                  Instances For

                                                                                                                    Insert or erase lhs to the occurrences of arguments of e on an equality in acR.

                                                                                                                    Equations
                                                                                                                    Instances For
                                                                                                                      @[inline]

                                                                                                                      Insert lhs to the occurrences of arguments of e on an equality in acR.

                                                                                                                      Equations
                                                                                                                      Instances For
                                                                                                                        @[inline]

                                                                                                                        Erase lhs to the occurrences of arguments of e on an equality in acR.

                                                                                                                        Equations
                                                                                                                        Instances For
                                                                                                                          @[inline]

                                                                                                                          Insert lhs to the occurrences on an equality in acR corresponding to the equality lhs := rhs.

                                                                                                                          Equations
                                                                                                                          Instances For
                                                                                                                            @[inline]

                                                                                                                            Erase lhs to the occurrences on an equality in acR corresponding to the equality lhs := rhs.

                                                                                                                            Equations
                                                                                                                            Instances For
                                                                                                                              @[inline]

                                                                                                                              Insert lhs to the occurrences of arguments of e on the right hand side of an equality in acR.

                                                                                                                              Equations
                                                                                                                              Instances For
                                                                                                                                @[inline]

                                                                                                                                Erase lhs to the occurrences of arguments of e on the right hand side of an equality in acR.

                                                                                                                                Equations
                                                                                                                                Instances For

                                                                                                                                  Try to simplify the right hand sides of equalities in acR by H : lhs = rhs.

                                                                                                                                  Equations
                                                                                                                                  • One or more equations did not get rendered due to their size.
                                                                                                                                  Instances For

                                                                                                                                    Try to simplify the left hand sides of equalities in acR by H : lhs = rhs.

                                                                                                                                    Equations
                                                                                                                                    • One or more equations did not get rendered due to their size.
                                                                                                                                    Instances For

                                                                                                                                      Given tsEqa : ts = a, for each equality trEqb : tr = b in acR where the intersection t of ts and tr is nonempty, let ts = t*s and tr := t*r, add a new equality r*a = s*b.

                                                                                                                                      Equations
                                                                                                                                      Instances For

                                                                                                                                        Process the tasks in the acTodo field.

                                                                                                                                        Equations
                                                                                                                                        • One or more equations did not get rendered due to their size.
                                                                                                                                        Instances For

                                                                                                                                          Given AC variables e₁ and e₂ which are in the same equivalence class, add the proof of e₁ = e₂ to the AC module.

                                                                                                                                          Equations
                                                                                                                                          • One or more equations did not get rendered due to their size.
                                                                                                                                          Instances For

                                                                                                                                            If the root expression of e is AC variable, add equality to AC module. If not, register the AC variable to the root entry.

                                                                                                                                            Equations
                                                                                                                                            • One or more equations did not get rendered due to their size.
                                                                                                                                            Instances For

                                                                                                                                              If e isn't an AC variable, set e as an new AC variable.

                                                                                                                                              Equations
                                                                                                                                              • One or more equations did not get rendered due to their size.
                                                                                                                                              Instances For

                                                                                                                                                Given e := op₁ (op₂ a₁ a₂) (op₃ a₃ a₄) where opₙs are canonicalized to op, internalize aₙs as AC variables and return (op (op a₁ a₂) (op a₃ a₄), args ++ #[a₁, a₂, a₃, a₄]).

                                                                                                                                                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.

                                                                                                                                                Equations
                                                                                                                                                • One or more equations did not get rendered due to their size.
                                                                                                                                                Instances For

                                                                                                                                                  The specialized internalizeCore for applications or literals.

                                                                                                                                                  Internalize e so that the congruence closure can deal with the given expression. Don't forget to process the tasks in the todo field later.

                                                                                                                                                  Propagate equality from a and b to a ↔ b.

                                                                                                                                                  Equations
                                                                                                                                                  • One or more equations did not get rendered due to their size.
                                                                                                                                                  Instances For

                                                                                                                                                    Propagate equality from a and b to a ∧ b.

                                                                                                                                                    Equations
                                                                                                                                                    • One or more equations did not get rendered due to their size.
                                                                                                                                                    Instances For

                                                                                                                                                      Propagate equality from a and b to a ∨ b.

                                                                                                                                                      Equations
                                                                                                                                                      • One or more equations did not get rendered due to their size.
                                                                                                                                                      Instances For

                                                                                                                                                        Propagate equality from a to ¬a.

                                                                                                                                                        Equations
                                                                                                                                                        • One or more equations did not get rendered due to their size.
                                                                                                                                                        Instances For

                                                                                                                                                          Propagate equality from a and b to a → b.

                                                                                                                                                          Propagate equality from p, a and b to if p then a else b.

                                                                                                                                                          Equations
                                                                                                                                                          Instances For

                                                                                                                                                            Propagate equality from a and b to disprove a = b.

                                                                                                                                                            Equations
                                                                                                                                                            • One or more equations did not get rendered due to their size.
                                                                                                                                                            Instances For

                                                                                                                                                              Propagate equality from subexpressions of e to e.

                                                                                                                                                              This method is invoked during internalization and eagerly apply basic equivalences for term e Examples:

                                                                                                                                                              • If e := cast H e', then it merges the equivalence classes of cast H e' and e'

                                                                                                                                                              In principle, we could mark theorems such as cast_eq as simplification rules, but this created problems with the builtin support for cast-introduction in the ematching module in Lean 3. TODO: check if this is now possible in Lean 4.

                                                                                                                                                              Eagerly merging the equivalence classes is also more efficient.

                                                                                                                                                              If e is a subsingleton element, push the equality proof between e and its canonical form to the todo list or register e as the canonical form of itself.

                                                                                                                                                              Add an new entry for e to the congruence closure.

                                                                                                                                                              Can we propagate equality from subexpressions of e to e?

                                                                                                                                                              Equations
                                                                                                                                                              Instances For

                                                                                                                                                                Remove parents of e from the congruence table and the symm congruence table, and append parents to propagate equality, to parentsToPropagate. Returns the new value of parentsToPropagate.

                                                                                                                                                                Equations
                                                                                                                                                                • One or more equations did not get rendered due to their size.
                                                                                                                                                                Instances For

                                                                                                                                                                  The fields target and proof in e's entry are encoding a transitivity proof Let e.rootTarget and e.rootProof denote these fields.

                                                                                                                                                                  e = e.rootTarget            := e.rootProof
                                                                                                                                                                  _ = e.rootTarget.rootTarget := e.rootTarget.rootProof
                                                                                                                                                                   ...
                                                                                                                                                                  _ = e.root                  := ...
                                                                                                                                                                  

                                                                                                                                                                  The transitivity proof eventually reaches the root of the equivalence class. This method "inverts" the proof. That is, the target goes from e.root to e after we execute it.

                                                                                                                                                                  Traverse the root's equivalence class, and for each function application, collect the function's equivalence class root.

                                                                                                                                                                  Equations
                                                                                                                                                                  • One or more equations did not get rendered due to their size.
                                                                                                                                                                  Instances For

                                                                                                                                                                    Reinsert parents of e to the congruence table and the symm congruence table.

                                                                                                                                                                    Together with removeParents, this allows modifying parents of an expression.

                                                                                                                                                                    Equations
                                                                                                                                                                    • One or more equations did not get rendered due to their size.
                                                                                                                                                                    Instances For

                                                                                                                                                                      Check for integrity of the CCStructure.

                                                                                                                                                                      Equations
                                                                                                                                                                      Instances For

                                                                                                                                                                        For each fnRoot in fnRoots traverse its parents, and look for a parent prefix that is in the same equivalence class of the given lambdas.

                                                                                                                                                                        remark All expressions in lambdas are in the same equivalence class

                                                                                                                                                                        Equations
                                                                                                                                                                        • One or more equations did not get rendered due to their size.
                                                                                                                                                                        Instances For

                                                                                                                                                                          Given c a constructor application, if p is a projection application (not .proj _ _ _, but .app (.const projName _) _) such that major premise is equal to c, then propagate new equality.

                                                                                                                                                                          Example: if p is of the form b.fst, c is of the form (x, y), and b = c, we add the equality (x, y).fst = x

                                                                                                                                                                          Equations
                                                                                                                                                                          • One or more equations did not get rendered due to their size.
                                                                                                                                                                          Instances For

                                                                                                                                                                            Given a new equality e₁ = e₂, where e₁ and e₂ are constructor applications. Implement the following implications:

                                                                                                                                                                            c a₁ ... aₙ = c b₁ ... bₙ => a₁ = b₁, ..., aₙ = bₙ
                                                                                                                                                                            
                                                                                                                                                                            c₁ ... = c₂ ... => False
                                                                                                                                                                            

                                                                                                                                                                            where c, c₁ and c₂ are constructors

                                                                                                                                                                            Equations
                                                                                                                                                                            • One or more equations did not get rendered due to their size.
                                                                                                                                                                            Instances For

                                                                                                                                                                              Given an injective theorem val : type, whose type is the form of a₁ = a₂ ∧ HEq b₁ b₂ ∧ .., destruct val and push equality proofs to the todo list.

                                                                                                                                                                              Derive contradiction if we can get equality between different values.

                                                                                                                                                                              Equations
                                                                                                                                                                              • One or more equations did not get rendered due to their size.
                                                                                                                                                                              Instances For

                                                                                                                                                                                Propagate equality from a ∧ b = True to a = True and b = True.

                                                                                                                                                                                Equations
                                                                                                                                                                                • One or more equations did not get rendered due to their size.
                                                                                                                                                                                Instances For

                                                                                                                                                                                  Propagate equality from a ∨ b = False to a = False and b = False.

                                                                                                                                                                                  Equations
                                                                                                                                                                                  • One or more equations did not get rendered due to their size.
                                                                                                                                                                                  Instances For

                                                                                                                                                                                    Propagate equality from ¬a to a.

                                                                                                                                                                                    Equations
                                                                                                                                                                                    • One or more equations did not get rendered due to their size.
                                                                                                                                                                                    Instances For

                                                                                                                                                                                      Propagate equality from (a = b) = True to a = b.

                                                                                                                                                                                      Equations
                                                                                                                                                                                      • One or more equations did not get rendered due to their size.
                                                                                                                                                                                      Instances For

                                                                                                                                                                                        Propagate equality from ¬∃ x, p x to ∀ x, ¬p x.

                                                                                                                                                                                        Equations
                                                                                                                                                                                        • One or more equations did not get rendered due to their size.
                                                                                                                                                                                        Instances For

                                                                                                                                                                                          Propagate equality from e to subexpressions of e.

                                                                                                                                                                                          Equations
                                                                                                                                                                                          • One or more equations did not get rendered due to their size.
                                                                                                                                                                                          Instances For

                                                                                                                                                                                            Performs one step in the process when the new equation is added.

                                                                                                                                                                                            Here, H contains the proof that e₁ = e₂ (if heqProof is false) or HEq e₁ e₂ (if heqProof is true).

                                                                                                                                                                                            Equations
                                                                                                                                                                                            • One or more equations did not get rendered due to their size.
                                                                                                                                                                                            Instances For

                                                                                                                                                                                              The auxiliary definition for addEqvStep to flip the input.

                                                                                                                                                                                              Equations
                                                                                                                                                                                              • One or more equations did not get rendered due to their size.
                                                                                                                                                                                              Instances For

                                                                                                                                                                                                Process the tasks in the todo field.

                                                                                                                                                                                                Equations
                                                                                                                                                                                                • One or more equations did not get rendered due to their size.
                                                                                                                                                                                                Instances For

                                                                                                                                                                                                  Internalize e so that the congruence closure can deal with the given expression.

                                                                                                                                                                                                  Equations
                                                                                                                                                                                                  Instances For

                                                                                                                                                                                                    Add H : lhs = rhs or H : HEq lhs rhs to the congruence closure. Don't forget to internalize lhs and rhs beforehand.

                                                                                                                                                                                                    Equations
                                                                                                                                                                                                    Instances For

                                                                                                                                                                                                      Add proof : type to the congruence closure.

                                                                                                                                                                                                      Instances For