Question 1  13p

1a  4p

  * 2p for pure
    * 0p if no good
  * 2p for bind
    * 0.5p for \a b, b a
  
  * -1p for each for freak syntax errors

1b  4p

  * 2p for pure_bind
    * 1p per step
    * 0p if not step-by-step calculational
  * 2p for bind_pure
    * 1p per step
      * 0.5p if only trivial step from >>= to bind
    * 0p if not step-by-step calculational

  * -0.5p for missing parens

1c  5p

  * 2p for throw
    * 0.5p for spurious catch-all good case
  * 3p for catch
    * 1p for good case
    * 2p for bad case

  * -1p for freak syntax errors
  * -0.5p for missing second argument


Question 2  19p

2a  4p

  * 1p per type
    * 0.5p bool for Prop

2b  3p

  * 3p for 1 + max a b
  * 1p for max a b
  * 0p for loopy def
  * 0p for anything else

2c  6p

  * 2p for zero
  * 2p for zero_add
    * 0p if expanding definition makes weird unbound vars appear
    * 1p if roughly half the proof is right
    * 1p if the proof is very implicit (reference to 2b only)
    * 1p if the proof doesn't split properly
  * 2p for add_zero
    * similar to zero_add

  * -0.5p globally for claiming that a : alpha

2d  4p

  * 2p for right answer
    * but 0p if justification is very wrong
    * but 1p if no justification at all is present
  * 2p for justification
    * 1p if problem not clearly stated (e.g. no counterexample)

  * 1p/4 for waffle

2e  2p

  * 2p for right answer


Question 3  16p

3a  4p

  * 2p per line
    * 1p for name + conditions
    * 1p for conclusion
      * -0.5p if odd call is missing

  * -1.5p globally for odd ... : ... := syntax
    but -1p for only := instead of :

  * -1p for spurious even 0 0case

  * -3p for a correct recursive definition
    * extra -0.5p for nonlinear pattern
    * extra -0.5p for nonpatterns
    * extra -0.5p for lemma names
  * -3p for odd recursive/inductive mixture (on a per-rule basis)

3b  4p

  * 2p per proof
    * -0.5p for spurious intro
    * -0.5p for missing args/_ in proof term, or for extra (implicit) args
    * -1p for nonworking simp call
    * -1.5p for weird dec_trivial proof where the correct lemmas were used
    * -0.5p for missing lemma name (but giving stmt)
    * -0.5p for weird comma
    * -1p for calculational proof (assuming "def" definition) without reference
      to symbol defined

3c  8p

  * 1p for "induction on h"
    * 0.5p for "cases h"
    * 0.5p for "induction" alone
    * 0p for induction on wrong thing (e.g. "induction n" but then as if
      "pal_xs")
    * 0p for proof by pattern matching
    * 0p for not-so-structural induction
  * 1.5p for correct statement of goals
    * 0.5p for one case
    * 1p for add_two case
  * 1.5p for correct statement of induction hypotheses
    * -0.5p for textual description
    * -0.5p for n + 1 instead of n in IH and goal
    * 0p for proof term instead of statement
  * 4p for correct proofs
    * 2p for zero case
      * 2p apply odd.one
    * 2p for add_one case
      * 2p apply odd.plus_two ih

  * 0p for equational proof with type-incorrect f (odd ...)


Question 4  12p

4a  3p
  * 3p: "Suppose we have different elements x, t : α, then the lhs is true
    regardless of p, but we can make the rhs false by taking p = \_, false,
    contradiction." OR
  * 3p: "The rule would imply that all x = t, which doesn't make sense." OR
  * 3p: "We cannot prove this rule because we cannot prove x = t for all x."

  Partial credit:
    * 1p: "The problem is that the LHS contains x = t." (Is this always a
      contradiction?)
    * 1p: "Replacing an → with ∧ would give a different truth value in some
      cases." (Why isn't the different truth value that it is true in more
      cases?)
    * 1p: "This would only be true for some x, as 4b shows." (Why aren't `some
      x' the same as `all x'?)
    * 2p: "We would need to prove `p x = p t', but we cannot do this for all
      x." (We don't need to prove `p x = p t', but it would be a problematic
      consequence.)

  * -1p for omitting the conclusion (e.g.: the answer ends with "The rule makes
    p t imply x = t for all x.")

4b  9p

  * 1p: start with iff.intro
    * -0.5p: proving ∃x, (x = t -> p x ↔ p t) and/or ∀...
    * -1p: proving ∃x, (x = t) -> (p x ↔ p t) and/or ∀...

  * 2p for (assume h, h t rfl : (∀ x, x = t -> p x) -> p t), i.e.
     assume hall : ∀x : α, x = t → p x,
     have hpt : p t :=
       begin
         apply hall t,
         refl
       end,
    * -1p: proving ∀x, ((x = t) -> p x -> p t) instead
    * -1p: no instantiation for ∀
    * -0.5p: forgetting to use a refl/rw
    * -1p: trying to use induction/cases on h : ∀ x, ...
    * -1p: writing `assume h, h' or equivalent to prove the -> case
  * 2p for (assume h, <t, rfl, h>), i.e.
     show ∃x : α, x = t ∧ p x,
       begin
         apply exists.intro t,
         apply and.intro,
         { refl },
         { exact hpt }
       end)
    * -0.5p: using and.elim_left and and.elim_right instead of and.intro
    * -1p: intro tactic on a goal of ∃ x, ...
    * -1p: using `simp` where `simpa` would work (e.g. to prove p t ⊢ t = t ∧ p t

  * 2p for (assume <x, p, h>, by rw [p] at h; assumption), i.e.
     assume hex : ∃x : α, x = t ∧ p x,
     /- show p x, -/
       begin
         cases hex with w h,
         cases h with hwt pw,
         rw hwt at pw,
    * -0.5p: forgetting to use a refl/rw
    * -1p: applying `h` to `t` or equivalent
    * -2p: going from ∃ x, x = t ∧ p x ⊢ p t to t = t ∧ p t ⊢ p t by exists.intro t or similar
  * 2p for (assume p x h, by rw [h] at p; assumption : p t -> ∀x, x = t -> p x), i.e.
     assume x,
     assume hxt : x = t,
     show p x,
       /- begin -/
         rw hxt,
         assumption
       end)
    * -0.5p: writing "apply (hxt : x = t)" instead of "rw hxt" (or equivalent)
    * -0.5p: forgetting to use a refl/rw


Question 5  12p

5a  8p

  * 1p for general proof structure
    * -1p for mixture of the two induction styles
  * 1.5p for correct statement of goals
    * 0.5p for var
    * 0.5p for num
    * 0.5p for plus
    * -1.5p globally for missing arguments to constructors
  * 1.5p for correct statement of induction hypotheses
    * also accept well-founded induction style IH (regrettably) but:
    * -0.5p if wf IH lacks quantifier
  * 4p for correct proofs
    * 1p for var case
      * 0.5p by def of shuffle
      * 0.5p by def of eval
      * -0.5p for spurious IH invocation
    * 1p for num case
      * 0.5p by def of shuffle
      * 0.5p by def of eval
      * -0.5p for spurious IH invocation
    * 2p for plus case
      * -2p for "nested" induction
      * 0.5p per step (shuffle_plus, IH1, IH2, eval_plus)
    * -0.5p globally for use of apply instead of rw/simp

5b  4p

  * 1p: general calc proof structure
  * 1p: regroup -> shuffle
  * 1p: eval_shuffle
  * 1p: eval_num_0


Question 6  18p

6a  6p

  * 1.5p for unless_true
  * 1.5p for unless_false
  * 1.5p for repeat_zero
  * 1.5p for repeat_succ

  * -1p per rule for small-step instead of big-step
  * -1.5p for missing evaluation of b in state

6b  6p

  * 1.5p for unless_true
  * 1.5p for unless_false
  * 1.5p for repeat_zero
  * 1.5p for repeat_succ

  * give points for the rule's being correct Lean w.r.t. the student's answer
    to 6a, not for absolute correctness

  * -0.5p for small discrepancies (e.g. S instead of repeat n S) that look like
    typos
  * -1p for bigger discrepancies

  * -0.5p globally for missing variable declarations
  * -0.5p per rule with _ in it (?)

6c  3p

  * 2p for yes
  * 1p for justification

6d  3p

  * 2p for yes
  * 1p for justification

  * exceptionally, accept "we cannot know because big-step"
