Documentation

Mathlib.Tactic.CC.Datatypes

Datatypes for cc #

Some of the data structures here are used in multiple parts of the tactic. We split them into their own file.

TODO #

This file is ported from C++ code, so many declarations lack documents.

Return true if e represents a constant value (numeral, character, or string).

Equations
Instances For

    Return true if e represents a value (nat/int numeral, character, or string).

    In addition to the conditions in Mathlib.Tactic.CC.isValue, this also checks that kernel computation can compare the values for equality.

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

      Given a reflexive relation R, and a proof H : a = b, build a proof for R a b

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

        Ordering on Expr.

        Equations
        Instances For
          @[reducible, inline]

          Red-black maps whose keys are Exprs.

          TODO: the choice between RBMap and HashMap is not obvious: the current version follows the Lean 3 C++ implementation. Once the cc tactic is used a lot in Mathlib, we should profile and see if HashMap could be more optimal.

          Equations
          Instances For
            @[reducible, inline]

            Red-black sets of Exprs.

            TODO: the choice between RBSet and HashSet is not obvious: the current version follows the Lean 3 C++ implementation. Once the cc tactic is used a lot in Mathlib, we should profile and see if HashSet could be more optimal.

            Equations
            Instances For

              CongrTheorems equipped with additional infos used by congruence closure modules.

              Instances For

                Automatically generated congruence lemma based on heterogeneous equality.

                This returns an annotated version of the result from Lean.Meta.mkHCongrWithArity.

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

                  Keys used to find corresponding CCCongrTheorems.

                  Instances For

                    Configs used in congruence closure modules.

                    • ignoreInstances : Bool

                      If true, congruence closure will treat implicit instance arguments as constants.

                      This means that setting ignoreInstances := false will fail to unify two definitionally equal instances of the same class.

                    • ac : Bool

                      If true, congruence closure modulo Associativity and Commutativity.

                    • If hoFns is some fns, then full (and more expensive) support for higher-order functions is only considered for the functions in fns and local functions. The performance overhead is described in the paper "Congruence Closure in Intensional Type Theory". If hoFns is none, then full support is provided for all constants.

                    • em : Bool

                      If true, then use excluded middle

                    • values : Bool

                      If true, we treat values as atomic symbols

                    Instances For
                      Equations

                      An ACApps represents either just an Expr or applications of an associative and commutative binary operator.

                      Instances For

                        Ordering on ACApps sorts .ofExpr before .apps, and sorts .apps by function symbol, then by shortlex order.

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

                          Return true iff e₁ is a "subset" of e₂.

                          Example: The result is true for e₁ := a*a*a*b*d and e₂ := a*a*a*a*b*b*c*d*d. The result is also true for e₁ := a and e₂ := a*a*a*b*c.

                          Equations
                          Instances For

                            Appends elements of the set difference e₁ \ e₂ to r. Example: given e₁ := a*a*a*a*b*b*c*d*d*d and e₂ := a*a*a*b*b*d, the result is #[a, c, d, d]

                            Precondition: e₂.isSubset e₁

                            Equations
                            • One or more equations did not get rendered due to their size.
                            • (↑e₂_2).diff e₂ r = if (e₂ == e₂_2) = true then r else r.push e₂_2
                            Instances For

                              Appends arguments of e to r.

                              Equations
                              Instances For

                                Appends elements in the intersection of e₁ and e₂ to r.

                                Equations
                                • One or more equations did not get rendered due to their size.
                                • e₁.intersection e₂ r = r
                                Instances For

                                  Converts an ACApps to an Expr. This returns none when the empty applications are given.

                                  Equations
                                  Instances For
                                    @[reducible, inline]

                                    Red-black maps whose keys are ACAppses.

                                    TODO: the choice between RBMap and HashMap is not obvious: the current version follows the Lean 3 C++ implementation. Once the cc tactic is used a lot in Mathlib, we should profile and see if HashMap could be more optimal.

                                    Equations
                                    Instances For
                                      @[reducible, inline]

                                      Red-black sets of ACAppses.

                                      TODO: the choice between RBSet and HashSet is not obvious: the current version follows the Lean 3 C++ implementation. Once the cc tactic is used a lot in Mathlib, we should profile and see if HashSet could be more optimal.

                                      Equations
                                      Instances For

                                        For proof terms generated by AC congruence closure modules, we want a placeholder as an equality proof between given two terms which will be generated by non-AC congruence closure modules later. DelayedExpr represents it using eqProof.

                                        Instances For

                                          This is used as a proof term in Entrys instead of Expr.

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

                                            Equivalence class data associated with an expression e.

                                            • next : Lean.Expr

                                              next element in the equivalence class.

                                            • root : Lean.Expr

                                              root (aka canonical) representative of the equivalence class.

                                            • cgRoot : Lean.Expr

                                              root of the congruence class, it is meaningless if e is not an application.

                                            • target : Option Lean.Expr

                                              When e was added to this equivalence class because of an equality (H : e = tgt), then we store tgt at target, and H at proof. Both fields are none if e == root

                                            • When e was added to this equivalence class because of an equality (H : e = tgt), then we store tgt at target, and H at proof. Both fields are none if e == root

                                            • Variable in the AC theory.

                                            • flipped : Bool

                                              proof has been flipped

                                            • interpreted : Bool

                                              true if the node should be viewed as an abstract value

                                            • constructor : Bool

                                              true if head symbol is a constructor

                                            • hasLambdas : Bool

                                              true if equivalence class contains lambda expressions

                                            • heqProofs : Bool

                                              heqProofs == true iff some proofs in the equivalence class are based on heterogeneous equality. We represent equality and heterogeneous equality in a single equivalence class.

                                            • fo : Bool

                                              If fo == true, then the expression associated with this entry is an application, and we are using first-order approximation to encode it. That is, we ignore its partial applications.

                                            • size : Nat

                                              number of elements in the equivalence class, it is meaningless if e != root

                                            • mt : Nat

                                              The field mt is used to implement the mod-time optimization introduce by the Simplify theorem prover. The basic idea is to introduce a counter gmt that records the number of heuristic instantiation that have occurred in the current branch. It is incremented after each round of heuristic instantiation. The field mt records the last time any proper descendant of this entry was involved in a merge.

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

                                              Stores equivalence class data associated with an expression e.

                                              Equations
                                              Instances For

                                                Equivalence class data associated with an expression e used by AC congruence closure modules.

                                                Instances For
                                                  Equations

                                                  Returns the occurrences of this entry in either the LHS or RHS.

                                                  Equations
                                                  • ent.ROccs true = ent.RLHSOccs
                                                  • ent.ROccs false = ent.RRHSOccs
                                                  Instances For

                                                    Used to record when an expression processed by cc occurs in another expression.

                                                    Instances For
                                                      @[reducible, inline]

                                                      Used to map an expression e to another expression that contains e.

                                                      When e is normalized, its parents should also change.

                                                      Equations
                                                      Instances For
                                                        Instances For
                                                          @[reducible, inline]

                                                          Maps each expression (via mkCongruenceKey) to expressions it might be congruent to.

                                                          Equations
                                                          Instances For
                                                            @[reducible, inline]

                                                            The symmetric variant of Congruences.

                                                            The Name identifies which relation the congruence is considered for. Note that this only works for two-argument relations: ModEq n and ModEq m are considered the same.

                                                            Equations
                                                            Instances For
                                                              @[reducible, inline]

                                                              Stores the root representatives of subsingletons.

                                                              Equations
                                                              Instances For
                                                                @[reducible, inline]

                                                                Stores the root representatives of .instImplicit arguments.

                                                                Equations
                                                                Instances For

                                                                  Congruence closure state. This may be considered to be a set of expressions and an equivalence class over this set. The equivalence class is generated by the equational rules that are added to the CCState and congruence, that is, if a = b then f(a) = f(b) and so on.

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

                                                                    Update the CCState by constructing and inserting a new Entry.

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

                                                                      Get the root representative of the given expression.

                                                                      Equations
                                                                      Instances For

                                                                        Get the next element in the equivalence class. Note that if the given Expr e is not in the graph then it will just return e.

                                                                        Equations
                                                                        Instances For

                                                                          Check if e is the root of the congruence class.

                                                                          Equations
                                                                          Instances For

                                                                            "Modification Time". The field mt is used to implement the mod-time optimization introduced by the Simplify theorem prover. The basic idea is to introduce a counter gmt that records the number of heuristic instantiation that have occurred in the current branch. It is incremented after each round of heuristic instantiation. The field mt records the last time any proper descendant of this entry was involved in a merge.

                                                                            Equations
                                                                            Instances For

                                                                              Is the expression in an equivalence class with only one element (namely, itself)?

                                                                              Equations
                                                                              Instances For

                                                                                Append to roots all the roots of equivalence classes in ccs.

                                                                                If nonsingletonOnly is true, we skip all the singleton equivalence classes.

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

                                                                                  Check for integrity of the CCState.

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

                                                                                    Check for integrity of the CCState.

                                                                                    Equations
                                                                                    Instances For
                                                                                      Equations
                                                                                      Instances For

                                                                                        Search for the AC-variable (Entry.acVar) with the least occurrences in the state.

                                                                                        Equations
                                                                                        • One or more equations did not get rendered due to their size.
                                                                                        • ccs.getVarWithLeastOccs (↑e₂_1) inLHS = some e₂_1
                                                                                        Instances For
                                                                                          Equations
                                                                                          • ccs.getVarWithLeastLHSOccs e = ccs.getVarWithLeastOccs e true
                                                                                          Instances For
                                                                                            Equations
                                                                                            • ccs.getVarWithLeastRHSOccs e = ccs.getVarWithLeastOccs e false
                                                                                            Instances For

                                                                                              Pretty print the entry associated with the given expression.

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

                                                                                                Pretty print the entire cc graph. If the nonSingleton argument is set to true then singleton equivalence classes will be omitted.

                                                                                                Equations
                                                                                                • One or more equations did not get rendered due to their size.
                                                                                                Instances For
                                                                                                  Equations
                                                                                                  • One or more equations did not get rendered due to their size.
                                                                                                  Instances For
                                                                                                    Equations
                                                                                                    • One or more equations did not get rendered due to their size.
                                                                                                    Instances For
                                                                                                      Equations
                                                                                                      • One or more equations did not get rendered due to their size.
                                                                                                      Instances For
                                                                                                        Equations
                                                                                                        • One or more equations did not get rendered due to their size.
                                                                                                        Instances For
                                                                                                          Equations
                                                                                                          • One or more equations did not get rendered due to their size.
                                                                                                          Instances For
                                                                                                            Equations
                                                                                                            • One or more equations did not get rendered due to their size.
                                                                                                            • ccs.ppACApps e₂_1 = ccs.ppACExpr e₂_1
                                                                                                            Instances For
                                                                                                              Equations
                                                                                                              • One or more equations did not get rendered due to their size.
                                                                                                              Instances For

                                                                                                                The congruence closure module (optionally) uses a normalizer. The idea is to use it (if available) to normalize auxiliary expressions produced by internal propagation rules (e.g., subsingleton propagator).

                                                                                                                • The congruence closure module (optionally) uses a normalizer. The idea is to use it (if available) to normalize auxiliary expressions produced by internal propagation rules (e.g., subsingleton propagator).

                                                                                                                Instances For
                                                                                                                  Instances For

                                                                                                                    CCStructure extends CCState (which records a set of facts derived by congruence closure) by recording which steps still need to be taken to solve the goal.

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