miscellaneous-docs/nngcheatsheet.org

• Lean syntax
• Strategies

Lean syntax

• rw takes a list of rewrite rules and applies them—left to right—so if you have a rule of the form h : a = b then rw [h] will replace all a s in the goal with b.
• rw [h] at h2 will do the same thing but in the assumption h2 instead
• rw \l [h] will reverse the direction of rewrite rule, taking a theorem of the form h : a = b and use it to rewrite all b s into a

• repeat rw [...] will apply the rewrite rules between the square brackets 0 or more times, as many times as it can

  • this is really useful when you need to do something like repeat rw [add_succ] in order to move a successor from deep inside a series of additions and pull it out to the front of the whole expression

• apply takes a theorem of the form h: A -> B, in other words a function that transforms evidence that A is true and turns it into evidence B is true, and lets you either transform a goal B into a goal A (backwards reasoning) or lets you transform an assumption A into an assumption B

  • unlike rw, apply always just takes one argument so it doesn't have the square brackets
  • apply can also just take a theorem of the form A and apply it to a goal A

• induction n with n' ih takes a number n and generates two new goals:

  • One where n is replaces with 0
  • One where n is replaces with succ n' but you get to have as an additional assumption ih which is evidence that the theorem is true for n'
  • You don't always need induction, but it's useful when you have no other "hand holds" to grip the proof with. Always stop and think if there's something easier than induction first, though.

• intro h lets you take a goal of the form A -> B and turn it into a goal of B with the assumption h : A. This is, basically, function definition and you're declaring an argument named h with type A and you get to use that h in the "body" of your "function" when making your proof

  • You can actually do multiple intro on one line like intro h1 h2 h3 in order to take a goal of A -> B -> C -> D and turn it into a goal of D with the assumptions h1 : A, h2 : B, h3 : C, &c.

    • Pop-quiz! If I have a goal of type (A -> B) -> C what is the type of h if I do intro h?
• use lets you prove an existential goal by providing an example of a thing that fits the condition

• cases lets you take apart an existential assumption and get back a thing that satisfies the proposition. You don't get to know what it is specifically, just that it is a thing

  • cases is also useful when you need to take a hypothesis of false and end the proof. Why does this work? Well, remember how in classical logic F -> q evaluates to true no matter what q is?

Strategies

• Don't use induction until after you've taken stock of what theorems might apply to the situation. If you look and don't see something that could obviously apply, then you probably need induction.
• If a proof isn't immediately obvious, try sketching it out with pen and paper instead

• When proving an existential goal, think hard about what you need

  • Again, try writing it out