1a  4p

  2p Left−hand sides
  1p for each left-hand side

    * leaf alone or (leaf w): 0.5/1p
    * no constructors: 0/1p
    * inner alone: 0.5/1p
    * completely wrong parentheses: 0/0.5p

  2p Right−hand sides
  1p for each right-hand side

    * general right shape of RHS: 0.5p
      * recursive calls: 0/0.5p
    * mysterious variables on rhs: 0.5/1p

1b  4p

  1p First line of declaration
  Roughly correct, ignoring brackets

    * 0.5/1p if alpha is not declared
    * 0.5/1p if parameters and indices are mixed up or doubled
    * -0.5p if types make no sense (e.g. `tree l`)

  1p Left−hand side

    * 0.5/1p if l and r appear but with major syntactic problems

  2p Right−hand side

    * 1p for constructor and l r arguments
      * 0.5/1p if `tree` instead of `node`
      * 0.5/1p if parentheses are grossly misapplied
    * 1p for the weight argument
      * 0.5/1p if weight is used weirdly elsewhere
      * 0.5/1p for recursive sum

1c  8p

  2p By case distinction on
  By case distinction or induction (1p) on right variable (1p)

    * but no need for variable if the case distinction is on emptiness

  1p Nil case statement
  Case label (0.5p) and goal statement (0.5p)

    * but no need for goal statement if the case distinction is on emptiness

  1p Nil case proof
  Singleton list is different from empty list

    * 0.5/1p: by refl
    * 0.5/1p: no singleton in sight (vague "by definition of insort")

  1p Cons case statement
  Case label (0.5 p) and goal statement (0.5 p)

    * but no need for goal statement if the cae distinction is on emptiness

  3p Cons case proof
  Case distinction (1p) and each case (1p each)

    * 0.5/1p per case for proof by refl
    * 1/3p for "by definition of insort this does not return an empty list"

2a  7p

  1p By iff elimination
  Clearly mention how the proof starts

    * 0p if both goals are shown but no iff-intro

  1p Forward assume−show
  Assume (0.5p), show (0.5p)

  2p Forward proof
  ∧-introduction (1p) and modus ponens (1p)

  1p Backward assume−show
  Assume (0.5p), show (0.5p)

  2p Backward proof
  ∧-elimination (1p) and modus ponens (1p)

    * 0/2p for p -> q -> r becomes p -> q
    * 1/2p if swapped q and r in last step

2b  8p

  1p Statement of goal
  1p Restatement of goal expected if it's not obvious from the proof

    * missing 

  2p Exist elimination
  ∃-elimination step introducing new variable

  3p Forall instantiation and modus ponens
  Clear instantiation of ∀x, p x → q x with new variable (1p) y
  and supplying proof of p y (2p)

  2p Exist introduction
  ∃-introduction step at the end

    * 0/2p if the witness comes from nowhere

3a  6p

  2p Left−hand sides
  1p per left-hand side

    * 1.5/2p if := for :
    * 1/2p for set-theoretic nonsense

  4p Right−hand sides
  2p per right-hand side (hypothesis, conclusion: 1p each)

    * 1/2p if sc and r are mixed somehow or if rS is used for sc
    * 0.5/1p if pairs are used

3b  7p

  1p Introduction
  Clear proof frame, including first step

  4p Forward direction
  Clear labeling of direction or goal (1p)
  Case distinction (1p)
  assumption case (1p)
  hrefl case (1p)

    * 0.5/1p for refl instead of assumption

  2p Backward direction
  Clear labeling of direction or goal (1p)
  Invocation of base (1p)

    * 0.5/1p for "from left to right" etc.

4a  5p

  0/1p if wrong

    * 0.5/1p if bool for Prop
    * 0.5/1p if two answers, one wrong

4b  4p

  2p Equal
  j and k are equal

  2p Not equal
  Everything except j and k is disequal

    * remove 1p for each spurious equality
    * remove 1p if nothing is said about i or r != j, k

4c  6p

  2p Zero
  subtype.mk (1p) and arguments (1p)

    * 0/1p if either argument is wrong

  4p Addition
  subtype.mk, first argument, even.add, subtype.property (each 1p)

    * 0/4p for + on evenN

4d  3p

  3p Term
  Argument to exists_minimal_arg (1.5p) and argument to classical.some (1.5p)

    * 0.5/1.5p for missing parentheses around argument to classical.some

5a  4p

  1p Left−hand side

  3p Right−hand side
  1p for each recursive call and 1p for the addition in between

    * 2/3p for overlapping equations
    * 2.5/3p for `eval env`

5b  4p

Criterion 1 (4)

  1p Constructor and parameters
  1p No hypotheses
  1p for each argument to conclusion

  * 0p if the argument is wrong, including missing ( )

5c  8p

  1p By induction on what
  By (rule) induction (0.5p) on the hypothesis (0.5p)

  2p Num case
  Label + statement (1p), brief proof (1p)

    * 0p for too vague or wrong proof

  2p Var case
  Label + statement (1p), brief proof (1p)

    * 0p for too vague or wrong proof

  3p Add case
  Statement + other hypotheses (1p)
  Induction hypothesis (1p)
  Rest of proof (1p)

6a  6p

  4p split_hyp
  1pt per key comment (infer_type, match, tactic.cases, tactic.failed)

    * 0/1p for any substantial mistake

  2p split_once
    1p per line

    * 0.5/1p if the local context is not characterized as being a list

6b  4p

  2p point for each expected goal, with
    1p for conclusion
    1p for hypothesis

    1/4p if forgot repeat in case_bash
    2/4p if spurious hyps.
