Documentation

Batteries.Tactic.Congr

congr with tactic, rcongr tactic #

Configuration options for congr & rcongr

  • closePre : Bool

    If closePre := true, it will attempt to close new goals using Eq.refl, HEq.refl, and assumption with reducible transparency.

  • closePost : Bool

    If closePost := true, it will try again on goals on which congr failed to make progress with default transparency.

Instances For

    Function elaborating Congr.Config

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

      Apply congruence (recursively) to goals of the form ⊢ f as = f bs and HEq (f as) (f bs). The optional parameter is the depth of the recursive applications. This is useful when congr is too aggressive in breaking down the goal. For example, given ⊢ f (g (x + y)) = f (g (y + x)), congr produces the goals ⊢ x = y and ⊢ y = x, while congr 2 produces the intended ⊢ x + y = y + x.

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

        Apply congruence (recursively) to goals of the form ⊢ f as = f bs and HEq (f as) (f bs).

        • congr n controls the depth of the recursive applications. This is useful when congr is too aggressive in breaking down the goal. For example, given ⊢ f (g (x + y)) = f (g (y + x)), congr produces the goals ⊢ x = y and ⊢ y = x, while congr 2 produces the intended ⊢ x + y = y + x.
        • If, at any point, a subgoal matches a hypothesis then the subgoal will be closed.
        • You can use congr with p (: n)? to call ext p (: n)? to all subgoals generated by congr. For example, if the goal is ⊢ f '' s = g '' s then congr with x generates the goal x : α ⊢ f x = g x.
        Equations
        • One or more equations did not get rendered due to their size.
        Instances For

          Recursive core of rcongr. Calls ext pats <;> congr and then itself recursively, unless ext pats <;> congr made no progress.

          Repeatedly apply congr and ext, using the given patterns as arguments for ext.

          There are two ways this tactic stops:

          • congr fails (makes no progress), after having already applied ext.
          • congr canceled out the last usage of ext. In this case, the state is reverted to before the congr was applied.

          For example, when the goal is

          ⊢ (fun x => f x + 3) '' s = (fun x => g x + 3) '' s
          

          then rcongr x produces the goal

          x : α ⊢ f x = g x
          

          This gives the same result as congr; ext x; congr.

          In contrast, congr would produce

          ⊢ (fun x => f x + 3) = (fun x => g x + 3)
          

          and congr with x (or congr; ext x) would produce

          x : α ⊢ f x + 3 = g x + 3
          
          Equations
          • One or more equations did not get rendered due to their size.
          Instances For