Documentation

Mathlib.Tactic.CC.MkProof

Make proofs from a congruence closure #

@[reducible, inline]

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

Equations
    Instances For
      @[inline]

      Run a computation in the CCM monad.

      Equations
        Instances For
          @[inline]

          Update the cache field of the state.

          Equations
            Instances For
              @[inline]

              Read the cache field of the state.

              Equations
                Instances For

                  Look up an entry associated with the given expression.

                  Equations
                    Instances For

                      Use the normalizer to normalize e.

                      If no normalizer was configured, returns e itself.

                      Equations
                        Instances For

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

                          Equations
                            Instances For

                              Is e the root of its congruence class?

                              Equations
                                Instances For

                                  Return true iff the given function application are congruent

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

                                  See paper: Congruence Closure for Intensional Type Theory.

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

                                  Equations
                                    Instances For

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

                                      Equations
                                        Instances For

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

                                          Equations
                                            Instances For

                                              Update the modification time of the congruence class of e.

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

                                              Equations
                                                Instances For

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

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

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

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

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

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

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

                                                              Equations
                                                                Instances For

                                                                  Is e₁ ≠ e₂ known to be true?

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

                                                                  Equations
                                                                    Instances For
                                                                      @[inline]

                                                                      Is the proposition e known to be true?

                                                                      Equations
                                                                        Instances For
                                                                          @[inline]

                                                                          Is the proposition e known to be false?

                                                                          Equations
                                                                            Instances For

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

                                                                              Equations
                                                                                Instances For

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

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

                                                                                  Equations
                                                                                    Instances For
                                                                                      partial def Mathlib.Tactic.CC.CCM.mkCongrProofCore (lhs rhs : Lean.Expr) (heqProofs : Bool) :

                                                                                      Use congruence on arguments to prove lhs = rhs.

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

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

                                                                                      partial def Mathlib.Tactic.CC.CCM.mkSymmCongrProof (e₁ e₂ : Lean.Expr) (heqProofs : Bool) :

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

                                                                                      • if lhs₁ is known to equal lhs₂, return none
                                                                                      • if lhs₁ is not known to equal rhs₂, fail.
                                                                                      partial def Mathlib.Tactic.CC.CCM.mkCongrProof (e₁ e₂ : Lean.Expr) (heqProofs : Bool) :

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

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

                                                                                      Turn a delayed proof into an actual proof term.

                                                                                      partial def Mathlib.Tactic.CC.CCM.mkProof (lhs rhs : Lean.Expr) (H : EntryExpr) (heqProofs : Bool) :

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

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

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

                                                                                      @[inline]

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

                                                                                      @[inline]

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

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

                                                                                      Equations
                                                                                        Instances For

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

                                                                                          Equations
                                                                                            Instances For

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

                                                                                              Equations
                                                                                                Instances For

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

                                                                                                  Equations
                                                                                                    Instances For

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

                                                                                                      Equations
                                                                                                        Instances For

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

                                                                                                          Equations
                                                                                                            Instances For

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

                                                                                                              Equations
                                                                                                                Instances For

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

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

                                                                                                                  Equations
                                                                                                                    Instances For

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

                                                                                                                      Equations
                                                                                                                        Instances For

                                                                                                                          The single step of simplifyAC.

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

                                                                                                                          Equations
                                                                                                                            Instances For

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

                                                                                                                              Equations
                                                                                                                                Instances For