# 1

## 1a (6p)

- intros x3: 2p
- apply `or.intro_left` or `or.intro_right`: 2p
- apply one of the hypotheses: 2p

Deductions:

- Confuses forall for exists: -1
- Confuses or for and: -2
- does not specify which or introduction: -0.5
- Uses non-existent tactic or.elim_left on a hypothesis: -1.5
- Uses refl at end: -1

## 1b (9p)

- apply `iff.intro`: 1p
- forward case: 4p
  - intro hypothesis: 1p
  - apply ∃-elim: 2p
  - rest: rewrite: 1p
- backward case: 4p
  - intro hypothesis and instantiate `x` with `t`: 1p
  - ∧-intro: 1p
  - `t = t`: 1p
  - `p t` by assumption: 1p

Deductions:

- Does not mention iff.intro: -1
- Does not do separate iff proofs: -6
- No exists elimination: -3
- missing backwards case: -4
- Implies use of classical.some: -0.5
- exists.intro instead of exists.elim: -2

# 2

## 2a (5p)

- correct case split: 2p
- per case 1p

Deductions:

- Does not add x in abs case: -1
- uses ++ instead of union: -1
- forgets to write union: -1
- has extra empty string cases: -1
- Treats string as a lamba in abs case: -1

## 2b (5p)

- correct case split: 1p
- var case: 1p
- abs case: 2p
- app case: 1p

Deductions:

- Does not remove x in abs case: -1
- forgets to union in app case: -0.5
- Writes vars instead of free_vars in recursion: -0.5

## 2c (7p)

- induction, correct cases and correct induction hypotheses: 2p
- var case: 1p
  - "need to show": 0.5p
  - rest of the proof: 0.5p
- abs case: 2p
  - "need to show": 0.5p
  - rest of the proof: 1.5p
- app case: 2p
  - "need to show": 0.5p
  - rest of the proof: 1.5p

Deductions:

- Missing "to show": -0.5
- Uses empty set incorrectly: -0.5
- Says rule induction on predicate instead of induction on term: -1
- cases instead of induction (wrong def meant still "successful"): -3
- Missing expansion of vars t, incomplete sequence of subsets from vars t0 to vars: -1
- Missing two cases in app case: -0.5
- Missing use of IH: -1
- Uses IH as = instead of subset: -1

# 3

## 3a (8p)

- choice rules: 3p
  - two rules that convey nondeterminism in some way: 1p
  - correct rules: 2p
- repeat rules: 5p
  - two rules that convey nondeterminism in some way: 1p
  - correct base rule: 1p
  - correct step rule: 3p
    - correct conclusion: 1p
    - correct premises: 1p each

Deductions:

- [] instead of "": -0
- includes unnecessary n for repeat rule: -1
- Choice rule has extra irrelevant premise: -0.5
- Choice rule missing premise: -0.5
- Repeat step does s ++ s with single premise: -2
- Repeat step missing repeat premise: -1
- Repeat step wrong conclusion: -1
- Repeat base has premise, doesn't go to empty: -1
- uses state case, not string: -2
- uses wrong statement (loop instead of repeat): -0.5
- repeat base goes to s instead of "": -0.5

## 3b (8p)

- one constructor per rule: 1p
- quantification over everything that appears in the rule: 1p
- correct syntax: 1p
- choice left, choice right, repeat base: 1p each
- repeat step: 2p

Deductions:

- uses := instead of ":": -0.25

# 4

## 4a (6p)

- correct syntax: 1p
- `list.pure`: 2p
- `list.bind`: 3p

Deductions:

- redundant case in the bind definition: -0p (if correct)

## 4b (9p)

- `list.pure_bind`: 5p
  - correct sequence of steps: 1p
  - expand definitions of pure/bind: 1p
  - lemma about map: 1p
  - lemma about flatten: 2p
- `list.bind_pure`: 4p
  - correct sequence of steps: 1p
  - expand definitions of pure/bind: 1p
  - lemma about flatten/map: 2p

Deductions:

- redundant case in a recursive def of bind: -1p (rest of the def was correct)
- definition expansions not step-by-step: -1p
- no steps given at all for 1st proof: -3p
- missing IH in inductive case for 2nd proof (when defined without flatten): -2p
- lemma not stated but "explained": half points
- redundant case from 4a not considered in the proofs: -1p

# 5

## 5a (4p)

- correct syntax: 1p
- case split: 1p
- base case: 0.5p
- inductive case: 1.5p

## 5b (4p)

- correct syntax: 1p
- constructors corresponding to empty and step: 1p
- empty case: 0.5p
- step case: 1.5p

Deductions:

- empty case missing altogether: -1p
- (wrong) definition in terms of `repeat`: 2p if syntax is correct
- missing hypothesis `s ∈ A` in step case: -1p

## 5c (6p)

- correct syntax: 1p
- case split: 1p
- choice case: 1p
- repeat case: 3p

Deductions:

- "kleene_star S s" instead of "kleene_star (denote S) s": -1p

# 6

## 6a (4p)

1p for each subquestion

## 6b (5p)

1p for each definition/proof

## 6c (4p)

- correct yes/no: 1p
- explanation: 3p
  - vague intuition: 2p
  - something approaching an actual proof: 1p
