Rewrite case study on automatic differentiation
This branch completely rewrites the case study on reverse mode automatic differentiation. In particular, it makes the following changes:
- Code. We make some changes in the style of the [HH] code to allow readability. We also change the representation of constants and variables.
- Mathematical definitions. We simplify some mathematical definitions, introduce notation and improve organization.
- Specification. We make the specification much more abstract by introducing the predicate [computes]. Other than being easier to read, this version of the specification allows the verification of programs where [diff] is applied to itself.
- Verification. We also improve organization of the verification effort and add tactics. (Some proofs still need tidying though.)