Documentation

Batteries.Tactic.Init

Simple tactics that are used throughout Batteries. #

_ in tactic position acts like the done tactic: it fails and gives the list of goals if there are any. It is useful as a placeholder after starting a tactic block such as by _ to make it syntactically correct and show the current goal.

Equations
Instances For

    Like exact, but takes a list of terms and checks that all goals are discharged after the tactic.

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

      by_contra h proves ⊢ p by contradiction, introducing a hypothesis h : ¬p and proving False.

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

        Given a proof h of p, absurd h changes the goal to ⊢ ¬ p. If p is a negation ¬q then the goal is changed to ⊢ q instead.

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

          split_ands applies And.intro until it does not make progress.

          Equations
          Instances For

            fapply e is like apply e but it adds goals in the order they appear, rather than putting the dependent goals first.

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

              eapply e is like apply e but it does not add subgoals for variables that appear in the types of other goals. Note that this can lead to a failure where there are no goals remaining but there are still metavariables in the term:

              example (h : ∀ x : Nat, x = x → True) : True := by
                eapply h
                rfl
                -- no goals
              -- (kernel) declaration has metavariables '_example'
              
              Equations
              • One or more equations did not get rendered due to their size.
              Instances For

                Deprecated variant of trivial.

                Equations
                Instances For

                  conv tactic to close a goal using an equality theorem.

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

                    The conv tactic equals claims that the currently focused subexpression is equal to the given expression, and proves this claim using the given tactic.

                    example (P : (Nat → Nat) → Prop) : P (fun n => n - n) := by
                      conv in (_ - _) => equals 0 =>
                        -- current goal: ⊢ n - n = 0
                        apply Nat.sub_self
                      -- current goal: P (fun n => 0)
                    
                    Equations
                    • One or more equations did not get rendered due to their size.
                    Instances For