Natural Numbers Game (Buzzard)

11 flashcards · Mathematics · by lakesare

1. Give a catchphrase for refl.

   Update goal: Solve A=A

2. Give a catchphrase for rw (h : A=B).

   Update goal: Detect all As, supersede with B

3. What are these theorems about: zero_add add_zero

   zero_add : what happens when we zero add smth add_zero : what happens when we smth add zero

4. Give a catchphrase for induction (n : Nat).

   Fork goal: 1) prove base case 2) prove inductive case

5. Give a catchphrase for simp.

   Update goal: Use all @[simp] lemmas to rw a goal. ⊢ a * t_n + b * t_n + (a + b) = a * t_n + a + (b * t_n + b) simp ⊢ Proof complete!

6. Give a cathphrase for: cases split

   cases - cases SOMETHING (affects the hypothesis) split - split (affects the goal)

7. Give a cathphrase for by_cases.

   Throw a truth table at it! Interestingly, by_cases assumes we have Classical.em.

8. Give catchphrases for what we should do: If we see = If we see →

   If we see =, we should do rw! rw/reflIf we see →, we should do apply! exact/intro/have/apply

9. Visually imagine what are these about exact/intro/have/apply. To manipulate functions effectively, we need to learn about a new collection of tactics, namely exact, intro, have and apply. These tactics are specially designed for dealing with functions.

   λ abstraction & application intro n - λ nexact n - return n

10. Give a catchphrase for simp.

    Mb good for mazes wait, is simp for = of for ->? i think cc might be for ->, and simp might be for =.

11. Visually imagine what a ≠ b translates into.