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
        Instances For

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

          Equations
            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
                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
                        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
                            Instances For

                              Deprecated variant of trivial.

                              Equations
                                Instances For

                                  conv tactic to close a goal using an equality theorem.

                                  Equations
                                    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
                                        Instances For