miscellaneous-docs/stgcheatsheet.org

• Lean syntax
• On the true nature of things
• 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

• 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?
• obtain \<x,hX\> := blah lets you take a blah that's an existential type and turn it into an x that satisfies the predicate and a proof hX that x satisfies the predicate
• left let's you choose the left side of an or, i.e. it turns a goal of A \/ B and turns it into a goal of A
• right let's you choose the right side of an or, i.e. it turns a goal of A \/ B and turns it into a goal of B

On the true nature of things

• x \in A \cup B is an or-statement that can be broken up into two subgoals by cases'
• x \in A \cap B is an and-statement that can be broken into two hypotheses by cases'

Strategies

• 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 before you use something

  • Again, try writing it out
• Always take apart your existentials and ors in the hypotheses before make a left, right, or use choice in your goals