Link Search Menu Expand Document

Lean Cheat Sheets

Tactics for Connectives & Quantifiers

PropositionsTo introduceTo eliminate
P β†’ Qintrofunction application
P ∧ Qsplitcases
P ∨ Qleft, rightcases
βˆƒ a : X, Hexistsicases
βˆ€ a : X, Hintrofunction application
P ↔ Qsplitcases
Β¬Pintrofunction application

Other Tactics for Logic

exact hp (prove a goal ⊒ P if you have hp : P by copying hp)

How does `exact` work?

If the goal is ⊒ X then exact hp will close the goal if and only if hp : X

theorem not_not_intro (P : Prop) :
  P β†’ ¬¬ P :=
  intro hp,
  apply not.intro,
  intro hnp,
  apply hnp,
  exact hp,

intro h (turns ⊒ P β†’ Q into h : P, ⊒ Q)

How does `intro` work?

intro hp will turn a goal ⊒ P β†’ Q into a hypothesis hp : P and goal ⊒ Q. If P and Q are sets intro p means β€œlet p be an arbitrary element of P”. If P and Q are propositions then intro hp says β€œassume P is true” (i.e. β€œlet hp be a proof of P). We also use intro to prove a universally quantified statement.

theorem forall_impl 
(A B : U β†’ Prop) : (βˆ€ x, A x β†’ B x) β†’ (βˆ€ x, A x) β†’ (βˆ€ x, B x) := 
  intro h, 
  intro u, 
  intro a, 
  have e, from u a,    
  have h_a, from h a, 
  show B a, from h_a e,   
  -- exact h_a e,  

apply h (turns h : P β†’ Q, ⊒ Q into ⊒ P)

How does `apply` work?

If you have h : P β†’ Q and your goal is ⊒ Q then apply h changes the goal to ⊒ P. If you are trying to create a proof of Q, and h is a rule which turns proofs of P into proofs of Q, then it will suffice to construct a proof of P. It is the bottom-to-top version of application. Here’s an example:

theorem curry (P Q R : Prop) : (P ∧ Q β†’ R) β†’ (P β†’ (Q β†’ R) :=
intro h,
intro hp, 
intro hq, 
apply h,  
exact hp, 
exact hq,

Puzzle: figure out what constructor does by examining what Lean tells you about your goals.

Proving Equalities With Tactics

refl (prove t = t goals)

How does `refl` work?

refl proves goals of the form t = t, and more generally goals of the form t ~ t where ~ is any reflexive binary relation.

example (a b c d : β„•) : (a + b) * (c + d) = (a + b) * (c + d) := 

rw h (use a proof h : x = y to change xs to ys)

How does `rw` work?

The rw tactic corresponds to the substitution rule of equality which we discussed in the lecture on the equality predicate. If h is a proof of A = B (i.e. h : x = y), then rw h will change all xs in the goal to ys. Variants: rw ←h (get the backward arrow with \l) changes y to x and rw h at u (changes x to y in hypothesis u instead of the goal). Here is an example:

example (m n : β„•) (h : n = m + 6) : 2 * n = 2 * (m + 6) :=
rw h, 

Here is another example:

example (P Q : Prop) (h : P ↔ Β¬ Q) : (P β†’ Β¬ Β¬ P) β†’ (Β¬ Q β†’ Β¬ Β¬ Β¬  Q) := 
  rw ← h, 
  intro u, 
  exact u, 

Note that here Lean uses propositional extensionality to equate two equivalent proposition.

#check propext

simp (use relevant lemmas and hypotheses to simplify the goal)

How does `simp` work?

This tactic has several variants and it is used quite frequently. In its most basic form, simp will try to use relevant lemmas and hypotheses to simplify the goal. dsimp is similar to simp, except that it only uses definitional equalities. See here for a full guide for all usages of simp.

example : βˆ€ n : β„•,  2 β‰  2 * 2 * n := begin
  intro n, 
  cases n with d hd,
  rw nat.succ_eq_add_one, 


example (n : β„•) (h : n + 1 - 1 β‰  0) : n + 1 β‰  1 :=
  simpa using h,