Skip to main content

Tactics

This page provides an index of the tactics we use in CS 22. It will update over the course of the semester as new tactics are introduced.

Introduction & Elimination Rules​

apply​

warning

We generally recommend using have, not apply, for implication elimination.

apply h makes use of some hypothesis h (this can be any named hypothesis in your context) and tries to match the current goal against the conclusion (consequent) of h. If it does, then it updates the goal to be the antecedent of h. Note that apply always requires an argument: writing just apply in your proof will produce a syntax error.

For example, if h : p → q, and the goal is q, then apply h changes the goal to p. In other words, apply uses h to "reason" that in order to show q, it suffices to show p.

Note that the proposition q could be complex: as long as it matches the consequent of h, then apply h will succeed. Be sure to be on the lookout for an if-then hypothesis whose consequent matches the conclusion—if its antecedent looks easier to prove than the current goal, then apply is likely a good tactic to try.

assume​

The assume tactic applies the introduction rule for implication: given a goal of the form P → Q (where P and Q could be any propositions), writing assume hp will add the hypothesis hp : P to your context and update your goal to be Q. (Recall that this is how we prove implications: we assume the antecedent, then, from that assumption, show the consequent.) On paper, the step taken by assume hp above would probably appear as something like "assume that P is true" or simply "suppose P." Note that names of hypotheses should begin with h (unless they are an inductive hypothesis in an induction proof, in which case they may begin with ih) per our naming conventions.

We also use assume to prove negations via proof by contradiction.1 Given a goal of the form ¬P, executing assume hp will add the hypothesis hp : P to your context and update your goal to be False. In other words, we want to show that supposing P to be true entails an absurd state of affairs (where "an absurd state of affairs" is formalized as "being able to prove False, something we should not be able to prove"), so that P must be false. This mirrors how we prove negations on paper: to show that "P is false," we'll usually write something like, "Assume for the sake of contradiction that P is true. Then [more steps here]. But now we've reached a contradiction, so P must be false." (Notice that we don't explicitly say that we've "proved False;" instead, this is implicit in our arrival at a contradiction. Similarly, in order to prove False in Lean, you'll want to obtain a context that's contradictory, then use the contradiction tactic.)

assumption​

If a hypothesis in your context matches the goal exactly, assumption will solve the goal. This tactic can only be used to close a goal, i.e., as the last step in a proof of a given goal. It roughly corresponds to a phrase like "as we've already assumed/shown" in a written proof.

contradiction​

The contradiction tactic applies the principle of explosion (sometimes also known by the Latin ex falso quodlibet—roughly, "from falsehood, anything [follows]"): if your context contains "obviously" impossible or contradictory claims, then contradiction can prove any goal (even one that's false). (This step is sometimes implicit in a paper proof, as when one considers some situation, shows that it entails a contradiction, and then deduces that the situation "is impossible"—implicitly discharging one's proof obligation—without explicitly invoking "explosion.") Note that this is implicitly using the elimination rule for falsehood: from contradictory claims, we can derive False; the elimination rule for False then allows us to prove anything. (contradiction combines all of this into a single step.)

Examples of contradictory contexts include any context in which you have hypotheses P and ¬P for some proposition P, as well as hypotheses like 0 = 1 and other definitional impossibilities. Note that contradiction cannot do sophisticated reasoning to deduce a contradiction from existing hypotheses: for instance, if you have hypotheses a > b and a ≤ b, contradiction will not close the goal (since a ≤ b is not syntactically the negation of a > b, even though they are logically equivalent).

eliminate​

eliminate applies elimination rules to existing hypotheses in your context. (Recall that elimination rules tell us how we can "use" or "destruct" an existing piece of knowledge of a given form.) The syntax of eliminate is eliminate h with ... where h is the hypothesis you want to "destruct" and the ... is filled in with names to be assigned to any variables or hypotheses generated by the elimination rule (the number and kind of names you supply here is determined by which elimination rule is being applied). Here is a list of common elimination rules that eliminate can apply:

  • Conjunction elimination: given a hypothesis h : p ∧ q, eliminate h with hp hq will "split apart" h into hypotheses hp : p and hq : q in your context.
  • Disjunction elimination ("proof by cases"): given a hypothesis h : p ∨ q, eliminate h with h1 h2 generates two goals, one with a hypothesis hp : p and one with a hypothesis hq : q. You'll then need to separately show that your original goal holds in each case.
  • Existential-quantification elimination ("extracting a witness"): if T is a type (like ℕ or ℤ) and P is a predicate, then given a hypothesis hex : ∃ x : T, P x, eliminate h with w hw will replace hex in your context with a value w : T and a hypothesis hw : P w. Intuitively, hex says that there's some value out there with property P, but you don't know what it is; the elimination rule applied by eliminate allows you to "get your hands on" a specific such value w (where hw reflects the fact that P does in fact hold of w).

Note that eliminate is not used for implication elimination or universal-quantification elimination: for those rules, see the have tactic.

have​

The have tactic allows you to add new hypotheses to your context. There are two main usages we'll see in this course:

  • have can be used to apply the elimination rules for universal quantification and implication, adding the resulting hypothesis to the context.

    The syntax for implication elimination (also known as modus ponens) is as follows: if your context contains hypotheses hpq : P → Q and hp : P, then have hq : Q := hpq hp will add the hypothesis hq : Q to your context. (On paper, this is analogous to writing "we know that P implies Q, and we also know P, so we can conclude Q by modus ponens.")

    The syntax for universal-quantification elimination (which corresponds to "instantiating" a universal claim at some particular value) is similar: if T is a type (like ℕ or ℤ) and you have in your context a hypothesis hp : ∀ n : T, P n and a value k : T, then have hk : P k := hp k adds the hypothesis hk : P k to your context. (This corresponds to an argument like, "we know that property P holds of any (rational/natural/integer) number, so since k is a (rational/natural/integer) number, we know P holds of k.")

  • have can also be used to create a new goal that, once discharged, will be added as a hypothesis to your context. This is a useful way of proving an ancillary result that you want to make use of later in your primary proof. The syntax for this is as follows: write have hp : P (note the lack of a := sign); this will create a new topmost goal P. Then use the { } syntax to focus that goal and prove it. Once you've finished (i.e., after your closing }), you'll now have a new hypothesis hp : P in your context.

left and right​

left and right apply the introduction rules for disjunction ("or"). Intuitively, they are used to "target" one side of a disjunctive (∨) proposition in the goal. When presented with a disjunction in your goal, your first instinct should generally be to use left or right to isolate one of the two propositions, then prove that selected goal.

For example, given a goal of p ∨ q, left would make the goal p, while right would make the goal q. This corresponds in a paper proof to reasoning along the lines of, "we need to show that either P holds or Q holds; we'll show that P [or, respectively, Q] holds." When deciding which of left or right to use, look at the two sides of your goal and what hypotheses you have in your context: if one side looks easier to prove than the other, try to prove that side!

split_goal​

The split_goal tactic applies the introduction rule for conjunction: if your goal is of the form p ∧ q, then split_goal will turn that into two separate goals p and q. split_goal also applies the introduction rule for bi-implication, turning a goal of p ↔ q into two goals p → q and q → p. (You can think of bi-implication as behaving like the conjunction of these two implications; thus, we use the same tactic for its introduction rule.) split_goal does not apply introduction rules for other connectives (such as disjunction or implication) because those connectives' introduction rules don't correspond to "splitting the goal!"

Working with Numbers​

Rewriting and Simplifying​

Set Theory​

Induction​

Footnotes​

  1. Note that we are using this term slightly differently from what you may see in a logic class. ↩