Question 1  11p

1a  5p

  * 2p for Var line (1p per side)
  * 1p for Num line (0.5p per side)
  * 2p for Plus line (1p per side)
    * -0.5p if subst is passed ρ explicitly
    * -1p for freak pattern matching syntax

  * OK if parentheses are missing in LHSs or if currying/uncurrying is confused

1b  6p

  * 1p for general proof structure
    * -1p for mixture of the two induction styles
      * wf but with two IHs
      * induction e with lemma name invocation later
  * 2p for correct statement of goals
    * 0.5p for Var
    * 0.5p for Num
    * 1p for Plus
    * -1p globally for writing rho instead of (lambda x, x)
    * -1.5p globally for missing arguments to constructors
  * 1p for correct statement of induction hypotheses
    * also accep well-founded induction style IH (regrettably) but:
    * -0.5p if wf IH lacks quantifier
  * 2p for correct proofs
    * 0.5p for Var case
    * 0.5p for Num case
    * 1p for Plus case
      * -1p for "nested" induction
    * -0.5p globally for missing justifications ("by the definition of subst")
    * -0.5p globally for use of apply instead of rw/simp


Question 2  11p

2a  4p

  * 2p for pure
  * 2p for bind
  * -1p for each for freak syntax errors

2b  7p

  * 2p for pure_bind
    * 1p per step
    * 0p if not step-by-step calculational
  * 2p for bind_pure
    * 1p per step
    * 0p if not step-by-step calculational
  * 3p for bind_assoc
    * 1.5p for the lhs simplification
      * 0p if it doesnt simplify to g (f ma) (or some other reasonable option)
    * 1.5p for the rhs simplification
    * -0.5p for missing parentheses in g (f ma), if it's only syntactic
    * 0p if not step-by-step calculational
    * -0.5p for wrong weird proofs (e.g. appeal to id.pure_bind)


Question 3  18p

3a  6p

  * 2p for havoc
    * -1p if not only x is randomized
    * -1.5p if weird premise with (S, s) => (S', ...) is used
    * -1.5p if weird x := random syntax is used and x |-> s(random)
  * 2p for choose_first and choose_second
    * -1p for skip instead of S'
    * -1p if both rules have a needless (sometimes undischargeable) premise
    * -1.5p if the two rules are merged in a 2-premise rule
    * -1p if premises are used and require single step to skip
    * 0p if ite rules are given
    * 0p if a rule with choose in premise is given (no progress)
  * 2p for loop
    * if two rules are given (for looping and existing), 1p per rule
      * 0p for "self-eating loop" loop S' on the RHS
      * 0p for "single-iteration loop"
      * 0p for "loopy" looping rule (loop S, s) ==> (loop S, s')
      * 0.5p if the exit rule has a tail ;; T
      * -0.5p if one of the two rules has a "free" state s'

  * -1.5p per rule group for weird "or" syntax
  * -1p per rule group for big-step instead of small-step (0.5p per rule of
    2-rule groups)
  * -1p per rule group for s' instead of s

  * -2p globally if all rules are given only with a tail ;; T
  * -1p globally for spurious references to boolean conditions

3b  6p

  * 2p for havoc
    * -1p for assign in havoc rule (no such constructor)
    * -1p for serious mismatch with answer to 3a
  * 2p for choose_first and choose_second
  * 2p for loop

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

  * -1p for spurious skip rule
  * -0.5p for small discrepancies (e.g. S instead of loop S) that look like
    typos
  * -1p for bigger discrepancies

  * -0.5p globally for missing variable declarations
  * -1p per rule group for rules with _ in them

3c  3p

  * 2p for no
  * 1p for justification
    * ideally: counterexample
    * OK if they talk about havoc, choose, and/or loop
    * 0.5p if vague "many statements"
    * 0.5p if they use an assign statement in their counterexample

3d  3p

  * 2p for no
  * 1p for justification
    * ideally: counterexample
    * probabilities if answer is no: 0p

  * exceptionally, give 3p to yes + reasonable probabilistic argument


Question 4  18p

4a  4p

  * 1p per type

4b  2p

  * 2p for (lambda x, x)

4c  6p

  * 2p for one
  * 2p for mul_one
    * 0p if expanding definition makes weird f and g appear
    * 1p if roughly half the proof is right
    * 1p if the proof is very implicit (reference to 4b only)
  * 2p for one_mul
    * similar to mul_one

  * -0.5p globally for claiming that a : alpha

4d  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 not clearly stated that inverse doesn't exist (e.g. with
      counterexample)

  * 1p/4 for waffle

4e  2p

  * 2p for right answer (abs)
    * 1p is a predicate is given, including < epsilon


Question 5  19p

5a  6p

  * 2p per line
    * 1p for name + conditions
      * -0.5p if palindrome ys condition is missing
    * 1p for conclusion
      * -0.5p if palindrome call is missing
      * -0.5p for [] instead of ()
      * -0.5p for :: instead of ++

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

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

5b  7p

  * 1p for "induction on pal_xs"
    * 0.5p for "cases pal_xs"
    * 0.5p for "induction" alone
    * 0p for induction on wrong thing (e.g. "induction xs" 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 nil case
    * 0.5p for single case
    * 0.5p for sandwich case
  * 1p for correct statement of induction hypotheses
    * -0.5p for textual description
    * 0p for proof term instead of statement
  * 3.5p for correct proofs
    * 1p for nil case
      * 1p invoke palindrome.nil
    * 1p for single case
      * 1p invoke palindrome.single
    * 1.5p for sandwich case
      * 0.5p for correct invocation of reverse_append_sandwich
      * 0.5p for correct invocation of palindrome.sandwich
      * 0.5p for correct invocation of IH
        * 0p for recursive call to rev_palindrome
        * 0p for extra step involving two goals, one of which is pal_xs

  * 0p for equational proof with type-incorrect reverse (palindrome ...)

5c  6p

  * 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 (for second and third proofs)
    * -1.5p for weird dec_trivial proof where the correct lemmas were used
    * -0.5p for missing lemma name (but giving stmt)
    * -1p for double call to palindrome.sandwich
    * -0.5p for weird comma
    * -1p for calculational proof (assuming "def" definition) without reference
      to symbol defined


Question 6  13p

6a  5p

  * 1p: start with iff.intro
    * -0.5p: proving ∀x, (x = t -> p x ↔ p t)
    * -1p: proving ∀x, (x = t) -> (p x ↔ p t)
  * 2p: (\p x h, by rw [h] at p; assumption : p t -> ∀x, x = t -> p x)
    * -0.5p: writing "apply (hxt : x = t)" instead of "rw hxt" (or equivalent)
    * -0.5p: forgetting to use a refl/rw
  * 2p: (\h, h t rfl : (∀ x, x = t -> p x) -> p t)
    * -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

6b  5p

  * 1p: start with iff.intro
  * 2p: (\<x, p, h>, by rw [p] at h; assumption)
    * -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: (\h, <t, rfl, h>)
    * -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

6c  3p
  * 3p: "Suppose we have different elements x, y : α, then for p = ..., p holds
      on x, so we conclude x = y, 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 6b 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.")
