partial

nngcheatsheet.org

@@ -0,0 +1,16 @@
+* 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=?