Documentation

Std.Tactic.Basic

exfalso converts a goal ⊢ tgt into False by applying False.elim.

Instances For

    _ 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.

    Instances For

      fail_if_success t fails if the tactic t succeeds.

      Instances For

        rwa calls rw, then closes any remaining goals using assumption.

        Instances For

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

          Instances For

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

            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.

              Instances For

                iterate n tac runs tac exactly n times. iterate tac runs tac repeatedly until failure.

                To run multiple tactics, one can do iterate (tac₁; tac₂; ⋯) or

                iterate
                  tac₁
                  tac₂
                  ⋯
                
                Instances For

                  repeat' tac runs tac on all of the goals to produce a new list of goals, then runs tac again on all of those goals, and repeats until tac fails on all remaining goals.

                  Instances For

                    repeat1 tac applies tac to main goal at least once. If the application succeeds, the tactic is applied recursively to the generated subgoals until it eventually fails.

                    Instances For

                      subst_eqs applies subst to all equalities in the context as long as it makes progress.

                      Instances For

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

                        Instances For

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

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

                              Tries to solve the goal using a canonical proof of True, or the rfl tactic. Unlike trivial or trivial', does not use the contradiction tactic.

                              Instances For

                                conv tactic to close a goal using an equality theorem.

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