Documentation

Lean.Meta.Tactic.Grind.Types

We use this auxiliary constant to mark delayed congruence proofs.

Equations
    Instances For

      Returns true if e is True, False, or a literal value. See Lean.Meta.LitValues for supported literals.

      Equations
        Instances For

          Context for GrindM monad.

          • simpMethods : Simp.Methods
          • config : Grind.Config
          • cheapCases : Bool

            If cheapCases is true, grind only applies cases to types that contain at most one minor premise. Recall that grind applies cases when introducing types tagged with [grind cases eager], and at Split.lean Remark: We add this option to implement the lookahead feature, we don't want to create several subgoals when performing lookahead.

          • reportMVarIssue : Bool
          Instances For

            Key for the congruence theorem cache.

            Instances For

              E-match theorems and case-splits performed by grind. Note that it may contain elements that are not needed by the final proof. For example, grind instantiated the theorem, but theorem instance was not actually used in the proof.

              Instances For
                Instances For

                  State for the GrindM monad.

                  • ShareCommon (aka Hashconsing) state.

                  • Congruence theorems generated so far. Recall that for constant symbols we rely on the reserved name feature (i.e., mkHCongrWithArityForConst?). Remark: we currently do not reuse congruence theorems

                  • simp : Simp.State
                  • trueExpr : Expr
                  • falseExpr : Expr
                  • natZExpr : Expr
                  • btrueExpr : Expr
                  • bfalseExpr : Expr
                  • lastTag : Name

                    Used to generate trace messages of the for [grind] working on <tag>, and implement the macro trace_goal.

                  • issues : List MessageData

                    Issues found during the proof search. These issues are reported to users when grind fails.

                  • trace : Trace

                    trace for grind?

                  • counters : Counters

                    Performance counters

                  Instances For
                    @[reducible, inline]
                    Equations
                      Instances For
                        @[inline]
                        def Lean.Meta.Grind.mapGrindM {m : TypeType u_1} [MonadControlT GrindM m] [Monad m] (f : {α : Type} → GrindM αGrindM α) {α : Type} (x : m α) :
                        m α
                        Equations
                          Instances For
                            def Lean.Meta.Grind.withoutReportingMVarIssues {m : TypeType u_1} {α : Type} [MonadControlT GrindM m] [Monad m] :
                            m αm α

                            withoutReportingMVarIssues x executes x without reporting metavariables found during internalization. See comment at Grind.Context.reportMVarIssue for additional details.

                            Equations
                              Instances For

                                Returns the user-defined configuration options

                                Equations
                                  Instances For

                                    Returns the internalized True constant.

                                    Equations
                                      Instances For

                                        Returns the internalized False constant.

                                        Equations
                                          Instances For

                                            Returns the internalized Bool.true.

                                            Equations
                                              Instances For

                                                Returns the internalized Bool.false.

                                                Equations
                                                  Instances For

                                                    Returns the internalized 0 : Nat numeral.

                                                    Equations
                                                      Instances For

                                                        Returns true if declName is the name of a match equation or a match congruence equation.

                                                        Equations
                                                          Instances For
                                                            def Lean.Meta.Grind.saveCases (declName : Name) (eager : Bool) :
                                                            Equations
                                                              Instances For

                                                                Returns maximum term generation that is considered during ematching.

                                                                Equations
                                                                  Instances For

                                                                    Abstracts nested proofs in e. This is a preprocessing step performed before internalization.

                                                                    Equations
                                                                      Instances For

                                                                        Applies hash-consing to e. Recall that all expressions in a grind goal have been hash-consed. We perform this step before we internalize expressions.

                                                                        Equations
                                                                          Instances For

                                                                            Returns true if e is the internalized True expression.

                                                                            Equations
                                                                              Instances For

                                                                                Returns true if e is the internalized False expression.

                                                                                Equations
                                                                                  Instances For

                                                                                    Creates a congruence theorem for a f-applications with numArgs arguments.

                                                                                    Equations
                                                                                      Instances For
                                                                                        Equations
                                                                                          Instances For

                                                                                            Stores information for a node in the egraph. Each internalized expression e has an ENode associated with it.

                                                                                            • self : Expr

                                                                                              Node represented by this ENode.

                                                                                            • next : Expr

                                                                                              Next element in the equivalence class.

                                                                                            • root : Expr

                                                                                              Root (aka canonical representative) of the equivalence class

                                                                                            • congr : Expr

                                                                                              congr is the term self is congruent to. We say self is the congruence class root if isSameExpr congr self. This field is initialized to self even if e is not an application.

                                                                                            • target? : Option Expr

                                                                                              When e was added to this equivalence class because of an equality h : e = target, then we store target here, and h at proof?.

                                                                                            • proof? : Option Expr
                                                                                            • flipped : Bool

                                                                                              Proof has been flipped.

                                                                                            • size : Nat

                                                                                              Number of elements in the equivalence class, this field is meaningless if node is not the root.

                                                                                            • interpreted : Bool

                                                                                              interpreted := true if node should be viewed as an abstract value.

                                                                                            • ctor : Bool

                                                                                              ctor := true if the head symbol is a constructor application.

                                                                                            • hasLambdas : Bool

                                                                                              hasLambdas := true if the equivalence class contains lambda expressions.

                                                                                            • heqProofs : Bool

                                                                                              If heqProofs := true, then some proofs in the equivalence class are based on heterogeneous equality.

                                                                                            • idx : Nat

                                                                                              Unique index used for pretty printing and debugging purposes.

                                                                                            • generation : Nat

                                                                                              The generation in which this enode was created.

                                                                                            • mt : Nat

                                                                                              Modification time

                                                                                            • offset? : Option Expr

                                                                                              The offset? field is used to propagate equalities from the grind congruence closure module to the offset constraints module. When grind merges two equivalence classes, and both have an associated offset? set to some e, the equality is propagated. This field is assigned during the internalization of offset terms.

                                                                                            • cutsat? : Option Expr

                                                                                              The cutsat? field is used to propagate equalities from the grind congruence closure module to the cutsat module. Its implementation is similar to the offset? field.

                                                                                            • ring? : Option Expr

                                                                                              The ring? field is used to propagate equalities from the grind congruence closure module to the comm ring module. Its implementation is similar to the offset? field.

                                                                                            Instances For
                                                                                              Equations
                                                                                                Instances For
                                                                                                  Equations
                                                                                                    Instances For

                                                                                                      New equalities and facts to be processed.

                                                                                                      Instances For
                                                                                                        @[reducible, inline]
                                                                                                        Equations
                                                                                                          Instances For
                                                                                                            structure Lean.Meta.Grind.CongrKey (enodes : ENodeMap) :

                                                                                                            Key for the congruence table. We need access to the enodes to be able to retrieve the equivalence class roots.

                                                                                                            Instances For
                                                                                                              Equations
                                                                                                                instance Lean.Meta.Grind.instBEqCongrKey {enodeMap : ENodeMap} :
                                                                                                                BEq (CongrKey enodeMap)
                                                                                                                Equations
                                                                                                                  @[reducible, inline]
                                                                                                                  Equations
                                                                                                                    Instances For
                                                                                                                      @[reducible, inline]
                                                                                                                      Equations
                                                                                                                        Instances For
                                                                                                                          @[reducible, inline]
                                                                                                                          Equations
                                                                                                                            Instances For

                                                                                                                              The E-matching module instantiates theorems using the EMatchTheorem proof and a (partial) assignment. We want to avoid instantiating the same theorem with the same assignment more than once. Therefore, we store the (pre-)instance information in set. Recall that the proofs of activated theorems have been hash-consed. The assignment contains internalized expressions, which have also been hash-consed.

                                                                                                                              Instances For
                                                                                                                                @[reducible, inline]
                                                                                                                                Equations
                                                                                                                                  Instances For

                                                                                                                                    New raw fact to be preprocessed, and then asserted.

                                                                                                                                    Instances For

                                                                                                                                      Canonicalizer state. See Canon.lean for additional details.

                                                                                                                                      Instances For

                                                                                                                                        Trace information for a case split.

                                                                                                                                        Instances For

                                                                                                                                          E-matching related fields for the grind goal.

                                                                                                                                          • Inactive global theorems. As we internalize terms, we activate theorems as we find their symbols. Local theorem provided by users are added directly into newThms.

                                                                                                                                          • gmt : Nat

                                                                                                                                            Goal modification time.

                                                                                                                                          • Active theorems that we have performed ematching at least once.

                                                                                                                                          • Active theorems that we have not performed any round of ematching yet.

                                                                                                                                          • numInstances : Nat

                                                                                                                                            Number of theorem instances generated so far

                                                                                                                                          • num : Nat

                                                                                                                                            Number of E-matching rounds performed in this goal since the last case-split.

                                                                                                                                          • preInstances : PreInstanceSet

                                                                                                                                            (pre-)instances found so far. It includes instances that failed to be instantiated.

                                                                                                                                          • nextThmIdx : Nat

                                                                                                                                            Next local E-match theorem idx.

                                                                                                                                          • matchEqNames : PHashSet Name

                                                                                                                                            match auxiliary functions whose equations have already been created and activated.

                                                                                                                                          Instances For

                                                                                                                                            Case-split information.

                                                                                                                                            • default (e : Expr) : SplitInfo

                                                                                                                                              Term e may be an inductive predicate, match-expression, if-expression, implication, etc.

                                                                                                                                            • imp (e : Expr) (h : e.isForall = true) : SplitInfo

                                                                                                                                              e is an implication and we want to split on its antecedent.

                                                                                                                                            • arg (a b : Expr) (i : Nat) (eq : Expr) : SplitInfo

                                                                                                                                              Given applications a and b, case-split on whether the corresponding i-th arguments are equal or not. The split is only performed if all other arguments are already known to be equal or are also tagged as split candidates.

                                                                                                                                            Instances For
                                                                                                                                              Equations
                                                                                                                                                Instances For
                                                                                                                                                  Equations
                                                                                                                                                    Instances For

                                                                                                                                                      Argument arg : type of an application app in SplitInfo.

                                                                                                                                                      Instances For

                                                                                                                                                        Case splitting related fields for the grind goal.

                                                                                                                                                        • num : Nat

                                                                                                                                                          Number of splits performed to get to this goal.

                                                                                                                                                        • casesTypes : CasesTypes

                                                                                                                                                          Inductive datatypes marked for case-splitting

                                                                                                                                                        • candidates : List SplitInfo

                                                                                                                                                          Case-split candidates.

                                                                                                                                                        • Case-splits that have been inserted at candidates at some point.

                                                                                                                                                        • resolved : PHashSet ENodeKey

                                                                                                                                                          Case-splits that have already been performed, or that do not have to be performed anymore.

                                                                                                                                                        • trace : List CaseTrace

                                                                                                                                                          Sequence of cases steps that generated this goal. We only use this information for diagnostics. Remark: casesTrace.length ≥ numSplits because we don't increase the counter for cases applications that generated only 1 subgoal.

                                                                                                                                                        • lookaheads : List SplitInfo

                                                                                                                                                          Lookahead "case-splits".

                                                                                                                                                        • argPosMap : Std.HashMap (Expr × Expr) (List Nat)

                                                                                                                                                          A mapping (a, b) ↦ is s.t. for each SplitInfo.arg a b i eq in candidates or lookaheads we have i ∈ is. We use this information to decide whether the split/lookahead is "ready" to be tried or not.

                                                                                                                                                        • Mapping from pairs (f, i) to a list of arguments. Each argument occurs as the i-th of an f-application. We use this information to add splits/lookaheads for triggering extensionality theorems and model-based theory combination. See addSplitCandidatesForExt.

                                                                                                                                                        Instances For

                                                                                                                                                          Clean name generator.

                                                                                                                                                          Instances For

                                                                                                                                                            The grind goal.

                                                                                                                                                            Instances For
                                                                                                                                                              Equations
                                                                                                                                                                Instances For
                                                                                                                                                                  Equations
                                                                                                                                                                    Instances For
                                                                                                                                                                      Equations
                                                                                                                                                                        Instances For
                                                                                                                                                                          @[reducible, inline]
                                                                                                                                                                          Equations
                                                                                                                                                                            Instances For
                                                                                                                                                                              @[inline]
                                                                                                                                                                              def Lean.Meta.Grind.GoalM.runCore {α : Type} (goal : Goal) (x : GoalM α) :
                                                                                                                                                                              Equations
                                                                                                                                                                                Instances For
                                                                                                                                                                                  @[inline]
                                                                                                                                                                                  def Lean.Meta.Grind.GoalM.run {α : Type} (goal : Goal) (x : GoalM α) :
                                                                                                                                                                                  Equations
                                                                                                                                                                                    Instances For
                                                                                                                                                                                      @[inline]
                                                                                                                                                                                      Equations
                                                                                                                                                                                        Instances For

                                                                                                                                                                                          Macro similar to trace[...], but it includes the trace message trace[grind] "working on <current goal>" if the tag has changed since the last trace message.

                                                                                                                                                                                          Equations
                                                                                                                                                                                            Instances For

                                                                                                                                                                                              A helper function used to mark a theorem instance found by the E-matching module. It returns true if it is a new instance and false otherwise.

                                                                                                                                                                                              Equations
                                                                                                                                                                                                Instances For
                                                                                                                                                                                                  def Lean.Meta.Grind.addNewRawFact (proof prop : Expr) (generation : Nat) :

                                                                                                                                                                                                  Adds a new fact prop with proof proof to the queue for preprocessing and the assertion.

                                                                                                                                                                                                  Equations
                                                                                                                                                                                                    Instances For
                                                                                                                                                                                                      def Lean.Meta.Grind.addTheoremInstance (thm : EMatchTheorem) (proof prop : Expr) (generation : Nat) :

                                                                                                                                                                                                      Adds a new theorem instance produced using E-matching.

                                                                                                                                                                                                      Equations
                                                                                                                                                                                                        Instances For

                                                                                                                                                                                                          Returns true if the maximum number of instances has been reached.

                                                                                                                                                                                                          Equations
                                                                                                                                                                                                            Instances For

                                                                                                                                                                                                              Returns true if the maximum number of case-splits has been reached.

                                                                                                                                                                                                              Equations
                                                                                                                                                                                                                Instances For

                                                                                                                                                                                                                  Returns true if the maximum number of E-matching rounds has been reached.

                                                                                                                                                                                                                  Equations
                                                                                                                                                                                                                    Instances For

                                                                                                                                                                                                                      Returns some n if e has already been "internalized" into the Otherwise, returns nones.

                                                                                                                                                                                                                      Equations
                                                                                                                                                                                                                        Instances For
                                                                                                                                                                                                                          @[inline]

                                                                                                                                                                                                                          Returns some n if e has already been "internalized" into the Otherwise, returns nones.

                                                                                                                                                                                                                          Equations
                                                                                                                                                                                                                            Instances For
                                                                                                                                                                                                                              Equations
                                                                                                                                                                                                                                Instances For

                                                                                                                                                                                                                                  Returns node associated with e. It assumes e has already been internalized.

                                                                                                                                                                                                                                  Equations
                                                                                                                                                                                                                                    Instances For
                                                                                                                                                                                                                                      @[inline]

                                                                                                                                                                                                                                      Returns node associated with e. It assumes e has already been internalized.

                                                                                                                                                                                                                                      Equations
                                                                                                                                                                                                                                        Instances For

                                                                                                                                                                                                                                          Returns the generation of the given term. Is assumes it has been internalized

                                                                                                                                                                                                                                          Equations
                                                                                                                                                                                                                                            Instances For

                                                                                                                                                                                                                                              Returns true if e is in the equivalence class of True.

                                                                                                                                                                                                                                              Equations
                                                                                                                                                                                                                                                Instances For

                                                                                                                                                                                                                                                  Returns true if e is in the equivalence class of False.

                                                                                                                                                                                                                                                  Equations
                                                                                                                                                                                                                                                    Instances For

                                                                                                                                                                                                                                                      Returns true if e is in the equivalence class of Bool.true.

                                                                                                                                                                                                                                                      Equations
                                                                                                                                                                                                                                                        Instances For

                                                                                                                                                                                                                                                          Returns true if e is in the equivalence class of Bool.false.

                                                                                                                                                                                                                                                          Equations
                                                                                                                                                                                                                                                            Instances For

                                                                                                                                                                                                                                                              Returns true if a and b are in the same equivalence class.

                                                                                                                                                                                                                                                              Equations
                                                                                                                                                                                                                                                                Instances For

                                                                                                                                                                                                                                                                  Returns true if the root of its equivalence class.

                                                                                                                                                                                                                                                                  Equations
                                                                                                                                                                                                                                                                    Instances For

                                                                                                                                                                                                                                                                      Returns the root element in the equivalence class of e IF e has been internalized.

                                                                                                                                                                                                                                                                      Equations
                                                                                                                                                                                                                                                                        Instances For
                                                                                                                                                                                                                                                                          @[inline]

                                                                                                                                                                                                                                                                          Returns the root element in the equivalence class of e IF e has been internalized.

                                                                                                                                                                                                                                                                          Equations
                                                                                                                                                                                                                                                                            Instances For

                                                                                                                                                                                                                                                                              Returns the root element in the equivalence class of e.

                                                                                                                                                                                                                                                                              Equations
                                                                                                                                                                                                                                                                                Instances For
                                                                                                                                                                                                                                                                                  @[inline]

                                                                                                                                                                                                                                                                                  Returns the root element in the equivalence class of e.

                                                                                                                                                                                                                                                                                  Equations
                                                                                                                                                                                                                                                                                    Instances For

                                                                                                                                                                                                                                                                                      Returns the root enode in the equivalence class of e.

                                                                                                                                                                                                                                                                                      Equations
                                                                                                                                                                                                                                                                                        Instances For

                                                                                                                                                                                                                                                                                          Returns the root enode in the equivalence class of e if it is in an equivalence class.

                                                                                                                                                                                                                                                                                          Equations
                                                                                                                                                                                                                                                                                            Instances For

                                                                                                                                                                                                                                                                                              Returns the next element in the equivalence class of e if e has been internalized in the given goal.

                                                                                                                                                                                                                                                                                              Equations
                                                                                                                                                                                                                                                                                                Instances For

                                                                                                                                                                                                                                                                                                  Returns the next element in the equivalence class of e.

                                                                                                                                                                                                                                                                                                  Equations
                                                                                                                                                                                                                                                                                                    Instances For
                                                                                                                                                                                                                                                                                                      @[inline]

                                                                                                                                                                                                                                                                                                      Returns the root element in the equivalence class of e.

                                                                                                                                                                                                                                                                                                      Equations
                                                                                                                                                                                                                                                                                                        Instances For

                                                                                                                                                                                                                                                                                                          Returns true if e has already been internalized.

                                                                                                                                                                                                                                                                                                          Equations
                                                                                                                                                                                                                                                                                                            Instances For
                                                                                                                                                                                                                                                                                                              Equations
                                                                                                                                                                                                                                                                                                                Instances For
                                                                                                                                                                                                                                                                                                                  @[inline]
                                                                                                                                                                                                                                                                                                                  Equations
                                                                                                                                                                                                                                                                                                                    Instances For
                                                                                                                                                                                                                                                                                                                      def Lean.Meta.Grind.pushEqCore (lhs rhs proof : Expr) (isHEq : Bool) :

                                                                                                                                                                                                                                                                                                                      If isHEq is false, it pushes lhs = rhs with proof to newEqs. Otherwise, it pushes HEq lhs rhs.

                                                                                                                                                                                                                                                                                                                      Equations
                                                                                                                                                                                                                                                                                                                        Instances For

                                                                                                                                                                                                                                                                                                                          Return true if a and b have the same type.

                                                                                                                                                                                                                                                                                                                          Equations
                                                                                                                                                                                                                                                                                                                            Instances For
                                                                                                                                                                                                                                                                                                                              @[inline]
                                                                                                                                                                                                                                                                                                                              def Lean.Meta.Grind.pushEqHEq (lhs rhs proof : Expr) :
                                                                                                                                                                                                                                                                                                                              Equations
                                                                                                                                                                                                                                                                                                                                Instances For
                                                                                                                                                                                                                                                                                                                                  @[inline]
                                                                                                                                                                                                                                                                                                                                  def Lean.Meta.Grind.pushEq (lhs rhs proof : Expr) :

                                                                                                                                                                                                                                                                                                                                  Pushes lhs = rhs with proof to newEqs.

                                                                                                                                                                                                                                                                                                                                  Equations
                                                                                                                                                                                                                                                                                                                                    Instances For
                                                                                                                                                                                                                                                                                                                                      @[inline]
                                                                                                                                                                                                                                                                                                                                      def Lean.Meta.Grind.pushHEq (lhs rhs proof : Expr) :

                                                                                                                                                                                                                                                                                                                                      Pushes HEq lhs rhs with proof to newEqs.

                                                                                                                                                                                                                                                                                                                                      Equations
                                                                                                                                                                                                                                                                                                                                        Instances For

                                                                                                                                                                                                                                                                                                                                          Pushes a = True with proof to newEqs.

                                                                                                                                                                                                                                                                                                                                          Equations
                                                                                                                                                                                                                                                                                                                                            Instances For

                                                                                                                                                                                                                                                                                                                                              Pushes a = False with proof to newEqs.

                                                                                                                                                                                                                                                                                                                                              Equations
                                                                                                                                                                                                                                                                                                                                                Instances For

                                                                                                                                                                                                                                                                                                                                                  Pushes a = Bool.true with proof to newEqs.

                                                                                                                                                                                                                                                                                                                                                  Equations
                                                                                                                                                                                                                                                                                                                                                    Instances For

                                                                                                                                                                                                                                                                                                                                                      Pushes a = Bool.false with proof to newEqs.

                                                                                                                                                                                                                                                                                                                                                      Equations
                                                                                                                                                                                                                                                                                                                                                        Instances For

                                                                                                                                                                                                                                                                                                                                                          Records that parent is a parent of child. This function actually stores the information in the root (aka canonical representative) of child.

                                                                                                                                                                                                                                                                                                                                                          Equations
                                                                                                                                                                                                                                                                                                                                                            Instances For

                                                                                                                                                                                                                                                                                                                                                              Returns the set of expressions e is a child of, or an expression in es equivalence class is a child of. The information is only up to date if e is the root (aka canonical representative) of the equivalence class.

                                                                                                                                                                                                                                                                                                                                                              Equations
                                                                                                                                                                                                                                                                                                                                                                Instances For

                                                                                                                                                                                                                                                                                                                                                                  Removes the entry eparents from the parent map.

                                                                                                                                                                                                                                                                                                                                                                  Equations
                                                                                                                                                                                                                                                                                                                                                                    Instances For

                                                                                                                                                                                                                                                                                                                                                                      Copy parents to the parents of root. root must be the root of its equivalence class.

                                                                                                                                                                                                                                                                                                                                                                      Equations
                                                                                                                                                                                                                                                                                                                                                                        Instances For
                                                                                                                                                                                                                                                                                                                                                                          def Lean.Meta.Grind.mkENodeCore (e : Expr) (interpreted ctor : Bool) (generation : Nat) :
                                                                                                                                                                                                                                                                                                                                                                          Equations
                                                                                                                                                                                                                                                                                                                                                                            Instances For
                                                                                                                                                                                                                                                                                                                                                                              def Lean.Meta.Grind.mkENode (e : Expr) (generation : Nat) :

                                                                                                                                                                                                                                                                                                                                                                              Creates an ENode for e if one does not already exist. This method assumes e has been hashconsed.

                                                                                                                                                                                                                                                                                                                                                                              Equations
                                                                                                                                                                                                                                                                                                                                                                                Instances For
                                                                                                                                                                                                                                                                                                                                                                                  Equations
                                                                                                                                                                                                                                                                                                                                                                                    Instances For
                                                                                                                                                                                                                                                                                                                                                                                      @[extern lean_process_new_offset_eq]

                                                                                                                                                                                                                                                                                                                                                                                      Notifies the offset constraint module that a = b where a and b are terms that have been internalized by this module.

                                                                                                                                                                                                                                                                                                                                                                                      Returns true if e is a numeral and has type Nat.

                                                                                                                                                                                                                                                                                                                                                                                      Equations
                                                                                                                                                                                                                                                                                                                                                                                        Instances For

                                                                                                                                                                                                                                                                                                                                                                                          Marks e as a term of interest to the offset constraint module. If the root of es equivalence class has already a term of interest, a new equality is propagated to the offset module.

                                                                                                                                                                                                                                                                                                                                                                                          Equations
                                                                                                                                                                                                                                                                                                                                                                                            Instances For
                                                                                                                                                                                                                                                                                                                                                                                              @[extern lean_process_cutsat_eq]

                                                                                                                                                                                                                                                                                                                                                                                              Notifies the cutsat module that a = b where a and b are terms that have been internalized by this module.

                                                                                                                                                                                                                                                                                                                                                                                              @[extern lean_process_cutsat_diseq]

                                                                                                                                                                                                                                                                                                                                                                                              Notifies the cutsat module that a ≠ b where a and b are terms that have been internalized by this module.

                                                                                                                                                                                                                                                                                                                                                                                              Returns true if e is a nonegative numeral and has type Int.

                                                                                                                                                                                                                                                                                                                                                                                              Equations
                                                                                                                                                                                                                                                                                                                                                                                                Instances For

                                                                                                                                                                                                                                                                                                                                                                                                  Returns true if e is a numeral and has type Int.

                                                                                                                                                                                                                                                                                                                                                                                                  Equations
                                                                                                                                                                                                                                                                                                                                                                                                    Instances For

                                                                                                                                                                                                                                                                                                                                                                                                      Returns true if e is a numeral supported by cutsat.

                                                                                                                                                                                                                                                                                                                                                                                                      Equations
                                                                                                                                                                                                                                                                                                                                                                                                        Instances For

                                                                                                                                                                                                                                                                                                                                                                                                          Returns true if type of t is definitionally equal to α

                                                                                                                                                                                                                                                                                                                                                                                                          Equations
                                                                                                                                                                                                                                                                                                                                                                                                            Instances For
                                                                                                                                                                                                                                                                                                                                                                                                              @[inline]

                                                                                                                                                                                                                                                                                                                                                                                                              For each equality b = c in parents, executes k b c IF

                                                                                                                                                                                                                                                                                                                                                                                                              • b = c is equal to False, and
                                                                                                                                                                                                                                                                                                                                                                                                              Equations
                                                                                                                                                                                                                                                                                                                                                                                                                Instances For

                                                                                                                                                                                                                                                                                                                                                                                                                  Given lhs and rhs that are known to be disequal, checks whether lhs and rhs have cutsat terms e₁ and e₂ attached to them, and invokes process Arith.Cutsat.processNewDiseq e₁ e₂

                                                                                                                                                                                                                                                                                                                                                                                                                  Equations
                                                                                                                                                                                                                                                                                                                                                                                                                    Instances For

                                                                                                                                                                                                                                                                                                                                                                                                                      Traverses disequalities in parents, and propagate the ones relevant to the cutsat module.

                                                                                                                                                                                                                                                                                                                                                                                                                      Equations
                                                                                                                                                                                                                                                                                                                                                                                                                        Instances For

                                                                                                                                                                                                                                                                                                                                                                                                                          Marks e as a term of interest to the cutsat module. If the root of es equivalence class has already a term of interest, a new equality is propagated to the cutsat module.

                                                                                                                                                                                                                                                                                                                                                                                                                          Equations
                                                                                                                                                                                                                                                                                                                                                                                                                            Instances For
                                                                                                                                                                                                                                                                                                                                                                                                                              @[extern lean_process_ring_eq]

                                                                                                                                                                                                                                                                                                                                                                                                                              Notifies the comm ring module that a = b where a and b are terms that have been internalized by this module.

                                                                                                                                                                                                                                                                                                                                                                                                                              @[extern lean_process_ring_diseq]

                                                                                                                                                                                                                                                                                                                                                                                                                              Notifies the comm ring module that a ≠ b where a and b are terms that have been internalized by this module.

                                                                                                                                                                                                                                                                                                                                                                                                                              Given lhs and rhs that are known to be disequal, checks whether lhs and rhs have ring terms e₁ and e₂ attached to them, and invokes process Arith.CommRing.processNewDiseq e₁ e₂

                                                                                                                                                                                                                                                                                                                                                                                                                              Equations
                                                                                                                                                                                                                                                                                                                                                                                                                                Instances For

                                                                                                                                                                                                                                                                                                                                                                                                                                  Traverses disequalities in parents, and propagate the ones relevant to the comm ring module.

                                                                                                                                                                                                                                                                                                                                                                                                                                  Equations
                                                                                                                                                                                                                                                                                                                                                                                                                                    Instances For

                                                                                                                                                                                                                                                                                                                                                                                                                                      Marks e as a term of interest to the ring module. If the root of es equivalence class has already a term of interest, a new equality is propagated to the ring module.

                                                                                                                                                                                                                                                                                                                                                                                                                                      Equations
                                                                                                                                                                                                                                                                                                                                                                                                                                        Instances For

                                                                                                                                                                                                                                                                                                                                                                                                                                          Returns true is e is the root of its congruence class.

                                                                                                                                                                                                                                                                                                                                                                                                                                          Equations
                                                                                                                                                                                                                                                                                                                                                                                                                                            Instances For

                                                                                                                                                                                                                                                                                                                                                                                                                                              Returns the root of the congruence class containing e.

                                                                                                                                                                                                                                                                                                                                                                                                                                              Return true if the goal is inconsistent.

                                                                                                                                                                                                                                                                                                                                                                                                                                              Equations
                                                                                                                                                                                                                                                                                                                                                                                                                                                Instances For
                                                                                                                                                                                                                                                                                                                                                                                                                                                  @[extern lean_grind_mk_eq_proof]

                                                                                                                                                                                                                                                                                                                                                                                                                                                  Returns a proof that a = b. It assumes a and b are in the same equivalence class, and have the same type.

                                                                                                                                                                                                                                                                                                                                                                                                                                                  @[extern lean_grind_mk_heq_proof]

                                                                                                                                                                                                                                                                                                                                                                                                                                                  Returns a proof that HEq a b. It assumes a and b are in the same equivalence class.

                                                                                                                                                                                                                                                                                                                                                                                                                                                  @[extern lean_grind_internalize]
                                                                                                                                                                                                                                                                                                                                                                                                                                                  opaque Lean.Meta.Grind.internalize (e : Expr) (generation : Nat) (parent? : Option Expr := none) :
                                                                                                                                                                                                                                                                                                                                                                                                                                                  @[extern lean_grind_process_new_facts]

                                                                                                                                                                                                                                                                                                                                                                                                                                                  Returns a proof that a = b if they have the same type. Otherwise, returns a proof of HEq a b. It assumes a and b are in the same equivalence class.

                                                                                                                                                                                                                                                                                                                                                                                                                                                  Equations
                                                                                                                                                                                                                                                                                                                                                                                                                                                    Instances For

                                                                                                                                                                                                                                                                                                                                                                                                                                                      Returns a proof that a = True. It assumes a and True are in the same equivalence class.

                                                                                                                                                                                                                                                                                                                                                                                                                                                      Equations
                                                                                                                                                                                                                                                                                                                                                                                                                                                        Instances For

                                                                                                                                                                                                                                                                                                                                                                                                                                                          Returns a proof that a = False. It assumes a and False are in the same equivalence class.

                                                                                                                                                                                                                                                                                                                                                                                                                                                          Equations
                                                                                                                                                                                                                                                                                                                                                                                                                                                            Instances For

                                                                                                                                                                                                                                                                                                                                                                                                                                                              Returns a proof that a = Bool.true. It assumes a and Bool.true are in the same equivalence class.

                                                                                                                                                                                                                                                                                                                                                                                                                                                              Equations
                                                                                                                                                                                                                                                                                                                                                                                                                                                                Instances For

                                                                                                                                                                                                                                                                                                                                                                                                                                                                  Returns a proof that a = Bool.false. It assumes a and Bool.false are in the same equivalence class.

                                                                                                                                                                                                                                                                                                                                                                                                                                                                  Equations
                                                                                                                                                                                                                                                                                                                                                                                                                                                                    Instances For

                                                                                                                                                                                                                                                                                                                                                                                                                                                                      Marks current goal as inconsistent without assigning mvarId.

                                                                                                                                                                                                                                                                                                                                                                                                                                                                      Equations
                                                                                                                                                                                                                                                                                                                                                                                                                                                                        Instances For
                                                                                                                                                                                                                                                                                                                                                                                                                                                                          def Lean.MVarId.assignFalseProof (mvarId : MVarId) (falseProof : Expr) :

                                                                                                                                                                                                                                                                                                                                                                                                                                                                          Assign the mvarId using the given proof of False. If type of mvarId is not False, then use False.elim.

                                                                                                                                                                                                                                                                                                                                                                                                                                                                          Equations
                                                                                                                                                                                                                                                                                                                                                                                                                                                                            Instances For

                                                                                                                                                                                                                                                                                                                                                                                                                                                                              Closes the current goal using the given proof of False and marks it as inconsistent if it is not already marked so.

                                                                                                                                                                                                                                                                                                                                                                                                                                                                              Equations
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                Instances For

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  Returns all enodes in the goal

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  Equations
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                    Instances For
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                      @[inline]

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                      Executes f to each term in the equivalence class containing e

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                      Equations
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                        Instances For
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                          @[inline]
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                          def Lean.Meta.Grind.foldEqc {α : Type} (e : Expr) (init : α) (f : ENodeαGoalM α) :

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                          Folds using f and init over the equivalence class containing e

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                          Equations
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                            Instances For
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                              Equations
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                Instances For
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  Equations
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                    Instances For
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                      Equations
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                        Instances For
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                          @[reducible, inline]
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                          Equations
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                            Instances For
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                              @[reducible, inline]
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                              Equations
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                Instances For
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  Instances For
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                    @[inline]
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                    Equations
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                      Instances For
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                        Equations
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                          Instances For
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                            Equations
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                              Instances For

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                Returns expressions in the given expression equivalence class.

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                Equations
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  Instances For
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                    partial def Lean.Meta.Grind.Goal.getEqc.go (goal : Goal) (first e : Expr) (acc : List Expr) :
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                    @[inline]

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                    Returns expressions in the given expression equivalence class.

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                    Equations
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                      Instances For

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                        Returns all equivalence classes in the current goal.

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                        Equations
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                          Instances For
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                            @[inline]

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                            Returns all equivalence classes in the current goal.

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                            Equations
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                              Instances For

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                Returns true if s has been already added to the case-split list at one point. Remark: this function returns true even if the split has already been resolved and is not in the list anymore.

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                Equations
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  Instances For

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                    Returns true if e is a case-split that does not need to be performed anymore.

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                    Equations
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                      Instances For

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                        Marks e as a case-split that does not need to be performed anymore. Remark: we currently use this feature to disable match-case-splits. Remark: we also use this feature to record the case-splits that have already been performed.

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                        Equations
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                          Instances For

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                            Inserts e into the list of case-split candidates if it was not inserted before.

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                            Equations
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                              Instances For

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                Returns extensionality theorems for the given type if available. If Config.ext is false, the result is #[].

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                Equations
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  Instances For

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                    Helper function for instantiating a type class type, and then using the result to perform isDefEq x val.

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                    Equations
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                      Instances For

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                        Add a new lookahead candidate.

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                        Equations
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                          Instances For

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                            Helper function for executing x with a fresh newFacts and without modifying the goal state.

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                            Equations
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                              Instances For