Documentation

Init.Grind.Util

def Lean.Grind.nestedProof (p : Prop) {h : p} :
p

A helper gadget for annotating nested proofs in goals.

Equations
    Instances For
      def Lean.Grind.simpMatchDiscrsOnly {α : Sort u} (a : α) :
      α

      Gadget for marking match-expressions that should not be reduced by the grind simplifier, but the discriminants should be normalized. We use it when adding instances of match-equations to prevent them from being simplified to true.

      Remark: it must not be marked as [reducible]. Otherwise, simp will reduce

      simpMatchDiscrsOnly (match 0 with | 0 => true | _ => false) = true
      

      using eq_self.

      Equations
        Instances For

          Gadget for representing offsets t+k in patterns.

          Equations
            Instances For
              def Lean.Grind.eqBwdPattern {α : Sort u_1} (a b : α) :

              Gadget for representing a = b in patterns for backward propagation.

              Equations
                Instances For
                  @[reducible, inline]
                  abbrev Lean.Grind.EqMatch {α : Sort u_1} (a b : α) {_origin : α} :

                  Gadget for annotating the equalities in match-equations conclusions. _origin is the term used to instantiate the match-equation using E-matching. When EqMatch a b origin is True, we mark origin as a resolved case-split.

                  Equations
                    Instances For
                      @[reducible, inline]

                      Gadget for annotating conditions of match equational lemmas. We use this annotation for two different reasons:

                      • We don't want to normalize them.
                      • We have a propagator for them.
                      Equations
                        Instances For

                          Similar to MatchCond, but not reducible. We use it to ensure simp will not eliminate it. After we apply simp, we replace it with MatchCond.

                          Equations
                            Instances For
                              theorem Lean.Grind.nestedProof_congr (p q : Prop) (h : p = q) (hp : p) (hq : q) :

                              A marker to indicate that a proposition has already been normalized and should not be processed again.

                              This prevents issues when case-splitting on the condition c of an if-then-else expression. Without this marker, the negated condition ¬c might be rewritten into an alternative form c', which grind may not recognize as equivalent to ¬c. As a result, grind could fail to propagate that if c then a else b simplifies to b in the ¬c branch.

                              Equations
                                Instances For

                                  Classical.em variant where disjuncts are marked with alreadyNorm gadget. See comment at alreadyNorm