Theorem Proving in Lean

lemma add_succ_zero (a : mynat) : a + succ(0) = succ(a)
begin
  # Goal is `a + succ(0) = succ(a)`.
  rw add_succ,  # Apply `add_succ (a b : mynat) : a + succ(b) = succ(a + b)`.
  # Goal is `succ(a + 0) = succ(a)`.
  rw add_zero,  # Apply `add_zero (a : mynat) : a + 0 = a`.
  # Goal is `succ(a) = succ(a)`.
  relf,
  # Proof complete by reflexivity.
end```
where
    - Lemmas (or theorems) are like functions. The type signature is a set of input hypotheses and an output statement.
    - The 'tactics' like `rw` are roughly like a more sophisticated form of function application?
    - The 'code' of the proof is a set of formal manipulations that begin with the goal, and apply the hypotheses to 'eliminate' it. Each of these manipulations are reversible, so we can think of this as moving in reverse to 'build' the output statement (return value) from nothing.
        - Is it true that these are reversible? Certainly the hypotheses of a theorem imply its conclusions, but the inverse is not true in general. But importantly the manipulations are *not* function application. The output type *itself* is an equality, and the rewrite is to substitute one side of the equality with the other. This is always valid in either direction. In order to apply the rewrite, we do need the hypotheses to be satisfied. But the 'function application' is really to the ambient set of hypotheses, and the result is a gadget that lets us do the rewriting either way we want. 
- Questions I have so far:
    - what is the 'type system' here? How does it compare / relate to types in standard programming languages?
    - how exactly should I think about tactics?
        - Tactics that exist include:
            - `apply`, `exact`, `have`, `rw`, `refl`, `intro`, `induction`,
    - what are the notions of abstraction and modularity here? 
- From [Proposition world](https://www.ma.imperial.ac.uk/~buzzard/xena/natural_number_game/?world=6&level=1): Lean interprets an implication `h: P => Q` as a function from *proofs of P* to a function of *proofs of Q*.
    - To assume a proposition `P` is to assume an element of the set of *proofs of `P`*.
- 


export const _frontmatter = {"tags":["math","papers"],"created":"2021-06-09T00:00:00.000Z","modified":"2021-06-09T00:00:00.000Z"}