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

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.

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.

Ordering on Expr.

Equations
@[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
@[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

CongrTheorems equipped with additional infos used by congruence closure modules.

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.

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.

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

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

Appends arguments of e to r.

Equations

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

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

Equations
@[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
@[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

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 :

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

  • mt :

    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

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

  • idx :

    Natural number associated to an expression.

  • RLHSOccs : RBACAppsSet

    AC variables that occur on the left hand side of an equality which e occurs as the left hand side of in CCState.acR.

  • RRHSOccs : RBACAppsSet

    AC variables that occur on the left hand side of an equality which e occurs as the right hand side of in CCState.acR. Don't confuse.

Instances For

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

Equations

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

@[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
@[reducible, inline]

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

Equations
@[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
@[reducible, inline]

Stores the root representatives of subsingletons, this uses FastSingleton instead of Subsingleton.

Equations
@[reducible, inline]

Stores the root representatives of .instImplicit arguments.

Equations

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.

  • entries : Entries

    Maps known expressions to their equivalence class data.

  • parents : Parents

    Maps an expression e to the expressions e occurs in.

  • congruences : Congruences

    Maps each expression to a set of expressions it might be congruent to.

  • symmCongruences : SymmCongruences

    Maps each expression to a set of expressions it might be congruent to, via the symmetrical relation.

  • subsingletonReprs : SubsingletonReprs

    Stores the root representatives of subsingletons, this uses FastSingleton instead of Subsingleton.

  • instImplicitReprs : InstImplicitReprs

    Records which instances of the same class are defeq.

  • frozePartitions : Bool

    The congruence closure module has a mode where the root of each equivalence class is marked as an interpreted/abstract value. Moreover, in this mode proof production is disabled. This capability is useful for heuristic instantiation.

  • Mapping from operators occurring in terms and their canonical representation in this module

  • opInfo : RBExprMap Bool

    Whether the canonical operator is supported by AC.

  • acEntries : RBExprMap ACEntry

    Extra Entry information used by the AC part of the tactic.

  • Records equality between ACApps.

  • inconsistent : Bool

    Returns true if the CCState is inconsistent. For example if it had both a = b and a ≠ b in it.

  • gmt :

    "Global Modification Time". gmt is a number stored on the CCState, it is compared with the modification time of a cc_entry in e-matching. See CCState.mt.

Instances For
Equations
  • One or more equations did not get rendered due to their size.
def Mathlib.Tactic.CC.CCState.mkEntryCore (ccs : CCState) (e : Lean.Expr) (interpreted constructor : Bool) :

Update the CCState by constructing and inserting a new Entry.

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

Get the root representative of the given expression.

Equations

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

Check if e is the root of the congruence class.

Equations

"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

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

Equations
def Mathlib.Tactic.CC.CCState.getRoots (ccs : CCState) (roots : Array Lean.Expr) (nonsingletonOnly : Bool) :

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.

Check for integrity of the CCState.

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

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

Equations

Search for the AC-variable (Entry.acVar) with the fewest occurrences in the LHS.

Equations

Search for the AC-variable (Entry.acVar) with the fewest occurrences in the RHS.

Equations

Pretty print the entry associated with the given expression.

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

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.
Equations
  • One or more equations did not get rendered due to their size.
Equations
  • One or more equations did not get rendered due to their size.
Equations
  • One or more equations did not get rendered due to their size.
Equations
  • One or more equations did not get rendered due to their size.
Equations
  • One or more equations did not get rendered due to their size.
Equations
  • One or more equations did not get rendered due to their size.
  • ccs.ppACApps e₂_1 = ccs.ppACExpr e₂_1
Equations
  • One or more equations did not get rendered due to their size.

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).

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.