# Project 2

Project 2 involves the construction of several modules defining stacks.

Start with these inductive types for defining the structure representing stacks and stack values:

```
Inductive SC : Type :=
| Value : nat -> SC
| Unknown : SC.
Inductive NatStack : Type :=
| Empty : NatStack
| Add : nat -> NatStack -> NatStack.
```

Note that `Add`

is just the push constructor, but I’ve named it `Add`

to avoid confusion in the specification when we start talking about the `push`

operator. Feel free to add `Notation`

definitions should you desire.

### Problem 1

- Define
`push`

, `pop`

, `top`

, and `isEmpty`

operations for the `NatStack`

.
- Using Coq comments, define preconditions, postconditions, and invariants for each operation.
- For each function, prove your invariants and postconditions. Remember that any preconditions you define can be used as assumptions for postconditions.

All operations will have postconditions, but not all operations will have preconditions and invariants. Your functions should implement runtime checks to make sure they do not crash for any input.

### Problem 2

- Define
`push`

, `pop`

, `top`

, and `isEmpty`

for a `Stack`

that is parameterized over the stack element.
- Redo your proofs from Problem 1.
- Using a Coq example, explain why (pop (pop (push y (push x empty)))) is safe and will not crash for arbitrary x and y.
- Using a Coq example, explain why
`(pop (pop (push x empty))`

is unsafe, but will not crash for arbitrary x.

### Problem 3

- Define
`push`

, `pop`

, `top`

and `isEmpty`

again for your parameterized `Stack`

type moving the runtime checks into the type system.
- Redo your proofs from Problem 1.
- Using a Coq example, explain why (pop (pop (push y (push x empty)))) is safe and will not crash for arbitrary x and y.
- Using a Coq example, explain why
`(pop (pop (push x empty))`

is unsafe, but will not crash for arbitrary x. (Hint: Show it will never run.)